Programming Language and Logic Links

These thread on Lambda the Ultimate has several interesting links to online papers and books about the links between logic and functional programming languages.

What’s interesting is that, with one giant exception (category theory), the mathematics used is among the least fashionable. Most mathematicians can go through their entire careers without learning anything about proof theory and intuitionistic logic, and I think the reason is that both undermine the naive model of mathematical foundations that most mathematicians carry around in their heads. Mathematicians hate thinking about foundations. Whenever a famous open problem turns out to be equivalent to the Continuum Hypothesis, it’s like a family member died, or worse joined a cult.

Proof theory is disconcerting because it treats mathematican proofs as purely syntactic. Mathematicians, whatever their actual philosophy, adopt a working philosophy of Platonism: symplectic manifolds and 7-spheres and von Neumann regular algebras all exist in some nebulous “out there”. While mathematicians occasionally argue that mathematics is just the formal manipulation of symbols, in practice they think of a 7-sphere as an actual object.

In proof theory, mathematics really is just a formal manipulation of symbols. The more elementary parts of proof theory consist of proving one method of representing proof symbolically is the same as another. More advanced proof theory consists of studying topics such as proof normalization, where it is shown that proofs can be systematically rewritten in a particular form. Here are some further links to proof theory texts.

Intuitionistic logic is another field more prominent in computer science than in mathematics. Intuitionistic logic unnerves mathematicians by removing the law of the excluded middle: that a statement is true, or its negation is true. In classical logic, every statement can be (in principle) assigned a value of either true or false. To do the same for intuitionistic logic, some statements must be assigned intermediate truth values (in fact, infinitely many intermediate values become possible). Most mathematicians regard intuitionism as a historical curiosity not particularly of study.

Intuitionism is attractive to computer scientists, because whether or not its axioms correctly model truth, they do model knowability. The law of excluded middle doesn’t apply to knowability. A statement that is not known to be true may also be not known to false. Curry-Howard correspondence between logical formulas and function types has insired study of even weaker logical systems.

6 thoughts on “Programming Language and Logic Links

  1. Well, I consider myself a mathematician, in outlook if not in form (I guess I just drank too much of the coolaid), just as I consider you one. And while I concede your central point, I must say that I always found those subjects interesting and worthy of study (but then again, look at me, I like model theory). I once convinced myself that the law of the excluded middle was OBVIOUSLY false. My downfall I suppose is that just like a vegan who can’t give up egg salad sandwiches, I could never give up contrapositive proofs.

    “I talk like a Platonist, but I’m not one” – M. Scott Osborne

  2. I’m also sort-of a mathematician who ended up showing more interest in the foundational stuff than the mathematics itself. Set theory, model theory, godel, lambda calculus, modal logics, intuitionism etc.

    I think most mathematicians have some awareness about constructive proofs, most will avoid using things like choice unless strictly necessary, some will even avoid gratuitous use of excluded middle and so on. Constructive mathematics is quite interesting in its own right too, in a philosophical sort of way. Constructive proofs are often easier to visualise and comprehend, too.

    The little of proof theory I’ve seen does seem rather irrelevant to mathematicians though – once you’ve proved completeness of first-order predicate calculus, and are aware of Godel’s incompleteness results, that’s about all the information on formal proofs that a mathematician cares about/needs. Although perhaps I’m missing something and people can enlighten me?

    Proof theory also seems intimidatingly technical and dull, but I can see it’s very useful for type theory / computer science so perhaps I should know more about it.

  3. Mathematicians don’t care about about foundations because they don’t matter! It’s like using a well encapsulated software library. You don’t care what the inner workings are as long as the library performs as specified. If someone came along and completely rewrote the library, only the users who had been exploting the pathological cases might actually notice anything had changed. Same goes for foundations. Even if someone came along and found a contradiction in ZF, say, it would probably be in some really abstruse area, someone would come along with a ‘patch’, we’d have a new set of axioms and 99.99% of published mathematics would remain unaltered.

    But – even though most mathematicians couldn’t care less about foundations, they are mostly glad to know that somewhere, someone else is working on them. It gives a sense of comfort to know your work is well founded (no pun intended), even if you don’t care what those foundations are.

  4. I meant my comment more as a sociological observation than as a universal truth. There are mathematicians interested in proof theory, and intuitionistic logic — they are, after all, branches of mathematics. But they’re not particularly fashionable within mathematics, and I was just speculating why.

    I think your point, sigfpe, is basically on target, but it’s interesting to me that foundations gets the software library treatment, and abstract algebra (for example) does not. Unlike virtually other academic discipline, the foundations of mathematics is just another branch of mathematics. What makes proof theory, a branch of mathematics, not matter, and algebraic topology, a branch of mathematics, matter? I think part of it is that most mathematicians have an ingrained Platonism (even when it is not their stated philosophy, a la Osborne), and topics that deviate from that seem weird. (You and I are outliers in that respect, Michael.)

    Citylight: Proof theory can be used to prove that Goodstein’s Theorem from a couple of days ago is independent of Peano Arithmetic. Maybe I’ll outline that in a post when I get a chance.

  5. I find it a bit ironic that THIS is the entry that has exploded with comments. That being said, I have to reply to sigfpe. It’s not so much that that mathematicians don’t concern themselves with foundations because they don’t matter (because they matter a great deal), it’s because they like to prove things. I am convinced that in order to manipulate these things in your mind to reach conclusions about them, it is almost a prerequisite that they take on a platonic reality in your head. In some sense, playing around with foundations is turtles all the way down, whereas the tangent bundle to S^7 can take on a hard reality that you can get your hands on (so to speak). It is, I think for most people, and easier task. I would go out on a limb, and say that if the foundations were thrown out tomorrow, due to some fatal logical inconsistency (that, for ther sake of argument, was not in some remote pathological case) the majority of mathematicians today would say “fuck it, I’m still doing what I have been doing”.

  6. Pingback: Ars Mathematica » Blog Archive » Goodstein Revisited

Comments are closed.