UofC Navigation

Sunday, April 13, 2008

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:

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?



At April 13, 2008 3:50 PM , Blogger Ole Thomassen Hjortland said...

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.

At April 13, 2008 5:09 PM , Anonymous Anonymous said...

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

At April 13, 2008 7:39 PM , Blogger Richard Zach said...

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?

At April 13, 2008 9:10 PM , Blogger Shawn said...

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.

At April 14, 2008 1:31 AM , Blogger Richard Zach said...

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

At April 16, 2008 1:51 AM , Anonymous Charles Stewart said...

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.


Post a Comment

Links to this post:

Create a Link

<< Home