Does the law of the excluded middle hold for finite sets in intuitionist set theory?

Question

There are local laws of the excluded middle in intuitionist logic, for instance I believe you can prove in Heyting Arithmetic that for all $\Sigma_1$ propositions, that $p \vee \neg p$. Is there something similar for propositions that only refer to finite sets (for some notion(s) of finite sets) in some intuitionist set theory?

Answer 1

I assume that your question asks intuitionistic set theories (like $\mathsf{IZF}$ or $\mathsf{CZF}$) can prove the excluded middle for specific kinds of formulas: namely, formulas whose quantifiers are bounded by finite sets and every parameter occurring in this formula is a finite set.

---

Here is an issue: there are many possible definitions of finite sets which is classically equivalent.

According to CZF book draft by Aczel and Rathjen, the term finite set denotes bijective images of an element of $\omega$ under some function. That is, $A$ is a finite set iff there is an one-to-one, onto function $f:n\to A$ for some $n = \{0,1,\cdots, n-1\}$.

However, you may require $f$ just onto. We will call these sets finitely enumerable sets. (Note: terms may vary from texts.)

Unfortunately, these two concepts are not stable under subset relation. There is no reason that a subset of a finite set is a finite set. A Brouwnian counterexample is as follows: $X= \{x\in 1\mid \phi\}$, where $\phi$ is an undecidable statement. We could not find a concrete bijection (or even surjection!) from a finite set to $X$ explicitly.

This is the reason why we introduce the concept subfinite set, which is defined by subsets of finite sets. The good news is that every subset of a finitely enumerable set is subfinite, so we do not need to define one more term.

---

The answer is no even if we assume aforementioned terms. Consider the following formula: $$\exists x\in \{\{0\mid \phi\}\} (0\in x).$$

Here $\{0\mid \phi\}$ is a subset of $\{0\}$ satisfying $$y\in \{0\mid\phi\} \iff y=0\land \phi.$$ It need not be a finite set, although it is subfinite. However, the set $\{\{0\mid \phi\}\}$ is finite. If the formula satisfies the excluded middle, then we have either

1. there is $x\in \{\{0\mid \phi\}\}$ which is inhabited (i.e. contains an element) or
2. no $x \in \{\{0\mid \phi\}\}$ is inhabited.

You can see that 1 implies $\phi$, since the only element of $\{\{0\mid \phi\}\}$, which is $\{0\mid \phi\}$, is inhabited so $\phi$. On the other hand, if 2 holds and $\phi$, then there must be an inhabited element of $\{\{0\mid \phi\}\}$. A contradiction! Hence $\lnot \phi$. In sum, we have $\phi\lor\lnot\phi$.

---

I recently found that the answer is yes if we restrict our attention to hereditarily finite sets. We should define what a hereditarily finite set is before examining the proof.

A hereditarily finite set is a finite set whose elements are finite. The definition is self-referencing. A classical way to define a set of hereditarily finite sets $H_\omega$ is to use cumulative hierarchy $V_\alpha$. Especially, $V_\omega$ is the set of all hereditarily finite sets.

However, $\mathsf{CZF}$ cannot prove $V_\omega$ is a set. Moreover, $V_\omega$ contains lots of subfinite sets that could not be finite. Hence we need another definition.

A way of expressing $H_\omega$ is using an inductive definition. I will not explain what an inductive definition is. If you are not familiar with it, you may ignore it and remember that my definition just rephrases 'every element is finite and every element is hereditarily finite.'

Let $\Phi$ be an inductive definition given as follows: $$\Phi:=\{(a,\{a\}\mid \text{$a$ is finite.}\}$$ Define $H_\omega$ be the smallest class which is closed under $\Phi$.

We do not know whether $H_\omega$ is a set from this definition. However, we can show that there is another way of expressing $H_\omega$.

For a set $X$, define $\operatorname{Dec}(X)$ be the set of all decidable subsets of $X$. i.e., $$\operatorname{Dec}(X) = \{A\subseteq X\mid \forall x\in X (x\in A \lor x\notin A)\}.$$ Unlike the power set of $X$, $\operatorname{Dec}(X)$ is always a set. Now consider the following hierarchy: $D_0=\varnothing$ and $D_{n+1}=\operatorname{Dec}(D_n)$, $D_\omega := \bigcup_{n<\omega} D_n$. Then we can show the following theorem:

Theorem. $H_\omega=D_\omega$.

We can show that if $\phi(x)$ is a bounded formula, then $\forall x\in H_\omega \phi(x)\lor\lnot\phi(x)$, by induction on formulas.

The atomic case follows from the properties of $D_n$: every element of $D_n$ is a decidable subset of $D_n$, and $D_n$ is discrete (i.e., $x=y$ or $x\neq y$ for all $x,y\in D_n$.)

The case for $\lnot$, $\lor$, $\land$ and $\to$ is trivial. The only nontrivial part is for bounded quantifiers. Let $x\in H_\omega$ and $\phi(y)$ be a decidable formula for $y\in H_\omega$. Fix a bijection $f:n\to x$ for some $n\in\omega$. Then $\forall y\in x\phi(x)$ is equivalent to $\forall k<n\phi(f(k))$, which can be shown to be decidable by induction on $n$.