> there exist some true theorems that you can't prove.

Emphasis mine.

Are all unprovable theorems true? I googled "are all Gödel sentences true", but came up with nothing. Also: Are all unprovable theorems Gödel sentences or are there other kinds?

EDIT: Lots of good answers to my first question, thanks a lot to everyone. For the second one I think I also found an answer:

According to the Wikipedia article about the incompleteness theorems [1]: "The Gödel sentence is designed to refer, indirectly, to itself." So the question really is if there are non self-referential unprovable statements, and the answer seems to be yes[2].

[1] https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...

[2] https://www.quora.com/Are-there-true-but-unprovable-statemen...

I'm not a logician, but I think the question (a good one) is not quite well-posed. As I understand, in mathematical logic, a statement being provable means one can deduce it from a set of axioms. If you have a set of axioms A sufficiently powerful for Godel's construction to go through, the resulting Godel sentence s is (by construction) not provable from A, but one can always make it provable by appending s to the axioms A.

For a statement to be true, on the other hand, has a technical meaning: it means that there is a model (in the sense of model theory, see https://en.wikipedia.org/wiki/Model_theory ) in which both the axioms A and the sentence s are true. Godel's completeness theorem (https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_th...) asserts that s is provable from A if and only if s is true in every model in which A holds.

It's a bit confusing to say that about the Completeness theorem without noting that it only applies to first order logic. It's not generally true.

Yet first order logic encompasses 99.9% of the mathematics anyone ever does, even professional mathematicians. The only people who consider anything but first order logic are people who have gone out of their way to make a point to study it just for its own sake. When the general subject of discussion is proof assistants and proofs in normal mathematics, I don't think it's necessary to constantly mention "only in first order logic". It's like discussing structural integrity of a building and constantly mentioning that all the calculations only hold on in our reality, but if we were living in an alternate dimension and the physical constants of the universe were different then the results wouldn't be applicable.

>Yet first order logic encompasses 99.9% of the mathematics anyone ever does, even professional mathematicians.

I'm way out of my depth here, but I'm curious about this statement. In first order logic you can't even assert that the natural numbers cannot be put into a one-to-one correspondence with the real numbers, which seems like a fairly basic mathematical fact.

You can, as long as your first-order statement is in the language of set theory, by translating "there does not exist a bijective function f: N->R".

Right, but you can't ensure that the only models of 'bijective functions' are actually bijective functions. To switch to a slightly simpler example, you can translate statements such as "x is finite" into a first order language (for example, set theory), but you can't ensure that x actually is finite in the models of this statement.

To your first point: yeah, some discomfort around it is valid, but I see it as a non-issue. Informally/philosophically, because a model's job is to capture everything a first-order theory can see about your object of study - so it's fine for (say) an "actually" countable set to model the reals, and not be up to the task of "actually being" the reals. Formally, you differentiate between internal and external statements and don't expect them to be the same (a rigorous version of my pretentious use of scare quotes above :).

It might be helpful to be a bit more precise here.

The expression "first-order logic" (FOL) is a bit vague. Do you mean pure FOL (i.e. all axioms are about equality) or FOL plus additional axioms? Pure FOL (without additional axioms) is indeed rather weak and cannot be used for much. That's why mathematicians build a foundation of mathematics on top of FOL by assuming the truth of additional axioms.

The most well known foundation of mathematics built on top of FOL is ZF-set theory which adds about a dozen additional axioms about how to construct new sets from old, and when two sets are equal.

There are other FOL-based axiomatisations of mathematics such as Quine's NF, or category theory (which can be expressed as a theory on top of FOL). There are also foundations of mathematics that are not using FOL (Martin-Loef type theory and successors such as HoTT).

Goedel's first incompleteness theorem forces all those axiomatisations of mathematics to be incomplete, meaning there are formulae A such that neither A nor the negation of A can be derived.

A statement like "99.9% of the mathematics anyone ever does" is about FOL extended with foundations of mathematics like ZF, or a type-theoretic equivalent.

However, mathematicians are getting ever better at producing interesting formulae whose truth (or otherwise) cannot be settled in ZF (or similar) [1]. In order to deal with such expressivity gaps, mathematicians investigate more powerful axioms, called "large cardinals", which claim the existence of certain extremely large sets. You can also think of them as more powerful induction principles.

The problem with inventing new large cardinals (i.e. more powerful induction principles) is to navigate between the Scylla of expressive weakness (the axiom is a consequence of other axioms) and the Charybdis of inconsistency (adding the axiom allows us to derive "false").

[1] https://u.osu.edu/friedman.8/

Yes, I was being sloppy. Thanks for the clarification.

In consistent systems, false theorems are always unprovable.

So it's only interesting when unprovable theorems are true.

(If you're looking for a false theorem that isn't disprovable, simply negate an unprovable true theorem.)

>So the question really is if there are non self-referential unprovable statements, and the answer seems to be yes

Some mathematicians believe that many popular conjectures are true but unprovable. Like Goldbach's conjecture, Riemann's hypothesis, or perhaps even the collatz conjecture.

We know these things are probably true. If the prime numbers are distributed randomly, there are probabilistic proofs that show the probability of goldbach's conjecture approaches 1, and there is a similar argument for Riemann's hypothesis. However it's just a "mathematical coincidence", there is no reason there can't be a counterexample at 10^500+1, it's just really improbable, so it's impossible to prove.

"Very difficult to find a counter example" =/= "unprovable"

No, the point is that there are no counterexamples. The probability of any counterexamples existing decreases exponentially, but is nonzero. So there is a 99.999...% chance that no counterexamples exist, and therefore it is true. But it's impossible to ever prove that.

> Are all unprovable theorems true?

"True" in this context means "conforms to my intuitive understanding of what true means".

Gödel sentences are an elaborate construction that express the concept "This sentence is unprovable from $AXIOMS" without using direct self-reference, but this construction only means what we think it means if the natural numbers are the "real" natural numbers.

Because no finite set of axioms can rule out all nonstandard models, you can't be sure that there isn't some "proof" corresponding to a nonstandard number.

If such a thing exists, the Gödel sentence is still unprovable (because no proof exists) but false (because it asserts that no "proof" exists, although there is a nonstandard one).

No. The definition of "undecidable" is that you can't prove it true or false. This means that if P is undecidable then so is not-P. But exactly one of these is true and the other false

This seems a little glib wrt the meaning of something being "true". We have undecidability results: the Axiom of Choice and its negation are both consistent with the Zermelo-Frankel axioms. The continuum hypothesis and its negation are both consistent with the ZFC axioms. The Parallel Postulate and its negation are both consistent with the other Euclidean axioms.

Are we justified in saying that for each of these, one must be true and the other false? Of course not. To resolve them one way or the other, you need additional axioms; none of those six propositions is true platonically. What you choose depends on the problem you're trying to describe.

Well, for one thing, you have to define 'true'. The incompleteness theorems don't have anything to do with what's 'true', they have to do with what's 'derivable'.

It's a consequence of the completeness theorem that every consistent theory has a model. Furthermore, in any incomplete system whereby a Godel sentence is useful, there are necessarily models that differ on the satisfaction of the Godel sentence.

Slightly off topic, but your comment reminded me of Tarski's paper The Semantic Conception of Truth and the Foundations of Semantics (http://www.jfsowa.com/logic/tarski.htm) Basically, it's actually kind of hard to define what true means and Tarski goes through a long discussion trying to pin it down.

If all unprovable theorems were true and you could prove that statement then you'd have proven the unprovable. So no.