The basic law for exhaustiveness says that having one of a pair of contradictory sentences as a premises comes to the same thing as having the other as an alternative. This does not apply to entailment directly, but we can consider a special case, the basic law for contradictories, which says that one of a pair of contradictory sentences is entailed by a set if and only if the other is inconsistent with that set. Since a sentence and its negation are contradictories, this gives us a pair of principles, laws for negation as a premise and as a conclusion.
Inconsistency is established by a reductio argument. In a derivation, this will be associated with a gap that has ⊥ as its goal. In order to show a sentence inconsistent with our premises, we add it as a further assumption in the reductio argument. This further assumption may be referred to as a supposition of this argument to distinguish it from the premises with which we hope to show it inconsistent. The rule implementing this idea is Reductio ad Absurdum (RAA). To actually reach the goal of ⊥, we add a rule allowing us to close a gap when a sentence and its negation are among the resources. This rule is Non-contradiction (Nc) and is named after the traditional law of non-contradiction.
The use of suppositions means that we will no longer always be able to group all uses of Ext at the beginning of a derivation. A more temporary complication is the need to use Adj to form a sentence contradictory to a negated conjunction, something that will be handled by a direct rule introduced in the next section.