There’s a few logicians, mathematicians and philosophers on here, so I’ll ask. I’ve searched on Google for an answer to this, but with no luck.
Philosophically, what is the significance of the Curry-Howard isomorphism, linking intuitionistic logic with simply type lambda-calculus? Doesn’t this imply something about logical monism—that is, that constructive logic is the “correct logic”, in some sense, and we should all be constructivists?
(Actually, I can see at least one counterargument: there’s no reason to believe that simple types are really anything special, and the logic that they induce via C-H is boring anyway. Also, there’s ways to recover a correspondence between typed lambda-calculi and classical logic, with the lambda-mu-calculus.)
But have any philosophers investigated this? Is C-H just a “happy coincidence”, or indicative of something deeper?
You might want to look at Lambek-Scott, Introduction to Higher Order Categorical Logic. There are many kinds of logic and they all correspond to some kind of standard categorical structure. For example, linear logic (there are actually many fragments of it that are called by that name) correspond to *-autonomous categories and there are Curry-Howard type correspondences for that. Classical logic corresponds to 2-valued Boolean toposes and, ZFC to the same with the added hypothesis that epimorphisms split.
I actually bought that book, but got distracted by something else after I started reading it. I’ll have to look at it again. Thanks. Although, my question was more along the lines of whether the correspondence between a simple model of computation and a logic has any philosophical significance. Aren’t all of your examples rather more complex, and in a sense, contrived, when considered against the lambda-calculus?
I know you know this, but just to be pedantic… reconstructing the cumulative hierarchy within an arbitrary such topos corresponds most directly only to ZFC with weakened Separation/Replacement (using only formulas with quantifiers ranging over domains which are sets, rather than over proper classes (such as that of all sets in the cumulative hierarchy)). Handling ZFC in full requires some further constraints on the nature of the topos.
[It’s also worth noting that any Boolean topos is at least “internally” 2-valued, and so would suffice for all the same purposes, at least from such an internal perspective]
Certainly, some philosophers have taken this tack (in particular, it seems to be a strain of thought among the Dummet-Prawitz school of proof-theoretic semantics), but it doesn’t seem ultimately tenable to me for many reasons, including most prominently the points made by Hari Seldon and you in your own counterargument: non-intuitionistic logics have Curry-Howard correspondences too, just with different classes of categories/notions of computation.
Just as there’s no One Correct Notion of computation, but rather different systems to be investigated for different purposes, so it is, I would say, with logic; the importance of the Curry-Howard correspondence should be to highlight this plenitude rather than to encourage blindness to it.
(Also, I’ve made that same “Curly Howard correspondence” joke to a friend before, who didn’t appreciate it. Long story short, we’re no longer friends… :))
Eh, perhaps instead of “notion of computation”, I should’ve used better wording for “variety of lambda calculus”. “function-definition system”, perhaps? This actually brings us rather close to making the observation of C-H in full generality almost trivial: that is, it seems to me the best statement of C-H isn’t, in itself, in anything particularly tied to the intuitionistic logic/simply typed lambda calculus/cartesian closed category triple; it’s in the fact that every logic can be interpreted as a kind of category and vice versa (objects as propositions, morphisms as deductions modulo some notion of proof-theoretic equivalence), and similarly every function-definition system can be interpreted as a kind of category and vice versa (morphisms as the functions of the system), and that this, of course, induces a way to see every logic as a function-definition system and vice versa. Of course, that this should happen to come out to relate the three above systems previously studied of their own accord was an exciting discovery, but perhaps this illustrates nothing other than that any interesting concept will eventually be studied from all three perspectives.
Incidentally, you raise the possible objection that these other classes of categories corresponding to other logics are rather complex in comparison to those for the simply-typed lambda calculus, but I wouldn’t say so. E.g., arbitrary (monoidal) closed categories [the Lambek calculus] could be argued to be an even simpler notion than specifically cartesian closed categories; these would correspond to a fragment of noncommutative logic, even more spartan than intuitionistic logic.
(Of course, my having been pedantic above, it’s only fair that I be called out on my own simplifications; I have of course been glib about the fact that the simply typed lambda calculus, propositional intuitionistic logic, and cartesian closed categories do not directly line up, in their usual formulations; they don’t all model the same connectives. Thus, sometimes I really mean “simply typed lambda calculus with tuples and tagged unions”, “cartesian closed categories with coproducts”, etc.)
Sorry, I have been away for a while and didn’t keep up with this. If I were forced to answer the question of the philosophical implications of all this, I would say, “None”. But then I have little interest in philosophy. Even less in philosophy of mathematics since the time I went to a series of talks on the subject and realized that these are claiming to study how I work and don’t have the foggiest notion of how I work. I do not, for example, spend any time worrying about applying the axioms of set theory. I use set theory naively, while conscience of the need to avoid certain constructions (e.g. the set of all sets, although there are set theories in even that is allowed, but then comprehension (is that the one?) has to be limited). They seem utterly ignorant of the roles of experimentation and intuition in this business.
Lambek once wrote a paper explaining how to resolve the differences between platonism, intuitionism, formalism,…, but I just checked and it is not on his ftp site (which seems to have only his more recent linguistics work). I glanced at the paper, but it didn’t interest my much. You could try writing to him asking to get a copy by mail. He doesn’t use email, so write him at McGill. (He doesn’t use computers, so someone else set up the ftp site.)
