Text used in the video
https://youtu.be/2EOW23uVcRA
==== ==== ==== ==== ==== ==== ==== ==== ==== ==== ==== ==== ==== ====
Theorem: ${\mathrm{Axiom\ of\ Choice}}$ implies ${\mathrm{LEM}}$
More concretely:
If equality is governed by set-extensionality, then for any predicate $P$ allowed
in inhabited subset definions $a,b\subset {0, 1}$ via Separation, existence of a choice function,
$f:{a,b}\to (a\cup b)$ with $fa\in a$ and $fb\in b$, implies $P\lor\neg P$.
Proof hint: While equality is not decidable for a general sets of subsets,
the function mediates it with equality of just some naturals.
==== History ====
Proven in 1975 in the following form (screen caps):
The first corollary says a topos with choice is a Boolean topos.
Three page paper by Redu Diaconescu:
https://www.ams.org/journals/proc/1975-051-01/S0002-9939-1975-0373893-X/S0002-9939-1975-0373893-X.pdf
(You'll find the text on this page in the description)
====Overview====
$\bullet$ 1. A dog story. (Semantics for our theorem.)
$\bullet$ 2. Logic and set theory definitions.
$\bullet$ 3. Basic notes on constructive set theory.
$\bullet$ 4. Proof of ${\mathrm{Axiom\ of\ Choice}}$ implies ${\mathrm{LEM}}$.
$\bullet$ 5. Proof of ${\mathrm{Axiom\ of\ Regularity}}$ implies ${\mathrm{LEM}}$. (Very short after the work form 4.)
Story time: You're a dog trainer and you're handed a bunch of dogs from a shelter, $D$.
Your boss wants you to model the teams as sets.
To have the story work as semantics, it's also important that "function"
is read as function in set theory.
We got ten dogs and name the dogs by numbers.
(Just so that the text is more readable.)
So $D = {0,1,2,3,4,5,6,7,8,9}$.
They are be trained and selected from.
You try to find the best two dogs. The other dogs are sent back to the shelter.
Here's the best dogs from last year:
You need to form two teams.
Firstly, the team avalanche rescue dog $a$.
Secondly, the team beach rescue dog $b$.
A dog from team $a$ from four years ago:
A dog from team $b$ from two years ago:
Each team has at least one but at most two dogs.
If both dogs are in both teams, always working together,
the two teams are actually the same team.
The dogpox virus is going around,
but there's an immunization $I$.
The dogs may or may not come with a pass.
If you got the pass for a dog $t$, you can certify that the dog is either provenly
immunized, or provenly not immunized.
$I(t)$ or $\neg I(t)$.
If a team has more than one dog, all dogs must be provenly immunized.
The proofs will informally concern the membership in and equality of teams of dogs.
The dog story is just one semantic to read the formula!
The proof will be entirely formal (in fact, a bit more formal than in a typical
math textbook).
The predicates, like $I$, are read constructively.
As in, to claim $I(t)$ or its negation ($\neg I(t)$), we need the immunization pass.
For dogs where you didn't get a pass, you can't decide $I$.
==== Some logic ====
We will narrate our proofs using a lot of stepwise rewriting, denoted "$\to$".
Of prominent use will be the principles...
...distributivity
$(\phi \land (\psi \lor \rho))\ \leftrightarrow\ ((\phi \land \psi) \lor (\phi \land \rho))$
$(\phi \lor (\psi \land \rho))\ \leftrightarrow\ ((\phi \lor \psi) \land (\phi \lor \rho))$
..."projection and insertion"
$(\phi\land \psi)\ \to\ \phi$
$\phi\ \to\ (\phi\lor \psi)$
...negation introduction, dysjunctive syllogism and contrapositive
$(\phi \implies (\psi\land\neg\psi))\ \to\ \neg \phi$
$((\phi\lor \psi)\land \neg \psi)\ \to\ \phi$
$(\phi \implies \psi)\ \to\ (\neg\psi \implies \neg\phi)$
==== Set theory axioms ====
$\bullet$ 1. Extensionality
For all sets $x, y$
$x\simeq y \implies x = y$
where
$x\simeq y := \forall u. (u\in x \iff u\in y)$
$\bullet$ 2. Pairing
For all $x, y$
$\exists u. \forall z. \big( z\in u \iff (z = x \lor z = y) \big)$
$\bullet$ 3. Union (i.e. set-of-sets-union)
For all $x$
$\exists u. \forall y. \big(y\in u \iff (\exists z. y\in z\land z\in x)\big)$
$\bullet$ 4. Separation (i.e. set-class-intersection)
For all sets $x$ and
For all predicates $\varphi$
$\exists z. \forall y. (y\in z \iff (y\in x \land \varphi))$
Read $\varphi$ as $\varphi(y)$.
(One may restrict the form of allowed $\varphi$'s, e.g. only with all
quantifiers in $\varphi$ bounded)
$\bullet$ (5). Emptyset
$\exists x. \forall y., \neg(y \in x)$
To the extent that I'll talk arithmetic at the end, we'll also have in the background...
$\bullet$ 5. Strong Infinity (the von Neumann naturals $\omega$ exist and we
have induction for formulas with only bounded quantifiers, e.g. $\forall (n\in\omega)$.)
$\bullet$ 6. Replacement (for direct sums, etc.)
$\bullet$ (7). Exponentiation for finite domains
(i.e. function spaces $y^{{0, 1,\dots, n}}$ and quantifiers over them.
Gives a model of ${\mathsf{HA}}$.)
Optional:
$\bullet$ 7. Exponentiation (i.e. general function spaces $y^x$.
Classicaly equivalent to Powerset axiom)
$\bullet$ (8). Natural number induction for general predicates
$\bullet$ 8. $\epsilon$-Induction in this video (classically equivalent to Regularity,
completing to $\mathsf{ZF}$).
$\bullet$ 9. Excluded Middle (a logical axiom, bringing us back $\mathsf{ZF}$).
==== Some set theory definitions ====
$V = {u\in U\mid Q(u)}$
equals
$V = {u\mid u\in U \land Q(u)}$
and really means
$t\in V \iff t\in U \land Q(t)$
$x\subset y$ means $\forall u. (u\in x)\implies (u \in y)$.
$\to$
${u\in U\mid Q(u)}\subset U$
(using $\phi\land \psi \to \phi$)
$(U\subset V\land V\subset U)\iff U=V$
$Sx:=x\cup {x}$
$0:={}$
$1:=S0$
$\to$
$1={0}$
$\to$
$0\in 1$
(only relevant for the Regularity proof)
$\to$
$\neg(0=1)$
(relevant)
Language for propositions $I$.
Warning: Language will be sloppy in principle, but should be always very clear in context.
Asserting $I$.
$\bullet$ Classical reading: "$I$ is true."
$\bullet$ Constructive reading: "$I$ is proven.", or "provenly true",
or "already provably true".
(I will also say "provably true", but I mean the same,
as of course we never want to assert $P$ before it's been proven)
Asserting $\neg I$.
$\bullet$ Classical reading: "$I$ is false."
$\bullet$ Constructive reading: "$I$ has been be rejected."
Sidenote on more sloppy language:
When either $I$ or $\neg I$ has been proven, we call $I$ decided or decidable.
A proposition in a theory can be fundamentally undecidable.
In this video, if an axiom $A$ prove $P\lor \neg I$ without proving
either $I$ or $\neg I$ (i.e. non-constructively),
I might still say that $A$ decides $I$.
However, we may call a proposition undecided if it's not decided,
so there's at least some value in that language.
From here on you might wanna get a paper out and think along.
Some clarifications, not strictly necessary for the proof below.
$D = {0,1,2,3,4,5,6,7,8,9}$
$2 \in D$
$3 \in D$
$4 \in D$
etc.
Say you collected immunization ertificates for the dogs $1$, $5$ and $7$.
And colleccted negartive certificates of immunization for $2$ and $3$.
Dog $1$, $5$ and $7$ are provenly immunized. I.e. $I(1), I(5), I(7)$.
Dog $2$, $3$ provenly not immunized. I.e. $\neg I(2), \neg I(3)$.
So
$I(1)\land I(5)\land I(7)\land \neg I(2)\land \neg I(3)$.
$1\in{u\in D\mid I(u)}$
$t\in{u\in D\mid I(u)}\implies I(t)$
${u\in D\mid I(u)}\subset D$
${1,5,7}\subset{u\in D\mid I(u)}$
${1,5,7}\subset D$
${u\in D\mid I(u)}\subset{1,5,7}\implies {u\in D\mid I(u)}={1,5,7}$
$I(8)$ is not decided. Might be undecidable.
$8\in{u\in D\mid I(u)}$ is undecided.
${u\in D\mid I(u)}\subset{1,5,7}\implies \neg I(8)$
so
${u\in D\mid I(u)}={1,5,7}\implies \neg I(8)$
${u\in D\mid I(u)\lor\neg I(u)}\subset D$
$D\subset{u\in D\mid I(u)\lor\neg I(u)}\implies \forall (u\in D). (I(u)\lor\neg I(u))$
Equality of ${u\in D\mid I(u)\lor\neg I(u)}$ and $D$ is undecided.
The best two dogs were $0$ and $1$.
We may let $P:=I(0)\land I(1)$, but none of the proof below depends on this semantics.
$P$ can be a generic proposition for which Separation is legal.
You get instructions to form the teams $a$ and $b$ as follows:
Def:
$a:={u\in{0, 1} \mid (u=0) \lor P}$
$b:={u\in{0, 1} \mid (u=1) \lor P}$
Finally, your boss tasks you to provide the following information, in form of
a set-function $f$:
For each team (which may be the same), specify one dog who is in that team.
I.e.
$f$ with $f:{a, b}\to (a\cup b)$ so that $fa\in a$ and $fb\in b$.
====Diaconescu's theorem====
Theorem: Existence of a choice function $f$ decides $P$, as in it implies $P\lor \neg P$.
(So if you couldn't possibly find out have the immunization status of the dogs,
you couldn't give your boss an $f$ either.)
Proof...
Again, for convenience,
$a:={u\in{0, 1} \mid (u=0) \lor P}$
$b:={u\in{0, 1} \mid (u=1) \lor P}$
Firstly, some rewrites:
$a={u \mid u\in{0, 1} \land (u=0 \lor P)}$
$\leftrightarrow$
$a={u \mid \big(u=0\lor u=1\big) \land \big(u=0 \lor P\big)}$
$\leftrightarrow$
$a={u \mid u=0\lor (u=1\land P)}$
$\leftrightarrow$
$t\in a \iff t=0\lor (t=1\land P)$
Similarly
$t\in b \iff t=1\lor (t=0\land P)$
(Maybe write these two down, I won't scroll up all the time.)
Observations:
$0\in a$
$1\in b$
So the sets are inhabited.
Observations relating to $P$:
$P\implies\big(a={0, 1}\land b={0, 1}\big)$
$\to$
$P\implies a=b$
$\to$
$P\implies {a,b}={a}$
$\neg P\implies\big(a={0}\land b={1}\big)$
$\leftrightarrow$
$\neg P\iff\neg(a=b)$
(Can e.g. use the contrapositive to get $\iff$)
$1\in a\iff P$
$0\in b\iff P$
(Try to interpret in terms of dog teams.)
For functions in general:
$x=y\implies fx=fy$
$\to$
$\neg(fx=fy)\implies \neg(x=y)$
In our setting:
$\to$
$\neg(fa=fb)\implies \Big(\big(a={0}\land b={1}\big)\land \neg P\Big)$
$\to$
$\neg(fa=fb)\implies fa=0\land fb=1$
$\to$
$\neg(fa=1\land fb=0\big)$
I.e. a choice function $f_{10}={\langle a, 1\rangle, \langle b, 0\rangle}$ is impossible.
(Again, read in terms of dog teams.)
In a disjunct (further below), we will discard $fa=1\land fb=0$ as contradictory clause.
Choice function:
$f$ with $\Big(f:{a, b}\to (a\cup b)\Big)\land fa\in a\land fb\in b$
$\to$
$fx=t \implies t\in x$
Pairing+Union:
$t\in (x\cup y) \iff \big(t=0\lor (t=1\land P)\big)\lor \big(t=1\lor (t=0\land P)\big)$
$\leftrightarrow$
$t\in (x\cup y) \iff (t=0\lor t=1)\lor\big((t=0\lor t=1)\land P\big)$
$\leftrightarrow$
$a\cup b = {0, 1}$
In a conjunct (now right below), we will discard $fa\in{0, 1}\land fb\in{0, 1}$ as established clause.
Finally,
$fa\in a\land fb\in b$
$\leftrightarrow$
$\big(fa=0\lor (fa=1\land P)\big)\land \big(fb=1\lor (fb=0\land P)\big)$
$\leftrightarrow$
$\big(fa=0\lor fa=1\big)\land \big(fa=0\lor P\big)\land \big(fb=1\lor fb=0\big)\land \big(fb=1\lor P\big)$
$\to$
$\neg(fa=fb)\lor P$
$\to$
$P\lor \neg P$
Bonus explicit analysis:
The above had shown the (weaker) disjunction equivalence:
$(1\in a)\lor(0\in b)\lor\neg(a=b) \iff (P\lor\neg P)$
Apply with knowledge that $f$ must be Boolean valued.
We give the concrete functions some more concrete names and discuss their implications.
$f_{00}={\langle a, 0\rangle,\langle b, 0\rangle}$, means $0\in b$, so $P$ and $a=b$
$f_{11}={\langle a, 1\rangle,\langle b, 1\rangle}$, means $1\in a$, so $P$ and $a=b$
$f_{01}={\langle a, 0\rangle,\langle b, 1\rangle}$, means $\neg(a=b)$, so $\neg P$ from the contrapositive of $P\implies a=b$
$f_{10}={\langle a, 1\rangle,\langle b, 0\rangle}$, means $\neg(a=b)$ but also $0\in b$, so $P$ and $a=b$, so this is
$f_{10}$ is impossible.
More observations relating to both $f$ and $P$:
We already established that
$f_{10}={\langle a, 1\rangle, \langle b, 0\rangle}$
is generally impossible.
$P$ collapses $a$ and $b$.
$P\iff \Big(f:{{0,1}}\to {0,1}\Big)\land \Big(f_{00}={\langle {0,1}, 0\rangle}\lor f_{11}={\langle {0,1},
1\rangle}\Big)$
i.e.
$\Big(f:{a}\to {0,1}\Big)\land \Big(f_{00}={\langle a, 0\rangle}\lor f_{11}={\langle a, 1\rangle}\Big)$
(Abuse of notation: The indices on the $f$'s in the second clause are just
for orientation, this is still just "$f$")
$\neg P$ fully separates $a$ and $b$.
$\neg P\iff \Big(f_{01}:{{0}, {1}}\to {0,1}\Big) \land \Big(f_{01}={\langle {0}, 0\rangle, \langle {1},
1\rangle}\Big)$
i.e.
$\Big(f_{01}:{a, b}\to {0,1}\Big)\land \Big(f_{01}={\langle a, 0\rangle, \langle b, 1\rangle}\Big)$
In summary, for undecided $P$, we capture all those above by the two sets
$f_{00,01}={\langle a, 0\rangle, \langle b, c\rangle}$
here $c={u\in{0}\mid\neg P}$
or
$f_{11,01}={\langle a, d\rangle, \langle b, 1\rangle}$,
where $d={u\in{0}\mid P}$.
These are uncountable.
In the constructive theory, we can't evaluate general $P$ as an "if-clause"
in the domain or return value for $f_{00,01}$.
Assuming $P\lor \neg P$, then the two sets are (formally) two choice
functions and (formally) countable.
(No concrete, i.e. $P$-independent, bijection with a one, or two element set.)
====Afterthought: Naive python interpretation====
Let's think of potential programming language interpretations of out theory.
To the extent to which the functions are computable in the interpretation,
it determine and the function then capable of querying $P$.
Our theory interprets HA, so let's require at least Turing completeness.
We'd also want language with set-comprehensions.
And with nice types.
In terms of python code (not typed), both cases of $f={\langle a, 0\rangle, \langle b, c\rangle}$ could be captured as
def f(x) -> int:
"""
A short at the f_{00,01} choice function.
:param x: A 0-ary function that computes and returns a set.
"""
if 0 in x():
return 0
return 1
f(lambda: {0, 1})
f(lambda: {0})
f(lambda: {1})
f(lambda: {7, 8, 9001}) # "Type protection" pyhton hack below
Note that this itself doesn't know about $a$ or $b$.
This is python and not a mathematical set function
- indeed it does not even have a domain.
We can mimic a type check and also determine $P$ and can query the input size:
def check_input(x) -> bool:
if not type(x()) == set:
return False
cadinality: int = len(x())
if not cadinality in {1, 2}:
return False
if not all((u == 0 or u == 1) for u in x()): # All sets are ordered!
return False
print(f"\n\tThe caller somehow knows that P is {True if cadinality == 2 else False}.\n")
return True
assert check_input(lambda: {0, 1})
assert check_input(lambda: {0})
assert check_input(lambda: {1})
assert check_input(lambda: {7, 8, 9001})
We can wreck it using python using a mean proposition.
I.e. this python interpretation doesn't properly do total computation on comprehended sets
def naturals_stream():
"""
:param x: A 0-ary function that computes and returns a set.
"""
n = 0
while True:
print(f"\tPopping {n}.")
yield n # stream all natural numbers
n += 1
P = lambda: len(set(naturals_stream())) == 7
a = lambda: {u == 0 or P() for u in {0, 1}}
f(a) # won't terminate
====Axiom of Regularity====
For every inhabited set $s$,
there exists an element $t$ in $s$ so that $t$ and $s$ share no elements.
This is a sort of "choice in a single set".
And in particular
$t={0}\implies \neg(0\in s)$
Recall
$u\in b \implies u=0\lor u=1$
$\to$
$u\in b \implies 0\in b\lor u={0}$
So if $t\in b$ is the element postulated to exists by Regularity.
$0\in b\lor \neg(0\in b)$
But recall
$0\in b \iff P$
