# Rule of Implication/Proof Rule

## 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$

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

## Technical Note

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

{{Implication|line|pool|statement|start|end}}

where:

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