The Suslin operator in applicative theories: Its proof-theoretic analysis via ordinal theories

&
Annals of Pure and Applied Logic 162 (8):647-660 (2011)
  Copy   BIBTEX

Abstract

The Suslin operator is a type-2 functional testing for the well-foundedness of binary relations on the natural numbers. In the context of applicative theories, its proof-theoretic strength has been analyzed in Jäger and Strahm [18]. This article provides a more direct approach to the computation of the upper bounds in question. Several theories featuring the Suslin operator are embedded into ordinal theories tailored for dealing with non-monotone inductive definitions that enable a smooth definition of the application relation

Categories

Keywords

Reprint years

DOI

10.1016/j.apal.2011.01.009

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 101,459

External links

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

Through your library

My notes

Similar books and articles

Totality in applicative theories.Gerhard Jäger & Thomas Strahm - 1995 - Annals of Pure and Applied Logic 74 (2):105-120.
The non-constructive μ operator, fixed point theories with ordinals, and the bar rule.Thomas Strahm - 2000 - Annals of Pure and Applied Logic 104 (1-3):305-324.
Ordinal analysis of non-monotone-definable inductive definitions.Wolfram Pohlers - 2008 - Annals of Pure and Applied Logic 156 (1):160-169.
On the proof theory of type two functionals based on primitive recursive operations.David Steiner & Thomas Strahm - 2006 - Mathematical Logic Quarterly 52 (3):237-252.
The [mathematical formula] quantification operator in explicit mathematics with universes and iterated fixed point theories with ordinals.Markus Marzetta & Thomas Strahm - 1997 - Archive for Mathematical Logic 36 (6):391-413.
Type-theoretic interpretation of iterated, strictly positive inductive definitions.Erik Palmgren - 1992 - Archive for Mathematical Logic 32 (2):75-99.
A flexible type system for the small Veblen ordinal.Florian Ranzi & Thomas Strahm - 2019 - Archive for Mathematical Logic 58 (5-6):711-751.
Systems of explicit mathematics with non-constructive μ-operator. Part I.Solomon Feferman & Gerhard Jäger - 1993 - Annals of Pure and Applied Logic 65 (3):243-263.
Universes over Frege structures.Reinhard Kahle - 2003 - Annals of Pure and Applied Logic 119 (1-3):191-223.
Characterizations of ordinal analysis.James Walsh - 2023 - Annals of Pure and Applied Logic 174 (4):103230.

Analytics

Added to PP
2013-10-27

Downloads
48 (#463,272)

6 months
16 (#195,366)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Add more citations

References found in this work

Fixed points in Peano arithmetic with ordinals.Gerhard Jäger - 1993 - Annals of Pure and Applied Logic 60 (2):119-132.
Definedness.Solomon Feferman - 1995 - Erkenntnis 43 (3):295 - 320.

View all 7 references / Add more references