# 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