9 found
Order:
  1.  22
    Fragments of Heyting Arithmetic.Wolfgang Burr - 2000 - Journal of Symbolic Logic 65 (3):1223-1240.
    We define classes $\Phi_n$ of formulae of first-order arithmetic with the following properties: Every $\varphi \in \Phi_n$ is classically equivalent to a $\Pi_n$-formula $. $\bigcup_{n\in \omega} \Phi_n = \mathscr L_A$. $I\Pi_n$ and $i\Phi_n$ prove the same $\Pi_2$-formulae. We further generalize a result by Visser and Wehmeier, namely that prenex induction within intuitionistic arithmetic is rather weak: After closing $\Phi_n$ both under existential and universal quantification the corresponding theories i$\Theta_n$ still prove the same $\Pi_2$-formulae. In a second part we consider i$\Delta_0$ (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  2.  10
    A Diller-Nahm-Style Functional Interpretation of $\Hbox{\Sf KP} \Omega$.Wolfgang Burr - 2000 - Archive for Mathematical Logic 39 (8):599-604.
    The Dialectica-style functional interpretation of Kripke-Platek set theory with infinity ( $\hbox{\sf KP} \omega$ ) given in [1] uses a choice functional (which is not a definable set function of ( $hbox{\sf KP} \omega$ ). By means of a Diller-Nahm-style interpretation (cf. [4]) it is possible to eliminate the choice functional and give an interpretation by set functionals primitive recursive in $x\mapsto\omega$ . This yields the following characterization: The class of $\Sigma$ -definable set functions of $\hbox{\sf KP} \omega$ coincides with (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  3.  10
    Functional Interpretation of Aczel's Constructive Set Theory.Wolfgang Burr - 2000 - Annals of Pure and Applied Logic 104 (1-3):31-73.
    In the present paper we give a functional interpretation of Aczel's constructive set theories CZF − and CZF in systems T ∈ and T ∈ + of constructive set functionals of finite types. This interpretation is obtained by a translation × , a refinement of the ∧ -translation introduced by Diller and Nahm 49–66) which again is an extension of Gödel's Dialectica translation. The interpretation theorem gives characterizations of the definable set functions of CZF − and CZF in terms of (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  4.  10
    A Characterization of the $\Sigma_1$ -Definable Functions of $KP\Omega + $.Wolfgang Burr & Volker Hartung - 1998 - Archive for Mathematical Logic 37 (3):199-214.
    The subject of this paper is a characterization of the $\Sigma_1$ -definable set functions of Kripke-Platek set theory with infinity and a uniform version of axiom of choice: $KP\omega+(uniform\;AC)$ . This class of functions is shown to coincide with the collection of set functionals of type 1 primitive recursive in a given choice functional and $x\mapsto\omega$ . This goal is achieved by a Gödel Dialectica-style functional interpretation of $KP\omega+(uniform\;AC)$ and a computability proof for the involved functionals.
    No categories
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  5.  6
    A Diller-Nahm-Style Functional Interpretation of [Mathematical Formula].Wolfgang Burr - 2000 - Archive for Mathematical Logic 8.
  6.  35
    Concepts and Aims of Functional Interpretations: Towards a Functional Interpretation of Constructive Set Theory.Wolfgang Burr - 2002 - Synthese 133 (1-2):257 - 274.
    The aim of this article is to give an introduction to functional interpretations of set theory given by the authorin Burr (2000a). The first part starts with some general remarks on Gödel's functional interpretation with a focus on aspects related to problems that arise in the context of set theory. The second part gives an insight in the techniques needed to perform a functional interpretation of systems of set theory. However, the first part of this article is not intended to (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  7. A Characterization of the Σ 1 -Definable Functions of KPω +.Wolfgang Burr & Volker Hartung - 2001 - Bulletin of Symbolic Logic 7 (4):532-533.
  8.  7
    A Characterization of the [Mathematical Formula]-Definable Functions of [Mathematical Formula].Wolfgang Burr & Volker Hartung - 1997 - Archive for Mathematical Logic 3.
    Direct download  
     
    Export citation  
     
    Bookmark  
  9. Fragments of Heyting Arithmetic.Wolfgang Burr - 2002 - Bulletin of Symbolic Logic 8 (4):533-534.
     
    Export citation  
     
    Bookmark