Utterly Astonishing For At Least Five Reasons

In which we take a tour through provability.

[foratleastfivereasons]

Minor Update

I originally planned to cover the semantics of GL for four reasons:

Frames are Rad As Hell.

They’re useful in the study of other modal logics.

They lead to nice soundness and completeness results.

We need them to prove the Fixed Point Theorem.

As of today, I’m down to three reasons - I found a purely syntactic proof of the fixed point theorem, due to Lindström!

It’s not actually the same statement as Boolos’ version, but I think they’re equivalent - and to show that, one needs the continuity theorem and other technical semantic results. Still, now I have to reorganize my notes a bit...

(Also, this post signifies that I haven’t forgotten about this blog, I’ve just been, you know, busy with other stuff. But this Lindström result got me pretty excited, so hopefully the next post will be sooner rather than later.)

[foratleastfivereasons]

The Semantics of Modal Logic, Part Two

Validity in a frame, however, will suffice:

Inductions of this type are common, and it was worth seeing one of them. They are usually routine, so in the future we will skip them.

In a very informal sense, the ‘dullness’ of coreflexivity corresponds to the un-interestingness of a logic where p → □p holds. So let’s look at another, more familiar logic, K4:

Of course, these are just a warmup for the real action - the frame condition on GL - which it turns out isn’t even a first order statement!

[foratleastfivereasons]

The Semantics of Modal Logic, Part One

In light of this theorem, we might ask “In what frames are the theorems of K4 valid? Of GL?” We will take up this study in the next section, by considering possible properties of the accessibility relation R.

[foratleastfivereasons]

In Which We List The Reasons

“[I]t is often hard to understand how vast the mathematical gap is between truth and provability.” - George Boolos

Recall Löb’s theorem: If PA ⊢ Bew(A) → A, then PA ⊢ A. As Boolos puts it, the theorem is interesting “for at least five reasons”, mostly concerning the aforementioned gap and misunderstandings thereof.

Here are some of them:

1. The hypothesis of Löb’s theorem seems trivially true - regardless of the veracity of A, when would it not be provable that Bew(A) → A? Well, if A is false - and so hopefully not provable! - then Löb’s theorem assures us that the seemingly obvious Bew(A) → A is not provable either.

2. Following this reasoning, we notice that there are no unprovable statements A with which PA nonetheless claims to be sound (that while PA doesn’t prove A, if PA proved A, then A would hold). Indeed PA claims that Bew(A) → A only when is has to, that is when A is actually provable. As Rohit Parikh put it, “PA couldn’t be more modest about its own veracity.”

3. Somewhat strangely, Bew seems to function like a negation, as in a proof by reductio ad absurdum: if ¬A → A, then A. Indeed if we think truth and provability capture the same notion, then Löb’s theorem tells us that proof by circular reasoning is valid in PA!

4. Writing Löb’s theorem with modal logic, we might think that provability is akin to necessity. Then the hypothesis of Löb’s theorem is “it is necessarily true that if a statement is necessarily true, it is true.” But then the hypothesis of Löb’s theorem would always be true, so this naïve line of thinking has led us astray.

5. Intuitively, shouldn’t “Bew(A) → A” be provable? It’s obvious that if A is provable, then A is true, so we might naïvely suspect that PA could capture such an obvious truth - yet it comes woefully short of doing so for all statements. Boolos asks “how could any such (apparently) obvious truth not be provable?”, the answer to which is of course “well it depends what system you’re working in, and PA, while powerful, isn’t that powerful”.

With the title of the blog finally explained, next up is semantics!

[foratleastfivereasons]

I haven't posted in a while, but I'm getting back in the swing of things - I have maybe three posts in draft form, waiting to be TeXed.

[foratleastfivereasons]

Brief Update

It's been a little while, but I haven't forgotten about this blog! I've been a bit busy with other responsibilities, but soon I will discuss Kripke frames, after a post about the reasons why Löb's theorem is so interesting. (As you may have guessed, there are at least five of them)

