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: “”, because “” 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 “”, 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 (), element of ().

But the most important relation of all is probably equality. We could write equality in function notation: , but everyone writes it in infix notation, 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: 

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: . 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  of any type  is equal to itself. That is, the following type is inhabited:

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: “”? My short advice: whenever possible, use judgmental equality, , otherwise use propositional equality, . That’s because judgmental equality is a stronger statement. It means the symbols on the two sides of  are completely interchangeable. In fact, “” directly implies “”. Proof:  is true by definition; now replace one of the ’s with  (we can do this because we have , which implies complete substitutability) now we have .

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  is true (where  is some predicate/property with ) and  is true, then  is also true. This is guaranteed by the following type’s inhabitedness:

(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  came with projection functions.) The type implies that if , then  can be substituted for  in any proposition that we can express in our type system. If  stands for the proposition that  is an even number, then if  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  where  is arbitrary, and plug this into the induction principle from above:

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

As another example, say that  and  are any two types, and let’s say that  is the relation that holds true iff there is a function from  to .[2] Then  obviously holds for any  because of the identify function . Now, if , replace the second  with . We get: . 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:

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  and  but also, for example, the type  which contains one function: , and the type  which contains a single pair: . And in terms of types with zero elements, there is  but also, for example, .

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 ” 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 , 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 -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  will work correctly with propositions-as-subsingleton-types, we can define a predicate that tells us whether a given type  is a subsingleton, based on the definition of equality that we conveniently just learned about: 

Meaning that  is inhabited if all elements of  are equal to each other. If  is the empty type, this is vacuously true, i.e.,  will just be our good friend, the empty function. If  contains just one element, , then  is of course inhabited as well; namely by an element of the type “” which, by the definition of equality, is inhabited for any . 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 “” 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  and “” to encode  and , 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  and  are subsingleton types. Is  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  and  have a single element (but we’ll revisit this question later when we talk about function extensionality). Conversely, if  is , then  can only contain the empty function which is also unique. And if  is  while  is not, then  has no elements at all, which is also fine for a subsingleton type.

How about ? Here, we can also be certain that there can be at most one element; namely  if both types have an element: , and zero elements otherwise.

Now, let’s say we have a predicate, , such that  is a subsingleton type for any . Then is 

a subsingleton as well? An element of this type can only exist if there is anything to map the ’s to. So, it requires that all the  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  to a single value, which allows us to conclude that if all the ’s are singletons, then  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: 

And this is easy to prove here for two functions . We’ll just invoke the fact that for all , we have  (by the assumption that  is a singleton). Thus,  for all .

We now turn our attention to  and it’s pretty clear that there is a problem here. If both  and  have an element (say,  and  respectively), then  will have two elements:  and . Similarly, if for  there is more than one  for which  has an element (say,  and  and ), then  will have more than one element; in this case  and .

But, as I said before, this is good news! We don’t need  and  anyway, because we already have  and .

The last one to investigate is negation, , which we encoded as . This is entirely unproblematic because the type  is a subsingleton for any type , 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 , we have 

if we already know that  is a subsingleton. Do we know that  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, , then we’re again in the position to prove anything, including , via the principle of explosion. So either way, we may conclude that  is a subsingleton.

By the way, the fact that that the type  is a subsingleton for any type  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 LogicType Theory
 (true)
 (false)

Additionally, we’ll assume the following axiom: 

That is, if  is a proposition (actually, a subsingleton) and we have a double-negated version of , then we may conclude . As you can see, DNE as defined above is a type; assuming DNE as an axiom means assuming it has exactly one element. We can call that element  (it’s sometimes useful for proofs). The subscript “” is there to distinguish it from the more general DNE that holds for all types; the “” stems from the other name for subsingletons: -types.

Encoding implication

Previously, we’ve used the function type  to encode  (“ implies ”), but in classical logic, implication is usually not a fundamental operator; rather, it’s defined via “” and “”, or, if you only have “” and “”, you can define “” as , which is “” when encoded as a type. However, it turns out that the type “” is logically equivalent to this.

(“Logically equivalent” here means that one type is inhabited if and only if the other type is inhabited.)

Let’s quickly prove this! We will again explicitly construct the witnesses.

Say, we have a function , and the function  that we want to construct takes a pair  as input, then we can define: 

This proves one direction of the equivalence because we were able to construct  from .

For the opposite direction, we are given a function  of the above type, and and want to construct a function  which takes a  as input. First, we’ll construct a helper function  (which will be used inside , so we can assume we have ): 

