List of rules of inference#Rules of classical predicate calculus

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

: $\backslash varphi\; \backslash vdash\; \backslash psi$

indicates such a subderivation from the temporary assumption $\backslash varphi$ to $\backslash psi$.

;Reductio ad absurdum (or Negation Introduction):

: $\backslash varphi\; \backslash vdash\; \backslash psi$

: $\backslash underline\{\backslash varphi\; \backslash vdash\; \backslash lnot\; \backslash psi\}$

: $\backslash lnot\; \backslash varphi$

;Reductio ad absurdum (related to the law of excluded middle):

: $\backslash lnot\; \backslash varphi\; \backslash vdash\; \backslash psi$

: $\backslash underline\{\backslash lnot\; \backslash varphi\; \backslash vdash\; \backslash lnot\; \backslash psi\}$

: $\backslash varphi$

;Ex contradictione quodlibet:

: $\backslash varphi$

: $\backslash underline\{\backslash lnot\; \backslash varphi\}$

: $\backslash psi$

;Deduction theorem (or Conditional Introduction):

: $\backslash underline\{\backslash varphi\; \backslash vdash\; \backslash psi\}$

: $\backslash varphi\; \backslash rightarrow\; \backslash psi$

;Modus ponens (a type of Conditional Elimination):

: $\backslash varphi\; \backslash rightarrow\; \backslash psi$

: $\backslash underline\{\backslash varphi\; \backslash quad\; \backslash quad\; \backslash quad\}$

: $\backslash psi$

;Modus tollens (a type of Conditional Elimination):

: $\backslash varphi\; \backslash rightarrow\; \backslash psi$

: $\backslash underline\{\backslash lnot\; \backslash psi\; \backslash quad\; \backslash quad\; \backslash quad\}$

: $\backslash lnot\; \backslash varphi$

;Adjunction (or Conjunction Introduction):

: $\backslash varphi$

: $\backslash underline\{\backslash psi\; \backslash quad\; \backslash quad\; \backslash \; \backslash \; \}$

: $\backslash varphi\; \backslash land\; \backslash psi$

;Simplification (or Conjunction Elimination):

: $\backslash underline\{\backslash varphi\; \backslash land\; \backslash psi\}$

: $\backslash varphi$

: $\backslash underline\{\backslash varphi\; \backslash land\; \backslash psi\}$

: $\backslash psi$

;Addition (or Disjunction Introduction):

: $\backslash underline\{\backslash varphi\; \backslash quad\; \backslash quad\; \backslash \; \backslash \; \}$

: $\backslash varphi\; \backslash lor\; \backslash psi$

: $\backslash underline\{\backslash psi\; \backslash quad\; \backslash quad\; \backslash \; \backslash \; \}$

: $\backslash varphi\; \backslash lor\; \backslash psi$

;Case analysis (or Proof by Cases or Argument by Cases or Disjunction elimination)

: $\backslash varphi\; \backslash rightarrow\; \backslash chi$

: $\backslash psi\; \backslash rightarrow\; \backslash chi$

: $\backslash underline\{\backslash varphi\; \backslash lor\; \backslash psi\}$

: $\backslash chi$

;Disjunctive syllogism:

: $\backslash varphi\; \backslash lor\; \backslash psi$

: $\backslash underline\{\backslash lnot\; \backslash varphi\; \backslash quad\; \backslash quad\}$

: $\backslash psi$

: $\backslash varphi\; \backslash lor\; \backslash psi$

: $\backslash underline\{\backslash lnot\; \backslash psi\; \backslash quad\; \backslash quad\}$

: $\backslash varphi$

;Constructive dilemma

: $\backslash varphi\; \backslash rightarrow\; \backslash chi$

: $\backslash psi\; \backslash rightarrow\; \backslash xi$

: $\backslash underline\{\backslash varphi\; \backslash lor\; \backslash psi\}$

: $\backslash chi\; \backslash lor\; \backslash xi$

;Biconditional introduction:

: $\backslash varphi\; \backslash rightarrow\; \backslash psi$

