Classical logic based on propositions-as-subsingleton-types

This is the third part of a series on type theory. This time we’re developing real, classical logic in type theory. However, before we can get there, we have to talk about equality first; specifically, propositional equality, which is different from judgmental equality.

Equality

Up until now, we’ve always used this weird triple equality “” when defining stuff. This is judgmental equality, and, like type judgments, it is a “meta” operation; it can’t be used within propositions. The following unfortunately doesn’t make any sense: “ $(x \equiv y) \Rightarrow (2 x \equiv 2 y)$ ”, because “ $\equiv$ ” doesn’t return a truth value that our logic can do anything with. This is of course a problem.

Another problem is that, by default, judgmental equality is very strict – especially for functions!^[1] This is why we might want to expand the concept of equality and assume axioms that declare two things to be equal that weren’t equal before, but, again, we can’t do that with “ $\equiv$ ”, because we can’t use it in logic statements, so we can’t formulate axioms about it.

The solution is to define a new equality, which will be a relation defined wholly within our logic.

As you’ll recall, predicates are functions from values to truth values (i.e., true and false). Relations are the same, except that they expect more than one argument (usually two). Examples of relations are: less than ( $<$ ), greater than ( $>$ ), subset of ( $\subset$ ), element of ( $\in$ ).

But the most important relation of all is probably equality. We could write equality in function notation: $E q (x, y)$ , but everyone writes it in infix notation, $x = y$ , and so will we. But keep in mind that it’s actually a type-valued function with two arguments, even if we’re not writing it like that.

If we’re precise, equality is actually a generic function with respect to the type of its arguments. So, it needs to accept three arguments where the first argument is a type:

= : \prod T : U T \to T \to U .

Just from this type we can tell that only elements of the same type can be equal to each other. In infix notation, we indicate the type argument with a subscript: $x =_{T} y$ . However, we will often drop it if it’s clear from context. (Just like we can drop type annotations in functional programing languages if the compiler can infer them from context!)

Now, which things should be equal in our new equality? Type theorists have condensed the essence of equality and have come up with the following definition: for all elements $a$ of any type $A$ , $a$ is equal to itself. That is, the following type is inhabited:

\prod A : U \prod a : A (a = a) .

In other words: equality is reflexive. We can then take this as the starting point to prove that other things are equal to other things.

(You might wonder whether this definition will really make our new equality behave like equality should behave. To really convince you of that, we would probably need to consider other possible definitions and compare the results. But I won’t do that here, so you’ll have to take it on faith that this is a good definition.)

The big question is now, when to use this equality and when to use the one from before: “ $\equiv$ ”? My short advice: whenever possible, use judgmental equality, $\equiv$ , otherwise use propositional equality, $=$ . That’s because judgmental equality is a stronger statement. It means the symbols on the two sides of $\equiv$ are completely interchangeable. In fact, “ $x \equiv y$ ” directly implies “ $x = y$ ”. Proof: $x = x$ is true by definition; now replace one of the $x$ ’s with $y$ (we can do this because we have $x \equiv y$ , which implies complete substitutability) now we have $x = y$ .

However, this might not always be true in the other direction. So, whenever we define something, we use judgmental equality because why use a weaker equality when we can use a stronger one?

But we aren’t done yet with the definition of propositional equality. We already said that one essential characteristic of equality is that all values are equal to themselves. Another characteristic is a sort of “induction principle”: if two things are equal, then everything that’s true about one of them should also be true of the other.

More formally: if $ϕ (x)$ is true (where $ϕ$ is some predicate/property with $ϕ : A \to U$ ) and $x = y$ is true, then $ϕ (y)$ is also true. This is guaranteed by the following type’s inhabitedness:

\prod x, y : A (x =_{A} y) \to ϕ (x) \to ϕ (y) .

(The existence of this function is still part of the definition; it’s not a theorem. It’s just like how the binary product type $A \times B$ came with projection functions.) The type implies that if $x = y$ , then $y$ can be substituted for $x$ in any proposition that we can express in our type system. If $ϕ (n)$ stands for the proposition that $n$ is an even number, then if $n = m$ , $m$ is also an even number. Within our logic, we cannot distinguish between two elements that are propositionally equal (though they may still be distinguishable with judgmental equality).

We can use this principle to prove that equality is transitive: define $ϕ (x) \equiv (x =_{A} z)$ where $z$ is arbitrary, and plug this into the induction principle from above:

