{{header | title = From intuitionistic to classical | subtitle = propositional logic | left = | right = | shortcut = | notes = Adding the Interface:Law of the excluded middle to Interface:Basic intuitionistic propositional logic gives classical propositional logic. }} {{interfaces | imports = Interface:Basic intuitionistic propositional logic<br /> Interface:Law of the excluded middle | exports = Interface:Principia Mathematica propositional logic theorems }}
Instead of proving the axioms of classical propositional logic (for example, Interface:Standard axioms of propositional logic), we prove the Interface:Principia Mathematica propositional logic theorems. This is for two reasons. The first is to show that all the connectives, not just those mentioned in the axioms, have the same meanings (this could alternately be achieved by including all the definitions in the interface with the axioms, as in Interface:Principia Mathematica propositional logic). The second is to present an alternative proof of the Interface:Principia Mathematica propositional logic theorems. In some cases the way we prove the theorems is very similar, but in others it is quite different. The proofs in Principia Mathematica propositional logic rely heavily on the relationships between the connectives (especially implication and disjunction), and the proofs via intuitionistic logic rely more heavily on theorems such as disjunction composition and conjunction composition.
We define some variables:
To prove this biconditional transposition law, we write the biconditional on the left and right side as a pair of implications, and then apply transposition to each of them.
The following version is similar, but with the negation placed differently. The proof is similar, but is based on different variants of transposition for implications.
It will also be convenient to have a commuted version of this theorem.
One of DeMorgan's laws holds (in both directions) intuitionistically.
Double negation elimination turns that one into the other three which distribute negation across disjunction.
The versions which distribute negation across a conjunction follow from the above versions and transposition.
We supply those rules which do not hold intuitionistically.
The intention of this theorem is similar to the intuitionistic TautologyId, but it is stated in terms of the law of the excluded middle.
Intuitionistic logic does have one equivalence relating disjunction to implication, ¬ (p ∨ q) ↔ ¬ (¬ p → q). That and transposition gets us one of the classical equivalences,
Although the treatment of propositional logic in Whitehead and Russell's ''Principia'' relies heavily on this relationship between implication and disjunction, we rely on it only for a handful of theorems.
This theorem, (p ↔ q) ↔ (p ∧ q) ∨ (¬ p ∧ ¬ q), can be thought of saying that the biconditional is true if and only if both formulas are true or neither is true. We prove it from BiconditionalConjunction by applying the distributive law several times.
The first lemma is ¬ p ∨ q ↔ (p ∨ ¬ p) ∧ (q ∨ ¬ p), which consists of the notion that we can add or remove a conjunct which is a theorem (p ∨ ¬ p), and a commutation.
Because of the classical relationship between disjunction and implication, case elimination follows readily from disjunctive case elimination.