Rule of Top-Introduction

Proof Rule

The Rule of Top-Introduction is a valid deduction sequent in propositional logic:

At any stage, we may conclude a tautology $\top$.

It can be written:

$\ds {\hspace{4em} \over \top} \top_i$

Sequent Form

The Rule of Top-Introduction can be symbolised by the sequent:

$\vdash \top$

Tableau Form

In a tableau proof, the Rule of Top-Introduction is invoked as follows:

			Pool:					Empty
			Formula:					$\top$
			Description:					Rule of Top-Introduction
			Depends on:					Nothing
			Discharged Assumptions:					None
			Abbreviation:					$\top \II$

Explanation

This entirely obvious rule allows to manipulate formulae involving $\top$ in tableau proofs.

Technical Note

When invoking the Rule of Top-Introduction in a tableau proof, use the {{TopIntro}} template:

{{TopIntro|line}}

where:

line is the number of the line on the tableau proof where the Rule of Top-Introduction is to be invoked