\prod z : A \prod x, y : A (x =_{A} y) \to (x =_{A} z) \to (y =_{A} z)

Meaning: if $x = y$ and $x = z$ , then we also have $y = z$ . More informally we could have argued: if $x = y$ and $y = z$ , then replace $y$ with $z$ in the first equality and we get $x = z$ . In a similar manner, we can easily prove that propositional equality is symmetric: start with $x = x$ , which is always true, then given $x = y$ , replace the first $x$ with $y$ .

As another example, say that $A$ and $B$ are any two types, and let’s say that $F (A, B)$ is the relation that holds true iff there is a function from $A$ to $B$ .^[2] Then $F (A, A)$ obviously holds for any $A$ because of the identify function ${i d}_{A}$ . Now, if $A = B$ , replace the second $A$ with $B$ . We get: $(A = B) \to F (A, B)$ . Thus, equality between two types asserts that there must be a function between them (in both directions actually).

So, this is our definition of (propositional) equality. It mostly behaves like you would expect it to: if two things are equal, they can’t be distinguished. However, this equality is a bit too strict for functions, which is why we’ll introduce the principle of function extensionality later on, but for now let’s just accept it as it is.

Subsingletons for truth values

As a reminder, our goal is now to assume DNE/LEM as an axiom in order to get classical logic:

L E M \equiv \prod A : U A + (A \to 0) .

However, for reasons that I myself don’t fully understand, we’ll get big problems if we just assume DNE/LEM for all types. But luckily, there is no problem if we assume DNE/LEM only for types that have either zero or exactly one element. This includes $0$ and $1$ but also, for example, the type $1 \to 1$ which contains one function: $λ x . x$ , and the type $1 \times 1$ which contains a single pair: $(⋆, ⋆)$ . And in terms of types with zero elements, there is $0 \times 0$ but also, for example, $0 \times 1$ .

However, if we only assume DNE/LEM for these types, then all of our logic must only produce types with either zero or exactly one element, otherwise we will get propositions for which DNE/LEM doesn’t hold! This means we’ll have to check whether we can make our predicates and logic operators work with this restricted collection of types. That’s what we’ll do in a second, but let’s take another look at the big picture first.

With hindsight, we can see that when we went from “a proposition-as-type is true if it is the type $1$ ” to “a proposition-as-type is true if it is inhabited at all” in the previous article, we went too far. In order to get to classical logic, we should have said “a proposition-as-type is true if it is basically like $1$ , i.e., it contains exactly one element”. Indeed, we will see that this new idea will work out splendidly.

Types with either zero or exactly one element are sometimes called $(- 1)$ -types, but this is a terrible name, so we’ll call them subsingletons instead, which is actually a term from set theory, but it describes the concept well. (The name comes from the fact that sets with one element are called singletons, but we’re also allowing sets with fewer elements than that, so it’s a sub-singleton.) If we ignore for the moment the question of whether the operator $\prod$ will work correctly with propositions-as-subsingleton-types, we can define a predicate that tells us whether a given type $A$ is a subsingleton, based on the definition of equality that we conveniently just learned about:

\begin{matrix} i s T r u t h V a l : U \to U i s T r u t h V a l (A) :\equiv \prod x : A \prod y : A (x =_{A} y) . \end{matrix}

Meaning that $i s T r u t h V a l (A)$ is inhabited if all elements of $A$ are equal to each other. If $A$ is the empty type, this is vacuously true, i.e., $Π_{x : A} Π_{y : A} (x = y)$ will just be our good friend, the empty function. If $A$ contains just one element, $a$ , then $i s T r u t h V a l (A)$ is of course inhabited as well; namely by an element of the type “ $a = a$ ” which, by the definition of equality, is inhabited for any $a$ . We will take the above definition as the official definition of a subsingleton: that all its elements are equal to each other.^[3]

I called the above predicate “ $i s T r u t h V a l$ ” because we will be using subsingletons to represent truth values, as mentioned before. Classical logic is a two-valued logic, which means the truth values are true (also denoted by ⊤), and false (denoted ⊥). And so we use subsingletons to encode these truth values: if the type has no elements, it corresponds to $⊥$ , and if it has a single element, it corresponds to $⊤$ . Note in particular that any type with exactly one element can represent $⊤$ and any type with zero elements can represent $⊥$ .

