The phenomenon of digital computation is explained (often differently) in computer science, computer engineering and more broadly in cognitive science. Although the semantics and implications of malfunctions have received attention in the philosophy of biology and philosophy of technology, errors in computational systems remain of interest only to computer science. Miscomputation has not gotten the philosophical attention it deserves. Our paper fills this gap by offering a taxonomy of miscomputations. This taxonomy is underpinned by a conceptual analysis of the design (...) and implementation of conventional computational systems at various levels of abstraction. It shows that ‘malfunction’ as it is typically used in the philosophy of artefacts only represents one type of miscomputation. (shrink)

We provide a full characterization of computational error states for information systems. The class of errors considered is general enough to include human rational processes, logical reasoning, scientific progress and data processing in some functional programming languages. The aim is to reach a full taxonomy of error states by analysing the recovery and processing of data. We conclude by presenting machine-readable checking and resolve algorithms.

This chapter investigates the computational consequences of a broadly Gricean view of language use as intentional activity. In this view, dialogue rests on coordinated reasoning about communicative intentions. The speaker produces each utterance by formulating a suitable communicative intention. The hearer understands it by recognizing the communicative intention behind it. When this coordination is successful, interlocutors succeed in considering the same intentions— that is, the same representations of utterance meaning—as the dialogue proceeds. In this paper, I emphasize that these intentions (...) can be formalized; we can provide abstract but systematic representations that spell out what a speaker is trying to do with an utterance. Such representations describe utterances simultaneously as the product of our knowledge of grammar and as actions chosen for a reason. In particular, they must characterize the speaker’s utterance in grammatical terms, provide the links to the context that the grammar requires, and so arrive at a contribution that the speaker aims to achieve. Because I have implemented this formalism, we can regard it as a possible analysis of conversational processes at the level of computational theory. Nevertheless, this analysis leaves open what the nature of the biological computation involved in inference to intentions is, and what regularities in language use support this computation. (shrink)

Various conceptual approaches to the notion of information can currently be traced in the literature in logic and formal epistemology. A main issue of disagreement is the attribution of truthfulness to informational data, the so called Veridicality Thesis (Floridi 2005). The notion of Epistemic Constructive Information (Primiero 2007) is one of those rejecting VT. The present paper develops a formal framework for ECI. It extends on the basic approach of Artemov’s logic of proofs (Artemov 1994), representing an epistemic logic based (...) on dependent justifications, where the definition of information relies on a strict distinction from factual truth. The definition obtained by comparison with a Normal Modal Logic translates a constructive logic for “becoming informed”: its distinction from the logic of “being informed”—which internalizes truthfulness—is essential to a general evaluation of information with respect to truth. The formal disentanglement of these two logics, and the description of the modal version of the former as a weaker embedding into the latter, allows for a proper understanding of the Veridicality Thesis with respect to epistemic states defined in terms of information. (shrink)

The new concept of lambda calculi with monotone inductive types is introduced byhelp of motivations drawn from Tarski's fixed-point theorem (in preorder theory) andinitial algebras and initial recursive algebras from category theory. They are intendedto serve as formalisms for studying iteration and primitive recursion ongeneral inductively given structures. Special accent is put on the behaviour ofthe rewrite rules motivated by the categorical approach, most notably on thequestion of strong normalization (i.e., the impossibility of an infinitesequence of successive rewrite steps). It (...) is shown that this key propertyhinges on the concrete formulation. The canonical system of monotone inductivetypes, where monotonicity is expressed by a monotonicity witness beinga term expressing monotonicity through its type, enjoys strong normalizationshown by an embedding into the traditional system of non-interleavingpositive inductive types which, however, has to be enriched by the parametricpolymorphism of system F. Restrictions to iteration on monotone inductive typesalready embed into system F alone, hence clearly displaying the differencebetween iteration and primitive recursion with respect to algorithms despitethe fact that, classically, recursion is only a concept derived from iteration. (shrink)

Glue has evolved significantly during the past decade. Although the recent move to type-theoretic notation was a step in the right direction, basing the current Glue system on System F (second-order λ-calculus) was an unfortunate choice. An extension to two sorts and ad hoc restrictions were necessary to avoid inappropriate composition of meanings. As a result, the current system is unnecessarily complicated. A first-order Glue system is hereby proposed as its replacement. This new system is not only simpler and more (...) elegant, as it captures the exact requirements for Glue-style compositionality without ad hoc improvisations, but it also turns out to be more powerful than the current two-sorted (pseudo-) second-order system. First-order Glue supports all existing Glue analyses as well as more elegant alternatives. It also supports new, more demanding analyses. (shrink)

