Identity in Martin-Löf type theory
Bibliographic Data
| ID | 4982258 |
|---|---|
| Authors | Ansten Klev (0000-0003-1091-284X, Institute of Philosophy of the Slovak Academy of Sciences, corresponding author) |
| Year | 2022 |
| Volume | 17 |
| Issue | 2 |
| Publication date | 2022-02-01 |
| Peer Reviewed | Yes |
| Open Access | Yes |
| Type | ARTICLE |
| Venue | Philosophy Compass (JOURNAL) |
| Journal identifiers | ISSN: 1747-9991 • E-ISSN: 1747-9991 |
| Publisher | Wiley (PUBLISHER • GB) |
| DOI | 10.1111/phc3.12805 |
| OpenAlex | W4200543038 |
| Language | EN |
| Citations received | 1 |
| References cited | 37 |
The logic of identity contains riches not seen through the coarse lens of predicate logic. This is one of several lessons to draw from the subtle treatment of identity in Martin-Löf type theory, to which the reader will be introduced in this article. After a brief general introduction we shall mainly be concerned with the distinction between identity propositions and identity judgements. These differ from each other both in logical form and in logical strength. Along the way, connections to philosophical debates concerning identity are noted. Some use of logical symbolism is inevitable in any serious discussion of type theory, but the emphasis here is on basic ideas rather than technicalities
Aesthetics · Epistemology · Linguistics · Logical analysis · Sociology · Type theory · Advanced Algebra and Logic · Computer Science · Logic, Reasoning, and Knowledge · Mathematics · Philosophy · Philosophy and Theoretical Science
| Unique citing works | 1 |
|---|---|
| Citations per year | 0,5 |
| Citation span | 2024 - 2024 (1) |
| Citation velocity | recent |
| Highly cited | No |
| Citation types | Neutral: 1 |