List of rules of inference
This is a list of rules of inference, logical laws that relate to mathematical formulae.
Introduction
Rules of inference are syntactical transform rules which one can use to infer a conclusion from a premise to create an argument. A set of rules can be used to infer any valid conclusion if it is complete, while never inferring an invalid conclusion, if it is sound. A sound and complete set of rules need not include every rule in the following list, as many of the rules are redundant, and can be proven with the other rules.Discharge rules permit inference from a subderivation based on a temporary assumption. Below, the notation
indicates such a subderivation from the temporary assumption to.
Rules for classical sentential calculus
Sentential calculus is also known as propositional calculus.Rules for negations
;Reductio ad absurdum :;Reductio ad absurdum :
;Noncontradiction :
;Double negation elimination:
;Double negation introduction:
Rules for conditionals
;Deduction theorem :;Modus ponens :
;Modus tollens:
Rules for conjunctions
;Adjunction :;Simplification :
Rules for disjunctions
;Addition :;Case analysis
;Disjunctive syllogism:
;Constructive dilemma
Rules for biconditionals
;Biconditional introduction:;Biconditional elimination:
Rules of classical predicate calculus">First-order logic">predicate calculus
In the following rules, is exactly like except for having the term wherever has the free variable.;Universal Generalization :
Restriction 1: is a variable which does not occur in.
Restriction 2: is not mentioned in any hypothesis or undischarged assumptions.
;Universal Instantiation :
Restriction: No free occurrence of in falls within the scope of a quantifier quantifying a variable occurring in.
;Existential Generalization :
Restriction: No free occurrence of in falls within the scope of a quantifier quantifying a variable occurring in.
;Existential Instantiation :
Restriction 1: is a variable which does not occur in.
Restriction 2: There is no occurrence, free or bound, of in.
Restriction 3: is not mentioned in any hypothesis or undischarged assumptions.
Rules of [substructural logic]
The following are special cases of universal generalization and existential elimination; these occur in substructural logics, such as linear logic.;Rule of weakening
;Rule of contraction
Table: Rules of Inference
The rules above can be summed up in the following table. The "Tautology" column shows how to interpret the notation of a given rule.| Rules of inference | Tautology | Name |
| Modus ponens | ||
| Modus tollens | ||
| Associative | ||
| Commutative | ||
| Law of biconditional propositions | ||
| Exportation | ||
| Transposition or contraposition law | ||
| Hypothetical syllogism | ||
| Material implication | ||
| Distributive | ||
| Absorption | ||
| Disjunctive syllogism | ||
| Addition | ||
| Simplification | ||
| Conjunction | ||
| Double negation | ||
| Disjunctive simplification | ||
| Resolution | ||
| Disjunction Elimination |
All rules use the basic logic operators. A complete table of "logic operators" is shown by a truth table, giving definitions of all the possible truth functions of 2 boolean variables :
| p | q | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 | 13 | 14 | 15 | ||
| T | T | F | F | F | F | F | F | F | F | T | T | T | T | T | T | T | T | ||
| T | F | F | F | F | F | T | T | T | T | F | F | F | F | T | T | T | T | ||
| F | T | F | F | T | T | F | F | T | T | F | F | T | T | F | F | T | T | ||
| F | F | F | T | F | T | F | T | F | T | F | T | F | T | F | T | F | T |
where T = true and F = false, and, the columns are the logical operators: 0, false, Contradiction; 1, NOR, Logical NOR ; 2, Converse nonimplication; 3, ¬p, Negation; 4, Material nonimplication; 5, ¬q, Negation; 6, XOR, Exclusive disjunction; 7, NAND, Logical NAND ; 8, AND, Logical conjunction; 9, XNOR, If and only if, Logical biconditional; 10, q, Projection function; 11, if/then, Logical implication; 12, p, Projection function; 13, then/if, Converse implication; 14, OR, Logical disjunction; 15, true, Tautology.
Each logic operator can be used in an assertion about variables and operations, showing a basic rule of inference. Examples:
- The column-14 operator, shows Addition rule: when p=T, we see that p∨q=T.
- : We can see also that, with the same premise, another conclusions are valid: columns 12, 14 and 15 are T.
- The column-8 operator, shows Simplification rule: when p∧q=T, we see that p=T.
- : With this premise, we also conclude that q=T, p∨q=T, etc. as showed by columns 9-15.
- The column-11 operator, shows Modus ponens rule: when p→q=T and p=T only one line of the truth table satisfies these two conditions. On this line, q is also true. Therefore, whenever p → q is true and p is true, q must also be true.
Example 1
Consider the following assumptions: "If it rains today, then we will not go on a canoe today. If we do not go on a canoe trip today, then we will go on a canoe trip tomorrow. Therefore, if it rains today, we will go on a canoe trip tomorrow".To make use of the rules of inference in the above table we let be the proposition "If it rains today", be "We will not go on a canoe today" and let be "We will go on a canoe trip tomorrow". Then this argument is of the form:
Example 2
Consider a more complex set of assumptions: "It is not sunny today and it is colder than yesterday". "We will go swimming only if it is sunny", "If we do not go swimming, then we will have a barbecue", and "If we will have a barbecue, then we will be home by sunset" lead to the conclusion "We will be home by sunset."Proof by rules of inference: Let be the proposition "It is sunny today", the proposition "It is colder than yesterday", the proposition "We will go swimming", the proposition "We will have a barbecue", and the proposition "We will be home by sunset". Then the hypotheses become and. Using our intuition we conjecture that the conclusion might be. Using the Rules of Inference table we can prove the conjecture easily:
| Step | Reason |
| 1. | Hypothesis |
| 2. | Simplification using Step 1 |
| 3. | Hypothesis |
| 4. | Modus tollens using Step 2 and 3 |
| 5. | Hypothesis |
| 6. | Modus ponens using Step 4 and 5 |
| 7. | Hypothesis |
| 8. | Modus ponens using Step 6 and 7 |