What is the effective axiomatization in Godel's incompleteness theorem?

Question

I've been always curious about Godel's incompleteness theorem and today, I decided to understand it. To understand the theorem, I started from the concepts of propositional logic and predicate logic. So to speak, I was a complete novice in mathematical logic before.

I studied through to the point that Godel's theorem states that the set of axioms cannot satisfy three conditions at the same time: 1. effective axiomatization 2. completeness 3. consistency.

I think I understand what they mean: The effective axiomatization is the existence of an algorithm that can enumerate all the theorems derived from the set of axioms. The completeness is that any statement in the language of the axioms can be proved or disproved. The consistency means that statement cannot be proved and disproved at the same time under the set of axioms.

I can connect with the concepts of completeness and consistency. Completeness is what Godel's theorem tries to disprove. Consistency seems quite natural because if it's not, the axioms are absurd as the system of axioms can't be used for proof. But I don't quite understand why we need effective axiomatization.

Can somebody please explain to me why we need effective axiomatization for Godel's theorem? And what's the implication of the condition?

Answer 1

It is easy to come up with a consistent and complete set of axioms. Usually Gödel's incompleteness theorem is phrased in terms of Peano arithmetic, which is supposed to axiomatise arithmetic in the natural numbers. So let's take that as an example. Let $\mathcal{L}$ be the language of Peano arithmetic and let $T$ be the set of all $\mathcal{L}$-sentences that are true in the natural numbers. Then for every sentence $\phi$ either $\phi \in T$ or $\neg \phi \in T$. So this system is complete, and it is clearly consistent because it has the natural numbers as a model. The point is of course that this is not effective.

So we have seen a reason why this assumption is necessary. We can also find a reason in the proof of the incompleteness theorem. It roughly goes as follows*. We can code the algorithm internally in our system (so the system also needs to be strong enough to be able to do this). What this means is that there is some formula $\operatorname{Thm}(n, t)$ that says "$t$ is the $n$th theorem on our list". Then the formula $\exists n \operatorname{Thm}(n, t)$ says "$t$ is a theorem of our system". So the system is able to talk about its own theorems! This then gives the famous "liar paradox" by constructing a sentence $G$ that is equivalent to $\neg \exists n \operatorname{Thm}(n, G)$. That is, $G$ is equivalent to the assertion that $G$ is not a theorem of our system. As you can see, this all heavily relies on our algorithm that enumerates all theorems, and on the fact that algorithms can be coded internally in our system.

---

*: Disclaimer, the second paragraph is not very mathematically precise (e.g. I have identified formulas with their Gödel number). I just wanted to sketch the argument of the proof and why effective axiomatisation is needed for it. Most steps are highly non-trivial. To fully understand these you just need to keep studying the proof, for which there are a lot of great sources.