Halchin's question re Curry-Howard

[F W Lawvere <wlawvere@buffalo.edu>]

>> I have been reading up on the Curry-Howard isomorphism.
>> In the last chapter of Conceptual Mathematics, Lawvere
>> and Schanuel say that the logical connectives are
>> completely analogous to the categorical operations x,
>> map object and +. Is this an oblique reference to the
>> Curry-Howard isomorphism?

   At the 1963 Model Theory conference in Berkeley, I pointed out
that an interlocking system of adjoints occurring in set theory and
type theory has also as a very special example the one arising in
the logic of parts. In Eilenberg and Kelly's 1965 pioneering paper on
closed categories, part of my result was cited and it came to be known as
the statement that Heyting algebras are cartesian closed categories.
In my papers "Adjointness in Foundations"(submitted December 15th
1967), "Equality in Hyperdoctrines...", and "Diagonal Arguments...",
I tried to clarify these and related matters. I became aware at some point
that Haskell Curry in one of his books had informally pointed out earlier
the possible importance of this as an analogy. In the late 1960s, Bill
Howard, a student of Mac Lane, began circulating his results which were
finally published in 1980; Howard's paper could be described as containing
an oblique reference to the closed category theorems.

   The term "isomorphism" which has emerged in the literature is
rather misleading since the map in question is bijective at best at the
level of subjective presentations, rather than at the level of objective
algebras. That is to say, a symbolic presentation of a particular Heyting
algebra can always be construed in many ways as an image of a
presentation of a cartesian closed category, but there is the additional
draconian rule of inference which says that any two maps with a given
domain and codomain are equal. I tried to give a more accurate description
of this situation by referring to "an adjunction" rather than to an
isomorphism in my paper

 "Adjointness in and Among Bi-categories" Logic and Algebra, Lecture Notes
in Pure and Applied Mathematics, vol. 180, pp 181-189, edited by A. Ursini
and P. Agliano', Marcel Dekker, 1996.


   Bill Lawvere





************************************************************
F. William Lawvere
Mathematics Department, State University of New York
244 Mathematics Building, Buffalo, N.Y. 14260-2900 USA
Tel. 716-645-6284
HOMEPAGE:  http://www.acsu.buffalo.edu/~wlawvere
************************************************************