Definition:Proof System/Formal Proof

From ProofWiki
Jump to navigation Jump to search


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