Richard Zach

Linear Logic is Pseudoscience?

There’s a very laudable enterprise: Blogging on Pseudoscience (at BPSDB.org) aggregates blog posts debunking or pointing out pseudo-scientific nonsense such as Intelligent Design. Lots of good stuff, PZ Meyers is part of it, etc. But, look at the logo they use:

BPSDB
Yes, that’s a sequent calculus for linear logic. I know Girard has an idiosyncratic style, and that ludics paper may look a bit hokey. Probably only Girard can get a logic paper published in a respectable journal which contains quotes like this:

Jurassic logic keeps celebrating the wedding of Semantics and Syntax through the intercession of the Holy Meta, and, of course, every ritual deserves its own mockery, the Cross upside down, the Gospel in reverse order… In paralogics, there is no syntax, no semantics (or, better, the semantics is called syntax and vice versa). These mockeries, religious or logical, betray a paradoxical respect for a tradition that the protagonists never understood.

as well as pictures of skunks:
I mean, those two appendices are weird. But the proof theory is ok, isn’t it? And there’s nothing wrong with linear logic, is there?

Posted

in

by

Richard Zach

Tags:

Comments

6 responses to “Linear Logic is Pseudoscience?”

  1. Ole Thomassen Hjortland

    Wow, one should have thought that there is enough bad science out there to keep linear logic safely on the good side. I wonder what computer scientists think of this. Last time I checked linear logic was a thriving branch of their field.Perhaps Girard’s style makes the philosophical side of his project a bit impenetrable, but that doesn’t debunk his logical contributions.However, I can’t find any references to Girard or linear logic when searching the posts.

    Reply
  2. Anonymous

    That’s a sad misunderstanding.Girard, other linear logicians and theoretical computer scientists found that linear sequent calculus proofs were so tedious to write that they invented proof-nets and other bureaucracy-free formalisms, leading to new insights!Implicitly accusing Girard of formalism is like calling Dawkins a creationnist…

    Reply
  3. Richard Zach

    I don’t get that last comment. Who ever writes out proofs? What do you mean by “formalism” and who do you think accused Girard of it?

    Reply
  4. Shawn

    What’s funny is that neither the website nor the logo references the weird stuff that Richard points to in the post. They just have the sequent calculus stuff which, I believe, can be found any lots of computer science and proof theory handbooks. Maybe it is a bias against proof theory? On a more serious note, Richard, have you made sense of Girard’s ludics paper? I tried to read it last year and it defeated me. I might give it another shot this summer.

    Reply
  5. Richard Zach

    No, not even tried. Do let me know if you do.

    Reply
  6. Charles Stewart

    Someone close to Girard’s inner circle told me that Girard delights in obscurity, and finds the idea of saying something obvious painful. Such a disposition is not conducive to writing for a broad audience, and it is perhaps remarkable that Proofs and Types got written.Curien is a much better expositor of ludics than Girard; try, for instance, his Introduction to linear logic and ludics (Part I and Part II. Currian and Faggian gave a two hour talk to the Girard Fest last year, though I haven’t seen the talk written up.

    Reply

Leave a Reply to Charles Stewart Cancel reply

Your email address will not be published. Required fields are marked *