List of rules of inference
From Free net encyclopedia
This is a list of rules of inference.
Contents |
Introduction
Rules of inference are syntactical transformation 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
- <math>\varphi \vdash \psi\,\!</math>
indicates such a subderivation from the temporary assumption <math>\varphi\,\!</math> to <math>\psi\,\!</math>.
Rules for classical sentential calculus
Rules for negations
- Reductio ad absurdum (or Negation Introduction)
- <math>\varphi \vdash \psi\,\!</math>
- <math>\underline{\varphi \vdash \lnot \psi}\,\!</math>
- <math>\lnot \varphi\,\!</math>
- Reductio ad absurdum (or Negation Elimination)
- <math>\lnot \varphi \vdash \psi\,\!</math>
- <math>\underline{\lnot \varphi \vdash \lnot \psi}\,\!</math>
- <math>\varphi\,\!</math>
- Double negation elimination
- <math>\underline{\lnot \lnot \varphi}\,\!</math>
- <math> \varphi\,\!</math>
- Double negation introduction
- <math>\underline{\varphi \quad \quad}\,\!</math>
- <math> \lnot \lnot \varphi\,\!</math>
Rules for conditionals
- Conditional Introduction
- <math>\underline{\varphi \vdash \psi}\,\!</math>
- <math>\varphi \rightarrow \psi\,\!</math>
- Modus ponens (or Conditional Elimination)
- <math>\varphi \rightarrow \psi\,\!</math>
- <math>\underline{\varphi \quad \quad \quad}\,\!</math>
- <math>\psi\,\!</math>
- Modus tollens
- <math>\varphi \rightarrow \psi\,\!</math>
- <math>\underline{\lnot \psi \quad \quad \quad}\,\!</math>
- <math>\lnot \varphi\,\!</math>
Rules for conjunctions
- Adjunction (or Conjunction Introduction)
- <math>\varphi\,\!</math>
- <math>\underline{\psi \quad \quad \ \ }\,\!</math>
- <math>\varphi \land \psi\,\!</math>
- Simplification (or Conjunction Elimination)
- <math>\underline{\varphi \land \psi}\,\!</math>
- <math>\varphi\,\!</math>
- <math>\underline{\varphi \land \psi}\,\!</math>
- <math>\psi\,\!</math>
Rules for disjunctions
- Addition (or Disjunction Introduction)
- <math>\underline{\varphi \quad \quad \ \ }\,\!</math>
- <math>\varphi \lor \psi\,\!</math>
- <math>\underline{\psi \quad \quad \ \ }\,\!</math>
- <math>\varphi \lor \psi\,\!</math>
- Separation of Cases (or Disjunction Elimination)
- <math>\varphi \lor \psi\,\!</math>
- <math>\varphi \rightarrow \chi\,\!</math>
- <math>\underline{\psi \rightarrow \chi}\,\!</math>
- <math>\chi\,\!</math>
- Disjunctive syllogism
- <math>\varphi \lor \psi\,\!</math>
- <math>\underline{\lnot \varphi \quad \quad}\,\!</math>
- <math>\psi\,\!</math>
- <math>\varphi \lor \psi\,\!</math>
- <math>\underline{\lnot \psi \quad \quad}\,\!</math>
- <math>\varphi\,\!</math>
Rules for biconditionals
- Biconditional Introduction
- <math>\varphi \rightarrow \psi\,\!</math>
- <math>\underline{\psi \rightarrow \varphi}\,\!</math>
- <math>\varphi \leftrightarrow \psi\,\!</math>
- Biconditional Elimination
- <math>\varphi \leftrightarrow \psi\,\!</math>
- <math>\underline{\varphi \quad \quad}\,\!</math>
- <math>\psi\,\!</math>
- <math>\varphi \leftrightarrow \psi\,\!</math>
- <math>\underline{\psi \quad \quad}\,\!</math>
- <math>\varphi\,\!</math>
Rules of classical predicate calculus
In the following rules, <math>\varphi(\beta / \alpha)\,\!</math> is exactly like <math>\varphi\,\!</math> except for having the free term <math>\beta\,\!</math> everywhere <math>\varphi\,\!</math> has the free variable <math>\alpha\,\!</math>.
- Universal Introduction (or Universal Generalization)
- <math>\underline{\varphi(\beta / \alpha)}\,\!</math>
- <math>\forall \alpha\, \varphi\,\!</math>
Restriction: <math>\beta\,\!</math> does not occur free in <math>\forall \alpha\, \varphi\,\!</math> or in any non-discharged assumption.
- Universal Elimination (or Universal Instantiation)
- <math> \forall \alpha\, \varphi\!</math>
- <math>\overline{\varphi{(\beta / \alpha)}}\!</math>
- Existential Introduction (or Existential Generalization)
- <math>\underline{\varphi(\beta / \alpha)}\,\!</math>
- <math>\exists \alpha\, \varphi\,\!</math>
- Existential Elimination
- <math>\exists \alpha\, \varphi\,\!</math>
- <math>\underline{\varphi(\beta / \alpha) \vdash \psi}\,\!</math>
- <math>\psi\,\!</math>
Restriction: <math>\beta\,\!</math> does not occur free in <math>\exists \alpha \varphi\,\!</math>, in <math>\psi\,\!</math> or in any non-discharged assumption.he:חוקי היקש