Rule of inference

Last updated October 05, 2024

In logic and the philosophy of logic, specifically in deductive reasoning, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion (or conclusions).

For example, the rule of inference called modus ponens takes two premises, one in the form "If p then q" and another in the form "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 in propositional logic include modus ponens , modus tollens , and contraposition. First-order predicate logic uses rules of inference to deal with logical quantifiers.

Standard form

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\to B

{\underline {A\quad \quad \quad }}\,\!

B\!

This is the modus ponens rule of propositional logic. Rules of inference are often formulated as schemata employing metavariables.^[2] In the rule (schema) above, the metavariables A and B can be instantiated to any element of the universe (or sometimes, by convention, a 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, also called 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."

Example: Hilbert systems for two propositional logics

In a Hilbert system, the premises and conclusion of the inference rules are simply formulae of some language, usually employing metavariables. For graphical compactness of the presentation and to emphasize the distinction between axioms and rules of inference, this section uses the sequent notation ( $\vdash$ ) instead of a vertical presentation of rules. In this notation,

${\begin{array}{c}{\text{Premise }}1\\{\text{Premise }}2\\\hline {\text{Conclusion}}\end{array}}$

is written as $({\text{Premise }}1),({\text{Premise }}2)\vdash ({\text{Conclusion}})$ .

The formal language for classical propositional logic can be expressed using just negation (¬), implication (→) and propositional symbols. A well-known axiomatization, comprising three axiom schemata and one inference rule (modus ponens), is:

(CA1) ⊢ A → (B → A)
 (CA2) ⊢ (A → (B → C)) → ((A → B) → (A → C))
 (CA3) ⊢ (¬A → ¬B) → (B → A)
 (MP)  A, A → B ⊢ B

It may seem redundant to have two notions of inference in this case, ⊢ and →. In classical propositional logic, they indeed coincide; the deduction theorem states that A ⊢ B if and only if ⊢ A → B. There is however a distinction worth emphasizing even in this case: the first notation describes a deduction, that is an activity of passing from sentences to sentences, whereas A → B is simply a formula made with a logical connective, implication in this case. Without an inference rule (like modus ponens in this case), there is no deduction or inference. This point is illustrated in Lewis Carroll's dialogue called "What the Tortoise Said to Achilles",^[3] as well as later attempts by Bertrand Russell and Peter Winch to resolve the paradox introduced in the dialogue.

For some non-classical logics, the deduction theorem does not hold. For example, the three-valued logic of Łukasiewicz can be axiomatized as:^[4]

(CA1) ⊢ A → (B → A)
 (LA2) ⊢ (A → B) → ((B → C) → (A → C))
 (CA3) ⊢ (¬A → ¬B) → (B → A)
 (LA4) ⊢ ((A → ¬A) → A) → A
 (MP)  A, A → B ⊢ B

This sequence differs from classical logic by the change in axiom 2 and the addition of axiom 4. The classical deduction theorem does not hold for this logic, however a modified form does hold, namely A ⊢ B if and only if ⊢ A → (A → B).^[5]

Admissibility and derivability

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 $n\,\,{\mathsf {nat}}$ asserts the fact that $n$ is a natural number):

