Bruno Bentzen

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 function names in Grundgesetze into simple type-theoretic open terms rather than into closed terms of a function type. This interpretation offers a still unhistorical but more faithful type-theoretic approximation of Frege’s theory of levels and can be naturally extended to accommodate second-level functions. It is made possible by two key observations that Frege’s Roman markers behave essentially like open terms and that Frege lacks a clear criterion for distinguishing between Roman markers and function names.

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 these areas. It is an essential resource for researchers, practitioners, and students interested in the latest advancements in logic and its applications to artificial intelligence and law.

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 implication, conjunction, disjunction, and falsity given in terms of a Hilbert-style axiomatization. As far as we know, our implementation is the first verified Henkin-style proof of completeness for intuitionistic logic following Troelstra and van Dalen's method in the literature.

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 : B) → C, all judgments of these forms fail to be analytic and therefore end up as synthetic. Going beyond the scope of Martin-Löf's original distinction, I also argue that all hypothetical judgments are synthetic and show how the analytic-synthetic distinction reworked here is capable of accommodating judgments of the forms A type and A = B type as well. Finally, I consider and reject an alternative account of analyticity as decidability and assess Martin-Löf's position on the analytic grounding of synthetic judgments.

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 natural numbers and systems sketched in an appendix to Brouwer's Cambridge lectures, I observe that the only plausible way he can make some elementary arithmetic in his separable mathematics is by allowing for the same canonical number to be determined by multiple separable entities, resulting in an overabundant mathematical ontology.

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 the interpretation is unsustainable regardless: (1) it is hard to determine, without appealing to propositional intentions on pain of circularity, what intention a proof-object should be understood as a fulfillment of; (2) due to a difficult fulfillment dilemma, it is unclear, at best, what the object of an intention corresponding to a proposition is.

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 to elementary results such as function extensionality, the derivation of weak connections and path induction, the groupoid structure of types, and the Eckmman–Hilton duality.

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 connectives and necessity as the only primitive modal operator. The full source code is available online and has been typechecked with Lean 3.4.2.

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 theory of sense and reference in the logical framework of Grundgesetze, his doctrine of truth values, and views on sameness of sense as equipollence of assertions.

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 senses is provided. It is argued that providing a solution based on proofs is more satisfactory from the standpoint of constructive semantics.

"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 "substantial-concept" and "functional-concept". Cassirer possesses along with a "theory of symbolical forms" a "theory of culture". These theories are "theories of conceptual formation" and they are in charge of various case studies developed by Cassirer in “Substanzbegriff und Funktionsbegriff”. Chapter 2, now translated, is a reading of the historical development of the concept of number under the view of a general theory of the concept that he presents in the second chapter of the book “Zur Theorie der Begriffsbildung” (On the theory of the conceptual formation).

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 an extension of knowledge. Second, we study this higher-dimensional account of equality from a constructive (computational) standpoint and, based on these considerations, we offer a new perspective to the project proposed by Peter Aczel of developing conventions and notations for an informal style of doing mathematics in type theory. To that end, we adopt the cubical type theory of Angiuli, Favonia and Harper, a framework that can be seen as constructive refinement of the ideas of homotopy type theory.

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 is argued that, in Frege’s standards of reducing arithmetic to logic, his solution to the indeterminacy does not give rise to any sort of Caesar problem in the book.