5 ms·

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 arithme

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
>Since Godel’s first incompleteness theorem is not a formal system, it does not apply to itself. Except the author is formalizing the theorem. Meaning the theorem is based off a formal system. That means the system itself that was created to derive this theorem is either incomplete or inconsistent. So Yes it does 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

>Since Godel’s first incompleteness theorem is not a formal system, it does not apply to itself. Except the author is formalizing the theorem. Meaning the theorem is based off a formal system. That means the system itself that was created to derive this theorem is either incomplete or inconsistent. So Yes it does apply to itself.