# 12

This is the second entry in my series on type theory. In this post, we will talk about how to recreate logic in type theory.

As you might know, in order to define ZFC set theory, you first define first-order (FO) logic separately, and then specify the ZFC axioms in the language of FO logic. But we want to be more ambitious here! We want to encode FO logic with the type concepts we already have! If that doesn’t make any sense right now, I hope at the end of this article it does.

But before we get there, a quick refresher on type-valued functions.

## Type-valued functions

In the definition of sum types, we briefly mentioned that  is a type-valued function:

We can of course precisely specify ’s type:

What is maybe surprising about this is that an instance of a type, like the function , becomes part of a type. But this is how it works in type theory. In fact, we could have written the type of all groups a little differently:

The function  here doesn’t only return a type; it also takes a type as input! A function on types can use the operators , and , and can get quite complicated. And, given any function  with codomain  (and arbitrary domain ), the following is a type: , namely, the disjoint union over all types in the image of .

## What to use for truth values?

OK, why do I mention all this? Because it will be relevant to how we will represent truth values (booleans in programming languages) in our encoding of logic.

The truth values in first-order logic are, shockingly, true and false. Propositions are statements that have a truth value – they're either true or false. (So, boolean variables/expressions in a programming language.)

And as mentioned in the beginning, we can talk about subsets of, say,  by talking about predicate functions (or just predicates) on . A predicate function is a function that takes a single argument and returns a truth value – true or false.

So, you see, truth values are needed everywhere. How to represent them?

Our first naïve approach might perhaps be to represent “true” and “false” with the values of the type , which is the type that has exactly two elements. Let’s call them  and  (distinct from  and ). So, let’s say  represents “false” and  represents “true”.

A predicate function  on the natural numbers would then have the type:

So, if  represents some property we care about, like whether a number is even, and we want to prove that the number 6 is even, then what we want to show at the end is

However, doing it like this doesn’t really play to the strengths of type theory. We would have to manually define all the logic operations on , which isn’t really better than how it’s done in set theory. We would like to re-use our type constructs in the encoding of logic.

So, what will we do instead?

## Types for truth values

We will not use two values for “true” and “false”, but two types! Of course! Specifically, the empty type and the unit type.

The empty type has, as the name suggests, no elements at all. It can be represented by  (a bold zero) or by . In a computer program, this could be seen as the return type of a function that crashes and never returns at all. In some programming languages, this type is called “Never”. (Note that this is different from the “nil” or “None” types in programming languages; those correspond to the unit type which we’ll talk about below.) The defining quality of the empty type is that for any other type , there exists a unique function mapping from  to

And this function is the “empty function” – there is no  after all. The empty function is quite weird, but unfortunately we will encounter it quite a lot. It just maps nothing to nothing. If you think of a function as a list of input-output pairs, then the empty function is a list with zero elements.

The unit type has exactly one element (I mentioned it once before) and is written  (a bold one) or . The one element that is in  is written as “” or “()”; the latter is meant to be a tuple without any entries.[1] We will use “” because we have enough parentheses as it is. The unit type has the property that for any other type , there exists a unique function from  to  (so exactly the opposite of the property of the empty type).[2] That function is the constant function which returns  for all inputs, . We won’t make much use of this property though.

A predicate is then a type-valued function (hence the refresher!) on some domain

More specifically, a predicate function returns either  or . Note: mapping to either  or  is very different from mapping to an element of either  or ; after all,  doesn’t have any elements.

And if  is again the predicate for even numbers, then we’ll have, for example, . Now, this might look suspiciously similar to our “naïve” solution based on , so what is the advantage? To unlock those advantages, we’ll note that we can express  also as  , because if  is an element of the type , then  must be the unit type!

So, if  is some proposition, then we will encode the logic statement

as

in our type theory, where the proposition  is a type-valued expression. This concept is known as propositions-as-types. If  is not well-typed, then  should be interpreted as a false statement.

