# Syntaxe transcendantale

En logique mathématique et en théorie de la démonstration, la syntaxe transcendantale est une conception de la logique proposée par le logicien Jean-Yves Girard dans une série d'articles$^,$$^,$$^,$ qui s'inscrit dans la continuité de ses précédents travaux sur la géométrie de l'interaction (en) et la ludique (en).
L'expression "syntaxe transcendantale" est une référence directe au transcendantal d'Emmanuel Kant.

## Contexte

À la suite de ses recherches sur la logique linéaire à la fin des années 1980, Girard a développé une nouvelle représentation dite "parallèle" des preuves mathématiques qu'il nomme réseau de preuve. En cherchant à caractériser mathématiquement les réseaux de preuve, il développe quelques années plus tard son programme de "géométrie de l'interaction" en 6 articles$^,$$^,$$^,$$^,$$^,$. Dans ces articles, les preuves sont représentées par des objets mathématiques interactifs (des permutations sur les entiers munis d'une opération d'interaction dans le cas le plus simple) avec lesquels on essaie de reconstruire la notion de preuve puis de formule (en particulier en logique linéaire). Ce sont en fait les prémisses de la syntaxe transcendantale (que l'on pourrait dater autour de 2013) : le sixième article de géométrie de l'interaction est en effet intitulé "Geometry of Interaction VI : a blueprint for Transcendental Syntax".
C'est dans ce contexte que Girard reformule et étend ses derniers travaux sous le titre de "syntaxe transcendantale" en y ajoutant une dimension philosophique. En particulier, par rapport à la géométrie de l'interaction qui manipule des objets complexes (issus des algèbres d'opérateurs) et infinis, la syntaxe transcendantale se recentre sur la finitude et la simplicité des objets : le modèle de calcul de constellations utilisé dans la syntaxe transcendantale se base sur l'unification de termes, un mécanisme déjà bien connu et utilisé en logique et en informatique théorique.

## Concepts clés
### Point aveugle et anti-transparentisme

Dans son livre Le Point Aveugle, Girard dénonce un scientisme qui serait présent dans le domaine de la logique et qui produirait de mauvais fondements pour la logique.
   "Le point aveugle c'est ce qu'on (qui) ne voit pas et on ne sait même pas qu'on ne le voit pas."
   (Le Point Aveugle, avant-propos)
Plus tard, dans son livre Le fantôme de la transparence, il développe ces idées et se focalise sur l'idée de "transparentisme" :
   "L'expérience de la connaissance nous enseigne qu'il n'y a pas de Réalité Dernière, que tout train en cache un autre. Une évidence qu'il n'est pas facile d'accepter, d'où l'idée de ce train ultime, celui qui ne cacherait plus rien. Le transparentisme postule l'existence, au-delà de la perception immédiate, d'un monde, d'un niveau de lecture, complètement intelligible, i.e., explicite et immédiat. D'où cette croyance en de prétendus "rayons X du savoir" qui nous dévoileraient l'envers de l'Univers."
   (Le fantôme de la transparence, quatrième de couverture)

### Monisme et justifications internes

Les phénomènes de logique mathématique sont habituellement expliqués et ordonnés par des moyens sémantiques externes évaluant une syntaxe. Il y a donc une dualité entre la syntaxe et la sémantique. Il s'agit d'une approche dualiste. En opposition à cela, la syntaxe transcendantale propose une approche moniste afin d'arriver à une justification interne de la logique où la syntaxe fait office de sémantique et substitue la notion de modèle en théorie des modèles. La logique ne serait alors expliquée que par des phénomènes observables dans l'interaction syntaxique, desquels émergent le sens logique.

### Morphologisme

L'idée de "morphologisme" a été introduite par Girard dans son article (non publié) Logique 2.0. Il s'agit d'une approche pour justifier la pertinence et l'effectivité de la logique formelle qui ne se focaliserait non plus sur des explications sémantiques ou évaluatives (jugées arbitraires) mais sur la forme (topologie, géométrie...) des objets observés.
   "C’est à partir de cette thèse morphologiste que nous serons amené à revoir les primitives logiques : peut-on les justifier du point de vue de la forme ?"
   (Logique 2.0)

## Architecture girardienne

Dans la syntaxe transcendantale, Girard propose une relecture de l'activité logique qu'il qualifie de kantienne . Cette relecture reprend la distinction entre type de jugement analytique et synthétique dans la théorie de la connaissance d'Emmanuel Kant en y intégrant la notion de calcul en informatique. Elle prend la forme d'un tableau de quatre cases censées structurer les conditions suffisantes d'émergence des concepts logiques (que Girard appelle conditions de possibilité du langage, toujours en référence à Kant bien qu'il s'agisse, chez Girard, de conditions suffisantes et non nécessaires). Cependant, contrairement à Kant, les termes d'analytique et de synthétique ne qualifient plus des jugements mais représentent des espaces d'entités.
Maillage "cognitif" de la syntaxe transcendantale :
| | Analytique / Brut / Réponses | Synthétique / Formaté / Questions |
| A posteriori / Explicite | Constat | Usine |
| A priori / Implicite | Performance | Usage |

### Analytique

L'analytique est un espace d'objets potentiellement sujets à un processus dynamique (performance) les menant à interagir entre eux pour arriver à une forme stable et terminée (constat). Il s'agit d'une transition de l'implicite (entité calculable) vers l'explicite (résultat). Il s'agit d'une généralisation des programmes informatiques mais Girard a plus particulièrement en tête un modèle de calcul d'objets appelés "étoiles et constellations" (plus tard appelé "résolution stellaire" par Eng en référence à la règle de résolution).
Ce qui lie la performance au constat est donc une forme d'exécution semblable à celle à l'œuvre en informatique, alors que ce qui les sépare serait, d'après Girard, l'indécidabilité que l'on pourrait interpréter comme l'impossibilité de réduire les programmes informatiques à leur résultat.
L'analytique est "brute" dans le sens où les objets ne sont pas teintés d'une quelconque signification. Les objets répondent à une dynamique et ont un certain comportement sans répondre à une intention (comme par exemple "calculer le résultat de l'opération 2+2" qui aurait pour réponse un programme donnant le résultat). En ce sens, on peut les voir comme des réponses en attente de questions, de la même manière que l'on pourrait prendre les mots "oui" et "non" indépendamment d'une question qui les contextualiserait.
Il doit être noté que l'espace analytique est choisi et non absolu. Il s'agit d'un ancrage syntaxique pour la logique qui influencera les propriétés et comportements que l'on peut exprimer. Plus les comportements possibles du modèle de calcul choisi sera riche, plus la logique qui en découlera sera expressive.

### Synthétique

Le synthétique est un espace d'objets porteurs de sens et d'intention décrivant des propriétés, spécifications ou encore contraintes sur l'espace analytique. Il s'agit des formules en logique mathématique ou, par la correspondance de Curry-Howard, des types en programmation que l'on peut voir comme des questions (par exemple, "quel est le résultat de l'opération 2+2 ?"). La particularité de la syntaxe transcendantale est que le synthétique est lui-même exprimé à partir des objets de l'analytique. La signification émerge du fait que la formation des objets du synthétique implique un choix arbitraire. Il existe deux notions de sens dans le synthétique : l'usine et l'usage.
Dans l'usage, le sens des objets est défini par interaction jugée correcte. Par exemple, pour savoir si un objet représente la fonction successeur $f(n)=n+1$, nous pourrions lui passer en argument l'encodage dans l'analytique de tous les entiers existants (servant de tests) et vérifier si l'on obtient bien le résultat attendu. Si c'est le cas, on pourra attacher à ce programme une étiquette de type certifiant qu'il s'agit d'une fonction successeur : c'est un sens qu'on lui donne. Cela correspond au "sens comme usage" de Wittgenstein.
L'usine se restreint à des ensemble de tests finis afin de garantir un test effectif et tractable. En effet, si l'on se contente de l'infinité de tests précédent, nous ne serions pas capable de dire qu'une fonction est une fonction successeur en un temps fini. Nous considérons donc que les étiquettes de spécification correspondent à des ensembles finis d'objets de l'analytique. Dans notre exemple précédent, cela correspondrait à connecter notre objet que l'on suspecte d'être une fonction successeur à un ensemble fini d'objets "exotiques" (qui ne sont pas des entiers) qui vérifieraient la structure de l'objet afin de déterminer qu'elle se comporte bien comme une fonction successeur (tout comme le feraient les règles de typage en théorie des types). À noter que cela n'est possible qu'à condition que l'espace analytique soit assez large, de la même manière que l'on étend l'ensemble des entiers réels aux nombres complexes afin de résoudre des équations comme $x^{2}=-1$ qui sont insolubles dans $\mathbb {R}$.
Usine et usage sont reliés par ce que Girard appelle l'adéquation qui exprime une pertinence de l'usine par rapport à l'usage : les tests (exprimés dans l'usine) que l'on effectue sur l'objet testé permettent bel et bien de garantir le comportement que nous visons (exprimé dans l'usage).

## Illustration

L'illustration intuitive proposée par Girard dans son livre Le fantôme de la transparence est celui d'une usine automobile. Les véhicules peuvent être vus comme des objets performatifs de l'espace analytique. Il est possible de les certifier avec une étiquette après leur avoir fait passer une batterie de tests d'usine garantissant leur bon fonctionnement. Cependant, ces tests (usine) sont nécessairement partiels : on ne peut pas tester toutes les possibilités (usage) et il ne serait pas raisonnable de faire rouler une voiture 30 000km afin de certifier qu'elle en est capable. Cependant, ces tests doivent être suffisants : il doit y avoir adéquation avec l'usage.

## Sujets ouverts

Dans ses derniers écrits sur la syntaxe transcendantale, Girard propose deux points de vue allant au-delà du tableau de "maillage cognitif" précédent.
La logique peut exister "sans système"$^,$ (dans le sens des systèmes logiques qui ferment le raisonnement à certaines règles et une certaine sémantique) si l'on se contente de l'analytique et du sémantique. Il qualifie cette approche d'apodictique ou de "logique du premier ordre" (à ne pas confondre avec le calcul des prédicats appelé de la même manière). En particulier, Girard propose une relecture de l'axiomatique de Peano qui serait sans axiomes, une chose possible puisque les axiomes sont définis comme des ensembles de tests à passer.
Cependant, bien qu'il ne s'est que peu penché sur le sujet, Girard s'est interrogé à ce qui fait l'émergence de la notion de système logique dans son nouveau cadre : c'est ce qu'il qualifie d'épidictique et qui concerne entre autres la logique du second ordre (avec en tête ses travaux sur Système F) ou encore la théorie des types dépendants. Il explore aussi des notions que l'on pourrait attribuer aux systèmes logiques comme la vérité, ce qui l'amène à des idées comme le déréalisme où des éléments de système logique seraient greffés aux objets de l'analytique (avec pour analogie des systèmes de voitures trafiqués afin de passer les tests d'usine).

## Travaux connexes

Le sujet a été commenté par V. Michele Abrusci et Paolo Pistone sur le plan philosophique. Et sur le plan technique, par la thèse de doctorat de Vincent Laurence Rouleau (pour un point de vue mathématique) et celle de Boris Eng (pour un point de vue informatique).
La syntaxe transcendantale faisait suite au programme de géométrie de l'interaction, des travaux proches se retrouvent chez Thomas Seiller qui utilise pour espace analytique des objets appelés graphes d'interaction et graphages. En restant dans la logique linéaire, Emmanuel Beffara utilise des calculs de processus comme le pi-calcul. Certains auteurs dans le domaine des relations logiques et de la réalisabilité classique ont des approches similaires avec le lambda-calcul, comme Colin Riba ou Jean-Louis Krivine.