Skip to main content
PRL Project

Constructive reading of classical logic
Table of Contents

Previous Page Next Page

Kleene 62: {~(AB) ⇔ (~A ∨ ~B)}


∀[A,B:ℙ].{¬(A ∧ B) ⇔ (¬A ∨ ¬B)}
{(¬A ∨ ¬B) ⇒ ¬(A ∧ B)} ⇐ Extract: λf.λg.spread(g; a,b.decide(na.ap(na.a);nb.ap(nb.b)))
¬A ∨ ¬B ⇒ ¬(A ∧ B)by λ(f.___)
f: ¬A ∨ ¬B ⊢ ¬(A ∧ B)by λ(g.___)
f: ¬A ∨ ¬B, g : A ∧ B ⊢ Falseby spread(g; a,b.___)
f: ¬A ∨ ¬B, a : A, b : B ⊢ Falseby decide(f;na. slot1 ;nb. slot2 )
na : ¬A, a : A, b : B ⊢ Falseby ap(na.a) for slot1
nb : ¬B, a : A, b : B ⊢ Falseby ap(nb.b) for slot2
{¬(A ∧ B) ⇒ (¬A ∨ ¬B)} ⇒ Extract: λf.(CC;g.inl(λa.ap(g.inr(λb.ap(f.<a;b>)))))
{¬(A ∧ B) ⇔ (¬A ∨ ¬B)}by λ(f.___)
f : ¬(A ∧ B) ⊢ {¬A ∨ ¬B}by (CC{¬A ∨ ¬B};g.___) Classical contradiction
f : ¬(A ∧ B), g : ¬(¬A ∨ ¬B) ⊢ {¬A ∨ ¬B}by inl(___) will also work for inr
f : ¬(A ∧ B), g : ¬(¬A ∨ ¬B) ⊢ {¬A}by λ(a.____)
f : ¬(A ∧ B), g : ¬(¬A ∨ ¬B), a : A ⊢ Falseby ap(g.___)
f : ¬(A ∧ B), a : A ⊢ ¬A ∨ ¬Bby inr(___) choose inl if chose inr before
f : ¬(A ∧ B), a : A ⊢ ¬Bby λ(b.___)
f : ¬(A ∧ B), a : A, b : B ⊢ Falseby ap(f.___)
a : A, b : B ⊢ A ∧ B by pair(a;b)


Nuprl Proof


⊢ ∀[A,B:ℙ]. {¬(A ∧ B) ⇔ (¬A ∨ ¬B)} | BY (D 0 THENA Auto) |\ | 1. A: ℙ | ⊢ ∀[B:ℙ]. {¬(A ∧ B) ⇔ (¬A ∨ ¬B)} | | 1 BY (D 0 THENA Auto) | |\ | | 2. B: ℙ | | ⊢ {¬(A ∧ B) ⇔ (¬A ∨ ¬B)} | | | 1 2 BY RepeatFor 4 ((D 0 THENA Auto)) | | |\ | | | 3. ¬(A ∧ B) | | | ⊢ {(¬A) ∨ (¬B)} | | | | 1 2 3 BY (ClassicalContradiction THENA Auto) Add contradiction of goal to hypotheses | | | | | | | 4. ¬((¬A) ∨ (¬B)) | | | ⊢ {(¬A) ∨ (¬B)} | | | | 1 2 3 BY (ElimClassical¬∑ THENA Auto) Unsquash goal | | | | | | | ⊢ (¬A) ∨ (¬B) | | | | 1 2 3 BY (OrLeft THENA Auto) | | | | | | | ⊢ ¬A | | | | 1 2 3 BY (D 0 THENA Auto) | | | | | | | 5. A | | | ⊢ False | | | | 1 2 3 BY D 4 | | | | | | | 4. A | | | ⊢ (¬A) ∨ (¬B) | | | | 1 2 3 BY (OrRight THENA Auto) | | | | | | | ⊢ ¬B | | | | 1 2 3 BY (D 0 THENA Auto) | | | | | | | 5. B | | | ⊢ False | | | | 1 2 3 BY D 3 | | | | | | | 3. A | | | 4. B | | | ⊢ A ∧ B | | | | 1 2 3 BY D 0 | | | |\ | | | | ⊢ A | | | | | 1 2 3 4 BY Hypothesis | | | \ | | | ⊢ B | | | | 1 2 3 BY Hypothesis | | \ | | 3. (¬A) ∨ (¬B) | | ⊢ {¬(A ∧ B)} | | | 1 2 BY (ElimClassical THENA Auto) Unsquash goal | | | | | ⊢ ¬(A ∧ B) | | | 1 2 BY (D 0 THENA Auto) | | | | | 4. A ∧ B | | ⊢ False | | | 1 2 BY D 4 | | | | | 4. A | | 5. B | | ⊢ False | | | 1 2 BY D 3 | | |\ | | | 3. ¬A | | | ⊢ False | | | | 1 2 3 BY D 3 | | | | | | | 3. A | | | 4. B | | | ⊢ A | | | | 1 2 3 BY Hypothesis | | \ | | 3. ¬B | | ⊢ False | | | 1 2 BY D 3 | | | | | 3. A | | 4. B | | ⊢ B | | | 1 2 BY Hypothesis | \ | 2. B: ℙ | 3. {x:Unit| ¬(A ∧ B) ⇔ (¬A ∨ ¬B)} | ⊢ Ax ∈ {x:Unit| ¬(A ∧ B) ⇔ (¬A ∨ ¬B)} | | 1 BY Auto \ 2 1. A: ℙ 2. B: ℙ 3. {x:Unit| ¬(A ∧ B) ⇔ (¬A ∨ ¬B)} ⊢ Ax ∈ {x:Unit| ¬(A ∧ B) ⇔ (¬A ∨ ¬B)} | BY Auto PDF version of proof

Previous Page Next Page


Table of Contents