Finite sets and principle of excluded middle

axiom-of-choicefoundationslogictopos-theory

This question is about the principle of excluded middle and its relation to the axiom of choice on finite sets.

I am new to the principle of excluded middle and I was reading it on nLab and Wikipedia. Intuitively, it is saying that any truth value can only be true or false.

https://ncatlab.org/nlab/show/excluded+middle

https://en.wikipedia.org/wiki/Law_of_excluded_middle

In nLab, it states the Diaconescu-Goodman-Myhill theorem. I kind of understand the statement in the theorem, but I don't understand the proof… Wikipedia also state the theorem in a different way, but I also don't quite understand it. I am going to state the theorem and the proof as in nLab below because it puzzles me more:

Diaconescu-Goodman-Myhill theorem:
The following statements are equivalent.

  1. The principle of excluded middle.
  2. Finitely indexed sets are projective (in fact, it suffices 2-indexed sets to be projective).
  3. Finite sets are choice (in fact, it suffices for 2 to be choice).

Here, a set $A$ is finite or finitely-indexed (respectively) if, for some natural number $n$, there is a bijection or surjection (respectively) $\{0,…,n−1\} \rightarrow A$.

Proof:
If $p$ is a truth value, then divide $\{0,1\}$ by the equivalence relation where $0 \equiv 1$ iff $p$ holds. Then we have a surjection $2 \rightarrow A$, whose domain is $2$ (and in particular, finite), and whose codomain $A$ is finitely-indexed. But this surjection splits iff $p$ is true or false, so if either $2$ is choice or $2$-indexed sets are projective, then PEM holds.

On the other hand, if PEM holds, then we can show by induction that if $A$ and $B$ are choice, so is $A\coprod B$ (add details). Thus, all finite sets are choice. Now if $n \rightarrow A$ is a surjection, exhibiting $A$ as finitely indexed, it has a section $A \rightarrow n$. Since a finite set is always projective, and any retract of a projective object is projective, this shows that $A$ is projective. $\blacksquare$

What I don't understand:

  • What is $A$? Is it $A = \{[x]: x \in \{0,1\} \wedge p\}$. My set notation may be a bit off; please correct me if there is something wrong.
  • Is the surjection from $2$ to $A$ define as $x \mapsto [x]$? Is $p$ playing any role in defining this map?
  • What does it mean that $A$ is finitely-indexed?
  • What is the $2$-indexed set? Is it $A$?
  • How do we show that if $A$ and $B$ are choice, then $A \coprod B$ is also choice.
  • The previous bullet point then implies that all finite sets are choice. Is it because all finite sets are disjoint union of some smaller sets? Then what is the base case in the induction? Is it the set $2$? How do we prove that $2$ is choice with PEM?
  • If $n \rightarrow A$ is a surjection, it has a section $A \rightarrow n$? It is because $n$ is finite and is a choice, hence we can invoke the axiom of choice?
  • Why is a finite set always projective?

I think the biggest problem I am facing is that I don't see the big picture of the proof. I guess it is because I am not familiar with mathematics without the excluded middle. It is such a strange world.

Best Answer

Unfortunately, some of the terminology they use such as "truth value", are defined for arbitrary topoi as I think they meant for this argument to work in any topos. In the category of sets, a truth value by nLab's definition is simply a function $p:1\to \Omega$ where $\Omega$ is a subobject classifier (here $1=\{0\}$). You can think of $\Omega$ as being the set of truth values and $p$ as being a function which picks out one of those truth values. So when they say $0\equiv 1$ iff $p$ holds, what they mean is $0\equiv 1$ if $p(0)=true$ and $0\not\equiv 1$ if $p(0)=false$ (a priori we cannot say "$p(0)=true$ or $p(0)=false$"). I will attempt to answer your questions in the order you listed them.

  • Yes, $A=\{[x]\mid x\in\{0,1\}\}$ where $[x]$ is the equivalence class of $x$. They should have made this more clear in my opinion.
  • Yes, the surjection is $x\mapsto[x]$. This map does in some sense depend of $p$ since the codomain of the surjection depends on $p$, but that's it.
  • They state what finitely-indexed means earlier: "Here, a set $A$ is finitely-indexed if, for some natural number $n$, there is a surjection $\{0,\ldots,n-1\}\to A$."
  • A set is $2$-indexed if it is indexed by $2$, i.e. there exists a surjection $\{0,1\}\to A$. In the proof, $A$ is $2$-indexed.
  • Suppose $A$ and $B$ are choice and let $R$ be an entire relation from a set $S$ to $A\sqcup B$. Let $$S_1=\{x\in S\mid \exists y\in A,\ (x,y)\in R\}$$ $$R_1=\{(x,y)\in R\mid x\in S_1\land y\in A\}$$ $$S_2=S\setminus S_1$$ $$R_2=\{(x,y)\in R\mid x\in S_2\}$$ Then $R_1$ is an entire relation from $S_1$ to $A$ and $R_2$ is an entire relation from $S_2$ to $B$, so by assumption, there exist functions $f_1:S_1\to A$ and $f_2:S_2\to B$ such that $f_1\subseteq R_1$ and $f_2\subseteq R_2$. Then $f_1\cup f_2$ defines a function from $S_1\cup S_2$ to $A\sqcup B$ with $f_1\cup f_2\subseteq R$. Finally, by the principle of excluded middle, $S_1\cup S_2=S$, from which we conclude that $A\sqcup B$ is choice.
  • The previous bullet implies that all finite sets are choice by simple induction since $\{0,\ldots,n-1\}$ is the disjoint union of $\{0,\ldots,n-2\}$ and $\{n-1\}$ for all $n\geq 2$. The base case would be the set $0=\emptyset$ and sets in bijection with $1=\{0\}$. Once the previous bullet has been proven, you shouldn't need excluded middle for this inductive argument.
  • This simply uses what was previously established. Since the map $n\to A$ is surjective, the inverse relation from $A$ to $n$ is an entire relation. And because $n$ is finite and we established that finite sets are choice, this entire relation has a subset which is a function $A\to n$ and which must therefore be a section of the original function $n\to A$.
  • This is a simple proof by induction on $\{0,\ldots,n-1\}$. I suggest you try it as an exercise instead of me proving it for you.

Let me know if you need any additional clarification on any points.