Advanced

Identity and intensionality in Univalent Foundations and philosophy

Angere, Staffan LU (2017) In Synthese p.1-41
Abstract

The Univalent Foundations project constitutes what is arguably the most serious challenge to set-theoretic foundations of mathematics since intuitionism. Like intuitionism, it differs both in its philosophical motivations and its mathematical-logical apparatus. In this paper we will focus on one such difference: Univalent Foundations’ reliance on an intensional rather than extensional logic, through its use of intensional Martin-Löf type theory. To this, UF adds what may be regarded as certain extensionality principles, although it is not immediately clear how these principles are to be interpreted philosophically. In fact, this framework gives an interesting example of a kind of border case between intensional and extensional... (More)

The Univalent Foundations project constitutes what is arguably the most serious challenge to set-theoretic foundations of mathematics since intuitionism. Like intuitionism, it differs both in its philosophical motivations and its mathematical-logical apparatus. In this paper we will focus on one such difference: Univalent Foundations’ reliance on an intensional rather than extensional logic, through its use of intensional Martin-Löf type theory. To this, UF adds what may be regarded as certain extensionality principles, although it is not immediately clear how these principles are to be interpreted philosophically. In fact, this framework gives an interesting example of a kind of border case between intensional and extensional mathematics. Our main purpose will be the philosophical investigation of this system, and the relation of the concepts of intensionality it satisfies to more traditional philosophical or logical concepts such as those of Carnap and Quine.

(Less)
Please use this url to cite or link to this publication:
author
organization
publishing date
type
Contribution to journal
publication status
epub
subject
keywords
Homotopy type theory, Identity, Intensionality, Univalent Foundations
in
Synthese
pages
41 pages
publisher
Springer
external identifiers
  • scopus:85010762654
ISSN
0039-7857
DOI
10.1007/s11229-016-1301-z
language
English
LU publication?
yes
id
f865efdc-b173-42d1-9cf0-c8e23c07ff7d
date added to LUP
2017-02-14 14:13:04
date last changed
2017-02-14 14:13:04
@article{f865efdc-b173-42d1-9cf0-c8e23c07ff7d,
  abstract     = {<p>The Univalent Foundations project constitutes what is arguably the most serious challenge to set-theoretic foundations of mathematics since intuitionism. Like intuitionism, it differs both in its philosophical motivations and its mathematical-logical apparatus. In this paper we will focus on one such difference: Univalent Foundations’ reliance on an intensional rather than extensional logic, through its use of intensional Martin-Löf type theory. To this, UF adds what may be regarded as certain extensionality principles, although it is not immediately clear how these principles are to be interpreted philosophically. In fact, this framework gives an interesting example of a kind of border case between intensional and extensional mathematics. Our main purpose will be the philosophical investigation of this system, and the relation of the concepts of intensionality it satisfies to more traditional philosophical or logical concepts such as those of Carnap and Quine.</p>},
  author       = {Angere, Staffan},
  issn         = {0039-7857},
  keyword      = {Homotopy type theory,Identity,Intensionality,Univalent Foundations},
  language     = {eng},
  month        = {01},
  pages        = {1--41},
  publisher    = {Springer},
  series       = {Synthese},
  title        = {Identity and intensionality in Univalent Foundations and philosophy},
  url          = {http://dx.doi.org/10.1007/s11229-016-1301-z},
  year         = {2017},
}