July 7, 2023
Version 0.2
| Name | Annotation | Rule | Rest On |
|---|---|---|---|
| Assumption | A | Assume any formula, π. | itself |
| Reiteration | Reit | From π, infer π. | whatever π rests on |
| Conjunction Introduction (Conjuction) | &I/Conj | From π and π, infer πβ&βπ. | whatever π and π rest on |
| Conjunction Elimination (Simplification) | &E/Simp | From πβ&βπ, infer either π or π. | whatever πβ&βπ rests on |
| Disjunction Introduction (Addition) | β¨I/Add | From π, infer either πββ¨βπ or πββ¨βπ. | whatever π rests on |
| Disjunction Elimination (Disjunctive Syllogism) | β¨E/DS | From πββ¨βπ and πβs denial, infer π. From πββ¨βπ and πβs denial, infer π.1 | whatever πββ¨βπ rests on |
| Conditional Introduction (Conditional Proof) | βI/CP | From π and an assumption π, infer πβββπ discharge π. | whatever π rests on, except the discharged assumption |
| Conditional Elimination (Modus ponens) | βE/MP | From π and πβββπ, infer π | whatever π rests on |
| Biconditional Introduction | βοΈI | From πβββπ and πβββπ, infer πββοΈβπ. | whatever πβββπ and πβββπ rest on |
| Biconditional Elimination | βοΈE | From πββοΈβπ, infer πβββπ or πβββπ. | whatever πββοΈβπ rests on |
| Negation Introduction | Β¬I | From π and Β¬π, discharge any assumption π and infer Β¬π. | whatever π and Β¬π rest on, except the discharged assumption |
| Negation Elimination | Β¬E | From ¬¬π, infer π. | whatever π rests on |
| Reductio ad absurdum (Indirect Proof)2 | RAA/IP | From π and Β¬π, discharge any assumption π and infer πβs denial. | whatever π and Β¬π rest on, except the discharged assumption |
For detailed explanations and examples, see Lemmon Proof System: Primitive Rules and Example Applications.
| Name | Annotation | Rule |
|---|---|---|
| Double Negation | DN | ¬¬π β£β’ π |
| Redundancy | Re | (πββ¨βπ) β£β’ π |
| Re | (πβ&βπ) β£β’ π | |
| Commutativity | Comm | (πβ&βπ) β£β’ (πβ&βπ) |
| Comm | (πββ¨βπ) β£β’ (πββ¨βπ) | |
| Comm | (πββοΈβπ) β£β’ (πββοΈβπ) | |
| Associativity | Assoc | (πβ&β(πβ&βπ)) β£β’ ((πβ&βπ)β&βπ) |
| Assoc | (πββ¨β(πββ¨βπ)) β£β’ ((πββ¨βπ)ββ¨βπ) | |
| Distribution | Dist | (πβ&β(πββ¨βπ)) β£β’ ((πβ&βπ)ββ¨β(πβ&βπ)) |
| Dist | (πββ¨β(πβ&βπ)) β£β’ ((πββ¨βπ)β&β(πββ¨βπ)) | |
| DeMorgan | DM | Β¬(πβ&βπ) β£β’ (Β¬πββ¨βΒ¬π) |
| DM | Β¬(πββ¨βπ) β£β’ (Β¬πβ&βΒ¬π) | |
| DM | (πββ¨βπ) β£β’ Β¬(Β¬πβ&βΒ¬π) | |
| DM | (πβ&βπ) β£β’ Β¬(Β¬πββ¨βΒ¬π) | |
| Def. of Conditional | βββdf | (Β¬πββ¨βπ) β£β’ (πβββπ) |
| βββdf | (πββ¨βπ) β£β’ (Β¬πβββπ) | |
| βββdf | (πββ¨βπ) β£β’ (Β¬πβββπ) | |
| βββdf | (πββ¨βΒ¬π) β£β’ (πβββπ) | |
| True Consequent | TC | π β’ (πβββπ) |
| False Antecedent | FA | Β¬π β’ (πβββπ) |
| Impossible Antecedent | IA | (πβββπ), (πβββΒ¬π) β’ Β¬π |
| Hypothetical Syllogism | HS | (πβββπ), (πβββπ) β’ (πβββπ) |
| Negated Conditional | Β¬βββ | Β¬(πβββπ) β£β’ (πβ&βΒ¬π) |
| Negated Biconditional | Β¬ββοΈβ | Β¬(πββοΈβπ) β£β’ ((πβ&βΒ¬π)ββ¨β(Β¬πβ&βπ)) |
| Conditional Contraposition | Con | (πβββπ) β£β’ (Β¬πβββΒ¬π) |
| Biconditional Contraposition | BiCon | (πββοΈβπ) β£β’ (Β¬πββοΈβΒ¬π) |
| Modus Tollens | MT | (πβββπ), Β¬π β’ Β¬π |
| MT | (Β¬πβββπ), Β¬π β’ π | |
| MT | (πβββΒ¬π), π β’ Β¬π | |
| MT | (Β¬πβββΒ¬π), π β’ π | |
| Biconditional Ponens | BP | (πββοΈβπ), π β’ π |
| BP | (πββοΈβπ), π β’ π | |
| Biconditional Tollens | BT | (πββοΈβπ), Β¬π β’ Β¬π |
| BT | (πββοΈβπ), Β¬π β’ Β¬π | |
| Import | Imp | (πβββ(πβββπ)) β’ ((πβ&βπ)βββπ) |
| Export | Exp | ((πβ&βπ)βββπ) β’ (πβββ(πβββπ)) |
| Special Dilemma | SpecD | (πβββπ), (Β¬πβββπ) β’ π |
| Simple Dilemma | SD | (πββ¨βπ), (πβββπ), (πβββπ) β’ π |
| Complex Dilemma | CD | (πββ¨βπ), (πβββπ), (πβββπ) β’ (πββ¨βπ) |
| Ex Falso Quodlibet | EFQ | π, Β¬π β’ π |
Β β― Β β―β―
A negated formula, Β¬π, has two denials, π and ¬¬π. All other formulas have only one denialβnamely, their negation. For example, the formula βΒ¬Pβ has two denials βPβ and ⬬Pβ but formula βQβ has one denial βΒ¬Q.ββ©οΈ
Reductio ad absurdum (RAA) (also called Indirect Proof (IP)) is similar to Negation introduction (Β¬I). In fact, some books equate Β¬I with RAA. The difference is subtle. RAA and IP allow you assume Β¬π to infer π; Β¬I does not. Negation introduction always introduces βΒ¬β and never eliminates it.β©οΈ