Logic portal

This is a list of rules of inference, logical laws that relate to mathematical formulae.

Introduction[link]

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

Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi \vdash \psi\,\!

indicates such a subderivation from the temporary assumption Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi\,\!

to Failed to parse (Missing texvc executable; please see math/README to configure.): \psi\,\!

.

Rules for classical sentential calculus[link]

Sentential calculus is also known as propositional calculus.

Rules for negations[link]

Reductio ad absurdum (or Negation Introduction)

Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi \vdash \psi\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \underline{\varphi \vdash \lnot \psi}\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \lnot \varphi\,\!

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

Failed to parse (Missing texvc executable; please see math/README to configure.): \lnot \varphi \vdash \psi\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \underline{\lnot \varphi \vdash \lnot \psi}\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi\,\!

Noncontradiction (or Negation Elimination)

Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \underline{\lnot \varphi}\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \psi\,\!

Double negation elimination

Failed to parse (Missing texvc executable; please see math/README to configure.): \underline{\lnot \lnot \varphi}\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi\,\!

Double negation introduction

Failed to parse (Missing texvc executable; please see math/README to configure.): \underline{\varphi \quad \quad}\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \lnot \lnot \varphi\,\!

Rules for conditionals[link]

Deduction theorem (or Conditional Introduction)

Failed to parse (Missing texvc executable; please see math/README to configure.): \underline{\varphi \vdash \psi}\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi \rightarrow \psi\,\!

Modus ponens (or Conditional Elimination)

Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi \rightarrow \psi\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \underline{\varphi \quad \quad \quad}\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \psi\,\!

Modus tollens

Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi \rightarrow \psi\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \underline{\lnot \psi \quad \quad \quad}\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \lnot \varphi\,\!

Rules for conjunctions[link]

Adjunction (or Conjunction Introduction)

Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \underline{\psi \quad \quad \ \ }\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi \land \psi\,\!

Simplification (or Conjunction Elimination)

Failed to parse (Missing texvc executable; please see math/README to configure.): \underline{\varphi \land \psi}\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \underline{\varphi \land \psi}\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \psi\,\!

Rules for disjunctions[link]

Addition (or Disjunction Introduction)

Failed to parse (Missing texvc executable; please see math/README to configure.): \underline{\varphi \quad \quad \ \ }\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi \lor \psi\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \underline{\psi \quad \quad \ \ }\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi \lor \psi\,\!

Case analysis

Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi \lor \psi\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi \rightarrow \chi\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \underline{\psi \rightarrow \chi}\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \chi\,\!

Disjunctive syllogism

Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi \lor \psi\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \underline{\lnot \varphi \quad \quad}\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \psi\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi \lor \psi\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \underline{\lnot \psi \quad \quad}\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi\,\!

Rules for biconditionals[link]

Biconditional introduction

Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi \rightarrow \psi\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \underline{\psi \rightarrow \varphi}\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi \leftrightarrow \psi\,\!

Biconditional Elimination

Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi \leftrightarrow \psi\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \underline{\varphi \quad \quad}\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \psi\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi \leftrightarrow \psi\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \underline{\psi \quad \quad}\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi \leftrightarrow \psi\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \underline{\lnot \varphi \quad \quad}\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \lnot \psi\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi \leftrightarrow \psi\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \underline{\lnot \psi \quad \quad}\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \lnot \varphi\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi \leftrightarrow \psi\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \underline{\psi \lor \varphi}\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \psi \land \varphi \,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi \leftrightarrow \psi\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \underline{\lnot \psi \lor \lnot \varphi}\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \lnot \psi \land \lnot \varphi \,\!

[edit] Rules of classical predicate calculus

In the following rules, Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi(\beta / \alpha)\,\!

is exactly like Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi\,\!
except for having the term Failed to parse (Missing texvc executable; please see math/README to configure.): \beta\,\!
everywhere Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi\,\!
has the free variable Failed to parse (Missing texvc executable; please see math/README to configure.): \alpha\,\!

.

Universal Introduction (or Universal Generalization)

Failed to parse (Missing texvc executable; please see math/README to configure.): \underline{\varphi{(\beta / \alpha)}}\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \forall \alpha\, \varphi\,\!

Restriction 1: Failed to parse (Missing texvc executable; please see math/README to configure.): \beta

does not occur in Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi

.
Restriction 2: Failed to parse (Missing texvc executable; please see math/README to configure.): \beta

is not mentioned in any hypothesis or undischarged assumptions.

Universal Elimination (or Universal Instantiation)

Failed to parse (Missing texvc executable; please see math/README to configure.): \forall \alpha\, \varphi\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \overline{\varphi{(\beta / \alpha)}}\!

Restriction: No free occurrence of Failed to parse (Missing texvc executable; please see math/README to configure.): \alpha\,\!

in Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi\,\!
falls within the scope of a quantifier quantifying a variable occurring in Failed to parse (Missing texvc executable; please see math/README to configure.): \beta\,\!

.