where  is of type  as before. Now, through double-negation elimination, we can turn  into an element of , which is exactly what we wanted to construct. If we use “” to denote the function that inhabits DNE, then we can define  as 

Thus, thanks to DNE, we were able to construct  from . So, “” and “” are logically equivalent under DNE and we can safely encode implication as .

Encoding disjunction

Another somewhat interesting question is what the types look like that you get when negating  and  in order to encode  and . That is, we know that we can get  from  in classical logic, but what does that look like as types?

Well, it turns out that if we use  and “” to encode , then the result is logically equivalent to , i.e., double-negated . We will prove that in a second, but let me first address a concern you might have here: if we have double-negated , doesn’t that mean we get  by our DNE axiom? No! Because  is not (in general) a subsingleton, so our DNE does not apply.

OK, let’s prove that 

(i.e., ) is logically equivalent to 

which would mean that we can encode the logical statement “” as . First we’ll prove the direction top to bottom. So, we are given  and the function  that we have to construct, takes  as the first argument. The solution is then: 

which proves we can get  from .

For the opposite direction, we are given , and the function  that we want to construct takes the pair  as an argument. We’ll again need a helper function  which is defined within  so we have access to  and  is defined by case analysis (aka pattern matching): 

With this, we can construct 

where  depends on  but I’m using loose notation so it’s not indicated.

So, we have proved that  and  are logically equivalent, and we didn’t even need DNE/LEM for it; this is just always true in type theory. We noted before that  is a subsingleton for any type , so one way to interpret this result is to say that the double negation turns a non-subsingleton type into a subsingleton while preserving the semantics of it. In other words:  had the problem that it might contain two elements, but  doesn’t have that problem but still sort of means the same thing (at least if we have DNE; though again, we can’t actually apply DNE here). So it seems double negation might be a general strategy for turning arbitrary types into subsingletons. This is in fact such a useful trick that it has its own notation: 

We always have  for any type , but we only have  if  is a subsingleton (provided we have assumed DNE). That is,  and  are equivalent for subsingletons in the presence of DNE.

We can show something similar for . We know that  is equivalent to  in classical logic. This identity can be used to derive that

can be used to encode . But this derivation is left as an exercise to the reader.

This means we can extend our translation table:

First-order LogicType Theory

This is now the final scheme; this is the correct way to encode classical first-order logic in type theory. It is fully compatible with DNE/LEM.

As a final note on this: if you look back at our proof that DNE implies LEM, you can see that we applied DNE to the following type: 

which you may think wasn’t allowed after all, because a union type is not a subsingleton. However, in this case, the inner union type is a subsingleton because the two halves of the union are mutually exclusive (at least if our whole theory is consistent), so this was valid. In general,  is equivalent to  if  and  are mutually exclusive.

At this point, we should verify that with the general rules of type theory, this encoding of first-order logic actually has all the rules of inference, like modus ponens, existential generalization and conjunction introduction. I won’t go through them here to prove them all, but if you’re interested, see this page.

The subuniverse of truth values

Now that we have set up logic, we will use the familiar logic symbols instead of , etc. So, when constructing propositions and functions that output truth values (like predicates and relations), we will use  and . The tables above define how these symbols get translated to the underlying operators on types. We can, for example, express LEM now as 

However, this is the version of LEM that applies to all types and not just subsingletons. The actual version we use is this

but wouldn’t it be nicer if we could quantify over the “subuniverse” of all subsingletons directly? This would be especially useful for specifying the type of predicate functions.

Until now we’ve always written the type of a predicate on  as , where  is a universe of types. However, the codomain is not actually all types in the universe; just the subsingletons.

We can define the subuniverse of all subsingletons through the following trick: 

Let’s think about what that means. Elements of this sum type are pairs where the first element is some type  and the second element is a witness  to the proposition . So, such a pair can only exist if the type representing the proposition is inhabited, meaning the proposition is true. Thus, the elements of  are exactly those types  which are subsingletons!

Technically, the elements of  are pairs of subsingletons and witnesses, , but we will usually pretend the elements are just the types. In any case, there is an obvious mapping from  to .

With this definition, the type of a predicate function on a base type  is . I called this subuniverse “” because it encompasses all truth values; that is, it encompasses all types that can encode falseness and truthiness.

However, with our current axioms, we can only define the type of all subsingletons for a particular universe . That is,  doesn’t give us all the “falsy” and “truthy” types out there but only the ones in universe . And this is a problem if we want to talk about power sets.

Power sets and propositional extensionality

