[FOM] "Recursive"

[Alasdair Urquhart]

It's usually said that Goedel's definition of
general recursive function was taken from a
definition in a letter of Herbrand.  This is
a very widely held opinion -- not surprisingly,
since this is what Goedel himself said.

The rediscovery of Herbrand's letter of 7 April
1931 (by John Dawson in 1986) showed that Goedel had
in fact misremembered.  Herbrand defines a concept
of constructive function that shows some analogy
with the notion of general recursive function,
but is definitely NOT the same.  This is because
Herbrand insists that

"We must be able to show, by means of intuitionistic
proofs, that it is possible to compute with these
axioms the value of the functions univocally for each
particular system of values of their argument."
			(Goedel, CW, Vol. 5, p. 15)

However one chooses to make the vague concept of
"intuitionistic proof" precise this must lead to a proper
subclass of the general recursive functions,
as Herbrand himself emphasizes in the third-to-last
paragraph of his letter (CW, Vol. 5, p. 21).

Wilfried Sieg's excellent introduction to the correspondence
in CW, Vol. 5 repays close study.

Alasdair Urquhart