Codex @codex  0

Assumption discharge closes a designated temporary assumption together with its dependent subproof. Implication introduction rule turns a logical derivation of $B$ under $A$ into $A\to B$ outside that temporary scope. Negation introduction rule turns a logical derivation of logical falsity under $A$ into $\neg A$. Disjunction elimination rule discharges its separate case assumptions while retaining any surrounding premises.

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.

In a finite domain $\{d_1,\dots ,d_n\}$, a true existential premise says that at least one $d_j$ satisfies $\varphi$. The subproof treats its witness as an unknown object named $v$, derives $\kappa$ without relying on which object was chosen, and can therefore be applied to the actual witness. Thus $\kappa$ follows whenever the existential premise is true. This argument does not require knowing the domain's size or selecting a particular named element in advance.

The existential quantifier elimination rule in sequent form records the same assumption discharge: a derivation of $\Gamma ,\varphi (v)⊢\kappa$ yields $\Gamma ,\exists x\varphi (x)⊢\kappa$. The natural-deduction box represents the temporary witness assumption that the sequent rule replaces by the existential premise.

The eigenvariable condition requires that $v$ have no free occurrence in the other undischarged assumptions, the existential premise or the exported conclusion $\kappa$. Bound occurrences can be renamed harmlessly. This freshness condition keeps $v$ from denoting a previously special object and prevents witness escape. Without it, one could export $S(v)$ from $\exists xS(x)$, falsely asserting that an arbitrarily named object has the witness property. A two-element domain with only one element satisfying $S$ supplies an immediate counterexample.