Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents
arxiv(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要