-
Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents
Authors:
Tim S. Lyon,
Ian Shillito,
Alwen Tiu
Abstract:
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…
▽ More
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.
△ Less
Submitted 5 May, 2024; v1 submitted 24 April, 2024;
originally announced April 2024.
-
Mechanised uniform interpolation for modal logics K, GL, and iSL
Authors:
Hugo Férée,
Iris van der Giessen,
Sam van Gool,
Ian Shillito
Abstract:
The uniform interpolation property in a given logic can be understood as the definability of propositional quantifiers. We mechanise the computation of these quantifiers and prove correctness in the Coq proof assistant for three modal logics, namely: (1) the modal logic K, for which a pen-and-paper proof exists; (2) Gödel-Löb logic GL, for which our formalisation clarifies an important point in an…
▽ More
The uniform interpolation property in a given logic can be understood as the definability of propositional quantifiers. We mechanise the computation of these quantifiers and prove correctness in the Coq proof assistant for three modal logics, namely: (1) the modal logic K, for which a pen-and-paper proof exists; (2) Gödel-Löb logic GL, for which our formalisation clarifies an important point in an existing, but incomplete, sequent-style proof; and (3) intuitionistic strong Löb logic iSL, for which this is the first proof-theoretic construction of uniform interpolants. Our work also yields verified programs that allow one to compute the propositional quantifiers on any formula in this logic.
△ Less
Submitted 29 April, 2024; v1 submitted 16 February, 2024;
originally announced February 2024.
-
A new calculus for intuitionistic Strong Löb logic: strong termination and cut-elimination, formalised
Authors:
Ian Shillito,
Iris van der Giessen,
Rajeev Goré,
Rosalie Iemhoff
Abstract:
We provide a new sequent calculus that enjoys syntactic cut-elimination and strongly terminating backward proof search for the intuitionistic Strong Löb logic $\sf{iSL}$, an intuitionistic modal logic with a provability interpretation. A novel measure on sequents is used to prove both the termination of the naive backward proof search strategy, and the admissibility of cut in a syntactic and direc…
▽ More
We provide a new sequent calculus that enjoys syntactic cut-elimination and strongly terminating backward proof search for the intuitionistic Strong Löb logic $\sf{iSL}$, an intuitionistic modal logic with a provability interpretation. A novel measure on sequents is used to prove both the termination of the naive backward proof search strategy, and the admissibility of cut in a syntactic and direct way, leading to a straightforward cut-elimination procedure. All proofs have been formalised in the interactive theorem prover Coq.
△ Less
Submitted 1 September, 2023;
originally announced September 2023.
