[HN Gopher] Transcendental Syntax
___________________________________________________________________
Transcendental Syntax
Author : 4ad
Score : 63 points
Date : 2025-01-03 21:24 UTC (4 days ago)
(HTM) web link (github.com)
(TXT) w3m dump (github.com)
| 4ad wrote:
| Guide (in French): https://tsguide.refl.fr/ts.html
|
| 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
| idlewords wrote:
| 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.
| illogicalconc wrote:
| 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.
| Twey wrote:
| 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.
| engboris wrote:
| 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.
| dboreham wrote:
| I've not been following since around 1985 when I realized there's
| no such thing as semantics. Is this mainstream now?
| saithound wrote:
| 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 wrote:
| 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 ;)
| qazxcvbnm wrote:
| 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 wrote:
| 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.
| woolion wrote:
| 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. Godel 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)
| Tainnor wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| > 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.)
| guerrilla wrote:
| 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.
|
| http://girard.perso.math.cnrs.fr/0.pdf
| hackable_sand wrote:
| I like this guy. Saving for later. Thanks!
| LudwigNagasena wrote:
| 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.
| engboris wrote:
| 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.
| Tainnor wrote:
| 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 wrote:
| 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.
| 4ad wrote:
| Seems to be solved now!
| dang wrote:
| 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 wrote:
| Thank you very much!
___________________________________________________________________
(page generated 2025-01-07 23:01 UTC)