1
$\begingroup$

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

$\endgroup$
  • 3
    $\begingroup$ 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. $\endgroup$ – Conifold Jul 3 '19 at 9:30
  • $\begingroup$ @conifold, what is the difference between "a truth value" and "a truth value gap", apart from terminology? $\endgroup$ – user56834 Jul 3 '19 at 9:43
  • 2
    $\begingroup$ 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$. $\endgroup$ – Conifold Jul 3 '19 at 9:45
1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thanks for the answer! I am a bit confused about what the central message is. Could you connect this to my question more explicitly (maybe with one sentence)? $\endgroup$ – user56834 Jul 4 '19 at 4:54
  • $\begingroup$ The first paragraph answers how Curry-Howard (with respect to the Simply Typed Lambda Calculus) would allow you to show that LEM is not derivable. The rest tries to clarify how semantics are actually connected to this. Curry-Howard isn't about semantics. Also, it doesn't make sense to say LEM is a syntactic property. The derivability of LEM is a syntactic property, but the validity of LEM is a semantic property. LEM is just a formula (schema). $\endgroup$ – Derek Elkins left SE Jul 4 '19 at 5:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.