Skip to main content

Mattias Granberg Olsson: A Model-Theoretic Proof of Gödel's Theorem: Kripke's Notion of Fulfilment

Presentation of master's thesis in mathematics

Time: Fri 2017-01-13 13.00 - 14.00

Location: Room 32, house 5, Kräftriket, Department of Mathematics, Stockholm University

Export to calendar

Supervisor: Erik Palmgren

Abstract:
In the 1930's Kurt Gödel proved the first version of what is thenceforth often referred to as Gödel's Incompleteness Theorem, that sufficiently strong arithmetic theories are incomplete, by formalising logic in arithmetic and using a diagonal construction with the formalised notion of derivation. The construction has since then been streamlined and generalised. Later on other constructions have also been used, yielding proofs that are more model-theoretic or more natural. Notable among these is Jeff Paris' and Leo Harrington's result from the late 1970's that a particular extension of the Finite Ramsey Theorem is true (in the standard model) but cannot be derived in Peano arithmetic (PA).

We present a third construction via the notion of fulfilment, which is originally due to Saul Kripke and subsequently developed and presented by Joseph Quinsey; our aim is to reproduce their results in a comprehensive manner. We thus introduce the concept of a formula being fulfilled by a sequence of numbers, which is an approximation of the formula being true. This notion is subsequently formalised in a weak subtheory of PA and, given a consistent, recursively axiomatisable extension T of PA which is sufficiently sound, used to construct a sentence we will show to be independent of T. The proof of the latter is by first showing that the sentence is true in the standard model and then constructing a model of T where it is false. We finally generalise this method to show that every consistent, recursively axiomatisable and sufficiently sound extension of a weak subtheory of PA is incomplete in a similar manner. This will be at the cost of some naturality, however, and an explicit falsifying model will only be obtained under additional assumptions.