[foratleastfivereasons]

Constructing GL, Part Three

[foratleastfivereasons]

Constructing GL, Part Two

Lemma 9 can be found in the Lemmata. Technically speaking, we have not yet proven that a modal logic statement in GL (like Lemma 9) can be translated into PA like this - that proof will appear in the next post.

(The above-mentioned ‘modal Löb’s theorem in K4’ is Theorem 10 in the Lemmata)

[foratleastfivereasons]

Update/To-Do List

“Constructing GL”, Parts Two and Three are just about done, as well as an ever-growing page of Lemmata. These will all be up soon!

I should write an intro/about page to explain what kind of background these posts assume.

I’m also considering adding some details about substitution to my first post, so that I can talk about GLS later.

[foratleastfivereasons]

The introduction and Lemmata are up, and I rewrote the first post to include details about substitution (I haven't put it online yet, though).

I almost have another page of Lemmata ready, at which point Parts Two and Three will follow in the next few days.

Whee!

[foratleastfivereasons]

Tentative Plan

A rough outline of what I’ll be posting about, to get this provability party started!

The next few posts will cover the arithmetical soundness theorem for GL, via: 1. Definitions, K4 (this just went up!) 2. The Diagonal Lemma, Löb’s Theorem 3. K4LR

I’ll probably also have some assorted commentary along the way.

Beyond that I’m not sure how I’ll be dividing things post by post, but basically I’m going to follow Boolos, starting in chapter 3. The current plan is then to cover

- Kripke frames (chapter 4) - Soundness and completeness theorems for GL (chapter 5) - Normal forms, rank, and trace (chapter 7) - The fixed point theorem (chapter 8) - Solovay’s arithmetical completeness theorem (chapter 9)

[foratleastfivereasons]

Constructing GL, Part One

Beginning from the well-known provability predicate in PA, we start to construct the modal logic system GL.

With that informal discussion informing our intuitions, let’s recall what a normal system is and discuss how to formally translate modal sentences into sentences of PA:

Though we haven’t proved it yet, a natural question arises about the arithmetical soundness theorem for GL - is the reverse true? If PA proves the statement A* for every realization *, can we say that GL proves A? Solovay proved that in fact yes, this arithmetical completeness theorem holds. In fact the theorem can be strengthened to a uniform arithmetical completeness theorem! There is a specific realization * such that PA proves A* iff GL proves A.

This is chapter 9 in Provability Logic - but we’re only halfway through chapter 3, so the proof of this remarkable theorem will have to wait.

[foratleastfivereasons]

Löb’s Theorem and the Second Incompleteness Theorem

The proofs below are more than a little informal - they should really have carefully justified notions of provability in PA via arithmetized syntax - but I quite like the symbolic manipulations on display. So as a warm up to provability and modal logic, here are a couple of proofs:

Here’s the Scott Aaronson paper I mention.

[foratleastfivereasons]

Soon.

I found a cute proof of Löb’s theorem that I hadn’t seen before, so I’ve written up a short thing about it - I’ll post it soon. After that I have a few more posts planned, but beyond those I’m not sure yet what direction I’ll go with this - I’ll probably just follow Boolos, but we’ll see.

Oh, speaking of textbooks, I put up a reading list! So you can check that out, if you want.

[foratleastfivereasons]

Placeholder

This blog will (one day) be a guided tour through modal logic, specifically Boolos’ text on provability logic (and then maybe other topics if there’s interest). But until then, here is a placeholder post.

[repeatedlycrispygolem]

there is no try

[foratleastfivereasons]

Ugh, fine, I will start getting my notes together :p

[foratleastfivereasons]

Placeholder

This blog will (one day) be a guided tour through modal logic, specifically Boolos' text on provability logic (and then maybe other topics if there's interest). But until then, here is a placeholder post.