Logblog: Richard Zach's Logic Blog

University of Calgary

UofC Navigation

Submitted by Richard Zach on Sun, 04/13/2008 - 7:45pm

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?

- Kalmár's Compleness Proof
- Dana Scott's Favorite Completeness Proof
- Lectures on the Epsilon Calculus
- The Real Reasons Why Philosophers Shouldn't Use LaTeX
- Bringing Logic (and Philosophy, CS) to the Masses
- Proof Formalization in Mathematics: Guest Post by Jeremy Avigad
- Edward Nelson, 1932-2014
- Awodey's "HoTT for Philosophers" on mathtube.org

## Comments

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.

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

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?

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.

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

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<> (< HREF="http://arxiv.org/pdf/cs/0501035v1" REL="nofollow">Part I<> and < HREF="http://arxiv.org/pdf/cs/0501039" REL="nofollow">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.