Category:Rule of Implication

From ProofWiki
Jump to navigation Jump to search

This category contains pages concerning Rule of Implication:


The rule of implication is a valid argument in types of logic dealing with conditionals $\implies$.

This includes propositional logic and predicate logic, and in particular natural deduction.


Proof Rule

If, by making an assumption $\phi$, we can conclude $\psi$ as a consequence, we may infer $\phi \implies \psi$.
The conclusion $\phi \implies \psi$ does not depend on the assumption $\phi$, which is thus discharged.


Sequent Form

The Rule of Implication can be symbolised by the sequent:

\(\ds \paren {p \vdash q}\) \(\) \(\ds \)
\(\ds \vdash \ \ \) \(\ds p \implies q\) \(\) \(\ds \)