#provability

[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]

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.