# Definition:Proof System

## Contents

## 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:

- 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 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**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 tableaus 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 - 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$