In this book the authors reconcile two different viewpoints of the foundations of mathematics, namely mathematical logic and category theory. In Part I, they show that typed lambda-calculi, a formulation of higher order logic, and cartesian closed categories are essentially the same. In Part II, it is demonstrated that another formulation of higher order logic is closely related to topos theory. Part III is devoted to recursive functions. Numerous applications of the close relationship between traditional logic and the algebraic language (...) of category theory are given. The authors have included an introduction to category theory and develop the necessary logic as required, making the book essentially self-contained. Detailed historical references are provided throughout, and each section concludes with a set of exercises. Thus it is well-suited for graduate courses and research in mathematics and logic. Researchers in theoretical computer science, artificial intelligence and mathematical linguistics will also find this an accessible introduction to a subject of increasing application to these disciplines. (shrink)

In this paper we consider the relations existing between four deductive systems that have been called categorial grammars and have relevant connections with linguistic investigations: the syntactic calculus, bilinear logic, compact bilinear logic and Curry''s semantic calculus.

This article was written jointly by a philosopher and a mathematician. It has two aims: to acquaint mathematicians with some of the philosophical questions at the foundations of their subject and to familiarize philosophers with some of the answers to these questions which have recently been obtained by mathematicians. In particular, we argue that, if these recent findings are borne in mind, four different basic philosophical positions, logicism, formalism, platonism and intuitionism, if stated with some moderation, are in fact reconcilable, (...) although with some reservations in the case of logicism, provided one adopts a nominalistic interpretation of Plato's ideal objects. This eclectic view has been asserted by Lambek and Scott (LS 1986) on fairly technical grounds, but the present argument is meant to be accessible to a wider audience and to provide some new insights. (shrink)

One way of coping with agreement of features in French is to perform two parallel computations, one in the free pregroup of syntactic types, the other in that of feature types. Technically speaking, this amounts to working in the direct product of two free pregroups.

Grammar can be formulated as a kind of substructural propositional logic. In support of this claim, we survey bare Gentzen style deductive systems and two kinds of non-commutative linear logic: intuitionistic and compact bilinear logic. We also glance at their categorical refinements.

We study the monoid of primitive recursive functions and investigate a onestep construction of a kind of exact completion, which resembles that of the familiar category of modest sets, except that the partial equivalence relations which serve as objects are recursively enumerable. As usual, these constructions involve the splitting of symmetric idempotents.