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

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, φ’, while still subject to limitations in these formal systems. These results, owing to the fact that φ’ may arise through the behavior of any unbounded inductive computation, establish results on the eventual behavior of a class of computational processes.