Mathematics – Logic
Scientific paper
2008-03-31
Annals of Pure and Applied Logic 160 (2009), no.1, pages 1--12
Mathematics
Logic
18 pages; v2: final journal version
Scientific paper
10.1016/j.apal.2008.12.003
One may formulate the dependent product types of Martin-L\"of 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 in 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 an alternative formulation which rectifies this deficiency.
No associations
LandOfFree
On the strength of dependent products in the type theory of Martin-Löf does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with On the strength of dependent products in the type theory of Martin-Löf, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and On the strength of dependent products in the type theory of Martin-Löf will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-197694