Hostname: page-component-cd9895bd7-hc48f Total loading time: 0 Render date: 2024-12-22T20:28:31.461Z Has data issue: false hasContentIssue false

An infinitistic rule of proof1

Published online by Cambridge University Press:  12 March 2014

H. B. Enderton*
Affiliation:
University of California, Berkeley

Extract

In this paper we consider a fonnal system of second-order Peano arithmetic with a rule of inference stronger than the ω-rule [3]. We also consider the relation to a class of models for analysis (i.e. second-order arithmetic) which lies between the class of ω-models and the class of β-models [5].

The notation used is largely that of [3] and [5]. We assume that the reader has some familiarity with at least the ideas of the former. The formal system (A) of Peano arithmetic employed in [3] includes the comprehension axioms and the second-order induction axiom.

Type
Research Article
Copyright
Copyright © Association for Symbolic Logic 1968

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

1

This research was supported by the National Science Foundation, grant GP-5632.

References

[1]Enderton, H. B., Hierarchies in recursive function theory, Transactions of the American Mathematical Society, vol. 111 (1964), pp. 457471.CrossRefGoogle Scholar
[2]Gandy, R., Kreisel, G. and Tait, W., Set existence, Bulletin de l' Academie Polonaise des Sciences, Série des sciences mathématiques, astronomiques et physiques, vol. 8 (1960), pp. 577582.Google Scholar
[3]Grzegorczyk, A., Mostowski, A. and Ryll-Nardzewski, C., The classical and the ω-complete arithmetic, this Journal, vol. 23 (1958), pp. 188205.Google Scholar
[4]Kleene, S. C., Recursive functional and quantifiers of finite types. I, Transactions of the American Mathematical Society, vol. 91 (1959), pp. 152.Google Scholar
[5]Mostowski, A., Formal system of analysis based on an infinitistic rule of proof, Infinitistic Methods, Pergamon Press, New York, 1961, pp. 141166.Google Scholar
[6]Orey, S., On ω-consistency and related properties, this Journal, vol. 21 (1956), pp. 246252.Google Scholar
[7]Putnam, H., A hierarchy containing all provable Δ31 sets, Notices of the American Mathematical Society, vol. 10 (1963), p. 352.Google Scholar
[8]Rosser, J. B., Gödel theorems for non-constructive logics, this Journal, vol. 2 (1937), pp. 129137.Google Scholar
[9]Shoenfield, J. R., A hierarchy for objects of type 2, Notices of the American Mathematical Society, vol. 12 (1965), pp. 369370.Google Scholar