15 found
Order:
  1.  23
    Aspects of General Topology in Constructive Set Theory.Peter Aczel - 2006 - Annals of Pure and Applied Logic 137 (1):3-29.
    Working in constructive set theory we formulate notions of constructive topological space and set-generated locale so as to get a good constructive general version of the classical Galois adjunction between topological spaces and locales. Our notion of constructive topological space allows for the space to have a class of points that need not be a set. Also our notion of locale allows the locale to have a class of elements that need not be a set. Class sized mathematical structures need (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   14 citations  
  2.  3
    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.
    Direct download  
     
    Export citation  
     
    My bibliography   42 citations  
  3.  20
    The Generalised Type-Theoretic Interpretation of Constructive Set Theory.Nicola Gambino & Peter Aczel - 2006 - Journal of Symbolic Logic 71 (1):67 - 103.
    We present a generalisation of the type-theoretic interpretation of constructive set theory into Martin-Löf type theory. The original interpretation treated logic in Martin-Löf type theory via the propositions-as-types interpretation. The generalisation involves replacing Martin-Löf type theory with a new type theory in which logic is treated as primitive. The primitive treatment of logic in type theories allows us to study reinterpretations of logic, such as the double-negation translation.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography   4 citations  
  4.  26
    On the T1 Axiom and Other Separation Properties in Constructive Point-Free and Point-Set Topology.Peter Aczel & Giovanni Curi - 2010 - Annals of Pure and Applied Logic 161 (4):560-569.
    In this note a T1 formal space is a formal space whose points are closed as subspaces. Any regular formal space is T1. We introduce the more general notion of a formal space, and prove that the class of points of a weakly set-presentable formal space is a set in the constructive set theory CZF. The same also holds in constructive type theory. We then formulate separation properties for constructive topological spaces , strengthening separation properties discussed elsewhere. Finally we relate (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  5.  44
    Binary Refinement Implies Discrete Exponentiation.Peter Aczel, Laura Crosilla, Hajime Ishihara, Erik Palmgren & Peter Schuster - 2006 - Studia Logica 84 (3):361 - 368.
    Working in the weakening of constructive Zermelo-Fraenkel set theory in which the subset collection scheme is omitted, we show that the binary re.nement principle implies all the instances of the exponentiation axiom in which the basis is a discrete set. In particular binary re.nement implies that the class of detachable subsets of a set form a set. Binary re.nement was originally extracted from the fullness axiom, an equivalent of subset collection, as a principle that was su.cient to prove that the (...)
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  6.  7
    The Relation Reflection Scheme.Peter Aczel - 2008 - Mathematical Logic Quarterly 54 (1):5-11.
    We introduce a new axiom scheme for constructive set theory, the Relation Reflection Scheme . Each instance of this scheme is a theorem of the classical set theory ZF. In the constructive set theory CZF–, when the axiom scheme is combined with the axiom of Dependent Choices , the result is equivalent to the scheme of Relative Dependent Choices . In contrast to RDC, the scheme RRS is preserved in Heyting-valued models of CZF– using set-generated frames. We give an application (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  7.  8
    The Strength of Martin-Löf's Intuitionistic Type Theory with One Universe.Peter Aczel, Seppo Miettinen & Jouko Vaananen - 1984 - Journal of Symbolic Logic 49 (1):313-313.
    Direct download  
     
    Export citation  
     
    My bibliography   5 citations  
  8.  18
    Situation Theory and its Applications Vol.Peter Aczel, David Israel, Yosuhiro Katagiri & Stanley Peters (eds.) - 1993 - CSLI Publications.
    Situation Theory and Its Applications, Vol. 1 . Robin Cooper, Kuniaki Mukai, and John Perry (Eds.). Lecture Notes No. 22. ...
    Direct download  
     
    Export citation  
     
    My bibliography   2 citations  
  9.  18
    Rudimentary and Arithmetical Constructive Set Theory.Peter Aczel - 2013 - Annals of Pure and Applied Logic 164 (4):396-415.
    The aim of this paper is to formulate and study two weak axiom systems for the conceptual framework of constructive set theory . Arithmetical CST is just strong enough to represent the class of von Neumann natural numbers and its arithmetic so as to interpret Heyting Arithmetic. Rudimentary CST is a very weak subsystem that is just strong enough to represent a constructive version of Jensenʼs rudimentary set theoretic functions and their theory. The paper is a contribution to the study (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  10.  23
    Describing Ordinals Using Functionals of Transfinite Type.Peter Aczel - 1972 - Journal of Symbolic Logic 37 (1):35-47.
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  11.  19
    Are There Enough Injective Sets?Peter Aczel, Benno Berg, Johan Granström & Peter Schuster - 2013 - Studia Logica 101 (3):467-482.
    The axiom of choice ensures precisely that, in ZFC, every set is projective: that is, a projective object in the category of sets. In constructive ZF (CZF) the existence of enough projective sets has been discussed as an additional axiom taken from the interpretation of CZF in Martin-Löf’s intuitionistic type theory. On the other hand, every non-empty set is injective in classical ZF, which argument fails to work in CZF. The aim of this paper is to shed some light on (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography  
  12.  3
    Binary Refinement Implies Discrete Exponentiation.Peter Aczel, Laura Crosilla, Hajime Ishihara, Erik Palmgren & Peter Schuster - 2006 - Studia Logica 84 (3):361-368.
    Working in the weakening of constructive Zermelo-Fraenkel set theory in which the subset collection scheme is omitted, we show that the binary refinement principle implies all the instances of the exponentiation axiom in which the basis is a discrete set. In particular binary refinement implies that the class of detachable subsets of a set form a set. Binary refinement was originally extracted from the fullness axiom, an equivalent of subset collection, as a principle that was sufficient to prove that the (...)
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  13.  5
    Are There Enough Injective Sets?Peter Aczel, Benno van den Berg, Johan Granström & Peter Schuster - 2013 - Studia Logica 101 (3):467-482.
  14.  17
    Proof Theory: A Selection of Papers From the Leeds Proof Theory Programme, 1990.Peter Aczel, Harold Simmons & S. S. Wainer (eds.) - 1992 - Cambridge University Press.
    This work is derived from the SERC "Logic for IT" Summer School Conference on Proof Theory held at Leeds University. The contributions come from acknowledged experts and comprise expository and research articles which form an invaluable introduction to proof theory aimed at both mathematicians and computer scientists.
    Direct download  
     
    Export citation  
     
    My bibliography  
  15. Situation Theory and its Applications, Volume 3.Peter Aczel, David Israel, Stanley Peters & Yasuhiro Katagiri (eds.) - 1993 - Center for the Study of Language and Inf.
    No categories
     
    Export citation  
     
    My bibliography