Par où commencer pour comprendre les travaux de Jean-Yves Girard ?

Entrain_

Bonjour à tous et à toutes, 

Je suis philosophe de formation et je me suis remis depuis quelques temps aux mathématiques. J'ai pu bénéficier d'une modeste formation en logique – j'ai eu une petite introduction pour philosophes (la technique restait très légère) en de théorie des modèles, de la démonstration et des ensembles. J'ai toujours eu le désir de comprendre plus en profondeur la logique mathématique (spécifiquement la théorie de la démonstration). À ce titre, cela fait quelques années que je lis les articles de Jean-Yves Girard. Pourquoi ? Parce que c'est un des seuls logiciens qui parle un peu des orientations philosophiques de son travail scientifique (même si je trouve que sur ce sujet de la philosophie, il peut écrire des bêtises). 

Je me suis vite rendu compte que si je me limitais à la couche philosophique des travaux de Girard (les articles non-techniques), je n'allais pas réellement comprendre ce qu'il essaye de faire en théorie de la démonstration. Le problème est que je n'ai tout simplement pas le bagage mathématique pour comprendre ses articles techniques. Je me suis dit alors qu'il fallait tout simplement que je me mette à la logique, et, plus spécifiquement, à la théorie de la démonstration.
D'où ma question : dans l'objectif de comprendre (à moyen/long terme) les réseaux de démonstration,  la logique linéaire, la ludique puis la syntaxe transcendantale, par quels ouvrages puis-je commencer ? 

J'en ai principalement deux en têtes : le Cori&Lascar (Logique mathématique) et le David&Nour&Raffalli (Introduction à la logique). Pensez-vous que ce soit un bon choix ? D'autres ouvrages à me conseiller ? 

Bien à vous, 


PS : S'il y a des connaisseurs des travaux de Girard : quel est l'enjeu pratique ou théorique d'avoir une nouvelle définition de la vérité (par exemple celle défendue dans cet article :  https://girard.perso.math.cnrs.fr/wo.pdf ) qui sorte de la conception tarskiste ? J'avais un jour posé cette question maladroitement à Girard, qui m'a répondu en substance qu'il s'en foutait que cela ait des implications ou non pour les mathématiques (ce n'était pas ce qu'il recherchait de toute manière). C'était maladroit car évidemment, un scientifique n'a généralement pas de justifications pratiques de ses découvertes théoriques (c'est généralement l'inverse : après la découverte théorique on découvre des applications et des implications inattendues).

Foys

L'article sur la logique linéaire (du même auteur) est assez clair je trouve. https://girard.perso.math.cnrs.fr/Synsem.pdf

Entrain_

@Foys Je ne connaissais pas cet article. Merci pour la référence, il est en effet clair. Cela dit, il date d'un moment où Girard n'avait pas encore débuté le projet de la syntaxe transcendantal.