Classical logic based on propositions-as-subsingleton-types

(Part of the series Introduction to dependent type theory.)

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 “$\equiv$” 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(2x\equiv 2y)$”, 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: $\mathsf{Eq}(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:\mathcal{U}}T\to T\to\mathcal{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:\mathcal{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 substitute one of the $x$’s with $y$ (we can do this because we have $x\equiv y$, which implies substitutability) now we have $x=y$.

However, this is usually not 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 $\phi(x)$ is true (where $\phi$ is some predicate/property) and $x=y$ is true, then $\phi(y)$ is also true. This is guaranteed by the following type’s inhabitedness:

$$\prod_{x,y:A}(x=_A y)\to \phi(x)\to \phi(y)~.$$

(This is still part of the definition; it’s not a theorem.) It means that if we have proved property $\phi$ for $x$, then all elements that are equal to $x$ also have this property (without further proof). So, if $\phi(n)$ is the predicate that tests whether $n$ is an even number, then if $n=m$ and $n$ is even, then $m$ is also even.

But we can do more! If $R$ is a relation on $A$, and $R$ is reflexive, then $R(x,y)$ holds for all $x,y:A$ where $x=y$. The corresponding type is this:

$$\prod_{R:\Pi_{x,y:A}(x=_Ay)\to\mathcal{U}} \left(\prod_{x:A}R(x, x)\right)\to\prod_{x,y:A}(x=_Ay)\to R(x, y)$$

where $\prod_{x:A}R(x,x)$ is the type corresponding to the proposition of reflexivity. It says that $R$ relates every element to itself. As a somewhat trivial example, “$\leq$” is reflexive, so whenever we have $x=y$, we also have $x\leq y$.

So, this is our definition of (propositional) equality. It mostly behaves like you would expect it to. However, it 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:

$$\mathrm{LEM}\equiv\prod_{A:\mathcal{U}} A+(A\to\mathbf{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 $\mathbf{0}$ and $\mathbf{1}$ but also, for example, the type $\mathbf{1}\to\mathbf{1}$ which contains one function: $\lambda x.x$, and the type $\mathbf{1}\times\mathbf{1}$ which contains a single pair: $(\star, \star)$. And in terms of types with zero elements, there is $\mathbf{0}\times\mathbf{0}$ but also, for example, $\mathbf{0}\times\mathbf{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 $\mathbf{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 $\mathbf{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:

$$\mathsf{isTruthVal}:\equiv\bigg(\lambda A.\prod_{x:A}\prod_{y:A}(x=_Ay)\bigg)~:\mathcal{U}\to\mathcal{U}$$

Meaning that $\mathsf{isTruthVal}(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., $\Pi_{x:A}\Pi_{y:A}(x=y)$ will just be our good friend, the empty function. If $A$ contains just one element, $a$, then $\mathsf{isTruthVal}(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.^[2]

I called the above predicate “$\mathsf{isTruthVal}$” 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 $\bot$, and if it has a single element, it corresponds to $\top$. Note in particular that any type with exactly one element can represent $\top$ and any type with zero elements can represent $\bot$.

But now we have to address the important question of whether we can still use $\prod$, $\sum$, $\times$, $+$ and “$\to\mathbf{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 $\mathbf{0}$, then $P\to Q$ can only contain the empty function which is also unique. And if $Q$ is $\mathbf{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, $\phi$, such that $\phi(x)$ is a subsingleton type for any $x:X$. Then is

$$\prod_{x:X}\phi(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 $\phi(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 $\phi(x)$’s are singletons, then $\Pi_{x:X}\phi(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}\Big(g(x)=f(x)\Big)$$

And this is easy to prove here for two functions $g, f:\Pi_{x:X}\phi(x)$. We’ll just invoke the fact that for all $p,q:\phi(x)$, we have $p=q$ (by the assumption that $\phi(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: $\mathsf{left}(p)$ and $\mathsf{right}(q)$. Similarly, if for $\phi(x)$ there is more than one $x$ for which $\phi(x)$ has an element (say, $y$ and $z:X$ and $\phi(y)\equiv\phi(z)\equiv\mathbf{1}$), then $\sum_{x:X}\phi(x)$ will have more than one element; in this case $(y,\star)$ and $(z,\star)$.

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\mathbf{0}$. This is entirely unproblematic because the type $P\to\mathbf{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\mathbf{0}$, we have

$$\prod_{p:P}\Big(g(p)=f(p)\Big)$$

if we already know that $\mathbf{0}$ is a subsingleton. Do we know that $\mathbf{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:\mathbf{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 $\mathbf{0}$ is a subsingleton.

By the way, the fact that that the type $A\to\mathbf{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:

Additionally, we’ll assume the following axiom:

$$\mathrm{DNE}_{-1}:\equiv \prod_{P:\mathcal{U}}\Big(\mathsf{isTruthVal}(P)\to\big((P\to\mathbf{0})\to\mathbf{0}\big)\to P\Big)$$

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

Encoding implication #

Previously, we’ve used the function type $P\to Q$ to encode $P\Rightarrow Q$ (“$P$ implies $Q$”), but in classical logic, implication is usually not a fundamental operator; rather, it’s defined via “$\neg$” and “$\lor$”, or, if you only have “$\neg$” and “$\land$”, you can define “$P\Rightarrow Q$” as $\neg(P\land\neg Q)$, which is “$(P\times(Q\to\mathbf{0}))\to\mathbf{0}$” when encoded as a type. However, it turns out that the type “$P\to Q$” 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 $f:P\to Q$, and the function $g$ that we want to construct takes a pair $(p, \bar{q}):P\times(Q\to\mathbf{0})$ as input, then we can define:

$$\begin{aligned} &g:(P\times(Q\to\mathbf{0}))\to\mathbf{0}\\ &g((p, \bar{q})):\equiv \bar{q}(f(p)) \end{aligned}$$

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

For the opposite direction, we are given a function $g$ of the above type, and and want to construct a function $f$ which takes a $p:P$ as input. First, we’ll construct a helper function $\check{q}$ (which will be used inside $f$, so we can assume we have $p:P$):

$$\begin{aligned} &\check{q}:(Q\to\mathbf{0})\to\mathbf{0}\\ &\check{q}(\bar{q}):\equiv g((p,\bar{q})) \end{aligned}$$

where $\bar{q}$ is of type $Q\to\mathbf{0}$ as before. Now, through double-negation elimination, we can turn $\check{q}$ into an element of $Q$, which is exactly what we wanted to construct. If we use “$\mathsf{dne}$” to denote the function that inhabits DNE, then we can define $f:P\to Q$ as

$$f(p):\equiv\mathsf{dne}_Q\big(\lambda \bar{q}.g((p,\bar{q}))\big)$$

Thus, thanks to DNE, we were able to construct $f$ from $g$. So, “$P\to Q$” and “$(P\times(Q\to\mathbf{0}))\to\mathbf{0}$” are logically equivalent under DNE and we can safely encode implication as $P\to Q$.

Encoding disjunction #

Another somewhat interesting question is what the types look like that you get when negating $\prod$ and $\times$ in order to encode $\exists$ and $\lor$. That is, we know that we can get $P\lor Q$ from $\neg(\neg P\land\neg Q)$ in classical logic, but what does that look like as types?

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

OK, let’s prove that

$$\big((P\to\mathbf{0})\times(Q\to\mathbf{0})\big)\to\mathbf{0}$$

(i.e., $\neg(\neg P\land\neg Q)$) is logically equivalent to

$$(P+Q\to\mathbf{0})\to\mathbf{0}$$

which would mean that we can encode the logical statement “$P\lor Q$” as $(P+Q\to\mathbf{0})\to\mathbf{0}$. First we’ll prove the direction top to bottom. So, we are given $f:((P\to\mathbf{0})\times(Q\to\mathbf{0}))\to\mathbf{0}$ and the function $h$ that we have to construct, takes $g:(P+Q)\to\mathbf{0}$ as the first argument. The solution is then:

$$\begin{aligned} &h: (P+Q\to\mathbf{0})\to\mathbf{0}\\ &h(g):\equiv f\Big(\Big(\lambda p.g\big(\mathsf{left}(p)\big) ,\lambda q.g\big(\mathsf{right}(q)\big)\Big)\Big) \end{aligned}$$

which proves we can get $h$ from $f$.

For the opposite direction, we are given $h:(P+Q\to\mathbf{0})\to\mathbf{0}$, and the function $f$ that we want to construct takes the pair $(\bar{p}, \bar{q}):(P\to\mathbf{0})\times(Q\to\mathbf{0})$ as an argument. We’ll again need a helper function $k:P+Q\to\mathbf{0}$ which is defined within $f$ so we have access to $\bar{p}$ and $\bar{q}$. $k$ is defined by case analysis (aka pattern matching):

$$\begin{aligned} k(\mathsf{left(p)})&:\equiv \bar{p}(p)\\ k(\mathsf{right(q)})&:\equiv \bar{q}(q) \end{aligned}$$

With this, we can construct $f$:

$$f((\bar{p}, \bar{q})):\equiv h(k)$$

where $k$ depends on $(\bar{p}, \bar{q})$ but I’m using loose notation so it’s not indicated.

So, we have proved that $((P\to\mathbf{0})\times(Q\to\mathbf{0}))\to\mathbf{0}$ and $(P+Q\to\mathbf{0})\to\mathbf{0}$ 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 $A\to\mathbf{0}$ is a subsingleton for any type $A$, 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: $P+Q$ had the problem that it might contain two elements, but $(P+Q\to\mathbf{0})\to\mathbf{0}$ 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:

$$\|A\|\equiv(A\to\mathbf{0})\to\mathbf{0}$$

We always have $A\to\|A\|$ for any type $A$, but we only have $\|A\|\to A$ if $A$ is a subsingleton (provided we have assumed DNE$_{-1}$). That is, $\|A\|$ and $A$ are equivalent for subsingletons in the presence of DNE.

We can show something similar for $\Sigma$. We know that $\exists(x:X).\phi(x)$ is equivalent to $\neg\forall(x:X).\neg \phi(x)$ in classical logic. This identity can be used to derive that

$$\left\|\sum_{x:X}\phi(x)\right\|$$

can be used to encode $\exists(x:X).\phi(x)$. But this derivation is left as an exercise to the reader.

This means we can extend our translation table:

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:

$$\Big(\big(B+(B\to\mathbf{0})\big)\to\mathbf{0}\Big)\to\mathbf{0}$$

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, $\|P+Q\|$ is equivalent to $P+Q$ if $P$ and $Q$ 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 $\Pi$, $\Sigma$, etc. So, when constructing propositions and functions that output truth values (like predicates and relations), we will use $\exists$, $\forall$, $\lor$, $\land$, $\neg$, $\Rightarrow$ and $\Leftrightarrow$. The tables above define how these symbols get translated to the underlying operators on types. We can, for example, express LEM now as

$$\mathrm{LEM}\equiv\forall(P:\mathcal{U}).P\lor\neg P~.$$

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

$$\mathrm{LEM}_{-1}\equiv\forall(P:\mathcal{U}).\mathsf{isTruthVal}(P)\Rightarrow (P\lor\neg P)$$

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 $X$ as $X\to\mathcal{U}$, where $\mathcal{U}$ 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:

$$\mathsf{TruthVal}_\mathcal{U} :\equiv \sum_{A:\mathcal{U}}\mathsf{isTruthVal}(A)~.$$

Let’s think about what that means. Elements of this sum type are pairs where the first element is some type $A$ and the second element is a witness $p$ to the proposition $\mathsf{isTruthVal}(A)$. So, such a pair can only exist if the type representing the proposition is inhabited, meaning the proposition is true. Thus, the elements of $\mathsf{TruthVal}_\mathcal{U}$ are exactly those types $A:\mathcal{U}$ which are subsingletons!

Technically, the elements of $\mathsf{TruthVal}_\mathcal{U}$ are pairs of subsingletons and witnesses, $(A, p)$, but we will usually pretend the elements are just the types. In any case, there is an obvious mapping from $(A, p)$ to $A$.

With this definition, the type of a predicate function on a base type $A$ is $\phi:A\to \mathsf{TruthVal}_\mathcal{U}$. I called this subuniverse “$\mathsf{TruthVal}$” 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 $\mathcal{U}$. That is, $\mathsf{TruthVal}_\mathcal{U}$ doesn’t give us all the “falsy” and “truthy” types out there but only the ones in universe $\mathcal{U}$. And this is a problem if we want to talk about power sets.

Power sets and propositional extensionality #

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

If there were some “truthy” type $T$ (i.e., a type with exactly one element) that’s not in $\mathsf{TruthVal}_\mathcal{U}$ but we have a function $\phi$ that maps some $a:A$ to this type, $\phi(a)\equiv T$, then this function $\phi$ wouldn’t be captured by the function type $A\to\mathsf{TruthVal}_\mathcal{U}$, but it would still be a predicate, so “$A\to\mathsf{TruthVal}_\mathcal{U}$” 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 $\mathsf{TruthVal}$ contains is the empty type $\mathbf{0}$ and the unit type $\mathbf{1}$ and then an infinite number of types that are combinations of these: $\mathbf{1}\times\mathbf{1}$, $\mathbf{0}\times\mathbf{1}$, $\mathbf{0}\to\mathbf{1}$, $\mathbf{1}\times\mathbf{1}\times\mathbf{0}$, … 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 $\mathbf{0}$ or $\mathbf{1}$ (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 $\Omega :\mathcal{U}$ together with an $\Omega$-indexed family of subsingletons (aka, a function $f:\Pi_{\omega:\Omega}P(\omega)$ where all $f(\omega)$ are subsingletons) such that this family (the range of $f$) contains all subsingletons up to equality. Thus, the elements of $\Omega$ constitute an index for all falsy and truthy types. And as it is easy to turn an element of $\Omega$ into a truth value (via the function $f$), we can define the power set type to be

$$\mathcal{P}(A):\equiv (A\to\Omega)$$

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

The good news is that the existence of $\Omega$ follows from LEM and propositional extensionality (mentioned above). So, we won’t actually have to assume a new axiom for $\Omega$ if we adopt propositional extensionality (which I think we do want to but more on that later). A possible (and obvious) choice for $\Omega$ under LEM and propositional extensionality is in fact $\mathbf{2}$ – 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 $\mathbf{2}$ 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 $\mathbf{2}$ 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 $\prod$ and $\times$ 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:

$$\mathcal{P}(A):\equiv (A\to\mathbf{2})$$

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 $X$ to $Y$), 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 $\mathcal{P}(A)$ for which I can formulate a predicate function in the lambda calculus formalism, which surely doesn’t cover all possible mappings from $A$ to $\mathbf{2}$, if $A$ is infinite. However, the same problem actually also exists in set theory: in practice I can only access those elements of $\mathcal{P}(A)$ for which I have a first-order logic formula proving that they are subsets of $A$. Still, the meaning we give to $\mathcal{P}(A)$ 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 $\Omega$, our version of logic actually looks more like second-order logic than first-order, because we can quantify over predicates too:

$$\forall(\phi:A\to\Omega).\Phi(\phi)\quad\text{and}\quad\exists(\phi:A\to\Omega).\Psi(\phi)~.$$

In fact, we could also quantify over predicates of predicates (i.e., $\phi':(A\to\Omega)\to\Omega$) 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 $\forall$ and $\exists$ 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.

This post is part of the series Introduction to dependent type theory.

• Next post: Law of excluded middle from axiom of choice
• Previous post: Recreating logic in type theory