I’ve been reading Lectures on the Howard-Curry Isomorphism by Sørensen and Urzyczyn recently. I wanted to comment on one of the interesting things in it.

Briefly, the Howard-Curry isomorphism is an isomorphism between proofs and λ-terms. In particular, it is well developed and explored for intuitionistic logic and typed λ calculi. It makes good sense of the BHK interpretation of intuitionistic logic. The intuitionistic conditional A→ B is understood of a way of transforming a proof of A into a proof of B. The λ-abstraction of a term of type B yields a function that, when given a term of type A, results in a term of type B. There is a nice connection that can be made explicit between intuitionistic logic and computability.

I’m not sure if I’ve read anyone using this to argue for intuitionistic logic over classical logic explicitly. Something like this is motivating Martin-Löf, I think. Classical logic doesn’t have this nice correspondence. At least, this is what I had thought. One of the surprising things in this book is that it presents a developed correspondence between classical proofs and λ-terms that makes sense of the double negation elimination rule, which is rejected by intuitionistic logic.

Double negation elimination corresponds to what the book terms a control structure. I’m not entirely clear on what this is supposed to mean. It apparently is from programming language theory. It involves the addition to the lambda calculus of a bunch of “addresses” and an operator μ for binding them. It is a little opaque to me what these addresses are supposed to be. When thinking about them in terms of computers, which is their conceptual origin I expect, it makes some sense to think of them in terms of place in memory or some such. I’m not sure how one should think of them generally. (I’m not sure if this is the right way to think of them in this context either.) Anyway, these addresses, like the terms themselves, come with types and rules of application and abstraction. There are also rules given for the way the types of the addresses and the types of the terms interact that involve negations. To make this a little clearer, the rule for address abstraction is:
Γ, a:¬ σ |- M: ⊥, infer
Γ |- (μa: ¬ σ M): σ.
The rule for address application is:
Γ, a: ¬ σ |- M: σ, infer
Γ |- ([a]M): ⊥.
In the above, Γ is a set of terms, M is a term, and the things after the colons are the types of the terms. (Anyone know of a way to get the single turnstile in html?)

The upshot of this, I take it, is that we can make (constructive?) computational sense of classical logic, like intuitionistic, relevance, and linear logics. Not exactly like them, since the classical case requires the addition a second sort of thing, the addresses, in addition to the λ-terms and another operator besides. Assessing the philosophical worth of this depends on getting clear on what the addition of this second sort of thing amounts to. I can’t reach any conclusions on the basis of what is given in the book. If the addresses are innocuous, then it seems like one could use this to construct an argument against some of Dummett’s and Prawitz’s views about meaning. This would proceed along the lines that, despite Dummett’s and Prawitz’s arguments to the contrary, we can make sense of the double negation elimination rule in terms of this particular correspondence. I don’t have any more meat to put on that skeleton because I don’t have a good sense of the details of their arguments, just rough characterizations of their conclusions.

There is also a brief discussion Kolmogorov’s double negation embedding of classical logic into intuitionistic logic. This is cased out in computational terms. It’s proved that if a term is derivable in the λμ calculus then its translation is derivable in the λ-calculus. One would expect this result since the translation shows that for anything provable in classical logic, its translation is provable in intuitionistic logic. It’s filling in the arrows in the diagram.

One thing that seemed to be missing in this part of the book was a discussion of combinators. One can characterize intuitionistic logic in terms of combinators. A similar characterization can be done for relevance logic and linear logic. There wasn’t any such characterization given for classical logic. Why would this be? The combinators correspond to certain λ-terms. Classical logic requires moving beyond the λ-calculus to the λμ calculus. The combinators either can’t express what is going on with μ or such an expression hasn’t been found yet, I expect. (Would another sort of combinator be needed to do this?) [Edit: As Noam notes in the comments, I was wrong on my conjecture. No new combinators are needed and apparently the old ones suffice.]

Advertisements