But now we have to address the important question of whether we can still use $\prod$ , $\sum$ , $\times$ , $+$ and “ $\to 0$ ” to encode $\forall$ , $\exists$ , $\land$ , $\lor$ and $\neg$ , when working with propositions as subsingleton types (so that we can safely apply DNE/LEM to all propositions). We’ll need to make sure that the operations we use will result in subsingleton types if they’re getting subsingleton types as inputs.

Operations on subsingletons

Say that $P$ and $Q$ are subsingleton types. Is $P \to Q$ one as well then? Well, it kind of makes sense that there is only one way to map one element to one element. So we’ll assume for the moment that this checks out if both $P$ and $Q$ have a single element (but we’ll revisit this question later when we talk about function extensionality). Conversely, if $P$ is $0$ , then $P \to Q$ can only contain the empty function which is also unique. And if $Q$ is $0$ while $P$ is not, then $P \to Q$ has no elements at all, which is also fine for a subsingleton type.

How about $P \times Q$ ? Here, we can also be certain that there can be at most one element; namely $(p, q)$ if both types have an element: $p : P$ , $q : Q$ , and zero elements otherwise.

Now, let’s say we have a predicate, $ϕ$ , such that $ϕ (x)$ is a subsingleton type for any $x : X$ . Then is

\prod x : X ϕ (x)

a subsingleton as well? An element of this type can only exist if there is anything to map the $x$ ’s to. So, it requires that all the $ϕ (x)$ are inhabited types (and by assumption, they can at most have a single element). Furthermore, it makes intuitive sense that there is only one way to map a given $x$ to a single value, which allows us to conclude that if all the $ϕ (x)$ ’s are singletons, then $Π_{x : X} ϕ (x)$ is a singleton as well. As I keep mentioning, we will revisit equality of functions later and make it rigorous, but for now let’s just use the intuitive notion where two functions are equal if all their outputs are equal, so:

\prod x : X (g (x) = f (x))

And this is easy to prove here for two functions $g, f : Π_{x : X} ϕ (x)$ . We’ll just invoke the fact that for all $p, q : ϕ (x)$ , we have $p = q$ (by the assumption that $ϕ (x)$ is a singleton). Thus, $g (x) = f (x)$ for all $x$ .

We now turn our attention to $P + Q$ and it’s pretty clear that there is a problem here. If both $P$ and $Q$ have an element (say, $p$ and $q$ respectively), then $P + Q$ will have two elements: $l e f t (p)$ and $r i g h t (q)$ . Similarly, if for $ϕ (x)$ there is more than one $x$ for which $ϕ (x)$ has an element (say, $y$ and $z : X$ and $ϕ (y) \equiv ϕ (z) \equiv 1$ ), then $\sum_{x : X} ϕ (x)$ will have more than one element; in this case $(y, ⋆)$ and $(z, ⋆)$ .

But, as I said before, this is good news! We don’t need $\lor$ and $\exists$ anyway, because we already have $\land$ , $\forall$ and $\neg$ .

The last one to investigate is negation, $\neg P$ , which we encoded as $P \to 0$ . This is entirely unproblematic because the type $P \to 0$ is a subsingleton for any type $P$ , not just subsingletons. This is because the only element this type can ever contain is the empty function. If we again use the intuitive notion of function equality, then it’s easy to show that for $g, f : P \to 0$ , we have

\prod p : P (g (p) = f (p))

if we already know that $0$ is a subsingleton. Do we know that $0$ is a subsingleton? Well, on the one hand, there are no elements, so we can make the vacuously-true argument mentioned before. On the other hand, if we assume we have two elements, $x, y : 0$ , then we’re again in the position to prove anything, including $x = y$ , via the principle of explosion. So either way, we may conclude that $0$ is a subsingleton.

By the way, the fact that that the type $A \to 0$ is a subsingleton for any type $A$ is somewhat intriguing… let’s put a pin in that; it might become relevant later!

And that’s all we need in order to encode classical logic in type theory:

First-order Logic	Type Theory
$\forall (x : X) . ϕ (x)$	$\prod_{x : X} ϕ (x)$
$P \land Q$

LESSWRONG
LW

LESSWRONG
LW

5

Classical logic based on propositions-as-subsingleton-types

5

5

Equality

Subsingletons for truth values

Operations on subsingletons