True Statements: Always Provable?

TylerH

Are all true statements provable? Is there an axiom or theorem that says one way or the other?

micromass

No, not all true statements are provable. One example that comes to mind is Goodstein's theorem. It is unprovable in the Peano axioms, but it is still a true statement.

Note that I'm not an expert at all on this field, so I might be wrong on this.

TylerH

Can Goodstein's be said to be true under the Peano axioms if it can't be proven within them?

micromass

Yes, you should research something called sigma 1-completeness. It tells us that any sigma 1-statement (which, I think, includes Goodstein's theorem) which is unprovable is in fact true. So Goodstein's theorem is true (in the sense that every model of Peano's axioms satisfy Goodstein), but unprovable.

AKG

If you're talking about formal mathematical statements (stated in some first-order language), then "true" depends on how you interpret the formal expression as a meaningful statement, and "provable" depends on what axioms you have to start with.

Every true field-theoretic statement about [itex]\mathbb{C}[/itex] is provable from the set of axioms which state that [itex]\mathbb{C}[/itex] is an algebraically closed field of characteristic 0.

On the other hand, there is a true arithmetic statement about [itex]\mathbb{N}[/itex] not provable from the Peano Axioms, and in fact for every "reasonable" set of axoims in the language of number theory, there's a true fact about [itex]\mathbb{N}[/itex] not provable from those axioms.Goodstein's theorem is a true fact about the natural numbers, but it's not provable from PA. What do you mean when you say "true under the Peano axioms"?This is false. If something is true in every model of the Peano axioms, then it's provable from the Peano axioms. Godel's completeness theorem says essentially:

Fix a first order language [itex]\mathcal{L}[/itex]. If [itex]\phi[/itex] is an [itex]\mathcal{L}[/itex]-sentence, [itex]\Sigma[/itex] a set of [itex]\mathcal{L}[/itex]-sentences, then [itex]\phi[/itex] is true in every model of [itex]\Sigma[/itex] iff [itex]\Sigma[/itex] proves [itex]\phi[/itex].

TylerH

I'm not sure how it should be said. It could be restated as "true within a system governed by the Peano Axioms."

micromass

Thanks for your reply, I knew there was something fishy about what I wrote. I guess I have a whole lot of logic to learn

micromass

A small question though: to my knowledge Godels incompleteness theorem tells us that there is a statement which is true, but not provable by Peano's axioms.

I always thought "true" was: it holds in every model. But this appears to be false. What do they mean with true then?

AKG

In the context of Godel's incompleteness theorem, "true" means "true in the standard model [itex](\mathbb{N}, 0, S, +, \times, <)[/itex]."

AKG

Godel's incompleteness theorem says, in some sense, PA is not strong enough to "govern" any system. There's a sentence [itex]\phi[/itex] such that there are two models [itex]M_1,\ M_2[/itex] such that both satisfy PA, but the first satisfies [itex]\phi[/itex] and the latter satisfies the negation [itex]\neg \phi[/itex]. So PA can't "govern" a system since it's not strong enough to tell systems it tries to govern how to behave, in particular it can't tell its systems whether to satisfy [itex]\phi[/itex] or its negation.

Normally, "true" means "true about the system of natural numbers [itex]\mathbb{N}[/itex]." In this case, there are true facts about [itex]\mathbb{N}[/itex] that PA can't prove.

TylerH

That helps, but the mention of PA was coincidental. In the general sense, does the fact a statement is true within some system imply it is provable within that system? Like with PA, for example, if PA was to be an axiomatic system, independent of other undeniable truths about N, would Goodstein's be true within that system?

AKG

There are structures such as:

• [itex](\mathbb{Q}, <)[/itex] - the rationals with its order structure (so we forget its arithmetic structure)
• [itex](\mathbb{N}, 0, S, +, \times, <)[/itex] - the natural numbers along with the constants, functions, and relations necessary to talk about its arithmetic structure
• [itex](\mathbb{C},0,1,+,-,\times)[/itex] - the complex numbers along with the constants and functions needed to talk about its field structure
• [itex](S_8, \cdot)[/itex] - the symmetric group on 8 elements

Strictly speaking, it doesn't make sense to talk about things being provable from these structures. You can ask about whether certain statements are true in these structures, but not provable from them. Think about what a proof is, it's a set of axioms followed by a finite sequence of steps where each step is some sentence which follows logically from the given axioms. Strictly speaking, a structure like [itex](\mathbb{Q}, <)[/itex] is not a set of axioms, so it doesn't make sense to ask that something be proved from it.

In contrast with structures, we have theories or sets of axioms. These often have TLA's (three letter acronyms :P):

• DLO - the axioms for dense linear orders without endpoints in the (first order) language consisting of one binary symbol
• PA - Peano arithmetic, a set of axioms in the language of number theory
• ZFC - the Zermelo Frankel axioms for set theory, with choice, in a language with one binary relation
• The group axioms
• The field axioms
• ACF₀ - the axioms for an algebraically closed field of characteristic 0

You can ask about what you can prove from these axioms. Remember, since a proof is just a finite sequence of essentially mechanical manipulations, starting with some set of axioms, and producing at each step a new sentence which follows from those axioms by some essentially mechanical rule of inference, the notion of "truth" need not come in to the picture here. Indeed, (at least for now) it doesn't make sense to ask if something is true in PA or in ZFC, since these are just essentially meaningless collections of strings of symbols. So, again, you can ask about things being provable from a set of axioms, but not about things being true in a set of axioms.

Since truth is about structures, and provability is about sets of axioms or sentences, any question of the form, "is everything that's true in X also provable from X?" is ill-formed. Either "true in X" or "provable in X" will not make sense. In particular, when discussing PA, since PA is an axiom system, "true in PA" doesn't make sense.

Of course, there is some connection between the semantic side of things, the structures, and the syntactic side of things, the sentences/axioms. A sentence is, on its own, just a meaningless string of symbols. But a particular structure gives a particular interpretation to the symbols in a sentence, and under such an interpretation we can decide whether the statement is true or false. The field axioms are true in the [itex]\mathbb{C}[/itex] structure mentioned above. The DLO axioms are true in [itex](\mathbb{Q}, <)[/itex]. The ZFC axioms, however, are not true in [itex](\mathbb{Q}, <)[/itex] since interpreting those axioms in the structure [itex](\mathbb{Q}, <)[/itex] would mean [itex]<[/itex] would have to play the role of the membership relation, but then the axiom stating the existence of the empty set would be interpreted in this structure as saying [itex]\exists x \forall y \neq (y < x)[/itex]. And it doesn't even make sense to try to interpret PA in the structure [itex](\mathbb{Q}, <)[/itex]. To summarize this paragraph:

• Given an arbitrary axiom system and arbitrary structure, it might not even make sense to try and interpret those axioms in that structure
• Given an axiom system and a structure in which it does make sense to interpret those axioms, it could be the case that all those axioms are true in that structure, or
• it can also be the case that some of those axioms are false in that structure

Now you might ask: Given a structure [itex]\mathfrak{A}[/itex], can we write down a nice set of axioms [itex]\Sigma[/itex] such that everything that's true in [itex]\mathfrak{A}[/itex] is provable from [itex]\Sigma[/itex]. Now "nice" could mean different things to different people, so one specific kind of "niceness" which I won't define is the property of being recursive. So we may ask whether our favourite structure [itex]\mathfrak{A}[/itex] has a consistent recursive axiomatization. In our list of structures above, the first, third, and fourth have this property. In fact, for the first structure, DLO gives such an axiomatization, and for the third structure, ACF₀ works.

The flip side of this question is: Given a set of axioms [itex]\Sigma[/itex], is there a unique (up to isomorphism) structure satisfying [itex]\Sigma[/itex]? By a corollary to the Compactness Theorem known as the Upwards Lowenheim-Skolem Theorem, the answer is no. In light of that theorem, the best we can hope for is categoricity, that for each infinite cardinal [itex]\kappa[/itex], there is at most one (up to isomorphism) structure of size [itex]\kappa[/itex] which satisfies [itex]\Sigma[/itex]. ACF₀ has this property. Categoricity is rare, and often the best we can hope for is just a particular instance of categoricity. DLO is [itex]\omega[/itex]-categorical, i.e. it has a unique countably infinite model up to isomorphism, namely [itex](\mathbb{Q}, <)[/itex]. However, for any uncountable cardinal [itex]\kappa[/itex], DLO is not [itex]\kappa[/itex]-categorical, i.e. for any uncountable cardinal [itex]\kappa[/itex], you can find two dense linear orders without endpoints, both of size [itex]\kappa[/itex], which aren't isomorphic to one another.

Finally, Goodstein's theorem can be formalized in the language of number theory and said formalization is true once interpreted in the structure [itex](\mathbb{N}, 0, S, +, \times, <)[/itex] but it's not provable from PA.

TylerH

Where's the like button? Seriously though, thanks. That explains it.

AKG

You're welcome! Glad to help.