Alexis Saurin
IRIF, Paris Cité
https://www.irif.fr/users/saurin/index
Date(s) : 28/03/2024 iCal
11 h 00 min - 12 h 30 min
In this talk, I will present a proof-relevant Craig-Lyndon interpolation theorem for first-order LL (linear logic). This interpolation result is proof-relevant in the following sense:
if π proves A ⊢ B and is cut-free, then we can find
(i) a formula C in the common vocabulary of A and B and
(ii) two proofs π1 and π2 of A ⊢ C and C ⊢ B respectively, such that Cut(π1,π2) reduces to π.
I will then show that the interpolation process can be regarded as a cut-introduction procedure, synthesizing the interpolation formula.
I will then discuss how this result follows in fact straightforwardly from the standard proof-theoretic method (Maehara’s method) used to prove interpolation in a number of sequent calculi. I will also discuss the computational interpretation of the result and in particular recall similar results discovered in the early nineties by Cubric, a student of Michael Makkai, without receiving significant attention.
Then, depending on time and interest of the audience, I will possibly discuss
(i) similar proof-relevant interpolation results for intuitionistic and classical logics (ii) how to extend the above result to (a fragment of) circular proofs of linear logic with least and greatest fixed-points and/or
(iii) a proof-net reformulation of the above results.
Emplacement
Site Sud, Luminy, TPR2, Salle de Séminaire 304-306 (3ème étage)
Catégories