Constructive reading of classical logic
Table of Contents
Kleene 52: {A ∧(B ∨ ~B) ⇔ A}
| A ∧ (B ∨ ¬B) ⇒ A | by λ(f.___) |
| aabonb : A ∧ (B ∨ ¬B) ⊢ A | by spread(f; a,g.___) |
| a : A, bonb : (B ∨ ¬B) ⊢ A | by a |
{A ⇒ A ∧ (B ∨ ¬B)}
⇐ Extract: λa.(CC;f.<a;inr(λb.ap(f.pair(a;inl(b))))>)
| {A ⇒ A ∧ (B ∨ ¬B)} | by λ(a.___) |
| a : A ⊢ {A ∧ (B ∨ ¬B)} | by (CC{A ∧ (B ∨ ¬B)};f.___) Classical contradiction |
| a : A, f : ¬(A ∧ (B ∨ ¬B)) ⊢ {A ∧ (B ∨ ¬B)} | by pair( slot1 ; slot2 ) |
| a : A, f : ¬(A ∧ (B ∨ ¬B)) ⊢ {A} | by a for slot1 |
| a : A, f : ¬(A ∧ (B ∨ ¬B)) ⊢ {B ∨ ¬B} | by inr(___) for slot2 |
| a : A, f : ¬(A ∧ (B ∨ ¬B)) ⊢ {¬B} | by λ(b.___) |
| a : A, f : ¬(A ∧ (B ∨ ¬B)), b : B ⊢ False | by ap(f.___) |
| a : A, b : B ⊢ A ∧ (B ∨ ¬B) | by pair( slot3 ; slot4 ) |
| a : A, b : B ⊢ A | by a for slot3 |
| a : A, b : B ⊢ B ∨ ¬B | by inl(___) for slot4 |
| a : A, b : B ⊢ B | by b |
Nuprl Proof
⊢ ∀[A,B:ℙ]. {A ∧ (B ∨ ¬B) ⇔ A}
|
BY (D 0 THENA Auto)
|\
| 1. A: ℙ
| ⊢ ∀[B:ℙ]. {A ∧ (B ∨ (¬B)) ⇔ A}
| |
1 BY (D 0 THENA Auto)
| |\
| | 2. B: ℙ
| | ⊢ {A ∧ (B ∨ (¬B)) ⇔ A}
| | |
1 2 BY RepeatFor 4 ((D 0 THENA Auto))
| | |\
| | | 3. A ∧ (B ∨ (¬B))
| | | ⊢ {A}
| | | |
1 2 3 BY D 3
| | | |
| | | 3. A
| | | 4. B ∨ (¬B)
| | | ⊢ {A}
| | | |
1 2 3 BY ElimClassical Unsquash goal
| | | |
| | | ⊢ A
| | | |
1 2 3 BY Hypothesis
| | \
| | 3. A
| | ⊢ {A ∧ (B ∨ (¬B))}
| | |
1 2 BY (ClassicalContradiction THENA Auto) Add contradiction of goal to hypotheses
| | |
| | 4. ¬(A ∧ (B ∨ (¬B)))
| | ⊢ {A ∧ (B ∨ (¬B))}
| | |
1 2 BY (ElimClassical THENA Auto) Unsquash goal
| | |
| | ⊢ A ∧ (B ∨ (¬B))
| | |
1 2 BY D 0
| | |\
| | | ⊢ A
| | | |
1 2 3 BY Hypothesis
| | \
| | ⊢ B ∨ (¬B)
| | |
1 2 BY (OrRight THENA Auto)
| | |
| | ⊢ ¬B
| | |
1 2 BY (D 0 THENA Auto)
| | |
| | 5. B
| | ⊢ False
| | |
1 2 BY D 4
| | |
| | 4. B
| | ⊢ A ∧ (B ∨ (¬B))
| | |
1 2 BY D 0
| | |\
| | | ⊢ A
| | | |
1 2 3 BY Hypothesis
| | \
| | ⊢ B ∨ (¬B)
| | |
1 2 BY (OrLeft THENA Auto)
| | |
| | ⊢ B
| | |
1 2 BY Hypothesis
| \
| 2. B: ℙ
| 3. {x:Unit| A ∧ (B ∨ (¬B)) ⇔ A}
| ⊢ Ax ∈ {x:Unit| A ∧ (B ∨ (¬B)) ⇔ A}
| |
1 BY Auto
\
1. A: ℙ
2. B: ℙ
3. {x:Unit| A ∧ (B ∨ (¬B)) ⇔ A}
⊢ Ax ∈ {x:Unit| A ∧ (B ∨ (¬B)) ⇔ A}
|
BY Auto
PDF version of proof
Table of Contents