Difference between $\lambda$-$\mu$-calculus and intuitionistic type theory + LEM for classical proofs?

Question

I have some experience with using type theory to do proofs in intuitionistic logic. If I want to prove theorems that require classical logic, I simply pose the law of excluded middle (LEM) as an axiom. As far as I understand, intuitionistic logic + LEM gives you classical logic, so I presume that all theorems that have a classical proof, have a proof in intuitionistic-logic-type-theory with LEM as an axiom.

But then I heard about so called $\lambda$-$\mu$-calculus, and that this is meant to extend the Curry-Howard isomorphism to classical logic. I haven't managed to get the point of $\lambda$-$\mu$-calculus yet, hence this question.

How is $\lambda$-$\mu$-calculus different from $\lambda$-calculus + Curry-Howard + LEM as an axiom?

Answer 1

As far as I can tell (I am no expert, I simply googled) they are different ways of doing the same thing. $mu$ calculus appears to give one continuations.

I shall use Haskell notations from here on out. If this does not work for you, I can rewrite my answer, but I am more familiar with logic through Haskell/Coq than the math, so I might get it wrong :)

Now, if we have continuations, then for any type a, we can construct the equivalent value cont_a :: forall r. (a -> r) -> r which is the continuation representation of a.

Setting r = Void gives us cont_a :: forall a. (a -> Void) -> Void. This is the principle of double negation elimination, since it allow us to "instantiate a value" (produce a proof) of $\lnot\lnot a$, since $\lnot a$ is encoded as a -> Void in the type theory.

Answer 2

First, Curry-Howard is not a thing you "add" to the lambda calculus. It is a family of theorems that relates typed lambda calculi and proof theories.

Anyway, let's say you are working in Agda. You want to do some classical reasoning so you postulate LEM, say as:

postulate lem : {P : Set} → isProp P → P ∨ ¬ P

where isProp P just asserts that there is at most one value of P. See below for a full listing.

Now we want to prove a classical theorem like double negation elimination.

dne : {P : Set} → isProp P → ¬ (¬ P) → P
dne isProp-P ¬¬p with lem isProp-P
dne isProp-P ¬¬p | Left p = p
dne isProp-P ¬¬p | Right ¬p = absurd (¬¬p ¬p)

This typechecks and is a valid classical proof, so what's the problem?

The problem is that this doesn't compute. If you try to normalize it, Agda will get stuck (as with all postulates) on the case analysis of lem. Okay, but who actually runs their Agda programs? Agda does. Agda normalizes terms during the course of typechecking, and if it gets stuck, it will just fail to typecheck. Regardless, a key part of the Curry-Howard correspondence is to connect computation to proof reduction, and postulates don't have any computation rules associated with them.

What the $\lambda\mu$ calculus does is make a computational system that does give computational meaning to classical theorems like lem. The equivalent to a use of thedne proof can then be "normalized". Essentially what happens is the call to lem immediately returns Right ¬p where ¬p is a continuation which gets passed to ¬¬p. ¬¬p either produces ⊥ without using ¬p, in which case we're good because we jump away abandoning this (sub)computation, or it applies ¬p to some p which causes us to jump back to the call to lem and return Left p and we're done. This approach to the computation is not available in the simply typed lambda calculus which represents intuitionistic (or minimal) propositional logic, and remains unavailable in an intuitionistic type theory such as Agda.

Full listing:

data ⊥ : Set where

absurd : {A : Set} → ⊥ → A
absurd ()

¬ : Set → Set
¬ A = A → ⊥

data _≡_ {A : Set} (a : A) : A → Set where
    Refl : a ≡ a

data _∨_ (A B : Set) : Set where
    Left : A → A ∨ B
    Right : B → A ∨ B

isProp : Set → Set
isProp P = (x y : P) → x ≡ y

postulate lem : {P : Set} → isProp P → P ∨ ¬ P

dne : {P : Set} → isProp P → ¬ (¬ P) → P
dne isProp-P ¬¬p with lem isProp-P
dne isProp-P ¬¬p | Left p = p
dne isProp-P ¬¬p | Right ¬p = absurd (¬¬p ¬p)