This theorem states that the law of excluded middle follows from
the axiom of choice.
Proof sketch
Let A be an arbitrary proposition. Consider the two sets
X := {x | x ∈ {0, 1} ∧ (A ∨ (x = 0))},
Y := {y | y ∈ {0, 1} ∧ (A ∨ (y = 1))},
which are non-empty due to 0 ∈ X and 1 ∈ Y, respectively. Accordingly,
there exists a choice function f: {X, Y} → X ∪ Y with f X ∈ X and
f Y ∈ Y. Since f X ∈ {0, 1} and f Y ∈ {0, 1}, there are only four
cases for the function values in total. We perform a case distinction.
In the two cases where f Y = 0, it holds that 0 ∈ Y, which simplifies
to A ∨ (0 = 1), i.e., to A, by which A ∨ ¬A is all the more true.
In the two cases where f X = 1, it holds that 1 ∈ X, which simplifies
to A ∨ (1 = 0), i.e., to A, by which A ∨ ¬A is all the more true.
In the remaining case f X = 0, f Y = 1, ¬A must hold, because
assuming A would imply f X = f Y, hence 0 = 1, which is absurd.
With ¬A, A ∨ ¬A is all the more true. Thus, A ∨ ¬A is shown in all
cases. q.e.d.
Proof
let X = {x | x ∈ {∅, {∅}} ∧ (A ∨ x = ∅)}.
let Y = {y | y ∈ {∅, {∅}} ∧ (A ∨ y = {∅})}.
001. ⊢ set ∅, empty_set_is_set.
002. ⊢ set {∅}, set_sg 1.
003. ⊢ ∅ ∈ {∅, {∅}}, in21 1.
004. ⊢ {∅} ∈ {∅, {∅}}, in22 2.
005. ⊢ u = u, eq_refl.
006. ⊢ A ∨ u = u, disj_intror 5.
007. ⊢ A ∨ ∅ = ∅, 6.
008. ⊢ A ∨ {∅} = {∅}, 6.
009. ⊢ ∅ ∈ {∅, {∅}} ∧ (A ∨ ∅ = ∅), conj_intro 3 7.
010. ⊢ {∅} ∈ {∅, {∅}} ∧ (A ∨ {∅} = {∅}), conj_intro 4 8.
011. ⊢ ∅ ∈ X, comp_intro 1 9, P x ↔ x ∈ {∅, {∅}} ∧ (A ∨ x = ∅).
012. ⊢ {∅} ∈ Y, comp_intro 2 10, P y ↔ y ∈ {∅, {∅}} ∧ (A ∨ y = {∅}).
013. ⊢ set {{∅}}, set_sg 2.
014. ⊢ set {∅, {∅}}, set_union 2 13.
015. ⊢ set X, sep_is_set 14.
016. ⊢ set Y, sep_is_set 14.
017. 17 ⊢ u ∈ {X, Y} ∩ {∅}, hypo.
018. 17 ⊢ u ∈ {∅}, intersection_elimr 17.
019. 17 ⊢ u = ∅, sg_elim 1 18.
020. 17 ⊢ u ∈ {X, Y}, intersection_eliml 17.
021. 17 ⊢ u ∈ {X} ∨ u ∈ {Y}, union_elim 20.
022. 22 ⊢ u ∈ {X}, hypo.
023. 22 ⊢ u = X, sg_elim 15 22.
024. 22 ⊢ X = u, eq_symm 23.
025. 17, 22 ⊢ X = ∅, eq_trans 24 19.
026. 17, 22 ⊢ ∅ ∈ ∅, eq_subst 25 11, P t ↔ ∅ ∈ t.
027. 17, 22 ⊢ u ∈ ∅, empty_efq 26.
028. 28 ⊢ u ∈ {Y}, hypo.
029. 28 ⊢ u = Y, sg_elim 16 28.
030. 28 ⊢ Y = u, eq_symm 29.
031. 17, 28 ⊢ Y = ∅, eq_trans 30 19.
032. 17, 28 ⊢ {∅} ∈ ∅, eq_subst 31 12, P t ↔ {∅} ∈ t.
033. 17, 28 ⊢ u ∈ ∅, empty_efq 32.
034. 17 ⊢ u ∈ ∅, disj_elim 21 27 33.
035. ⊢ u ∈ {X, Y} ∩ {∅} → u ∈ ∅, subj_intro 34.
036. ⊢ ∀u. u ∈ {X, Y} ∩ {∅} → u ∈ ∅, uq_intro 35.
037. ⊢ {X, Y} ∩ {∅} ⊆ ∅, incl_intro 36.
038. ⊢ ∅ ⊆ {X, Y} ∩ {∅}, empty_set_is_least.
039. ⊢ {X, Y} ∩ {∅} = ∅, incl_antisym 37 38.
040. ⊢ {X, Y} \ {∅} = {X, Y}, diff_disjoint 39.
041. 41 ⊢ ∀M. ∃f. choice_function f ∧ dom f = M \ {∅}, hypo.
042. 41 ⊢ ∃f. choice_function f ∧ dom f = {X, Y} \ {∅}, uq_elim 41.
043. 43 ⊢ choice_function f ∧ dom f = {X, Y} \ {∅}, hypo.
044. 43 ⊢ choice_function f, conj_eliml 43.
045. 43 ⊢ dom f = {X, Y} \ {∅}, conj_elimr 43.
046. 43 ⊢ dom f = {X, Y}, eq_trans 45 40.
047. 43 ⊢ function f ∧ ∀x. x ∈ dom f → app f x ∈ x,
choice_fn_unfold 44.
048. 43 ⊢ function f, conj_eliml 47.
049. 43 ⊢ ∀x. x ∈ dom f → app f x ∈ x, conj_elimr 47.
050. ⊢ X ⊆ {∅, {∅}}, sep_is_subclass.
051. ⊢ Y ⊆ {∅, {∅}}, sep_is_subclass.
052. ⊢ X ∈ {X, Y}, in21 15.
053. ⊢ Y ∈ {X, Y}, in22 16.
054. 43 ⊢ X ∈ dom f, eq_subst_rev 46 52, P u ↔ X ∈ u.
055. 43 ⊢ Y ∈ dom f, eq_subst_rev 46 53, P u ↔ Y ∈ u.
056. 43 ⊢ app f X ∈ X, uq_bounded_elim 49 54.
057. 43 ⊢ app f Y ∈ Y, uq_bounded_elim 49 55.
058. 43 ⊢ app f X ∈ {∅, {∅}} ∧ (A ∨ app f X = ∅), comp_elim 56.
059. 43 ⊢ app f Y ∈ {∅, {∅}} ∧ (A ∨ app f Y = {∅}), comp_elim 57.
060. 43 ⊢ A ∨ app f X = ∅, conj_elimr 58.
061. 43 ⊢ A ∨ app f Y = {∅}, conj_elimr 59.
062. 43 ⊢ app f X ∈ {∅, {∅}}, conj_eliml 58.
063. 43 ⊢ app f Y ∈ {∅, {∅}}, conj_eliml 59.
064. 43 ⊢ app f X ∈ {∅} ∨ app f X ∈ {{∅}}, union_elim 62.
065. 43 ⊢ app f Y ∈ {∅} ∨ app f Y ∈ {{∅}}, union_elim 63.
066. 66 ⊢ app f Y ∈ {∅}, hypo.
067. 66 ⊢ app f Y = ∅, sg_elim 1 66.
068. 43, 66 ⊢ A ∨ ∅ = {∅}, eq_subst 67 61, P u ↔ A ∨ u = {∅}.
069. 43, 66 ⊢ A, tollendo_ponens_left 68 zero_neq_one.
070. 43, 66 ⊢ A ∨ ¬A, disj_introl 69.
071. 71 ⊢ app f Y ∈ {{∅}}, hypo.
072. 71 ⊢ app f Y = {∅}, sg_elim 2 71.
073. 73 ⊢ app f X ∈ {∅}, hypo.
074. 73 ⊢ app f X = ∅, sg_elim 1 73.
075. 75 ⊢ A, hypo.
076. 76 ⊢ u ∈ X, hypo.
077. 76 ⊢ u ∈ {∅, {∅}} ∧ (A ∨ u = ∅), comp_elim 76.
078. 76 ⊢ u ∈ {∅, {∅}}, conj_eliml 77.
079. 75 ⊢ A ∨ u = {∅}, disj_introl 75.
080. 75, 76 ⊢ u ∈ {∅, {∅}} ∧ (A ∨ u = {∅}), conj_intro 78 79.
081. 76 ⊢ set u, set_intro 78.
082. 75, 76 ⊢ u ∈ Y, comp_intro 81 80.
083. 75 ⊢ u ∈ X → u ∈ Y, subj_intro 82.
084. 84 ⊢ u ∈ Y, hypo.
085. 84 ⊢ u ∈ {∅, {∅}} ∧ (A ∨ u = {∅}), comp_elim 84.
086. 84 ⊢ u ∈ {∅, {∅}}, conj_eliml 85.
087. 75 ⊢ A ∨ u = ∅, disj_introl 75.
088. 75, 84 ⊢ u ∈ {∅, {∅}} ∧ (A ∨ u = ∅), conj_intro 86 87.
089. 84 ⊢ set u, set_intro 86.
090. 75, 84 ⊢ u ∈ X, comp_intro 89 88.
091. 75 ⊢ u ∈ Y → u ∈ X, subj_intro 90.
092. 75 ⊢ u ∈ X ↔ u ∈ Y, bij_intro 83 91.
093. 75 ⊢ ∀u. u ∈ X ↔ u ∈ Y, uq_intro 92.
094. 75 ⊢ X = Y, ext 93.
095. 75 ⊢ app g X = app g Y, eq_cong 94, f x = app g x.
096. 75 ⊢ app f X = app f Y, 95.
097. 73 ⊢ ∅ = app f X, eq_symm 74.
098. 73, 75 ⊢ ∅ = app f Y, eq_trans 97 96.
099. 71, 73, 75 ⊢ ∅ = {∅}, eq_trans 98 72.
100. 71, 73, 75 ⊢ ⊥, neg_elim zero_neq_one 99.
101. 71, 73 ⊢ ¬A, neg_intro 100.
102. 71, 73 ⊢ A ∨ ¬A, disj_intror 101.
103. 103 ⊢ app f X ∈ {{∅}}, hypo.
104. 103 ⊢ app f X = {∅}, sg_elim 2 103.
105. 43, 103 ⊢ A ∨ {∅} = ∅, eq_subst 104 60, P u ↔ A ∨ u = ∅.
106. ⊢ ¬{∅} = ∅, neq_symm zero_neq_one.
107. 43, 103 ⊢ A, tollendo_ponens_left 105 106.
108. 43, 103 ⊢ A ∨ ¬A, disj_introl 107.
109. 43, 71 ⊢ A ∨ ¬A, disj_elim 64 102 108.
110. 43 ⊢ A ∨ ¬A, disj_elim 65 70 109.
111. 41 ⊢ A ∨ ¬A, ex_elim 42 110.
Diaconescu_Goodman_Myhill_theorem. ⊢
(∀M. ∃f. choice_function f ∧ dom f = M \ {∅}) →
A ∨ ¬A, subj_intro 111.
Dependencies
The given proof depends on nine axioms:
comp, efq, eq_refl, eq_subst, ext, infinity, pairing, subset, union.