Rule of Implication/Proof Rule

From ProofWiki
Jump to navigation Jump to search

Proof Rule

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.

As a proof rule it is expressed in the form:

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.

It can be written:

$\ds {\begin {array} {|c|} \hline \phi \\ \vdots \\ \psi \\ \hline \end {array} \over \phi \implies \psi} \to_i$

Tableau Form

Let $\phi$ and $\psi$ be two well-formed formulas in a tableau proof.

The Rule of Implication is invoked for $\phi$ and $\psi$ in the following manner:

Pool:    The pooled assumptions of $\psi$      
Formula:    $\phi \implies \psi$      
Description:    Rule of Implication      
Depends on:    The series of lines from where the assumption $\phi$ was made to where $\psi$ was deduced      
Discharged Assumptions:    The assumption $\phi$ is discharged      
Abbreviation:    $\text{CP}$ or $\implies \II$      


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}$).

Also see

Technical Note

When invoking the Rule of Implication in a tableau proof, use the {{Implication}} template:



line is the number of the line on the tableau proof where the Rule of Implication is to be invoked
pool is the pool of assumptions (comma-separated list)
statement is the statement of logic that is to be displayed in the Formula column, without the $ ... $ delimiters
start is the line of the tableau proof where the antecedent can be found
end is the line of the tableau proof where the consequent can be found