3 ms·

> There are type theories that model classical logic and are yet still computable programming languages. Thanks, but this seems absurd to me. Please elaborate!

by shigeo 6y ago

bread_juice 6y ago
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 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/ https://www.cs.ru.nl/~freek/courses/tt-2011/), including the original Parigot's paper.
outlace 6y ago
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 https://arxiv.org/abs/1809.03094 >. The original idea that the Curry-Howard correspondence only applies to intuitionist logic is wrong.

> There are type theories that model classical logic and are yet still computable programming languages. Thanks, but this seems absurd to me. Please elaborate!

by shigeo 6y ago

> There are type theories that model classical logic and are yet still computable programming languages. Thanks, but this seems absurd to me. Please elaborate!

bread_juice 6y ago

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 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/ https://www.cs.ru.nl/~freek/courses/tt-2011/), including the original Parigot's paper.

outlace 6y ago

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 https://arxiv.org/abs/1809.03094 >. The original idea that the Curry-Howard correspondence only applies to intuitionist logic is wrong.