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

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").

• Intuitionist logic is not a three-valued logic, and $undetermined$ is not a truth value, it is a truth value gap. Intuitionist connectives are not truth functional, for example. CH does not capture this semantics because it is not the right semantics. For the correct semantics one needs to map formulas into a Heyting algebra. Jul 3, 2019 at 9:30
• @conifold, what is the difference between "a truth value" and "a truth value gap", apart from terminology? Jul 3, 2019 at 9:43
• You can not define operations on "truth values" that work correctly. For formulas evaluated as $undetermined$ the disjunction will sometimes be $undetermined$ and sometimes $true$. Jul 3, 2019 at 9:45

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.