Cfrgtkky

Godel's Incompleteness Theorem says there are statements in an axiomatic system which are TRUE but UNPROVABLE. I have read other answers here, but none of them captures the essence of such statements. So, my question is

1. What is the nature of such True statements which cannot be proved syntactically? What do they talk about? What are the requirements for a truth to be proved syntactically?


2. If there are truths that cannot be proved by manipulation of symbols, does this mean that manipulation rules/symbols are not capable enough to express some Truths?

I'll try to provide an explanation that doesn't need such proof technicalities as arithmoquines. It'll still probably require some readers to learn a little bit of theory, but I hope it'll be accessible.

Peano arithmetic is an axiomatisation of the arithmetic of non-negative integers. It is a first-order theory, i.e. the only types of object we can talk about are non-negative integers. For instance, $forall n (phi(n))$ means all non-negative integers have the property $phi$, which can be written with a formula such as $n=n$, but can't be an object in its own right in this formalism. Such a $phi$ is called a unary predicate, unary meaning it takes one argument. For each individual unary predicate $phi$ we can write down, Peano arithmetic includes the following as an axiom:

$$phi(0)landforall n (phi(n)tophi(Sn))toforall n(phi(n))$$(where $Sn$ means $n+1$). This is called induction. Note that because we can't put a "for all $phi$" wrapper around the above statement in a first-order theory, we have to install induction with an infinite collection of axioms called an axiom schema, not a single axiom.

How many such axioms are there? You might think there's one for every set of non-negative integers. Just as a set with $12$ elements has $2^{12}$ subsets (because each individual element either does or doesn't make the cut), there are $2^{aleph_0}$ sets of non-negative integers, where $aleph_0$ (pronounced aleph null) is the name of how many non-negative integers there are. But you'd be wrong. Each unary predicate is a formula of finite length, and there are only finitely many symbols in the language, and it can be shown we can only write down $aleph_0$ formulae that way. (Even if you had $aleph_0$ symbols, this conclusion would remain true.) And because every set has more subsets than elements (a result called Cantor's theorem), Peano arithmetic doesn't guarantee induction for every set you might think it would.

Meanwhile, second-order approaches to arithmetic can talk about two kinds of object, the non-negative integers and predicates on them. This allows a for-all-$phi$ wrapper on the induction described above, so one axiom covers all $2^{aleph_0}$ scenarios.

Given axioms, a model of them is a hypothetical scenario in which they're all valid (that's not the rigorous definition, but it'll do here). In accord with intuition, all models of second-order arithmetic have the same properties (we say they're isomorphic), so there's "only one" such arithmetic. But given any set $S$ of non-negative integers for which no $phi$ you can write down satisfies $forall n (phi(n)leftrightarrow nin S)$ (where $forall$ quantifies over non-negative integers), in at least one model of Peano arithmetic induction doesn't work on $S$. Why? Because a model exists iff a contradiction can't be derived, and of course Peano arithmetic doesn't assume enough to prove induction works on $S$. This is why there are statements that are "true" in second-order arithmetic but not provable in Peano arithmetic. Note in particular that Peano arithmetic's models aren't in general isomorphic, because they include but aren't limited to second-order arithmetic's unique-up-to-isomorphism model.

Most interestingly of all, this limitation even includes some statements Peano arithmetic can write down. Why? Well, at this point a simple explanation can only go so far. A theory's non-isomorphic models can still be elementarily equivalent, meaning that the language of the theory is inadequate to express the differences between them, i.e. each statement in that language is true in either all or none of the models.That's actually what happens in a weaker version of arithmetic called Presburger arithmetic (which is therefore incomplete), but it doesn't happen to Peano arithmetic (which therefore isn't). Both theories aren't the whole second-order story, but Peano arithmetic's greater ability to discuss multiplication is what makes it incomplete. Why does that make all the difference? Because a theorem says so, I guess.

In any first-order theory that models Peano arithmetic, such as set theories, the same predicate-counting logic reaches much the same conclusion. In fact, Peano arithmetic has an induction-lacking fragment called Robinson arithmetic that has the same problem. When an incomplete theory can't be made complete by adding axioms to it, because its language is too expressive for such an extension's models to end up all elementarily equivalent, we say it's essentially undecidable, and that is true of both Robinson and Peano.