Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis
Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis
复制标题
零型和一型的超限归纳和条形归纳，以及连续性在直觉分析中的作用
DOI：
10.2307/2270450
复制
发表时间：
1966
影响因子：
0.6
通讯作者：
G. Kreisel
中科院分区：
文献类型：
--
作者：
W. A. Howard;G. Kreisel
以下是一个自包含的证明理论治疗的两个主要公理图式目前直觉分析：公理的酒吧归纳（布劳威尔酒吧定理）和公理的连续性。结果是根据初等直觉分析H（§ 1）中的形式可导性来公式化的，因此正（即，可导性）的结果也适用于初等经典分析Z1（附录1）。这两个图式都包含量词νf ~ n的组合，其中f、g、.旨在覆盖合适种类的对象x、y、.的自由选择序列;例如，自然数或自然数的序列，以及n、m、p、r、.覆盖自然数（非负整数）。
The following is a self-contained proof theoretic treatment of two of the principal axiom schemata of current intuitionistic analysis: the axiom of bar induction (Brouwer's bar theorem) and the axiom of continuity. The results are formulated in terms of formal derivability in elementary intuitionistic analysis H(§ 1), so the positive (i.e., derivability) results also apply to elementary classical analysis Z1 (Appendix 1). Both schemata contain the combination of quantifiers νfΛn, where f, g, … are intended to range over free choice sequences of suitable kinds of objects x, y, …; for example, natural numbers or sequences of natural numbers, and n, m, p, r, … over natural numbers (non-negative integers).