Change search
Refine search result
1 - 17 of 17
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Rows per page
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sort
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
Select
The maximal number of hits you can export is 250. When you want to export more records please use the 'Create feeds' function.
  • 1. Awodey, Steve
    et al.
    Gambino, Nicola
    Palmgren, Erik
    Stockholm University, Faculty of Science, Department of Mathematics.
    Introduction - from type theory and homotopy theory to univalent foundations of mathematics2015In: Mathematical Structures in Computer Science, ISSN 0960-1295, E-ISSN 1469-8072, Vol. 25, no 5, p. 1005-1009Article in journal (Other academic)
    Abstract [en]

    We give an overview of the main ideas involved in the development of homotopy type theory and the univalent foundations of Mathematics programme. This serves as a background for the research papers published in the special issue.

  • 2. Berger, Josef
    et al.
    Bridges, Douglas
    Palmgren, Erik
    Stockholm University, Faculty of Science, Department of Mathematics.
    Double sequences, almost Cauchyness and BD-N2012In: Logic journal of the IGPL (Print), ISSN 1367-0751, E-ISSN 1368-9894, Vol. 20, no 1, p. 349-354Article in journal (Refereed)
    Abstract [en]

    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.

  • 3. Bridges, Douglas S.
    et al.
    Hendtlass, Matthew
    Stockholm University, Faculty of Science, Department of Mathematics.
    Palmgren, Erik
    Stockholm University, Faculty of Science, Department of Mathematics.
    A Constructive Examination of Rectifiability2016In: Journal of Logic and Analysis, ISSN 1759-9008, E-ISSN 1759-9008, Vol. 8, article id UNSP 4Article in journal (Refereed)
    Abstract [en]

    We present a Brouwerian example showing that the classical statement 'Every Lipschitz mapping f : [0; 1] -> [0; 1] has rectifiable graph' is essentially nonconstructive. We turn this Brouwerian example into an explicit recursive example of a Lipschitz function on [0; 1] that is not rectifiable. Then we deal with the connections, if any, between the properties of rectifiability and having a variation. We show that the former property implies the latter, but the statement 'Every continuous, real-valued function on [0; 1] that has a variation is rectifiable' is essentially nonconstructive.

  • 4. Bridges, Douglas S.
    et al.
    Palmgren, Erik
    Stockholm University, Faculty of Science, Department of Mathematics.
    Constructive Mathematics2013In: Stanford Encyclopedia of Philosophy, ISSN 1095-5054, E-ISSN 1095-5054Article in journal (Refereed)
  • 5.
    Crossilla, Laura
    et al.
    Leeds University.
    Palmgren, Erik
    Stockholm University, Faculty of Science, Department of Mathematics.
    Schuster, Peter
    Leeds University.
    A generalized cut characterization of the fullness axiom in CZF2013In: Logic journal of the IGPL (Print), ISSN 1367-0751, E-ISSN 1368-9894, Vol. 21, no 1, p. 63-76Article in journal (Refereed)
  • 6. Lindström, Sten
    et al.
    Palmgren, Erik
    Stockholm University, Faculty of Science, Department of Mathematics.
    Westerståhl, Dag
    Stockholm University, Faculty of Humanities, Department of Philosophy. University of Gothenburg, Sweden.
    Introduction: The philosophy of logical consequence and inference2012In: Synthese, ISSN 0039-7857, E-ISSN 1573-0964, Vol. 187, no 3, p. 157p. 817-820Article in journal (Other academic)
  • 7.
    Palmgren, Erik
    Stockholm University, Faculty of Science, Department of Mathematics.
    A Constructive Examination of a Russell-style Ramified Type Theory2017Manuscript (preprint) (Other academic)
    Abstract [en]

    In this paper 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 mathematics. We present a ramified type theory suitable for this purpose. One may regard the results of this paper as an alternative solution to the problems of Russell’s theory, which avoids impredicativity, but instead imposes constructive logic. The intuitionistic ramified type theory introduced here, also suggests that there is a natural associated notion of predicative elementary topos. 

  • 8.
    Palmgren, Erik
    Stockholm University, Faculty of Science, Department of Mathematics.
    A CONSTRUCTIVE EXAMINATION OF A RUSSELL-STYLE RAMIFIED TYPE THEORY2018In: Bulletin of Symbolic Logic, ISSN 1079-8986, E-ISSN 1943-5894, Vol. 24, no 1, p. 90-106Article in journal (Refereed)
    Abstract [en]

    In this article we examine the natural interpretation of a ramified type hierarchy into Martin-Lof 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 article as an alternative solution to the problem of the proliferation of levels of real numbers in Russell's theory, which avoids impredicativity, but instead imposes constructive logic. The intuitionistic ramified type theory introduced here also suggests that there is a natural associated notion of predicative elementary topos.

  • 9.
    Palmgren, Erik
    Stockholm University, Faculty of Science, Department of Mathematics.
    A note on Brouwer's weak continuity principle and the transfer principle in nonstandard analysis2012In: Journal of Logic and Analysis, ISSN 1759-9008, E-ISSN 1759-9008, Vol. 4, no 2, p. 1-7Article in journal (Refereed)
    Abstract [en]

    A wellknown model of nonstandard analysis is obtained by extending the structure of real numbers using an ultrapower construction. A constructive approach due to Schmieden and Laugwitz uses instead a reduced power construction modulo a cofinite filter, but has the drawback that the transfer principle is weak. In this paper it is shown that this principle can be strengthened by employing Brouwerian continuity axioms familiar from intuitionistic systems. We end by commenting on the relation between the transfer principle and Ishihara’s boundedness principle.

  • 10.
    Palmgren, Erik
    Stockholm University, Faculty of Science, Department of Mathematics.
    Categories with families, FOLDS and logic enriched type theory2016Manuscript (preprint) (Other academic)
    Abstract [en]

    Categories with families (cwfs) is an established semantical structure for dependent type theories, such as Martin-Lö type theory. Makkai's first-order logic with dependent sorts (FOLDS) is an example of a so-called logic enriched type theory. We introduce in this article a notion of hyperdoctrine over a cwf, and show how FOLDS and Aczel's and Belo's dependently typed (intuitionistic) first-order logic (DFOL) fit in this semantical framework. A soundness and completeness theorem is proved for such a logic. The semantics is functorial in the sense of Lawvere, and uses a dependent version of the Lindenbaum-Tarski algebra for a DFOL theory. Agreement with standard first-order semantics is established. Some applications of DFOL to constructive mathematics and categorical foundations are given. A key feature is a local propositions-as-types principle.

  • 11.
    Palmgren, Erik
    Stockholm University, Faculty of Science, Department of Mathematics.
    Constructions of categories of setoids from proof-irrelevant families2017In: Archive for mathematical logic, ISSN 0933-5846, E-ISSN 1432-0665, Vol. 56, no 1-2, p. 51-66Article in journal (Refereed)
    Abstract [en]

    When formalizing mathematics in constructive type theories, or more practically in proof assistants such as Coq or Agda, one is often using setoids (types with explicit equivalence relations). In this note we consider two categories of setoids with equality on objects and show, within intensional Martin-Lof 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 has for arrows triples where f is an extensional function. Two such arrows are identified if appropriate composition with transportation maps (given by F) makes them equal. In the second category the arrows are triples where R is a total functional relation between the subobjects of the setoid sum of the family. This category is simpler to use as the transportation maps disappear. Moreover we also show that the full image of a category along an E-functor into an E-category is a category.

  • 12.
    Palmgren, Erik
    Stockholm University, Faculty of Science, Department of Mathematics.
    Constructions of categories of setoids from proof-irrelevant families2017In: Archive for mathematical logic, ISSN 0933-5846, E-ISSN 1432-0665, Vol. 56, no 1-2, p. 51-66Article in journal (Refereed)
    Abstract [en]

    When formalizing mathematics in constructive type theories, or more practically in proof assistants such as Coq or Agda, one is often using setoids (types with explicit equivalence relations). 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 has for arrows triples (a,b,f:F(a)→F(b))" role="presentation">(a,b,f:F(a)→F(b)) where f is an extensional function. Two such arrows are identified if appropriate composition with transportation maps (given by F) makes them equal. In the second category the arrows are triples (a,b,R↪Σ(I,F)2)" role="presentation">(a,b,R↪Σ(I,F)2) where R is a total functional relation between the subobjects F(a),F(b)↪Σ(I,F)" role="presentation">F(a),F(b)↪Σ(I,F) of the setoid sum of the family. This category is simpler to use as the transportation maps disappear. Moreover we also show that the full image of a category along an E-functor into an E-category is a category.

  • 13.
    Palmgren, Erik
    Stockholm University, Faculty of Science, Department of Mathematics.
    Constructivist versus Structuralist Foundations2012In: Epistemology versus Ontology: Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf / [ed] Peter Dybjer, Sten Lindström, Erik Palmgren, Göran Sundholm, Springer Berlin/Heidelberg, 2012, p. 265-279Chapter in book (Refereed)
  • 14.
    Palmgren, Erik
    Stockholm University, Faculty of Science, Department of Mathematics.
    Formal continuity implies uniform continuity near compact images on metric spaces2014In: Mathematical logic quarterly, ISSN 0942-5616, E-ISSN 1521-3870, Vol. 60, no 1-2, p. 66-69Article in journal (Refereed)
    Abstract [en]

    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. 

  • 15.
    Palmgren, Erik
    Stockholm University, Faculty of Science, Department of Mathematics.
    Proof relevance of families of setoids and identity in type theory2012In: Archive for mathematical logic, ISSN 0933-5846, E-ISSN 1432-0665, Vol. 51, no 1-2, p. 35-47Article in journal (Refereed)
    Abstract [en]

    Families of types are fundamental objects in Martin-Lof 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 fibre representations of families. The ubiquitous role of proof-irrelevant families is discussed.

  • 16.
    Palmgren, Erik
    et al.
    Stockholm University, Faculty of Science, Department of Mathematics.
    Dybjer, Peter
    Intuitionistic Type Theory2016In: Stanford Encyclopedia of Philosophy, ISSN 1095-5054, E-ISSN 1095-5054, no Winter 2016 editionArticle in journal (Refereed)
  • 17.
    Palmgren, Erik
    et al.
    Stockholm University, Faculty of Science, Department of Mathematics.
    Wilander, Olov
    Stockholm University, Faculty of Science, Department of Mathematics.
    Constructing categories and setoids of setoids in type theory2014In: Logical Methods in Computer Science, ISSN 1860-5974, E-ISSN 1860-5974, Vol. 10, no 3, p. 25-Article in journal (Refereed)
    Abstract [en]

    In this paper we consider the problem of building rich categories of setoids, in standard intensional Martin-Lo ̈f type theory (MLTT), and in particular how to handle the problem of equality on objects in this context. Any (proof-irrelevant) family F of setoids over a setoid A gives rise to a category C(A,F) of setoids with objects A. We may regard the family F as a setoid of setoids, and a crucial issue in this article is to construct rich or large enough such families. Depending on closure conditions of F , the category C(A, F ) has corresponding categorical constructions. We exemplify this with finite limits. A very large family F may be obtained from Aczel’s model construction of CZF in type theory. It is proved that the category so obtained is isomorphic to the internal category of sets in this model. Set theory can thus establish (categorical) properties of C(A,F) which may be used in type theory. We also show that Aczel’s model construction may be extended to include the elements of any setoid as atoms or urelements. As a byproduct we obtain a natural extension of CZF, adding atoms. This extension, CZFU, is validated by the extended model. The main theorems of the paper have been checked in the proof assistant Coq which is based on MLTT. A possible application of this development is to integrate set-theoretic and type-theoretic reasoning in proof assistants. 

1 - 17 of 17
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf