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)