If we think of $\top$ as $(\neg\bot)$, we might be able to make a natural deduction rules for $\top$ from the natural deduction rules of $ \neg $ and $\bot$. The following are some of the natural deduction rules of my logic book.
axioms: $\Sigma \vdash \alpha$ iff $\alpha$ occurs in $\Sigma$
FI: $\dfrac{\Sigma \vdash \alpha, \ \Sigma \vdash (\neg\alpha) }{\Sigma \vdash ⊥}$
NI: $\dfrac{\Sigma\cdot \alpha\vdash ⊥ }{\Sigma \vdash (\neg \alpha)},\quad $
NE: $\dfrac{\Sigma\cdot (\neg \alpha) \vdash ⊥ }{\Sigma \vdash\alpha}$
According to these rules, we can prove $\Sigma\vdash \top $ for any $\Sigma$. So, can we think of $\Sigma\vdash \top$ as an axiom? And what should be the $\top$-elimination rule?
Best Answer
For a structural, natural deduction presentation, the rules for $\top$ just contain $$\dfrac{}{\Sigma\vdash\top}\top\mathrm{I}$$ and that's it. There is no elimination rule. One way to see why this makes sense is that dually we want an elimination rule for $\bot$ but we certainly don't want an introduction rule. Another argument for this is that we can view $\top$ as a $0$-ary case of conjunction. For (binary) conjunction, we have an introduction rule with two premises and two elimination rules. Therefore, $\top$ should have an introduction rule with zero premises and zero elimination rules.
If we define (as is often done) $\neg\alpha$ as $\alpha\to\bot$, your FI rule (which I assume stands for something like "falsum introduction") is revealed to be a special case of $\to$ elimination. This rule is often called $\neg$ elimination, if $\neg$ is primitive (and especially if we can use an empty right-hand side of $\vdash$ to represent contradiction). I assume this is what NE is supposed to stand for, but that rule doesn't really have the appropriate form for an elimination rule. As I mentioned in an answer to an earlier question of yours, these rules are not ideally stated from a structural proof theory perspective since they combine multiple logical connectives.
We can derive the $\top$ introduction rule via the definition of $\top$ as $\neg\bot$ using your rules via: $$\dfrac{}{\dfrac{\Sigma\cdot\bot\vdash\bot}{\Sigma\vdash\top}\rlap{\mathrm{NI}}}\rlap{\mathrm{Axiom}}$$