Martin-Löf's constructive type theory forms the basis of this paper. His central notions of category and set, and their relations with Russell's type theories, are discussed. It is shown that addition of an axiom - treating the category of propositions as a set and thereby enabling higher order quantification - leads to inconsistency. This theorem is a variant of Girard's paradox, which is a translation into type theory of Mirimanoff's paradox (concerning the set of all well-founded sets). The occurrence of (...) the contradiction is explained in set theoretical terms. Crucial here is the way a proof-object of an existential proposition is understood. It is shown that also Russell's paradox can be translated into type theory. The type theory extended with the axiom mentioned above contains constructive higher order logic, but even if one only adds constructive second order logic to type theory the contradictions arise. (shrink)

A two-stage procedure is described which induces type-logical grammar lexicons from sentences annotated with skeletal terms of the simply typed lambda calculus. First, a generalized formulae-as-types correspondence is exploited to obtain all the type-logical proofs of the sample sentences from their lambda terms. The resulting lexicons are then optimally unified. The first stage constitutes the semantic bootstrapping (Pinker, Language Learnability and Language Development, Harvard University Press, 1984), while the unification procedure of Buszkowski and Penn represents a first attempt at structure-dependent (...) distributional learning of the syntactic and semantic categories. This effort extends earlier induction procedures (Buszkowski and Penn, 1990, Studia Logica 49, 431–454; Kanazawa, 1998, CSLI Publications and the European Association for Logic, Language and Information) for classical categorial grammar to at first the non-associative Lambek calculus, and then to a large class of type logics enriched by modal operators and structural rules. (shrink)

We describe a sequent calculus, based on work of Herbelin, of which the cut-free derivations are in 1-1 correspondence with the normal natural deduction proofs of intuitionistic logic. We present a simple proof of Herbelin's strong cut-elimination theorem for the calculus, using the recursive path ordering theorem of Dershowitz.

The main concern of this paper is the design of a noetherian and confluent normalization for LK 2. The method we present is powerful: since it allows us to recover as fragments formalisms as seemingly different as Girard's LC and Parigot's λμ, FD, delineates other viable systems as well, and gives means to extend the Krivine/Leivant paradigm of `programming-with-proofs' to classical logic ; it is painless: since we reduce strong normalization and confluence to the same properties for linear logic using (...) appropriate embeddings ; it is unifying: it organizes known solutions in a simple pattern that makes apparent the how and why of their making. A comparison of our method to that of embedding LK into LJ brings to the fore the latter's defects for these `deconstructive purposes'. (shrink)

In this paper we consider an intuitionistic variant of the modal logic S4 (which we call IS4). The novelty of this paper is that we place particular importance on the natural deduction formulation of IS4— our formulation has several important metatheoretic properties. In addition, we study models of IS4— not in the framework of Kirpke semantics, but in the more general framework of category theory. This allows not only a more abstract definition of a whole class of models but also (...) a means of modelling proofs as well as provability. (shrink)

Using the programming-language concept of continuations, we propose a new, multimodal analysis of quantification in Type Logical Grammar. Our approach provides a geometric view of in-situ quantification in terms of graphs, and motivates the limited use of empty antecedents in derivations. Just as continuations are the tool of choice for reasoning about evaluation order and side effects in programming languages, our system provides a principled, type-logical way to model evaluation order and side effects in natural language. We illustrate with an (...) improved account of quantificational binding, weak crossover, wh-questions, superiority, and polarity licensing. (shrink)

Logic has pride of place in mathematics and its 20th century offshoot, computer science. Modern symbolic logic was developed, in part, as a way to provide a formal framework for mathematics: Frege, Peano, Whitehead and Russell, as well as Hilbert developed systems of logic to formalize mathematics. These systems were meant to serve either as themselves foundational, or at least as formal analogs of mathematical reasoning amenable to mathematical study, e.g., in Hilbert’s consistency program. Similar efforts continue, but have been (...) expanded by the development of sophisticated methods to study the properties of such systems using proof and model theory. In parallel with this evolution of logical formalisms as tools for articulating mathematical theories (broadly speaking), much progress has been made in the quest for a mechanization of logical inference and the investigation of its theoretical limits, culminating recently in the development of new foundational frameworks for mathematics with sophisticated computer-assisted proof systems. In addition, logical formalisms developed by logicians in mathematical and philosophical contexts have proved immensely useful in describing theories and systems of interest to computer scientists, and to some degree, vice versa. Three examples of the influence of logic in computer science are automated reasoning, computer verification, and type systems for programming languages. (shrink)

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. (shrink)

