Rule of Implication/Proof Rule/Tableau Form

Proof Rule

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$

Sources

• 1965: E.J. Lemmon: Beginning Logic ... (previous) ... (next): $\S 1.2$: Conditionals and Negation