Ars Mathematica

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.