At this point, I’ll remind you that the point of a logic system is to make truth-preserving transformations. So, if we represent truth with the fact that  is a member of the type that represents the proposition, then all our inference steps need to preserve that property or our logic system is useless. We will show in the following that we can make our logic truth-preserving.

I can understand if this feels a bit mind-bending right now. But I hope that you will see shortly that this all makes sense and isn’t a terrible idea. In fact, it will be rather elegant.

## Existential quantifier

Now that we have decided how to represent true and false propositions in our theory, we would also like to use the other parts of first-order logic, like existential quantification. Can we again do something really clever with types here?

Let’s see… Say that  is a predicate on the natural numbers with type . It might represent evenness as before. As  is a type-valued function, we can construct a sum type from it:

Now, what does it mean if there exists some pair  such that the above is well-typed? Or in other words: what does it mean if the above sum type is inhabited? (We say that a type is inhabited if it has at least one element.)

As you’ll recall, the elements of sum types are pairs. In this case, the first element of the pair is a natural number , and the second element is an element of either  or , depending on whether  is  or . However…  doesn’t have any elements! So actually, all elements of  must have  as the type of the second entry of the pair. In other word, a pair of type  can only exist for those , where . For those , the pair is given by , where the second entry is .

So, if I can find some  such that

is well-typed, then this must mean that there exists an  such that  is well-typed, or equivalently, there exists an  such that  is inhabited.

It’s worth repeating again: if the type  is inhabited, then there exists an  such that  is inhabited. So, in a way, the  operator is acting like an existential quantifier: .

However, to really make this work, we’ll have to change our definition of truth a bit.

If we say, “as long as a type is inhabited at all, it represents a true proposition,” then the step from  to  is truth-preserving. Because if  is true (i.e., is inhabited) for some , then  is also true (inhabited). We have successfully reasoned that if I have a concrete  with property , then I can conclude that there exists an element in  for which  holds. This rule is known as existential introduction in first-order logic.

So, in the propositions-as-types system, the sum type operator  acts like the existential quantifier. This has been our first step towards encoding all of first-order logic as operations on types in type theory. But don’t be alarmed – when we actually write down propositions later, we will not transcribe them as types every time. Rather, it’s sufficient to know that we could always do that, and that everything we’re doing is well-defined.

As mentioned, we have to tweak our definition of truth a bit, because the members of  actually look like  and not just . The new definition will just check for inhabitedness.

So,

gets encoded as

where  is again a type. The members of  are sometimes called the witnesses for the proposition’s truth.[3]

So, if we encode this first-order-logic statement:

in type theory, we get

Great!

## Universal quantifier

Let’s do the universal quantifier, , next. In order to figure this out, it helps to think about what object would be proof enough that  holds for all elements in . One such object is a (total) function that maps each  to an element in , because for a (total) function like that to exist, the types  for all  must have at least one element, right? You can’t map a value to an empty type! That is, if there is even one  such that , then no function from  to  can exist. So, the existence of the function is sufficient proof that all  are inhabited.

What is the type of such a witness function? We know that function types are written , but that assumes that the return type is the same for all . What we need instead, is a function type where the return type varies with the input value:

This is called a dependent function type. It’s a bit of a strange type – most programming languages don’t have an equivalent to this, though some very fancy functional programming languages do. It’s usually not that useful, but it is very useful to encode a universal quantifier: .

One way to think about dependent function types is as a generalization of tuples. For example, take the following tuple type: . Given an index type that has three elements, , we can also realize this with a dependent function type. We need a type-valued function  that is defined like this:

With this, an element of  is equivalent to a 3-tuple.

Another way to see dependent function types is as functions that return a union, except that the type is specified more precisely. We previously discussed the example of the division function on the rational numbers, which returned the special value  for division by zero. But instead of saying that the return type is , we can be more precise! We could specify a dependent return type, which is  for all inputs except where the second argument is 0. So, if

