4
$\begingroup$

In dependently typed languages such as Agda, Lean, Coq, Idris (and Pie), a mathematical or logical statement can be expressed as a type, and then proven by writing a program that creates an instance of that type. The Curry-Howard isomorphism justifies this by noting that certain structures used to manipulate types are isomorphic to inference rules in logic.

Some types in these languages are not naturally viewed as expressing statements, but are nevertheless types of objects that can be constructed. Consider, for example, the type of function multiplying a natural number (using Nat as the type of natural numbers, and using roughly Idris/Agda syntax):

double : Nat -> Nat
double x = 2 * x

triple : Nat -> Nat
triple x = 3 * x

quadruple : ...

Are these proofs of Nat -> Nat? If so, what does that type "say", if anything? That if Nat, then Nat, but what does that mean? "If natural number then natural number" is not a sentence of English.

The only partial answer I've seen on this topic is from the dialogue in Friedman and Christiansen's The Little Typer, in chapter 8, frames 25-30, pages 177-178. However, Friedman's The Little books are often playful, so it's not clear how seriously to take what's said:

Can every type be read as a statement?
In principle, they could be, but many types would be very uninteresting as statements.
...
... Nat is not an interesting statement because it is too easy to prove.
How can Nat be proved?
Pick a number, any number.
Okay, 15.
Good job. You have a proof.

According to this, Nat is a statement, even though it's "uninteresting". However, in English "natural number" not an uninteresting statement; it's not a statement at all.

I wondered whether one should interpret Nat in Friedman and Christiansen's discussion as existentially quantified, i.e. as $\exists x : \mbox{Nat}(x)$. That would make sense of the fact that 15 is supposed to be a proof of Nat. But it's not clear why that is the correct interpretation.

$\endgroup$
3
  • 1
    $\begingroup$ Basically the truth value of a type is whether that type is inhabited, so your existential is the right idea. There are some type theories which go full Curry-Howard and don’t not even have Prop at all. Then you would represent logic with type operations like Prod. But in type theories with Prop, note it isn’t always the case that the Prop version of a statement and the Type version are the same. Depending on the type theory there are subtle but important differences. $\endgroup$
    – Jason Rute
    Mar 30 at 22:29
  • 1
    $\begingroup$ For example, a two element type like Unit+ Unit translates logically to something like the statement “True and True”. If you are working in a type theory with proof irrelevance, then “True and True” has one proof, while Unit+ Unit has two distinct elements. Also if propositional extensionality holds then “True” is equal to “True and True”, but you never want Unit to be equal to Unit + Unit. $\endgroup$
    – Jason Rute
    Mar 30 at 22:36
  • 1
    $\begingroup$ In my comment above I meant to say “True or True”, not “True and True”. 🤦‍♂️ $\endgroup$
    – Jason Rute
    Mar 31 at 11:59

2 Answers 2

6
$\begingroup$

To make the basics clear: languages don't mean anything before you assign them meanings manually, and you can interpret the same language different ways. So if you want to interpret a dependent type theory purely as a programming language, there are no "statements", only programs and their types.

