Definition of Algorithms in Gödel's incompleteness theorems

Question

I wish to check if my understanding of the limitations on mathematical logic due to Gödel's incompleteness theorem is correct. I was under the impression that it is possible to both avoid contradictions and prove every false statement false. For some statements it may not be possible to find an algorithm that can be used to prove them true. The word algorithm in this definition is where my question lies.

Is it possible to prove certain statements true by just chancing upon the proof?

Unless my definition or use of the term is wrong, doing so would not require an algorithm to arrive at that point.

I feel this question is relevant to a lot of people, because if true, it changes the perspective on incompleteness theorems from one of impossibility to unlikelihood of certain things been proved.

(I have also heard that some statements are simply not provable in a finite amount of time; but I was under the impression that there exist a few true statements that no algorithm can prove true given a number of axioms to start with).

Answer 1

There is nothing about not being able to find an algorithm to prove a statement in the conclusion of Godel's theorem. It is about the existence of proofs themselves within formal systems. Perhaps the confusion is from the fact that proofs in formal systems are very mechanical in nature; they are rigid applications of rules of inference to axioms and could in principle be listed off one by one by a computer.

What Godel's (first) incompleteness theorem says is, roughly, in any formal system of axioms and rules of inference (that is sufficiently rich that it supports basic arithmetic), there are well-defined statements for which there is no proof either way. The part in the theorem about algorithms isn't about the existence of an algorithm to prove a given result, but rather the existence of an algorithm that will list all the theorems off one by one, which is an important precondition for the theorem to hold.

If you have a statement that you want to prove, you could in principle wait for the algorithm to spit it out, but you could be waiting for an arbitrarily long time and you're out of luck if it isn't a theorem after all. To prove a theorem, you don't use this enumeration, you try to figure out the proof (chance upon it). This all doesn't have much to do with the conclusion of Godel's theorem, that there are statements that cannot be proven either way from the axioms, since the existence of the enumeration algorithm is a different issue than the existence of particular proofs and the provability of statements.

Answer 2

Suppose I write down a system of axioms, like so:

1. $\forall x. \forall y. (x y) z = x (y z)$
2. $\exists e. \forall x. e x = x e = e$
3. $\forall x. \exists y. x y = y x = e$

This system of axioms is incomplete, because for instance it does not allow us to determine whether the following statement is true or false:

4. $\forall x. \forall y. x y = y x$.

Why? Well, if you consider axioms (1) - (3), there is more than one mathematical object satisfying them. One object which satisfies them is the multiplicative group $\mathbb{R}^\times$ of real numbers. Another is the group $\operatorname{GL}_2(\mathbb{R})$ of $2 \times 2$ real matrices. In $\mathbb{R}^\times$ axiom (4) is true; in $\operatorname{GL}_2(\mathbb{R})$ it is false.

Moreover, any time a system of axioms is incomplete it is for precisely this reason: it describes more than one mathematical object and those objects have different properties.

Now if we're trying to describe $\mathbb{R}^\times$ with our axioms and we want to rule out $\operatorname{GL}_2(\mathbb{R})$, we could add (4) to our list of axioms. But they'd still be incomplete. (Exercise: check this!)

Now, maybe if you have a particular mathematical object in mind you can just keep adding true statements about it and at some point your axioms will completely describe it (up to elementary equivalence). At that point your axioms will be complete, since they can determine if any first-order statement about the object is true or false.

But there's no guarantee you'd ever finish. To draw an analogy, consider an arbitrary real number, say

$r = 2,345,098.231456981324509813245098123409123409123049\ldots$

If there's no useful "pattern" to the number, it's possible that we can't describe it in a finite amount of space. To make this precise, we say that a number $r$ is computable if there exists a Turing machine that, given a positive integer $n$ as input, prints out the first $n$ decimal digits of $r$. Since there are countably many Turing machines and uncountably many real numbers, almost all real numbers are uncomputable.

It's often the case that a mathematical object requires infinitely many axioms to completely describe it (up to elementary equivalence). (It's always possible, because you could simply take your list of axioms to be every single true statement about the object.) However, such a list might be more akin to

$\pi = 3.14159265358\ldots$

-- that is, computable -- or it may be more akin to the uncomputable number $r$ above.

What Godel's incompleteness theorem says is that if you're trying to describe the natural numbers, every complete set of axioms describing them is uncomputable.