Definition:Proof System

From ProofWiki
Jump to navigation Jump to search

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.


Also see


Sources