This work addresses biological explanations and aims to provide a philosophical account which brings together logical-procedural and historical-processual aspects when considering molecular pathways. It is argued that, having molecular features as explananda, a particular non-classical logical language – Zsyntax – can be used to formally represent, in terms of logical theorems, types of molecular processes, and to grasp how we get from one molecular interaction to another, hence explaining why a given outcome occurs. Expressing types of molecular biology processes in (...) terms of the Zsyntax language allows us to represent causal interactions by taking into account their context-sensitivity, and amounts to partly reviving the spirit of the so-called received view of explanation – which aimed to capture scientific explanatory accounts in terms of their logical structure and their appealing to nomological relations. Such a partial revival is pursued by invoking here non-classical deductions and empirical generalisations, which are called to provide the epistemic norms to explain the behavior of molecular pathways. (shrink)

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 (...) debates concerning identity are noted. Some use of logical symbolism is inevitable in any serious discussion of type theory, but the emphasis here is on basic ideas rather than technicalities. (shrink)

Proof, Computation and Agency: Logic at the Crossroads provides an overview of modern logic and its relationship with other disciplines. As a highlight, several articles pursue an inspiring paradigm called 'social software', which studies patterns of social interaction using techniques from logic and computer science. The book also demonstrates how logic can join forces with game theory and social choice theory. A second main line is the logic-language-cognition connection, where the articles collected here bring several fresh perspectives. Finally, the book (...) takes up Indian logic and its connections with epistemology and the philosophy of science, showing how these topics run naturally into each other. (shrink)

A comprehensive survey of Martin-Löf's constructive type theory, considerable parts of which have only been presented by Martin-Löf in lecture form or as part of conference talks. Sommaruga surveys the prehistory of type theory and its highly complex development through eight different stages from 1970 to 1995. He also provides a systematic presentation of the latest version of the theory, as offered by Martin-Löf at Leiden University in Fall 1993. This presentation gives a fuller and updated account of the system. (...) Earlier, brief presentations took no account of the issues related to the type-theoretical approach to logic and the foundations of mathematics, while here they are accorded an entire part of the book. Readership: Comprehensive accounts of the history and philosophy of constructive type theory and a considerable amount of related material. Readers need a solid background in standard logic and a first, basic acquaintance with type theory. (shrink)

This collection of papers, celebrating the contributions of Swedish logician Dag Prawitz to Proof Theory, has been assembled from those presented at the Natural Deduction conference organized in Rio de Janeiro to honour his seminal research. Dag Prawitz’s work forms the basis of intuitionistic type theory and his inversion principle constitutes the foundation of most modern accounts of proof-theoretic semantics in Logic, Linguistics and Theoretical Computer Science. The range of contributions includes material on the extension of natural deduction with higher-order (...) rules, as opposed to higher-order connectives, and a paper discussing the application of natural deduction rules to dealing with equality in predicate calculus. The volume continues with a key chapter summarizing work on the extension of the Curry-Howard isomorphism, via methods of category theory that have been successfully applied to linear logic, as well as many other contributions from highly regarded authorities. With an illustrious group of contributors addressing a wealth of topics and applications, this volume is a valuable addition to the libraries of academics in the multiple disciplines whose development has been given added scope by the methodologies supplied by natural deduction. The volume is representative of the rich and varied directions that Prawitz work has inspired in the area of natural deduction. (shrink)

Ranging from Alan Turing’s seminal 1936 paper to the latest work on Kolmogorov complexity and linear logic, this comprehensive new work clarifies the relationship between computability on the one hand and constructivity on the other. The authors argue that even though constructivists have largely shed Brouwer’s solipsistic attitude to logic, there remain points of disagreement to this day. Focusing on the growing pains computability experienced as it was forced to address the demands of rapidly expanding applications, the content maps the (...) developments following Turing’s ground-breaking linkage of computation and the machine, the resulting birth of complexity theory, the innovations of Kolmogorov complexity and resolving the dissonances between proof theoretical semantics and canonical proof feasibility. Finally, it explores one of the most fundamental questions concerning the interface between constructivity and computability: whether the theory of recursive functions is needed for a rigorous development of constructive mathematics. This volume contributes to the unity of science by overcoming disunities rather than offering an overarching framework. It posits that computability’s adoption of a classical, ontological point of view kept these imperatives separated. In studying the relationship between the two, it is a vital step forward in overcoming the disagreements and misunderstandings which stand in the way of a unifying view of logic. (shrink)

