3 ms·
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, mean
by Tainnor 2y ago
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 2y agoGirard 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 2y agoYeah, 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.
- Nevermark 2y agoAgreed! I would think the target audience might include people who would like to be in the target audience. It always bothers me when that is apparently not the case.
- woolion 2y agoHis 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.