Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents

Tim LyonTim Lyon, Ian ShillitoIan Shillito, Alwen TiuAlwen Tiu

Tim Lyon, Ian Shillito, Alwen Tiu
Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents
In Jörg Endrullis, Sylvain Schmitz, eds., Proceedings of the 33rd EACSL Annual Conference on Computer Science Logic 2025, volume 326 of LIPIcs, to appear. Schloss Dagstuhl - Leibniz-Zentrum für Informatik

Details
Bibtex

KurzfassungAbstract
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 an interesting 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 as a 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.
Weitere Informationen unter:Further Information: Link
Projekt:Project: DeciGUT
Forschungsgruppe:Research Group: Computational LogicComputational Logic

@inproceedings{LST2025,
  author    = {Tim Lyon and Ian Shillito and Alwen Tiu},
  title     = {Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic
               Investigation via Polytree Sequents},
  editor    = {J{\"{o}}rg Endrullis and Sylvain Schmitz},
  booktitle = {Proceedings of the 33rd {EACSL} Annual Conference on Computer
               Science Logic 2025},
  series    = {LIPIcs},
  volume    = {326},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year      = {2025}
}