The predicate K of the current mathematical knowledge non-trivially extends computability theory
Apoloniusz Tyszka · HAL (Le Centre pour la Communication Scientifique Directe) · 2024
K denotes both the knowledge predicate satisfied by every currently known theorem and the finite set of all currently known theorems.The set K is time-dependent and publicly available.Any theorem of any mathematician from past or present forever belongs to K. We prove the following Statement 1: there is a limit-computable function β : N → N of unknown computability which eventually dominates every function δ : N → N with a single-fold Diophantine representation.Statement 1 holds when, for every n ∈ N, β(n) is the smallest b ∈ N such that if a system of equations S ⊆ {1 = x k , x i + x j = x k , x i • x j = x k : i, j, k ∈ {0, . . ., n}} has a unique solution in N n+1 , then this solution belongs to {0, . . ., b} n+1 .Statement 1 does not follow from any widely known mathematical theorem.Ignoring the epistemic condition in Statement 1, Statement 1 is implied by the following result of Royer and Case: There is a limit-computable function β 1 : N → N which eventually dominates every computable function δ 1 : N → N. The proof of Statement 1 shows that Statement 1 follows from some mathematical theorem and the following conjunction: ((The function β is computable) ∈ K) ∧ ((The function β is uncomputable) ∈ K).