Constructive reading of classical logic
Table of Contents
Kleene 59: {(A ⇒ B) ⇔ (~A ∨ B)}
The extract of the backwards direction shows the constructive part of the proof. It can be done without classical reasoning. We see that in choosing ¬A of the or disjunction with evidence na we can create evidence for A ⇒ B because when we build the function that assumes A in order to prove B, we have the context λx. __ where x is of type A. Therefore na(x) will be in the type False, and we can use any(na(x)) as evidence for B. Thus λx.any(na(x)) is evidence for A ⇒ B under the assumption na in the decide operator.
The forward direction, (A ⇒ B) ⇒(¬A ∨ B) can not be proved constructively -- although we do not give that argument here, it is not difficult to show this. Therefore we need a use classical contradiction. This will provide evidence needed to prove the goal. We choose inl then do a construction rule. We then apply our newly generated evidence, and do inr to yield B as our goal. We can get B by applying the function A ⇒ B to A, which we have evidence for.
| ¬A ∨ B ⇒ A ⇒ B | by λ(f.___) |
| f : ¬A ∨ B ⊢ A ⇒ B | by λ(a.___) |
| f : ¬A ∨ B, a : A ⊢ B | by decide(f; na. slot1 ;b. slot2 ) |
| na : ¬A, a : A ⊢ B | by apseq(na;a;False.any(..)) for slot1 |
| b : B, A ⊢ B | by b for slot2 |
{(¬A ∨ B) ⇒ (A ⇒ B)}
⇒ Extract: λf.(CC;g.inl(λa.ap(g.inr(ap(f.a)))))
| {(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(___) |
| f : A ⇒ B, g : ¬(¬A ∨ B) ⊢ {¬A} | by λ(a.___) |
| f : A ⇒ B, g : ¬(¬A ∨ B), a : A ⊢ False | by ap(g.___) |
| f : A ⇒ B, a : A ⊢ ¬A ∨ B | by inr(___) |
| f : A ⇒ B, a : A ⊢ B | by ap(f.a) |
Nuprl Proof
⊢ ∀[A,B:ℙ]. {(A ⇒ B) ⇔ (¬A ∨ B)}
|
BY (D 0 THENA Auto)
|\
| 1. A: ℙ
| ⊢ ∀[B:P]. {(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 3
| | | |\
| | | | 3. A
| | | | ⊢ A
| | | | |
1 2 3 4 BY Hypothesis
| | | \
| | | 3. A
| | | 4. B
| | | ⊢ B
| | | |
1 2 3 BY Hypothesis
| | \
| | 3. (¬A) ∨ B
| | ⊢ {A ⇒ B}
| | |
1 2 BY (RepeatFor 2 (D 0) THENA Auto)
| | |
| | 4. A
| | ⊢ {B}
| | |
1 2 BY ElimClassical Unsquash goal
| | |
| | ⊢ B
| | |
1 2 BY D 3
| | |\
| | | 3. ¬A
| | | ⊢ B
| | | |
1 2 3 BY D 3
| | | |
| | | 3. A
| | | ⊢ A
| | | |
1 2 3 BY Hypothesis
| | \
| | 3. 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
\
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