# The relationship between "true formula" and types in the Curry–Howard correspondence

I have been working through the Implication World in the Natural Number Game using Lean from the following link: https://adam.math.hhu.de/#/g/leanprover-community/nng4/world/Implication/level/0

While solving the exercises, I have started to get a sense of how proofs can be constructed using types. However, when I read the following description on the Curry–Howard correspondence Wikipedia page (https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence), I found something that doesn’t quite sit right with me:

Logic side Programming side
true formula unit type or top type
false formula empty type or bottom type

In languages like OCaml, a unit type is an empty tuple, and in languages like TypeScript, a top type is a type that encompasses all other types. These are very different concepts, so I don't understand why they are both listed as corresponding to a true formula. Additionally, in typical programming languages, true and false are usually represented as boolean values(boolean type). Why, then, do true formula correspond to unit type or top type?

• As usual, Wikipedia strikes again by being wrong. Commented Jul 13 at 11:38
• There, I fixed the Wikipedia page. Thanks for pointing out the deficiency. Commented Jul 13 at 12:01

Wikipedia is wrong, as it often is. Under the Curry-Howard correspondence we have:

Logic Type theory
formula $$A$$ type $$A$$
proof $$p$$ of $$A$$ term $$t : A$$
constant $$\top$$ unit type $$1$$
constant $$\bot$$ the empty type $$0$$
true formula $$A$$ inhabited type $$A$$
false formula $$A$$ uninhabited type $$A$$

(A type is said to be inhabited if it has some elements.)

The confusion arises because Wikipedia does not distinguish between the truth constant $$\top$$ and a true formula. Likewise for the falsehood constant $$\bot$$ is not the same things as a false formula.

Specifically, if $$A$$ is a true formula then $$\top$$ and $$A$$ are logically equivalent, but not actually the same. On the type-theoretic side, such a logical equivalence corresponds to having maps $$f : A \to 1$$ and $$g : 1 \to A$$, but there is no requirement that they be inverses of each other. This is why Wikipedia is wrong (it has since been fixed): it literally says that under propositions-as-types all true formulas maps to the unit type, whereas it should say that they map to various types, all of which are inhabited.

There is often a further confusion regarding the type bool of boolean values. Under the Curry-Howard correspondence, bool correponds to a logical statement that has exactly two canonical proofs. (Similarly, nat would correspond to a logical statement that has infinitely many canonical proofs, one for each number.) If you think this is strange, you are right, and a further refinement is possible under which formulas correspond to those type that have at most one element.

A second source of confusion arises because one would naturally expect that bool corresponds to the type of truth values. This is also the case, except that bool does not reprsent all types, only the decidable ones. Recall that $$A$$ is decidable if $$A + (A \to 0)$$ is inhabited. Let Prop be the type of propositions, i.e., those types that have at most one type. Then we have:

Theorem: The types $$\mathsf{bool}$$ and $$\Sigma_{A : \mathsf{Prop}} A + (A \to 0)$$ are equivalent.

It's not surprising that programming languages only use bool, because the whole point of bool is to be able to make if-then-else descisions.

• I upvoted your answer. However, I am a programmer and currently lack the mathematical knowledge to fully understand your answer (especially the difference between the constant ⊤ and a true formula 𝐴, and how they differ from the bool type in programming). So I am unable to approve the answer now. Commented Jul 14 at 0:43
• It's the difference between $True$ and $1=1 \lor 2=2$. Both are formulas. Both are "true" as in "can be proven." But only the first is "literally the formula called $True$" whereas the other is a disjunction, with each subformula being an equation. The second formula also has two canonical proofs (since you can prove either side of the disjunction), whereas the first has only one (the one proof that $True$ is indeed true, there's only one). Commented Jul 14 at 3:59
• A boolean is not a formula. Saying "true the boolean is true" is a type error, like saying "1 is false" or true + true = 42. It makes no sense. You can talk about whether a formula is true or whether a boolean is true. Both are completely different things that happen to unfortunately have the same name. Commented Jul 14 at 4:00
• @shingo.nakanishi: Would you say that the constant true and Pythagora's theorem are the same thing? Both are true, therefore logically equivalent. But if they are the same thing, why didn't your math teacher in school just say "true", instead of drawing triangles, and explaining things so that you could absorb Pythagora's theorem? Commented Jul 14 at 7:15
• Yoou should forget about the constant $\top$ for the moment and concentrate on what is written in the table about "formula $A$ is true", namely "type $A$ has an element". Think about that: a type represents a true formula when it has an element. Now, as an exercise, write down three types that have elements, and three types that do not have elements. Commented Jul 14 at 7:21

The unifying perspective is category theory, sometimes listed as a third column in a "Curry-Howard-Lambek" correspondence (also called the computational trilogy).

Unit types, usually written $$\top$$, are terminal objects in the (hand-wavey) category of types and functions, which means that for any other type $$A$$ there is a (unique) morphism $$A \to \top$$. Top types, also written $$\top$$ but used in different contexts, are greatest elements in the set of types partially ordered by the subtyping relationship $$\leq$$. Viewing partially ordered sets as thin categories, this means that they are also terminal objects: for every other type $$A$$, there is a subtyping relationship $$A \leq \top$$, which also implies $$A \to \top$$ (this morphism need not be unique, but this doesn't really matter to the propositions-as-types interpretation).

Dually, empty types and bottom types $$\bot$$ are both instances of initial objects in different contexts, which means that for every other type $$A$$ there is a (unique) morphism $$\bot \to A$$ or a subtyping relationship $$\bot \leq A$$ (which implies a morphism $$\bot \to A$$).

And of course, true and false formulae are terminal and initial objects in the poset of formulae ordered by implication.

• What's with the downvote? Commented Jul 16 at 8:16
• Indeed, the downvote is concerning. I have upvoted it to restore it. I am not an expert in this field and could only find resources in Japanese, but your answer seems similar to the order theory and lattice theory described in this link: zenn.dev/estra/books/algebraic-subtyping-models/viewer/…. Commented Jul 17 at 1:51
• Alternatively, it might be similar to the category theory described in this link (could this be the Lambek part?): zenn.dev/estra/books/algebraic-subtyping-models/viewer/…. Commented Jul 17 at 1:52
• Your answer mentions Curry-Howard-Lambek, but Wikipedia does not seem to provide a detailed explanation of Curry-Howard-Lambek. Could you add a table for Curry-Howard-Lambek into your answer? Commented Jul 17 at 1:53
• shingo: see computational trilogy on the nLab for such a table. @JulioDiEgidio there's nothing vague about it; this is an extremely uncontroversial viewpoint among modern mathematicians and computer scientists. I'm not claiming that category theory is a feasible foundation for mathematics, but it certainly has been successful in informing our design for such (see HoTT). Logic, types, and categories. Commented Jul 17 at 8:35