Geodesic
On the geometry of intuitionistic S4 proofs
Homology, homotopy, and applications, Tome 5 (2003) no. 2, pp. 137-209.

Voir la notice de l'article provenant de la source International Press of Boston

The Curry-Howard correspondence between formulas and types, proofs and programs, proof simplification and program execution, also holds for intuitionistic modal logic S4. It turns out that the S4 modalities translate as a monoidal comonad on the space of proofs, giving rise to a canonical augmented simplicial structure. We study the geometry of these augmented simplicial sets, showing that each type gives rise to an augmented simplicial set which is a disjoint sum of nerves of finite lattices of points, plus isolated $(-1)$-dimensional subcomplexes. As an application, we give semantics of modal proofs (a.k.a., programs) in categories of augmented simplicial sets and of topological spaces, and prove a completeness result in the style of Friedman: if any two proofs have the same denotations in each augmented simplicial model, then they are convertible. This result rests both on the fine geometric structure of the constructed spaces of proofs and on properties of subscone categories—the categorical generalization of the notion of logical relations used in lambda-calculus.
DOI : 10.4310/HHA.2003.v5.n2.a6
Classification : 03B45, 03B70, 18A25, 18C15, 18C50, 18D15, 18F20, 18G10, 55U10, 68N18, 68Q55
Keywords: comonads, completeness, Curry-Howard correspondence, distributivity laws (for comonads), intuitionistic logic, lambda-calculus, logical relations, modal logic, presheaves, resolution functors, S4, simplicial sets, subscones 
@article{HHA_2003_5_2_a7,
     author = {\'Eric Goubault and Jean Goubault-Larrecq},
     title = {On the geometry of intuitionistic {S4} proofs},
     journal = {Homology, homotopy, and applications},
     pages = {137--209},
     publisher = {mathdoc},
     volume = {5},
     number = {2},
     year = {2003},
     doi = {10.4310/HHA.2003.v5.n2.a6},
     language = {en},
     url = {http://geodesic.mathdoc.fr/articles/10.4310/HHA.2003.v5.n2.a6/}
}
TY  - JOUR
AU  - Éric Goubault
AU  - Jean Goubault-Larrecq
TI  - On the geometry of intuitionistic S4 proofs
JO  - Homology, homotopy, and applications
PY  - 2003
SP  - 137
EP  - 209
VL  - 5
IS  - 2
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/articles/10.4310/HHA.2003.v5.n2.a6/
DO  - 10.4310/HHA.2003.v5.n2.a6
LA  - en
ID  - HHA_2003_5_2_a7
ER  - 
%0 Journal Article
%A Éric Goubault
%A Jean Goubault-Larrecq
%T On the geometry of intuitionistic S4 proofs
%J Homology, homotopy, and applications
%D 2003
%P 137-209
%V 5
%N 2
%I mathdoc
%U http://geodesic.mathdoc.fr/articles/10.4310/HHA.2003.v5.n2.a6/
%R 10.4310/HHA.2003.v5.n2.a6
%G en
%F HHA_2003_5_2_a7
Éric Goubault; Jean Goubault-Larrecq. On the geometry of intuitionistic S4 proofs. Homology, homotopy, and applications, Tome 5 (2003) no. 2, pp. 137-209. doi : 10.4310/HHA.2003.v5.n2.a6. http://geodesic.mathdoc.fr/articles/10.4310/HHA.2003.v5.n2.a6/

Cité par Sources :