A theory of rules for enumerated classes of functions (Q1805407)

In classical logic, the fact that we have proved the existence of a solution does not necessarily mean that we have thus got an algorithm for producing this solution: For example, our proof can be based on considering two cases: when the Riemann hypothesis is true, and when it is not, and lead to different constructions in both cases; unless we know whether the Riemann hypothesis is true, we cannot produce an algorithm. In many cases, we need an algorithm, so it would be nice to have a logic in which proofs will automatically lead to algorithms. Such logics are called constructive. In constructive logics, a proof of a statement \(A\) carries with it an object (if any) whose existence is declared in \(A\). Correspondingly, a proof of an implication \(A\to B\) carries with it an algorithm that transforms an object whose existence is declared in \(A\) into an object whose existence is declared in \(B\). For formulas with iterated implications, like \((A\to B)\to C\), we will need mappings of higher type: from functions to objects, from functions to functions, etc. The resulting system becomes very complicated. In traditional constructive logic, this complicated structure is simplified by the existence of a universal (enumerating) algorithm. In programming terms, a universal algorithm is simply a compiler. In mathematical terms, it is a function \(f(m, n)\) of two variables (\(m\) is the code of a program, and \(n\) is the program's input) such that every computable function \(g(n)\) can be represented as \(f(m, n)\) for an appropriate code \(m\). The existence of such a function enables us to use codes to describe functions; hence, mapping from functions to objects can be coded as mappings from codes to objects, and thus, again simply by codes. One of the convenient forms of constructive logic in which this idea is implemented is combinatory logic (a basis for \(\lambda\)-calculus). For traditional combinatory logic, it is important that the universal function is also an algorithm (i.e. that it also belongs to the class of functions that we call constructive). It is true if we consider all algorithms, no matter how long they run, as constructive. In reality, an algorithm whose running time on small inputs exceeds the lifetime of the Universe can hardly be called constructive. If we restrict ourselves to a class of truly constructive algorithms (be it polynomial time, or primitive recursive), the enumerating function still exists (the compiler is still there), but it no longer belongs to the chosen function class (because a small program can run forever). For these situations, traditional combinatory logic is not applicable. Since the codes still exist (i.e., a class of functions is still enumerated), it is desirable to design a modification of combinatory logic in which these codes are used to simplify the hierarchy; care must be taken because the universal function is no longer constructive. Such a modification is proposed in the reviewed paper. This modification distinguishes between variables that occur in argument position in expressions (so that the dependency of the expression on these variables is computable), and other variables (related to codes) with respect to which computations are not necessarily possible. In particular, a \(\lambda\)-construction that uses a given term \(t\) to generate a constructive function \(\lambda x.t\) (meaning computing \(t\) from \(x\)) is only possible for variables \(x\) in argument position. An abstract Recursion Theorem is proven that generalizes recursion theorems for recursive and primitive recursive functions. The existence of the enumeration enables us to describe explicitly objects constructed by iterative constructions. Thus, the above theory is applied to explicit mathematics, first described by \textit{S. Feferman} [Lect. Notes Math. 450, 87-139 (1975; Zbl 0357.02029)].