9 found
Order:
See also
Bruno Bentzen
Zhejiang University
  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 (...)
    Download  
     
    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.
    Download  
     
    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 (...)
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  4. 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 (...)
    Download  
     
    Export citation  
     
    Bookmark  
  5. 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 (...)
    Download  
     
    Export citation  
     
    Bookmark  
  6. 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 (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  7. 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 (...)
    Download  
     
    Export citation  
     
    Bookmark  
  8. Naive cubical type theory.Bruno Bentzen - 2022 - Mathematical Structures in Computer Science:1-27.
    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 (...)
    Download  
     
    Export citation  
     
    Bookmark  
  9. 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 (...)
    Download  
     
    Export citation  
     
    Bookmark