Definition:Rule of Inference

From ProofWiki
Jump to navigation Jump to search

Definition

Let $\LL$ be a formal language.

Part of defining a proof system $\mathscr P$ for $\LL$ is to specify its rules of inference.


A rule of inference is a specification of a valid means to conclude new theorems in $\mathscr P$ from given theorems and axioms of $\mathscr P$.

Often, the formulation of rules of inference also appeals to the notion of provable consequence to be able to deal with assumptions as part of a proof.


Structure of a Proof Rule

In most cases, an application of a proof rule can be given a structure, as follows:

  • Definition: This specifies what the proof rule actually does. Note the careful use of can and may in the definition:
  1. Can implies that it is possible to achieve something based on the structure of the system which is being constructed.
  2. May implies that this is what this particular proof rule is allowing you to do.
  • Abbreviation: When deriving a sequent, it is convenient to use a precisely defined shorthand to indicate which rule is being applied at a particular point. While important when used in a medium where space is limited, for example in printed books, on $\mathsf{Pr} \infty \mathsf{fWiki}$ these are not so much relied upon.
  • Deduced from: The truth value of a result which is being deduced by a particular proof rule depends on a specific set of premises, or assumptions made during the course of derivation. This pool of assumptions will vary depending on what the proof rule is and what previously derived result or results the proof rule depends on.
  • Discharged assumptions: This specifies which, if any, assumptions have been discharged, that is, no longer contribute to the truth value of the conclusion being derived.
  • Depends on: This specifies the result from which the proof rule directly derives its result.

However, some proof systems defy such description, such as the Proof System of Propositional Tableaux.


Also known as

A rule of inference is also known as:

an inference rule
a rule of transformation or a transformation rule
a rule of derivation
a rule of proof.
a rule of deduction.

With all these, literature might have a specific meaning attached, so be careful before treating any of these as synonyms.

On $\mathsf{Pr} \infty \mathsf{fWiki}$, proof rule and rule of inference are the terminology of choice and are used interchangeably.


Examples

Modus Ponendo Ponens

In the context of propositional logic, an example of a rule of inference is:

If $p$ is a theorem, and $p \implies q$ is a theorem, then $q$ is a theorem.

which expresses Modus Ponendo Ponens.


Also see

  • Results about rules of inference can be found here.


Sources

Retrieved from "https://proofwiki.org/w/index.php?title=Definition:Rule_of_Inference&oldid=702478"