Switch to: References

Add citations

You must login to add citations.
  1. On Different Ways of Being Equal.Bruno Bentzen - 2020 - Erkenntnis 87 (4):1809-1830.
    The aim of this paper is to present a constructive solution to Frege's puzzle (largely limited to the mathematical context) based on type theory. Two ways in which an equality statement may be said to have cognitive significance are distinguished. One concerns the mode of presentation of the equality, the other its mode of proof. Frege's distinction between sense and reference, which emphasizes the former aspect, cannot adequately explain the cognitive significance of equality statements unless a clear identity criterion for (...)
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • Analyticity and Syntheticity in Type Theory Revisited.Bruno Bentzen - forthcoming - Review of Symbolic Logic:1-27.
    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.
    Philosophy Compass, Volume 17, Issue 2, February 2022.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Spiritus Asper versus Lambda: On the Nature of Functional Abstraction.Ansten Klev - 2023 - Notre Dame Journal of Formal Logic 64 (2):205-223.
    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  
  • Identity in Martin‐Löf type theory.Ansten Klev - 2021 - Philosophy Compass 17 (2):e12805.
    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   1 citation