Rule of Inference - Axiom Schemas and Axioms

Axiom Schemas and Axioms

Inference rules may also be stated in this form: (1) some (perhaps zero) premises, (2) a turnstile symbol, which means "infers", "proves" or "concludes", (3) a conclusion. This usually embodies the relational (as opposed to functional) view of a rule of inference, where the turnstile stands for a deducibility relation holding between premises and conclusion.

An inference rule containing no premises is called an axiom schema or it if contains no metavariables simply an axiom.

Rules of inference must be distinguished from axioms of a theory. In terms of semantics, axioms are valid assertions. Axioms are usually regarded as starting points for applying rules of inference and generating a set of conclusions. Or, in less technical terms:

Rules are statements ABOUT the system, axioms are statements IN the system. For example:

• The RULE that from you can infer is a statement that says if you've proven p, then it is provable that p is provable. This holds in Peano arithmetic, for example.
• The Axiom would mean that every true statement is provable. This does not hold in Peano arithmetic.

Rules of inference play a vital role in the specification of logical calculi as they are considered in proof theory, such as the sequent calculus and natural deduction.