Identity in Martin-Löf type theory

0553397 - FLÚ 2023 RIV GB eng J - Článek v odborném periodiku
Klev, Ansten
Identity in Martin-Löf type theory.
Philosophy Compass. Roč. 17, č. 2 (2022), č. článku e12805. E-ISSN 1747-9991
Grant CEP: GA ČR(CZ) GJ17-18344Y
Grant ostatní: AV ČR(CZ) LQ300092101
Program: Prémie Lumina quaeruntur
Institucionální podpora: RVO:67985955
Klíčová slova: normalization * perspective * truth * proof
Obor OECD: Philosophy, History and Philosophy of science and technology
Impakt faktor: 1.8, rok: 2022
Způsob publikování: Omezený přístup
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.
Trvalý link: http://hdl.handle.net/11104/0331574