Existential Introduction (or Existential Generalization)

Failed to parse (Missing texvc executable; please see math/README to configure.): \underline{\varphi(\beta / \alpha)}\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \exists \alpha\, \varphi\,\!

Restriction: No free occurrence of Failed to parse (Missing texvc executable; please see math/README to configure.): \alpha\,\!

in Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi\,\!
falls within the scope of a quantifier quantifying a variable occurring in Failed to parse (Missing texvc executable; please see math/README to configure.): \beta\,\!

.

Existential Elimination (or Existential Instantiation)

Failed to parse (Missing texvc executable; please see math/README to configure.): \exists \alpha\, \varphi\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \underline{\varphi(\beta / \alpha) \vdash \psi}\,\!

Failed to parse (Missing texvc executable; please see math/README to configure.): \psi\,\!

Restriction 1: No free occurrence of Failed to parse (Missing texvc executable; please see math/README to configure.): \alpha\,\!

in Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi\,\!
falls within the scope of a quantifier quantifying a variable occurring in Failed to parse (Missing texvc executable; please see math/README to configure.): \beta\,\!

.
Restriction 2: There is no occurrence, free or bound, of Failed to parse (Missing texvc executable; please see math/README to configure.): \beta\,\!

in Failed to parse (Missing texvc executable; please see math/README to configure.): \psi\,\!

.

Table: Rules of Inference - a short summary[link]

The rules above can be summed up in the following table.^[1] The "Tautology" column shows how to interpret the notation of a given rule.

All rules use the basic logic operators. A complete table of "logic operators" is showed by a truth table, giving definitions of all the possible (16) truth functions of 2 boolean variables (p, q):

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 a 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 showed 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.

Example 1[link]

Let us 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 Failed to parse (Missing texvc executable; please see math/README to configure.): \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 Failed to parse (Missing texvc executable; please see math/README to configure.): p

be the proposition "If it rains today", Failed to parse (Missing texvc executable; please see math/README to configure.): q
be " We will not go on a canoe today" and let Failed to parse (Missing texvc executable; please see math/README to configure.): r
be "We will go on a canoe trip tomorrow". Then this argument is of the form:

Failed to parse (Missing texvc executable; please see math/README to configure.): \begin{align} p \rightarrow q\\ q \rightarrow r\\ \therefore \overline{p \rightarrow r} \\ \end{align}

Example 2[link]

Let us 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 before sunset." Proof by rules of inference: Let Failed to parse (Missing texvc executable; please see math/README to configure.): p

be the proposition "It is sunny this today", Failed to parse (Missing texvc executable; please see math/README to configure.): q
the proposition "It is colder than yesterday", Failed to parse (Missing texvc executable; please see math/README to configure.): r
the proposition "We will go swimming", Failed to parse (Missing texvc executable; please see math/README to configure.): s
the proposition "We will have a barbecue", and Failed to parse (Missing texvc executable; please see math/README to configure.): t
the proposition "We will be home by sunset". Then the hypotheses become Failed to parse (Missing texvc executable; please see math/README to configure.): \neg p \wedge q, r \rightarrow p, \neg r \rightarrow s
and Failed to parse (Missing texvc executable; please see math/README to configure.): s \rightarrow t

. Using our intuition we conjecture that the conclusion might be Failed to parse (Missing texvc executable; please see math/README to configure.): t . Using the Rules of Inference table we can proof the conjecture easily:

References[link]

1. ^ Kenneth H. Rosen: Discrete Mathematics and its Applications,Fifth Edition, p. 58.

This section may be confusing or unclear to readers. Please help clarify the section; suggestions may be found on the talk page. (October 2010)

In logic, a rule of inference, inference rule, or transformation rule is the act of drawing a conclusion based on the form of premises interpreted as a function which takes premises, analyses their syntax, and returns a conclusion (or conclusions). For example, the rule of inference modus ponens takes two premises, one in the form of "If p then q" and another in the form of "p" and returns the conclusion "q". The rule is valid with respect to the semantics of classical logic (as well as the semantics of many other non-classical logics), in the sense that if the premises are true (under an interpretation) then so is the conclusion.

Typically, a rule of inference preserves truth, a semantic property. In many-valued logic, it preserves a general designation. But a rule of inference's action is purely syntactic, and does not need to preserve any semantic property: any function from sets of formulae to formulae counts as a rule of inference. Usually only rules that are recursive are important; i.e. rules such that there is an effective procedure for determining whether any given formula is the conclusion of a given set of formulae according to the rule. An example of a rule that is not effective in this sense is the infinitary ω-rule.^[1]

Popular rules of inference include modus ponens, modus tollens from propositional logic and contraposition. First-order predicate logic uses rules of inference to deal with logical quantifiers. See List of rules of inference for examples.

Overview[link]

In formal logic (and many related areas), rules of inference are usually given in the following standard form:

  Premise#1
  Premise#2
        ...
  Premise#n   
  Conclusion

