6 ms·

Godel's work has always been incomprehensible to me. no matter how I attempt to understand his theorems, I find them impenetrable. Apparently they are of great

Godel's work has always been incomprehensible to me. no matter how I attempt to understand his theorems, I find them impenetrable. Apparently they are of great consequence, so I'm very interested, but to no avail.

headshock1111 7y ago
I was the same until I watched this: https://www.youtube.com/watch?v=V9ohtKameio https://www.youtube.com/watch?v=V9ohtKameio
rwill128 7y ago
I can relate. My understanding of it thus far leads me to think I can summarize it fairly well though, and I would welcome other people's input or critique on this. It seems like it's so consequential because he demonstrated that no matter what kind of mathematical system you're using -- and no matter how much mathematics generally speaking develops -- there will be objectively true mathematical statements within that system that can't be proven. If that part of my understanding is correct, the part that's really interesting to me is whether we can know these true statements to be true, despite them not having proofs. This is where I could be misunderstanding things I suppose, but it suggests there's a disconnect between what's knowable and what's provable, and furthermore, that we can know more than we can prove. To actual seasoned mathematicians: is this a really naive interpretation of what I've read, or not?
- SomeOldThrow 7y ago
  > If that part of my understanding is correct, the part that's really interesting to me is whether we can know these true statements to be true, despite them not having proofs. There may be proofs, just using different fundamental axioms. The finding is that there is no initial set of axioms that by themselves allow proving all provable truths.
- xamuel 7y ago
  You need to be a bit more specific: no matter what kind of true, computable axiom-set you're using (this has nothing to do with 'how much mathematics generally speaking develops'), there will be objectively true mathematical statements that can't be proven by that axiom-set. >a disconnect between what's knowable and what's provable "what's provable [from a given axiom-set]" is a concrete, technical, unambiguously defined set of things. "what's knowable" is a vague philosophical set of things. Goedel's Incompleteness Theorem is a technical result about the former, and it's a common mistake to assume it says anything about the latter, except very tangentially. For those who are interested in the misty area where the two things do overlap, I will shamelessly plug this 2-page paper of mine, "Mathematical shortcomings in a simulated universe": https://philpapers.org/archive/ALEMSI.pdf https://philpapers.org/archive/ALEMSI.pdf
  - guerrilla 7y ago
    I think they meant what is true, which is also concrete, technical and unambiguously defined in this setting. But you are very correct to make the distinction between truth and knowledge. Pointing out that many philosophers have believed that knowledge is justified true belief might elucidate the relationship a bit.
- guerrilla 7y ago
  You're thinking of his incompleteness theorems, not this completeness theorem for first order logic. My response to the parent covers both.
