Bulletin of Symbolic Logic 25 (3):333-359 (2019)

Ansten Klev
Czech Academy of Sciences
The eta rule for a set A says that an arbitrary element of A is judgementally identical to an element of constructor form. Eta rules are not part of what may be called canonical Martin-Löf type theory. They are, however, justified by the meaning explanations, and a higher-order eta rule is part of that type theory. The main aim of this paper is to clarify this somewhat puzzling situation. It will be argued that lower-order eta rules do not, whereas the higher-order eta rule does, accord with the understanding of judgemental identity as definitional identity. A subsidiary aim is to clarify precisely what an eta rule is. This will involve showing how such rules relate to various other notions of type theory, proof theory, and category theory.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1017/bsl.2019.21
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 54,740
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

A Natural Extension of Natural Deduction.Peter Schroeder-Heister - 1984 - Journal of Symbolic Logic 49 (4):1284-1300.
Intensional Interpretations of Functionals of Finite Type I.W. W. Tait - 1967 - Journal of Symbolic Logic 32 (2):198-212.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

The Friedman‐Translation for Martin‐Löf's Type Theory.Erik Palmgren - 1995 - Mathematical Logic Quarterly 41 (3):314-326.
Well-Ordering Proofs for Martin-Löf Type Theory.Anton Setzer - 1998 - Annals of Pure and Applied Logic 92 (2):113-159.
Reply to Martin on Type Crossings.Theodore Drange - 1969 - Philosophy and Phenomenological Research 30 (1):136-139.
Martin-Löf Complexes.S. Awodey & M. A. Warren - 2013 - Annals of Pure and Applied Logic 164 (10):928-956.
Stability and Paradox in Algorithmic Logic.Wayne Aitken & Jeffrey A. Barrett - 2007 - Journal of Philosophical Logic 36 (1):61-95.
Polynomial-Time Martin-Löf Type Theory.L. Pe Joseph - 1992 - Archive for Mathematical Logic 32 (2):137-150.
The Inconsistency of Higher Order Extensions of Martin-Löf's Type Theory.Bart Jacobs - 1989 - Journal of Philosophical Logic 18 (4):399 - 422.
EM + Ext_ + AC~I~N~T is Equivalent to AC~E~X~T.J. Carlstrom - 2004 - Mathematical Logic Quarterly 50 (3):236.


Added to PP index

Total views
15 ( #636,350 of 2,386,872 )

Recent downloads (6 months)
2 ( #366,616 of 2,386,872 )

How can I increase my downloads?


My notes