This book brings together philosophers, mathematicians and logicians to penetrate important problems in the philosophy and foundations of mathematics. In philosophy, one has been concerned with the opposition between constructivism and classical mathematics and the different ontological and epistemological views that are reflected in this opposition. The dominant foundational framework for current mathematics is classical logic and set theory with the axiom of choice. This framework is, however, laden with philosophical difficulties. One important alternative foundational programme that is actively pursued (...) today is predicativistic constructivism based on Martin-Löf type theory. Associated philosophical foundations are meaning theories in the tradition of Wittgenstein, Dummett, Prawitz and Martin-Löf. What is the relation between proof-theoretical semantics in the tradition of Gentzen, Prawitz, and Martin-Löf and Wittgensteinian or other accounts of meaning-as-use? What can proof-theoretical analyses tell us about the scope and limits of constructive and predicative mathematics? (shrink)

In a recent paper by Tranchini (Topoi, 2019), an introduction rule for the paradoxical proposition ρ∗ that can be simultaneously proven and disproven is discussed. This rule is formalized in Martin-Löf’s constructive type theory (CTT) and supplemented with an inferential explanation in the style of Brouwer-Heyting-Kolmogorov semantics. I will, however, argue that the provided formalization is problematic because what is paradoxical about ρ∗ from the viewpoint of CTT is not its provability, but whether it is a proposition at all.

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. (shrink)

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. (shrink)

This monograph proposes a new way of studying the different forms of correlational inference, known in the Islamic jurisprudence as qiyās. According to the authors’ view, qiyās represents an innovative and sophisticated form of dialectical reasoning that not only provides new epistemological insights into legal argumentation in general but also furnishes a fine-grained pattern for parallel reasoning which can be deployed in a wide range of problem-solving contexts and does not seem to reduce to the standard forms of analogical reasoning (...) studied in contemporary philosophy of science and argumentation theory. After an overview of the emergence of qiyās and of the work of al-Shīrāzī penned by Soufi Youcef, the authors discuss al-Shīrāzī’s classification of correlational inferences of the occasioning factor. The second part of the volume deliberates on the system of correlational inferences by indication and resemblance. The third part develops the main theoretical background of the authors’ work, namely, the dialogical approach to Martin-Löf's Constructive Type Theory. The authors present this in a general form and independently of adaptations deployed in parts I and II. Part III also includes an appendix on the relevant notions of Constructive Type Theory, which has been extracted from an overview written by Ansten Klev. The book concludes with some brief remarks on contemporary approaches to analogy in Common and Civil Law and also to parallel reasoning in general. (shrink)

Penelope Maddy has recently addressed the set-theoretic multiverse, and expressed reservations on its status and merits ([Maddy, 2017]). The purpose of the paper is to examine her concerns, by using the interpretative framework of set-theoretic naturalism. I first distinguish three main forms of 'multiversism', and then I proceed to analyse Maddy's concerns. Among other things, I take into account salient aspects of multiverse-related mathematics , in particular, research programmes in set theory for which the use of the multiverse seems to (...) be crucial, and show how one may provide responses to Maddy's concerns based on a careful analysis of 'multiverse practice'. (shrink)

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.

This monograph proposes a new way of implementing interaction in logic. It also provides an elementary introduction to Constructive Type Theory. The authors equally emphasize basic ideas and finer technical details. In addition, many worked out exercises and examples will help readers to better understand the concepts under discussion. One of the chief ideas animating this study is that the dialogical understanding of definitional equality and its execution provide both a simple and a direct way of implementing the CTT approach (...) within a game-theoretical conception of meaning. In addition, the importance of the play level over the strategy level is stressed, binding together the matter of execution with that of equality and the finitary perspective on games constituting meaning. According to this perspective the emergence of concepts are not only games of giving and asking for reasons, they are also games that include moves establishing how it is that the reasons brought forward accomplish their explicative task. Thus, immanent reasoning games are dialogical games of Why and How. (shrink)