This expression states, that whenever in the course of some logical derivation the given premises have been obtained, the specified conclusion can be taken for granted as well. The exact formal language that is used to describe both premises and conclusions depends on the actual context of the derivations. In a simple case, one may use logical formulae, such as in:

  A→B
  A        
  ∴B

This is just the modus ponens rule of propositional logic. Rules of inference are usually formulated as rule schemata by the use of universal variables. In the rule (schema) above, A and B can be instantiated to any element of the universe (or sometimes, by convention, some restricted subset such as propositions) to form an infinite set of inference rules.

A proof system is formed from a set of rules chained together to form proofs, or derivations. Any derivation has only one final conclusion, which is the statement proved or derived. If premises are left unsatisfied in the derivation, then the derivation is a proof of a hypothetical statement: "if the premises hold, then the conclusion holds."

Admissibility and derivability[link]

In a set of rules, an inference rule could be redundant in the sense that it is admissible or derivable. A derivable rule is one whose conclusion can be derived from its premises using the other rules. An admissible rule is one whose conclusion holds whenever the premises hold. All derivable rules are admissible. To appreciate the difference, consider the following set of rules for defining the natural numbers (the judgment Failed to parse (Missing texvc executable; please see math/README to configure.): n\,\,\mathsf{nat}

asserts the fact that Failed to parse (Missing texvc executable; please see math/README to configure.): n
is a natural number):

Failed to parse (Missing texvc executable; please see math/README to configure.): \begin{matrix} \frac{}{\mathbf{0} \,\,\mathsf{nat}} & \frac{n \,\,\mathsf{nat}}{\mathbf{s(}n\mathbf{)} \,\,\mathsf{nat}} \\ \end{matrix}

The first rule states that 0 is a natural number, and the second states that s(n) is a natural number if n is. In this proof system, the following rule demonstrating that the second successor of a natural number is also a natural number, is derivable:

Failed to parse (Missing texvc executable; please see math/README to configure.): \frac{n \,\,\mathsf{nat}}{\mathbf{s(s(}n\mathbf{))} \,\,\mathsf{nat}}

Its derivation is just the composition of two uses of the successor rule above. The following rule for asserting the existence of a predecessor for any nonzero number is merely admissible:

Failed to parse (Missing texvc executable; please see math/README to configure.): \frac{\mathbf{s(}n\mathbf{)} \,\,\mathsf{nat}}{n \,\,\mathsf{nat}}

This is a true fact of natural numbers, as can be proven by induction. (To prove that this rule is admissible, assume a derivation of the premise and induct on it to produce a derivation of Failed to parse (Missing texvc executable; please see math/README to configure.): n \,\,\mathsf{nat} .) However, it is not derivable, because it depends on the structure of the derivation of the premise. Because of this, derivability is stable under additions to the proof system, whereas admissibility is not. To see the difference, suppose the following nonsense rule were added to the proof system:

Failed to parse (Missing texvc executable; please see math/README to configure.): \frac{}{\mathbf{s(-3)} \,\,\mathsf{nat}}

In this new system, the double-successor rule is still derivable. However, the rule for finding the predecessor is no longer admissible, because there is no way to derive Failed to parse (Missing texvc executable; please see math/README to configure.): \mathbf{-3} \,\,\mathsf{nat} . The brittleness of admissibility comes from the way it is proved: since the proof can induct on the structure of the derivations of the premises, extensions to the system add new cases to this proof, which may no longer hold.

Admissible rules can be thought of as theorems of a proof system. For instance, in a sequent calculus where cut elimination holds, the cut rule is admissible.

Other considerations[link]

Inference rules may also be stated in this form: (1) some (perhaps zero) premises, (2) a turnstile symbol Failed to parse (Missing texvc executable; please see math/README to configure.): \vdash , which means "infers", "proves" or "concludes", (3) a conclusion. This usually embodies the relational (as opposed to functional) view of a rule of inference, where the turnstile stands for a deducibility relation holding between premises and conclusion.

Rules of inference must be distinguished from axioms of a theory. In terms of semantics, axioms are valid assertions. Axioms are usually regarded as starting points for applying rules of inference and generating a set of conclusions. Or, in less technical terms:

Rules are statements ABOUT the system, axioms are statements IN the system. For example:

• The RULE that from Failed to parse (Missing texvc executable; please see math/README to configure.): \vdash p

you can infer Failed to parse (Missing texvc executable; please see math/README to configure.): \vdash\text{Provable}(p)
is a statement that says if you've proven p, then it is provable that p is provable. This holds in Peano arithmetic, for example.

• The Axiom Failed to parse (Missing texvc executable; please see math/README to configure.): p \to \text{Provable}(p)

would mean that every true statement is provable. This does not hold in Peano arithmetic.

Rules of inference play a vital role in the specification of logical calculi as they are considered in proof theory, such as the sequent calculus and natural deduction.

See also[link]

• Inference objection
• Immediate inference
• Law of thought
• Logical truth

References[link]