Kleene 57

PRL Home Introduction Math Library Publications Projects System

Seminar People The Book Lectures Other Groups

Constructive reading of classical logic

Kleene 57: {(A ∧ B) ⇔ ~(~A ∨ ~B)}

This theorem is interesting because we have to use classical contradiction twice in order to prove the non constructive direction. At the squashed goal {A ∧ B}, we have the hypothesis ¬(¬A ∨ ¬B), which by DeMorgan's law, is equivalent to (A ∧ B). However we couldn't prove our goal without the classical contradicion because we lack the necessary evidence; we omit the details here and leave it as an exercise for the reader. We must therefore use the new rule to prove this. We first separate the ∧ and are left with two goals, ⊢{A} and ⊢{B}. We will only consider the {A} case here, as the {B} case proceeds similarly -- see the full proof below. We can use classical contradiction to get evidence for ¬A. Then we use the application rule on ¬(¬A ∨ ¬ B), taking advantage of ex falso quodlibit. We choose the left disjunctive because we know we have evidence for ¬A. The {B} case proceeds exactly the same except we would choose the right disjunctive since our evidence is ¬B.

If we had done classical contradiction on (A ∧ B) without splitting the pair, then we would have come to an impass in the proof where we would be missing evidence for either A or B. This is the only proof of Kleene's that is not doubly squashed that requires two instances of classical contradiction.

∀[A,B: ℙ]. {(A ∧ B) ⇔ ¬(¬A ∨ ¬B)} {(A ∧ B) ⇒ ¬(¬A ∨ ¬B)} ⇒ Extract: λf.λg.spread(f; a,b.decide(g; 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 ⊢ False	by spread(f; a,b.___)
a : A, b : B, g : ¬A ∨ ¬ B ⊢ False	by decide(g; na. slot1 ; nb. slot2 )
a : A, b : B, na: ¬A ⊢ False	by ap(na.a) for slot1
a : A, b : B, nb : ¬ B ⊢ False	by ap(nb.b) for slot2

{¬(¬A ∨ ¬B) ⇒ (A ∧ B)} ⇐ Extract: λf.<CC;na.ap(f.inl(na));CC;nb.ap(f.inr(nb))>

{¬(¬A ∨ ¬B) ⇒ (A ∧ B)}	by λ(f.___)
f : ¬(¬A ∨ ¬B) ⊢ {A ∧ B}	by pair( slot1 ; slot2 )
f : ¬(¬A ∨ ¬B) ⊢ {A}	by (CC{A};na.___) Classical contradiction, for slot1
f : ¬(¬A ∨ ¬B), na : ¬A ⊢ {A}	by ap(f.___)
na : ¬A ⊢ ¬A ∨ ¬B	by inl(___)
na : ¬A ⊢ ¬A	by na
f : ¬(¬A ∨ ¬B) ⊢ {B}	by (CC{B};nb.___) Classical contradiction, for slot2
f : ¬(¬A ∨ ¬B), nb : ¬B ⊢ {B}	by ap(f.___)
nb : ¬B ⊢ ¬A ∨ ¬B	by inr(___)
nb: ¬B ⊢ ¬B	by nb

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 3 | | | | | | | 3. A | | | 4. B | | | 5. (¬A) ∨ (¬B) | | | ⊢ False | | | | 1 2 3 BY D 5 | | | |\ | | | | 5. ¬A | | | | ⊢ False | | | | | 1 2 3 4 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 RepeatFor 2 (D 0) | | |\ | | | ⊢ {A} | | | | 1 2 3 BY (ClassicalContradiction THENA Auto) Add contradiction of goal to hypotheses | | | | | | | 4. ¬A | | | ⊢ {A} | | | | 1 2 3 BY D 3 | | | | | | | 3. ¬A | | | ⊢ (¬A) ∨ (¬B) | | | | 1 2 3 BY (OrLeft THENA Auto) | | | | | | | ⊢ ¬A | | | | 1 2 3 BY Hypothesis | | \ | | ⊢ {B} | | | 1 2 BY (ClassicalContradiction THENA Auto) Add contradiction of goal to hypotheses | | | | | 4. ¬B | | ⊢ {B} | | | 1 2 BY D 3 | | | | | 3. ¬B | | ⊢ (¬A) ∨ (¬B) | | | 1 2 BY (OrRight THENA Auto) | | | | | ⊢ ¬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

Table of Contents