On the Definitional Embeddability of the Combinatory Logic Theory into the First-Order Predicate Calculus


V. I. Shalack


In this article we prove a theorem on the definitional embeddability of the combinatory logic into the first-order predicate calculus without equality. Since all efficiently computable functions can be represented in the combinatory logic, it immediately follows that they can be represented in the first-order classical predicate logic. So far mathematicians studied the computability theory as some applied theory. From our theorem it follows that the notion of computability is purely logical. This result will be of interest not only for logicians and mathematicians but also for philosophers who study foundations of logic and its relation to mathematics.






Engeler, E. Metamathematik der Elementarmathematik. New York: Springer, 1983. 132 pp.
Karpovich, V.N. Terminy v strukture teorii. Logicheskij analiz [Terms in the structure of the theory. Logical analysis]. Novosibirsk: Nauka, 1978. 128 pp. (In Russian)
Smirnov, V.A. “Logical Relations between Theories”, Synthese, 1986, 66(1), pp. 71–87.
Shalack, V. “On Some Applied First-Order Theories which Can be Represented by Definitions”, Bulletin of the Section of Logic, 2015, 44/1-2, pp. 19–24.