lacker 7y ago
Do you understand Turing's proof that the halting problem is undecidable? Godel's proof of the incompleteness of mathematics is really the same thing. He just did his proofs before computers were invented so a lot of his explanations are needlessly complicated by modern-talking-about-algorithms standards.
guerrilla 7y ago
I wonder if a slightly higher level explanation might help. If any real mathemeticians are around, please correct me if I'm inaccurate. An alphabet is a set of symbols. Symbols can be combined by the operation of concatenation to form strings. Strings either satisfy a property of being a syntactically valid or not. Let those strings that satisfy the property of syntactic validity be called sentences. The set of all sentences that are syntactically valid is called a language. I think the trick to understanding this particular theorem of Gödel is to know that in such formal systems there is a difference between semantic consequence (which is about truth) and syntactic consequence (which is about proof). A sentence is provable if it is derivable from other sentences of the language by applying certain syntactic transformation rules (inference rules) to them. On the other hand, a sentence of the language is logically valid if it is true under all possible interpretations (sorting out what this means is what model theory does for you.) If every sentence that is provable is logically valid then the system has the property of soundness. If every sentence that is logically valid is provable then the system has the property of completeness. The systems are designed so that we only need to do this syntatic manipulation, much like algebra, to produce proofs, but we always have a map giving us the meaning of any given sentence. This is in fact what "formal" means in this context: that in proofs we're only looking at the form (syntax) of the sentences and not the interpretation/meaning (semantics) of any of the sentences. To re-iterate: Something can be true but not provable, i.e. in any incomplete system. Something can be provable but not true, i.e. in an unsound system. If everything that can be proven is true, then the system is sound. If everything that is true can be proven, then the system is complete. First-order logic is sound and complete. Now when a system is extended with artihmetic, then due to Gödel numbering, it is suddenly capable of a form self-reference. This allows a system to state metatheorems about itself. If it can do this, then it is necessarily incomplete. In particular, it cannot prove its own consistency.
tel 7y ago
It is pretty incomprehensible. It relates to the nature of words like "proof" and just, without and doubt, those are tricky concepts. There's also a lot of implied background. It sounds simple to say what's going on in informal language and hope that it makes sense. That's not true, however. The statement of the theorem relies on the machinery of formal proof. That machinery and, more importantly, it's relation to day-to-day reasoning is big and complicated. --- A formal theorem is a statement in a language about the world. Typically speaking, these statements are not interesting without "quantification", the use of terms like "for all" or "there exists". Quantification makes formal theorems powerful by letting them speak about an entire universe of things all at once. The meaning of quantification is difficult. A sentence like "For all x, E(x)" is a discussion of the nature of the "universe" of x's. Sometimes we even refer to that explicitly when we say "For all x in X, E(x)" and upper-case X is that universe itself. For the theorem to be true, we need to not only pick an explicit universe X and then show that E(x) is true for any choice of x in X, but also we often have to show that this whole process continues to work no matter which universe X is chosen. This is the power of universality: making such an incredibly wide-reaching claim. (From a programming perspective this is the difference between types and tests. Tests show E(x) for all kinds of interesting x's. Types show "for all x in X, E(x)". There's some magic to this.) So one kind of way to show the validity of a theorem is to enumerate all universes (at least all of those that are considered "compatible" with the theorem) and then show that all choices of elements from that universe support the statement of the theorem. This is considered to be "semantic" meaning in that it's how theorems are practically useful. We only care about theorems when they've been instantiated in a practical way. Their value comes out of how freely we can choose to instantiate them. But there's another tricky way. Formal proofs are (usually) data structures constructed cleverly so that their shape relates to the syntactic structure of a theorem. They exploit the compositional nature of the theorem language and afford means to manipulate theorems (and their corresponding proofs) in a purely mechanical way. For instance, if I have theorems A and B as well as formal proofs of those theorems, a and b respectively, then I can have a proof of the composed theorem (A & B) by composing the sub-proofs together into a tuple like (a, b). This is a totally mechanical exploitation of the structure of (formal) proofs and theorems. The benefit of formal proofs is that syntactic manipulation can be verified very quickly. Given a theorem T and a (potential) proof P I can tell you whether P actually proves T very quickly. It's very difficult to find a proof P given only a theorem T. It's very difficult to write a theorem T which matches what you're interested in, but if you've got them all then I can verify your proof quickly. On the other hand, actually checking every universe where your theorem might hold and proving that it does is expensive no matter how you cut it. We'd like to be able to skip over that work. And that's what Gödel Completeness does. Gödel showed that when a theorem holds in all possible universes (it has semantic meaning) then there must be a formal proof of it (it has syntactic meaning). Since we're generally interested in semantic meaning (e.g. the applicability of a theorem to whichever universe(s) we happen to care about) then we're very excited to learn that syntactic meaning will mirror that semantic meaning. Without Completeness, syntactic proofs would still be valuable. A syntactic proof still implies semantic validity. What wouldn't be true is the applicability of syntactic reasoning. Maybe there are tons of important theorems out there which are true but can only be shown to be true through exhaustive enumeration? Suddenly mathematics as an act of human communication is fraught---many interesting things can only be explained exhaustively. There's often no way to "compress" meaning down into a pithy proof. But, no, completeness holds and formal proofs hold exactly the position of meaning we'd hope that they would. Well. At least for first-order theories.

