346
ALONZO
CHURCH.
The purpose of the present paper is to propose a definition of effective
calculability
which is thought to correspond satisfactorily to the somewhat
vague intuitive notion in terms of which problems of this class are often stated,
and to show, by means of an example, that not every problem of this class
is solvable.
2.
Conversion and A-definability. We select a particular list of sym-
bols, consisting of the symbols
{
,
),
(
,
),
X,
[
,
1,
and an enumerably infinite
set of symbols a,
b,
c,
.
.
.
to be called variables. And we define the word
formula to mean any finite sequence of symbols out of this list. The terms
well-formed formula, free variable, and bound variable are then defined by
induction as follows.
A
variable x standing alone is a well-formed formula
and the occurrence of x in it is an occurrence of
x
as a free variable in it;
if the formulas
F
and X are well-formed, {F)(X) is well-formed, and an
occurrence of x as a free (bound) variable in
F
or
X
is an occurrence of
x
as a free (bound) variable in {F) (X)
;
if the formula M is well-formed and
contains an occurrence of
x
as a free variable in M, then hx[M] is well-formed,
any occurrence of x in h[M] is an occurrence of x as a bound variable in
hx[M], and an occurrence of a variable
y,
other than x, as a free (bound)
variable in M is an occurrence of
y
as a free (bound) variable in hx[M].
As will appear, this definition of effective calculability can be stated in either
of two equivalent forms, (1) that a function of positive integers shall be called
effectively calculable if
it
is h-definable in the sense of $2 below,
(2)
that a function
of positive integers shall be called effectively calculable if it is recursive in the sense
of
$
4
below. The notion of h-definability is due jointly to the present author and
S.
C.
Kleene, successive steps towards it having been taken by the present author in
the Annals of Mathematics, vol.
34 (1933), p. 863, and by Kleene in the American
Journal
of
Mathematics, vol. 57 (1935), p. 219.
The notion of recursiveness in the
sense of
$
4 below is due jointly to Jacques Herbrand and Kurt Gijdel, as is there
explained. And the proof of equivalence of the two notions is due chiefly to Kleene,
but also partly to the present author and to
J.
B.
Rosser, as explained below. The
proposal to identify these notions with the intuitive notion of effective calculability
is first made in the present paper (but see the first footnote to $7 below).
With the aid of the methods of Kleene (American Journal of Mathematics, 1935),
the considerations of the present paper could, with comparatively slight modification,
be carried through entirely in terms of X-definability, without making use of the notion
of recursiveness. On the other hand, since the results of the present paper were
obtained, it has been shown by Kleene (see his forthcoming paper, "General recursive
functions of natural numbers") that analogous results can be obtained entirely in
terms of recursiveness, without making use of X-definability. The fact, however, that
two such widely different and (in the opinion of the author) equally natural definitions
of effective calculability turn out to be equivalent adds to the strength of the reasons
adduced below for believing that they constitute as general a characterization of this
notion as is consistent with the usual intuitive understanding of it.