[Tazerenix]

A theorem which is true in every model is provable by Godel's completeness theorem. Since this theorem is true for the standard model of the natural numbers but not provable, it follows there are nonstandard models of the natural numbers for which it is false.

That is, there are models of Peano arithmetic which contain all of the natural numbers we know and love, and some other ones on top of that and there are some Goodstein sequences using those extra "non-standard" natural numbers which do not terminate at zero.

https://en.wikipedia.org/wiki/Non-standard_model_of_arithmet...

[hfhdjdks]

>Since this theorem is true for the standard model of the natural numbers but not provable

I've always found the provable vs true comparison confusing. How can we say the statement is true under the standard model if we cannot prove it? I understand that it could be true, but how do we know it? If it's proven with second order arithmetic, then this implies it is true under the standard model too?

Or are there statements true independently of the axiomatic system you use to prove them? (Apologies if this is too off-topic)

[symple]

The provability of a statement depends upon which system you are in. For instance, within PA one can’t prove that PA is consistent but within ZFC one can prove that PA is consistent. We can say of a statement: Statement A can’t be proven in a given axiomatic system but it can be proven in a different system.

Let’s assume the Natural Numbers are consistent system. Let’s collect all true statements in this system and use that collection as our axioms. It is now the case that every true statement about the Natural Numbers can be proven in this system. The problem with this system of axioms is that there is no effective procedure for determining if a statement is an axiom or not. It is not a useful system.

Every true statement can be proven in some system. The incompleteness theorems show that we can’t have a relatively simple set of axioms that are powerful enough to prove all true statements about the Natural Numbers. Every simple enough set of axioms for the Natural Numbers will have nonstandard implementations (models) in which some statements are false in these nonstandard models but true in the Natural Numbers.

[theteapot]

Quote from linked page:

> The existence of non-standard models of arithmetic can be demonstrated by an application of the compactness theorem. To do this, a set of axioms P* is defined in a language including the language of Peano arithmetic together with a new constant symbol x. The axioms consist of the axioms of Peano arithmetic P together with another infinite set of axioms: for each numeral n, the axiom x > n is included. Any finite subset of these axioms is satisfied by a model that is the standard model of arithmetic plus the constant x interpreted as some number larger than any numeral mentioned in the finite subset of P. Thus by the compactness theorem there is a model satisfying all the axioms P. Since any model of P* is a model of P (since a model of a set of axioms is obviously also a model of any subset of that set of axioms), we have that our extended model is also a model of the Peano axioms. The element of this model corresponding to x cannot be a standard number, because as indicated it is larger than any standard number.

So basically take Peano arithmetic and say "Hey Peano Arithmetic, what's the largest number you have? Oh n you say? well exists x > n. Haha". Seems like childish game.

[anvuong]

It's philosophical. It's either turtle all the way down or the axiomatic systems. With axiomatic systems you'll always get things like this, and this is what keeps mathematician awake at night.

[Kranar]

Not at all. There is no largest natural number to begin with even in the standard model. One way to conceptualize non-standard natural numbers would be to consider natural numbers with an infinite number of digits. Any such number would be greater than any natural number, and no first order model of arithmetic can exclude every possible way to express such numbers.

The main issue is that first order logic can't define the concept of finite. There is no way for a first order system to express a statement like "There are only finitely many x such that P(x) holds." Introducing such a finite quantifier or finite predicate will also introduce inconsistencies.

If it were possible then one could introduce an axiom along the lines of "For all x, x has a finite number of predecessors." and then we could eliminate all non-standard natural numbers.

[lanstin]

Is there a cite for that? (About true in all models implies provable?). This post is the first I have heard that but it seems very significant.

[magneticnorth]

Godel's completeness theorem https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_th...

(Not to be confused with Godel's incompleteness theorems)

[symple]

It’s the Completeness Theorem.