Hacker News Reader

Comment by shigeo | Hacker News Reader

Intuitionistic logic and intuitionistic type theory follow essentially the same set of rules, so how does type theory allow for a "marriage of mathematics and computation" any more than logic, which everyone already uses?

View on HN

Because conventional mathematics, whether based on set theory or some categorical alternative, has (usually classical) logic as a background theory. In type theory, that's all you need. It is a theory of computation that has a "built-in" logic. And there's more than just intuitionism. There are type theories that model non-constructive/classical logic and are yet still computable programming languages. So we can write computable code and prove properties about that code in the same theory.

> There are type theories that model classical logic and are yet still computable programming languages.

Thanks, but this seems absurd to me. Please elaborate!

I'm not an expert, so please take the following with the grain of salt.

One of the examples of computation formalisms providing the classical logic at the type level is the Parigot's [λμ-calculus](https://en.wikipedia.org/wiki/Lambda-mu_calculus). λμ-calculus adds μ-abstraction to the classical λ-calculus.

μ-abstraction resembles the notion of continuation. With that addition Peirce's law of classical logic becomes deductible without any modifications (e.g. double-negation translation). The program that proves Peirce's law is just call/cc function.

This topic seems to be an ongoing research, so you may find lots of articles in public internet space. Many interesting introductory articles are among the advanced materials of [this course](https://www.cs.ru.nl/~freek/courses/tt-2011/), including the original Parigot's paper.

There are a number of different type theory models for classical logic. The first to my knowledge was a model that uses the call-with-current-continuation (call/cc) control flow operator. While this does model classical logic, some say it is not particularly useful as a practical programming construct, which is perhaps why it does not seem to be adopted by any major proof assistant. More recently I've seen a few papers showing that type theoretic models of concurrency can also model classical logic, e.g. see "Classical Proofs as Parallel Programs" < https://arxiv.org/abs/1809.03094 >. The original idea that the Curry-Howard correspondence only applies to intuitionist logic is wrong.

Reply on news.ycombinator.com