It is well-known that extending the Hilbert axiomatic system for first-order intuitionistic logic with an exclusion operator, that is dual to implication, collapses the domains in the model into a constant domain. This makes it a very challenging problem to find a sound and complete proof system for first-order bi-intuitionistic logic with non-constant domains, that is also conservative over first-order intuitionistic logic. We solve this problem by presenting the first sound and complete proof system for first-order bi-intuitionistic logic with increasing domains. We formalize our proof system in a labeled polytree sequent calculus (a notational variant of nested sequents), and prove that it enjoys cut-elimination and is conservative over first-order intuitionistic logic. A key feature of our calculus is an explicit eigenvariable context, which allows us to control precisely the scope of free variables in a polytree structure. Semantically this context can be seen as encoding a notion of Scott's existence predicate for intuitionistic logic. This turns out to be crucial to avoid the collapse of domains and to prove the completeness of our proof system. The explicit consideration of the variable context in a formula sheds light on a previously overlooked dependency between the residuation principle and the existence predicate in the first-order setting, that may help explain the difficulty in obtaining a complete proof system for first-order bi-intuitionistic logic.

翻译：众所周知，在一阶直观逻辑的希尔伯特公理系统中引入与蕴涵对偶的排斥算子会导致模型中的论域坍缩为常域。这使得为非连续域的一阶双直观逻辑构建同时满足可靠性和完全性的证明系统成为极具挑战性的问题——该系统还需保持对一阶直观逻辑的保守性。本文通过提出首个适用于增长域一阶双直观逻辑的可靠且完全证明系统解决了该问题。我们将该证明系统形式化为带标签的多树矢列演算（嵌套矢列的符号变体），并证明其具有切割消去性质且对一阶直观逻辑保持保守性。该演算的核心特征在于显式的本征变量上下文，这使得我们能在多树结构中精确控制自由变量的作用域。从语义角度看，该上下文可被理解为对直观逻辑中斯科特存在谓词概念的编码。这一设计对于避免论域坍缩及证明系统的完全性至关重要。对公式中变量上下文的显式考量揭示了一阶框架下残差原理与存在谓词之间此前被忽视的依存关系，这或许能解释为何构建一阶双直观逻辑的完全证明系统长期存在困难。