Definition:Proof System/Formal Proof

Definition

Let $\mathscr P$ be a proof system for a formal language $\LL$.

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 see

• Definition:Proof

• Results about formal proofs can be found here.

Sources

• 1959: A.H. Basson and D.J. O'Connor: Introduction to Symbolic Logic (3rd ed.) ... (previous) ... (next): $\S 4.3$: Derivable Formulae
• 1998: David Nelson: The Penguin Dictionary of Mathematics (2nd ed.) ... (previous) ... (next): proof
• 2008: David Nelson: The Penguin Dictionary of Mathematics (4th ed.) ... (previous) ... (next): proof
• 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 3.1$: Definition $3.1$