×

Il forcing come principio logico per la costruzione dei fasci. I. (English) Zbl 0431.03024

En se servant des objets d’un site \( C \) comme ensemble de conditions, on definit une notion de ”forcing” pour les formules d’un langage multisorte L. Ceci fournit une interprétation de \( I \) dans le topos associé à \( C \) qui vérifie les clauses inductives de la sémantique de Kripke-Joyal. On reussit ainsi, en utilisant des techniques essentiellement logiques, à établir quelques théorèmes fondamentaux de la théorie des topos de Grothendieck, notamment le fait que tout topos de Grothendieck forme un topos élémentaire au sens de Lawvere-Tierney et le theorème du faisceau associé.

MSC:

03C90 Nonclassical models (Boolean-valued, sheaf, etc.)
18B25 Topoi
03C25 Model-theoretic forcing
03G30 Categorical logic, topoi