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.
Read more about this topic: Rule Of Inference
Famous quotes containing the words axiom and/or axioms:
“It’s an old axiom of mine: marry your enemies and behead your friends.”
—Robert N. Lee. Rowland V. Lee. King Edward IV (Ian Hunter)
““I tell you the solemn truth that the doctrine of the Trinity is not so difficult to accept for a working proposition as any one of the axioms of physics.””
—Henry Brooks Adams (1838–1918)