Hacker News Reader

Comment by wk_end | Hacker News Reader

> 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#...

View on HN

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

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.

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.

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.

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

Would you mind explaining how the system avoids proofs being a recursive set implying the axioms are recursive? I'm afraid I don't understand how you can invoke axioms that are not expressible via finite strings in a proof that is expressible in such a manner.

Instances of the induction axiom are uncountable for the higher order theory of the natural numbers, which obviously means that they cannot be enumerated using the natural numbers. However, it is very easy to use the induction axiom in proofs that are expressible using finite strings. Please see the article above published in HAL Archives.

The 1st order variant of the Dedekind/Peano theory of natural numbers is not suitable for computer science because it allows infinite integers and other monsters.

See the following: https://cacm.acm.org/blogs/blog-cacm/231495-what-turing-and-...

Reply on news.ycombinator.com