I'm no mathematician and this might be way out of my league, but I've wondered how Gödel's incompleteness theorems come into play if Mathematicians are using proof assistants to verify their mathematics.
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...
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.
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.
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").
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.)
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.
"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).
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.
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.
> IT IS VITALLY IMPORTANT THAT YOU DO NOT THINK OF A Prop AS BEING EITHER "TRUE" OR "FALSE". A Prop either has a proof or it does not have a proof. Godel shattered mathematics by showing that some true propositions can never proven. Tarski went further and showed that some propositions cannot even said be to be true or false!!! Coq deals with these obstacles in modern mathematics by restricting Prop to being either proven or unproven, rather than true or false.
..the first because the second is essentially a stronger form of the first..
> First Incompleteness Theorem: "Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there are statements of the language of F which can neither be proved nor disproved in F." (o)
what's important is the statements are incapable of being proved or disproved, to me this is confusing language, let me try to show the possibilities
a statement can be:
o. proved : there exists at least one complete collection of validating evidence
i. disproved : there exists at least one complete collection of confuting evidence
ii. incapable of being proved : there only exists incomplete collections of validating evidence
iii. incapable of being disproved : there only exists incomplete collections of confuting evidence
the first incompleteness theorem is making a claim for the existence of ii and iii
if this statement is true how could you prove it?
if the statement is true it means you would need to prove that specific statements in the language of F are incapable of being proved or disproved, but if the statements themselves are incapably proved or disproved how can you express through evidence that your proof is even working on those same statements
a theorem is proved or disproved when one can express through finite steps, or statements of evidence, a proof
if a theorem has an incomplete proof or disproof how could i prove said incomplete proof?
but we know the statement to be true because that is how it essentially self references
by stating there are statements being incapably proved or disproved is itself incapable of being proved or disproved
making the statement true, but without proof of evidence
..except some strange brain itching intuition :P ..
but now we have left the domain of arithmetic and entered the domain of semantics(ii)
and here is where tarski comes in with his undefinability theorem{iii)
..is it irony that undefinability is underlined by this spell checker?..
coq is stating here that it is itself a semantic domain only dealing with arithmetic statements that can be proved or disproved
implying imperatively to avoid the incomplete and undefined because they explicitly and by design exist outside of this proof assistant's restricted domain of interest and so will be inexpressible
naively, if you wrote a program with the restriction of only computing the addition of positive integers; if you wanted to add using a negative integer you would have to write a new program
which going back to your original question:
> I've wondered how Gödel's incompleteness theorems come into play if Mathematicians are using proof assistants to verify their mathematics
they come into play only by being the very things that are disallowed in the spec from coming into play
in coq at least, you are required to work without them because it is written to only play with propositions that can be proved or disproved
and we showed above they are unable to be proved or disproved
(o) https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
(i) https://en.wikipedia.org/wiki/Russell%27s_paradox
(ii) https://en.wikipedia.org/wiki/Semantics
(iii) https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theo...
However, once you already have a proof, checking is much easier (at the formal level). Modern mathematical proofs, however, are not generally written in a fashion in any way similar to how the formal system operates, so applying this in practice is non-trivial.
First, let's look at computability. The intuitive idea that some functions can be computed by an algorith is very old (think Euclid's algorithm). The idea was formalized in the 20th century by the notion of a computable function. Several different definitions were given, but surprisingly, they turned out to be equivalent. Today, most programming languages are Turing complete. As far as pure computation is concerned, it is possible to translate between different programming languages.
The idea that a mathematical statement can be conclusively proven is also very old. Again, different formal definitions emerged: provable in PA, provable in ZFC, provable in ZFC + some large cardinal axiom, etc. These are not equivalent. And this, in a sense, is one way of framing Gödel's first incompleteness theorem. There is no absolute notion of provability: no equivalent of Turing completeness; no precisely definable concept that would deserve the name "provable".
In particular, this means that it is not always possible to translate proofs from one system A to system B. At least unless you are willing to add new axioms to system B.
Goedel's second incompleteness theorem says you can't do that. Ever. And more generally, it says that you will hit a roadblock as you try to prove what it is that your proof assistant does. This is really annoying.
But you can get pretty damn close. HOL Light has something of a self-consistency proof that is so close to the real thing that it's worth taking seriously.
But incompleteness, by itself, isn't a big deal for theorem provers. Russell himself worked as if the existence of infinities wasn't provable, which is why Goedel had little relevance to Russell. Hilbert on the other hand....