Modus ponens aplicado a \(P\to Q\) y \(P\) produce \(Q\), que queda justificada por esa regla. Las otras opciones carecen de regla válida que las sostenga.
Una demostración formal de \(\varphi_n\) es una sucesión \(\varphi_1,\ldots,\varphi_n\) en la que cada término es un axioma, una hipótesis admitida o el resultado de una regla aplicada a términos anteriores.