Switch to: References

Add citations

You must login to add citations.
  1. Predicativity through transfinite reflection.Andrés Cordón-Franco, David Fernández-Duque, Joost J. Joosten & Francisco Félix Lara-martín - 2017 - Journal of Symbolic Logic 82 (3):787-808.
    Let T be a second-order arithmetical theory, Λ a well-order, λ < Λ and X ⊆ ℕ. We use $[\lambda |X]_T^{\rm{\Lambda }}\varphi$ as a formalization of “φ is provable from T and an oracle for the set X, using ω-rules of nesting depth at most λ”.For a set of formulas Γ, define predicative oracle reflection for T over Γ ) to be the schema that asserts that, if X ⊆ ℕ, Λ is a well-order and φ ∈ Γ, then$$\forall \,\lambda (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Large sets in intuitionistic set theory.Harvey Friedman & Andrej Ščedrov - 1984 - Annals of Pure and Applied Logic 27 (1):1-24.
    We consider properties of sets in an intuitionistic setting corresponding to large cardinals in classical set theory. Adding such ‘large set axioms’ to intuitionistic ZF set theory does not violate well-know metamathematical properties of intuitionistic systems. Moreover, we consider statements in constructive analysis equivalent to the consistency of such ‘large set axioms’.
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • On the impossibility of explicit upper bounds on lengths of some provably finite algorithms in computable analysis.Andre Scedrov - 1986 - Annals of Pure and Applied Logic 32:291-297.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • CZF does not have the existence property.Andrew W. Swan - 2014 - Annals of Pure and Applied Logic 165 (5):1115-1147.
    Constructive theories usually have interesting metamathematical properties where explicit witnesses can be extracted from proofs of existential sentences. For relational theories, probably the most natural of these is the existence property, EP, sometimes referred to as the set existence property. This states that whenever ϕϕ is provable, there is a formula χχ such that ϕ∧χϕ∧χ is provable. It has been known since the 80s that EP holds for some intuitionistic set theories and yet fails for IZF. Despite this, it has (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Effective inseparability in a topological setting.Dieter Spreen - 1996 - Annals of Pure and Applied Logic 80 (3):257-275.
    Effective inseparability of pairs of sets is an important notion in logic and computer science. We study the effective inseparability of sets which appear as index sets of subsets of an effectively given topological T0-space and discuss its consequences. It is shown that for two disjoint subsets X and Y of the space one can effectively find a witness that the index set of X cannot be separated from the index set of Y by a recursively enumerable set, if X (...)
    Download  
     
    Export citation  
     
    Bookmark   4 citations