⊥ Intro

• Posso inferire ⊥ usando P∧¬P, avendo magari P già provato e ¬P inferito in usa sottoprova.

$$ \bot\ Intro:P,\neg P \models_T P $$

⊥ Elim

• Avendo ⊥ posso inferire qualsiasi cosa (ma tutto, cioè, tutto)

$$ \bot Elim: \bot \models_T P $$