Order-theoretic, geometric and combinatorial models of intuitionistic S4 proofs

Jean Goubault-Larrecq (1, 2) , Eric Goubault (3, 4)

1 COQ - Formal Specifications and Program Validation
2 GIE Dyade
3 CEA - CEA- Saclay
4 DACLE-LETI - Département d'Architectures, Conception et Logiciels Embarqués-LETI

We propose a few models of proof terms for the intuitionistic modal propositional logic S4. Some of them are based on partial orders, or cpos, or dcpos, some of them on a suitable category of topological spaces and continuous maps. A structure that emerges from these interpretations is that of augmented simplicial sets. This leads to so-called combinatorial models, where simplices play an important role: the point is that the simplicial structure interprets the 2 modality, and that the category of augmented simplicial sets is itself already a model of intuitionistic propositional S4 proof terms. In fact, this category is an elementary topos, and is therefore a prime candidate to interpret all proof terms for intuitionistic S4 set theory. Finally, we suggest that geometric-like realizations functors provide a recipe to build other models of intuitionistic propositional S4 proof terms

Domaines: Logique en informatique [cs.LO]

Jean Goubault-Larrecq, Eric Goubault. Order-theoretic, geometric and combinatorial models of intuitionistic S4 proofs. IMLA 1999 - 1st Workshop on Intuitionistic Modal Logics and Applications, Jul 1999, Trento, Italy. ⟨hal-03208846⟩