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 .
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 .
Five traditional closing rules
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.
- 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
- In words: If p is a sufficient condition for q and q is not true , then p is also not true .
- 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 .
- In words: if p or q and p is not true , then q is true .
- 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.
- In words: If p and q are not true , but p is true , then q is not true .
- 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.
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 ).