headshock1111 7y ago

I was the same until I watched this: https://www.youtube.com/watch?v=V9ohtKameio https://www.youtube.com/watch?v=V9ohtKameio

rwill128 7y ago

I can relate. My understanding of it thus far leads me to think I can summarize it fairly well though, and I would welcome other people's input or critique on this. It seems like it's so consequential because he demonstrated that no matter what kind of mathematical system you're using -- and no matter how much mathematics generally speaking develops -- there will be objectively true mathematical statements within that system that can't be proven. If that part of my understanding is correct, the part that's really interesting to me is whether we can know these true statements to be true, despite them not having proofs. This is where I could be misunderstanding things I suppose, but it suggests there's a disconnect between what's knowable and what's provable, and furthermore, that we can know more than we can prove. To actual seasoned mathematicians: is this a really naive interpretation of what I've read, or not?

SomeOldThrow 7y ago
> If that part of my understanding is correct, the part that's really interesting to me is whether we can know these true statements to be true, despite them not having proofs. There may be proofs, just using different fundamental axioms. The finding is that there is no initial set of axioms that by themselves allow proving all provable truths.
xamuel 7y ago
You need to be a bit more specific: no matter what kind of true, computable axiom-set you're using (this has nothing to do with 'how much mathematics generally speaking develops'), there will be objectively true mathematical statements that can't be proven by that axiom-set. >a disconnect between what's knowable and what's provable "what's provable [from a given axiom-set]" is a concrete, technical, unambiguously defined set of things. "what's knowable" is a vague philosophical set of things. Goedel's Incompleteness Theorem is a technical result about the former, and it's a common mistake to assume it says anything about the latter, except very tangentially. For those who are interested in the misty area where the two things do overlap, I will shamelessly plug this 2-page paper of mine, "Mathematical shortcomings in a simulated universe": https://philpapers.org/archive/ALEMSI.pdf https://philpapers.org/archive/ALEMSI.pdf
- guerrilla 7y ago
  I think they meant what is true, which is also concrete, technical and unambiguously defined in this setting. But you are very correct to make the distinction between truth and knowledge. Pointing out that many philosophers have believed that knowledge is justified true belief might elucidate the relationship a bit.
guerrilla 7y ago
You're thinking of his incompleteness theorems, not this completeness theorem for first order logic. My response to the parent covers both.

lacker 7y ago

Do you understand Turing's proof that the halting problem is undecidable? Godel's proof of the incompleteness of mathematics is really the same thing. He just did his proofs before computers were invented so a lot of his explanations are needlessly complicated by modern-talking-about-algorithms standards.

guerrilla 7y ago

I wonder if a slightly higher level explanation might help. If any real mathemeticians are around, please correct me if I'm inaccurate. An alphabet is a set of symbols. Symbols can be combined by the operation of concatenation to form strings. Strings either satisfy a property of being a syntactically valid or not. Let those strings that satisfy the property of syntactic validity be called sentences. The set of all sentences that are syntactically valid is called a language. I think the trick to understanding this particular theorem of Gödel is to know that in such formal systems there is a difference between semantic consequence (which is about truth) and syntactic consequence (which is about proof). A sentence is provable if it is derivable from other sentences of the language by applying certain syntactic transformation rules (inference rules) to them. On the other hand, a sentence of the language is logically valid if it is true under all possible interpretations (sorting out what this means is what model theory does for you.) If every sentence that is provable is logically valid then the system has the property of soundness. If every sentence that is logically valid is provable then the system has the property of completeness. The systems are designed so that we only need to do this syntatic manipulation, much like algebra, to produce proofs, but we always have a map giving us the meaning of any given sentence. This is in fact what "formal" means in this context: that in proofs we're only looking at the form (syntax) of the sentences and not the interpretation/meaning (semantics) of any of the sentences. To re-iterate: Something can be true but not provable, i.e. in any incomplete system. Something can be provable but not true, i.e. in an unsound system. If everything that can be proven is true, then the system is sound. If everything that is true can be proven, then the system is complete. First-order logic is sound and complete. Now when a system is extended with artihmetic, then due to Gödel numbering, it is suddenly capable of a form self-reference. This allows a system to state metatheorems about itself. If it can do this, then it is necessarily incomplete. In particular, it cannot prove its own consistency.

