Functionals defined by transfinite recursion
Functionals defined by transfinite recursion
复制标题
由超限递归定义的泛函
DOI：
10.2307/2270132
复制
发表时间：
1965
影响因子：
0.6
通讯作者：
W. Tait
中科院分区：
文献类型：
--
作者：
W. Tait
本文主要讨论无量词二阶系统（即，用自由变量表示数和函数，用常数表示数、函数和泛函），其基本规则是原始递归算术以及通过原始递归和显式定义来定义泛函的规则。精确描述见§2。额外的规则具有通过超限递归直到某个序数递归来定义的形式（其中递归由原始递归（p.r.）排序）。在§3中，我们讨论了递归系统的一些初等闭包性质（在推理和定义规则下）。设R（暂时）表示递归到的系统。本文的主要结果有两类：第5-7节是关于系统R_n的较少初等的闭包性质。也就是说，我们证明了Rη中的某些函数方程类可以在Rη中求解，其中η < ε（η）（最小ε数> ε）是显式确定的。所考虑的函数方程类都大致具有通过递归对给定函数F的不安全序列的偏序或通过简单的序数运算从该偏序中获得的某种排序进行定义的形式。将这些方程归约为超限递归所需的关键引理（定理1）只是对Brouwer-Kleene思想的一种强化。
This paper deals mainly with quantifier-free second order systems (i.e., with free variables for numbers and functions, and constants for numbers, functions, and functionals) whose basic rules are those of primitive recursive arithmetic together with definition of functionals by primitive recursion and explicit definition. Precise descriptions are given in §2. The additional rules have the form of definition by transfinite recursion up to some ordinal ξ (where ξ is represented by a primitive recursive (p.r.) ordering). In §3 we discuss some elementary closure properties (under rules of inference and definition) of systems with recursion up to ξ. Let Rξ denote (temporarily) the system with recursion up to ξ. The main results of this paper are of two sorts: Sections 5–7 are concerned with less elementary closure properties of the systems Rξ. Namely, we show that certain classes of functional equations in Rη can be solved in Rη for some explicitly determined η < ε(η) (the least ε-number > ξ). The classes of functional equations considered all have roughly the form of definition by recursion on the partial ordering of unsecured sequences of a given functional F, or on some ordering which is obtained from this by simple ordinal operations. The key lemma (Theorem 1) needed for the reduction of these equations to transfinite recursion is simply a sharpening of the Brouwer-Kleene idea.