Gödel's Incompleteness theorem in modal logic

Question

I think I once taught that the statement of the Gödel's Incompleteness theorem is equivalent to :

$ \diamond \neg \square \square p $, if p is a complex enough system.

Is this right?

Answer 1

This is not right. There's a few things wrong here.

• First, you seem to be using $p$ to denote both a statement which is undecidable, and the theory (usually denoted "$T$") that we're analyzing. The latter is built into the modalities - e.g. "$\Box p$" means "$T$ proves $p$," etc. (Note that if we want to talk about different theories, we have to use different modalities - this is often a stumbling point.)

• Second, what you've written means "it is consistent that $p$ is not provably provable." This is true if $p$ is undecidable in $T$, but it's not really what we want to say. Godel's first incompleteness theorem says that (for appropriate $T$) if $T$ is consistent, then there is an undecidable sentence - that is, $$\neg\Box \perp\implies [\neg\Box p\wedge\neg\Box\neg p]$$ where "$\perp$" is a name for the sentence $0=1$ (say) and $p$ is the Godel sentence (well, actually $p$ should be the Rosser sentence, but whatever). Godel's second incompleteness theorem then says the same thing, but for a different $p$ - namely, "$Con(T)$."

Of course, you might mean different things by your modal operators than I do; but then you should specify what you mean.