Switch to: Citations

Add references

You must login to add references.
  1. Ü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   162 citations  
  • What's so special about Kruskal's theorem and the ordinal Γo? A survey of some results in proof theory.Jean Gallier - 1991 - Annals of Pure and Applied Logic 53 (3):199-260.
    This paper consists primarily of a survey of results of Harvey Friedman about some proof-theoretic aspects of various forms of Kruskal's tree theorem, and in particular the connection with the ordinal Γ0. We also include a fairly extensive treatment of normal functions on the countable ordinals, and we give a glimpse of Verlen hierarchies, some subsystems of second-order logic, slow-growing and fast-growing hierarchies including Girard's result, and Goodstein sequences. The central theme of this paper is a powerful theorem due to (...)
    Download  
     
    Export citation  
     
    Bookmark   11 citations  
  • Friedman's Research on Subsystems of Second Order Arithmetic.Stephen G. Simpson - 1990 - Journal of Symbolic Logic 55 (2):870-874.
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • The Type Theoretic Interpretation of Constructive Set Theory.Peter Aczel, Angus Macintyre, Leszek Pacholski & Jeff Paris - 1984 - Journal of Symbolic Logic 49 (1):313-314.
    Download  
     
    Export citation  
     
    Bookmark   78 citations  
  • Type-theoretic interpretation of iterated, strictly positive inductive definitions.Erik Palmgren - 1992 - Archive for Mathematical Logic 32 (2):75-99.
    We interpret intuitionistic theories of (iterated) strictly positive inductive definitions (s.p.-ID i′ s) into Martin-Löf's type theory. The main purpose being to obtain lower bounds of the proof-theoretic strength of type theories furnished with means for transfinite induction (W-type, Aczel's set of iterative sets or recursion on (type) universes). Thes.p.-ID i′ s are essentially the wellknownID i -theories, studied in ordinal analysis of fragments of second order arithmetic, but the set variable in the operator form is restricted to occur only (...)
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • 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  
  • (1 other version)The formulæ-as-types notion of construction.W. A. Howard - 1995 - In Philippe De Groote (ed.), The Curry-Howard isomorphism. Louvain-la-Neuve: Academia.
    Download  
     
    Export citation  
     
    Bookmark   68 citations  
  • Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen.Justus Diller - 1974 - Archive for Mathematical Logic 16 (1-2):49-66.
    Download  
     
    Export citation  
     
    Bookmark   27 citations  
  • Infinitely Long Terms of Transfinite Type.W. W. Tait, J. N. Crossley & M. A. E. Dummett - 1975 - Journal of Symbolic Logic 40 (4):623-624.
    Download  
     
    Export citation  
     
    Bookmark   13 citations  
  • Recursive models for constructive set theories.N. Beeson - 1982 - Annals of Mathematical Logic 23 (2/3):127.
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • On the relationship between ATR 0 and.Jeremy Avigad - 1996 - Journal of Symbolic Logic 61 (3):768-779.
    Download  
     
    Export citation  
     
    Bookmark   22 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  
  • What's so special about Kruskal's theorem and the ordinal Γo? A survey of some results in proof theory.Jean H. Gallier - 1991 - Annals of Pure and Applied Logic 53 (3):199-260.
    This paper consists primarily of a survey of results of Harvey Friedman about some proof-theoretic aspects of various forms of Kruskal's tree theorem, and in particular the connection with the ordinal Γ0. We also include a fairly extensive treatment of normal functions on the countable ordinals, and we give a glimpse of Verlen hierarchies, some subsystems of second-order logic, slow-growing and fast-growing hierarchies including Girard's result, and Goodstein sequences. The central theme of this paper is a powerful theorem due to (...)
    Download  
     
    Export citation  
     
    Bookmark   11 citations  
  • Recursive models for constructive set theories.M. Beeson - 1982 - Annals of Mathematical Logic 23 (2-3):127-178.
    Download  
     
    Export citation  
     
    Bookmark   13 citations  
  • (1 other version)Frege Structures and the notions of proposition, truth and set.Peter Aczel - 1980 - Journal of Symbolic Logic 51 (1):244-246.
    Download  
     
    Export citation  
     
    Bookmark   54 citations  
  • Realizability and intuitionistic logic.J. Diller & A. S. Troelstra - 1984 - Synthese 60 (2):253 - 282.
    Download  
     
    Export citation  
     
    Bookmark   15 citations  
  • On the relationships between ATR0 and $\widehat{ID}_{.Jeremy Avigad - 1996 - Journal of Symbolic Logic 61 (3):768 - 779.
    We show that the theory ATR 0 is equivalent to a second-order generalization of the theory $\widehat{ID}_{ . As a result, ATR 0 is conservative over $\widehat{ID}_{ for arithmetic sentences, though proofs in ATR 0 can be much shorter than their $\widehat{ID}_{ counterparts.
    Download  
     
    Export citation  
     
    Bookmark   20 citations