4 ms·

The Dedekind/Peano higher order theory of the natural numbers prove its own formal consistency. In this theory, proof checking is computationally decidable eve

The Dedekind/Peano higher order theory of the natural numbers prove its own formal consistency. In this theory, proof checking is computationally decidable even though the theorems are not computationally enumerable by a total procedure.

wk_end 8y ago
> The Dedekind/Peano higher order theory of the natural numbers prove its own formal consistency. No it doesn't - that would contradict Goedel's well-established theorem. The formal consistency of Peano arithmetic has been proven, but not by Peano arithmetic: > Gentzen's theory obtained by adding quantifier-free transfinite induction to primitive recursive arithmetic proves the consistency of first-order Peano arithmetic (PA) but does not contain PA [...] Gentzen's theory is not contained in PA, either, however, since it can prove a number-theoretical fact—the consistency of PA—that PA cannot. [1] [1] https://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof#Relation_to_Hilbert's_program_and_G%C3%B6del's_theorem https://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof#...
- carlehewitt 8y ago
  Godel's results are for the 1st order variant of the Dedekind/Peano theory of the natural numbers. Consequently, there is no contradiction with the inferential completeness (every proposition is provable or disprovable) or self-provability of formal consistency in the higher order theory. Also, Godel's proposition "I'mUnprovable" does not exist in the higher order theory because it doesn't type check. See https://hal.archives-ouvertes.fr/hal-01566393 https://hal.archives-ouvertes.fr/hal-01566393
- johncolanduoni 8y ago
  What's being proposed is a analogue of Peano arithmetic that isn't effectively axiomatized (i.e. the axioms are not recursively enumerable), and therefore not subject to Goedel's theorems. That isn't usually palatable in a formal theory, and therefore not what most mathematicians would think "Peano arithmetic is consistent" means.
  - carlehewitt 8y ago
    Of course, [Dedekind 1888] famously proved that the higher order theory characterized the natural numbers up to a unique isomorphism, which is impossible in the first order variant of this theory, which was developed later. Proof checking is computationally decidable in the higher order theory, which means that it is "effectively axiomatized." The fact that the theorems of the higher order theory cannot be computationally enumerated by a provably total procedure is irrelevant because, in practice, it does no good to enumerate the theorems.
    - johncolanduoni 8y ago
      That is not the definition of effectively axiomatizable as required for Godel's theorem to apply, which is that the axioms be recursively enumerable (not the theorems, which I agree is of little use aside from metatheory). I also don't understand how proof checking can be decidable if the axioms are not recursively enumerable. If proof checking is decidable, there must be a way of determining if a use of an axiom refers to a valid axiom. But if you can do that, as long as you can put the syntactic formulas of the system in bijection with the natural numbers (which I presume is the case if this is aimed at computing, and would hope in general that you can write them on paper using a finite string of symbols) you can produce an enumerating program by just running the decision procedure on every syntactic formula and only emitting ones that pass. More succinctly, all recursive sets are recursively enumerable.
      - carlehewitt 8y ago
        The axioms of the higher order theory of the natural numbers are not countable and consequently not computationally enumerable. For example, there are uncountable many instances of the higher order induction axiom. Consequently, there are axioms that are not expressible as the abstractions of finite strings, just as there are real numbers that are not expressible as the abstractions of finite strings. But proof checking is still computationally decidable by a provably total higher order procedure. See the following: https://hal.archives-ouvertes.fr/hal-01566393 https://hal.archives-ouvertes.fr/hal-01566393

wk_end 8y ago

> The Dedekind/Peano higher order theory of the natural numbers prove its own formal consistency. No it doesn't - that would contradict Goedel's well-established theorem. The formal consistency of Peano arithmetic has been proven, but not by Peano arithmetic: > Gentzen's theory obtained by adding quantifier-free transfinite induction to primitive recursive arithmetic proves the consistency of first-order Peano arithmetic (PA) but does not contain PA [...] Gentzen's theory is not contained in PA, either, however, since it can prove a number-theoretical fact—the consistency of PA—that PA cannot. [1] [1] https://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof#Relation_to_Hilbert's_program_and_G%C3%B6del's_theorem https://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof#...

carlehewitt 8y ago
Godel's results are for the 1st order variant of the Dedekind/Peano theory of the natural numbers. Consequently, there is no contradiction with the inferential completeness (every proposition is provable or disprovable) or self-provability of formal consistency in the higher order theory. Also, Godel's proposition "I'mUnprovable" does not exist in the higher order theory because it doesn't type check. See https://hal.archives-ouvertes.fr/hal-01566393 https://hal.archives-ouvertes.fr/hal-01566393
johncolanduoni 8y ago
What's being proposed is a analogue of Peano arithmetic that isn't effectively axiomatized (i.e. the axioms are not recursively enumerable), and therefore not subject to Goedel's theorems. That isn't usually palatable in a formal theory, and therefore not what most mathematicians would think "Peano arithmetic is consistent" means.
- carlehewitt 8y ago
  Of course, [Dedekind 1888] famously proved that the higher order theory characterized the natural numbers up to a unique isomorphism, which is impossible in the first order variant of this theory, which was developed later. Proof checking is computationally decidable in the higher order theory, which means that it is "effectively axiomatized." The fact that the theorems of the higher order theory cannot be computationally enumerated by a provably total procedure is irrelevant because, in practice, it does no good to enumerate the theorems.
  - johncolanduoni 8y ago
    That is not the definition of effectively axiomatizable as required for Godel's theorem to apply, which is that the axioms be recursively enumerable (not the theorems, which I agree is of little use aside from metatheory). I also don't understand how proof checking can be decidable if the axioms are not recursively enumerable. If proof checking is decidable, there must be a way of determining if a use of an axiom refers to a valid axiom. But if you can do that, as long as you can put the syntactic formulas of the system in bijection with the natural numbers (which I presume is the case if this is aimed at computing, and would hope in general that you can write them on paper using a finite string of symbols) you can produce an enumerating program by just running the decision procedure on every syntactic formula and only emitting ones that pass. More succinctly, all recursive sets are recursively enumerable.
    - carlehewitt 8y ago
      The axioms of the higher order theory of the natural numbers are not countable and consequently not computationally enumerable. For example, there are uncountable many instances of the higher order induction axiom. Consequently, there are axioms that are not expressible as the abstractions of finite strings, just as there are real numbers that are not expressible as the abstractions of finite strings. But proof checking is still computationally decidable by a provably total higher order procedure. See the following: https://hal.archives-ouvertes.fr/hal-01566393 https://hal.archives-ouvertes.fr/hal-01566393