×

On the syntax of Martin-Löf’s type theories. (English) Zbl 0638.03056

The paper gives a precise syntactical presentation of the arithmetical fragment (without universes and W-operator for the formation of well- founded trees) of Martin-Löf’s type theories, both in an intensional and an extensional version. Some elementary proof-theoretic properties are established, such as normalization of terms, the equivalence between several versions, and the dropping of type-statement premises.
Reviewer: A.S.Troelstra

MSC:

03F35 Second- and higher-order arithmetic and fragments
03F50 Metamathematics of constructive systems
03F05 Cut-elimination and normal-form theorems

Software:

Automath; Nuprl
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Aczel, P. H.G.; Troelstra, A. S.; van Dalen, D., The type-theoretic interpretation of constructive set theory: choice principles, (The L.E.J. Brouwer Centenary Symposium (1982), North-Holland: North-Holland Amsterdam), 1-40
[2] Barendregt, H. P.; Rezus, A., Semantics for classical AUTOMATH and related systems, Inform. and Control, 59, 127-147 (1983) · Zbl 0564.68060
[3] Beeson, M. J., Foundations of Constructive Mathematics (1985), Springer: Springer Berlin · Zbl 0565.03028
[4] Constable, R. L.; Allen, S. F.; Bromley, H. M.; Cleveland, W. R.; Cremer, J. F.; Harper, R. W.; Howe, D. J.; Knoblock, T. B.; Mendler, N. P.; Panangaden, P.; Sasaki, J. T.; Smith, S. F., Implementing Mathematics with the Nuprl Proof Development System (1986), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ
[5] Läuchli, H., An abstract notion of realizability for which intuitionistic predicate calculus is complete, (Kino, A.; Myhill, J.; Vesley, R. E., Intuitionism and Proof Theory (1970), North-Holland: North-Holland Amsterdam), 227-234 · Zbl 0216.00501
[6] Martin-Löf, P., An intuitionistic theory of types, predicative part, (Rose, H. E.; Shepherdson, J. E., Logic Colloquium ’73 (1975), North-Holland: North-Holland Amsterdam), 73-118 · Zbl 0334.02016
[7] Martin-Löf, P., Constructive mathematics and computer programming, (Cohen, L. J.; Łos, J.; Pfeiffer, H.; Podewski, K. D., Logic, Methodology and Philosophy of Science VI (1982), North-Holland: North-Holland Amsterdam), 153-179, and Polish Scientific Publishers, Warsaw · Zbl 0552.03040
[8] Martin-Löf, P., Intuitionistic Type Theory (1984), Bibliopolis: Bibliopolis Naples
[9] Prawitz, D., Natural Deduction, a Proof-Theoretic Study (1965), Almquist and Wiksell: Almquist and Wiksell Stockholm · Zbl 0173.00205
[10] Rezus, A., Semantics of constructive type theory, (Rep. No. 70 (1985), Informatics Department, Faculty of Science, Nijmegen University: Informatics Department, Faculty of Science, Nijmegen University The Netherlands) · Zbl 0632.03047
[11] Troelstra, A. S., Mathematical Investigation of Intuitionistic Arithmetic and Analysis (1973), Springer: Springer Berlin · Zbl 0275.02025
[12] Troelstra, A. S., Definability of finite sum types in Martin-Löf’s type theories, Indag. Math., 45, 475-481 (1983) · Zbl 0532.03027
[13] Troelstra, A. S., Strong normalization for typed terms with surjective pairing, Notre Dame J. of Formal Logic, 27, 547-550 (1986) · Zbl 0624.03043
[14] van Benthem Jutting, L. S., Checking Landau’s “Grundlagen” in the AUTOMATH system, (Ph.D. Thesis (1973), Technical University Eindhoven). (Ph.D. Thesis (1973), Technical University Eindhoven), Math. Centre Tracts 83 (1973), Mathematish Centrum: Mathematish Centrum Amsterdam · Zbl 0402.68064
[15] van Daalen, D. T., The language theory of AUTOMATH, (Ph.D. Thesis (1980), Technical University Eindhoven) · Zbl 0422.68045
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.