: $\backslash underline\{\backslash psi\; \backslash rightarrow\; \backslash varphi\}$

: $\backslash varphi\; \backslash leftrightarrow\; \backslash psi$

;Biconditional elimination:

: $\backslash varphi\; \backslash leftrightarrow\; \backslash psi$

: $\backslash underline\{\backslash varphi\; \backslash quad\; \backslash quad\}$

: $\backslash psi$

: $\backslash varphi\; \backslash leftrightarrow\; \backslash psi$

: $\backslash underline\{\backslash psi\; \backslash quad\; \backslash quad\}$

: $\backslash varphi$

: $\backslash varphi\; \backslash leftrightarrow\; \backslash psi$

: $\backslash underline\{\backslash lnot\; \backslash varphi\; \backslash quad\; \backslash quad\}$

: $\backslash lnot\; \backslash psi$

: $\backslash varphi\; \backslash leftrightarrow\; \backslash psi$

: $\backslash underline\{\backslash lnot\; \backslash psi\; \backslash quad\; \backslash quad\}$

: $\backslash lnot\; \backslash varphi$

: $\backslash varphi\; \backslash leftrightarrow\; \backslash psi$

: $\backslash underline\{\backslash psi\; \backslash lor\; \backslash varphi\}$

: $\backslash psi\; \backslash land\; \backslash varphi$

: $\backslash varphi\; \backslash leftrightarrow\; \backslash psi$

: $\backslash underline\{\backslash lnot\; \backslash psi\; \backslash lor\; \backslash lnot\; \backslash varphi\}$

: $\backslash lnot\; \backslash psi\; \backslash land\; \backslash lnot\; \backslash varphi$

In the following rules, $\backslash varphi(\backslash beta\; /\; \backslash alpha)$ is exactly like $\backslash varphi$ except for having the term $\backslash beta$ wherever $\backslash varphi$ has the free variable $\backslash alpha$.

;Universal Generalization (or Universal Introduction):

: $\backslash underline\{\backslash varphi\{(\backslash beta\; /\; \backslash alpha)\}\}$

: $\backslash forall\; \backslash alpha\backslash ,\; \backslash varphi$

Restriction 1: $\backslash beta$ is a variable which does not occur in $\backslash varphi$.

Restriction 2: $\backslash beta$ is not mentioned in any hypothesis or undischarged assumptions.

;Universal Instantiation (or Universal Elimination):

: $\backslash forall\; \backslash alpha\backslash ,\; \backslash varphi$

: $\backslash overline\{\backslash varphi\{(\backslash beta\; /\; \backslash alpha)\}\}$

Restriction: No free occurrence of $\backslash alpha$ in $\backslash varphi$ falls within the scope of a quantifier quantifying a variable occurring in $\backslash beta$.

;Existential Generalization (or Existential Introduction):

: $\backslash underline\{\backslash varphi(\backslash beta\; /\; \backslash alpha)\}$

: $\backslash exists\; \backslash alpha\backslash ,\; \backslash varphi$

Restriction: No free occurrence of $\backslash alpha$ in $\backslash varphi$ falls within the scope of a quantifier quantifying a variable occurring in $\backslash beta$.

;Existential Instantiation (or Existential Elimination):

: $\backslash exists\; \backslash alpha\backslash ,\; \backslash varphi$

: $\backslash underline\{\backslash varphi(\backslash beta\; /\; \backslash alpha)\; \backslash vdash\; \backslash psi\}$

: $\backslash psi$

Restriction 1: $\backslash beta$ is a variable which does not occur in $\backslash varphi$.

Restriction 2: There is no occurrence, free or bound, of $\backslash beta$ in $\backslash psi$.

Restriction 3: $\backslash beta$ is not mentioned in any hypothesis or undischarged assumptions.

The following are special cases of universal generalization and existential elimination; these occur in substructural logics, such as linear logic.

;Rule of weakening (or monotonicity of entailment) (aka no-cloning theorem)

: $\backslash alpha\backslash vdash\backslash beta$

