Representing Scope in Intuitionistic Deductions

Intuitionistic proofs can be segmented into scopes which describe when assumptions can be used. In standard descriptions of intuitionistic logic, these scopes occupy contiguous regions of proofs. This leads to an explosion in the search space for automated deduction, because of the difficulty of planning to apply a rule inside a particular scoped region of the proof. This paper investigates an alternative representation which assigns scope explicitly to formulas, and which is inspired in part by semantics-based translation methods for modal deduction. This calculus is simple and is justified by direct proof-theoretic arguments that transform proofs in the calculus so that scopes match standard descriptions. A Herbrand theorem, established straightforwardly, lifts this calculus to incorporate unification. The resulting system has no impermutabilities whatsoever—rules of inference may be used equivalently anywhere in the proof. Nevertheless, a natural specification describes how λ-terms are to be extracted from its deductions.