3
$\begingroup$

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$ ?

  • 2
    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?2012-09-16

1 Answers 1

5

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".

  • 0
    The constructors in $C'$ have the feature that they mean the same whether interpreted in $L$ or $V$. But more importantly they have the property that every hereditary element of a set constructed by a term in $C'$ is also given by a term in $C'$. So working in $C'$ I can assume every set has a term. If I want to define the set $P$ represented by the non-$C'$ term "Power($\omega$)", I have to choose: should $P$ be the set of terms that give subsets of $\omega$, or should it contain all subsets of $\omega$, even though some of them don't have terms? This is the complication I was alluding to.2012-10-05