: $\backslash overline\{\backslash alpha,\backslash alpha\backslash vdash\backslash beta\}$

;Rule of contraction (or idempotency of entailment) (aka no-deleting theorem)

: $\backslash underline\{\backslash alpha,\backslash alpha,\backslash gamma\backslash vdash\backslash beta\}$

: $\backslash alpha,\backslash gamma\backslash vdash\backslash beta$

The rules above can be summed up in the following table.Kenneth H. Rosen: Discrete Mathematics and its Applications, Fifth Edition, p. 58. The "Tautology" column shows how to interpret the notation of a given rule.

class="wikitable"
Rules of inference ! Tautology ! Name
$\backslash begin\{align\}$ p\\ p \rightarrow q\\ \therefore \overline{q \quad \quad \quad} \\ \end{align} | $(p\; \backslash wedge\; (p\; \backslash rightarrow\; q))\; \backslash rightarrow\; q$ | Modus ponens
$\backslash begin\{align\}$ \neg q\\ p \rightarrow q\\ \therefore \overline{\neg p \quad \quad \quad} \\ \end{align} | $(\backslash neg\; q\; \backslash wedge\; (p\; \backslash rightarrow\; q))\; \backslash rightarrow\; \backslash neg\; p$ | Modus tollens
$\backslash begin\{align\}$ p \rightarrow q\\ q \rightarrow r\\ \therefore \overline{p \rightarrow r} \\ \end{align} | $((p\; \backslash rightarrow\; q)\; \backslash wedge\; (q\; \backslash rightarrow\; r))\; \backslash rightarrow\; (p\; \backslash rightarrow\; r)$ | Hypothetical syllogism
$\backslash begin\{align\}$ p \rightarrow q\\ \therefore \overline{p \rightarrow (p \wedge q)} \\ \end{align} | $(p\; \backslash rightarrow\; q)\; \backslash rightarrow\; (p\; \backslash rightarrow\; (p\; \backslash wedge\; q))$ | Absorption
$\backslash begin\{align\}$ p\\ q\\ \therefore \overline{p \wedge q} \\ \end{align} | $((p)\; \backslash wedge\; (q))\; \backslash rightarrow\; (p\; \backslash wedge\; q)$ | Conjunction introduction
$\backslash begin\{align\}$ p \wedge q \\ \therefore \overline{p \quad \quad \quad} \\ \end{align} | $(p\; \backslash wedge\; q)\; \backslash rightarrow\; p$ | Conjunction elimination
$\backslash begin\{align\}$ p \\ \therefore \overline{p \vee q} \\ \end{align} | $p\; \backslash rightarrow\; (p\; \backslash vee\; q)$ | Disjunction introduction
$\backslash begin\{align\}$ p \rightarrow q\\ r \rightarrow q\\ p \vee r\\ \therefore \overline{q \quad \quad \quad} \\ \end{align} | $((p\; \backslash rightarrow\; q)\; \backslash wedge\; (r\; \backslash rightarrow\; q)\; \backslash wedge\; (p\; \backslash vee\; r))\; \backslash rightarrow\; q$ | Disjunction elimination
$\backslash begin\{align\}$ p \vee q \\ \neg p \\ \therefore \overline{q \quad \quad \quad} \\ \end{align} | $((p\; \backslash vee\; q)\; \backslash wedge\; \backslash neg\; p)\; \backslash rightarrow\; q$ | Disjunctive syllogism
$\backslash begin\{align\}$ p \vee p \\ \therefore \overline{p \quad \quad \quad} \\ \end{align} | $(p\; \backslash vee\; p)\; \backslash rightarrow\; p$ | Disjunctive simplification
$\backslash begin\{align\}$ p \vee q \\ \neg p \vee r \\ \therefore \overline{q \vee r} \\ \end{align} | $((p\; \backslash vee\; q)\; \backslash wedge\; (\backslash neg\; p\; \backslash vee\; r))\; \backslash rightarrow\; (q\; \backslash vee\; r)$ | Resolution
$\backslash begin\{align\}$ p \rightarrow q\\ q \rightarrow p\\ \therefore \overline{p \leftrightarrow q} \\ \end{align} | $((p\; \backslash rightarrow\; q)\; \backslash wedge\; (q\; \backslash rightarrow\; p))\; \backslash rightarrow\; (p\; \backslash leftrightarrow\; q)$ | Biconditional introduction
$?$ |$?$ |{{See|List of rules of inference#Rules for propositional calculus}}
$?$ |$?$ |{{See|List of rules of inference#Rules for negations}}
$?$ |$?$ |{{See|List of rules of inference#Rules for conditionals}}
$?$ |$?$ |{{See|List of rules of inference#Rules for conjunctions}}
$?$ |$?$ |{{See|List of rules of inference#Rules for disjunctions}}
$?$ |$?$ |{{See|List of rules of inference#Rules for biconditionals}}
$?$ |$?$ |{{See|List of rules of inference#Rules of classical predicate calculus}}
$?$ |$?$ |{{See|List of rules of inference#Rules of substructural logic}}

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 (16) truth functions of 2 boolean variables (p, q):

class="wikitable" style="margin:1em auto 1em auto; text-align:center;"
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 (Peirce's arrow);
• 2, Converse nonimplication;
• 3, ¬p, Negation;
• 4, Material nonimplication;
• 5, ¬q, Negation;
• 6, XOR, Exclusive disjunction;
• 7, NAND, Logical NAND (Sheffer stroke);
• 8, AND, Logical conjunction;
• 9, XNOR, If and only if, Logical biconditional;
• 10, q, Projection function;
• 11, if/then, Material conditional;
• 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 (OR), shows Addition rule: when p=T (the hypothesis selects the first two lines of the table), we see (at column-14) 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 (AND), shows Simplification rule: when p∧q=T (first line of the table), we see that p=T.
• : With this premise, we also conclude that q=T, p∨q=T, etc. as shown by columns 9–15.
• The column-11 operator (IF/THEN), shows Modus ponens rule: when p→q=T and p=T only one line of the truth table (the first) 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.

Machines and well-trained people use this look at table approach to do basic inferences, and to check if other inferences (for the same premises) can be obtained.{{Citation needed|date=September 2024}}

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 (Mathematical symbol for "therefore" is $\backslash 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 $p$ be the proposition "If it rains today", $q$ be "We will not go on a canoe today" and let $r$ be "We will go on a canoe trip tomorrow". Then this argument is of the form:

$\backslash begin\{align\}$

p \rightarrow q\\

q \rightarrow r\\

\therefore \overline{p \rightarrow r} \\

\end{align}

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 $p$ be the proposition "It is sunny today", $q$ the proposition "It is colder than yesterday", $r$ the proposition "We will go swimming", $s$ the proposition "We will have a barbecue", and $t$ the proposition "We will be home by sunset". Then the hypotheses become $\backslash neg\; p\; \backslash wedge\; q,\; r\; \backslash rightarrow\; p,\; \backslash neg\; r\; \backslash rightarrow\; s$ and $s\; \backslash rightarrow\; t$. Using our intuition we conjecture that the conclusion might be $t$. Using the Rules of Inference table we can prove the conjecture easily:

class="wikitable"
Step ! Reason
1.$\backslash neg\; p\; \backslash wedge\; q$ | Hypothesis
2. $\backslash neg\; p$ | Simplification using Step 1
3. $r\; \backslash rightarrow\; p$ | Hypothesis
4. $\backslash neg\; r$ | Modus tollens using Step 2 and 3
5. $\backslash neg\; r\; \backslash rightarrow\; s$ | Hypothesis
6. $s$ | Modus ponens using Step 4 and 5
7. $s\; \backslash rightarrow\; t$ | Hypothesis
8. $t$ | Modus ponens using Step 6 and 7

{{Portal|Philosophy}}

• List of logic systems
• Modus ponendo tollens

{{Logic}}

{{DEFAULTSORT:Rules Of Inference}}

*

Category:Mathematics-related lists

Category:Logic-related lists

de:Schlussregel

he:חוקי היקש