The other day, Arnon Avron asked on FOM whether the Second Incompleteness Theorem holds for Robinson’s Q. I remembered wondering about that myself back when I was preparing for the foundations qual. The issue is this: the usual proof of the unprovability of Con(T) requires that T is not just “sufficiently strong” in the usual sense, i.e., you can arithmetize syntax in T, but the provability predicate used to formalize Con(T) must satisfy the Hilbert-Bernays-Löb provability conditions:

1. If T proves A, then T proves Pr(A)
2. T proves Pr(A → B) → (Pr(A) → Pr(B))
3. T proves Pr(A) → Pr(Pr(A))

Now Q doesn’t have induction, so it can prove only very few universal claims, in particular, it does not satisfy condition 3. (Does it satisfy condition 2?) So does Q prove Con(Q), i.e., ¬Pr_Q(0 = 1)? It does not. The first result to this effect, as far as I know, is Bezboruah and Shepherdson, Gödel’s Second Incompleteness Theorem for Q (JSL 1976). In the late 70s, Wilkie and others developed the model theory of weak fragments of arithmetic sufficiently for more informative results to be obtained, e.g., Pudlák’s 1985 “Cuts, consistency statements and interpretations.” Wilkie and Paris (On the scheme of induction for bounded arithmetic formulas, APAL 1987, Thm 3.5) showed that Con(Q) isn’t even provable in IΔ₀ + exp.

I recommend Bezboruah and Shepherdson’s paper also for the references to the discussion in Kreisel’s papers and elsewhere about the philosophical significance of the derivability conditions. The classic treatment of the logic of provability predicates satisfying these conditions is Boolos’s Logic of Provability.

UPDATE: There are some good replies to Arnon’s question in the FOM archives, especially that by Curtis Franks and the one by Arnold Beckmann. Incidentally, Curtis’s post made me look up Buss’s article on proof theory of arithmetic in the Handbook of Proof Theory, where Buss formulates the Second Incompleteness Theorem as:

Let T be a decidable [should be: axiomatizable], consistent theory and suppose T ⊇ Q. The T does not prove Con(T). (p. 121).

In a comment to an Antimeta post about the Formal Epistemology Workshop, Jon Cohen asks:

[W]hat’s the deal with the “commentator” listed for some of the talks? To me it sounds like someone will be sitting there saying things like “Kenny has gone for the slide striptease trick, not sure how this will go down with the crowd” (you can probably guess how many philosophy talks I have been to…).

That would be much more fun than having the comments at the end. But also much more distracting for the speaker.

Since school’s out, I thought I’d try to spend some of my time otherwise than reading, writing, and grading. So I started a blog about things to do in Calgary. Not that many of you care, but perhaps there’s someone from Calgary reading this. My plan for next Summer is to actually go out and do these things, rather than just blog about them. (j/k)

The Society for Exact Philosophy is meeting in Toronto right now. (Someone told me that the name of the society is a joke, but maybe they were joking. It’s serious philosophy, in any event. And it’s the 33rd annual conference, so if it’s a joke, it’s a long-running joke.) The keynote speakers are Jason Stanley, who did some rabble-rousing in phil of language today; Ernie Lepore, who spoke about quotation; and Jeff Pelletier, who will take steps towards “making it work” tomorrow (but I don’t know what “it” is, yet). Other highlights (that I attended) thus far: Michael Glanzberg on unrestricted quantification, Chris Pincock on applications of mathematics, Byeong-Uk Yi on Priest’s version of Zeno’s paradox, and Greg Ray on refuting epistemicism. I took some stabs at Brian’s recent “Truer” paper. (Two days of work getting the diagrams right in pgf!)

If I were a more conscientious blogger, I’d tell you what they all said. As it is, you’ll have to email them for their papers. But anyway, Phil Kremer put on a fine meeting, and y’all should come to the meeting next year in San Diego.

UPDATE: More fun yesterday: Jeff Pelletier showed how to get n-ary exclusive or from 3-ary exclusive or (you can’t get it from binary exclusive or); Imogen Dickie argued for the superiority of Fregean over Tarskian semantics for quantifiers; and Bernie Linsky presented Russell’s notes to Frege’s Grundgesetze and talked about what Russell understood of Frege’s work in 1902.

John MacFarlane‘s entry on logical constants is up at the Stanford Encyclopedia of Philosophy. Everyone interested in this should also read John’s dissertation (including me, I admit).

Stewart Shapiro posted a little “Primer on Vagueness” on the FOM list yesterday.

There are two new logic blogs linked on the sidebar. The first is Andrej Bauer’s Mathematics and Computation, the other is Logicomp, a blog on logic and complexity theory by Anthony Widjaja at the University of Toronto.

This year’s workshop Prologic 2005, July 6-8 at LSE, will focus on objective Bayesianism. Registration deadline is June 3.

There’s an interesting discussion going on at Leiter’s blog and on Certain Doubts about Dreben and the history of analytic philosophy. I recommend especially Jason Stanley’s comment on the Certain Doubts post.

While on the subject of Dreben, I thought I’d point out something pointed out to me not too long ago by Bill Tait. Dreben is commonly credited with discovering the (now well-known) errors in Herbrand’s Thesis. But these errors were actually discovered by Peter Andrews in 1961/62 (he was then a grad student at Princeton). Andrews has a full account of the discovery and the correspondence with Dreben in his Herbrand Award Acceptance Speech.

I try to keep an eye out for uses of logical connectives, etc., in “everyday life” that I can use in logic classes. Here’s a nice use of excluded middle, in which neither disjunct is assertible, from “Two to go,” the penultimate episode of Buffy, Season Six. Or maybe it’s really an example of the failure of Ought(A ∨ B) → (Ougth A ∨ Ought B).

ANYA: She [Willow] tried to use you for a hood ornament, Xander! She doesn’t care if you live or die.

XANDER: Guess you two finally have something in common.

ANYA: I care if you live or die, Xander. I’m just not sure which one I want.