Conceptual completeness for first-order intuitionistic logic: An application of categorical logic (Q1115868)

This paper deals with first order theories in intuitionistic logic and their models. A notion of an interpretation I: \({\mathcal T}\to {\mathcal T}'\) is presented, where \({\mathcal T}\) and \({\mathcal T}'\) are first order theories, and the main result states that if I induces an equivalence between \({\mathcal T}'\)-models and \({\mathcal T}\)-models, then I is an equivalence, i.e. there exists an interpretation J: \({\mathcal T}'\to {\mathcal T}\) with \(I\circ J\) and \(J\circ I\) the appropriate identity interpretations. In fact, a stronger result is proved characterizing when \({\mathcal T}'\) is a quotient theory of \({\mathcal T}\). The approach is via categorical logic, as categories and functors replace theories and models and the author very carefully develops the necessary background making the article as self-contained as is reasonable. This greatly enhances the readability and accessibility of the work. The first section of the paper describes the categorical notion of a logos as the framework for studying theories. A category \({\mathcal C}\) is a logos if it has finite limits, the set of subobjects of each object \(X\in {\mathcal C}\), \(Sub_ X({\mathcal C})\), has finite joins, the map \(f^{-1}: Sub_ Y({\mathcal C})\to Sub_ X({\mathcal C})\) of pulling back along a morphism f: \(X\to Y\) in \({\mathcal C}\) has left and right adjoints \(\exists f\) and \(\forall f\) (existential and universal quantification) and \(\exists\) satisfies the so-called Beck-Chevalley condition for pullbacks. If in addition \({\mathcal C}\) has finite disjoint coproducts and effective coequalizers of equivalence relations, then it is called a Heyting pretopos. Every theory has a classifying Heyting pretopos and an interpretation \({\mathcal T}\to {\mathcal T}'\) of theories is defined as a \({\mathcal T}\)-model in the classifying Heyting pretopos of \({\mathcal T}'\). The desired theorems are proved in the context of Heyting pretoposes, using various properties of geometric morphisms of Grothendieck toposes. These necessary properties are developed in the text, as is the ``topos of filters'' construction introduced by the author in J. Pure Appl. Algebra 29, 313-326 (1983; Zbl 0521.03051), which plays a key role in proving the main theorems.