How exactly does the currry-howard formalization of logic capture the semantics of LEM not holding?

Question

Let $p$ be a proposition and $P$ the collection of propositions. In classical logic, the law of excluded middle holds, and we can model the semantics of this as saying that there is a function $\text{Truthvalue}:P\to \{true,false\}$.

In intuitionist/constructivist logic, the law of excluded middle doesn't hold, and we can model the semantics of this as saying that the function $\text{Truthvalue}$ has a range that doesn't contain only $true,false$. For example, we could have $\text{Truthvalue}:P\to \{true,false, undetermined\}$.

I am having trouble seeing how the (syntactic) formalization of proofs in the curry-howard (CH) isomorphism capture this (semantic) idea. I can see that in the CH isomorphism, LEM doesn't hold by default, but LEM is a syntactic property, and I cannot see how CH can capture the underlying semantics that I just explained.

To be clear, I am referring to the formalization where a proposition $P$ is a type, and a proof of $P$ is an inhabitant of $P$ and a proof of $\neg P$ is an inhabitant of the type $P\to 0$ where $0$ is the uninhabited type. My question essentially is, how can we understand these proof-theoretic (syntactic) notions as capturing the truth-theoretic/model-theoretic (semantic) notion that a truth value cannot just be true or false (but also e.g. "undetermined").

Answer 1

Let's take the archetypal example of the Curry-Howard correspondence: the correspondence between the natural deduction presentation of Intuitionistic Propositional Logic and the Simply Typed Lambda Calculus (with products and sums). With this, the argument is simply there is no term in the Simply Typed Lambda Calculus of type $P+(P\to 0)$ where $P$ is some unspecified base type. Proving this usually uses standard (but non-trivial) properties about the Simply Typed Lambda Calculus, e.g. strong normalization.

Often discussions of Curry-Howard talk about the BHK interpretation. This is essentially a semantics, it just happens to be a semantics that doesn't validate excluded middle. You can fairly easily generalize this semantics to interpreting intuitionistic propositional logic into any bicartesian closed category. This provides a more typical route to showing that LEM isn't validated by choosing a particular bicartesian closed category for which LEM is false.

One choice would be a bicartesian closed category built out of the syntax of the Simply Typed Lambda Calculus (with products and sums), called a syntactic category. This would connect the perspectives of the first and second paragraphs, albeit Curry-Howard states something stronger than this because it links proofs and terms, not just propositions and types. We can go even further and state that the Simply Typed Lambda Calculus (with products and sums) is the internal language of bicartesian closed categories.

These connections lead to computational trinitiarianism.

However, the general idea of Curry-Howard is the ability to connect derivations in a proof system to terms in a type theory. This can be applied to classical logics as well; it doesn't itself lead to intuitionistic logic. We can also extend the categorical connections to other logics. Intuitionistic logic only really comes up because from a computational/type theoretic view and from a categorical view, the systems corresponding to intuitionistic logic are more natural, so these correspondences were discovered first and are more relevant.