The non-constructive μ operator, fixed point theories with ordinals, and the bar rule

Annals of Pure and Applied Logic 104 (1-3):305-324 (2000)
  Copy   BIBTEX

Abstract

This paper deals with the proof theory of first-order applicative theories with non-constructive μ operator and a form of the bar rule, yielding systems of ordinal strength Γ0 and 20, respectively. Relevant use is made of fixed-point theories with ordinals plus bar rule

Categories

Keywords

Reprint years

DOI

10.1016/s0168-0072(00)00016-6

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,061

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 [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.
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.
The \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document} $\mu$\end{document} quantification operator in explicit mathematics with universes and iterated fixed point theories with ordinals. [REVIEW]Markus Marzetta & Thomas Strahm - 1998 - Archive for Mathematical Logic 37 (5-6):391-413.
Systems of explicit mathematics with non-constructive μ-operator. Part II.Solomon Feferman & Gerhard Jäger - 1996 - Annals of Pure and Applied Logic 79 (1):37-52.
Fixed points in Peano arithmetic with ordinals.Gerhard Jäger - 1993 - Annals of Pure and Applied Logic 60 (2):119-132.
The Suslin operator in applicative theories: Its proof-theoretic analysis via ordinal theories.Gerhard Jäger & Dieter Probst - 2011 - Annals of Pure and Applied Logic 162 (8):647-660.
Systems of explicit mathematics with non-constructive μ-operator and join.Thomas Glaß & Thomas Strahm - 1996 - Annals of Pure and Applied Logic 82 (2):193-219.
Some theories with positive induction of ordinal strength ϕω.Gerhard Jäger & Thomas Strahm - 1996 - Journal of Symbolic Logic 61 (3):818-842.
Proof theory for theories of ordinals—I: recursively Mahlo ordinals.Toshiyasu Arai - 2003 - Annals of Pure and Applied Logic 122 (1-3):1-85.

Analytics

Added to PP
2014-01-16

Downloads
29 (#809,878)

6 months
10 (#280,518)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Unfolding finitist arithmetic.Solomon Feferman & Thomas Strahm - 2010 - Review of Symbolic Logic 3 (4):665-689.
Universes over Frege structures.Reinhard Kahle - 2003 - Annals of Pure and Applied Logic 119 (1-3):191-223.

Add more citations

References found in this work

Systems of predicative analysis.Solomon Feferman - 1964 - Journal of Symbolic Logic 29 (1):1-30.
The unfolding of non-finitist arithmetic.Solomon Feferman & Thomas Strahm - 2000 - Annals of Pure and Applied Logic 104 (1-3):75-96.

View all 14 references / Add more references