Two other interpretations are relevant here. The "Propositions = Types" one, and the "Propositions ⊆ Types" one. ("Proposition" is synonymous with "logical statement" in your question, which may be confusing because some people use that word for "a proven logical statement". We don't do that here.)

Under the first interpretation, Nat is equivalent to the true proposition, so it indeed is not very interesting. Your last expression $\exists x. \operatorname{Nat}(x)$ doesn't quite make sense, because every variable here has a type, and you can't assume some untyped mysterious object, and later decide what the type is. However, you can say $\exists (x : \textrm{Nat}). \textrm{True}$, which is isomorphic (under the "Propositions = Types" reading) to $\textrm{Nat}$, because $\textrm{True}$ has exactly one proof, so it doesn't add any new information. And indeed, the Little Typer is completely serious here: $\textrm{Nat}$ can be read as the proposition "there exists a natural number such that $\textrm{True}$ is true (which is a trivial condition and can be removed)" this way.

However, under the second reading, Nat is not a proposition. Only some types are propositions: namely the ones where there are at most one element. This is quite natural: suppose $f$ is the map from even numbers to integers, and $f(p) = f(q)$, it definitely should be true that $p = q$. If we define the type of even numbers as an integer together with an element of $\textrm{isEven}(n)$, then this means any two elements of $\textrm{isEven}(n)$ has to be equal, otherwise we could have the same $n$ equipped with two different proofs, giving use two different even numbers, which is absurd. Since Nat has at least two different elements (you can see a proof in the Little Typer later in the book), we conclude that it cannot be interpreted as a proposition under this reading.

Ultimately, you choose between these interpretations as you see fit. Different interpretations may give different insights in different situations. I hope this sorts things up a bit.

$\endgroup$
4
  • $\begingroup$ Thanks very much Trebor! Very interesting and helpful, though I'm still digesting the first paragraph. I was not aware of the points in the second paragraph. I suppose that on that interpretation, every proof of a mathematical theorem is considered the same proof. Maybe further questions later. $\endgroup$
    – Mars
    Mar 31 at 17:36
  • $\begingroup$ Thanks again Trebor. I remain a bit surprised about the claim that propositions have exactly one proof. Of course in math itself, there are often structurally different proofs of the same proposition. I'm not sure I've seen different proofs in a dependently typed language--I think I have but I'm not finding examples at the moment. However, in general algorithmically different programs can compute the same function. So the claim that propositions can have at most one proof sounds strange to me. I assume that there is a specific sense of equality that is the basis of the claim. $\endgroup$
    – Mars
    Apr 11 at 4:02
  • $\begingroup$ @Mars It's not supposed to be claiming anything. It's one of the valid interpretations. Also, algorithmically different programs are counted as equal if you assume function extensionality is true — this is a theorem in ZFC, extensional type theory, book HoTT and cubical Agda. $\endgroup$
    – Trebor
    Apr 11 at 4:06
  • $\begingroup$ Thanks Trebor. I take the point to be that propositions as types have at most one element when is equality understood as extensional equality, so that any function that maps the same things to the same things counts as the same function, whatever algorithm is used. That makes sense. Then different proofs might look like different proofs in some intuitive sense, but they compute the same function, so they are the same. Great--thanks! $\endgroup$
    – Mars
    Apr 11 at 14:05
4
$\begingroup$

You can look at the ways to define types as ways to define propositions.

One simple definition of Nat is its Boehm-Berarducci encoding: forall p : Type. (p -> p) -> p -> p. That's a proposition expressible in any practical higher-order logic. It just didn't have a name before because it's an obvious tautology. Knowing that, Nat -> Nat as a proposition is no more informative than True -> True.

The other typical definition of Nat is as an inductive type (aka. algebraic data type). Inductive propositions are also a perfectly sensible concept in any higher-order logic. Nat is the smallest proposition, with respect to the ordering by implication, satisfying the rules:

  • Nat is true
  • if Nat is true, then Nat is true

Again, wholly uninteresting if you only care about truth values. (Inductive propositions are more useful when they are indexed, e.g., defining evenness and oddness mutually recursively.) (Those two definitions Nat are essentially the same for those familiar with encoding of inductive types in System F/MLTT, but I still listed both in the hope that others may find either one especially illuminating.)

Digression

That question is natural to ask, but I think it comes from a too naive idea of what kind of insights the Curry-Howard correspondence teaches us. So I'm going on a tangent to explain my own perspective.

If the above seems like a disappointing answer, perhaps we should reexamine the question and the implied expectation, that since propositions are types, perhaps interesting types are interesting propositions. "Interesting" depends on the usage. A formal logic is a tool. A lambda calculus is a tool. Even if they are actually the same tool at their core, their usages may remain distinct. Is brushing your teeth the same as painting with a brush?

The Curry-Howard correspondence connects formal logic with lambda calculus. One key observation that gives depth to the correspondence is that beta reduction corresponds to cut-elimination. But only logicians (who study the formal logic) care about cut-elimination. For a user of a proof assistant who's just trying to formalize standard mathematics, the "computational content" of proofs is quite an alien concept. Thus, a significant component of the Curry-Howard correspondence is conceptually out of reach.

I think that the Curry-Howard correspondence cannot really be made sense of as an "isomorphism" without a lot of technical baggage (whatever is needed to explain "cut-elimination") which is largely irrelevant to writing formal proofs. On the contrary, from the point of view of a proof assistant user who's translating conventional "informal" mathematics into "formal" type theory, I would rather acknowledge an asymmetry between what an "informal" logical statement expresses and what a "formal" type in type theory expresses.

Since there are interesting types that are not interesting propositions (like Nat), there is a sense in which types are more general than propositions. Indeed, types play more than one role in logic: as propositions, and as "data types", meaning "collections of objects that we can talk about". Accordingly, a classical formalization of logic would stratify its language in multiple levels: a syntax of propositions, which contains a syntax of terms which denote objects (for example, "y = 42x" is a proposition containing the terms "y" and "42x" which denote numbers), next to a syntax of proofs. But terms, propositions, and proofs can also be seen as merely different kinds of "constructions", and that's how we may arrive---through dependent types---to a unified calculus of constructions.

$\endgroup$
1
  • $\begingroup$ Thanks Li-yao Xia! The point about the Boehm-Berarducci encoding (which I didn't know about but looked up) is interesting. Still thinking about the second part of the answer. $\endgroup$
    – Mars
    Mar 31 at 18:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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