# Undecidability in constructive subsystems of ZFC

The axioms of set theory can be divided into three categories :

-The "restrictive" axioms, which impose that set have certain regularity properties (extensionality, foundation).

-The "constructive" axioms, which allow one to form a uniquely defined set from older ones or from nothing (Empty set, pairing, union set, infinity, subset, replacement, power set)

-The "nonconstructive" axiom (choice).

(So for my purposes here it will be convenient to consider the infinity axiom only in the form "The set $\omega$ of all finite ordinals exists" instead of vaguer forms not defining a unique new set). One can create a mini-language of terms representing sets, associating a "constructor" to each constructive axiom : we will then have ${\bf Empty, Infinity}$ with no arguments, ${\bf Union, Power}$ with one argument, ${\bf Pair}$ with two arguments,${\bf Subset}$ with two arguments, the second of which must be a formula in one variable, and ${\bf Replacement}$ with two arguments, the second of which must be a formula in two variables.

So we have a set of seven constructors,

$$C=\lbrace {\bf Empty,Infinity,Union,Power,Pair,Subset,Replacement }\rbrace$$

For any subset $C’$ of $C$, one may form the language $L(C’)$ of terms formed from constructors in $C’$ only. On $L(C’)$, there is a natural membership relation coming from the interpretation of the terms. Since there are only countably many formulas, $L(C’)$ is effectively countable, so it makes sense to talk about the decidability of the membership relation on $L(C’)$.

Of course, the full language $L(C)$ will be undecidable (unless $ZFC$ is inconsistent). Now I ask : Is membership decidable when $C’=\lbrace{\bf Empty,Infinity,Pair,Union,Subset }\rbrace$ ?

-
I don't think so because the formula in Subset may look ugly: Is $\mathbf{Subset}(\omega,\phi(n))=\mathbf{Empty}$ true, where $\phi(n)$ "says" that $n$ is the Gödel number of a suitable undecideable statement? – Hagen von Eitzen Sep 16 '12 at 12:35

Let $\phi(n)$ be a formula of arithmetic defining a noncomputable set $A \subseteq \omega$; there are many such formulas. There is a corresponding formula $\hat\phi$ of ZFC such that $A = \{ x : x \in \omega \land \hat\phi(x)\}$.

In your system, there will be a term that defines $A$, using a single instance of the "Subset" principle on $\hat\phi$ and $\omega$. So in general membership will not be decidable as long as you have both $\omega$ and the ability to construct arbitrary definable subsets.

As an aside, although the subsystems you are talking about do not include the axiom of choice, they are not "constructive" in any serious way, because they stil include both the subset principle for arbitrary formulas and all of classical logic. To make genuinely "constructive" systems of set theory, these are the things that have to be restricted. The axiom of choice, on the other hand, it true in many constructive settings.

In particular, every set that is given by a term made with your seven constructors is in the constructible universe $L$. There is a single canonical, definable well ordering of the sets in $L$ that can be formalized in ZF. Thus you could add a Choice constructor that takes a term $\tau$ and whose semantic value is a choice function on the set defined by $\tau$, if every member of this set is nonempty, or $\emptyset$ otherwise. The resulting system would be just as constructive as the system you already have (for example, ZF set theory without choice is able to prove that every term of the extended system defines a unique set in $L$). What you are doing in the question, in fact, is defining a subclass of $L$ via your constructors. Essentially, $L$ is what you would get if you added to your system a term for every ordinal. As long as you stay inside $L$, you get the axiom of choice "for free".

-
I agree that $L$ has definable well orderings, but I think it's a stretch to stay that there's a single canonical one. The constructions I've seen lead to orderings that depend on many minor details such as how to enumerate formulas, which are fairly arbitrary and often even left to the reader's imagination (because it suffices that the reader can imagine some way to write a formula that achieves the purpose at hand). – Henning Makholm Sep 16 '12 at 14:57
Sure - I agree it can be argued in what sense the ordering of $L$ is "canonical". Some meanings of "canonical" exclude arbitrary choices, but others don't; some things (like the Computus for calculating the date of Easter) were chosen somewhat arbitrarily but are still canonical. I would put the particular well-ordering of $L$ in the latter category: of the many possible definable well orderings of $L$, each author picks one to be the canonical ordering $<_L$. – Carl Mummert Sep 16 '12 at 15:15
Why is it that all terms made from my constructors will be in $L$ ? What I see is that, since $L$ satisfies ZFC, there will be a canonical map mapping each term to an element of $L$. But how does that imply $V=L$ ? – Ewan Delanoy Oct 4 '12 at 8:44
@Ewan: First, let me be clear I am talking about $C'$, without the "Power" constructor. If the constructors in $C'$ are applied to sets in $L$, the resulting set is in $L$ (for Subset, this is because $L$ satisfies the separation scheme). Thus, as you say, there is a canonical map that assigns a unique set in $L$ to each term from $C'$. That does not imply that $V = L$. But, because there a fixed well ordering of $L$, there is a canonical choice function for every set in $L$, and thus we could extend $C'$ with a "Choice" constructor and still interpret every term as an element of $L$. – Carl Mummert Oct 4 '12 at 13:55
@CarlMummert : would adding the “Power” constructor change anything in the argument? Also, can one effectively construct a model satisfying $V \neq L$ but where every set is “constructible” in my very mild sense? – Ewan Delanoy Oct 5 '12 at 6:57