# Logic and set theory using only uniquely defined items

In Prenex form, a set theoretic sentence can be written $\forall \exists \forall \exists ...\forall \exists \psi$ where $\psi$ has no quantifiers. Now, consider all formulas of the more restrictive form $\forall \exists! \forall \exists! (...)$ (recall that $\exists!$ means "there is a unique"). I call those "constructive" because $\forall x \exists ! y \phi(x,y)$ can be viewed as expressing the existence of a "function" $f$ such that $y=f(x)$ is the only solution to $\phi(x,y)$.

Several axioms or axiom schemes of ZFC are naturally "constructive" in this sense, such as replacement, power set, union, while others like foundation and choice are not.

Is it known whether the non-constructive axioms can be replaced with constructive ones, while keeping a theory that's equiconsistent with ZFC ? A related question : if a theory knows the truth value of any constructive sentence, must it necessarily be complete ?

• First of all, let me point out that the "constructive" part that you mention is not the natural way to phrase these axioms. The reason being that $\exists!$ is not a standard quantifier, but in fact a shorthand for a generally more complex formula. However, the axiom of extensionality lets us prove these "constructive versions" from the usual axioms. – Asaf Karagila Oct 25 '17 at 9:17
• It's not obvious power set is constructive in this sense. To say $y=\mathcal{P}(x)$ is to say $\forall z((z \in y \rightarrow z \subset x) \wedge (z \not \in y \rightarrow z \not \subset x)).$ The formula $z \not \subset x$ is equivalent to $\exists s \in z(s \not \in x),$ which is not constructive. – Elliot Glazer Oct 26 '17 at 3:19
• @ElliotGlazer $z\not\subset x$ is in fact constructive as you show in your answer below. – Ewan Delanoy Oct 26 '17 at 5:45
• You're right, I meant to say "not obviously constructive." I think for the axiom of union and many instances of replacement, there is no provably equivalent constructive sentence. – Elliot Glazer Oct 26 '17 at 6:43

It's not obvious most axioms of ZFC are constructive in this sense, e.g. the replacement schema has many sentences involving $\phi$ with non-constructive existential quantifiers. The only axioms that seem to have obvious constructive statements are pairing and extensionality. Still, I think it's plausible that ZFC+V=L can be axiomatized using only constructive sentences. I'll sketch out a possible approach:

Start with extensionality and pairing. Define $x \neq \emptyset"$ by $\exists! b \forall a(a \not \in b \wedge b \neq x)$ (taken from Dap's answer).

Define $x \not \subset y$ by $\exists! z(\forall a (a \in z \leftrightarrow (a \in x \wedge a \not \in y))\wedge z \neq \emptyset).$

Define $\alpha \in Ord$ by $\forall \beta \in \alpha (\forall \gamma \in \beta (\gamma \in \alpha)) \wedge \forall S(S \not \subset \alpha \vee S=\emptyset \vee \exists!\beta \in S(\forall \gamma \in S(\beta = \gamma \vee \beta \in \gamma))).$

I think the basic theory of ordinals (and functions on them) should be constructively axiomatizable. We should be able to state $V=L$ using the auxillary Jensen hierarchy $S_{\alpha}$ (which is rather convoluted to define, see Schindler's text book). In particular, we should be able to constructively define the notion of an "$S$-sequence," i.e. a transfinite sequence of the form $\langle (S_{\alpha}, <_{\alpha}): \alpha<\beta \rangle,$ where $<_{\alpha}$ is the canonical well-order on each $S_{\alpha}.$ We need to construct the well-order simultaneously because the definition of successive $S_{\alpha}$'s uses the notion of union, and I think we need to use the well-order to constructively define the union of a set.

Now we can state $V=L$ as the statement that for each $x,$ there is a unique $S$-sequence whose final $S_{\alpha}$ is the first to have $x$ as an element. Now we can constructively state the other axioms of ZFC by noting $\exists \phi(x)$ is equivalent to there existing a unique $<_L$-minimal $x$ satisfying $\phi.$

Addendum: Here's a possible counterexample to the suggestion that a theory deciding all constructive sentences is necessarily complete. Define a poset $(P,<)=(\mathbb{Z} \cup \{\infty, \infty'\},<),$ where $<|_{\mathbb{Z}}$ is the standard order and $\infty$ and $\infty'$ are both maximal elements. Consider two models in the language of a single binary predicate $<,$ namely $(M_1,<), (M_2,<),$ where $M_1=\mathbb{N} \times P$ and $M_2=M_1 \cup (\{-1\} \times \mathbb{Z}).$ In each, we define $(a,b)<(c,d)$ iff $a=c$ and $b<d.$ I strongly suspect $(M_1,<)$ and $(M_2,<)$ have the same constructive truths, but are clearly not elementary equivalent.