On the strength of dependent products in the type theory of Martin-Lof
2009 (English)In: Annals of Pure and Applied Logic, ISSN 0168-0072, E-ISSN 1873-2461, Vol. 160, no 1, 1-12 p.Article in journal (Refereed) Published
One may formulate the dependent product types of Martin-Lof type theory either in terms of abstraction and application operators like those for the lambda-calculus; or in terms of introduction and elimination rules like those for the other constructors of type theory. It is known that the latter rules are at least as strong as the former: we show that they are in fact strictly stronger. We also show, in the presence of the identity types, that the elimination rule for dependent products - which is a "higher-order" inference rule ill the sense of Schroeder-Heister - can be reformulated in a first-order manner. Finally, we consider the principle of function extensionality in type theory, which asserts that two elements of a dependent product type which are pointwise propositionally equal, are themselves propositionally equal. We demonstrate that the usual formulation of this principle fails to verify a number of very natural propositional equalities; and suggest all alternative formulation which rectifies this deficiency. (C) 2009 Elsevier B.V. All rights reserved.
Place, publisher, year, edition, pages
2009. Vol. 160, no 1, 1-12 p.
Dependent type theory, Dependent products, Function extensionality
IdentifiersURN: urn:nbn:se:uu:diva-129025DOI: 10.1016/j.apal.2008.12.003ISI: 000266648600001OAI: oai:DiVA.org:uu-129025DiVA: diva2:337475