The main objective of this PhD Thesis is to present a method of obtaining strong normalization via natural ordinal, which is applicable to natural deduction systems and typed lambda calculus. The method includes (a) the definition of a numerical assignment that associates each derivation (or lambda term) to a natural number and (b) the proof that this assignment decreases with reductions of maximal formulas (or redex). Besides, because the numerical assignment used coincide with the length of a specific sequence of (...) reduction - the worst reduction sequence - it is the lowest upper bound on the length of reduction sequences. The main commitment of the introduced method is that it is constructive and elementary, produced only through analyzing structural and combinatorial properties of derivations and lambda terms, without appeal to any sophisticated mathematical tool. Together with the exposition of the method, it is presented a comparative study of some articles in the literature that also get strong normalization by means we can identify with the natural ordinal methods. Among them we highlight Howard[1968], which performs an ordinal analysis of Godel’s Dialectica interpretation for intuitionistic first order arithmetic. We reveal a fact about this article not noted by the author himself: a syntactic proof of strong normalization theorem for the system of typified lambda calculus λ⊃ is a consequence of its results. This would be the first strong normalization proof in the literature. (written in Portuguese). (shrink)

The investigations on higher-order type theories and on the related notion of parametric polymorphism constitute the technical counterpart of the old foundational problem of the circularity of second and higher-order logic. However, the epistemological significance of such investigations has not received much attention in the contemporary foundational debate.We discuss Girard’s normalization proof for second order type theory or System F and compare it with two faulty consistency arguments: the one given by Frege for the logical system of the Grundgesetze and (...) the one given by Martin-Löf for the intuitionistic type theory with a type of all types.The comparison suggests that the question of the circularity of second order logic cannot be reduced to Russell’s and Poincaré’s 1906 “vicious circle” diagnosis. Rather, it reveals a bunch of mathematical and logical ideas hidden behind the hazardous idea of impredicative quantification, constituting a vast domain for foundational research. (shrink)

We may try to explain proofs as chains of valid inference, but the concept of validity needed in such an explanation cannot be the traditional one. For an inference to be legitimate in a proof it must have sufficient epistemic power, so that the proof really justifies its final conclusion. However, the epistemic concepts used to account for this power are in their turn usually explained in terms of the concept of proof. To get out of this circle we may (...) consider an idea within intuitionism about what it is to justify the assertion of a proposition. It depends on Heyting’s view of the meaning of a proposition, but does not presuppose the concept of inference or of proof as chains of inferences. I discuss this idea and what is required in order to use it for an adequate notion of valid inference. (shrink)

Machine awareness is a disputed research topic, in some circles considered a crucial step in realising Artificial General Intelligence. Understanding what that is, under which conditions such feature could arise and how it can be controlled is still a matter of speculation. A more concrete object of theoretical analysis is algorithmic iteration for computational intelligence, intended as the theoretical and practical ability of algorithms to design other algorithms for actions aimed at solving well-specified tasks. We know this ability is already (...) shown by current AIs, and understanding its limits is an essential step in qualifying claims about machine awareness and Super-AI. We propose a formal translation of algorithmic iteration in a fragment of modal logic, formulate principles of transparency and faithfulness across human and machine intelligence, and consider the relevance to theoretical research on -AI as well as the practical import of our results. (shrink)

The Univalent Foundations project constitutes what is arguably the most serious challenge to set-theoretic foundations of mathematics since intuitionism. Like intuitionism, it differs both in its philosophical motivations and its mathematical-logical apparatus. In this paper we will focus on one such difference: Univalent Foundations’ reliance on an intensional rather than extensional logic, through its use of intensional Martin-Löf type theory. To this, UF adds what may be regarded as certain extensionality principles, although it is not immediately clear how these principles (...) are to be interpreted philosophically. In fact, this framework gives an interesting example of a kind of border case between intensional and extensional mathematics. Our main purpose will be the philosophical investigation of this system, and the relation of the concepts of intensionality it satisfies to more traditional philosophical or logical concepts such as those of Carnap and Quine. (shrink)

