1 = ⊥ in MLL
Date(s) : 02/07/2026 iCal
11h00 - 12h30
The introduction of units in multiplicative linear logic (MLL) makes syntactic properties much more complex, in particular regarding the question of identity of proofs and thus of proof nets. Starting from the well known relation between the axioms 1 ⊢ ⊥ and ⊥ ⊢ 1 and the mix rules, we study which equivalence on sequent-calculus proofs provides a syntactic isomorphism 1 ≃ ⊥. This leads to the introduction of MLLM, a variant of MLL with a self dual unit identifying 1 and ⊥.
Moving to the categorical side of the Curry-Howard-Lambek correspondence, we give a semantic counterpart of the previous syntactic construction in symmetric monoidal closed and *-autonomous categories.
Emplacement
I2M Luminy - TPR2, Salle de Séminaire 304-306 (3ème étage)
Catégories
