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.

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.

Agreed! 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.

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.