1. 4
  1.  

  2. 3

    Highlight from Hacker News on this article. Too out of my expertise to evaluate but analysis looked really interesting:

    “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.”

    1. 2

      Can you link to the HN comment here?

      1. 2

        Wait, I was tired and slipped on my description. It wasn’t this article. I was digging through a bunch in a discussion of it to find context on Girard’s thinking. The original disappeared overnight (?) but I got that comment from this prior discussion someone linked to:

        https://news.ycombinator.com/item?id=14244408

        It was the only set of comments I found that got in depth about the context of Girard’s work. Hope that helps you.

        1. 2

          Thanks! Formal logic and Continental philosophy are both above my pay grade but if anyone can clarify them it’s MJD.