Rule of Top-Introduction

From ProofWiki
Jump to navigation Jump to search

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