[FOM] Kleene's T predicate

[Daniel Schwartz]

Yiannis,

Thanks for this.  It makes sense, and answers a question that I too have
entertained for a long time.

--Dan Schwartz

"Yiannis N. Moschovakis" <ynm at math.ucla.edu> wrote:

> ??????
> To supplement Martin's detailed account of the facts about the S
> and T predicates, I have a (now vague) memory of Kleene explaining
> that "S" stood for "substitution", the main rule for deducing
> equations from Herbrand-Goedel-Kleene systems of equations, and
> "T" is simply the next letter in the alphabet; nothing more
> profound than that.
>
> As Martin explains, the move from S to T in Kleene (1943) was made
> "to deal with the non-determinism of the equation calculus". In
> some detail (to make a point further down),
>       S(e,x,y) <==> y is the code of a computation from the
>                     system with code e on the input x,
> and there may be many y's and many output values on the same input
> x; setting
>       T(e,x,y) <==> S(e,x,y) & (forall t<y) not S(e,x,t)
> admits at most one computation with each e and x and so each e
> computes exactly one partial function. This, however, addresses
> only a small part of the problem introduced by the indeterminacy
> of the HGK computation model, as the connection between a system E
> and the (partial) function it computes is generally obscure,
> except for very simple systems: it depends, for example, on the
> specific coding for tuples we use to pick "the least computation"
> in defining T. The deterministic Turing machines used in Martin's
> classic 1958 book provide a much tighter connection between the
> computation model and the partial function it computes.
>
> A different approach to this problem was taken by John McCarthy in
> his classic 1963 paper "A basis for a mathematical theory of
> computation" (google it). McCarthy adds conditionals to the
> term-formation rules of the equation calculus and so he can
> restrict himself to systems of equations in which each (partial) function
> is "defined" by a single term equation. Each "recursive program"
>           f_i(x_i) = E_i   (i=1, ..., K)
> computes the tuple of least partial functions f*_1,...,f*_K which
> satisfy its equations, a direct, coding-independent connection of
> denotational and operational semantics which (in many cases)
> provides trivial "correctness proofs" for programs. Recursive
> programs also provide very simple proofs of some basic results of
> elementary recursion theory, such as the so-called First Recursion
> Theorem of Kleene; and they can be easily extended to yield a
> theory of recursion on arbitrary sets from arbitrary functions and
> relations. They are well-known to computer scientists, of course,
> but not as much to logicians who work in "computability theory".
>
> Yiannis Moschovakis
>
>
> On Mon, May 23, 2016 at 8:07 PM, Martin Davis <martin at eipye.com> wrote:
>
> > Trying to find a connection with Turing is hopelessly anachronistic. The
> > first version of the T predicate was introduced in Kleene's paper "General
> > Recursive Functions of Natural Numbers" Mathematische Annalen vol.
> > 112(1936) 727-742.
> > A footnote reads: "Presented to the American Mathematical Society,
> > September 1935." The paper refers to works by Ackermann, Péter, Gödel, and
> > Skolem, but not Turing. The formalism to which Kleene applies Gödel
> > arithmetization in this paper is an equation calculus. Because it enables
> > derivation of the values from recursion equations going beyond "primitive"
> > (so named by Kleene in this paper) recursions, as for example the defining
> > equations of Ackermann's function, Kleene spoke of "general recursive
> > functions". The main result of this paper is that every general recursive
> > function h can be written in the form:
> >                     h(x) =  f(min y [g(x,y])
> > where f and g are primitive recursive. This Kleene Normal Form Theorem
> > turned proving the equivalence of different formulations of computability
> > into a routine chore.
> >
> > What we think of as Kleene's T predicate was introduced in his "Recursive
> > Predicates and Quantifiers," Transactions of the American Mathematical
> > Society, vol. 53(1943)  41-73. What was called T in the 1936 paper is now
> > called S, and T is defined from S by choosing the least of the values of
> > one of the variables satisfying the predicate. This is to deal with the
> > non-determinism of the equation calculus.
> >
> > In my anthology "The Undecidable" (available in a Dover reprint) are
> > included both of these papers as well as notes taken by Kleene and Rosser
> > (then graduate students) on Gödel's lectures in 1934 at which the idea of a
> > formalism for general recursive functions was first mentioned.
> >
> > I had the idea that if one applied Kleene's methods to the Turing machine
> > formalism there was no indeterminancy to deal with so the development could
> > proceed more simply and smoothly. This is what led to my book
> > "Computability and Unsolvability" published in 1958, but also available as
> > a Dover reprint. I used the letter T as a tribute to Kleene.  It never
> > occurred to me to consider that it was also Turing's initial.
> >
> > Martin
> >
> > _______________________________________________
> > FOM mailing list
> > FOM at cs.nyu.edu
> > http://www.cs.nyu.edu/mailman/listinfo/fom
> >
> >