diff --git a/main.bib b/main.bib index 696c48f..addee0c 100644 --- a/main.bib +++ b/main.bib @@ -196,7 +196,7 @@ @article{maietti:modular, author = {Maietti, M.}, - title = {Modular correspondence between dependent type theories and categories}, + title = {Modular correspondence between dependent type theories and categories including pretopoi and topoi}, journal = {Math. Struct. Comput. Sci.}, volume = {15}, number = {6}, @@ -379,24 +379,24 @@ note = {Book draft}, year = {2010}} -%incollection{rathjen:genind, -% author = {Rathjen, M.}, -% title = {Generalized inductive definitions in Constructive Set Theory}, -% booktitle = {From Sets and Types to Topology and Analysis: Towards Practicable Foundations for Constructive Mathematics}, -% chapter = {16}, -% editor = {Crosilla, L. and Schuster, P.}, -% publisher = {Clarendon Press}, -% series = {Oxford Logic Guides}, -% volume = {48}, -% year = {2005}} - -@article{rathjen:genind, +@incollection{rathjen:genind, author = {Rathjen, M.}, title = {Generalized inductive definitions in Constructive Set Theory}, - journal = {Oxford Logic Guides}, + booktitle = {From Sets and Types to Topology and Analysis: Towards Practicable Foundations for Constructive Mathematics}, + chapter = {16}, + editor = {Crosilla, L. and Schuster, P.}, + publisher = {Clarendon Press}, + series = {Oxford Logic Guides}, volume = {48}, year = {2005}} +%article{rathjen:genind, +% author = {Rathjen, M.}, +% title = {Generalized inductive definitions in Constructive Set Theory}, +% journal = {Oxford Logic Guides}, +% volume = {48}, +% year = {2005}} + @inproceedings{schuster-wessel:cie2020, author = {Schuster, P. and Wessel, D.}, title = {{The computational significance of Hausdorff’s maximal chain principle}}, @@ -595,3 +595,12 @@ volume = {23}, number = {2}, pages = {181--200}} + +@article{berardi-valentini:krivine, + author = {Berardi, S. and Valentini, S.}, + title = {Krivine's intuitionistic proof of classical completeness (for countable languages)}, + journal = {Ann. Pure Appl. Log.}, + volume = {129}, + number = {1--3}, + pages = {93--106}, + year = {2004}} diff --git a/main.pdf b/main.pdf index 02d287e..1b9df93 100644 Binary files a/main.pdf and b/main.pdf differ diff --git a/main.tex b/main.tex index 83ec600..11aae7f 100644 --- a/main.tex +++ b/main.tex @@ -28,7 +28,7 @@ \begin{abstract} The existence of a maximal ideal in a general nontrivial commutative ring is tied together with the axiom of choice. - Using the relative interpretation of + Following Berardi, Valentini and thus Krivine but using the relative interpretation of negation (that is, as ``implies~$0=1$'') we show, in constructive set theory with minimal logic, how for countable rings one can do without any kind of choice and without the usual decidability assumption that the ring is strongly @@ -119,7 +119,8 @@ We assume that the ring~$A$ is countable, with~$x_0, x_1, \ldots$ an enumeration of the elements of~$A$. We do \emph{not} assume that~$A$ is discrete (that is, that~$x = y$ or~$x \neq y$ for all elements of~$A$) or that it is strongly discrete (that is, that finitely generated -ideals of~$A$ are detachable). +ideals of~$A$ are detachable). Up to Corollary~\ref{cor:is-prime-max}(a) below +we follow~\cite{berardi-valentini:krivine}. We study the following recursive construction of ideals~$\mmm_0, \mmm_1, \ldots$ of~$A$: @@ -210,7 +211,7 @@ and~$\neg\neg\neg\varphi \Rightarrow \neg\varphi$ is a tautology of minimal logic.\end{remark} This first-order maximality condition is % of Proposition~\ref{prop:is-maximal} is -equivalent to the following higher-order version: For every ideal~$\nnn$ such that~$1 +equivalent~\cite{berardi-valentini:krivine} to the following higher-order version: For every ideal~$\nnn$ such that~$1 \not\in \nnn$, if~$\mmm \subseteq \nnn$, then~$\mmm = \nnn$. The quotient ring~$A/\mmm$ is a \emph{residue field} in that~$1 \neq 0$ @@ -298,7 +299,7 @@ then also~$1 \in \mmm + (x_n)$. If~$1 \not\in \mmm_n + (x_n)$, then~$x_n \in \mmm$ by Lemma~\ref{lemma:omnibus}(c). \end{proof} -It is remarkable that under the assumption of Proposition~\ref{prop:with-test}, the ideal~$\mmm$ is detachable even though in +Remarkably, under the assumption of Proposition~\ref{prop:with-test}, the ideal~$\mmm$ is detachable even though in general it fails to be finitely generated. Usually in constructive mathematics, ideals which are not finitely generated are seldom detachable. For instance the ideal~$\{ x \in \ZZ \,|\, x = 0 \vee \varphi \} \subseteq \ZZ$ is detachable if and only @@ -348,6 +349,7 @@ setup, we have the following substitute concerning complements: \[ \sqrt{(0)}^c = \bigcup_{\substack{\text{$\ppp \subseteq A$}\\\text{$\ppp$ prime}\\\text{$\ppp$ $\neg\neg$-stable}}} \ppp^c = \bigcup_{\substack{\text{$\ppp \subseteq A$}\\\text{$\ppp$ prime}\\\text{$\ppp$ radical}}} \ppp^c. \] +\newpage \begin{lemma}\label{lemma:x-prime} Let~$x \in A$. Then there is an ideal~$\ppp \subseteq A$ which is @@ -463,18 +465,18 @@ induction. Just as Corollary~\ref{cor:nilp-prime} is a constructive substitute for the recognition of the intersection of all prime ideals as the nilradical, -the following proposition is one for the -recognition of the intersection of all maximal ideals as the Jacobson radical. +the following proposition is a substitute for the classical fact that +the intersection of all maximal ideals is the Jacobson radical. % As is customary in constructive algebra~\cite[Section~IX.1]{lombardi-quitte:constructive-algebra}, by \emph{Jacobson radical} we mean the ideal $\{ x \in A \,|\, \forall y \in A\_ 1 - xy \in A^\times \}$. -An element~$x$ is said to be \emph{apart from the Jacobson radical} if and only if -there exists an element~$y \in A$ such that~$1-xy$ is not invertible. +%An element~$x$ is said to be \emph{apart} from it iff +%there is an element~$y \in A$ such that~$1-xy$ is not invertible. % In general, this condition is stronger than~$x$ merely not being an element of~$J$. -\begin{proposition}Let~$x \in A$. If~$x$ is apart from the Jacobson radical, then +\begin{proposition}Let~$x \in A$. If~$x$ is \emph{apart} from the Jacobson radical (that is, $1-xy \not\in A^\times$ for some element~$y$), then there is a maximal ideal~$\mmm$ such that~$x \not\in \mmm$. \end{proposition} @@ -568,11 +570,11 @@ a ring; such that axioms such as\par \end{align*}}% hold. This conception of arithmetized rings deviates from the usual definition in reverse mathematics~\cite[Definition~III.5.1]{simpson:subsystems} to support -quotients even when Heyting arithmetic cannot verify the existence of +quotients even when~\textsc{ha} cannot verify the existence of canonical representatives of equivalence classes. Although first-order arithmetic cannot quantify over ideals of arithmetized -rings, specific ideals can be given by formulas~$I(n)$ such that axioms such that +rings, specific ideals can be given by formulas~$I(n)$ such that axioms such as {\small\begin{align*} \forall n\_ & I(n) \Rightarrow A(n) && \text{``$I \subseteq A$''} \\ \exists n\_ & Z(n) \wedge I(n) && \text{``$0 \in I$''} @@ -600,8 +602,7 @@ a uniform definition might not be possible. This issue has a counterpart in type-theoretic foundations of mathematics, where the family~$(\mmm_n)_{n \in \NN}$ cannot be given as an inductive family (failing the positivity check), and is also noted, though not resolved, in -related work on a constructive version of Gödel's completeness -theorem~\cite[p.~11]{herbelin-ilik:henkin}. +related work~\cite[p.~11]{herbelin-ilik:henkin}. The issue does not arise in the context of~\textsc{pa}, where the law of excluded middle allows us to bound the logical complexity: We can blithely define the joint indicator function~$g(n,i)$ for the sets~$G_n$ (such that~$G_n = \{