Godel theorems

Introduction

Gödel's incompleteness theorems establish certain limitations on what is possible to prove through mathematical reasoning. To speak precisely about what can be proven or not, a mathematical model called formal theory is studied. A formal theory consists of a series of symbols and a set of rules for manipulating and combining them. Through these rules, certain collections of symbols can be distinguished as formulas, and certain sequences of formulas as proofs. The theorems of a certain theory are then all the formulas that can be proven from a certain initial collection of formulas that are assumed as axioms.

A theory can be:

• A consistent theory contains no contradictions, that is, it is not possible to prove both a formula and its negation at the same time. A theory that is not consistent is useless: due to the principle of explosion, from a contradiction all its formulas can be proven, and it is not suitable for modeling mathematical reasoning.
• A complete theory answers any question, in the sense that for each of its formulas, either it is provable, or there is a proof of its negation (it is refutable). A complete theory is optimal, and corresponds to the intuition about logical truth: just as every sentence must be true or false, in a complete theory every formula is provable or refutable.

Incompleteness theorem

The first theorem of incompleteness establishes that, under certain hypotheses, a formal theory cannot have both properties at the same time. The first of these is that it is an arithmetic theory, that is, that its symbols serve to describe natural numbers and their operations and relations; and that it is able to prove some basic properties about them. The second hypothesis is that it is a recursive theory, which means that the rules for manipulating its symbols and formulas in proofs must be able to be executed using an algorithm: a precise series of unambiguous steps that can be carried out in a finite time, and even implemented by a computer program.

The statement of the first theorem reads:
Theorem
Any consistent recursive arithmetic theory is incomplete.$◼$

The proof of this theorem involves constructing a certain formula, the Gödel sentence $G$, that cannot be proven or refuted in $T$: neither $G$ nor $\mathrm{\neg }G$ (the negation of $G$) are theorems of $T$. It is then said that $G$ and $\mathrm{\neg }G$ are undecidable or independent in $T$.

To arrive at this, Gödel developed a method for encoding symbols and formulas using numbers, called Gödel numbering. Using this numbering, it is possible to translate the properties of a formal theory $T$, such as these symbols constitute a formula or these formulas are not a proof in T, to arithmetic properties of those numbers. In particular, the Gödel sentence $G$ is an arithmetic formula whose meaning is there is no proof of $G$ in theory $T$, or in other words, I am not provable in theory $T$.

Consequences:
The Gödel sentence $G$ is not provable but is true, since it precisely asserts its own unprovability. This means that no arithmetic theory under the conditions of the theorem is able to prove all true statements of arithmetic.
Furthermore, even though $\mathrm{\neg }G$ is false (for asserting the opposite of $G$) it is not refutable (since $G$ is unprovable). This sentence can be taken as an axiom if desired and this does not produce a contradiction. The resulting theory contains many true statements about natural numbers and some false ones, starting with $\mathrm{\neg }G$. The objects described by such a theory form a non-standard model of arithmetic.
Taking $G$ (or its negation) as an axiom produces a new theory $T^{\prime }$ in which $G$ (or its negation) is automatically provable. However, this does not invalidate the theorem, since $G$ asserts its relative unprovability to theory $T$. The new theory $T^{\prime }$ is also incomplete: a new independent sentence $G^{\prime }$ can be found, which asserts I am not provable in $T^{\prime }$.

In short, in a consistent and complete formal theory, one of the hypotheses must fail: either it is not recursive and there is no algorithm to distinguish axioms from the rest of the formulas; or they are not arithmetic, and they do not include the necessary basic properties of natural numbers. For example, in the proof of the semantic completeness theorem, consistent and complete theories that are not recursive are used. On the other hand, Presburger arithmetic is a collection of axioms about natural numbers that omits several of their properties, to the point that a theory based on them can be consistent and complete.

Completeness theorem

Theorem
A sentence is provable from a set of axioms iff every structure (model) that satisfies the axioms also satisfies the sentence.$◼$

Remember that a "model" of an axiomatic system means a particular interpretation of the primitive notions that makes that makes the axioms true in that interpretation.
True and False in this context refer to models. True should really be true in the model $M$; that is, there is a particular interpretation of the axioms which makes the statement true. When we talk about arithmetic statements being true, we mean true in the standard model (the standard model being a particular interpretation of the primitive notions of arithmetic). There are non-standard models for arithmetic, which include other chains similar to $1,2,3,\dots$

Provable means that there is a formal derivation of the statement from the axioms. If a statement is provable, then it is true in all models; conversely, Godel's Completeness Theorem shows that if a (first order) statement is true in all models, then it is provable.

In particular, a statement is formally undecidable in an axiomatic system if there are some models in which it is true, and some models in which it is false. When you have a prefered model (as we do with arithmetic), we often talk simply about true instead of true in a particular model.

In this whole reasoning we are assuming first order logic. We can know about the trueness of a sentence not only by proving it in a bigger axiomatic system but also by using second-order logic, or infinite quantification, or, in the case of Godel sentece,via a meta-analysis from outside the system. In general, this meta-analysis can be carried out within the weak formal system known as "primitive recursive arithmetic'').

However within the confines of first-order logic, and the given theory there are sentences which we can prove are unprovable from this given theory, but can be true in some model. Furthermore, in every model there is some statement which is true (in that specific model) but has no proof.