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.
In this theory, proof checking is computationally decidable even though the theorems are not computationally enumerable by a total procedure.
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#...
Also, Godel's proposition "I'mUnprovable" does not exist in the higher order theory because it doesn't type check.
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.
But proof checking is still computationally decidable by a provably total higher order procedure. See the following: https://hal.archives-ouvertes.fr/hal-01566393
See the following: https://cacm.acm.org/blogs/blog-cacm/231495-what-turing-and-...