Is "$X$ is finite" decidable (in ZFC)?

Question

Disclaimer: This question is about formalizing the idea that a particular set is "finite" in strict first-order ZFC, without any extensions or informal statements, except where otherwise noted (mostly abbreviations). If you don't like the idea of purely formal mathematics, feel free to find your own cup of tea and drink it, this is mine.

---

It is a simple and natural question to ask: "how do we know that a given set is finite?"

A Naive Argument in Favor of Decidability

At first glance, this seems like a trivial question; an intuitive answer might follow something along the lines of:

"Suppose that $X$ is a finite set. There must be some natural number $n$ equal to the number of elements in $X$, and we can construct a bijective enumeration of $X$ to show that this is the case. Define the pair of sets $Z_0=\emptyset$ and $X_0=X$, and choose an element $x\in X$. Then define $Z_1=\{(0,x)\},X_1=X_0\setminus\{x\}$. Repeat this process for an element of $X_1$ to obtain $Z_2,X_2$, and so on until you have $Z_n\in X^n,X_n=\emptyset$. The set $Z_n$ is then a bijective enumeration of $X$, and we have shown that $X$ has exactly $n$ elements."

This procedure outlines a program which takes a finite set $X$ and produces a function mapping the cardinality of that set to the elements of that set. We can write this program as follows:

λ X : Set . enum(X) : Set -> (Nat -> X);
enum(X) := {
   Z : Nat -> X;
   i = 0;
   for x in X
   {
      Z(i) = x;
      i++;
   }
   return Z
}
X = get_input;
enum(X)

(Note 1)

It should be immediately obvious from this that we know that a set $X$ is finite if and only if $P$ halts on $X$. So now the question becomes "Does $P$ halt on every finite set $X$?" It is tempting to respond with an immediate "yes, obviously." Indeed, if you were to actually run the program for $X=\{x_0,\ldots,x_{n-1}\}$ an infinite number of times, choosing different values for $x_0,\ldots,x_{n-1}$ every time, you would never find a case where $P$ did not halt. It then seems reasonable to conclude that "finiteness" is at least semi-decidable. (Note 2)

But "it is not possible to list the elements of a finite set $X$ such that $P$ does not halt on $X$" is a long way from "$P$ halts on every finite set $X$."

In fact, the "finite set = list" convention and accompanying notation is not even native to ZFC, whose sole nonlogical symbol is the membership relation "$\in$," so we really shouldn't be trying to list the elements of $X$ anyway. We need to clarify how to interpret the informal statement "$X$ has $n$ elements" in ZFC.

The Gory Details

We may identify any specific set in ZFC with a "definition" - a formula $\phi$ such that $\mathsf{ZFC}\vdash \exists!x\phi$ (Note 3). If we take "is finite" to be a predicate, then we would want the domain of this predicate to be the set of all definitions. Thus we take "Suppose $X$ is a [finite] set." to mean that that we have been given a formula $\phi$ such that $\mathsf{ZFC}\vdash\exists!x\phi$, this being the definition of the set referred to by "$X$."

Now we want to say that $X$ is finite. The simplest way to do this is with a formula that states "there are exactly $n$ elements in $X$," which we may write somewhat lazily as:

$$\exists!x\left(\phi\land\exists x_0\cdots\exists x_{n-1}\left(\bigwedge_{i\ne j}\neg(x_i=x_j)\land\forall x_n\left(x_n\in x\implies\bigvee_{i\in n} x_n=x_i\right)\right)\right)$$

where $\bigwedge_{i\ne j}x_i\ne x_j$ and $\bigvee_{i\in n}x_n=x_i$ are shorthand for the repeated logical conjunction $x_0\ne x_1\land x_0\ne x_2\land\cdots\land x_{n-1}\ne x_{n-2}$ and disjunction $x_n=x_0\lor x_n=x_1\lor\cdots x_n=x_{n-1}$, respectively. This is equivalently "there exist pairwise distinct elements $x_0,\ldots, x_{n-1}$ such that every element $x\in X$ is equal to $x_i$ for some $i\in n$," "the cardinality of $X$ is $n$," and "there exists a bijection from $n$ to $X$" For convenience' sake, we'll use the abbreviation

$$\nu_n(x):=\exists x_0\cdots\exists x_{n-1}\left(\bigwedge_{i\ne j}\neg(x_i=x_j)\land\forall x_n\left(x_n\in x\implies\bigvee_{i\in n} x_n=x_i\right)\right)$$

Now, the statement

"$X$ is finite"

becomes the metaproposition

"There exists a natural number $n$ such that $\mathsf{ZFC}\vdash\exists!x(\phi\land\nu_n(x))$."

As with the "program" before, we find that if the elements of every finite set can be listed (i.e. there are formula $\phi_0,\phi_1,\cdots,\phi_{n-1}$ such that $\mathsf{ZFC}\vdash\exists!x_i\phi_i\land\forall x_i(\phi_i\implies\exists x(\phi\land x_i\in x))$ for each $i\in n$), then we are always able to prove this.

