List of rules of inference

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

${\displaystyle \varphi \vdash \psi }$

indicates such a subderivation from the temporary assumption ${\displaystyle \varphi }$ to ${\displaystyle \psi }$.

Reductio ad absurdum (or Negation Introduction)

${\displaystyle \varphi \vdash \psi }$

${\displaystyle {\underline {\varphi \vdash \lnot \psi }}}$

${\displaystyle \lnot \varphi }$

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

${\displaystyle \lnot \varphi \vdash \psi }$

${\displaystyle {\underline {\lnot \varphi \vdash \lnot \psi }}}$

${\displaystyle \varphi }$

Ex contradictione quodlibet

${\displaystyle \varphi }$

${\displaystyle {\underline {\lnot \varphi }}}$

${\displaystyle \psi }$

Deduction theorem (or Conditional Introduction)

${\displaystyle {\underline {\varphi \vdash \psi }}}$

${\displaystyle \varphi \rightarrow \psi }$

Modus ponens (a type of Conditional Elimination)

${\displaystyle \varphi \rightarrow \psi }$

${\displaystyle {\underline {\varphi \quad \quad \quad }}}$

${\displaystyle \psi }$

Modus tollens (a type of Conditional Elimination)

${\displaystyle \varphi \rightarrow \psi }$

${\displaystyle {\underline {\lnot \psi \quad \quad \quad }}}$

${\displaystyle \lnot \varphi }$

Adjunction (or Conjunction Introduction)

${\displaystyle \varphi }$

${\displaystyle {\underline {\psi \quad \quad \ \ }}}$

${\displaystyle \varphi \land \psi }$

Simplification (or Conjunction Elimination)

${\displaystyle {\underline {\varphi \land \psi }}}$

${\displaystyle \varphi }$

${\displaystyle {\underline {\varphi \land \psi }}}$

${\displaystyle \psi }$

Addition (or Disjunction Introduction)

${\displaystyle {\underline {\varphi \quad \quad \ \ }}}$

${\displaystyle \varphi \lor \psi }$

${\displaystyle {\underline {\psi \quad \quad \ \ }}}$

${\displaystyle \varphi \lor \psi }$

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

${\displaystyle \varphi \rightarrow \chi }$

${\displaystyle \psi \rightarrow \chi }$

${\displaystyle {\underline {\varphi \lor \psi }}}$

${\displaystyle \chi }$

Disjunctive syllogism

${\displaystyle \varphi \lor \psi }$

${\displaystyle {\underline {\lnot \varphi \quad \quad }}}$

${\displaystyle \psi }$

${\displaystyle \varphi \lor \psi }$

${\displaystyle {\underline {\lnot \psi \quad \quad }}}$

${\displaystyle \varphi }$

Constructive dilemma

${\displaystyle \varphi \rightarrow \chi }$

${\displaystyle \psi \rightarrow \xi }$

${\displaystyle {\underline {\varphi \lor \psi }}}$

${\displaystyle \chi \lor \xi }$

Biconditional introduction

${\displaystyle \varphi \rightarrow \psi }$

${\displaystyle {\underline {\psi \rightarrow \varphi }}}$

${\displaystyle \varphi \leftrightarrow \psi }$

Biconditional elimination

${\displaystyle \varphi \leftrightarrow \psi }$

${\displaystyle {\underline {\varphi \quad \quad }}}$

${\displaystyle \psi }$

${\displaystyle \varphi \leftrightarrow \psi }$

${\displaystyle {\underline {\psi \quad \quad }}}$

${\displaystyle \varphi }$

${\displaystyle \varphi \leftrightarrow \psi }$

${\displaystyle {\underline {\lnot \varphi \quad \quad }}}$

${\displaystyle \lnot \psi }$

${\displaystyle \varphi \leftrightarrow \psi }$

${\displaystyle {\underline {\lnot \psi \quad \quad }}}$

${\displaystyle \lnot \varphi }$

${\displaystyle \varphi \leftrightarrow \psi }$

${\displaystyle {\underline {\psi \lor \varphi }}}$

${\displaystyle \psi \land \varphi }$

${\displaystyle \varphi \leftrightarrow \psi }$

${\displaystyle {\underline {\lnot \psi \lor \lnot \varphi }}}$

${\displaystyle \lnot \psi \land \lnot \varphi }$

Summarize Timeline Fact Check

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

Universal Generalization (or Universal Introduction)

${\displaystyle {\underline {\varphi {(\beta /\alpha )}}}}$

${\displaystyle \forall \alpha \,\varphi }$

Restriction 1: ${\displaystyle \beta }$ is a variable which does not occur in ${\displaystyle \varphi }$.
Restriction 2: ${\displaystyle \beta }$ is not mentioned in any hypothesis or undischarged assumptions.

Universal Instantiation (or Universal Elimination)

${\displaystyle \forall \alpha \,\varphi }$

${\displaystyle {\overline {\varphi {(\beta /\alpha )}}}}$

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

Existential Generalization (or Existential Introduction)

${\displaystyle {\underline {\varphi (\beta /\alpha )}}}$

${\displaystyle \exists \alpha \,\varphi }$

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

Existential Instantiation (or Existential Elimination)

${\displaystyle \exists \alpha \,\varphi }$

${\displaystyle {\underline {\varphi (\beta /\alpha )\vdash \psi }}}$

${\displaystyle \psi }$

Restriction 1: ${\displaystyle \beta }$ is a variable which does not occur in ${\displaystyle \varphi }$.
Restriction 2: There is no occurrence, free or bound, of ${\displaystyle \beta }$ in ${\displaystyle \psi }$.
Restriction 3: ${\displaystyle \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)

${\displaystyle \alpha \vdash \beta }$

${\displaystyle {\overline {\alpha ,\alpha \vdash \beta }}}$

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

${\displaystyle {\underline {\alpha ,\alpha ,\gamma \vdash \beta }}}$

${\displaystyle \alpha ,\gamma \vdash \beta }$