# Definition:Proof System

## Definition

Let $\mathcal L$ be a formal language.

A proof system $\mathscr P$ for $\mathcal L$ 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 $\mathcal L$ 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.

### Axiom

Let $\mathcal L$ be a formal language.

Part of defining a proof system $\mathscr P$ for $\mathcal L$ is to specify its axioms.

An axiom of $\mathscr P$ is a well-formed formula of $\mathcal L$ that $\mathscr P$ approves of by definition.

### Formal Proof

Let $\phi$ be a WFF of $\mathcal L$.

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.

## Examples

### Gentzen Proof Systems

Gentzen proof systems are a class of proof systems for propositional and predicate logic.

Their characteristics include:

### Hilbert Proof Systems

Hilbert proof systems are a class of proof systems for propositional and predicate logic.

Their characteristics include:

### Propositional Tableaus

Tableau proofs form a proof system $\mathrm{PT}$ for the language of propositional logic $\mathcal L_0$.

It consists solely of axioms, in the following way:

A WFF $\mathbf A$ is a $\mathrm{PT}$-axiom iff 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 tableaus can informally be regarded as such.