Switch to: Citations

Add references

You must login to add references.
  1. Recent Advances in Ordinal Analysis: Π 1 2 — CA and Related Systems.Michael Rathjen - 1995 - Bulletin of Symbolic Logic 1 (4):468-485.
    §1. Introduction. The purpose of this paper is, in general, to report the state of the art of ordinal analysis and, in particular, the recent success in obtaining an ordinal analysis for the system of-analysis, which is the subsystem of formal second order arithmetic, Z2, with comprehension confined to-formulae. The same techniques can be used to provide ordinal analyses for theories that are reducible to iterated-comprehension, e.g.,-comprehension. The details will be laid out in [28].Ordinal-theoretic proof theory came into existence in (...)
    Download  
     
    Export citation  
     
    Bookmark   21 citations  
  • Note on the Fan theorem.A. S. Troelstra - 1974 - Journal of Symbolic Logic 39 (3):584-596.
    Download  
     
    Export citation  
     
    Bookmark   16 citations  
  • Godel's unpublished papers on foundations of mathematics.W. W. Tatt - 2001 - Philosophia Mathematica 9 (1):87-126.
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • Eckart Menzler-Trott. Translated by Craig Smoryński and Edward Griffor. Logic's lost genius: The life of Gerhard Gentzen. History of mathematics, vol. 33. American Mathematical Society, Providence, RI, 2007, xxii+441 pp. [REVIEW]W. W. Tait - 2010 - Bulletin of Symbolic Logic 16 (2):270-275.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Gödel's reformulation of Gentzen's first consistency proof for arithmetic: The no-counterexample interpretation.W. W. Tait - 2005 - Bulletin of Symbolic Logic 11 (2):225-238.
    The last section of “Lecture at Zilsel’s” [9, §4] contains an interesting but quite condensed discussion of Gentzen’s first version of his consistency proof for P A [8], reformulating it as what has come to be called the no-counterexample interpretation. I will describe Gentzen’s result (in game-theoretic terms), fill in the details (with some corrections) of Godel's reformulation, and discuss the relation between the two proofs.
    Download  
     
    Export citation  
     
    Bookmark   10 citations  
  • The Collected Papers of Gerhard Gentzen. [REVIEW]G. Kreisel - 1971 - Journal of Philosophy 68 (8):238-265.
    Download  
     
    Export citation  
     
    Bookmark   33 citations  
  • Proof theory of reflection.Michael Rathjen - 1994 - Annals of Pure and Applied Logic 68 (2):181-224.
    The paper contains proof-theoretic investigation on extensions of Kripke-Platek set theory, KP, which accommodate first-order reflection. Ordinal analyses for such theories are obtained by devising cut elimination procedures for infinitary calculi of ramified set theory with Пn reflection rules. This leads to consistency proofs for the theories KP+Пn reflection using a small amount of arithmetic and the well-foundedness of a certain ordinal system with respect to primitive decending sequences. Regarding future work, we intend to avail ourselves of these new cut (...)
    Download  
     
    Export citation  
     
    Bookmark   37 citations  
  • Recent advances in ordinal analysis: Π 21-CA and related systems.Michael Rathjen - 1995 - Bulletin of Symbolic Logic 1 (4):468 - 485.
    §1. Introduction. The purpose of this paper is, in general, to report the state of the art of ordinal analysis and, in particular, the recent success in obtaining an ordinal analysis for the system of -analysis, which is the subsystem of formal second order arithmetic, Z2, with comprehension confined to -formulae. The same techniques can be used to provide ordinal analyses for theories that are reducible to iterated -comprehension, e.g., -comprehension. The details will be laid out in [28].Ordinal-theoretic proof theory (...)
    Download  
     
    Export citation  
     
    Bookmark   17 citations  
  • An ordinal analysis of parameter free Π12-comprehension.Michael Rathjen - 2005 - Archive for Mathematical Logic 44 (3):263-362.
    Abstract.This paper is the second in a series of three culminating in an ordinal analysis of Π12-comprehension. Its objective is to present an ordinal analysis for the subsystem of second order arithmetic with Δ12-comprehension, bar induction and Π12-comprehension for formulae without set parameters. Couched in terms of Kripke-Platek set theory, KP, the latter system corresponds to KPi augmented by the assertion that there exists a stable ordinal, where KPi is KP with an additional axiom stating that every set is contained (...)
    Download  
     
    Export citation  
     
    Bookmark   18 citations  
  • An ordinal analysis of stability.Michael Rathjen - 2005 - Archive for Mathematical Logic 44 (1):1-62.
    Abstract.This paper is the first in a series of three which culminates in an ordinal analysis of Π12-comprehension. On the set-theoretic side Π12-comprehension corresponds to Kripke-Platek set theory, KP, plus Σ1-separation. The strength of the latter theory is encapsulated in the fact that it proves the existence of ordinals π such that, for all β>π, π is β-stable, i.e. Lπ is a Σ1-elementary substructure of Lβ. The objective of this paper is to give an ordinal analysis of a scenario of (...)
    Download  
     
    Export citation  
     
    Bookmark   12 citations  
  • Logic's lost genius: The life of Gerhard Gentzen. History of mathematics, vol. 33.W. Tait - 2010 - Bulletin of Symbolic Logic 16 (2):270-275.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • On the interpretation of non-finitist proofs–Part II.G. Kreisel - 1952 - Journal of Symbolic Logic 17 (1):43-58.
    Download  
     
    Export citation  
     
    Bookmark   31 citations  
  • On the interpretation of non-finitist proofs—Part I.G. Kreisel - 1951 - Journal of Symbolic Logic 16 (4):241-267.
    Download  
     
    Export citation  
     
    Bookmark   27 citations  
  • Hilbert's programme.Georg Kreisel - 1958 - Dialectica 12 (3‐4):346-372.
    Hilbert's plan for understanding the concept of infinity required the elimination of non‐finitist machinery from proofs of finitist assertions. The failure of the original plan leads to a hierarchy of progressively less elementary, but still constructive methods instead of finitist ones . A mathematical proof of this failure requires a definition of « finitist ».—The paper sketches the three principal methods for the syntactic analysis of non‐constructive mathematics, the resulting consistency proofs and constructive interpretations, modelled on Herbrand's theorem, and their (...)
    Download  
     
    Export citation  
     
    Bookmark   26 citations  
  • Hilbert's Programme.Georg Kreisel - 1962 - Journal of Symbolic Logic 27 (2):228-229.
    Download  
     
    Export citation  
     
    Bookmark   17 citations  
  • Der erste Widerspruchsfreiheitsbeweis für die klassische Zahlentheorie.Gerhard Gentzen - 1974 - Archive for Mathematical Logic 16 (3-4):97-118.
    Download  
     
    Export citation  
     
    Bookmark   11 citations  
  • Die Gegenwärtige Lage in der Mathematischen Grundlagenforschung.Rózsa Péter - 1938 - Journal of Symbolic Logic 3 (4):166-167.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Beweisbarkeit und Unbeweisbarkeit von Anfangsfallen der Transfiniten Induktion in der reinen Zahlentheorie.Gerhard Gentzen - 1944 - Journal of Symbolic Logic 9 (3):70-72.
    Download  
     
    Export citation  
     
    Bookmark   15 citations  
  • Über eine bisher noch nicht benützte erweiterung Des finiten standpunktes.Von Kurt Gödel - 1958 - Dialectica 12 (3‐4):280-287.
    ZusammenfassungP. Bernays hat darauf hingewiesen, dass man, um die Widerspruchs freiheit der klassischen Zahlentheorie zu beweisen, den Hilbertschen flniter Standpunkt dadurch erweitern muss, dass man neben den auf Symbole sich beziehenden kombinatorischen Begriffen gewisse abstrakte Begriffe zulässt, Die abstrakten Begriffe, die bisher für diesen Zweck verwendet wurden, sinc die der konstruktiven Ordinalzahltheorie und die der intuitionistischer. Logik. Es wird gezeigt, dass man statt deesen den Begriff einer berechenbaren Funktion endlichen einfachen Typs über den natürlichen Zahler benutzen kann, wobei keine anderen (...)
    Download  
     
    Export citation  
     
    Bookmark   161 citations  
  • On interpreting Gödel's second theorem.Michael Detlefsen - 1979 - Journal of Philosophical Logic 8 (1):297 - 313.
    In this paper I have considered various attempts to attribute significance to Gödel's second incompleteness theorem (G2 for short). Two of these attempts (Beth-Cohen and the position maintaining that G2 shows the failure of Hilbert's Program), I have argued, are false. Two others (an argument suggested by Beth, Cohen and ??? and Resnik's Interpretation), I argue, are groundless.
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • Notation systems for infinitary derivations.Wilfried Buchholz - 1991 - Archive for Mathematical Logic 30 (5-6):277-296.
    Download  
     
    Export citation  
     
    Bookmark   30 citations  
  • Explaining the Gentzen–Takeuti reduction steps: a second-order system.Wilfried Buchholz - 2001 - Archive for Mathematical Logic 40 (4):255-272.
    Using the concept of notations for infinitary derivations we give an explanation of Takeuti's reduction steps on finite derivations (used in his consistency proof for Π1 1-CA) in terms of the more perspicious infinitary approach from [BS88].
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • On the Original Gentzen Consistency Proof for Number Theory.Paul Bernays, A. Kino, J. Myhill & R. E. Vesley - 1975 - Journal of Symbolic Logic 40 (1):95-95.
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • Wellfoundedness proofs by means of non-monotonic inductive definitions II: first order operators.Toshiyasu Arai - 2010 - Annals of Pure and Applied Logic 162 (2):107-143.
    Download  
     
    Export citation  
     
    Bookmark   6 citations  
  • Wellfoundedness proofs by means of non-monotonic inductive definitions I: Π₂⁰-operators.Toshiyasu Arai - 2004 - Journal of Symbolic Logic 69 (3):830-850.
    In this paper, we prove the wellfoundedness of recursive notation systems for reflecting ordinals up to Π₃-reflection by relevant inductive definitions.
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • Proof theory for theories of ordinals—I: recursively Mahlo ordinals.Toshiyasu Arai - 2003 - Annals of Pure and Applied Logic 122 (1-3):1-85.
    This paper deals with a proof theory for a theory T22 of recursively Mahlo ordinals in the form of Π2-reflecting on Π2-reflecting ordinals using a subsystem Od of the system O of ordinal diagrams in Arai 353). This paper is the first published one in which a proof-theoretic analysis à la Gentzen–Takeuti of recursively large ordinals is expounded.
    Download  
     
    Export citation  
     
    Bookmark   16 citations  
  • Proof theory for theories of ordinals II: Π3-reflection.Toshiyasu Arai - 2004 - Annals of Pure and Applied Logic 129 (1-3):39-92.
    This paper deals with a proof theory for a theory T3 of Π3-reflecting ordinals using the system O of ordinal diagrams in Arai 1375). This is a sequel to the previous one 1) in which a theory for recursively Mahlo ordinals is analyzed proof-theoretically.
    Download  
     
    Export citation  
     
    Bookmark   12 citations  
  • Proof theory for theories of ordinals II:< i> Π_< sub> 3-reflection.Toshiyasu Arai - 2004 - Annals of Pure and Applied Logic 129 (1):39-92.
    Download  
     
    Export citation  
     
    Bookmark   6 citations