- The implication introduction rule assumes locally, derives under that assumption, then concludes while discharging the temporary assumption.
- The disjunction elimination rule uses and two local cases: one derives a common conclusion from , and the other derives that same from . It concludes and discharges both case assumptions.
- The negation introduction rule assumes locally and derives logical falsity. Discharging that assumption gives .
The boxes delimit a subproof and identify the lifetime of its temporary assumptions. A result depending on a boxed assumption is available inside that box and its nested boxes; it cannot simply be exported outside. The enclosing rule specifies what may be exported and which assumptions are discharged. Other premises on which the derivation depends remain undischarged. This assumption discharge discipline distinguishes a conditional argument from an unconditional proof.
Articles by others on the same topic
There are currently no matching articles.