15 found
Order:
  1. Propositions as Intentions.Bruno Bentzen - 2023 - Husserl Studies 39 (2):143-160.
    I argue against the interpretation of propositions as intentions and proof-objects as fulfillments proposed by Heyting and defended by Tieszen and van Atten. The idea is already a frequent target of criticisms regarding the incompatibility of Brouwer’s and Husserl’s positions, mainly by Rosado Haddock and Hill. I raise a stronger objection in this paper. My claim is that even if we grant that the incompatibility can be properly dealt with, as van Atten believes it can, two fundamental issues indicate that (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  2. What Types Should Not Be.Bruno Bentzen - 2020 - Philosophia Mathematica 28 (1):60-76.
    In a series of papers Ladyman and Presnell raise an interesting challenge of providing a pre-mathematical justification for homotopy type theory. In response, they propose what they claim to be an informal semantics for homotopy type theory where types and terms are regarded as mathematical concepts. The aim of this paper is to raise some issues which need to be resolved for the successful development of their types-as-concepts interpretation.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  3. Sense, reference, and computation.Bruno Bentzen - 2020 - Perspectiva Filosófica 47 (2):179-203.
    In this paper, I revisit Frege's theory of sense and reference in the constructive setting of the meaning explanations of type theory, extending and sharpening a program–value analysis of sense and reference proposed by Martin-Löf building on previous work of Dummett. I propose a computational identity criterion for senses and argue that it validates what I see as the most plausible interpretation of Frege's equipollence principle for both sentences and singular terms. Before doing so, I examine Frege's implementation of his (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  4.  60
    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 (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  5.  43
    Brouwer's Intuition of Twoity and Constructions in Separable Mathematics.Bruno Bentzen - forthcoming - History and Philosophy of Logic.
    My first aim in this paper is to use time diagrams in the style of Brentano to analyze constructions in Brouwer's separable mathematics more precisely. I argue that constructions must involve not only pairing and projecting as basic operations guaranteed by the intuition of twoity, as sometimes assumed in the literature, but also a recalling operation. My second aim is to argue that Brouwer's views on the intuition of twoity and arithmetic lead to an ontological explosion. Redeveloping the constructions of (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  6. Frege’s Theory of Types.Bruno Bentzen - 2023 - Manuscrito 46 (4):2022-0063.
    It is often claimed that the theory of function levels proposed by Frege in Grundgesetze der Arithmetik anticipates the hierarchy of types that underlies Church’s simple theory of types. This claim roughly states that Frege presupposes a type of functions in the sense of simple type theory in the expository language of Grundgesetze. However, this view makes it hard to accommodate function names of two arguments and view functions as incomplete entities. I propose and defend an alternative interpretation of first-level (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  7. A Henkin-style completeness proof for the modal logic S5.Bruno Bentzen - 2021 - In Pietro Baroni, Christoph Benzmüller & Yì N. Wáng (eds.), Logic and Argumentation: Fourth International Conference, CLAR 2021, Hangzhou, China, October 20–22. Springer. pp. 459-467.
    This paper presents a recent formalization of a Henkin-style completeness proof for the propositional modal logic S5 using the Lean theorem prover. The proof formalized is close to that of Hughes and Cresswell, but the system, based on a different choice of axioms, is better described as a Mendelson system augmented with axiom schemes for K, T, S4, and B, and the necessitation rule as a rule of inference. The language has the false and implication as the only primitive logical (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  8. Verified completeness in Henkin-style for intuitionistic propositional logic.Huayu Guo, Dongheng Chen & Bruno Bentzen - 2023 - In Bruno Bentzen, Beishui Liao, Davide Liga, Reka Markovich, Bin Wei, Minghui Xiong & Tianwen Xu (eds.), Logics for AI and Law: Joint Proceedings of the Third International Workshop on Logics for New-Generation Artificial Intelligence and the International Workshop on Logic, AI and Law, September 8-9 and 11-12, 2023, Hangzhou. College Publications. pp. 36-48.
    This paper presents a formalization of the classical proof of completeness in Henkin-style developed by Troelstra and van Dalen for intuitionistic logic with respect to Kripke models. The completeness proof incorporates their insights in a fresh and elegant manner that is better suited for mechanization. We discuss details of our implementation in the Lean theorem prover with emphasis on the prime extension lemma and construction of the canonical model. Our implementation is restricted to a system of intuitionistic propositional logic with (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  9. Constructive mathematics and equality.Bruno Bentzen - 2018 - Dissertation, Sun Yat-Sen University
    The aim of the present thesis is twofold. First we propose a constructive solution to Frege's puzzle using an approach based on homotopy type theory, a newly proposed foundation of mathematics that possesses a higher-dimensional treatment of equality. We claim that, from the viewpoint of constructivism, Frege's solution is unable to explain the so-called ‘cognitive significance' of equality statements, since, as we shall argue, not only statements of the form 'a = b', but also 'a = a' may contribute to (...)
     
    Export citation  
     
    Bookmark   1 citation  
  10.  41
    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 : (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  11. Naive cubical type theory.Bruno Bentzen - 2021 - Mathematical Structures in Computer Science 31:1205–1231.
    This article proposes a way of doing type theory informally, assuming a cubical style of reasoning. It can thus be viewed as a first step toward a cubical alternative to the program of informalization of type theory carried out in the homotopy type theory book for dependent type theory augmented with axioms for univalence and higher inductive types. We adopt a cartesian cubical type theory proposed by Angiuli, Brunerie, Coquand, Favonia, Harper, and Licata as the implicit foundation, confining our presentation (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  12. Frege on Referentiality and Julius Caesar in Grundgesetze Section 10.Bruno Bentzen - 2019 - Notre Dame Journal of Formal Logic 60 (4):617-637.
    This paper aims to answer the question of whether or not Frege's solution limited to value-ranges and truth-values proposed to resolve the "problem of indeterminacy of reference" in section 10 of Grundgesetze is a violation of his principle of complete determination, which states that a predicate must be defined to apply for all objects in general. Closely related to this doubt is the common allegation that Frege was unable to solve a persistent version of the Caesar problem for value-ranges. It (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark  
  13. Logics for AI and Law: Joint Proceedings of the Third International Workshop on Logics for New-Generation Artificial Intelligence and the International Workshop on Logic, AI and Law, September 8-9 and 11-12, 2023, Hangzhou.Bruno Bentzen, Beishui Liao, Davide Liga, Reka Markovich, Bin Wei, Minghui Xiong & Tianwen Xu (eds.) - 2023 - College Publications.
    This comprehensive volume features the proceedings of the Third International Workshop on Logics for New-Generation Artificial Intelligence and the International Workshop on Logic, AI and Law, held in Hangzhou, China on September 8-9 and 11-12, 2023. The collection offers a diverse range of papers that explore the intersection of logic, artificial intelligence, and law. With contributions from some of the leading experts in the field, this volume provides insights into the latest research and developments in the applications of logic in (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  14.  12
    O conceito de número.Fernando Raul Neto & Bruno Bentzen - 2013 - Perspectiva Filosófica 2 (40):140-178.
    "The Concept of Number", by Ernst Cassirer, is the second chapter of his first systematic work, the "Substanzbegriff und Funktionsbegriff: Untersuchungen über die Grundfragen der Erkenntniskritik", originally published in German in 1910. The translation to English, in 1953, by Marie Collins Swabeyand William Curtis Swabey, under the title "Substance and Function and Einstein's Theory of Relativity", despite its importance for having widely disseminated the work, loses in its title the work's essence: the opposition between "concept-substance" and "concept-function", or rather, between (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  15.  52
    John MacFarlane, Philosophical Logic: A Contemporary Introduction, Routledge Contemporary Introductions to Philosophy, Routledge, New York, and London, 2021, xx + 238 pp. [REVIEW]Bruno Bentzen - 2023 - Bulletin of Symbolic Logic 29 (3):456-457.