# Curry-Howard Isomorphism For Classical Logic

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?

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.

• OK, but truth tables checking is exponential in complexity (I think?), so what is the implication? Oct 11, 2022 at 8:17
• Just that it is difficult to even find resources on the subject. Also, if we naively think about it, type inhabitation is like searching for a formal proof of the given formula. This by the CHC. It is definitely not something that is easily computed. Oct 11, 2022 at 8:23
• Yes, but I'm not looking for an effective computation, just for a stupid one. BTW I didn't give you the downvote! Oct 11, 2022 at 8:25
• I have deleted my last comment and updated my answer. Oct 13, 2022 at 6:17
• Cool, thanks! I'll accept the answer later but I just want to leave it open for a few days to see if somebody else comments... Do you maybe have an example of a $\lambda$-$\mu$-term of type $P\to Q$ where $Q$ is not an atom? Oct 13, 2022 at 6:29