Does Logic Count?

Abstract

What is the relation of the ordinary first-order logic and the general theory of computation? A hoped-for connection would be to interpret a computation of the value b of a function f(x) for the argument a as a deduction of the equation (b = f(a)) in a suitable elementary number theory. This equation may be thought of as being obtained by a computation in an equation calculus from a set of defining equations plus propositional logic plus substitution of terms for variables and substitution of identicals. Received first-order logic can be made commensurable with this equation calculus by eliminating predicates in terms of their characteristic functions and eliminating existential quantifiers in terms of Skolem functions. It turns out that not all sets of defining equations can be obtained in this way if the received first-order logic is used. However, they can all be obtained if independence-friendly logic is used. This turns all basic problems of computation theory into problems of logical theory.