43 found
Order:
  1.  47
    Type theories, toposes and constructive set theory: predicative aspects of AST.Ieke Moerdijk & Erik Palmgren - 2002 - 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 (6 more)  
     
    Export citation  
     
    Bookmark   25 citations  
  2.  64
    Wellfounded trees in categories.Ieke Moerdijk & Erik Palmgren - 2000 - 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 (7 more)  
     
    Export citation  
     
    Bookmark   23 citations  
  3. Developments in constructive nonstandard analysis.Erik Palmgren - 1998 - 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 (8 more)  
     
    Export citation  
     
    Bookmark   15 citations  
  4.  71
    Minimal models of Heyting arithmetic.Ieke Moerdijk & Erik Palmgren - 1997 - Journal of Symbolic Logic 62 (4):1448-1460.
    In this paper, we give a constructive nonstandard model of intuitionistic arithmetic (Heyting arithmetic). We present two axiomatisations of the model: one finitary and one infinitary variant. Using the model these axiomatisations are proven to be conservative over ordinary intuitionistic arithmetic. The definition of the model along with the proofs of its properties may be carried out within a constructive and predicative metatheory (such as Martin-Löf's type theory). This paper gives an illustration of the use of sheaf semantics to obtain (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   15 citations  
  5.  46
    Constructivist and structuralist foundations: Bishop’s and Lawvere’s theories of sets.Erik Palmgren - 2012 - Annals of Pure and Applied Logic 163 (10):1384-1399.
  6.  50
    Constructive Sheaf Semantics.Erik Palmgren - 1997 - 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 (3 more)  
     
    Export citation  
     
    Bookmark   12 citations  
  7.  57
    Inaccessibility in constructive set theory and type theory.Michael Rathjen, Edward R. Griffor & Erik Palmgren - 1998 - 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 (5 more)  
     
    Export citation  
     
    Bookmark   10 citations  
  8.  33
    Type-theoretic interpretation of iterated, strictly positive inductive definitions.Erik Palmgren - 1992 - 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)  
     
    Export citation  
     
    Bookmark   9 citations  
  9.  31
    Maximal and partial points in formal spaces.Erik Palmgren - 2006 - Annals of Pure and Applied Logic 137 (1-3):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 (6 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  10.  24
    Domain interpretations of martin-löf’s partial type theory.Erik Palmgren & Viggo Stoltenberg-Hansen - 1990 - Annals of Pure and Applied Logic 48 (2):135-196.
  11.  59
    Intuitionistic choice and classical logic.Thierry Coquand & Erik Palmgren - 2000 - 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 (4 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  12.  32
    A constructive approach to nonstandard analysis.Erik Palmgren - 1995 - 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 (5 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  13.  38
    Quotient topologies in constructive set theory and type theory.Hajime Ishihara & Erik Palmgren - 2006 - 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 (4 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  14. Proof-relevance of families of setoids and identity in type theory.Erik Palmgren - 2012 - 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 (5 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  15.  23
    An Effective Conservation Result for Nonstandard Arithmetic.Erik Palmgren - 2000 - Mathematical Logic Quarterly 46 (1):17-24.
    We prove that a nonstandard extension of arithmetic is effectively conservative over Peano arithmetic by using an internal version of a definable ultrapower. By the same method we show that a certain extension of the nonstandard theory with a saturation principle has the same proof-theoretic strength as second order arithmetic, where comprehension is restricted to arithmetical formulas.
    Direct download  
     
    Export citation  
     
    Bookmark   5 citations  
  16.  18
    An Intuitionistic Axiomatisation of Real Closed Fields.Erik Palmgren - 2002 - 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 (2 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  17.  25
    A sheaf-theoretic foundation for nonstandard analysis.Erik Palmgren - 1997 - 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 (4 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  18.  77
    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 (5 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  19.  23
    Regular universes and formal spaces.Erik Palmgren - 2006 - Annals of Pure and Applied Logic 137 (1-3):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 (5 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  20.  15
    Formal continuity implies uniform continuity near compact images on metric spaces.Erik Palmgren - 2014 - Mathematical Logic Quarterly 60 (1-2):66-69.
    The localic completion of a metric space induces a canonical notion of continuous map between metric spaces. It is shown that these maps are continuous in the sense of Bishop constructive mathematics, i.e., uniformly continuous near every compact image.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  21.  37
    Partial Horn logic and cartesian categories.Erik Palmgren & Steven J. Vickers - 2007 - Annals of Pure and Applied Logic 145 (3):314-353.
  22.  35
    A constructive examination of a Russell-style ramified type theory.Erik Palmgren - 2018 - Bulletin of Symbolic Logic 24 (1):90-106.
    In this article we examine the natural interpretation of a ramified type hierarchy into Martin-Löf type theory with an infinite sequence of universes. It is shown that under this predicative interpretation some useful special cases of Russell’s reducibility axiom are valid, namely functional reducibility. This is sufficient to make the type hierarchy usable for development of constructive mathematical analysis in the style of Bishop. We present a ramified type theory suitable for this purpose. One may regard the results of this (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  23.  28
    Constructive completions of ordered sets, groups and fields.Erik Palmgren - 2005 - 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 (4 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  24.  41
    Double sequences, almost Cauchyness and BD-N.Josef Berger, Douglas Bridges & Erik Palmgren - 2012 - Logic Journal of the IGPL 20 (1):349-354.
    It is shown that, relative to Bishop-style constructive mathematics, the boundedness principle BD-N is equivalent both to a general result about the convergence of double sequences and to a particular one about Cauchyness in a semi-metric space.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  25.  54
    A predicative completion of a uniform space.Josef Berger, Hajime Ishihara, Erik Palmgren & Peter Schuster - 2012 - Annals of Pure and Applied Logic 163 (8):975-980.
  26.  52
    Metric Boolean algebras and constructive measure theory.Thierry Coquand & Erik Palmgren - 2002 - 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 (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  27.  30
    Metric complements of overt closed sets.Thierry Coquand, Erik Palmgren & Bas Spitters - 2011 - 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 (2 more)  
     
    Export citation  
     
    Bookmark  
  28.  28
    A generalized cut characterization of the fullness axiom in CZF.Laura Crosilla, Erik Palmgren & Peter Schuster - 2013 - Logic Journal of the IGPL 21 (1):63-76.
    In the present note, we study a generalization of Dedekind cuts in the context of constructive Zermelo–Fraenkel set theory CZF. For this purpose, we single out an equivalent of CZF's axiom of fullness and show that it is sufficient to derive that the Dedekind cuts in this generalized sense form a set. We also discuss the instance of this equivalent of fullness that is tantamount to the assertion that the class of Dedekind cuts in the rational numbers, in the customary (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  29.  26
    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 (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  30.  38
    Exact completion and constructive theories of sets.Jacopo Emmenegger & Erik Palmgren - 2020 - Journal of Symbolic Logic 85 (2):563-584.
    In the present paper we use the theory of exact completions to study categorical properties of small setoids in Martin-Löf type theory and, more generally, of models of the Constructive Elementary Theory of the Category of Sets, in terms of properties of their subcategories of choice objects. Because of these intended applications, we deal with categories that lack equalisers and just have weak ones, but whose objects can be regarded as collections of global elements. In this context, we study the (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  31. 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 & B. Göran Sundholm - 2012 - 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 (ZFC). This framework is, however, laden with philosophical difficulties. One important alternative foundational programme that is actively (...)
     
    Export citation  
     
    Bookmark  
  32.  84
    Introduction: The philosophy of logical consequence and inference.Sten Lindström, Erik Palmgren & Dag Westerståhl - 2012 - Synthese 187 (3):817-820.
  33. Introduction: The three foundational programmes.Sten Lindström & Erik Palmgren - 2008 - In Sten Lindstr©œm, Erik Palmgren, Krister Segerberg & Viggo Stoltenberg-Hansen (eds.), logicism, intuitionism, and formalism - What has become of them? Berlin, Germany: Springer.
  34. logicism, intuitionism, and formalism - What has become of them?Sten Lindstr©œm, Erik Palmgren, Krister Segerberg & Viggo Stoltenberg-Hansen (eds.) - 2008 - Berlin, Germany: Springer.
    The period in the foundations of mathematics that started in 1879 with the publication of Frege's Begriffsschrift and ended in 1931 with Gödel's Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I can reasonably be called the classical period. It saw the development of three major foundational programmes: the logicism of Frege, Russell and Whitehead, the intuitionism of Brouwer, and Hilbert's formalist and proof-theoretic programme. In this period, there were also lively exchanges between the various schools culminating in (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  35.  35
    Hyperfinite type structures.Dag Normann, Erik Palmgren & Viggo Stoltenberg-Hansen - 1999 - Journal of Symbolic Logic 64 (3):1216-1242.
  36.  26
    A Construction of Type: Type in Martin-Lof's Partial Type Theory with One Universe.Erik Palmgren - 1991 - Journal of Symbolic Logic 56 (3):1012-1015.
  37.  35
    A logical presentation of the continuous functionals.Erik Palmgren & Viggo Stoltenberg-Hansen - 1997 - Journal of Symbolic Logic 62 (3):1021-1034.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark  
  38.  63
    (1 other version)A note on mathematics of infinity.Erik Palmgren - 1993 - Journal of Symbolic Logic 58 (4):1195-1200.
  39.  16
    Constructions of categories of setoids from proof-irrelevant families.Erik Palmgren - 2017 - Archive for Mathematical Logic 56 (1-2):51-66.
    When formalizing mathematics in constructive type theories, or more practically in proof assistants such as Coq or Agda, one is often using setoids. In this note we consider two categories of setoids with equality on objects and show, within intensional Martin-Löf type theory, that they are isomorphic. Both categories are constructed from a fixed proof-irrelevant family F of setoids. The objects of the categories form the index setoid I of the family, whereas the definition of arrows differs. The first category (...)
    No categories
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  40.  33
    Categories with families and first-order logic with dependent sorts.Erik Palmgren - 2019 - Annals of Pure and Applied Logic 170 (12):102715.
    First-order logic with dependent sorts, such as Makkai's first-order logic with dependent sorts (FOLDS), or Aczel's and Belo's dependently typed (intuitionistic) first-order logic (DFOL), may be regarded as logic enriched dependent type theories. Categories with families (cwfs) is an established semantical structure for dependent type theories, such as Martin-Löf type theory. We introduce in this article a notion of hyperdoctrine over a cwf, and show how FOLDS and DFOL fit in this semantical framework. A soundness and completeness theorem is proved (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  41.  28
    Resolution of the uniform lower bound problem in constructive analysis.Erik Palmgren - 2008 - 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  
     
    Export citation  
     
    Bookmark   1 citation  
  42.  41
    The Friedman‐Translation for Martin‐Löf's Type Theory.Erik Palmgren - 1995 - 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  
     
    Export citation  
     
    Bookmark   1 citation  
  43.  20
    (1 other version)Review: Wilfried Buchholz, An Intuitionistic Fixed Point Theory. [REVIEW]Erik Palmgren - 2001 - Bulletin of Symbolic Logic 7 (3):391-392.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark