I wonder if there is some direct proof of how $\lambda$–$\mu$-calculus maps to classical logic via the Curry-Howard correspondence. Just like one can verify a valid sentence in propositional logic by stupidly checking truth tables, I'm curious if there is a similarily stupid (not necessarily efficient!) algorithm to find a $\lambda$–$\mu$-term belonging to a given (classically valid) type.
I imagine some kind of dialogue game, I try to prove $P:=P_0\Rightarrow P_1$, either there is already an intuitionistic proof, in which case I'm done. Otherwise, I pretend to have a term of type $P$ and see if my opponent feeds something of type $P_0$ into it. I continue recursively and every time I encounter an atom, then somehow return it to the root (this part I'm not sure how to do in $\lambda$–$\mu$-calculus).
Let $X$ be the subset of atoms in $P$ which evaluate to true (in a given interpretation), $P_1$ is then either classically true or false. In the first case, I assume to get enough ressources while recursively poking $P_0$ so that I can continue at the root and construct $P_1$. In the other case, my bluff of calling $P$ is never revealed.
Is there some way to formalize this idea in $\lambda$–$\mu$-calculus?
Best Answer
What you are referring to is called the type inhabitation problem. Since for the simplest case, simply typed $\lambda$-calculus, the problem is PSPACE complete, any generalization of that inherits this difficulty.
UPDATE: (To account for the comments)
One can extract the term that inhabits the given type using prover skeptic dialogues. You may search further, and I would recommend reading about the simpler case of intuitionistic formulae with implication symbol only.
Your analogy with brute-force checking the truth tables of a formula does not stand. Lambda terms are a formality for describing proofs, and propositional formulae are to be proven. Brute forcing the truth tables outputs yes or no, where inhabitation of a type provides a formal proof. The first being on the semantics side, the other on the syntax side.