Decision Methods in the Theory of Ordinals
For an ordinal α, let RS(α), the restricted second order theory of [α, <], be the interpreted formalism containing the first order theory of [α, <] and quantification on monadic predicate variables, ranging over all subsets of α. For a cardinal γ, RS(α, γ) is like RS(α), except that the predicate variables are now restricted to range over subsets of α of cardinality less than γ. ω = ω 0 and ω 1 denote the first two infinite cardinals. In this note I will outline results concerning RS(α, ω 0), which were obtained in the Spring of 1964 (detailed proofs will appear in ), and the corresponding stronger results about RS(α, ω 1), which were obtained in the Fall of 1964.
KeywordsFinite Subset Detailed Proof Order Theory Finite Automaton Decision Method
Unable to display preview. Download preview PDF.
- 2.J. R. Büchi, On a decision method in restricted second order arithmetic, Proc. Int. Cong. Logic, Method, and Philos. Sci., 1960, Stanford Univ. Press, Stanford, Calif., 1962.Google Scholar
- 3.S. Feferman, Some recent work of Ehrenfeucht and Fraïssé, Summer Institute for Symbolic Logic, Cornell Univ., 1957, Commun. Research Div., Institute for Defense Analyses, 1960, pp. 201–209.Google Scholar
- 8.J. R. Büchi, Transfinite automata recursions and weak second order theory of ordinals, Proc. Int. Cong. Logic, Method, and Philos. Sci., Jerusalem, 1964 (to appear).Google Scholar