Giulio Guerrieri (Université Paris Diderot), Injectivity of relational semantics for connected MELL proof-structures via Taylor expansion

Programme

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.