Thomas M. Kehrenberg

Classical logic based on propositions-as-subsingleton-types

(Part of the series .)

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.


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: “(xy)(2x2y)(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: Eq(x,y)\mathsf{Eq}(x, y), but everyone writes it in infix notationx=yx=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:

=  :T:UTTU .{=}\;:\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=Tyx=_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 aa of any type AAaa is equal to itself. That is, the following type is inhabited:

A:Ua:A(a=a) .\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, “xyx\equiv y” directly implies “x=yx=y”. Proof: x=xx=x is true by definition; now substitute one of the xx’s with yy (we can do this because we have xyx\equiv y, which implies substitutability) now we have x=yx=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 ϕ(x)\phi(x) is true (where ϕ\phi is some predicate/property) and x=yx=y is true, then ϕ(y)\phi(y) is also true. This is guaranteed by the following type’s inhabitedness:

x,y:A(x=Ay)ϕ(x)ϕ(y) .\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 xx, then all elements that are equal to xx also have this property (without further proof). So, if ϕ(n)\phi(n) is the predicate that tests whether nn is an even number, then if n=mn=m and nn is even, then mm is also even.

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

R:Πx,y:A(x=Ay)U(x:AR(x,x))x,y:A(x=Ay)R(x,y)\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 x:AR(x,x)\prod_{x:A}R(x,x) is the type corresponding to the proposition of reflexivity. It says that RR relates every element to itself. As a somewhat trivial example, “\leq” is reflexive, so whenever we have x=yx=y, we also have xyx\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:

LEMA:UA+(A0) .\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 0\mathbf{0} and 1\mathbf{1} but also, for example, the type 11\mathbf{1}\to\mathbf{1} which contains one function: λx.x\lambda x.x, and the type 1×1\mathbf{1}\times\mathbf{1} which contains a single pair: (,)(\star, \star). And in terms of types with zero elements, there is 0×0\mathbf{0}\times\mathbf{0} but also, for example, 0×1\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 1\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 1\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)(-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 AA is a subsingleton, based on the definition of equality that we conveniently just learned about:

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

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

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

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


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


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

We now turn our attention to P+QP+Q and it’s pretty clear that there is a problem here. If both PP and QQ have an element (say, pp and qq respectively), then P+QP+Q will have two elements: left(p)\mathsf{left}(p) and right(q)\mathsf{right}(q). Similarly, if for ϕ(x)\phi(x) there is more than one xx for which ϕ(x)\phi(x) has an element (say, yy and z:Xz:X and ϕ(y)ϕ(z)1\phi(y)\equiv\phi(z)\equiv\mathbf{1}), then x:Xϕ(x)\sum_{x:X}\phi(x) will have more than one element; in this case (y,)(y,\star) and (z,)(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, ¬P\neg P, which we encoded as P0P\to\mathbf{0}. This is entirely unproblematic because the type P0P\to\mathbf{0} is a subsingleton for any type PP, 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:P0g,f:P\to\mathbf{0}, we have


if we already know that 0\mathbf{0} is a subsingleton. Do we know that 0\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:0x,y:\mathbf{0}, then we’re again in the position to prove anything, including x=yx=y, via the principle of explosion. So either way, we may conclude that 0\mathbf{0} is a subsingleton.

By the way, the fact that that the type A0A\to\mathbf{0} is a subsingleton for any type AA 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
(x:X).ϕ(x)\forall (x:X).\phi(x) x:Xϕ(x)\prod_{x:X}\phi(x)
PQP\land Q P×QP\times Q
¬P\neg P P0P\to\mathbf{0}
\top (true) 1\mathbf{1}
\bot (false) 0\mathbf{0}

Additionally, we’ll assume the following axiom:

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

Encoding implication

Previously, we’ve used the function type PQP\to Q to encode PQP\Rightarrow Q (“PP implies QQ”), 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 “PQP\Rightarrow Q” as ¬(P¬Q)\neg(P\land\neg Q), which is “(P×(Q0))0(P\times(Q\to\mathbf{0}))\to\mathbf{0}” when encoded as a type. However, it turns out that the type “PQP\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:PQf:P\to Q, and the function gg that we want to construct takes a pair (p,qˉ):P×(Q0)(p, \bar{q}):P\times(Q\to\mathbf{0}) as input, then we can define:

g:(P×(Q0))0g((p,qˉ)):qˉ(f(p))\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 gg from ff.

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

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

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

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

Thus, thanks to DNE, we were able to construct ff from gg. So, “PQP\to Q” and “(P×(Q0))0(P\times(Q\to\mathbf{0}))\to\mathbf{0}” are logically equivalent under DNE and we can safely encode implication as PQP\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 PQP\lor Q from ¬(¬P¬Q)\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 “0\to\mathbf{0}” to encode PQP\lor Q, then the result is logically equivalent to (P+Q0)0(P+Q\to\mathbf{0})\to\mathbf{0}, i.e., double-negated P+QP+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+QP+Q, doesn’t that mean we get P+QP+Q by our DNE axiom? No! Because P+QP+Q is not (in general) a subsingleton, so our DNE1_{-1} does not apply.

OK, let’s prove that


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


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

h:(P+Q0)0h(g):f((λp.g(left(p)),λq.g(right(q))))\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 hh from ff.

For the opposite direction, we are given h:(P+Q0)0h:(P+Q\to\mathbf{0})\to\mathbf{0}, and the function ff that we want to construct takes the pair (pˉ,qˉ):(P0)×(Q0)(\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+Q0k:P+Q\to\mathbf{0} which is defined within ff so we have access to pˉ\bar{p} and qˉ\bar{q}kk is defined by case analysis (aka pattern matching):

k(left(p)):pˉ(p)k(right(q)):qˉ(q)\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 ff:

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

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

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


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

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


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

This means we can extend our translation table:

First-order Logic Type Theory
PQP\Rightarrow Q PQP\to Q
PQP\Leftrightarrow Q (PQ)×(QP)(P\to Q)\times(Q\to P)
(x:X).ϕ(x)\exists (x:X).\phi(x) x:Xϕ(x)|\sum_{x:X}\phi(x)|
PQP\lor Q P+Q|P+ Q|

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, P+Q\|P+Q\| is equivalent to P+QP+Q if PP and QQ 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

LEM(P:U).P¬P .\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

LEM1(P:U).isTruthVal(P)(P¬P)\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 XX as XUX\to\mathcal{U}, where U\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:

TruthValU:A:UisTruthVal(A) .\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 AA and the second element is a witness pp to the proposition isTruthVal(A)\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 TruthValU\mathsf{TruthVal}_\mathcal{U} are exactly those types A:UA:\mathcal{U} which are subsingletons!

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

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

Power sets and propositional extensionality

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

If there were some “truthy” type TT (i.e., a type with exactly one element) that’s not in TruthValU\mathsf{TruthVal}_\mathcal{U} but we have a function ϕ\phi that maps some a:Aa:A to this type, ϕ(a)T\phi(a)\equiv T, then this function ϕ\phi wouldn’t be captured by the function type ATruthValUA\to\mathsf{TruthVal}_\mathcal{U}, but it would still be a predicate, so “ATruthValUA\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 TruthVal\mathsf{TruthVal} contains is the empty type 0\mathbf{0} and the unit type 1\mathbf{1} and then an infinite number of types that are combinations of these: 1×1\mathbf{1}\times\mathbf{1}0×1\mathbf{0}\times\mathbf{1}01\mathbf{0}\to\mathbf{1}1×1×0\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 0\mathbf{0} or 1\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 Ω:U\Omega :\mathcal{U} together with an Ω\Omega-indexed family of subsingletons (aka, a function f:Πω:ΩP(ω)f:\Pi_{\omega:\Omega}P(\omega) where all f(ω)f(\omega) are subsingletons) such that this family (the range of ff) 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 ff), we can define the power set type to be

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

and this will be guaranteed to encompass all predicates on AA 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 2\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 2\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 2\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:

P(A):(A2)\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 XX to YY), 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 P(A)\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 AA to 2\mathbf{2}, if AA is infinite. However, the same problem actually also exists in set theory: in practice I can only access those elements of P(A)\mathcal{P}(A) for which I have a first-order logic formula proving that they are subsets of AA. Still, the meaning we give to P(A)\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:

(ϕ:AΩ).Φ(ϕ)and(ϕ:AΩ).Ψ(ϕ) .\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., ϕ:(AΩ)Ω\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.

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

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



This post is part of the series .