A completeness result for µ
Phillipe Audebaud, Steffen van Bakel · 2006
We study the expressivity of Parigot's �µ-calculus, and show that each statement ⊢LKthat is provable in Gentzen's LK has a proof in �µ. This result is obtained through defining an interpretation from nets from the X -calculus into both the �-calculus and �µ; X enjoys the full Curry-Howard isomorphism for (the implicative fragment of) LK, and cut-elimination in LK is represented by reduction in X. This interpretation will be shown to preserve reduction in X via equality in the target calculi, and to preserve typeability using the standard double negation translatio n technique of types. Using the fact that, in �µ, we can inhabit ¬¬A→A for all types A, a completeness result as well as a consistency result are sh own for�µ.