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: ℙ]. {((A ⇒ B) ⇒ A) ⇒ A}
Extract: λf.(CC;na.ap(f.λa.any(ap(na.a))))
 {((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