Rule of Implication/Proof Rule

From ProofWiki
Jump to: navigation, search

Proof Rule

The Rule of Implication is a valid deduction sequent in propositional logic.

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


It can be written:

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


Tableau Form

Let $\phi$ and $\psi$ be two propositional 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 \mathcal I$             


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


Sources