Jean-Yves Girard, " La syntaxe transcendantale " à Nantes

Le premier séminaire du LINA aura lieu le jeudi 18 octobre 2012.
*Jean-Yves Girard*, Directeur de Recherche CNRS, Institut de Mathématiques
de Luminy nous parlera de logique et de preuves.

Venez nombreux, le sujet nous concerne tous et les exposés de Jean-Yves
sont toujours une grande source d'inspiration.

*Titre* : "La syntaxe transcendantale"

*Date et heure* : *jeudi 18 octobre, 14h - 15h30*

*Lieu* : bâtiment LINA de la fac de science (salle 3)

*Résumé *:
Autrement dit, les conditions de possibilité du langage logique, en
particulier de la démonstration et du typage, notions à peu près
isomorphes. On peut voir un type comme une essence, une espèce de surmoi
régulant le "ça" de l’existence pure. Mais les conditions transcendantales
du typage sont contradictoires, car l’exigence de finitude est incompatible
avec celle d’une certitude irréfragable (l’apodictique) : cette dernière
demanderait un fondement contradictoire, alors que la finitude s’oppose à
l’équilibre parfait entre un type et sa négation, i.e., entre introductions
et éliminations, entre création et utilisation. On observe ainsi un déficit
de compositionalité, autrement dit de cohérence (au sens le plus large du
terme) : problèmes avec le Modus Ponens, i.e., avec l’élimination des
coupures. Ce qui se traduit par un phénomène bien connu, l’incomplétude.

Si l’apodictique n’est pas de ce monde, la finitude l’est : un bon siècle
d’expériences formelles permet de dégager des principes plausibles, i.e.,
des protocoles supposés relier un type à sa négation ; ces protocoles sont
forcément incomplets et peut-être faux, d’où leur dimension pragmatique :
ils n’ont qu’une valeur relative. Pas tout à fait relative, puisque
subsiste une vraie certitude, et la seule possible : celle, toute
formaliste, d’avoir suivi les protocoles, d’avoir obéi à la loi.