HOWEVER, it need not be the case that $\mathsf{ZFC}\vdash\exists!x\phi\implies\exists x(\phi\land\nu_n(x))$ for some natural $n$ whenever $\phi$ defines a finite set. I see no reason to think it impossible to produce some formula describing a "finite" set which is not "provably finite" - or, at the very least, a finite set $X$ for which "$X$ contains $n$ elements" is not provable for any $n$ (there may well be a weaker notion of "finiteness" which does not require the cardinality of $X$ to be known or knowable.) (Note 4)

The question of whether or not such sets exist, and hence whether or not "finiteness" is decidable, can be approached in different ways. I believe that for the negative case "finiteness is not decidable," it is necessary to prove the independence of $\exists x(\phi\land \nu_n(x))$ for all $n\in \omega$ for some $\phi$ such that $\mathsf{ZFC}\vdash\exists!x\phi$. It should be enough to do this for exactly one $n$, since the assumption of $\exists x(\phi\land\nu_n(x))$ and $\exists!x\phi$ suffices to prove $\neg\exists x(\phi\land\nu_m(x))$ for any $m\ne n$.

In general, to say that "finiteness" is decidable, I think we would want to prove

"For every formula $\phi$ such that $\mathsf{ZFC}\vdash\exists! x\phi$, either there exists a [unique] natural number $n$ such that $\mathsf{ZFC}\vdash\exists x(\phi\land\nu_n(x))$ or $\mathsf{ZFC}\vdash\forall x(\phi\implies\neg\nu_n(x))$ for all $n\in\omega$."

