Switch to: References

Citations of:

Beweistheorie von KPN

Kurt Schutte & Gerhard Jager

Journal of Symbolic Logic 48 (3):879 (1983)

Add citations

You must login to add citations.

Fixed points in Peano arithmetic with ordinals.Gerhard Jäger - 1993 - Annals of Pure and Applied Logic 60 (2):119-132.details Jäger, G., Fixed points in Peano arithmetic with ordinals, Annals of Pure and Applied Logic 60 119-132. This paper deals with some proof-theoretic aspects of fixed point theories over Peano arithmetic with ordinals. It studies three such theories which differ in the principles which are available for induction on the natural numbers and ordinals. The main result states that there is a natural theory in this framework which is a conservative extension of Peano arithmeti. Download Export citation Bookmark 21 citations
Full operational set theory with unbounded existential quantification and power set.Gerhard Jäger - 2009 - Annals of Pure and Applied Logic 160 (1):33-52.details We study the extension of Feferman’s operational set theory provided by adding operational versions of unbounded existential quantification and power set and determine its proof-theoretic strength in terms of a suitable theory of sets and classes. Download Export citation Bookmark 9 citations
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.details The aim of this article is to give the proof-theoretic analysis of various subsystems of Feferman's theory T1 for explicit mathematics which contain the non-constructive μ-operator and join. We make use of standard proof-theoretic techniques such as cut-elimination of appropriate semiformal systems and asymmetrical interpretations in standard structures for explicit mathematics. Download Export citation Bookmark 10 citations
Universes over Frege structures.Reinhard Kahle - 2003 - Annals of Pure and Applied Logic 119 (1-3):191-223.details In this paper, we study a concept of universe for a truth predicate over applicative theories. A proof-theoretic analysis is given by use of transfinitely iterated fixed point theories . The lower bound is obtained by a syntactical interpretation of these theories. Thus, universes over Frege structures represent a syntactically expressive framework of metapredicative theories in the context of applicative theories. Download Export citation Bookmark 5 citations

1