Rule of Top-Introduction
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