Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 7 of 7
Thanks for the pointer.
I keep finding when reading that I tend to have trouble spotting the focus in Girard’s writing. For instance when I open that document “Transcendental syntax 2.0” (pdf) on pages 27-28, the paragraph headlined “dependent types”, then I read it again, and then I still could not reproduce the intended message. What I do get away with is somebody expressing strong opinions, but I am not always sure what the opinion actually is.
Well, I also get the impression that he’s often talking to an in-crowd of people who can follow and are willing to discuss and debate his allusions (and jokes).
Sometimes he does hard mathematics too, and indeed his original Linear Logic paper has some hard combinatorics in it (cf. the ’long trip’ criterion for the correctness of a proof net). I’m probably not alone in finding that material quite useful and important.
So Tony, if you’re up on your Girard and know of places where he (or somebody else) proves actual theorems relevant to GoI, etc., that might be very useful for us here to sink our teeth in.
I see Todd’s point, we have been somewhat excessively increasing the ratio of philosophical over mathematical discussion as of late and it would be good to re-balance that a bit. Nevertheless, given the title of this thread here, if you could give me a summary of what that “transcendental syntax” is supposed to be about, I’d really appreciate it. In the little spare time that I have I briefly looked through Girard’s note, but I didn’t get much out of it yet.
A kind soul pointed out to me that this recent thesis here may be a helpful read for transcendental syntax:
I have added that to new entry transcendental syntax which I gave a mini-minimum of an Idea-section. Experts (if any?) please expand!
1 to 7 of 7