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?

  • 2
    $\begingroup$ What do you mean "only refer to finite sets" ? Like, quantified over finite sets with finite parameters ? $\endgroup$ Commented Aug 31, 2019 at 20:16
  • $\begingroup$ (Side issue: Excluded middle for $\Sigma^0_1$ statements have a separated name: the limited principle of omniscience. This is not provable in intuitionistic sense.) $\endgroup$
    – Hanul Jeon
    Commented Sep 1, 2019 at 12:30

1 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$.

  • $\begingroup$ The argument in the middle section doesn't refute the question, though. It shows if $\{0|φ\}$ is finite then $φ$ is decidable. But if $φ$ only refers to finite sets, then we're expecting it to be decidable, therefore $\{0|φ\}$ being finite is fine. It seems to me that the motivation for sub-finite sets is the ability to define subsets of a finite set that refer to infinite sets, so exhaustive search is no longer a plausible method of deciding propositions. If only finite sets are ever used, EM should be fine (I think) unless we're ultrafinitist. $\endgroup$
    – Dan Doel
    Commented Sep 1, 2019 at 21:03
  • $\begingroup$ I guess it depends on exactly what a proposition 'refering' to finite sets means, though, which hasn't been nailed down. $\endgroup$
    – Dan Doel
    Commented Sep 1, 2019 at 21:11
  • $\begingroup$ That is an answer to the question I asked so I'm accepting it, but I guess I wonder about whether you can remove those counterexamples by putting some constructive conditions on set formation. E.g. Bishop says more or less that the set you've described doesn't exist. $\endgroup$ Commented Sep 1, 2019 at 21:42
  • $\begingroup$ @WilliamBell I do not know the Bishop's mathematics in detail. To explain within my knowledge, the set $\{0\mid\phi\}$ provably exists in $\mathsf{CZF}$ when $\phi$ is a $\Delta_0$-formula (due to bounded separation), and even the excluded middle for $\Delta_0$-formulas is not constructive. $\endgroup$
    – Hanul Jeon
    Commented Sep 2, 2019 at 11:13
  • $\begingroup$ @DanDoel This is the reason why I put the comment at the last part of my answer. I also know that the set $\{0\mid\phi\}$ could not be regarded as finitary one. However, I just do not know how to proceed it under this strict requirement. $\endgroup$
    – Hanul Jeon
    Commented Sep 2, 2019 at 11:18

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .