Hacker News new | past | comments | ask | show | jobs | submit | illogicalconc's comments login

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.


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.


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.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: