 A few remarks: First, the expression [α — γ] represents the fact that α is an auxiliary assumption in the proof of γ that eventually gets discharged, i.e. discarded. For example, ∃E tells us that if in the process of constructing a proof one has already derived ∃xα(x) and also β with α(a/x) as an auxiliary assumption then the inference to β is allowed. Second, the eigenparameter, a, in ∃E and ∀I must be foreign to the premises, undischarged—“active”—assumptions, to the rule’s conclusion and, in the case of ∃E, to ∃xα(x). Third, ⊥ is shorthand for two contradictory formulas, β and ~β. Finally, NK is complete: If Γ  ⊨  α then there is a proof of α from Γ using the rules of NK.