3 ms·

This is an implementation of Girard's "transcendental syntax" program which aims to give foundations to logic that do not rely on axiomatics and a form of tarsk

This is an implementation of Girard's "transcendental syntax" program which aims to give foundations to logic that do not rely on axiomatics and a form of tarskian semantics (tarskian semantics is the idea that "A & B" is true means that "A" and "B" is true; you've simply changed the and to a "meta" one rather than the logical one). This program is more than 10 years old, with first written versions appearing around 2016, and the ideas appearing in his talks before that. Girard has been a vocal critic of foundational problems, labeling them as "hell levels", with the typical approach of set theory and tarskian semantics as the lowest one and category theory as a "less worse" one (at least one level above). One issue with his program is that he mixes abstract, philosophical ideas with technical ones. So even if some things have interesting technical applications, they may be different when seen from a more philosophical point of view. For instance, set theory as the foundations of mathematics is a pretty solid model but it is seen as fundamentally unsatisfying for many reasons -- most famously the continuous hypothesis. Gödel and other very high-profile mathematicians thought it was a very unsatisfying issue even though from a mathematical model theory point of view, it's not even a paradox. So the new foundational approaches tend to have maybe deeper philosophical problems about them; for example see Jacob Lurie's critic of the Univalent foundations program (after the "No comment" meme he expressed a long list of issues with it). The other issue with this particular work is that it uses new vocabulary for everything to avoid the bagage of usual mathematical logic, but it kind of give a weird vibe to the work and make it hard to get into without dedicating much work. The result is therefore something that is supposed to solve many longstanding problems in philosophical and technical approaches to the foundations of mathematics but has not had a big impact on the community. This is not too surprising either because the lambda calculus or other logical works were seen as trivial mathematical games. We'll see if it's a case of it being too novel to be appreciated fully, and this work seems to try to explore it in a technical way to answer this question. https://girard.perso.math.cnrs.fr/Logique.html https://girard.perso.math.cnrs.fr/Logique.html (in French, it gives an overview of the program) https://girard.perso.math.cnrs.fr/Archives.html https://girard.perso.math.cnrs.fr/Archives.html (transcendental syntax papers are there in English)

Tainnor 2y ago
I tried looking into the Transcendental Syntax I paper. It starts with > We study logic in the light of the Kantian distinction between analytic (untyped, meaningless, locative) answers and synthetic (typed, meaningful, spiritual) questions. Which is specially relevant to proof-theory: in a proof-net, the upper part is locative, whereas the lower part is spititual: a posteriori (explicit) as far as correctness is concerned, a priori (implicit) for questions dealing with consequence, typically cut-elimination. The divides locative/spiritual and explicit/implicit give rise to four blocks which are enough to explain the whole logical activity. Honestly, this and the rest of the paper read like a caricature of (a particularly grumpy) continental philosopher. I suspect many mathematicians don't engage with this because they are drawn to precision. From what I read (and from your comment), I have no idea what this program really is about. Maybe there's something of value in there but it seems really hard to tell.
- saithound 2y ago
  Girard is one of the top logicians of his time. He can write standard mathematical prose when he wants to. In turn, when he chooses to use the continental philosophy style, it's a deliberate choice: people who can't read it are not in the target audience anyway. Somebody who worked through the two volumes of "Proof Theory and Logical Complexity", and worked through the later chapters of "The Blind Spot" will already be used to the style, so won't find it an obstacle when reading the Transcendental Syntax papers. And those who didn't read these works? Well, they don't know the prerequisites anyway (the author assumes), so making the style more palatable to them is not a priority. The aforementioned works are better starting points: they cover classical proof theory, so there are many other textbooks that can be consulted while the reader develops familiarity with Girard's style. And one needs to know the material to understand Transcendental Syntax anyway.
  - Tainnor 2y ago
    Yeah, after doing some research I realised that he isn't some crank and actually has done a lot of relevant work in logic. I still don't think that justifies writing in a deliberately obtuse style, but I guess he can do whatever he wants.

Tainnor 2y ago

I tried looking into the Transcendental Syntax I paper. It starts with > We study logic in the light of the Kantian distinction between analytic (untyped, meaningless, locative) answers and synthetic (typed, meaningful, spiritual) questions. Which is specially relevant to proof-theory: in a proof-net, the upper part is locative, whereas the lower part is spititual: a posteriori (explicit) as far as correctness is concerned, a priori (implicit) for questions dealing with consequence, typically cut-elimination. The divides locative/spiritual and explicit/implicit give rise to four blocks which are enough to explain the whole logical activity. Honestly, this and the rest of the paper read like a caricature of (a particularly grumpy) continental philosopher. I suspect many mathematicians don't engage with this because they are drawn to precision. From what I read (and from your comment), I have no idea what this program really is about. Maybe there's something of value in there but it seems really hard to tell.

saithound 2y ago
Girard is one of the top logicians of his time. He can write standard mathematical prose when he wants to. In turn, when he chooses to use the continental philosophy style, it's a deliberate choice: people who can't read it are not in the target audience anyway. Somebody who worked through the two volumes of "Proof Theory and Logical Complexity", and worked through the later chapters of "The Blind Spot" will already be used to the style, so won't find it an obstacle when reading the Transcendental Syntax papers. And those who didn't read these works? Well, they don't know the prerequisites anyway (the author assumes), so making the style more palatable to them is not a priority. The aforementioned works are better starting points: they cover classical proof theory, so there are many other textbooks that can be consulted while the reader develops familiarity with Girard's style. And one needs to know the material to understand Transcendental Syntax anyway.
- Tainnor 2y ago
  Yeah, after doing some research I realised that he isn't some crank and actually has done a lot of relevant work in logic. I still don't think that justifies writing in a deliberately obtuse style, but I guess he can do whatever he wants.