Does Law of the excluded middle collapse constructivity?

This is the law of the excluded middle:

¬a ∨ a

It states that for the refutation of a refutation, we can get a proof. It can be also interpreted that only either one can be proven. Same thing cannot be both proven and disproven.

Classical logic tends to manifest as introduction of continuations into lambda calculus. I've been starting to notice a pattern in such constructs that suggests we never had any problem with the excluded middle in expressions.

It suggests that the capability of intuitionistic logic to provide a computational medium might simply be due to implicit linearity present in the expressions. As you cannot duplicate the environment and then answer to two different environments.

Typed lambda calculus also suffers from the lack of linearity, despite that it is linear enough to have any constructivity at all. To illustrate lets consider few things.

You know that the sum types get the following shape:

type Sum a b = (a -> c) -> (b -> c) -> c

inl :: a -> Sum a b
inr :: b -> Sum a b
case :: Sum a b -> (a -> c) -> (b -> c) -> c

inl a = λf. λg. f a
inr b = λf. λg. g b
case x f g = x f g

Then the product type can be modeled with:

type Product a b = (a -> b -> c) -> c

product a b = λx. x a b
left a  = a λx.λy.x
right a = a λx.λy.y

These are treated as duals, to the point that you may call them products and coproducts.

Linear logic starts from the viewpoint that these are not dual concepts. Both are forms of conjunction. Ability to copy without control collapses them into the same.

Duals can be obtained by examining the values on the argument side of a function.

Product a b -> c ≡ a -> b -> c
Sum a b -> c

From currying you know that you can dempose product argument so it connects functions and products together. For the sum we actually are unable to construct a proper dual. Specifically you'd like to convey "You can take either one of these, but not both". But you can't because dual of the sum collapses into a product.

There is actually a linear logic formula that states this collapse.

!(A & B) ≡ !A ⊗ !B

Similar posts