I'm the author of this repository. I just want to point out that it was an experiment / proof-of-concept for the ideas of Girard's transcendental syntax (I didn't even expect it would be posted somewhere outside of my small circle of collaborators -- that's why the "guide" is written in French). You could call it an "esoteric programming language" at this point if you want. I wanted to have fun while working on ideas I'm passionate about but also to build something people interested in Girard's works could play with. So it's not ready to convince anyone of its relevance yet. It wasn't even meant to be a programming language at first.
Girard's ideas are indeed cryptic and may sound like a caricature of (a particularly grumpy) continental philosopher. One of my goals is to make these ideas more understandable and more down-to-earth, to show that they can be illustrated in a toy programming language. But there's a still a lot of work to be done (way more than what you could imagine just from reading Girard's papers). Although I studied Girard's last works for 4 years, I'm still far from understanding all its consequences. That's because it is related to pretty much everything in logic and computation (what is a type/formula/specification, how do you know whether an object is of some type, what is a proof, what is meaning, what is a system, what are logical rules, what all models of computation have in common, what all logical systems have in common, what is a program, what is an algorithm).
The idea is to go beyond the current proof-as-program correspondence (on which proof assistants like Coq are based). After its analysis of the notion of proof, Girard wanted a computational space in which elements would be able to "test themselves", without relying on some "hard-coded" semantics. In programming terms, it would correspond to the ability to build types from programs. There is no primitive types, not even the arrow type of functional programming. We just have Prolog-like bricks of terms which can interact with each other. They can express programs or tests for programs. You build everything with that like how you do chemical experiments.
To give a probably familiar illustration, I'm often asked whether we could "do transcendental syntax" with the untyped lambda-calculus. It would be possible if for any type T you could find a finite set of lambda-terms acting as "tests" such that interaction with it ensures being of type T. The space of lambda-terms is not "large enough / flexible" for that. You need to introduce exotic objects like how you extend the set of rationals Q to the real numbers R to solve more equations. You can also think of how to tell whether a finite automaton recognizes some (infinite) rational language without relying on an external semantics. You only have input words and infinite testing by feeding it all words of the language. But yet, we are able to do it with an external semantics. So the question is how you internalize semantics in the object language.
If there's anyone who has any inspirations or insights, I'm open and interested. The right path to follow is still undefined. I just have some tools coming from my understanding of Girard's works.
idlewords 4 days ago [-]
This is so French that a baguette appeared in my hand after I clicked the theory link. Probably a cognitive hazard to anyone who is really into generics.
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.
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 3 days 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 3 days 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.
woolion 2 days ago [-]
His books "the blind spot - a course in logic" is despite its title a bad offender in mixing fairly outrageous claims and philosophical rants with technical statements; and it is one of his most accessible texts. His writing is deliberately off-putting and hard to read; you actually need to already understand his ideas to understand his writing.
His main contribution, through linear logic, are ways to separate 'elementary' operations of logic into simpler ones. Linear logic decomposes the classical "and" and "or" into multiplicative and additive ones, and some modalities. This gives a more precise encoding of operations that can directly link logic to complexity theory, and have interesting applications to compiler design.
Note that academia has been very receptive of his technical achievement, the proof of consistency of System F through reducibility candidates, but much less welcoming of some of his other papers that he deemed way more interesting (as we saw recently with Terence Tao "I got a paper rejected today"). I think him writing this way is a reaction to that; rather than try to court people who might reject his ideas, he already filters people who are looking for the good stuff in them.
BalinKing 3 hours ago [-]
> 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.
To confirm, s/continuous hypothesis/continuum hypothesis/ ?
Also, for the curious, here's a paper pushing back on the idea that the continuum hypothesis et al. even "need" to be resolved in the first place: https://arxiv.org/abs/1108.4223 (The set-theoretic multiverse, JD Hamkins, 2011). (I don't know anything about set theory myself, so I can't personally comment on what it says—but AFAICT Hamkins is respected in the area.)
hackable_sand 2 hours ago [-]
I like this guy. Saving for later. Thanks!
guerrilla 3 hours ago [-]
So he's not crazy? After a period of my life where I had just read tons of type theory and logic and found his "Locus solum" by accident but couldn't understand a damned thing. It feels like an insane asylum. I could never figure out if he was a crank or a genius.
On the topic of Girard, I've been very attracted to his ideas about the "dynamics" of logic and "communication without understanding". It always appears to me that such ideas and things like the "execution formula" should have profound implications on static analysis of algorithms and things like abstract interpretation and collapsing stacks of interpreters.
Has there been any literature on concrete steps in this direction, or is there anything holding back Girard's theories from practical application (I know that Girard's Geometry of Interaction was supposed to have problems with additives, of which exact implications I do not quite comprehend, which may or may not be relevant)?
engboris 2 days ago [-]
I'm not very familiar with the static analysis of algorithms, abstract interpretation and collapsing stacks of interpreters but I'm curious if you have any intuitions (even vague ones).
I don't think there is any concrete steps in this direction. However, those ideas still live in the transcendental syntax since it is the successor of his geometry of interaction programme.
> or is there anything holding back Girard's theories from practical application
In theory, I don't think so. In practice, it's very difficult to approach his ideas. Not only because he's hard to read but also because you have to read and understand a lot of his previous works but also of other people's work to put everything into context. Once you do it, you then need enough practical knowledge to have an idea of what applications can come out of it.
> I know that Girard's Geometry of Interaction was supposed to have problems with additives, of which exact implications I do not quite comprehend, which may or may not be relevant
It's not very clear. From what I understand, he now considers he was "doing it wrong" and then the problem disappeared because he now distinguishes between "local" (asystemic/particular) and "global" (systemic/generic) mechanisms which are apparently and mistakenly mixed in logic. Full additives are global and live in a "system" (which defines contraints over a "free" computational space -- think of "complex systems") although we can define weaker "local" additives. This difference between local (he calls it first-order but it has nothing to do with FOL/predicate calculus) and global (he calls it "second-order") is mentionned in his "Logique 2.0" paper.
illogicalconc 4 days ago [-]
I haven’t been keeping up with Girard as much as I would like, but am I correct in intuiting that this is the next step past Ludics?
Update: I don’t see a citation, so I guess this is an exploration in a different direction.
engboris 2 days ago [-]
Formally speaking, transcendental syntax is the successor of the Geometry of Interaction programme (which is sort of parallel to the development of ludics). It gives a new and more general version (or an abstraction) of proof-nets. Whereas ludics is an abstraction of proof trees in sequent calculus.
There might be links or transcendental syntax may subsume both geometry of interaction and ludics but nobody studied the relationship with ludics as far as I know.
My current understanding is that we should distinguish "proof-objects" (a sort of certificate) and what I call "proof-process" (a recipe, a method for building proof-objects). GoI/TS mostly speak about proof-objects. If you know about proof-nets, I don't see them as the essence of proofs behind sequent calculus proofs but as formal certificate constructed by sequent calculus proofs (seen as recipes). The link between ludics and GoI may be there but I don't know. There's nothing written about this.
Twey 3 days ago [-]
This is a further step in the same programme. The programme itself is somewhat agnostic as to the underlying dynamics; the ‘stellar resolution’ mechanism (Eng's terminology, not Girard's, who AFAIR doesn't name the system) is a better-behaved replacement for the ‘designs’ of _Locus Solum_, which IMO remains the best introduction for the bigger ideas of the programme.
LudwigNagasena 3 days ago [-]
I’m sympathetic towards Girard’s dissatisfaction with the current state of model theory, but I don’t see how his project may in any practical sense fix it.
dboreham 4 days ago [-]
I've not been following since around 1985 when I realized there's no such thing as semantics. Is this mainstream now?
saithound 4 days ago [-]
Of course. Pretty hard to deny it when transformers learmed to produce useful human language not by figuring out how it relates to some Tarskian "true reality" but by looking at a lot of text and figuring out its internal use, exactly as Girard (and implicitly Kant) predicted it would happen.
Girard even noted that we'd know progress was happening as soon as early models started making certain specific kinds of mistakes children also tend to make, such as the answer to "which is heavier, 5kg of bricks or 5kg of feathers".
So yes, Kant, Girard and you got this right early on, but the mainstream has caught up since then.
Of course, semantics still works well as a technical tool in formal logic, though it has no link to its philosophical counterpart (not that this prevents B-grade philosophers from abusing the unfortunately chosen terminology to equivocate them).
dboreham 3 days ago [-]
Good to hear. I need to look up my Philosophy major friend who disagreed with me in 1985 and issue a formal "I told you so" notice ;)
Tainnor 2 days ago [-]
Why are all comments in this thread by engboris (the author of the repo) dead? They appear really relevant.
pinging dang in case he reads it
engboris 2 days ago [-]
I created an account for this thread and answered right away. If it's not because of that, then I suspect it's because of too much subjectivity / bias / self-promotion. I didn't exactly talk about my own works but my interpretation of Girard's works though, but I can understand if speaking as the owner of the repo is problematic.
dang 20 hours ago [-]
I'm an admin here. You just got caught in a (totally erroneous) spam filter. Sorry! It's hard to make these things work properly.
Fortunately other HN users vouched for your comments, and emailed us so we could mark your account legit. Everything's fine now and I hope you'll continue to participate in the community!
engboris 13 hours ago [-]
Thank you very much!
4ad 1 days ago [-]
Seems to be solved now!
Rendered at 23:52:25 GMT+0000 (UTC) with Wasmer Edge.
Girard's ideas are indeed cryptic and may sound like a caricature of (a particularly grumpy) continental philosopher. One of my goals is to make these ideas more understandable and more down-to-earth, to show that they can be illustrated in a toy programming language. But there's a still a lot of work to be done (way more than what you could imagine just from reading Girard's papers). Although I studied Girard's last works for 4 years, I'm still far from understanding all its consequences. That's because it is related to pretty much everything in logic and computation (what is a type/formula/specification, how do you know whether an object is of some type, what is a proof, what is meaning, what is a system, what are logical rules, what all models of computation have in common, what all logical systems have in common, what is a program, what is an algorithm).
The idea is to go beyond the current proof-as-program correspondence (on which proof assistants like Coq are based). After its analysis of the notion of proof, Girard wanted a computational space in which elements would be able to "test themselves", without relying on some "hard-coded" semantics. In programming terms, it would correspond to the ability to build types from programs. There is no primitive types, not even the arrow type of functional programming. We just have Prolog-like bricks of terms which can interact with each other. They can express programs or tests for programs. You build everything with that like how you do chemical experiments. To give a probably familiar illustration, I'm often asked whether we could "do transcendental syntax" with the untyped lambda-calculus. It would be possible if for any type T you could find a finite set of lambda-terms acting as "tests" such that interaction with it ensures being of type T. The space of lambda-terms is not "large enough / flexible" for that. You need to introduce exotic objects like how you extend the set of rationals Q to the real numbers R to solve more equations. You can also think of how to tell whether a finite automaton recognizes some (infinite) rational language without relying on an external semantics. You only have input words and infinite testing by feeding it all words of the language. But yet, we are able to do it with an external semantics. So the question is how you internalize semantics in the object language.
If there's anyone who has any inspirations or insights, I'm open and interested. The right path to follow is still undefined. I just have some tools coming from my understanding of Girard's works.
Theory: https://ncatlab.org/nlab/show/transcendental+syntax
More Theory: https://ncatlab.org/nlab/show/Geometry+of+Interaction
Some sort of explanation: https://x.com/noncanonicAleae/status/1874893997791170719
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 (in French, it gives an overview of the program)
https://girard.perso.math.cnrs.fr/Archives.html (transcendental syntax papers are there in English)
> 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.
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.
His main contribution, through linear logic, are ways to separate 'elementary' operations of logic into simpler ones. Linear logic decomposes the classical "and" and "or" into multiplicative and additive ones, and some modalities. This gives a more precise encoding of operations that can directly link logic to complexity theory, and have interesting applications to compiler design.
Note that academia has been very receptive of his technical achievement, the proof of consistency of System F through reducibility candidates, but much less welcoming of some of his other papers that he deemed way more interesting (as we saw recently with Terence Tao "I got a paper rejected today"). I think him writing this way is a reaction to that; rather than try to court people who might reject his ideas, he already filters people who are looking for the good stuff in them.
To confirm, s/continuous hypothesis/continuum hypothesis/ ?
Also, for the curious, here's a paper pushing back on the idea that the continuum hypothesis et al. even "need" to be resolved in the first place: https://arxiv.org/abs/1108.4223 (The set-theoretic multiverse, JD Hamkins, 2011). (I don't know anything about set theory myself, so I can't personally comment on what it says—but AFAICT Hamkins is respected in the area.)
http://girard.perso.math.cnrs.fr/0.pdf
Has there been any literature on concrete steps in this direction, or is there anything holding back Girard's theories from practical application (I know that Girard's Geometry of Interaction was supposed to have problems with additives, of which exact implications I do not quite comprehend, which may or may not be relevant)?
I don't think there is any concrete steps in this direction. However, those ideas still live in the transcendental syntax since it is the successor of his geometry of interaction programme.
> or is there anything holding back Girard's theories from practical application
In theory, I don't think so. In practice, it's very difficult to approach his ideas. Not only because he's hard to read but also because you have to read and understand a lot of his previous works but also of other people's work to put everything into context. Once you do it, you then need enough practical knowledge to have an idea of what applications can come out of it.
> I know that Girard's Geometry of Interaction was supposed to have problems with additives, of which exact implications I do not quite comprehend, which may or may not be relevant
It's not very clear. From what I understand, he now considers he was "doing it wrong" and then the problem disappeared because he now distinguishes between "local" (asystemic/particular) and "global" (systemic/generic) mechanisms which are apparently and mistakenly mixed in logic. Full additives are global and live in a "system" (which defines contraints over a "free" computational space -- think of "complex systems") although we can define weaker "local" additives. This difference between local (he calls it first-order but it has nothing to do with FOL/predicate calculus) and global (he calls it "second-order") is mentionned in his "Logique 2.0" paper.
Update: I don’t see a citation, so I guess this is an exploration in a different direction.
There might be links or transcendental syntax may subsume both geometry of interaction and ludics but nobody studied the relationship with ludics as far as I know.
My current understanding is that we should distinguish "proof-objects" (a sort of certificate) and what I call "proof-process" (a recipe, a method for building proof-objects). GoI/TS mostly speak about proof-objects. If you know about proof-nets, I don't see them as the essence of proofs behind sequent calculus proofs but as formal certificate constructed by sequent calculus proofs (seen as recipes). The link between ludics and GoI may be there but I don't know. There's nothing written about this.
Girard even noted that we'd know progress was happening as soon as early models started making certain specific kinds of mistakes children also tend to make, such as the answer to "which is heavier, 5kg of bricks or 5kg of feathers".
So yes, Kant, Girard and you got this right early on, but the mainstream has caught up since then.
Of course, semantics still works well as a technical tool in formal logic, though it has no link to its philosophical counterpart (not that this prevents B-grade philosophers from abusing the unfortunately chosen terminology to equivocate them).
pinging dang in case he reads it
Fortunately other HN users vouched for your comments, and emailed us so we could mark your account legit. Everything's fine now and I hope you'll continue to participate in the community!