Finite Definability of Number-Theoretic Functions and Parametric Completeness of Equational Calculi
✍ Scribed by Georg Kreisel; William W. Tait
- Publisher
- John Wiley and Sons
- Year
- 1961
- Tongue
- English
- Weight
- 628 KB
- Volume
- 7
- Category
- Article
- ISSN
- 0044-3050
No coin nor oath required. For personal study only.
✦ Synopsis
This paper has the limited aim of presenting. an elementary treatment of the notion of defining the values of a number-theoretic function q from a finite number of substitution instances of a system r of equations, or as we shall say, of the finite definubility of 9 by r. We construct an equational calculus E in which q is reckonable (in the sense of [3]) from-rjust in case it is finitely defined by r. The notion of ''parametric completeness" introduced here plays the same role in relating finite definability to reckonability that the usual notion of completeness (with respect t o the class of N-models) plays in relating the usual notion of definability by definite descriptions to reckonability.
In 0 2, we give a model-theoretic proof that the finite definahility of p.' (but not its definability) implics that q isrecursive (via Theorem 1). Convcrscly Theorcm 2 in 0 5 asserts that reckonability (from I') in a parametrically sound and complct,e calculus implies definability (by r), and Theorem 3 in 5 6 assorts that finite definability of q from r implies that q can be reckoned from r in a parametrically complete calculus. In 5 7 we construct E and give an elementary proof that it is parametrically complete (Theorem 4). I n J 8 we decide the analogous question for finite definability and definability of partial numbcr-theoretic functions. -Theorem A in $ 3 , which is of independent interest, gives a derivation of Theorem 4 from Theorem 1, but is less eleme?ntary than 5 7.