Hacker News new | comments | show | ask | jobs | submit login

Jean-Yves Girard, a great logician, also has a lot of quarrels to pick with analytic philosophy. His prose is idiosyncratic, lyrical and definitely at odds with the dryness of "logic of the 20th century". If you like the idea of an energetic approach to reconceptualize philosophy, in particular the philosophy of logic, I recommend reading Girard's work. The Blind Spot: Lectures on Logic is an organized survey of logic starting with Hilbert's formalism and ending up in the operator algebras of Geometry of Interaction. Along the way, Girard's combative, highly opinionated and witty commentary ceaselessly entertains and engages.

Perhaps what is most striking about Girard in contrast to Nozick is how he manages to be very rigorous and artful simultaneously. Something as abstract of logic becomes a living creature when Girard talks about it. To see logic this way is to expect it to flourish in subordination to the rest of human experience, not languish in its own obscure enclave, ceaselessly chasing its own tail, reducing the alluring to the banal.




Energetic though it may be, and notwithstanding Girard's brilliance, I doubt that I could consider a quirky treatise on proof theory to be a _philosophical_ text.

And one can be rigorous without resorting to formulae.


Girard is French, and The Blind Spot is best understood as a piece of continental philosophy, not analytic.

The short version is that back in the late 60s, Althusser suggested that fields of knowledge inherently have "a blind spot" -- his idea was that every field of knowledge has to resort to structuring/organizational principles which cannot be properly articulated within the field of knowledge itself. Jacques-Alain Miller applied this idea to logic, arguing that the Fregean definition of equality (and hence number) exhibits precisely this kind of problem. Namely, Frege defined zero as the extension of the predicate "not equal to itself", and so Frege implicitly excludes the subject from logic, as Lacan had defined "subject" as the non-self-identical.

However, Alain Badiou objected very strongly against the extension of Althusser's ideas to logic. He thinks that science and mathematics can generate definitively true, objective, non-political knowledge, and so while blind spots can occur in daily ("ideological") life, they cannot occur in science.

Girard is essentially making an argument against Badiou and in favor of Miller. Because Girard is Girard, he never explicitly mentions any of these people in his lectures. This way, he can laugh at those of us who were too ill-informed to catch the fact that the TITLE of his lectures is a direct reference to Althusser.

Anyway, Girard begins with Lorenzen's idea that a proof can be understood as a dialogue between a proponent and a refuter, and the observation that the continuation-passing-style translation embedding classical logic into intuitionistic logic doesn't require that the answer type of the continuation be the empty type. He observes that these two ideas fit together in Krivine-style realizability models of classical logic: every formula can be interpreted as a set of proofs and refutations, and the interaction of a proof with a refutation yields a behaviour in the answer type. As a programmer, I think of the answer type as the runtime system of a programming language. The Krivine construction ensures that every proof -- every program -- both respects the invariants of the answer type/runtime system, and can never observe them.

So the runtime system of a programming language exhibits the essential structure of an Althusserian blind spot, and so via Curry-Howard so must logic.

I don't claim to understand the implications of all this, but I find the idea of bringing continental philosophy into the foundations of logic in a really serious, technically profitable way to be very exciting.


> He observes that these two ideas fit together in Krivine-style realizability models of classical logic: every formula can be interpreted as a set of proofs and refutations, and the interaction of a proof with a refutation yields a behaviour in the answer type.

I've wanted to see this paradigm implemented in the Isbell envelope of a category, whose objects are pairs of a presheaf and copresheaf T, E and a natural transformation from T(-) x E(--) ~> Hom(-,--) . I think it would be really striking if the answer type could be Hom itself, which I like to think of as a formalisation of the turnstile |- by itself.


That's the thing about Girard though. His work isn't merely proof theory, but foundations in the grand sense; Foundations if you will. This is the sort of thing when endeavored in the 21st century that can either be a huge bust or something new and interesting. I think it's the latter.

For example, through linear logic, one can find new justifications for logical constructions internally in contrast to justifications externally through model theory. This is clearly a philosophical program within logic. I believe it has philosophical implications outside of logic.

I think this is a serviceable explication of Girard's program as a philosophical program: http://s3.amazonaws.com/academia.edu.documents/36506773/SinT...


That link you provided doesn't work.


Sorry about that. Here's a link that works, but you need to sign up to download the pdf. However if you search for the paper on scholar.google.com, you can download a cached version directly: http://www.academia.edu/10495057/On_Trascendental_syntax_a_K...




Applications are open for YC Winter 2019

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

Search: