It may be slightly easier to work through it for the formula ¬¬¬P ⇒ ¬P. (This also a constructive tautology, and the above formula is an instance of it, taking

It may be slightly easier to work through it for the formula ¬¬¬P ⇒ ¬P. (This also a constructive tautology, and the above formula is an instance of it, taking P = ¬ϕ). So let's prove that. Expanding the definition of ¬, we must prove (((P⇒False)⇒False)⇒False)⇒P⇒False. I.e. we are given two assumptions f : ((P⇒False)⇒False)⇒False x : P and should prove False. So we can use the assumption f, provided we can find an argument of type ((P⇒False)⇒False) to call it with. And in fact that's easy: (λg. g x). The full proof term is λf.λx. f (λg. g x) Indeed, this is a perfectly good function (so it's constructive). If we type that function into (say) a Haskell repl, the typechecker will infer an even more general type for it, but we can check that the type we wanted is an instance: ghci> :type (\f x -> f (\g -> g x)) (\f x -> f (\g -> g x)) :: (((t2->t1)->t1)->t) -> t2 -> t gchi> type Not a = (a -> False) ghci> :type (\f x -> f (\g -> g x)) :: (Not (Not (Not p)))->Not p (\f x -> f (\g -> g x)) :: (Not (Not (Not p))) -> Not p