Existential Quantification in Type Theory

All of logic can be encoded with a suitable type theory and this includes the usual existential and universal quantifiers. The universal quantifier is easy because it corresponds to Π types but the existential quantifier is a little more tricky. It took me some time to make sense of it so here’s a small outline of how to think about it (this is as much to help me understand as it is for someone else so if you find any issues then let me know).

In “Type Theory and Formal Proof” the existential quantifier is defined with a second order Π type (I’m going to use Coq syntax)

Variables (S : Type) (P : S -> Prop).
(* exists x : S, P x *)
Hypothesis existential : forall (alpha : Type),
  (forall x, P x -> alpha) -> alpha.

The weird thing about this definition is that it doesn’t look like we have explicit terms that verify there is an inhabitant (a : S) that satisfies the predicate (ha : P a). In the book, the justification is in terms of introduction and elimination rules but I didn’t find that very enlightening so I’m going to follow a different route to understanding why it works

If you squint at that definition it should remind you of something: it looks suspiciously like continuation passing style. I’m sure there is a connection here but I don’t know where it goes so going to set that aside for the time being.

So let’s assume for a second that we actually have a term that corresponds to the existential then what can we do? Well, the simplest thing we can do is apply it to S

Let applied_to_S := existential S.
(* (forall x, P x -> S) -> S *)

We have almost recovered what we need and to push things through need to construct a term that corresponds to (forall x, P x -> S)

Let recover := fun (x : S) (proof : P x) => x.
(* forall x, P x -> S *)

Notice how we are ignoring the proof term. It’s almost like the proof is irrelevant. This is another avenue that I’m sure is fruitful but I don’t know enough to pursue it.

Applying one more time gets us the element

Let element := applied_to_S recover.

Then applying the predicate to the element gives us the certificate for the proof

Let element_proof := P element.

So what did we just do? Starting with a term for the existential we recovered an element of S and the corresponding proof object for the predicate. I don’t know about you but this is kinda amazing. It also makes sense because what is the only way to use recover? The only way to use it is to provide an element and the proof that the element satisfies the predicate. So all along the existential term must have had the element and the proof stashed away somewhere (for another take on this stashing away process I recommend reading one of Dan Piponi’s posts on the Yoneda Lemma).

How about the other direction? If we have an element and a proof that the element satisfies the predicate then can we recover the existential term? It wouldn’t be much fun if we couldn’t so let’s try it

Variable a : S.
Hypothesis proof_for_a : P a.

The existential term is really a function so what we want to do is construct a function that given the right inputs gives us the right output but that’s really easy to do given the above assumptions

fun (alpha : Type) (exists : forall x, P x -> alpha) =>
  (exists a proof_for_a)

It’s literally just function application with the assumptions we had. Pretty cool if you ask me.

Now I don’t know if I could have actually come up with that definition of an existential if my starting point wasn’t given but it sure was fun figuring out the pieces.