Completeness and Well-Definability of a Provability Degree Measure in Sufficiently Powerful Formal Systems, and Finite-Time Effective Knowers

TL;DR

This paper investigates the properties of provability degree measures in powerful formal systems, demonstrating their completeness, well-definability, and the construction of finite-time theorem knowers, with implications for computational process behavior.

Contribution

It introduces a provability degree measure that remains well-defined and complete in strong formal systems and constructs finite-time theorem knowers within these frameworks.

Findings

Provability degrees are well-defined and complete in sufficiently powerful systems.

The union of provability degrees is isomorphic to the system's statements.

Construction of finite-time theorem knowers up to quadratic complexity.

Abstract

We show that including degrees of a particular kind of provability in the search target for any theorem-prover in sufficiently powerful formal systems over finite-sized statements preserves well-definition and a sufficient consistency while establishing completeness. Moreover, the union of such degrees is isomorphic to such a system's {\aleph_0} statements and permits the construction of a best-possible (up to a quadratic term) finite-time theorem knower, {\phi}', while still subject to limitations in these formal systems. These results, owing to the fact that {\phi}' may arise through the behavior of any unbounded inductive computation, establish results on the eventual behavior of a class of computational processes.