Final rule

This article or section needs to be revised. Details should be given on the talk page. Please help to improve it , and then remove this flag.

This article or the following section is not adequately provided with supporting documents ( e.g. individual evidence ). Information without sufficient evidence could be removed soon. Please help Wikipedia by researching the information and including good evidence.

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 .

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.

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 .

5) Indirect proof by reductio ad absurdum

${\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.

• Modus ponendo tollens

${\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 .

• Counterposition

${\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 .

• Appointment rule
• Replacement rule

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 ).