The Logic of Unprovability

Abstract

The first incompleteness theorem of Kurt Gödel states that a theory in which we can develop most of modern arithmetic is incomplete. We will take a look at such a theory: Peano Arithmetic (PA). We will develop the tools to formulate a sentence that essentially asserts in PA that it is not provable. Then we use this sentence to prove both Gödel's first and second incompleteness theorems, where the second states that PA cannot prove its own consistency. To prove Gödel's first incompleteness theorem also for consistent extensions of PA we will use Rosser sentences. These are sentences that are equivalent in PA to the assertion that a disproof of them occurs before any proof of them. After developing the necessary technical tools, we prove that Rosser sentences need not to be all provably equivalent but there are constructions where they are.