Number of the records: 1
Identity in Martin-Löf type theory
- 1.0553397 - FLÚ 2023 RIV GB eng J - Journal Article
Klev, Ansten
Identity in Martin-Löf type theory.
Philosophy Compass. Roč. 17, č. 2 (2022), č. článku e12805. E-ISSN 1747-9991
R&D Projects: GA ČR(CZ) GJ17-18344Y
Grant - others:AV ČR(CZ) LQ300092101
Program: Prémie Lumina quaeruntur
Institutional support: RVO:67985955
Keywords : normalization * perspective * truth * proof
OECD category: Philosophy, History and Philosophy of science and technology
Impact factor: 1.8, year: 2022
Method of publishing: Limited access
https://doi.org/10.1111/phc3.12805
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.
Permanent Link: http://hdl.handle.net/11104/0331574
Number of the records: 1