Systems of iterated projective ordinal notations and combinatorial statements about binary labeled trees

Archive for Mathematical Logic 29 (1):29-46 (1989)
  Copy   BIBTEX

Abstract

We introduce the appropriate iterated version of the system of ordinal notations from [G1] whose order type is the familiar Howard ordinal. As in [G1], our ordinal notations are partly inspired by the ideas from [P] where certain crucial properties of the traditional Munich' ordinal notations are isolated and used in the cut-elimination proofs. As compared to the corresponding “impredicative” Munich' ordinal notations (see e.g. [B1, B2, J, Sch1, Sch2, BSch]), our ordinal notations arearbitrary terms in the appropriate simple term algebra based on the notion of collapsing functions (which we would rather identify as projective functions). In Sect. 1 below we define the systems of ordinal notationsPRJ( ), for any primitive recursive limit wellordering . In Sect. 2 we prove the crucial well-foundness property by using the appropriate well-quasi-ordering property of the corresponding binary labeled trees [G3]. In Sect. 3 we interprete inPRJ( ) the familiar Veblen-Bachmann hierarchy of ordinal functions, and in Sect. 4 we show that the corresponding Buchholz's system of ordinal notationsOT( ) is a proper subsystem ofPRJ( ), although it has the same order type according to [G3] together with the interpretation from Sect. 2 in the terms of labeled trees. In Sect. 5 we use Friedman's approach in order to obtain an appropriate purely combinatorial statement which is not provable in the theory of iterated inductive definitions ID< λ, for arbitrarily large limit ordinalλ. Formal theories, axioms, etc. used below are familiar in the proof theory of subsystems of analysis (see [BFPS, T, BSch]).

Other Versions

No versions found

Links

PhilArchive

    This entry is not archived by us. If you are the author and have permission from the publisher, we recommend that you archive it. Many publishers automatically grant permission to authors to archive pre-prints. By uploading a copy of your work, you will enable us to better index it, making it easier to find.

    Upload a copy of this work     Papers currently archived: 103,566

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

A flexible type system for the small Veblen ordinal.Florian Ranzi & Thomas Strahm - 2019 - Archive for Mathematical Logic 58 (5-6):711-751.
Generalizations of the Kruskal-Friedman theorems.L. Gordeev - 1990 - Journal of Symbolic Logic 55 (1):157-181.
Assignment of Ordinals to Patterns of Resemblance.Gunnar Wilken - 2007 - Journal of Symbolic Logic 72 (2):704 - 720.
Normal forms for elementary patterns.Timothy J. Carlson & Gunnar Wilken - 2012 - Journal of Symbolic Logic 77 (1):174-194.
Ordinal arithmetic and $\Sigma_{1}$ -elementarity.Timothy J. Carlson - 1999 - Archive for Mathematical Logic 38 (7):449-460.
Proof theory and ordinal analysis.W. Pohlers - 1991 - Archive for Mathematical Logic 30 (5-6):311-376.

Analytics

Added to PP
2013-11-23

Downloads
25 (#946,416)

6 months
1 (#1,597,861)

Historical graph of downloads
How can I increase my downloads?

References found in this work

Proof theory.Gaisi Takeuti - 1987 - New York, N.Y., U.S.A.: Sole distributors for the U.S.A. and Canada, Elsevier Science Pub. Co..
A new system of proof-theoretic ordinal functions.W. Buchholz - 1986 - Annals of Pure and Applied Logic 32:195-207.
An independence result for (II11-CA)+BI.Wilfried Buchholz - 1987 - Annals of Pure and Applied Logic 33 (C):131-155.

Add more references