Ultrafilter Extensions for Veltman Semantics
Felix Frigola Gonzalez, Joost J. Joosten, Vicent Navarro Arroyo, Cosimo Perini Brogi

TL;DR
This paper introduces ultrafilter extensions for interpretability logic, addressing a long-standing open problem by developing algebraic tools and demonstrating their key properties, despite the frame condition being non-modally definable.
Contribution
It presents the first first-order frame condition for interpretability logic that is not modally definable and develops ultrafilter extensions to analyze such conditions.
Findings
Frame condition holds on ILM and ILP frames.
Ultrafilter extensions are successfully developed for interpretability logic.
Algebraic tools for ultrafilter extensions are established.
Abstract
In this paper, we present a first-order frame condition for interpretability logic and show that the condition is not modally definable. Yet, the frame-condition holds both on ILM and on ILP frames and, hence, is of potential importance for the long-standing open problem about the interpretability logic of all reasonable arithmetical theories. In the light of the Goldblatt-Thomason Theorem, the modally inexpressible frame condition serves as motivation to develop ultrafilter extensions for inter pretability logic. We develop the necessary algebraic tools to define these ultrafilter extensions and prove the main properties about both the tools and the ultrafilter extensions.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Formal Methods in Verification · Logic, programming, and type systems