tel 7y ago

It is pretty incomprehensible. It relates to the nature of words like "proof" and just, without and doubt, those are tricky concepts. There's also a lot of implied background. It sounds simple to say what's going on in informal language and hope that it makes sense. That's not true, however. The statement of the theorem relies on the machinery of formal proof. That machinery and, more importantly, it's relation to day-to-day reasoning is big and complicated. --- A formal theorem is a statement in a language about the world. Typically speaking, these statements are not interesting without "quantification", the use of terms like "for all" or "there exists". Quantification makes formal theorems powerful by letting them speak about an entire universe of things all at once. The meaning of quantification is difficult. A sentence like "For all x, E(x)" is a discussion of the nature of the "universe" of x's. Sometimes we even refer to that explicitly when we say "For all x in X, E(x)" and upper-case X is that universe itself. For the theorem to be true, we need to not only pick an explicit universe X and then show that E(x) is true for any choice of x in X, but also we often have to show that this whole process continues to work no matter which universe X is chosen. This is the power of universality: making such an incredibly wide-reaching claim. (From a programming perspective this is the difference between types and tests. Tests show E(x) for all kinds of interesting x's. Types show "for all x in X, E(x)". There's some magic to this.) So one kind of way to show the validity of a theorem is to enumerate all universes (at least all of those that are considered "compatible" with the theorem) and then show that all choices of elements from that universe support the statement of the theorem. This is considered to be "semantic" meaning in that it's how theorems are practically useful. We only care about theorems when they've been instantiated in a practical way. Their value comes out of how freely we can choose to instantiate them. But there's another tricky way. Formal proofs are (usually) data structures constructed cleverly so that their shape relates to the syntactic structure of a theorem. They exploit the compositional nature of the theorem language and afford means to manipulate theorems (and their corresponding proofs) in a purely mechanical way. For instance, if I have theorems A and B as well as formal proofs of those theorems, a and b respectively, then I can have a proof of the composed theorem (A & B) by composing the sub-proofs together into a tuple like (a, b). This is a totally mechanical exploitation of the structure of (formal) proofs and theorems. The benefit of formal proofs is that syntactic manipulation can be verified very quickly. Given a theorem T and a (potential) proof P I can tell you whether P actually proves T very quickly. It's very difficult to find a proof P given only a theorem T. It's very difficult to write a theorem T which matches what you're interested in, but if you've got them all then I can verify your proof quickly. On the other hand, actually checking every universe where your theorem might hold and proving that it does is expensive no matter how you cut it. We'd like to be able to skip over that work. And that's what Gödel Completeness does. Gödel showed that when a theorem holds in all possible universes (it has semantic meaning) then there must be a formal proof of it (it has syntactic meaning). Since we're generally interested in semantic meaning (e.g. the applicability of a theorem to whichever universe(s) we happen to care about) then we're very excited to learn that syntactic meaning will mirror that semantic meaning. Without Completeness, syntactic proofs would still be valuable. A syntactic proof still implies semantic validity. What wouldn't be true is the applicability of syntactic reasoning. Maybe there are tons of important theorems out there which are true but can only be shown to be true through exhaustive enumeration? Suddenly mathematics as an act of human communication is fraught---many interesting things can only be explained exhaustively. There's often no way to "compress" meaning down into a pithy proof. But, no, completeness holds and formal proofs hold exactly the position of meaning we'd hope that they would. Well. At least for first-order theories.