On duality and model theory for polyadic spaces

This paper is a study of first-order coherent logic from the point of view of duality and categorical logic. We prove a duality theorem between coherent hyperdoctrines and open polyadic Priestley spaces, which we subsequently apply to prove completeness, omitting types, and Craig interpolation theorems for coherent or intuitionistic logic. Our approach emphasizes the role of interpolation and openness properties, and allows for a modular, syntax-free treatment of these model-theoretic results. As further applications of the same method, we prove completeness theorems for constant domain and Godel-Dummett intuitionistic predicate logics. (c) 2023 Elsevier B.V. All rights reserved.

Automated summary

This paper studies first-order coherent logic from the perspective of duality and categorical logic. It proves a duality theorem between coherent hyperdoctrines and open polyadic Priestley spaces, which is subsequently used to prove completeness, omitting types, and Craig interpolation theorems for coherent or intuitionistic logic. The approach emphasizes the importance of interpolation and openness properties and allows for a modular, syntax-free treatment of these model-theoretic results.