Skip to Main content Skip to Navigation
Conference papers

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

Abstract : 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
Document type :
Conference papers
Complete list of metadata
Contributor : Jean Goubault-Larrecq <>
Submitted on : Tuesday, April 27, 2021 - 11:08:18 AM
Last modification on : Thursday, April 29, 2021 - 3:10:24 AM


Files produced by the author(s)


  • HAL Id : hal-03208846, version 1



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⟩



Record views


Files downloads