Syntax and semantics in highertype recursion theory
Author:
David P. Kierstead
Journal:
Trans. Amer. Math. Soc. 276 (1983), 67105
MSC:
Primary 03D65
MathSciNet review:
684494
Fulltext PDF Free Access
Abstract 
References 
Similar Articles 
Additional Information
Abstract: Recursion in higher types was introduced by S. C. Kleene in 1959. Since that time, it has come to be recognized as a natural and important generalization of ordinary recursion theory. Unfortunately, the theory contains certain apparent anomalies, which stem from the fact that higher type computations deal with the intensions of their arguments, rather than the extensions. This causes the failure of the substitution principle (that if and are recursive, then there should be a recursive such that at least whenever is total), and of the first recursion principle (that if is a recursive functional, then the minimal solution of the equation should be recursive as well). In an effort to removeor at least explainthese anomalies, Kleene, in 1978, developed a system for computation in higher types which was based entirely on the syntactic manipulation of formal expressions, called expressions. As Kleene pointed out, no adequate semantics for these expressions can be based on the classical (total) type structure over . In a paper to appear in The Kleene Symposium (NorthHolland), we showed that an appropriate semantics could be based on the type structure , which is obtained by adding a new object at level 0 and, at level , allowing all monotone, partial functions from type into . Over , both of the principles mentioned above do hold. There is a natural embedding to into . In this paper, we complement the syntactic structure with a syntaxfree definition of recursion over , and show that the two notions are equivalent. This system admits an enumeration theorem, in spite of the fact that the presence of partial objects complicates the coding of finite sequences. Indeed, it is not possible to code all finite sequences from type as type objects. We use the combination of the syntactic and semantic systems to prove that, for any , the following are equivalent: A. is recursive in the sense of Kleene [1959], B. is recursive in the sense of Kleene [1978], and C. is the pullback in of some recursive . Using these equivalences, we give a necessary and sufficient condition on , under which the substitution principle mentioned above will hold for any recursive . With one trivial exception, the condition is that if , then must contain a variable of type greater than . We feel that this result is particularly natural in the current setting.
 [A]
Handbook of mathematical logic, NorthHolland Publishing Co.,
AmsterdamNew YorkOxford, 1977. Edited by Jon Barwise; With the
cooperation of H. J. Keisler, K. Kunen, Y. N. Moschovakis and A. S.
Troelstra; Studies in Logic and the Foundations of Mathematics, Vol. 90. MR 0457132
(56 #15351)
 [S]
Stephen
Cole Kleene, Introduction to metamathematics, D. Van Nostrand
Co., Inc., New York, N. Y., 1952. MR 0051790
(14,525m)
 1.
S.
C. Kleene, Recursive functionals and quantifiers
of finite types. I, Trans. Amer. Math. Soc.
91 (1959), 1–52.
MR
0102480 (21 #1273), http://dx.doi.org/10.1090/S00029947195901024809
 2.
S.
C. Kleene, Recursive functionals and quantifiers
of finite types. II, Trans. Amer. Math.
Soc. 108 (1963),
106–142. MR 0153557
(27 #3521), http://dx.doi.org/10.1090/S00029947196301535574
 3.
S.
C. Kleene, Recursive functionals and quantifiers of finite types
revisited. I, Generalized recursion theory, II (Proc. Second Sympos.,
Univ. Oslo, Oslo, 1977) Stud. Logic Foundations Math., vol. 94,
NorthHolland, AmsterdamNew York, 1978, pp. 185–222. MR 516936
(80k:03048)
 4.
S.
C. Kleene, Recursive functionals and quantifiers of finite types
revisited. II, The Kleene Symposium (Proc. Sympos., Univ. Wisconsin,
Madison, Wis., 1978), Stud. Logic Foundations Math., vol. 101,
NorthHolland, AmsterdamNew York, 1980, pp. 1–29. MR 591873
(83j:03076)
 5.
[to appear] Recursive functionals and quantifiers of finite types revisited. III.
 [D]
David
P. Kierstead, A semantics for Kleene’s
𝑗expressions, The Kleene Symposium (Proc. Sympos., Univ.
Wisconsin, Madison, Wis., 1978), Stud. Logic Foundations Math.,
vol. 101, NorthHolland, AmsterdamNew York, 1980,
pp. 353–366. MR 591890
(82f:03039)
 [R]
A. Platek [1966] Foundations of recursion theory, Ph.D. Thesis, Stanford University, Stanford, Calif.
 [A]
 S. Kechris and Y. N. Moschovakis [1977] Recursion in higher types, Handbook of Mathematical Logic, K. J. Barwise, Editor, NorthHolland, Amsterdam, pp. 681737. MR 0457132 (56:15351)
 [S]
 C. Kleene [1952] Introduction to metamathematics, NorthHolland, Amsterdam. MR 0051790 (14:525m)
 1.
 [1959] Recursive functionals and quantifiers of finite types. I, Trans. Amer. Math. Soc. 91, 152. MR 0102480 (21:1273)
 2.
 [1963] Recursive functionals and quantifiers of finite types. II, Trans. Amer. Math. Soc. 108, 106142. MR 0153557 (27:3521)
 3.
 [1978] Recursive functionals and quantifiers of finite types revisited. I, Generalized Recursion Theory. II, J. E. Fenstad, R. O. Gandy and G. E. Sacks, Editors, NorthHolland, Amsterdam, pp. 185222. MR 516936 (80k:03048)
 4.
 [1980] Recursive functionals and quantifiers of finite types revisited. II, The Kleene Symposium, K. J. Barwise, H. J. Keisler and K. Kunen, Editors, NorthHolland, Amsterdam, pp. 129. MR 591873 (83j:03076)
 5.
 [to appear] Recursive functionals and quantifiers of finite types revisited. III.
 [D]
 P. Kierstead [1980] A semantics for Kleene's expressions, The Kleene Symposium, K. J. Barwise, H. J. Keisler and K. Kunen, Editors, NorthHolland, Amsterdam, pp. 253366. MR 591890 (82f:03039)
 [R]
 A. Platek [1966] Foundations of recursion theory, Ph.D. Thesis, Stanford University, Stanford, Calif.
Similar Articles
Retrieve articles in Transactions of the American Mathematical Society
with MSC:
03D65
Retrieve articles in all journals
with MSC:
03D65
Additional Information
DOI:
http://dx.doi.org/10.1090/S00029947198306844947
PII:
S 00029947(1983)06844947
Article copyright:
© Copyright 1983
American Mathematical Society