The power set type  is of course the type of all “subsets” of some type . In our theory, subsets are actually predicates – functions from  to truth values – so the power set type is the function type . And here we see the problem. If this is supposed to be a real power set, then  better contain all “falsy” and “truthy” types. But it actually only contains those from universe !

If there were some “truthy” type  (i.e., a type with exactly one element) that’s not in  but we have a function  that maps some  to this type, , then this function  wouldn’t be captured by the function type , but it would still be a predicate, so “” wouldn’t actually encompass all predicates.

So, we need some way to get the type of all the possible truth values.

One radical solution to this problem is drastically reduce the space of truth values. After all, what we want in the end is a two-valued logic, so do we really need a distinction beyond “has no elements” and “has exactly one element”? What  contains is the empty type  and the unit type  and then an infinite number of types that are combinations of these: , … But the distinction between these types (beyond whether they’re “truthy” or “falsy”) carries basically no information. So, we might say, “let’s just declare all truthy types to be equal to each other and the same for all falsy types and be done with it”. This would correspond to the principle of propositional extensionality, and would be a solution to our problem, because then we knew that any subsingleton was either equal to  or  (which are both present in all universes).

We’ll talk about more propositional extensionality when talking about extensionality in general. But for now, let’s assume something a bit weaker (in order to be able to define power sets): There exists a type  together with an -indexed family of subsingletons (aka, a function  where all  are subsingletons) such that this family (the range of ) contains all subsingletons up to equality. Thus, the elements of  constitute an index for all falsy and truthy types. And as it is easy to turn an element of  into a truth value (via the function ), we can define the power set type to be

and this will be guaranteed to encompass all predicates on  because  indexes all “falsy” and “truthy” types.

The good news is that the existence of  follows from LEM and propositional extensionality (mentioned above). So, we won’t actually have to assume a new axiom for  if we adopt propositional extensionality (which I think we do want to but more on that later). A possible (and obvious) choice for  under LEM and propositional extensionality is in fact  – the type that has exactly two elements.

This is kind of funny because that means we have come full circle: in the beginning we decided against using  to represent truth values – instead using types that are either inhabited or not – but now we find out that what we ended up constructing is equivalent to using  for representing truth values (assuming LEM and propositional extensionality). Still, the concept of propositions-as-types allowed us to reuse all the type operators like  and  to construct first-order logic, so we didn’t have to separately define all these operators for our encoding of logic.

With propositional extensionality, we may thus define the power set type like this instead: 

which looks quite similar to how it works in set theory.

Now, you might wonder whether we need a new type forming rule/axiom for power sets analogous to the axiom of power set in ZF set theory. But we don’t, because our theory already has a type forming rule for function types and as we saw, we can express the power set type as a function type. It’s actually also true in set theory that you can get the existence of power sets from the existence of function sets (set of all functions from  to ), but it’s usually done the other way around when axiomatizing set theory.

(Another thing that worried me about this definition of power sets is that in practice I can only access those elements of  for which I can formulate a predicate function in the lambda calculus formalism, which surely doesn’t cover all possible mappings from  to , if  is infinite. However, the same problem actually also exists in set theory: in practice I can only access those elements of  for which I have a first-order logic formula proving that they are subsets of . Still, the meaning we give to  in set theory is that it really does contain all subsets, even if we can’t access all of them. We declare the same thing for function types in type theory.)

With the type , our version of logic actually looks more like second-order logic than first-order, because we can quantify over predicates too: 

In fact, we could also quantify over predicates of predicates (i.e., ) and so on; meaning it’s actually a higher-order logic. (Though, higher-order logic is of course not any more powerful than second-order logic.) One peculiar aspect of type theory is, however, that we don’t just have a single domain of discourse; instead, we have a lot of different types, and the quantifiers  and  only range over one type at a time. This is similar to many-sorted logics where quantifiers always range over only one “sort”. But I don’t know exactly how to compare the “strengths” of these formal systems. I assume they’re all about equally powerful? Type theory is in any case certainly sufficiently expressive to be affected by Gödel’s incompleteness theorems.


This concludes the third post in this series. Next time, we’ll talk about how to do set-like mathematics in type theory and we’ll discuss the axiom of choice.

  1. ^

    Two functions, that return exactly the same values for all inputs, might not be judgmentally equal. More on that later.

  2. ^

    We could express that simply as  will be inhabited if there is a function .

  3. ^

    This might seem like a somewhat strange definition, but the advantage is that this definition generalizes to 0-types, 1-types, and so on.

New to LessWrong?

New Comment