A note on intuitionistic models of ${\rm ZF}$.
Ren� Lavendhomme, T. Lucas · Notre Dame Journal of Formal Logic · 1983
An analysis of the forcing construction of models of ZF by means of intuitionistic logic and Kripke semantics (or sheaf semantics) has been made by many authors (see for example [ 1 ], [2], [5]).We feel however that some basic information is still available from this approach, the motto of which could be "think of a sheaf of structures as a structure, using intuitionistic logic".In this note, we are not really interested in obtaining independence results, but want to sketch a set-theoretic forcing along lines which closely agree with that motto.In usual forcing constructions, there are two sheaf structures: peC , and passing from the first to the second is nothing else than a sheaf-version of the extensionalization of a binary relation.This is discussed in Section 2 for Kripke-structures but the proofs are designed so as to immediately extend to sheaf structures as is indicated in Section 4. Application to the construction of models of ZF is given in Section 3. To this we add definitions and notions which bring the construction closer to the classical construction of inner models of ZF and, as a "test-case", indicate how to adapt the well-known proof of relative consistency oϊVΦL.Roughly speaking, we may distinguish between two approaches to forcing.In the first, the model, be it Boolean-valued or intuitionistic, is constructed from the base model Masa union of a sequence of M a indexed by ordinals of M ([1], [2], [4], [5]).In the second, no hierarchy is present, at least to begin with, and the hierarchy effect remains concentrated in the various forms of induction [7].Our approach is of the second kind and may be viewed as an intuitionistic version of [7], whereas [2] for example is an intuitionistic construction of the first kind.In fact, this distinction is not so clear-cut and the