×

Spielquantorinterpretation unstetiger Funktionale der höheren Analysis. (English) Zbl 0544.03021

The following extensions \({\mathfrak A}^+\), \({\mathfrak A}^{++}\) of classical analysis \({\mathfrak A}\) are considered in the language of functionals of finite type: \({\mathfrak A}^+\) is \({\mathfrak A}\) plus \((AC)^{\alpha,0}\) for arithmetical formulae, \({\mathfrak A}^{++}\) moreover contains analytical comprehension over objects of any type. Following a proposal of Luckhardt, in order to make functional interpretation applicable, a pre- translation is given, which applies to these theories and eliminates the discontinuous functionals. For this purpose a special game quantifier is used. The prime formulae are translated into statements about continuous functionals built with the game quantifier. The outer quantifier structure is not changed except that a relativization takes place and that the types are raised. The provable discontinuities now are absorbed by the game quantifier prefix, so that in the kernel only recursive operations are used. The strength of the discontinuous functionals thus is reduced to the strength of a special game quantifier, which is used axiomatically in the form of a unary predicate \(\square z\) over objects z of type 2. Especially it is shown that all analytical statements provable in the original theory are also provable in the corresponding game quantifier theory. In the case of \({\mathfrak A}^+\), instead of the axiomatic \(\square\) also a defined \(\square\) can be used. Thereby \({\mathfrak A}^+\) is not stronger than \({\mathfrak A}\). In opposite to this, the consistency of \({\mathfrak A}\) can be shown in a subsystem of \({\mathfrak A}^{++}\). The mentioned functional interpretation of classical analysis with the axiomatic \(\square\) is done in the author’s paper ”Gödelsche Funktionalinterpretation für eine Erweiterung der klassischen Analysis” [Z. Math. Logik Grundlagen Math. (to appear)].

MSC:

03D99 Computability and recursion theory
03F25 Relative consistency and interpretations
03C80 Logic with extra quantifiers and operators
PDFBibTeX XMLCite
Full Text: DOI EuDML

References:

[1] Gale, D., Stewart, F.M.: Infinite games with perfect information, contributions to the theory of games 2. Ann. Math. Studies28, 245–266 (1953).
[2] Gödel, K.: Über eine bisher noch nicht benützte Erweiterung des finiten Standpunkts. Dialectica12, 280–287 (1958). · Zbl 0090.01003 · doi:10.1111/j.1746-8361.1958.tb01464.x
[3] Howard, W.A., Kreisel, G.: Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis. J. Symb. Logic31, 325–358 (1966). · Zbl 0156.00804 · doi:10.2307/2270450
[4] Luckhardt, H.: Extensional Gödel functional interpretation. A consistency proof of classical analysis. Lecture Notes in Mathematics, Vol. 306. Berlin, Heidelberg, New York: Springer 1973. · Zbl 0262.02031
[5] Luckhardt, H.: The real elements in a consistency proof for simple type theory. saI. Proof theory symposion Kiel 1974. Lecture Notes in Mathematics, Vol. 500, pp. 233–256. Berlin, Heidelberg, New York: Springer 1975.
[6] Luckhardt, H.: The real elements in a consistency proof for simple type theory. II. Bisher unpubliziert. · Zbl 0326.02019
[7] Moschovakis, Y.N.: Descriptive set theory. Studies in Logic and the Foundations of Mathematics 100. Amsterdam 1980.
[8] Spector, C.: Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics. Proc. Symp. Pure Math. AMSV, 1–27 (1962). · Zbl 0143.25502 · doi:10.1090/pspum/005/0154801
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.