Definition:Proof System
Definition
Let $\LL$ be a formal language.
A proof system $\mathscr P$ for $\LL$ comprises:
- Axioms and/or axiom schemata;
- Rules of inference for deriving theorems.
It is usual that a proof system does this by declaring certain arguments concerning $\LL$ to be valid.
Informally, a proof system amounts to a precise account of what constitutes a (formal) proof.
Rule 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.
Axiom
Let $\LL$ be a formal language.
Part of defining a proof system $\mathscr P$ for $\LL$ is to specify its axioms.
An axiom of $\mathscr P$ is a well-formed formula of $\LL$ that $\mathscr P$ approves of by definition.
Formal Proof
Let $\phi$ be a WFF of $\LL$.
A formal proof of $\phi$ in $\mathscr P$ is a collection of axioms and rules of inference of $\mathscr P$ that leads to the conclusion that $\phi$ is a theorem of $\mathscr P$.
The term formal proof is also used to refer to specific presentations of such collections.
For example, the term applies to tableau proofs in natural deduction.
Also known as
A proof system is referred to by some sources as an axiom system.
Others call it a mathematical theory.
Some sources consider the formal language $\LL$ as an implicit part of the proof system and do not define it separately.
Examples
Gentzen Proof Systems
Gentzen proof systems are a class of proof systems for propositional and predicate logic.
Their characteristics include:
- The presence of few axioms and many rules of inference.
- Use of formal, sequent-like notation involving the turnstile $\vdash$.
- Proofs whose structure can be viewed as rooted trees.
Hilbert Proof Systems
Hilbert proof systems are a class of proof systems for propositional and predicate logic.
Their characteristics include:
- The presence of many axioms;
- Typically only Modus Ponendo Ponens as a rule of inference.
Propositional Tableaux
Tableau proofs form a proof system $\mathrm{PT}$ for the language of propositional logic $\LL_0$.
It consists solely of axioms, in the following way:
- A WFF $\mathbf A$ is a $\mathrm{PT}$-axiom if and only if there exists a tableau proof of $\mathbf A$.
Likewise, we can define the notion of provable consequence for $\mathrm{PT}$:
- A WFF $\mathbf A$ is a $\mathrm{PT}$-provable consequence of a collection of WFFs $\mathbf H$ if there exists a tableau proof of $\mathbf A$ from $\mathbf H$.
Although formally $\mathrm{PT}$ has no rules of inference, the rules for the definition of propositional tableaux can informally be regarded as such.
Also see
Sources
- 1959: A.H. Basson and D.J. O'Connor: Introduction to Symbolic Logic (3rd ed.) ... (previous) ... (next): $\S 4.3$: Derivable Formulae
- 1968: Nicolas Bourbaki: Theory of Sets ... (previous): Chapter $\text I$: Description of Formal Mathematics: $1$. Terms and Relations: $1$. Signs and Assemblies
- 1972: A.G. Howson: A Handbook of Terms used in Algebra and Analysis ... (previous) ... (next): $\S 1$: Some mathematical language: Axiom systems
- 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 3.1$: Definition $3.1$