×

The justification of identity elimination in Martin-Löf’s type theory. (English) Zbl 1428.03045

Summary: On the basis of Martin-Löf’s meaning explanations for his type theory a detailed justification is offered of the rule of identity elimination. Brief discussions are thereafter offered of how the univalence axiom fares with respect to these meaning explanations and of some recent work on identity in type theory by Ladyman and Presnell.

MSC:

03B38 Type theory
03A05 Philosophical and critical aspects of logic and foundations
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Boolos G (1971) The iterative conception of set. J Philos 68:215-232 · doi:10.2307/2025204
[2] Curry HB (1942) The inconsistency of certain formal logics. J Symb Log 7:115-117 · Zbl 0060.02209 · doi:10.2307/2269292
[3] Dybjer P (1994) Inductive families. Form Asp Comput 6:440-465 · Zbl 0808.03044 · doi:10.1007/BF01211308
[4] Garner R (2009) On the strength of dependent products in the type theory of Martin-Löf. Ann Pure Appl Log 160:1-12 · Zbl 1171.03004 · doi:10.1016/j.apal.2008.12.003
[5] Hofmann, M.; Streicher, T.; Sambin, G. (ed.); Smith, JM (ed.), The groupoid interpretation of type theory, 83-111 (1998), Oxford · Zbl 0930.03089
[6] Husserl E (1891) Philosophie der Arithmetik. C.E.M. Pfeffer, Halle · JFM 23.0058.01
[7] Ladyman J, Presnell S (2015) Identity in homotopy type theory, part I: the justification of path induction. Philos Math 23:386-406 · Zbl 1380.03027 · doi:10.1093/philmat/nkv014
[8] Ladyman J, Presnell S (2016) Does homotopy type theory provide a foundation for mathematics? Br J Philos Sci. doi:10.1093/bjps/axw006 · Zbl 1400.03012 · doi:10.1093/bjps/axw006
[9] Martin-Löf P (1971) Hauptsatz for the intuitionistic theory of iterated inductive definitions. In Fenstad JE (ed) Proceedings of the second Scandinavian logic symposium, pp 179-216. North-Holland, Amsterdam · Zbl 0231.02040
[10] Martin-Löf, P.; Rose, HE (ed.); Shepherdson, JC (ed.), An intuitionistic theory of types: predicative part, 73-118 (1975), Amsterdam · Zbl 0334.02016
[11] Martin-Löf, P.; Cohen, JL (ed.); Łoś, J. (ed.); etal., Constructive mathematics and computer programming, 153-175 (1982), Amsterdam · Zbl 0541.03034
[12] Martin-Löf P (1984) Intuitionistic type theory. Bibliopolis, Naples · Zbl 0571.03030
[13] Nordström B, Petersson K, Smith J (1990) Programming in Martin-Löf’s type theory. Oxford University Press, Oxford · Zbl 0744.03029
[14] Nordström, B.; Petersson, K.; Smith, JM; Abramsky, S. (ed.); Gabbay, D. (ed.); Maibaum, TSE (ed.), Martin-Löf’s type theory, 1-37 (2000), Oxford
[15] Prawitz D (1965) Natural deduction. Almqvist & Wiksell, Stockholm · Zbl 0173.00205
[16] Prawitz D (1971) Ideas and results in proof theory. In Fenstad JE (ed) Proceedings of the second Scandinavian logic symposium, North-Holland, Amsterdam, pp 235-307 · Zbl 0226.02031
[17] Prawitz, D.; Wansing, H. (ed.), A short scientific autobiography, 33-64 (2015), Dordrecht · Zbl 1429.01028
[18] Shoenfield, J.; Barwise, J. (ed.), The axioms of set theory, 321-344 (1977), Amsterdam · doi:10.1016/S0049-237X(08)71106-6
[19] The Univalent Foundations Program (2013) Homotopy type theory: Univalent foundations of mathematics. Institute for Advanced Study, Princeton. http://homotopytypetheory.org/book · Zbl 1298.03002
[20] Walsh P (2017) Categorical harmony and path induction. Rev Symb Log 10:301-321 · Zbl 1384.03093 · doi:10.1017/S1755020317000077
[21] Zermelo E (1930) Über Grenzzahlen und Mengenbereiche. Fundam Math 16:29-47 · JFM 56.0082.02 · doi:10.4064/fm-16-1-29-47
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.