9

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"? – Not_Here May 8 '17 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. – Not_Here May 8 '17 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. – Boris E. May 8 '17 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. – Boris E. May 8 '17 at 18:25
  • Doesn't Girard's transcendental syntax, which you asked about before, focus on exactly these types of issues: Curry-Howard isomorphism, computational justification for logical rules, etc? The second question takes it too far, I think. Classical logic, on standard interpretation, certainly pays no attention to computability, that seems to be a constructivist/proof-theoretic trait. Modal logic, Kripke's version anyway, has an even more bloated platonist semantics. I'd say one can single out computation-friendly logics, but they don't need to be so. – Conifold May 8 '17 at 22:44
9

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.

  • Very clear and interesting answer. I also felt that it's "under-appreciated" as you said. Now, I have some questions and remarks. (1) Are we sure that Logic and computability are not identical ? Do we really understand what a proof is ? It seems that Girard's Ludics give a computational/interactive nature to proofs, I don't know if it's relevant in our context. (2) What do you mean by "formal in nature" (about logic) (3) You don't have any references discussing the correspondence from a philosophical viewpoint ? – Boris E. May 10 '17 at 20:41
  • 1
    One might argue that what is computable is constrained by the laws of nature. There are several proposed 'hypercomputers', i.e. devices that transcend what is Turing-computable, but they cannot be built in our universe. Logic is usually understood as more abstract. By 'formal in nature' I just mean to refer to accounts of logic in which the formality is an essential feature of what we understand by logic, rather than a product of the way we study it. There are several different ways logic can be formal. If you search for John MacFarlane's Ph.D. thesis online he has a good account of this... – Bumble May 11 '17 at 13:10
  • As to philosophical references on the Curry-Howard correspondence itself, I think there are very few: most discussion focuses on the technical aspects. – Bumble May 11 '17 at 13:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.