5 ms·

If Godel's theorem applies to all formal systems. Then in formalizing Godel's theorem, doesn't that make the theorem apply to itself? So the calculus that form

If Godel's theorem applies to all formal systems. Then in formalizing Godel's theorem, doesn't that make the theorem apply to itself? So the calculus that formalises the theorem is either inconsistent or there are other true statements about it that can't be proven? Which is it? Can someone with a bigger brain elaborate on how the theorem applies to itself in a language for tiny brained people? No big words please.

jameshart 4y ago
I think the short version is: just because any formal system is guaranteed to be incomplete doesn't mean it can't prove useful things. And even an incomplete formal system can prove Gödel's Incompleteness Theorem.
birriel 4y ago
I asked a similar question a while back: https://news.ycombinator.com/item?id=27915824 https://news.ycombinator.com/item?id=27915824
irq-1 4y ago
> true statements about it that can't be proven? Its missing the qualifier: can't be proven in that system. They can be examined from outside the system, or say, with a different system.
- qiskit 4y ago
  The problem still continues. Even if you add the unprovable formula ( lets say formula1) in System1 as an axiom to System2 ( System1 + formula1 ), System2 will have its own unprovable formulas even though formula1 would be superficially provable in System2. You could add the unprovable formulas in System2 as axioms to System3 but System3 will have its own unprovable formulas . Godel showed that it's simply the nature of any formal system with complexity greater than or equal to arithmetic.
bumbledraven 4y ago
Godel’s incompleteness theorems are about formal systems. A formal system can be thought of as an algorithm that takes a purported formal proof of some arithmetical statement (e.g. there is no largest twin prime) and returns true/false depending on whether the proof is correct. Call the algorithm a “proof checker” and say it “accepts” a statement if it returns true for some purported proof of the statement. Godel’s first incompleteness theorem says that at least one of the following is true: (1) There is some statement such that the checker accepts both the statement and the statement’s negation (e.g. the checker accepts both “2 + 2 = 4” and “2 + 2 ≠ 4”). This is called inconsistency. (2) There is some true statement which the checker will not accept. This is called incompleteness. Since Godel’s first incompleteness theorem is not a formal system, it does not apply to itself.
- joshuaissac 4y ago
  There are two more options: (3) The system's axioms are not finitely enumerable (i.e. not finite, and cannot be generated by a generator of finite length; e.g. a system where every true statement is an axiom and there are infinitely many axioms) (4) The system is not complex enough to express arithmetic (e.g. propositional calculus)
  - bumbledraven 4y ago
    Good point. For (3), I should have said something about the axioms being computable. I think I already excluded cases like (4) by stating that the checker operates on "arithmetical statement[s]".
    - Tainnor 4y ago
      > I think I already excluded cases like (4) by stating that the checker operates on "arithmetical statement[s]". It's at least a bit vague, I think you need something that is at least as strong as Robinson arithmetic. In particular, I believe that if you throw out multiplication (or addition, and keep multiplication), you get a complete theory.
- deltaonefour 4y ago

jameshart 4y ago

I think the short version is: just because any formal system is guaranteed to be incomplete doesn't mean it can't prove useful things. And even an incomplete formal system can prove Gödel's Incompleteness Theorem.

birriel 4y ago

I asked a similar question a while back: https://news.ycombinator.com/item?id=27915824 https://news.ycombinator.com/item?id=27915824

irq-1 4y ago

> true statements about it that can't be proven? Its missing the qualifier: can't be proven in that system. They can be examined from outside the system, or say, with a different system.

qiskit 4y ago
The problem still continues. Even if you add the unprovable formula ( lets say formula1) in System1 as an axiom to System2 ( System1 + formula1 ), System2 will have its own unprovable formulas even though formula1 would be superficially provable in System2. You could add the unprovable formulas in System2 as axioms to System3 but System3 will have its own unprovable formulas . Godel showed that it's simply the nature of any formal system with complexity greater than or equal to arithmetic.

bumbledraven 4y ago

Godel’s incompleteness theorems are about formal systems. A formal system can be thought of as an algorithm that takes a purported formal proof of some arithmetical statement (e.g. there is no largest twin prime) and returns true/false depending on whether the proof is correct. Call the algorithm a “proof checker” and say it “accepts” a statement if it returns true for some purported proof of the statement. Godel’s first incompleteness theorem says that at least one of the following is true: (1) There is some statement such that the checker accepts both the statement and the statement’s negation (e.g. the checker accepts both “2 + 2 = 4” and “2 + 2 ≠ 4”). This is called inconsistency. (2) There is some true statement which the checker will not accept. This is called incompleteness. Since Godel’s first incompleteness theorem is not a formal system, it does not apply to itself.

joshuaissac 4y ago
There are two more options: (3) The system's axioms are not finitely enumerable (i.e. not finite, and cannot be generated by a generator of finite length; e.g. a system where every true statement is an axiom and there are infinitely many axioms) (4) The system is not complex enough to express arithmetic (e.g. propositional calculus)
- bumbledraven 4y ago
  Good point. For (3), I should have said something about the axioms being computable. I think I already excluded cases like (4) by stating that the checker operates on "arithmetical statement[s]".
  - Tainnor 4y ago
    > I think I already excluded cases like (4) by stating that the checker operates on "arithmetical statement[s]". It's at least a bit vague, I think you need something that is at least as strong as Robinson arithmetic. In particular, I believe that if you throw out multiplication (or addition, and keep multiplication), you get a complete theory.
deltaonefour 4y ago