34 found
Sort by:
  1. Erik Palmgren (2014). Formal Continuity Implies Uniform Continuity Near Compact Images on Metric Spaces. Mathematical Logic Quarterly 60 (1-2):66-69.
    No categories
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  2. Josef Berger, Hajime Ishihara, Erik Palmgren & Peter Schuster (2012). A Predicative Completion of a Uniform Space. Annals of Pure and Applied Logic 163 (8):975-980.
  3. Sten Lindström, Erik Palmgren & Dag Westerståhl (2012). Introduction: The Philosophy of Logical Consequence and Inference. Synthese 187 (3):817-820.
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  4. Erik Palmgren (2012). Constructivist and Structuralist Foundations: Bishop's and Lawvere's Theories of Sets. Annals of Pure and Applied Logic 163 (10):1384-1399.
  5. Erik Palmgren (2012). Proof-Relevance of Families of Setoids and Identity in Type Theory. Archive for Mathematical Logic 51 (1-2):35-47.
    Families of types are fundamental objects in Martin-Löf type theory. When extending the notion of setoid (type with an equivalence relation) to families of setoids, a choice between proof-relevant or proof-irrelevant indexing appears. It is shown that a family of types may be canonically extended to a proof-relevant family of setoids via the identity types, but that such a family is in general proof-irrelevant if, and only if, the proof-objects of identity types are unique. A similar result is shown for (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  6. Thierry Coquand, Erik Palmgren & Bas Spitters (2011). Metric Complements of Overt Closed Sets. Mathematical Logic Quarterly 57 (4):373-378.
    We show that the set of points of an overt closed subspace of a metric completion of a Bishop-locally compact metric space is located. Consequently, if the subspace is, moreover, compact, then its collection of points is Bishop-compact. © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  7. Sten Lindström & Erik Palmgren (2009). Introduction: The Three Foundational Programmes. In Sten Lindström, Erik Palmgren, Krister Segerberg & Viggo Stoltenberg-Hansen (eds.), Logicism, Intuitionism and Formalism: What has become of them? Springer.
  8. Sten Lindström, Erik Palmgren, Krister Segerberg & Viggo Stoltenberg-Hansen (eds.) (2009). Logicism, Intuitionism, and Formalism - What has Become of Them? Springer.
    These questions are addressed in this volume by leading mathematical logicians and philosophers of mathematics.A special section is concerned with constructive ...
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  9. Erik Palmgren (2008). Resolution of the Uniform Lower Bound Problem in Constructive Analysis. Mathematical Logic Quarterly 54 (1):65-69.
    In a previous paper we constructed a full and faithful functor ℳ from the category of locally compact metric spaces to the category of formal topologies . Here we show that for a real-valued continuous function f, ℳ factors through the localic positive reals if, and only if, f has a uniform positive lower bound on each ball in the locally compact space. We work within the framework of Bishop constructive mathematics, where the latter notion is strictly stronger than point-wise (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  10. Erik Palmgren & Steven J. Vickers (2007). Partial Horn Logic and Cartesian Categories. Annals of Pure and Applied Logic 145 (3):314-353.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  11. Peter Aczel, Laura Crosilla, Hajime Ishihara, Erik Palmgren & Peter Schuster (2006). Binary Refinement Implies Discrete Exponentiation. 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)  
     
    My bibliography  
     
    Export citation  
  12. Hajime Ishihara & Erik Palmgren (2006). Quotient Topologies in Constructive Set Theory and Type Theory. Annals of Pure and Applied Logic 141 (1):257-265.
    The standard construction of quotient spaces in topology uses full separation and power sets. We show how to make this construction using only the predicative methods available in constructive type theory and constructive set theory.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  13. Erik Palmgren (2006). Maximal and Partial Points in Formal Spaces. Annals of Pure and Applied Logic 137 (1):291-298.
    The class of points in a set-presented formal topology is a set, if all points are maximal. To prove this constructively a strengthening of the dependent choice principle to infinite well-founded trees is used.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  14. Erik Palmgren (2006). Regular Universes and Formal Spaces. Annals of Pure and Applied Logic 137 (1):299-316.
    We present an alternative solution to the problem of inductive generation of covers in formal topology by using a restricted form of type universes. These universes are at the same time constructive analogues of regular cardinals and sets of infinitary formulae. The technique of regular universes is also used to construct canonical positivity predicates for inductively generated covers.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  15. Erik Palmgren (2005). Constructive Completions of Ordered Sets, Groups and Fields. Annals of Pure and Applied Logic 135 (1-3):243-262.
    In constructive mathematics it is of interest to consider a more general, but classically equivalent, notion of linear order, a so-called pseudo-order. The prime example is the order of the constructive real numbers. We examine two kinds of constructive completions of pseudo-orders: order completions of pseudo-orders and Cauchy completions of ordered groups and fields. It is shown how these can be predicatively defined in type theory, also when the underlying set is non-discrete. Provable choice principles, in particular a generalisation of (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  16. Thierry Coquand & Erik Palmgren (2002). Metric Boolean Algebras and Constructive Measure Theory. Archive for Mathematical Logic 41 (7):687-704.
    This work concerns constructive aspects of measure theory. By considering metric completions of Boolean algebras – an approach first suggested by Kolmogorov – one can give a very simple construction of e.g. the Lebesgue measure on the unit interval. The integration spaces of Bishop and Cheng turn out to give examples of such Boolean algebras. We analyse next the notion of Borel subsets. We show that the algebra of such subsets can be characterised in a pointfree and constructive way by (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  17. Ieke Moerdijk & Erik Palmgren (2002). Type Theories, Toposes and Constructive Set Theory: Predicative Aspects of AST. Annals of Pure and Applied Logic 114 (1-3):155-201.
    We introduce a predicative version of topos based on the notion of small maps in algebraic set theory, developed by Joyal and one of the authors. Examples of stratified pseudotoposes can be constructed in Martin-Löf type theory, which is a predicative theory. A stratified pseudotopos admits construction of the internal category of sheaves, which is again a stratified pseudotopos. We also show how to build models of Aczel-Myhill constructive set theory using this categorical structure.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  18. Erik Palmgren (2002). An Intuitionistic Axiomatisation of Real Closed Fields. Mathematical Logic Quarterly 48 (2):297-299.
    We give an intuitionistic axiomatisation of real closed fields which has the constructive reals as a model. The main result is that this axiomatisation together with just the decidability of the order relation gives the classical theory of real closed fields. To establish this we rely on the quantifier elimination theorem for real closed fields due to Tarski, and a conservation theorem of classical logic over intuitionistic logic for geometric theories.
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  19. Erik Palmgren (2001). Review: Wilfried Buchholz, An Intuitionistic Fixed Point Theory. [REVIEW] Bulletin of Symbolic Logic 7 (3):391-392.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  20. Thierry Coquand & Erik Palmgren (2000). Intuitionistic Choice and Classical Logic. Archive for Mathematical Logic 39 (1):53-74.
    . The effort in providing constructive and predicative meaning to non-constructive modes of reasoning has almost without exception been applied to theories with full classical logic [4]. In this paper we show how to combine unrestricted countable choice, induction on infinite well-founded trees and restricted classical logic in constructively given models. These models are sheaf models over a $\sigma$ -complete Boolean algebra, whose topologies are generated by finite or countable covering relations. By a judicious choice of the Boolean algebra we (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  21. Ieke Moerdijk & Erik Palmgren (2000). Wellfounded Trees in Categories. Annals of Pure and Applied Logic 104 (1-3):189-218.
    In this paper we present and study a categorical formulation of the W-types of Martin-Löf. These are essentially free term algebras where the operations may have finite or infinite arity. It is shown that W-types are preserved under the construction of sheaves and Artin gluing. In the proofs we avoid using impredicative or nonconstructive principles.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  22. Dag Normann, Erik Palmgren & Viggo Stoltenberg-Hansen (1999). Hyperfinite Type Structures. Journal of Symbolic Logic 64 (3):1216-1242.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  23. Erik Palmgren (1998). Developments in Constructive Nonstandard Analysis. Bulletin of Symbolic Logic 4 (3):233-272.
    We develop a constructive version of nonstandard analysis, extending Bishop's constructive analysis with infinitesimal methods. A full transfer principle and a strong idealisation principle are obtained by using a sheaf-theoretic construction due to I. Moerdijk. The construction is, in a precise sense, a reduced power with variable filter structure. We avoid the nonconstructive standard part map by the use of nonstandard hulls. This leads to an infinitesimal analysis which includes nonconstructive theorems such as the Heine-Borel theorem, the Cauchy-Peano existence theorem (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  24. Michael Rathjen, Edward R. Griffor & Erik Palmgren (1998). Inaccessibility in Constructive Set Theory and Type Theory. Annals of Pure and Applied Logic 94 (1-3):181-200.
    This paper is the first in a series whose objective is to study notions of large sets in the context of formal theories of constructivity. The two theories considered are Aczel's constructive set theory and Martin-Löf's intuitionistic theory of types. This paper treats Mahlo's π-numbers which give rise classically to the enumerations of inaccessibles of all transfinite orders. We extend the axioms of CZF and show that the resulting theory, when augmented by the tertium non-datur, is equivalent to ZF plus (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  25. Ieke Moerdijk & Erik Palmgren (1997). Minimal Models of Heyting Arithmetic. Journal of Symbolic Logic 62 (4):1448-1460.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  26. Erik Palmgren (1997). A Sheaf-Theoretic Foundation for Nonstandard Analysis. Annals of Pure and Applied Logic 85 (1):69-86.
    A new foundation for constructive nonstandard analysis is presented. It is based on an extension of a sheaf-theoretic model of nonstandard arithmetic due to I. Moerdijk. The model consists of representable sheaves over a site of filter bases. Nonstandard characterisations of various notions from analysis are obtained: modes of convergence, uniform continuity and differentiability, and some topological notions. We also obtain some additional results about the model. As in the classical case, the order type of the nonstandard natural numbers is (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  27. Erik Palmgren (1997). Constructive Sheaf Semantics. Mathematical Logic Quarterly 43 (3):321-327.
    Sheaf semantics is developed within a constructive and predicative framework, Martin-Löf's type theory. We prove strong completeness of many sorted, first order intuitionistic logic with respect to this semantics, by using sites of provably functional relations.
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  28. Erik Palmgren & Viggo Stoltenberg-Hansen (1997). A Logical Presentation of the Continuous Functionals. Journal of Symbolic Logic 62 (3):1021-1034.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  29. Erik Palmgren (1995). A Constructive Approach to Nonstandard Analysis. Annals of Pure and Applied Logic 73 (3):297-325.
    In the present paper we introduce a constructive theory of nonstandard arithmetic in higher types. The theory is intended as a framework for developing elementary nonstandard analysis constructively. More specifically, the theory introduced is a conservative extension of HAω + AC. A predicate for distinguishing standard objects is added as in Nelson's internal set theory. Weak transfer and idealisation principles are proved from the axioms. Finally, the use of the theory is illustrated by extending Bishop's constructive analysis with infinitesimals.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  30. Erik Palmgren (1995). The Friedman‐Translation for Martin‐Löf's Type Theory. Mathematical Logic Quarterly 41 (3):314-326.
    In this note we show that Friedman's syntactic translation for intuitionistic logical systems can be carried over to Martin-Löf's type theory, inlcuding universes provided some restrictions are made. Using this translation we show that the theory is closed under a higher type version of Markov's rule.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  31. Erik Palmgren (1993). A Note on Mathematics of Infinity. Journal of Symbolic Logic 58 (4):1195-1200.
  32. Erik Palmgren (1992). Type-Theoretic Interpretation of Iterated, Strictly Positive Inductive Definitions. Archive for Mathematical Logic 32 (2):75-99.
    We interpret intuitionistic theories of (iterated) strictly positive inductive definitions (s.p.-ID i′ s) into Martin-Löf's type theory. The main purpose being to obtain lower bounds of the proof-theoretic strength of type theories furnished with means for transfinite induction (W-type, Aczel's set of iterative sets or recursion on (type) universes). Thes.p.-ID i′ s are essentially the wellknownID i -theories, studied in ordinal analysis of fragments of second order arithmetic, but the set variable in the operator form is restricted to occur only (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  33. Erik Palmgren (1991). A Construction of Type: Type in Martin-Löf's Partial Type Theory with One Universe. Journal of Symbolic Logic 56 (3):1012-1015.
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  34. Erik Palmgren & Viggo Stoltenberg-Hansen (1990). Domain Interpretations of Martin-Löf's Partial Type Theory. Annals of Pure and Applied Logic 48 (2):135-196.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation