Switch to: References

Citations of:

Eta-rules in Martin-löf type theory

Ansten Klev

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

Add citations

You must login to add citations.

The purely iterative conception of set.Ansten Klev - 2024 - Philosophia Mathematica 32 (3):358-378.details According to the iterative conception of set, sets are formed in stages. According to the purely iterative conception of set, sets are formed by iterated application of a set-of operation. The cumulative hierarchy is a mathematical realization of the iterative conception of set. A mathematical realization of the purely iterative conception can be found in Peter Aczel’s type-theoretic model of constructive set theory. I will explain Aczel’s model construction in a way that presupposes no previous familiarity with the theories on (...) which it is based. (shrink) Download Export citation Bookmark
Spiritus Asper versus Lambda: On the Nature of Functional Abstraction.Ansten Klev - 2023 - Notre Dame Journal of Formal Logic 64 (2):205-223.details The spiritus asper as used by Frege in a letter to Russell from 1904 bears resemblance to Church’s lambda. It is natural to ask how they relate to each other. An alternative approach to functional abstraction developed by Per Martin-Löf some thirty years ago allows us to describe the relationship precisely. Frege’s spiritus asper provides a way of restructuring a unary function name in Frege’s sense such that the argument place indicator occurs all the way to the right. Martin-Löf’s alternative (...) Download Export citation Bookmark 1 citation
Analyticity and Syntheticity in Type Theory Revisited.Bruno Bentzen - forthcoming - Review of Symbolic Logic.details I discuss problems with Martin-Löf's distinction between analytic and synthetic judgments in constructive type theory and propose a revision of his views. I maintain that a judgment is analytic when its correctness follows exclusively from the evaluation of the expressions occurring in it. I argue that Martin-Löf's claim that all judgments of the forms a : A and a = b : A are analytic is unfounded. As I shall show, when A evaluates to a dependent function type (x : (...) Download Export citation Bookmark
Identity in Martin‐Löf type theory.Ansten Klev - 2021 - Philosophy Compass 17 (2):e12805.details The logic of identity contains riches not seen through the coarse lens of predicate logic. This is one of several lessons to draw from the subtle treatment of identity in Martin‐Löf type theory, to which the reader will be introduced in this article. After a brief general introduction we shall mainly be concerned with the distinction between identity propositions and identity judgements. These differ from each other both in logical form and in logical strength. Along the way, connections to philosophical (...) Download Export citation Bookmark 3 citations

1