Constructive reading of classical logic
Table of Contents
Kleene 60: {(A ∧ B) ⇔ ~(A ⇒ ~B)}
| A ∧ B ⇒ ¬(A ⇒ ¬B) | by λ(f.___) |
| f : A ∧ B ⊢ ¬(A ⇒ ¬B) | by λ(g.___) |
| f : A ∧ B, g : A ⇒ ¬B ⊢ False | spread(f; a,b.___) |
| a : A, b : B, g : A ⇒ ¬B ⊢ False | by apseq(g;a;nb.___) |
| a : A, b : B, nb : ¬B ⊢ False | by ap(nb.___) |
| a : A, b : B ⊢ B | by 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 ⇒ ¬ B | by λ(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
Table of Contents