5 ms·

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 pr

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.

zitterbewegung 10y ago
Seems like you can formulate it using a proof assistant. See http://www.academia.edu/4271278/A_Mechanised_Proof_of_Gödel_s_Incompleteness_Theorems_using_Nominal_Isabelle http://www.academia.edu/4271278/A_Mechanised_Proof_of_Gödel_...
Houshalter 10y ago
The incompleteness theorem says that there exist some (paradoxical and self referencing) true theorems that you can't prove (i.e. "this sentence is unprovable".) Neither humans nor proof assistants should be able to prove them.
- weinzierl 10y ago
  > 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_theorems#Syntactic_form_of_the_G.C3.B6del_sentence https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... [2] https://www.quora.com/Are-there-true-but-unprovable-statements-that-arent-self-referential https://www.quora.com/Are-there-true-but-unprovable-statemen...
  - marcelluspye 10y ago
    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.
    - kxyvr 10y ago
      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 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.
  - klipt 10y ago
    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.)
    - deleted 10y ago
      [deleted]
  - kkylin 10y ago
    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 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_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.
marcelluspye 10y ago
There's a relationship between the incompleteness theorems and the halting problem in that no turing machine can decide whether an arbitrary statement in a logical system where the incompleteness theorems apply is derivable or not. Equivalently, there's no turing machine with input 'statement in the logical system' and outputs a proof or a "unprovable". 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.
- indolering 10y ago
  This problem actually goes back to Descarte's proofs-of-god: in order to solve some problems Descarte needed infinite computational power. Guess who has infinite computational power?
  - Retra 10y ago
    I suppose you could assert that anyone you like has infinite computational power.
Chattered 10y ago
Proof assistants are frequently used to prove the correctness of computer programs. And since a proof assistant is a computer program, and often quite a complex one that could contain bugs that render everything it does useless, you might want to use your proof assistant to prove that its code does what you hope it does. 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....
justifier 10y ago
from the tutorial(o): > 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. (o) https://coq.inria.fr/tutorial-nahas#lab9 https://coq.inria.fr/tutorial-nahas#lab9
- justifier 10y ago
  i'll use the first incompleteness theorem itself to explain this distinction between truth and proof ..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 ..think of complete and incomplete in terms of russell's paradox(i): a set containing all sets; any proof would be incomplete because the evidence for the set containing all sets must also contain itself because it is a set; creating a subsequent requirement for evidence that this new self contained set is also contained in the set of all sets, ad infinitum, perpetually and subsequently incomplete.. 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_theorems#First_incompleteness_theorem https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... (i) https://en.wikipedia.org/wiki/Russell%27s_paradox https://en.wikipedia.org/wiki/Russell%27s_paradox (ii) https://en.wikipedia.org/wiki/Semantics https://en.wikipedia.org/wiki/Semantics (iii) https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theorem https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theo...
MrManatee 10y ago
Here's one interpretation of Gödel's first incompleteness theorem that may help. 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.

zitterbewegung 10y ago

Seems like you can formulate it using a proof assistant. See http://www.academia.edu/4271278/A_Mechanised_Proof_of_Gödel_s_Incompleteness_Theorems_using_Nominal_Isabelle http://www.academia.edu/4271278/A_Mechanised_Proof_of_Gödel_...

Houshalter 10y ago

The incompleteness theorem says that there exist some (paradoxical and self referencing) true theorems that you can't prove (i.e. "this sentence is unprovable".) Neither humans nor proof assistants should be able to prove them.

weinzierl 10y ago
> 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_theorems#Syntactic_form_of_the_G.C3.B6del_sentence https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... [2] https://www.quora.com/Are-there-true-but-unprovable-statements-that-arent-self-referential https://www.quora.com/Are-there-true-but-unprovable-statemen...
- marcelluspye 10y ago
  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.
  - kxyvr 10y ago
    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 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.
- klipt 10y ago
  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.)
  - deleted 10y ago
    [deleted]
- kkylin 10y ago
  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 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_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.

marcelluspye 10y ago

There's a relationship between the incompleteness theorems and the halting problem in that no turing machine can decide whether an arbitrary statement in a logical system where the incompleteness theorems apply is derivable or not. Equivalently, there's no turing machine with input 'statement in the logical system' and outputs a proof or a "unprovable". 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.

indolering 10y ago
This problem actually goes back to Descarte's proofs-of-god: in order to solve some problems Descarte needed infinite computational power. Guess who has infinite computational power?
- Retra 10y ago
  I suppose you could assert that anyone you like has infinite computational power.

Chattered 10y ago

Proof assistants are frequently used to prove the correctness of computer programs. And since a proof assistant is a computer program, and often quite a complex one that could contain bugs that render everything it does useless, you might want to use your proof assistant to prove that its code does what you hope it does. 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....

justifier 10y ago

from the tutorial(o): > 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. (o) https://coq.inria.fr/tutorial-nahas#lab9 https://coq.inria.fr/tutorial-nahas#lab9

justifier 10y ago
i'll use the first incompleteness theorem itself to explain this distinction between truth and proof ..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 ..think of complete and incomplete in terms of russell's paradox(i): a set containing all sets; any proof would be incomplete because the evidence for the set containing all sets must also contain itself because it is a set; creating a subsequent requirement for evidence that this new self contained set is also contained in the set of all sets, ad infinitum, perpetually and subsequently incomplete.. 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_theorems#First_incompleteness_theorem https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... (i) https://en.wikipedia.org/wiki/Russell%27s_paradox https://en.wikipedia.org/wiki/Russell%27s_paradox (ii) https://en.wikipedia.org/wiki/Semantics https://en.wikipedia.org/wiki/Semantics (iii) https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theorem https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theo...

MrManatee 10y ago

Here's one interpretation of Gödel's first incompleteness theorem that may help. 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.