True yet unprovable statement?

Question

I have recently been studying Godel's Incompleteness Theorem. I am completely new to the study of logic, so I have been working to break down each component. Assuming I've understood the theorem correctly there exists true yet unprovable statements within any system. So to ask my question please picture this: (Bear with me, as I am not very familiar with set notation as a high school student)

There is a set that holds all natural numbers. The rule for this system is that adding one to any integer will result in the integer immediately after it. Within this system, how would you find a particular statement that is true yet unprovable? Does it have to do with the innumerability of infinity? Meaning after numbers are uncountable, the rule still stands except it can't be represented?

I would appreciate any input into the subject. Please feel free to correct any discrepancies in my understanding.

Answer 1

It depends on what kinds of claims you want to make and prove about the natural numbers. If all you're interested in is how the numbers are ordered (i.e. that 18 is the next one from 17), then that's all perfectly provable.

Also, it turns out you can prove any claims that are purely about addition (see Presburger Arithmetic).

But, once you add multiplication in there, you get into trouble. That is, Godel's Incompleteness Theorem says there is no complete (and sound and recursive) set of axioms that can prove all truths involving addition and multiplication for the natural numbers.

Very crudely, the reason is that you can use natural numbers to encode logic statements about numbers, and even statements about logic proofs. Thus, logic statements about numbers become statements about statements (or proofs) about numbers. And, once you have addition and multiplication in your proof system, the system becomes 'strong enough' to be able to encode the infamous Godel sentence $G$ which effectively ends up saying "I am not provable within this system" (so note that the Godel system refers to the system you are using, meaning that every different system has its very own Godel sentence).

OK, so now consider $G$: Yes, through the encoding it ends up making a claim about its own (un)provability, but it is also still a statement about numbers. So, is it true or false? Well, if false, then it would be provable .. and (assuming the system is sound) therefore true. OK, so it can;t be false. So .. it's true ... and therefore not provable (again, within the system you're working with)!

Answer 2

Within this system, how would you find a particular statement that is true yet unprovable?

The statement is a statement of the form $P(x)$ (a predicate with 1 free variable). It is constructed in such a way that $P(0)$ has a proof, $P(1)$ has a proof, $P(2)$ has a proof, etc for all natural numbers. However, it is also constructed in a way such that $\forall k.P(k)$ does not have a proof.

The specific statement used is $P_z(x) = x \text{ IsNotAProofOf } z$. An implicit mapping between natural numbers, proofs, and propositions is used (for example $4 \text{ IsNotAProofOf } 7$ would mean that the fourth proof is not a proof of the seventh proposition, taking all possible proofs and propositions into account).

Then using Godel's Diagonalization Lemma a sentence $D$ (which is the $d^\text{th}$ proposition) is constructed with the property that $$D \iff \forall x~.~P_d(x)$$

First, $P_d(x)$ is always provable or disprovable, since it is a straightforward mechanical process to verify if a proof is correct or not and what the conclusion of the proof is (you could write a computer program to do it).

Second, $\forall x~.~P_d(x)$ cannot be provable: if it were, then $D$ would be provable, so $d$ would have a proof, which is a contraction of $\forall x~.~x \text{ IsNotAProofOf } d$.

Third, each of $P_d(0),~P_d(1),~P_d(2),~\dots$ must have a proof: each is decidable by the first claim, but if any were true then $d$ (and thus $D$) would be provable contradicting the second claim.

So there you have it, $\forall x~.~P_d(x)$, true but not provable.