5
$\begingroup$

I was reading a bit about Gödel's incompleteness theorems. I haven't took the time to really study it, but I'm very curious about statements like these:

In other words, if our axioms are consistent then in every model of the axioms there is a statement which is true but not provable. source

And

Given any system of axioms that produces no paradoxes, there exist statements about numbers which are true, but which cannot be proved using the given axioms.

What I don't understand is this. How can you show that such a statement is true, without proving it ? This seems like a contradiction in itself to me.

Can someone give me an example of such a statement (about numbers) that we know is true, but which cannot be proven to be true ? And how then do you conclude that such a statement is true ? Because of the relations that numbers have with the real world ?

$\endgroup$
  • 3
    $\begingroup$ 'True' does not mean what you think it means. (Though as a formalist, I think it should). $\endgroup$ – Git Gud Jan 24 '15 at 17:20
  • 2
    $\begingroup$ Did you look at the zillion other threads about incompleteness and about "true but unprovable" statements? There are literally a gjziliion of them. $\endgroup$ – Asaf Karagila Jan 24 '15 at 17:22
  • $\begingroup$ Here is one, here is another. I'm too lazy to find the rest, but I recall writing at least three more answers discussing "true" in the context of the incompleteness theorems. $\endgroup$ – Asaf Karagila Jan 24 '15 at 17:25
  • 1
    $\begingroup$ The Gödel Theorem says that there is a statment $\varphi$ s.t. neither $\varphi$ nor $\neg\varphi$ is provable from the axioms (presupposed that they are consistent). However, by definition, in any model $M$ of the axioms, either $\varphi$ holds in the model or $\neg\varphi$ holds in the model. Identifying phrase "holds in the model" with "is true in the model" may explain why some people talk about "true but unprovable" statements. $\endgroup$ – russoo Jan 24 '15 at 17:26
  • 1
    $\begingroup$ @AsafKaragila Well, actually one of my quotes in this question, is from your answer to the top voted incompleteness question.. I did take some time, but agreed I could have taken some more time. $\endgroup$ – Kasper Jan 24 '15 at 17:37
3
$\begingroup$

True and false are relative to a structure, these are semantics properties of a sentence in a given interpretation of the language.

In some cases, like in the case of arithmetics, when we say that a statement is true we mean that it is true in a very specific model. In the case of arithmetical theories (like $\sf PA$ for example) we take the model to be $\Bbb N$.

So to determine if a statement about the natural numbers is "true" we need to see if it is true in $\Bbb N$.

Provable, again, depends on the theory. The axiom of choice is not provable from $\sf ZF$ but it is most certainly provable from $\sf ZFC$. So when we just say that something is provable or unprovable we need to have a proper context to give a correct interpretation of the statement.

In the case of $\Bbb N$ and the natural numbers, this is commonly Peano axioms, $\sf PA$.

So when we say that the statement "Every Goodstein sequence terminates" is true but unprovable, we really say that it is true that in $\Bbb N$ every Goodstein sequence terminates, but it is not true in every model of $\sf PA$.

Other true, but unprovable statements may include various consistency claims (e.g. $\operatorname{Con}\sf (PA)$ is true but unprovable) and other similar results from related incompleteness proofs. And we can encode many of them in the form of Diophantine equations or polynomials (see this particular example).

(All this, of course, has nothing to do with the real world.)

$\endgroup$
1
$\begingroup$

In the First Incompleteness Theorem, the word 'proof' does not refer to the general informal style of argument that people create to establish results. It instead has the far more specific meaning 'a derivation from axioms in formal system $X$'. The theorem's proof (in the informal sense) shows how to construct a sentence $S$ (i.e a first-order formula with no free variables) in the formal system $X$, which we humans interpret as (metaphorically) 'saying' "Sentence $S$ has no derivation in formal system $X$". *From outside of formal system $X^*$, we humans can see that if $S$ actually DID have a derivation, $S$ would be false. If system $X$ is consistent (and not perverse), as we expect, then only true sentences should be derivable. So $S$ must not be derivable.

So $S$ is 'true but not provable' - meaning that $S$ is not provable - meaning not derivable in system $X$ - but we have proved --from outside of system $X$-- that it is true.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.