# Final rule

A rule of inference (or rule of inference ) describes a rule of transformation (transformation rule ) in a calculus of formal logic , i. H. a syntactic rule according to which it is allowed to move from existing expressions of a formal language to new expressions. This rule-based transition represents a conclusion .

## General

A valid final rule should only allow the transition to expressions whose statements also follow semantically from the statement of the existing expressions ( see logical derivation ).

The exact nature of the rules of inference depends on the logical system for which the calculus is drawn up. For traditional and classical logic, which satisfy the principle of duality , conclusions must be truth-preserving (“only truth follows from truth”). Due to this property, modern propositional calculi and predicate logic systems understand themselves as proof calculi , although inference rules per se are not yet rules of proof. Inference rules differ within classical logic from axioms or axiom schemes, insofar as they do not place any concrete semantic requirements on the universe of discourse .

Modern logic calculi use in particular the modus ponens , as well as introduction and elimination rules for certain logical connectives .

The following five rules come from traditional propositional logic, the tradition of which begins at the latest in the Stoa ( Megarian propositional logic ). One or two statements are written above the horizontal line, from which the statement under the horizontal line follows.

1) Modus ponendo ponens (Latin for setting that which is to be posited , also rule of separation ) is the basic form of direct proof :

${\ displaystyle p \ rightarrow q \ qquad p \ over q}$ In words: If p is a sufficient condition for q and p is true , then q is also true . (semantic)

If p is asserted, q can also be asserted. Now p is asserted, thus: q . (syntactically)

2) Modus tollendo tollens (Latin for canceling what is to be canceled ): the indirect proof

${\ displaystyle p \ rightarrow q \ qquad \ neg q \ over \ neg p}$ In words: If p is a sufficient condition for q and q is not true , then p is also not true .

3) Chain link (occasionally - actually wrong, because after another meaning of the word "chain link" - called Modus Barbara )

${\ displaystyle p \ rightarrow q \ qquad q \ rightarrow r \ over p \ rightarrow r}$ In words: If p is a sufficient condition for q and q is a sufficient condition for r , then p is a sufficient condition for r .

4) Modus tollendo ponens (sometimes incorrectly called disjunctive syllogism )

${\ displaystyle p \ lor q \ qquad \ neg p \ over q}$ In words: if p or q and p is not true , then q is true .
${\ displaystyle \ neg p \ rightarrow (q \ land \ neg q) \ over p}$ In words: If non-p is a sufficient condition for a contradiction (q and non-q) to be true , then non-p is false (because a contradiction cannot be true, so its sufficient condition must not be true either be), so p is true.

## Further final rules

Other known inference rules include: a.

${\ displaystyle \ neg (p \ land q) \ qquad p \ over \ neg q}$ In words: If p and q are not true , but p is true , then q is not true .
${\ displaystyle p \ rightarrow q \ over \ neg q \ rightarrow \ neg p}$ In words: If p is a sufficient condition for q , then q is not a sufficient condition for not p .

Calculi of natural inference usually include a large number of inference rules; for further examples of common inference rules, see the article Systems of Natural Inference .

Logical statements can also be reformulated using resolution rules. In this way, certain types of conclusions can be automated as evidence of contradiction.

Abduction is not a valid rule of thumb . Nevertheless, it is used in artificial intelligence and knowledge representation to simulate “ common sense ”.

A regular conclusion that has only one of its premises as a consequence is a circular reasoning and represents a conclusion, but no proof or no argument for the conclusion (see also petitio principii ).