[HN Gopher] Transcendental Syntax
___________________________________________________________________
Transcendental Syntax
Author : 4ad
Score : 51 points
Date : 2025-01-03 21:24 UTC (1 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.
| 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)?
| 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)
| 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.
___________________________________________________________________
(page generated 2025-01-04 23:02 UTC)