Logic and Computation: a philosophical viewpoint on Curry-Howard isomorphism

Question

The link between logic and computation is stronger than ever, especially since the establishment of the Curry-Howard isomorphism specifying that proofs can be seen as programs and formulas as program's types.

I wondered if we could find any texts providing a philosophical viewpoint of the relation between logic and computation. I couldn't find any document about that.

Moreover, I have some related questions :

1) Since most logical systems (e.g intuitionnistic natural deduction, classical sequent calculus) corresponds to computational systems (e.g simply typed λ-calculus, system F, combinatory logic...), can we say that logic and computation have the same nature and origin ? A lot of difficulties arised from the question of the nature of Logic, does computation give an answer ?

2) Can we say that any system which doesn't share computational properties with a computational system is not "a logic" ? (e.g no cut elimination theorem, no confluence/church-rosser property)

EDIT : After some research

The only things I could find were the work of the french group LIGC but most of the articles they write are in french only.

It seems that most of the works linking philosophy and computation concern Linear Logic (which emerges from the Curry-Howard isomorphism) and the Lambda-Calculus (which give a formal account to [functional] computer programs).

If I'm not wrong, Linear Logic takes computation (cut-rule elimination seen as evaluation of programs) as a basis for logic. Some properties on programs such that the cut-elimination theorem, confluence or the church-rosser property, when taking the point of view of logic, ensure that our logic behave in a coherent way. We rely on the operational behaviour of logic rather than language or purely philosophical foundations.

It seems that these work haven't reached the english community yet but maybe one can find some articles in english written by the members of the group.

Some not-too-technical papers (unfortunately in french) :

• Interaction et Signification, Samuel Tronçon
• Y a-t-il une Kehre de la logique ?, Jean-Michel Salanskis
• La logique linéaire et la question des fondements des lois logiques , Alain Lecomte

Answer 1

I think you are right to be impressed with the Curry-Howard correspondence. It is a detailed and extensive rule-by-rule and feature-by-feature isomorphism. This strongly suggests that proof and computability are closely related. I also agree that it is under-appreciated within the philosophy of logic and that we can and should allow it to inform our understanding of logic.

Logicians are fond of arguing about logic. They will disagree even over basic things such as what account to give of the concept of validity. Ask Frege, Quine, Tarski, Davidson, Lewis, Prawitz, Etchemendy, McGee, Brandom and MacFarlane and you will get ten different answers. They will also argue about whether there is a single "one logic to rule them all" and if so, which one it is, or whether logical pluralism is defensible. According to Dummett, intuitionism is the only way to go; for Read it is relevance logic, for Priest paraconsistent logic, for Quine classical logic.

On the computability side of the fence, there is relatively little argument about what account to give of computability. There are some issues about the precise way to state the Church-Turing thesis, whether and how it applies to interactive computers, and whether considerations such as the laws of nature should be allowed to determine what we may call a computation.

So since we apparently understand computability pretty well, and logic rather less well, it seems to make sense to allow our grasp of the former to help us with the latter.

It is important to notice that the Curry-Howard correspondence extends to classical logic. Curry and Howard themselves were not aware of this when they formulated the correspondence. They started from the BHK interpretation of intuitionism and used the fact that intuitionistic proofs are constructive to read these proofs as recipes for a computation. But subsequent work by computer scientists, including Griffin, Parigot, Aschieri and others showed that even classical logic shares the correspondence. What this means in practice is that there are computational interpretations of classical systems that are normalizable and allow computations to be extracted from classical proofs.

This does not mean that any classical sentence is computable: clearly there are any number of undecidable sentences. The full extent of what is classically computable is still an area of research. But it does mean we can dispense with the simplistic idea that classical logic is non-constructive while intuitionistic logic is constructive. Classical disjunctions, for example, can be the objects of cut-free proofs, as Girard noted in his paper A New Constructive Logic: Classical Logic.

To address your specific questions:

1. Logic and computability are indeed closely related. They are not identical however. At the least, computations take place over time and require a computing engine of some kind. Proofs are often thought of as abstract structures, though any instance of a proof will require some physical form.

2. The idea that a logic should possess some computable apparatus to qualify as a logic is not as weird as it may sound. It would not exclude classical logic from qualifying. It is a strong requirement though, and might be contested by those who view the semantics of logic as taking primacy over the proof theory.

As a final speculation, I suspect that the link between logic and computability supports the view that we should understand logic as essentially formal in nature. Accounts of logic that play down formality would have more difficulty in explaining the connection with computability. Also, some very broad notions of what counts as validity might be rejected on the basis that they cannot be rendered straightforwardly into a computable form.