then this is a more precise type for

However, more realistically, you would probably just restrict the type of the second argument to be .

A more common use case is “generic” functions. The truth is, we already used a dependent function type once before – in the type of the generic identity function:

If we define , then the above type can be written as . So, this was actually a dependent function all along.

Anyway, we now know that this first-order logic statement:

can be encoded as

## Complete first-order logic

Now we only have  and  left. The first two will be very easy, the last one will be trouble. So, let’s start with the easy ones. Say that types  and  may or may not be inhabited, what new type could we construct that will be inhabited if and only if both are inhabited? Well, a pair (aka 2-tuple) of course! You can only form a pair out of elements from  and  if both have elements. So, the logic statement  will be encoded as .

If you take a moment to think about logical or, it should be pretty clear that we can encode  as .

Finally, negation: . If I have a type  that may or may not be inhabited, what new type could we construct that will be inhabited exactly when  is not inhabited and vice versa? The trick that we’ll use for this is that if  is uninhabited, then we can still use it as the domain for the empty function. The empty function maps from  to any type , and… does just absolutely nothing, as we discussed. So, if  is uninhabited, then  is still inhabited by the empty function for any type .

However, if  is actually inhabited, then  could still have an element – namely just a normal function that maps  to some element of .  So we can’t use  to represent “” because it doesn’t fulfill the requirement that “” be inhabited if and only if  is not inhabited.

But we can fix this by using  as the codomain: . If , this has an element (the empty function), but if there exists , then this can’t have an element because what are you going to map this  to?

So, we encode  as . Where is the promised trouble? The trouble is that with this encoding,  does not imply . To be clear, it works in the other direction: if I have a , then I know that  is uninhabited, and so this is inhabited:

(by the empty function). This means that  implies . However, when we try to prove the opposite direction, we run into the problem that we can’t produce an element of  out of nothing – there is just no rule that allows us to construct an element of  out of, essentially, the empty function.

At this point, we must realize the shocking truth, that what we have constructed here is not classical first-order logic, but intuitionistic logic! (Also called constructive logic as it’s used for constructive mathematics.) In intuitionistic logic, proof by contradiction does not work in general and, more pertinently, double-negation elimination is not a thing.

What should have tipped us off from the beginning was that we used two different operators,  and , to encode  and , because in classical logic, you only need one of them and the other is just the negation of the first. In intuitionistic logic, on the other hand,  and  are different operators that can’t be defined in terms of each other. For example, in intuitionistic logic, the following does not hold:

The intuitive argument for why this does not hold is that you need to construct a concrete  for which , but there is no way to do that from just knowing .

Intuitionistic logic has its charms, but it would be nice to be able to use classical logic as well. In order to do that, we will simply assume double-negation elimination as an axiom! As it turns out, such an axiom causes problems with the encoding of  and  as  and , but this is a good sign! Because those are not actually needed to define classical logic. It suffices if we have , and .

It might seem a bit unsatisfactory that we have to assume an additional axiom in order to get classical logic, but on the other hand, it’s remarkable that we got even this far without assuming anything specific to logic. Also, we will later see that double-negation elimination follows from the axiom of choice, which we probably want to assume anyway, so this isn’t so bad.

Which is interesting: in a deep way, it is the axiom of choice which allows us to do classical logic.

Anyway, before we define the axiom, let’s introduce some simplified notation.

## Function types revisited

At this point I should come clean and admit that type theorists don’t actually write their function types like this: . If the codomain is a constant type, and not a type-valued function, then function types are usually written in this simplified notation:

So, a function from  to  can be written as . However, if it’s a dependent function, you still have to write its type as .

(It’s actually interesting that “” with the colon is a common notation even outside of type theory because if you use set theory as your foundation, then I think this should actually be “”, but I guess in set theory you’re not supposed to read “” as a set with elements, like we do in type theory where  is just a shorthand for .)

With this simplified notation, we can write the negation of  as . And the type of the generic identity function is this:

