\begin{definition}[Definition:Proof System/Formal Proof]
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.
\end{definition}