Completeness and Well-Definability of a Provability Degree Measure in Sufficiently Powerful Formal Systems, and Finite-Time Effective Knowers
Fuente:
arXiv
Gespeichert in:
| 1. Verfasser: | |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866912134187712512 |
|---|---|
| author | Bahl, Rohan |
| author_facet | Bahl, Rohan |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_01972 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Completeness and Well-Definability of a Provability Degree Measure in Sufficiently Powerful Formal Systems, and Finite-Time Effective Knowers Bahl, Rohan Logic 03B22 (Primary) 03B42, 03D70 (Secondary) 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. |
| title | Completeness and Well-Definability of a Provability Degree Measure in Sufficiently Powerful Formal Systems, and Finite-Time Effective Knowers |
| topic | Logic 03B22 (Primary) 03B42, 03D70 (Secondary) |
| url | https://arxiv.org/abs/2410.01972 |