## 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) ⇒ 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