2008/09/23 by Michael Pfender, Pfender, Michael · 2 citations
Computer Science · #03D75 #Category Theory (math.CT) #Computability, Logic, AI Algorithms #FOS: Mathematics #Logic (math.LO) #Logic, programming, and type systems #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.0809.3881
openalex publication_date 2008/09/23 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We construct here an iterative evaluation of all PR map codes: progress of this iteration is measured by descending complexity within "Ordinal" O := N[ω] of polynomials in one indeterminate, ordered lexicographically. Non-infinit descent of such iterations is added as a mild additional axiom schema (πO) to Theory PRA = PR+(abstr) of Primitive Recursion with predicate abstraction, out of forgoing part RCF 1. This then gives (correct) "on"-termination of iterative evaluation of argumented deduction trees as well, for theories PRA+(πO). By means of this constructive evaluation the Main Theorem is proved, on Termination-conditioned (Inner) Soundness for such theories, Ordinal O extending N[ω]. As a consequence we get Self-Consistency for these theories, namely derivation of its own free-variable Consistency formula. As to expect from classical setting, Self-Consistency gives (unconditioned) Objective Soundness. Termination-Conditioned Soundness holds "already" for PRA, but it turns out that at least present derivation of Consistency from this conditioned Soundness depends on schema (πO) of non-infinit descent in Ordinal O := \N[ω].