選択公理または基礎の公理から排中律

------------------------------------------------------------------------

Theorem Exy1sbの証明図の主要部分
[He:Exy1 P y]
x∈y <-> (x = s1∧P)∨x = s2
[Hx:x∈y] x∈y -> (x = s1∧P)∨x = s2
(x = s1∧P)∨x = s2
↓
↓ [Hs1:x = s1∧P]    
↓ x = s1 [Hs2:x = s2]
↓ x = s1∨x = s2 x = s1∨x = s2 Hs1,Hs2

x = s1∨x = s2

↓

 [Hsp:SPairf]
x∈{ s1 , s2 } Hx
x∈y -> x∈{ s1 , s2 }
y⊆ { s1 , s2 }

Theorem Exyeqの証明のための準備。ファイルa+0acsh.vの証明を改良。
[H1:x = s1] [p:P]
[Hxs:x∈{ s1 , s2 }] [Hsp:SPairf] x = s1∧P [H2:x = s2]
x = s1∨x = s2 (x = s1∧P)∨x = s2 (x = s1∧P)∨x = s2 H1,H2
(x = s1∧P)∨x = s2
↓
↓ [He:Exy1 P y]
↓ x∈y <-> (x = s1∧P)∨x = s2
↓ (x = s1∧P)∨x = s2 -> x∈y

x∈y

 Hxs
x∈{ s1 , s2 } -> x∈y
{ s1 , s2 }⊆y He,p
Exy1 P y -> P -> { s1 , s2 }⊆y
∀P∀y, Exy1 P y -> P -> { s1 , s2 }⊆y Hsp
SPairf -> ∀P∀y(Exy1 P y -> P -> { s1 , s2 }⊆y)
これに上記の
Theorem Exy1sb : SPairf -> ∀P∀y(Exy1 P y -> y⊆{ s1 , s2 })
を合わせれば
SPairf -> ∀P∀y(Exy1 P y -> P -> y /= { s1 , s2 })
が証明できる。同様に
SPairf -> ∀P∀y(Exy2 P y -> P -> y /= { s1 , s2 })
であるから、そこから
Theorem Exyeq : Set_eq -> SPairf -> ∀P∀y1∀y2 (Exy1 P y1 -> Exy2 P y2 -> P -> y1 = y2).
を証明するのはやさしい。

Theorem Exy2Pの証明図の主要部分
[He:Exy2 P y]
s1∈y <-> (s1 = s1∧P)∨s1 = s2
[Hs1:s1∈y] s1∈y -> (s1 = s1∧P)∨s1 = s2
(s1 = s1∧P)∨s1 = s2
↓ [Hd:Dist]
↓ [Hs12:s1 = s2] s1 ≠ s2
↓ [Hs1p:s1 = s1∧P] False
↓ P P Hs1p,Hs12
P

Theorem AC2EMpの証明図の主要部分
[Exyfy1] [Hpe:PrEmp] [Hsp:SPairf] [Hac:ACf] [He1:Exy1 P y1] [He2:Exy2 P y2]
∃f:Set, (f ` y1)∈y1∧(f ` y2)∈y2
↓
↓

[Hfy:(f ` y1)∈y1∧(f ` y2)∈y2]
↓ [Hfy1:(f ` y1)∈y1] [Hfy2:(f ` y2)∈y2]
↓
↓ [Exy1sb] [Hsp]
↓ [He1] Exy1 P y1 -> (y1⊆{ s1 , s2 })
↓ [Hfy1] y1⊆{ s1 , s2 }
↓ [Hsp] (f ` y1)∈{ s1 , s2 }
↓ (f ` y1) = s1∨(f ` y1) = s2
↓ ↓
↓ ↓ [Exy2sb] [Hsp] [He2] [Hfy2]
↓ ↓ 上記と同様に
↓ ↓ (f ` y2) = s1∨(f ` y2) = s2
↓ ↓ ↓
↓ ↓ ↓ [Exy2P] [Hd:Dist] [H21:(f ` y2) = s1] [Hfy2:(f ` y2)∈y2]
↓ ↓ ↓ Exy2 P y2 -> (s1∈y2) -> P [He2] s1∈y2
↓ ↓ ↓ P
↓ ↓ ↓ P∨¬P
↓ ↓ ↓ ↓
↓ ↓ ↓ ↓ [Exyeq] [Hse:Set_eq] [Hsp] [He1] [He2] [p:P]
↓ ↓ ↓ ↓ y1 = y2
↓ ↓ ↓ ↓ ↓
↓ ↓ ↓ ↓ ↓ [Hd]
↓ ↓ ↓ ↓ ↓ s1 ≠ s2 [H11:(f ` y1) = s1] [H22:(f ` y2) = s2]
↓ ↓ ↓ ↓ (f ` y1) = (f ` y2) (f ` y1) ≠ (f ` y2)
↓ ↓ ↓ ↓ False p
↓ ↓ ↓ ↓ ¬P
↓ ↓ ↓ ↓ P∨¬P H21,H22
↓ ↓ P∨¬P [H12:(f ` y1) = s2] [Hfy1:(f ` y1)∈y1]
↓ ↓ ↓

s2∈y1
↓ ↓ ↓ [Exy1P] [Hd]

↓
↓ ↓ ↓

Exy1 P y1 -> (s2∈y1) -> P

 [He1]

↓

 
↓ ↓ ↓ P
↓ ↓ ↓ P∨¬P H11,H12
↓ P∨¬P Hfy
P∨¬P

これでほぼ、選択公理ACfから、排中律が導かれているのがわかると思う。

------------------------------------------------------------------------

Theorem EmRgpの証明図の主要部分
Section AC2EMsの中では、Exy2 P y2であったが、Section AC2EMsの外に出てしまったので引数が2つ増えてExy2 s1 s2 P y2となっている。
[Exy2in]
Exy2 s1 s2 P y2 -> s2∈y2 [He2:Exy2 s1 s2 P y2]
s2∈y2
[Hrg:SReg] ∃y:Set, y∈y2
∃y:Set, (y∈y2)∧∀z:Set, ¬((z∈y2)∧(z∈y))
↓
↓ [Hyy:(y∈y2)∧∀z:Set, ¬((z∈y2)∧(z∈y))]
↓ [Hyy2:y∈y2] [Hy2y:∀z:Set, ¬(z∈y2∧z∈y)]
↓
↓ [He2] [Hyy2] [Hsp]
↓ (y = s1∧P)∨y = s2 s∈{`s} [Hs1:s1 = s] [Hs2:s2 = {`s}]
↓ ↓

s1∈s2

 [Hys2:y = s2]
↓ ↓ [Exy21in] [Hsp:SPairf] s1∈y
↓ ↓ P -> Exy2 s1 s2 P y2 -> s1∈y2 [p:P] [He2] ↓
↓ ↓

s1∈y2

 ↓
↓ ↓ [Hy2y] s1∈y2∧s1∈y
↓ ↓ ¬(s1∈y2∧s1∈y) ↓
↓ ↓ False p [Hys:y = s1∧P]
↓ ↓ ¬P P
↓ ↓ P∨¬P P∨¬P Hys,Hys2
↓ P∨¬P Hyy
P∨¬P
これでほぼ、基礎の公理SRegから、排中律が導かれているのがわかると思う。

------------------------------------------------------------------------

もどる