An alternative approach (which might only work in a second-order theory, I'm not sure) is to prove that the elements of any finite set can be "named." That is:

"For every formula $\phi$ such that $\mathsf{ZFC}\vdash\exists! x\phi$ and $\mathsf{ZFC}\vdash\exists x(\phi\land\nu_n(x))$ for some $n\in \omega$, there exist formulae $\phi_0,\ldots,\phi_{n-1}$ such that $\mathsf{ZFC}\vdash\exists!x_i\phi_i$ for each $i\in n$ and $\mathsf{ZFC}\vdash\exists x\left(\phi\land\forall x_n\left(x_n\in x\implies\bigvee_{i\in n}\phi_i[x_i:=x_n]\right)\right)$."

For the former, we would want a procedure which takes a ZFC proof of $\exists!x\phi$ as an argument and returns a proof of $\exists x(\phi\land\nu_n(x))$ if the set defined by $\phi$ has $n$ elements (for some $n\in\omega$), and enumerates proofs of $\forall x(\phi\implies\neg\nu_n(x))$ for each $n$ otherwise.

In the latter case we would want a procedure which takes a ZFC proof of $\exists!x\phi$ as an argument, and returns proofs $\exists!x_i\phi_i$ for each $\phi_i$ defining an element of the set defined by $\phi$ and a proof of $\forall x_n(\phi_i[x_i:=x_n]\implies \exists x(\phi\land x_n\in x))$.

Whatever the case, I'm not qualified to prove any of it one way or another.

---

Notes:

1. This is only to show the algorithm used in constructing an enumeration, and is not intended to represent functioning code. The key takeaway is that the suggested method for proving that a given set is finite is a computation on that set. If it helps, I can provide a register machine that explicitly performs the computation in question (modulo some macros, because the method of encoding sets is arbitrary and can easily take up this entire page.)

2. If we commit to the idea that every finite set can be identified with an actual list of its elements, that is, if we assume the physical realizability of arbitrary finite sets (a dubious assumption, given that there are uncountably many finite sets, but who knows what we might accomplish with the full power of interdimensional quantum spirit-cryptography?)$^{2.1}$ then this shows that "finiteness" is decidable iff "infiniteness" is decidable. Obviously the program doesn't halt when $X$ is infinite.

3. While we may prove the existence of sets for which no such definition exists (e.g. we can prove "there exists a set such that" without being able to "name" the set), it is difficult to define "finite" in such a way that it applies. Consider $\exists x\exists y(y\in x)$ "there is a nonempty set." Certainly such a set exists, but we can hardly say whether it is finite or infinite.

4. Another possibility is that we produce a formula $\Phi$ with a free variable $n$which directly asserts $\exists x(\phi\land\nu_n(x))$ using some kind of clever encoding. I'm not sure how exactly this would be done (if it can be done at all). There is a bit of nuance with how we interpret the results of this approach, since we can't necessarily know that the encoded statement is "actually" true of the theory (for example we may end up with $\Box (\exists n\in\omega)\Phi$ but not $(\exists n\in\omega)\Box\Phi$).

2.1 Yes, this is a footnote-footnote. Yes, that was a jab at overly optimistic techno-futurologists and theoretical physicists. There is no evidence at this time to suggest that it is possible for a human, or any human creation, to make use of any "transcomputational" system the likes of which is necessary to truthfully assert "every finite set can be written as a list of its elements." To say otherwise is to make some very, very strong claims about the nature of cognition, computation, and fundamental physics, and to grossly overstate the capabilities and significance of mathematical logic.

Answer 1

It seems (per the comments) that the key issue is why/how definition by cases works. This is less about $\mathsf{ZFC}$ specifically than it is about first-order logic, but to keep things concrete I'll focus on $\mathsf{ZFC}$ to start with.

Suppose I have $(i)$ a sentence $\chi$ and $(ii)$ a pair of formulas $\theta(x),\eta(x)$ such that $\mathsf{ZFC}\vdash\exists!x\theta(x)$ and $\mathsf{ZFC}\vdash\exists!x\eta(x)$. I claim that $$\mathsf{ZFC}\vdash\exists!x[(\chi\rightarrow\theta(x))\wedge(\neg\chi\rightarrow\eta(x))].$$

(In my comments I was typing too fast and my "$\rightarrow$"s were bi-directional. That was a mistake, but it's too late to edit those comments now.)

The proof is ... by cases! Specifically, we have $\mathsf{ZFC}\vdash\chi\vee\neg\chi$ by LEM, so we reason as follows:

• If $\chi$ holds, then $\chi\rightarrow\theta(x)$ is equivalent to $\theta(x)$ and $\neg\chi\rightarrow\eta(x)$ is equivalent to $\top$. This means that every $x$ vacuously satisfies $\neg\chi\rightarrow\eta(x)$ but exactly one $x$ satisfies $\chi\rightarrow\theta(x)$. So exactly one $x$ satisfies the conjunction $[(\chi\rightarrow\theta(x))\wedge(\neg\chi\rightarrow\eta(x))]$ - namely, the unique $x$ satisfiying $\theta$.

• If $\chi$ fails, then $\neg\chi\rightarrow\eta(x)$ is equivalent to $\eta(x)$ and $\chi\rightarrow\theta(x)$ is equivalent to $\top$. This means that \every $x$ vacuously satisfies $\chi\rightarrow\theta(x)$ but exactly one $x$ satisfies $\neg\chi\rightarrow\eta(x)$. So exactly one $x$ satisfies the conjunction $[(\chi\rightarrow\theta(x))\wedge(\neg\chi\rightarrow\eta(x))]$ - namely, the unique $x$ satisfiying $\eta$.

As said above, none of this is specific to $\mathsf{ZFC}$. We can replace $\mathsf{ZFC}$ with any theory whatsoever and, as long as we're using classical logic as our underlying framework, the same situation will hold.

Answer 2

I'm really not understanding the problem. It's easy enough to define $\omega$ in ZFC, so we can say that $X$ is finite $\iff \exists n \in \omega, f$ such that $f$ is a $1$-$1$ map $f:X \to n$.

If you want to know whether $\mathsf{ZFC}$ can always prove that a particular set is or is not finite, the answer is clearly no: $\mathsf{ZFC}$ cannot decide whether $X= \{n \in \omega \mid 2^{\aleph_n}=\aleph_{n+1} \}$ is finite.

Answer 3

"For every formula $\phi$ such that $\mathsf{ZFC}\vdash\exists! x\phi$, either there exists a [unique] natural number $n$ such that $\mathsf{ZFC}\vdash\exists x(\phi\land\nu_n(x))$ or $\mathsf{ZFC}\vdash\forall x(\phi\implies\neg\nu_n(x))$ for all $n\in\omega$."

This is clearly false, assuming ZFC is consistent. Given a sentence $P$ in ZFC, let $\phi_P(x)$ be $P \land x = \emptyset \lor \neg P \land x = \mathbb{N}$. If your statement were true, we could apply it to $\phi_P$ to deduce that either ZFC $\vdash \exists x (\phi_P(x) \land \nu_0(x))$, in which case ZFC $\vdash P$, or ZFC $\vdash \forall x (\phi_P(x) \to \neg v_0(x))$, in which case ZFC $\vdash \neg P$. So ZFC would be complete, which, by Godel’s incompleteness theorems, would mean ZFC is inconsistent.

"For every formula $\phi$ such that $\mathsf{ZFC}\vdash\exists! x\phi$ and $\mathsf{ZFC}\vdash\exists x(\phi\land\nu_n(x))$ for some $n\in \omega$, there exist formulae $\phi_0,\ldots,\phi_{n-1}$ such that $\mathsf{ZFC}\vdash\exists!x_i\phi_i$ for each $i\in n$ and $\mathsf{ZFC}\vdash\exists x\left(\phi\land\forall x_n\left(x_n\in x\implies\bigvee_{i\in n}\phi_i[x_i:=x_n]\right)\right)$."

This statement I’m not so sure about. I don’t immediately see a reason to believe that any definable finite set’s elements should also be definable. I suspect this is false, but I’m not certain. If we add in $V = HOD$ to our axioms, it becomes true.