This concise manuscript investigates the nonlocal nature of natural deduction, particularly the possibility of introducing assumptions at intermediate stages of a derivation after those stages have already been passed. By examining the structural correspondence between natural deduction and sequent calculus, we demonstrate how the structural rule of left-weakening (LW) permits the enlargement of an antecedent after its corresponding succedent has been derived, without modifying the original inference. Through a number of symmetrical derivations, we establish the proof-theoretic relationship between the introduction of assumptions in natural deduction and antecedent expansion in sequent calculus. On this basis, we formulate the principle of Nonlocal Assumption Introduction (NAI), according to which assumptions may be introduced at any intermediate stage prior to the final conclusion, provided that the corresponding structural expansion is proof-theoretically valid. We further specify the conditions governing this operation, including the preservation of inferential validity, assumption dependencies, and the scope and discharge requirements of the resulting derivation.

翻译：暂无翻译