Saturated models of intuitionistic theories (Q1887664): Difference between revisions

The paper sets out to construct models of intuitionistic first-order theories that realize an arbitrary family of formulae if every finite subset is realized. Hence such models can be construed as \textit{saturated} models of intuitionistic theories. The language used is that of categorical logic and the saturated models lie in Grothendieck toposes (this would also work for Kripke or Heyting-valued models). An application to classical logic is to show that infinitary first-order logic with complete distributivity and a saturation rule is conservative over finitary first-order logic. The main technique is the study of the filter construction on small categories with finite limits, the completion of subobject lattices under filtered meets. The construction restricts well to regular and coherent categories, giving for coherent categories filtered meet coherent categories. Then coherent filter logic is introduced via sequents, and moreover coherent logic with an additional rule for infinitary meets and two rules saying that binary disjunctions and existential quantification both distribute over filtered meets. For a coherent theory \textbf{T} identified with its classifying coherent category \(\Phi\)(\textbf{T}) -- \(\Phi\) being the contravariant embedding from small coherent categories \(\mathcal Coh\) into \(\mathcal Top^{\text{op}}\) of the opposite of Grothendieck toposes -- the topos \(\Phi\)(\textbf{T}) contains a saturated model of \textbf{T}. This goes through also for Heyting categories (not the restriction of the filter construction). An example studied is the saturated model of Heyting arithmetic (HA) in \(\Phi\)(HA). Finally, a different construction of saturated models of intuitionistic first-order theories is given which produces models with stronger infinitary theories. If the first-order theory satisfies classical \textit{tertium non datur}, this gives a Boolean topos which contains a conservative saturated model of the theory, proving the conservativity result for classical logic.