Séminaire,
12 mars 2015
Giulio Guerrieri (Université Paris Diderot), Injectivity of relational semantics for connected MELL proof-structures via Taylor expansion
Programme
- 12 mars 2015, 15:30 - 16:30
Résumé
We show that:
(1) the Taylor expansion of a cut-free MELL proof-structure R with atomic axioms is the (most informative part of the) relational semantics of R;
(2) every box-connected MELL proof-structure is uniquely determined by the element of order 2 of its Taylor expansion;
(3) the relational semantics is injective for box-connected MELL proof-structures.
We point out that our notion of box-connection is rather general: all ACC or connected proof-structures are box-connected (the converse does not hold).
This is joint work with Lorenzo Tortora de Falco. Our results are deeply related to a previous work of Lorenzo Tortora de Falco and Daniel de Carvalho, but is based on a slightly different viewpoint.