Constructive Reading of Classical Logic
Robert L. Constable and Sarah Sernaker 2015Table of Contents
- Introduction
- Theorems
- Propositional calculus
- Pierce's Law -- {((A ⇒ B) ⇒ A) ⇒ A}
- Kleene 14 -- {(~A ⇒ B) ⇒ ~B ⇒ A}
- Kleene 15 -- {(~A ⇒ ~B) ⇒ B ⇒ A}
- Kleene 49-- {~~A ⇔ A}
- Kleene 52 -- {A ∧(B ∨ ~B) ⇔ A}
- Kleene 55 -- {(A ∨ B ∨ ~B) ⇔ (B ∨ ~B)}
- Kleene 56 -- {(A ∨ B) ⇔ ~(~A ∧ ~B)}
- Kleene 57 -- {(A ∧ B) ⇔ ~(~A ∨ ~B)}
- Kleene 58 -- {(A ⇒ B) ⇔ (~A ∧ ~B)}
- Kleene 59 -- {(A ⇒ B) ⇔ (~A ∨ B)}
- Kleene 60 -- {(A ∧ B) ⇔ ~(A ⇒ ~B)}
- Kleene 61 -- {(A ∨ B) ⇔ (~A ⇒ B)}
- Kleene 62 -- {~(A ∧ B) ⇔ (~A ∨ ~B)}
- First order logic
- Kleene 83 -- {∃x:T.(A x) ⇔ ~(∀x:T.~(A x))}
- Kleene 84 -- {∀x:T.(A x) ⇔ ~(∃x.T:~(A x))}
- Kleene 85 -- {~(∀x:T.(A x)) ⇔ (∃x:T.~(A x))}
- Kleene 92 -- {(A ∨ ∀x:T.(B x)) ⇔ ∀x:T. (A ∨ (B x))}
- Kleene 97 -- {∃x:T.(A ⇒ (B x)) ⇔ (A ⇒ (∃x:T.(B x)))}
- Kleene 98 -- {∃x.T:((A x) ⇒ B) ⇔ ∀x:T.{A x} ⇒ B}
- Kleene 99 -- {∃x:T.((A x) ⇒ (B x)) ⇔ ∀x.T:{A x} ⇒ ∃x:T.(B x)}
- References