RCF2: Evaluation and Consistency
| dc.creator | Pfender, Michael | |
| dc.date | 2008-09-23 | |
| dc.date | 2009-01-30 | |
| dc.date.accessioned | 2026-07-07T12:35:25Z | |
| dc.date.available | 2026-07-07T12:35:25Z | |
| dc.description | 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 PR_A = 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 PR_A+(π_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 PR_A, 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[ω]. | |
| dc.description | Full version. Inserted Sections 3-7, Coda. Introduction and summary unchanged | |
| dc.identifier | https://arxiv.org/abs/0809.3881 | |
| dc.identifier | http://arxiv.org/abs/0809.3881 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/217758 | |
| dc.subject | Category Theory | |
| dc.subject | Logic | |
| dc.subject | 03D75 | |
| dc.title | RCF2: Evaluation and Consistency | |
| dc.type | text |