//
Skip to main content
PRL Project

Constructive reading of classical logic
Table of Contents

Previous Page Next Page

Kleene 52: {A ∧(B ∨ ~B) ⇔ A}


∀[A,B: ℙ]. {A ∧ (B ∨ ¬B) ⇔ A}
{A ∧ (B ∨ ¬B) ⇒ A} ⇒ Extract: λf.spread(f; a,g.a)
A ∧ (B ∨ ¬B) ⇒ Aby λ(f.___)
aabonb : A ∧ (B ∨ ¬B) ⊢ Aby spread(f; a,g.___)
a : A, bonb : (B ∨ ¬B) ⊢ Aby 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 ⊢ Falseby ap(f.___)
a : A, b : B ⊢ A ∧ (B ∨ ¬B)by pair( slot3 ; slot4 )
a : A, b : B ⊢ Aby a for slot3
a : A, b : B ⊢ B ∨ ¬Bby inl(___) for slot4
a : A, b : B ⊢ Bby 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

Previous Page Next Page


Table of Contents