Finite investigations of transfinite derivations
Finite investigations of transfinite derivations
复制标题
超限导数的有限研究
DOI：
10.1007/bf01091743
复制
发表时间：
1978
期刊：
影响因子：
--
通讯作者：
G. Mints
中科院分区：
文献类型：
--
作者：
G. Mints
分析了算术公式的抽象ω导子。第一部分构造了一个本原递归归一化算子E。它不仅剔除了递归描述的派生(即，有充分根据的证明图)，而且还删除了通过推导规则从公理构造的任意(不一定是有充分基础的)证明图。这使得我们可以在模型理论中应用E，它在证明论中的应用是基于E的基本性质在本原递归算法中的形式化。第二部分证明了基于有限类型选择公理的Heyting算法HA、ω+AC的割消性。允许切割消除的公式使用与Carry、Howard、Girard和Martin-Löf方法的派生相关的术语。这些术语包括在规则的制定中。作为推论之一，得出了HA、ω+AC对HA的保守性。
Abstractω-derivations of arithmetic formulas are analyzed. A primitive recursive normalization operator E is constructed in the first part. It cut-eliminates not only recursively described derivations (i.e., well-founded proof-figures) but also arbitrary (not necessarily well-founded) proof-figures constructed from an axiom by derivation rules. This permits us to apply E in the theory of models, Its application in the theory of proofs is based on the formalizability of the fundamental properties of E in a primitive recursive arithmetic. Cut-eliminability in the Heyting arithmetic HAω+AC with the axiom of choice of all finite types is proved in the second part. The formulation allowing cut-elimination uses terms associated with the derivations by a method due to Carry, Howard, Girard, and Martin-Löf. These terms are included in the very formulation of the rules. The conservativity of HAω+AC over HA is obtained as one of the corollaries.