Skip to main content
PRL Project

Constructive reading of classical logic
Table of Contents

Previous Page Next Page

Kleene 60: {(AB) ⇔ ~(A ⇒ ~B)}


∀[A,B: ℙ]. {(A ∧ B) ⇔ ¬(A ⇒ ¬B)}
{(A ∧ B) ⇒ ¬(A ⇒ ¬B)} ⇒ Extract: λf.λg.spread(f; a,b.ap(ap(g.a).b))
A ∧ B ⇒ ¬(A ⇒ ¬B)by λ(f.___)
f : A ∧ B ⊢ ¬(A ⇒ ¬B)by λ(g.___)
f : A ∧ B, g : A ⇒ ¬B ⊢ Falsespread(f; a,b.___)
a : A, b : B, g : A ⇒ ¬B ⊢ Falseby apseq(g;a;nb.___)
a : A, b : B, nb : ¬B ⊢ Falseby ap(nb.___)
a : A, b : B ⊢ Bby b


{¬(A ⇒ ¬B) ⇒ (A ∧ B)} ⇐ Extract: λf.(CC;g.ap(f.λa.λb.ap(g.<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 ap(f.____)
g : ¬(A ∧ B) ⊢ A ⇒ ¬ Bby λ(a.____)
g : ¬(A ∧ B), a : A ⊢ ¬ B by λ(b.___)
g : ¬(A ∧ B), a : A, b : B ⊢ False by ap(g.___)
a : A, b : B ⊢ A ∧ B by pair( slot1 ; slot2 )
a : A, b : B ⊢ A by a for slot1
a : A, b : B ⊢ B by b for slot2

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 D 3 | | | | | | | 3. A | | | 4. B | | | ⊢ {¬(A ⇒ (¬B))} | | | | 1 2 3 BY (ElimClassical THENA Auto) Unsquash goal | | | | | | | ⊢ ¬(A ⇒ (¬B)) | | | | 1 2 3 BY (D 0 THENA Auto) | | | | | | | 5. A ⇒ (¬B) | | | ⊢ False | | | | 1 2 3 BY D 5 | | | |\ | | | | ⊢ A | | | | | 1 2 3 4 BY Hypothesis | | | \ | | | 5. ¬B | | | ⊢ False | | | | 1 2 3 BY D 5 | | | | | | | ⊢ B | | | | 1 2 3 BY Hypothesis | | \ | | 3. ¬(A ⇒ (¬B)) | | ⊢ {A ∧ B} | | | 1 2 BY (ClassicalContradiction THENA Auto) Add contradiction of goal to hypotheses | | | | | 4. ¬(A ∧ B) | | ⊢ {A ∧ B} | | | 1 2 BY D 3 | | | | | 3. ¬(A ∧ B) | | ⊢ A ⇒ (¬B) | | | 1 2 BY RepeatFor 2 ((D 0 THENA Auto)) | | | | | 4. A | | 5. B | | ⊢ False | | | 1 2 BY D 3 | | | | | 3. A | | 4. B | | ⊢ A ∧ B | | | 1 2 BY D 0 | | |\ | | | ⊢ A | | | | 1 2 3 BY Hypothesis | | \ | | ⊢ B | | | 1 2 BY Hypothesis | \ | 2. B: ℙ | 3. {x:Unit| A ∧ B ⇔ ¬(A ⇒ (¬B))} | ⊢ Ax ∈ {x:Unit| A ∧ B ⇔ ¬(A ⇒ (¬B))} | | 1 BY Auto \ 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