## Kleene 59: {(A ⇒ B) ⇔ (~A ∨ B)}

The extract of the backwards direction shows the constructive part of the proof. It can be done without classical reasoning. We see that in choosing ¬A of the or disjunction with evidence na we can create evidence for A ⇒ B because when we build the function that assumes A in order to prove B, we have the context λx. __ where x is of type A. Therefore na(x) will be in the type False, and we can use any(na(x)) as evidence for B. Thus λx.any(na(x)) is evidence for A ⇒ B under the assumption na in the decide operator.

The forward direction, (A ⇒ B) ⇒(¬A ∨ B) can not be proved constructively -- although we do not give that argument here, it is not difficult to show this. Therefore we need a use classical contradiction. This will provide evidence needed to prove the goal. We choose inl then do a construction rule. We then apply our newly generated evidence, and do inr to yield B as our goal. We can get B by applying the function A ⇒ B to A, which we have evidence for.
∀[A,B: ℙ]. {(A ⇒ B) ⇔ (¬A ∨ B)}
{(A ⇒ B) ⇒ (¬A ∨ B)} ⇐ Extract: λnaob.λa.decide(naob; na.any(ap(na.a)); b.b)
 ¬A ∨ B ⇒ A ⇒ B by λ(f.___) f : ¬A ∨ B ⊢ A ⇒ B by λ(a.___) f : ¬A ∨ B, a : A ⊢ B by decide(f; na. slot1 ;b. slot2 ) na : ¬A, a : A ⊢ B by apseq(na;a;False.any(..)) for slot1 b : B, A ⊢ B by b for slot2
{(¬A ∨ B) ⇒ (A ⇒ B)} ⇒ Extract: λf.(CC;g.inl(λa.ap(g.inr(ap(f.a)))))
 {(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 inl(___) f : A ⇒ B, g : ¬(¬A ∨ B) ⊢ {¬A} by λ(a.___) f : A ⇒ B, g : ¬(¬A ∨ B), a : A ⊢ False by ap(g.___) f : A ⇒ B, a : A ⊢ ¬A ∨ B by inr(___) f : A ⇒ B, a : A ⊢ B by ap(f.a)

### Nuprl Proof

⊢ ∀[A,B:ℙ]. {(A ⇒ B) ⇔ (¬A ∨ B)} | BY (D 0 THENA Auto) |\ | 1. A: ℙ | ⊢ ∀[B:P]. {(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 (ClassicalContradiction THENA Auto) Add contradiction of goal to hypotheses | | | | | | | 4. ¬((¬A) ∨ B) | | | ⊢ {(¬A) ∨ B} | | | | 1 2 3 BY (ElimClassical THENA Auto) Unsquash goal | | | | | | | ⊢ (¬A) ∨ B | | | | 1 2 3 BY (OrLeft THENA Auto) | | | | | | | ⊢ ¬A | | | | 1 2 3 BY (D 0 THENA Auto) | | | | | | | 5. A | | | ⊢ False | | | | 1 2 3 BY D 4 | | | | | | | 4. A | | | ⊢ (¬A) ∨ B | | | | 1 2 3 BY (OrRight THENA Auto) | | | | | | | ⊢ B | | | | 1 2 3 BY D 3 | | | |\ | | | | 3. A | | | | ⊢ A | | | | | 1 2 3 4 BY Hypothesis | | | \ | | | 3. A | | | 4. B | | | ⊢ B | | | | 1 2 3 BY Hypothesis | | \ | | 3. (¬A) ∨ B | | ⊢ {A ⇒ B} | | | 1 2 BY (RepeatFor 2 (D 0) THENA Auto) | | | | | 4. A | | ⊢ {B} | | | 1 2 BY ElimClassical Unsquash goal | | | | | ⊢ B | | | 1 2 BY D 3 | | |\ | | | 3. ¬A | | | ⊢ B | | | | 1 2 3 BY D 3 | | | | | | | 3. A | | | ⊢ A | | | | 1 2 3 BY Hypothesis | | \ | | 3. B | | ⊢ 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