Constructive reading of classical logic
Table of Contents
Pierce's Law: {((A ⇒ B) ⇒ A) ⇒ A}
This theorem can not be solved constructively so we must use the classical contradiction rule. We can use the construction rule to get {A} as our goal. If we apply the construction rule over squashed terms we are technically getting {((A ⇒ B) ⇒ A)} ⊢ {A}. However since our goal is still squashed we can open the hypothesis that is squashed to get ((A ⇒ B) ⇒ A) ⊢ {A}. Therefore whenever we present the construction rule we omit the middle step of removing the curly brackets on the hypothesis.
| {((A ⇒ B) ⇒ A) ⇒ A} | by λ(f.___) |
| f : (A ⇒ B) ⇒ A ⊢ {A} | by (CC{A};na.___) Classical contradiction |
| f : (A ⇒ B) ⇒ A, na : ¬A ⊢ {A} | by apseq(f;___;a.a) |
| na : ¬A ⊢ A ⇒ B | by λ(a.___) |
| na : ¬A, a : A ⊢ B | by apseq(na;a;False.any(..)) |
Nuprl Proof
⊢ ∀[A,B: ℙ]. {((A ⇒ B) ⇒ A) ⇒ A}
|
BY (D 0 THENA Auto)
|\
[1]. A: ℙ
⊢ ∀[B: ℙ]. {((A ⇒ B) ⇒ A) ⇒ A}
|
BY (D 0 THENA Auto)
|
| |\
| | 2. B: ℙ
| | ⊢ {((A ⇒ B) ⇒ A) ⇒ A}
| | |
1 2 BY RepeatFor 2 ((D 0 THENA Auto))
| | |
| | 3. (A ⇒ B) ⇒ A
| | ⊢ {A}
| | |
1 2 BY (ClassicalContradiction THENA Auto) Add contradiction of goal to hypotheses
| | |
| | 4. ¬A
| | ⊢ {A}
| | |
1 2 BY D 3
| | |\
| | | 3. ¬A
| | | ⊢ A ⇒ B
| | | |
1 2 3 BY (D 0 THENA Auto)
| | | |
| | | 4. A
| | | ⊢ B
| | | |
1 2 3 BY D 3
| | | |
| | | 3. A
| | | ⊢ A
| | | |
1 2 3 BY Hypothesis
| | \
| | 3. ¬A
| | 4. A
| | ⊢ {A}
| | |
1 2 BY ElimClassical
| | |
| | ⊢ A
| | |
1 2 BY Hypothesis
| \
| 2. B: ℙ
| 3. {x:Unit| ((A ⇒ B) ⇒ A) ⇒ A}
| ⊢ Ax ∈ {x:Unit| ((A ⇒ B) ⇒ A) ⇒ A}
| |
1 BY Auto
\
1. A: ℙ
2. B: ℙ
3. {x:Unit| ((A ⇒ B) ⇒ A) ⇒ A}
⊢ Ax ∈ {x:Unit| ((A ⇒ B) ⇒ A) ⇒ A}
|
BY Auto
PDF version of proof
Table of Contents