Note that for the first argument (the type parameter) we still need the standard notation, because the other types depend on the value of that first argument.

Functions that have multiple arguments and use currying, are written like this:

However, we usually leave out the parentheses if their scope extends to the end of the expression:

As the arrow notation may already suggest, we can encode logical implication as a function type. If a function  exists, and  is inhabited by, say, , then we can simply apply the function, , to get an element of  and conclude that  is inhabited as well. Conversely, if we have , but  is not inhabited, then we can’t conclude anything about  from this (except that  must be the empty function). So,  behaves exactly like logical implication does.

## Law of excluded middle

Our goal was to recreate classical first-order logic within type theory. The main problem was that double-negation elimination (abbreviated DNE) didn’t hold. The idea was then to assume DNE as an axiom; i.e., to assume that the following type is inhabited

Before we do that, we’ll note that, given all the other constructions we already have, DNE is equivalent to the law of excluded middle (abbreviated LEM):

LEM says: for any proposition , we have either  or .

In order to better get to know DNE and LEM, let’s verify that they are indeed equivalent in our logic system. Going from LEM to DNE is easier, so let’s do that first.

(The proof will showcase how constructive mathematics works in type theory. In order to prove a proposition, we’ll have to explicitly construct an element of the corresponding type! This style of reasoning certainly takes some getting used to.)

So, we are given a function of type LEM, which, for any type , gives us an element . We want to construct a function of type DNE, that maps the function  to an element of .

Given , an element of a union type, we can do a case analysis. If  corresponds to an element of , we’re already done: that’s what we wanted.

If  corresponds to an element of , then we can map this with  to an element of . Getting an element of  is always exciting, because as I mentioned when introducing the empty type, there is a function  for any type , which means there is also one for ; call it . So, if we have an element of , we can also get an element of . Of course, (assuming our theory is consistent) there are no elements of , so (again assuming our theory is consistent) there can be no element of  which we could then map to  with , so the element of  must have been an element of  all along. But in any case, we have conclusively demonstrated that we can construct an element of , given  and . Thus, LEM implies DNE.

The fact that we can get anything from an element of  corresponds to the principle of explosion in classical logic.

The opposite direction – from DNE to LEM – is slightly trickier, but it’s also a short proof. First, we’ll have to convince ourselves that, regardless of DNE, for any type , a function of the following type exists:

So, it’s a function that takes in another function – let’s call it  – and maps that to the empty type,  in turn is a function mapping an element from  to . Why do we want this function ? Because if we had this, then by DNE (double-negation elimination), we would have an element of , which is exactly what LEM says exists. So, let’s explicitly construct ! We know that it gets  as input:

So, we will probably want to call  at some point. However, for that we need an element of . We won’t be able to just construct an element of , but  seems potentially doable. In fact, can’t we use  itself to construct an element of ? Yes, we can!

As a reminder,  allows us to construct an element of  from a . Great, now we’ll just pass this function to  and we’ll have it:

So, we managed to construct  for an arbitrary type , which means that the double-negated version of LEM is already always inhabited in our theory. Now we just apply DNE to it and get the regular LEM.

This concludes our first proof in constructive mathematics; I hope it wasn’t too bad!

To construct classical logic we can now just assume either DNE or LEM, right? Unfortunately, there is one last slight complication, which we will discuss in the next post!

To summarize what we have learned: we can use types as truth values, which then allows us to re-use , ... as , ... However, this only gives us intuitionstic logic, so we’ll need to assume an axiom in order to get classical logic.

1. ^

Haskell, for example, writes the single element of the unit type as (). However, the unit type itself is also written as (), so () :: () in Haskell.

2. ^

For the category theorists: if we view types as objects in a category, then this means that the empty type is an initial object and the unit type is a terminal object.

3. ^

Or, more old-fashioned, they’re called the proofs of the proposition, which is why we use the letter  to represent them.

New Comment