Definition:Proof System

From ProofWiki
Jump to: navigation, 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

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.


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