Homotopy Type Theory is a putative new foundation for mathematics grounded in constructive intensional type theory that offers an alternative to the foundations provided by ZFC set theory and category theory. This article explains and motivates an account of how to define, justify, and think about HoTT in a way that is self-contained, and argues that, so construed, it is a candidate for being an autonomous foundation for mathematics. We first consider various questions that a foundation for mathematics might be (...) expected to answer, and find that many of them are not answered by the standard formulation of HoTT as presented in the ‘HoTT Book’. More importantly, the presentation of HoTT given in the HoTT Book is not autonomous since it explicitly depends upon other fields of mathematics, in particular homotopy theory. We give an alternative presentation of HoTT that does not depend upon ideas from other parts of mathematics, and in particular makes no reference to homotopy theory, and argue that it is a candidate autonomous foundation for mathematics. Our elaboration of HoTT is based on a new interpretation of types as mathematical concepts, which accords with the intensional nature of the type theory. 1 Introduction2 What Is a Foundation for Mathematics?2.1 A characterization of a foundation for mathematics2.2 Autonomy3 The Basic Features of Homotopy Type Theory3.1 The rules3.2 The basic ways to construct types3.3 Types as propositions and propositions as types3.4 Identity3.5 The homotopy interpretation4 Autonomy of the Standard Presentation?5 The Interpretation of Tokens and Types5.1 Tokens as mathematical objects?5.2 Tokens and types as concepts6 Justifying the Elimination Rule for Identity7 The Foundations of Homotopy Type Theory without Homotopy7.1 Framework7.2 Semantics7.3 Metaphysics7.4 Epistemology7.5 Methodology8 Possible Objections to this Account8.1 A constructive foundation for mathematics?8.2 What are concepts?8.3 Isn’t this just Brouwerian intuitionism?8.4 Duplicated objects8.5 Intensionality and substitution salva veritate9 Conclusion9.1 Advantages of this foundation. (shrink)

The classical propositional logic is known to be sound and complete with respect to the set semantics that interprets connectives as set operations. The paper extends propositional language by a new binary modality that corresponds to partial recursive function type constructor under the above interpretation. The cases of deterministic and non-deterministic functions are considered and for both of them semantically complete modal logics are described and decidability of these logics is established.

A two-stage procedure is described which induces type-logical grammar lexicons from sentences annotated with skeletal terms of the simply typed lambda calculus. First, a generalized formulae-as-types correspondence is exploited to obtain all the type-logical proofs of the sample sentences from their lambda terms. The resulting lexicons are then optimally unified. The first stage constitutes the semantic bootstrapping (Pinker, Language Learnability and Language Development, Harvard University Press, 1984), while the unification procedure of Buszkowski and Penn represents a first attempt at structure-dependent (...) distributional learning of the syntactic and semantic categories. This effort extends earlier induction procedures (Buszkowski and Penn, 1990, Studia Logica 49, 431–454; Kanazawa, 1998, CSLI Publications and the European Association for Logic, Language and Information) for classical categorial grammar to at first the non-associative Lambek calculus, and then to a large class of type logics enriched by modal operators and structural rules. (shrink)

The aim of this paper is to argue that logic can play an important role in the “toolbox” of molecular biology. We show how biochemical pathways, i.e., transitions from a molecular aggregate to another molecular aggregate, can be viewed as deductive processes. In particular, our logical approach to molecular biology — developed in the form of a natural deduction system — is centered on the notion of Curry-Howard isomorphism, a cornerstone in nineteenth-century proof-theory.

This book sets out the foundations, methodology, and practice of a formal framework for the description of language. The approach embraces the trends of lexicalism and compositional semantics in computational linguistics, and theoretical linguistics more broadly, by developing categorial grammar into a powerful and extendable logic of signs. Taking Montague Grammar as its point of departure, the book explains how integration of methods from philosophy (logical semantics), computer science (type theory), linguistics (categorial grammar) and meta-mathematics (mathematical logic ) provides a (...) categorial foundation with coverage including intensionality, quantification, featural polymorphism, domains and constraints. For the first time, the book systematises categorial thinking into a unified program which is at once both logically secured, and a practical tool for pure lexical grammar development with type-theoretic semantics. It should be of interest to all those active in computational linguistics and formal grammar and is suitable for use at advanced undergraduate, postgraduate, and research levels. (shrink)

I define the notion of normality for deductions in a Gentzen system for the classical case; I prove the normalization theorem for this notion and I build two direct maps between normal Gentzen deductions and natural deductions in *-normal form, i.e., natural deductions in normal form that also satisfy other conditions. I give the proof of the '*-normalization theorem', i.e. I give a procedure for transforming a normal deduction of →Nc into a unique deduction in *-normal form.

We present a categorical/denotational semantics for the Lambek Syntactic Calculus , indeed for a λlD-typed version Curry-Howard isomorphic to it. The main novelty of our approach is an abstract noncommutative construction with right and left adjoints, called sequential product. It is defined through a hierarchical structure of categories reflecting the implicit permission to sequence expressions and the inductive construction of compound expressions. We claim that Lambek's noncommutative product corresponds to a noncommutative bi-endofunctor into a category, which encloses all categories of (...) such hierarchical structure. A soundness theorem for LSC is shown with respect to this semantical framework. (shrink)