Switch to: References

Add citations

You must login to add citations.
  1. Epistemology Versus Ontology: Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf.Peter Dybjer, Sten Lindström, Erik Palmgren & Göran Sundholm (eds.) - 2012 - Dordrecht, Netherland: Springer.
    This book brings together philosophers, mathematicians and logicians to penetrate important problems in the philosophy and foundations of mathematics. In philosophy, one has been concerned with the opposition between constructivism and classical mathematics and the different ontological and epistemological views that are reflected in this opposition. The dominant foundational framework for current mathematics is classical logic and set theory with the axiom of choice. This framework is, however, laden with philosophical difficulties. One important alternative foundational programme that is actively pursued (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • A cumulative hierarchy of sets for constructive set theory.Albert Ziegler - 2014 - Mathematical Logic Quarterly 60 (1-2):21-30.
    The von Neumann hierarchy of sets is heavily used as a basic tool in classical set theory, being an underlying ingredient in many proofs and concepts. In constructive set theories like without the powerset axiom however, it loses much of its potency by ceasing to be a hierarchy of sets as its single stages become only classes. This article proposes an alternative cumulative hierarchy which does not have this drawback and provides examples of how it can be used to prove (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Non-deterministic inductive definitions.Benno van den Berg - 2013 - Archive for Mathematical Logic 52 (1-2):113-135.
    We study a new proof principle in the context of constructive Zermelo-Fraenkel set theory based on what we will call “non-deterministic inductive definitions”. We give applications to formal topology as well as a predicative justification of this principle.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • 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  
  • From the weak to the strong existence property.Michael Rathjen - 2012 - Annals of Pure and Applied Logic 163 (10):1400-1418.
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • Constructive Zermelo–Fraenkel set theory and the limited principle of omniscience.Michael Rathjen - 2014 - Annals of Pure and Applied Logic 165 (2):563-572.
    In recent years the question of whether adding the limited principle of omniscience, LPO, to constructive Zermelo–Fraenkel set theory, CZF, increases its strength has arisen several times. As the addition of excluded middle for atomic formulae to CZF results in a rather strong theory, i.e. much stronger than classical Zermelo set theory, it is not obvious that its augmentation by LPO would be proof-theoretically benign. The purpose of this paper is to show that CZF+RDC+LPO has indeed the same strength as (...)
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • Kripke models for subtheories of CZF.Rosalie Iemhoff - 2010 - Archive for Mathematical Logic 49 (2):147-167.
    In this paper a method to construct Kripke models for subtheories of constructive set theory is introduced that uses constructions from classical model theory such as constructible sets and generic extensions. Under the main construction all axioms except the collection axioms can be shown to hold in the constructed Kripke model. It is shown that by carefully choosing the classical models various instances of the collection axioms, such as exponentiation, can be forced to hold as well. The paper does not (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations