Definition:Proof System/Formal Proof

From ProofWiki
Jump to: navigation, search

Definition

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


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 see


Sources