{\begin{matrix}{\begin{array}{c}\\\hline {\mathbf {0} \,\,{\mathsf {nat}}}\end{array}}&{\begin{array}{c}{n\,\,{\mathsf {nat}}}\\\hline {\mathbf {s(} n\mathbf {)} \,\,{\mathsf {nat}}}\end{array}}\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:

{\begin{array}{c}{n\,\,{\mathsf {nat}}}\\\hline {\mathbf {s(s(} n\mathbf {))} \,\,{\mathsf {nat}}}\end{array}}

Its derivation is 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:

{\begin{array}{c}{\mathbf {s(} n\mathbf {)} \,\,{\mathsf {nat}}}\\\hline {n\,\,{\mathsf {nat}}}\end{array}}

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 $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:

{\begin{array}{c}\\\hline {\mathbf {s(-3)} \,\,{\mathsf {nat}}}\end{array}}

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

Related Research Articles

In classical logic, disjunctive syllogism is a valid argument form which is a syllogism having a disjunctive statement for one of its premises.

The propositional calculus is a branch of logic. It is also called (first-order) propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions and relations between propositions, including the construction of arguments based on them. Compound propositions are formed by connecting propositions by logical connectives representing the truth functions of conjunction, disjunction, implication, biconditional, and negation. Some sources include other connectives, as in the table below.

In propositional logic, modus ponens, also known as modus ponendo ponens, implication elimination, or affirming the antecedent, is a deductive argument form and rule of inference. It can be summarized as "P implies Q.P is true. Therefore, Q must also be true."

In propositional logic, modus tollens (MT), also known as modus tollendo tollens and denying the consequent, is a deductive argument form and a rule of inference. Modus tollens is a mixed hypothetical syllogism that takes the form of "If P, then Q. Not Q. Therefore, not P." It is an application of the general truth that if a statement is true, then so is its contrapositive. The form shows that inference from P implies Q to the negation of Q implies the negation of P is a valid argument.

In logic and deductive reasoning, an argument is sound if it is both valid in form and has no false premises. Soundness has a related meaning in mathematical logic, wherein a formal system of logic is sound if and only if every well-formed formula that can be proven in the system is logically valid with respect to the logical semantics of the system.

In mathematics and theoretical computer science, a type theory is the formal presentation of a specific type system. Type theory is the academic study of type systems.

In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use axioms as much as possible to express the logical laws of deductive reasoning.

Deductive reasoning is the process of drawing valid inferences. An inference is valid if its conclusion follows logically from its premises, meaning that it is impossible for the premises to be true and the conclusion to be false. For example, the inference from the premises "all men are mortal" and "Socrates is a man" to the conclusion "Socrates is mortal" is deductively valid. An argument is sound if it is valid and all its premises are true. One approach defines deduction in terms of the intentions of the author: they have to intend for the premises to offer deductive support to the conclusion. With the help of this modification, it is possible to distinguish valid from invalid deductive reasoning: it is invalid if the author's belief about the deductive support is false, but even invalid deductive reasoning is a form of deductive reasoning.

"What the Tortoise Said to Achilles", written by Lewis Carroll in 1895 for the philosophical journal Mind, is a brief allegorical dialogue on the foundations of logic. The title alludes to one of Zeno's paradoxes of motion, in which Achilles could never overtake the tortoise in a race. In Carroll's dialogue, the tortoise challenges Achilles to use the force of logic to make him accept the conclusion of a simple deductive argument. Ultimately, Achilles fails, because the clever tortoise leads him into an infinite regression.

In classical logic, a hypothetical syllogism is a valid argument form, a deductive syllogism with a conditional statement for one or both of its premises. Ancient references point to the works of Theophrastus and Eudemus for the first investigation of this kind of syllogisms.

In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology instead of an unconditional tautology. Each conditional tautology is inferred from other conditional tautologies on earlier lines in a formal argument according to rules and procedures of inference, giving a better approximation to the natural style of deduction used by mathematicians than David Hilbert's earlier style of formal logic, in which every line was an unconditional tautology. More subtle distinctions may exist; for example, propositions may implicitly depend upon non-logical axioms. In that case, sequents signify conditional theorems of a first-order theory rather than conditional tautologies.

In mathematical logic, a sequent is a very general kind of conditional assertion.

In mathematical logic, a deduction theorem is a metatheorem that justifies doing conditional proofs from a hypothesis in systems that do not explicitly axiomatize that hypothesis, i.e. to prove an implication A → B, it is sufficient to assume A as a hypothesis and then proceed to derive B. Deduction theorems exist for both propositional logic and first-order logic. The deduction theorem is an important tool in Hilbert-style deduction systems because it permits one to write more comprehensible and usually much shorter proofs than would be possible without it. In certain other formal proof systems the same conveniency is provided by an explicit inference rule; for example natural deduction calls it implication introduction.

Condensed detachment is a method of finding the most general possible conclusion given two formal logical statements. It was developed by the Irish logician Carew Meredith in the 1950s and inspired by the work of Łukasiewicz.

In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation-complete theorem-proving technique for sentences in propositional logic and first-order logic. For propositional logic, systematically applying the resolution rule acts as a decision procedure for formula unsatisfiability, solving the Boolean satisfiability problem. For first-order logic, resolution can be used as the basis for a semi-algorithm for the unsatisfiability problem of first-order logic, providing a more practical method than one following from Gödel's completeness theorem.

Metamath is a formal language and an associated computer program for archiving and verifying mathematical proofs. Several databases of proved theorems have been developed using Metamath covering standard results in logic, set theory, number theory, algebra, topology and analysis, among others.

In logic, more specifically proof theory, a Hilbert system, sometimes called Hilbert calculus, Hilbert-style system, Hilbert-style proof system, Hilbert-style deductive system or Hilbert–Ackermann system, is a type of formal proof system attributed to Gottlob Frege and David Hilbert. These deductive systems are most often studied for first-order logic, but are of interest for other logics as well.

In mathematical logic, monoidal t-norm based logic, the logic of left-continuous t-norms, is one of the t-norm fuzzy logics. It belongs to the broader class of substructural logics, or logics of residuated lattices; it extends the logic of commutative bounded integral residuated lattices by the axiom of prelinearity.

Suppes–Lemmon notation is a natural deductive logic notation system developed by E.J. Lemmon. Derived from Suppes' method, it represents natural deduction proofs as sequences of justified steps. Both methods use inference rules derived from Gentzen's 1934/1935 natural deduction system, in which proofs were presented in tree-diagram form rather than in the tabular form of Suppes and Lemmon. Although the tree-diagram layout has advantages for philosophical and educational purposes, the tabular layout is much more convenient for practical applications.

References

↑ Boolos, George; Burgess, John; Jeffrey, Richard C. (2007). Computability and logic. Cambridge: Cambridge University Press. p. 364. ISBN 978-0-521-87752-7.
↑ John C. Reynolds (2009) [1998]. Theories of Programming Languages. Cambridge University Press. p. 12. ISBN 978-0-521-10697-9.
↑ Kosta Dosen (1996). "Logical consequence: a turn in style". In Maria Luisa Dalla Chiara; Kees Doets; Daniele Mundici; Johan van Benthem (eds.). Logic and Scientific Methods: Volume One of the Tenth International Congress of Logic, Methodology and Philosophy of Science, Florence, August 1995. Springer. p. 290. ISBN 978-0-7923-4383-7. preprint (with different pagination)
↑ Bergmann, Merrie (2008). An introduction to many-valued and fuzzy logic: semantics, algebras, and derivation systems . Cambridge University Press. p. 100. ISBN 978-0-521-88128-9.
↑ Bergmann, Merrie (2008). An introduction to many-valued and fuzzy logic: semantics, algebras, and derivation systems . Cambridge University Press. p. 114. ISBN 978-0-521-88128-9.

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.

[1] Boolos, George; Burgess, John; Jeffrey, Richard C. (2007). Computability and logic. Cambridge: Cambridge University Press. p. 364. ISBN 978-0-521-87752-7.

[Reynolds2009-2] John C. Reynolds (2009) [1998]. Theories of Programming Languages. Cambridge University Press. p. 12. ISBN 978-0-521-10697-9.

[ChiaraDoets1996-3] Kosta Dosen (1996). "Logical consequence: a turn in style". In Maria Luisa Dalla Chiara; Kees Doets; Daniele Mundici; Johan van Benthem (eds.). Logic and Scientific Methods: Volume One of the Tenth International Congress of Logic, Methodology and Philosophy of Science, Florence, August 1995. Springer. p. 290. ISBN 978-0-7923-4383-7. preprint (with different pagination)

[4] Bergmann, Merrie (2008). An introduction to many-valued and fuzzy logic: semantics, algebras, and derivation systems . Cambridge University Press. p. 100. ISBN 978-0-521-88128-9.

[5] Bergmann, Merrie (2008). An introduction to many-valued and fuzzy logic: semantics, algebras, and derivation systems . Cambridge University Press. p. 114. ISBN 978-0-521-88128-9.

[1]

[2]

[3]

[4]

[5]