Constructive reading of classical logic

## Kleene 58: {(A ⇒ B) ⇔ ~(A ∧ ~B)}

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

{¬(A ∧ ¬B) ⇒ (A ⇒ B)} ⇐ Extract: λf.λa.(CC;nb.ap(f.<a;nb>))
 {¬(A ∧ ¬B) ⇒ (A ⇒ B)} by λ(f.___) f : ¬(A ∧ ¬B) ⊢ {A ⇒ B} by λ(a.___) f : ¬(A ∧ ¬B), a : A ⊢ {B} by (CC{B};nb.___) Classical contradiction f : ¬(A ∧ ¬B), a : A, nb : ¬B ⊢ {B} by ap(f.____) a : A, nb : ¬B ⊢ A ∧ ¬B by pair( slot1 ; slot2 ) a : A, nb : ¬B ⊢ A by a for slot1 a : A, nb : ¬B ⊢ nb by nb 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 (ElimClassical THENA Auto) Unsquash goal | | | | | | | ⊢ ¬(A ∧ ¬B) | | | | 1 2 3 BY (D 0 THENA Auto) | | | | | | | 4. A ∧ ¬B | | | ⊢ False | | | | 1 2 3 BY D 4 | | | | | | | 4. A | | | 5. ¬B | | | ⊢ False | | | | 1 2 3 BY D 3 | | | |\ | | | | 3. A | | | | 4. ¬B | | | | ⊢ A | | | | | 1 2 3 4 BY Hypothesis | | | \ | | | 3. A | | | 4. ¬B | | | 5. B | | | ⊢ False | | | | 1 2 3 BY D 4 | | | | | | | 4. B | | | ⊢ B | | | | 1 2 3 BY Hypothesis | | \ | | 3. ¬(A ∧ ¬B) | | ⊢ {A ⇒ B} | | | 1 2 BY (RepeatFor 2 (D 0) THENA Auto) 1 | | | | | 4. A | | ⊢ {B} | | | 1 2 BY (ClassicalContradiction THENA Auto) Add contradiction of goal to hypotheses | | | | | 5. ¬B | | ⊢ {B} | | | 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