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

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) :

• In regards to (1) computability theory and proof theory are branches of (mathematical) logic which seems to be the logic you're interested in, so I don't see how someone could say they are unrelated. But remember that the notion of computability is informal, the Church-Turing thesis is based off of the informal idea of computability. In regards to (2) that depends on what you mean by "a logic," if you just mean any formal system, then no. This about a very basic axiomatic, deductive formal system like Hofstadter's MU system. Are you using "a logic" synonymously with "a formal system"? May 8, 2017 at 14:15
• But also you should think about what a 'computational system' is. There is an easy argument to make that even a basic system like MU can be used to represent some sort of computation. I believe Scott Aaronson in a lecture about the limits of computation made the quip that its possible to consider any system as a computational system, even a toaster making toast, but that doesn't mean its useful to do so. Associate one of the deductive rules with the successor function and if you can show a proof that there is some derivation of some string in that language then you can prove some arithmetic. May 8, 2017 at 14:19
• @Not_Here (1) I read that the "nature" of logic wasn't clear. Maybe I'm a bit out of date but some seems to think that logic depends on human's ideas (psychologism), comes from reason etc whereas computation "seems" to come from "the nature". I thought it could somehow provide answers on the justification of the logical rules/laws or the fundations of Logic for instance. May 8, 2017 at 18:24
• @Not_Here (2) I admit it's not clear. I'm not sure myself but I think I mean "logic" in an informal way, the one we think of when talking about the human reasoning. Maybe I still have a naive conception of Logic but I wondered if logical systems without any correspondence to a system like the lambda-calculus should enjoy the same status as, say, the natural deduction. J.Y Girard once said that he see logics without cut-elimination like cars without engine. May 8, 2017 at 18:25
• It seems that classical uses of classical logic paid little attention to its computational properties, whatever they might be, and nonconstructive reasoning appears already in Euclid. If so, then our paradigmatic example already shows that the idea of logic is distinct from the idea of algorithm. Intuitively, even in computational contexts, logic is not so much about computing per se, as about verifying validity of a documented computation, it is normative in a way computing isn't. May 8, 2017 at 23:03

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.