Loyalty and Faithfulness of Model Constructions for Constructive Set Theory
Robert Paßmann
Abstract:
Model constructions for intuitionistic and constructive set theories, such as CZF or IZF, are commonly built upon Kripke- or Heyting-semantics for intuitionistic logic. We discuss how much of the logical structure of the underlying Kripke frame or Heyting algebra can be recovered from within the set-theoretical model construction.
We will use Heyting structures (introduced by Fourman and Scott in the 1970s) to develop a framework that allows us to compare the propositional logics of classes of models with the propositional logics of the classes of their underlying Heyting algebras (resp., Kripke frames): A class of models will be called faithful if any valuation on an underlying Heyting algebra can be imitated by a collection of sentences in a model of that class. We will call it loyal if it has the same logic as the underlying class of Heyting algebras and connect these two notions to the de Jongh property.
The main part of the thesis deals with an analysis of different model constructions by Iemhoff, Lubarsky, and the well-known Heyting-valued and Boolean-valued models for set theory. It turns out that the class of Iemhoff models is loyal and faithful to a very high degree. The class of full Lubarsky models is not faithful to its underlying Kripke frames, and the class of Lubarsky models based on a finite Kripke frame is not loyal as its propositional logic contains the principle of weak excluded middle despite the fact that this principle is not valid in the class of finite Kripke frames. A representation theorem allows us to transfer this result to the class of Heyting-valued models based on a finite Heyting algebra. We will conclude with an analysis of the propositional logics of Boolean-valued and Heyting-valued models for set theory.