Rule of Implication

From ProofWiki
Jump to navigation Jump to search

Proof Rule

The rule of implication is a valid deduction sequent in propositional logic.


Proof Rule

If, by making an assumption $\phi$, we can conclude $\psi$ as a consequence, we may infer $\phi \implies \psi$.


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 \)


Explanation

The Rule of Implication can be expressed in natural language as:

If by making an assumption $\phi$ we can deduce $\psi$, then we can encapsulate this deduction into the compound statement $\phi \implies \psi$.


Also known as

The Rule of Implication is sometimes known as:

  • The rule of implies-introduction
  • The rule of conditional proof (abbreviated $\text{CP}$).


Sources