This website is out of date, please refer to the site on github.

Type is not in Type

Posted on August 26, 2015
Tags: jonprl, types, haskell

I was reading a recent proposal to merge types and kinds in Haskell to start the transition to dependently typed Haskell. One thing that caught my eye as I was reading it was that this proposal adds * :: * to the type system. This is of some significance because it means that once this is fully realized, Haskell will be inconsistent (as a logic) in a new way! Of course, this isn’t a huge deal since Haskell is already woefully inconsistent with

So it’s not like we’ll be entering new territory here. All that it means is that there’s a new way to inhabit every type in Haskell. If you were using Haskell as a proof assistant you were already in for a rude awakening I’m afraid :)

This is an issue of significance though for languages like Idris or Agda where such a thing would actually render proofs useless. Famously, Martin-Löf’s original type theory did have Type : Type (or * :: * in Haskell spelling) and Girard managed to derive a contradiction (Girard’s paradox). I’ve always been told that the particulars of this construction are a little bit complicated but to remember that Type : Type is bad.

In this post I’d like to prove that Type : Type is a contradiction in JonPRL. This is a little interesting because in most proof assistants this would work in two steps

  1. Hack the compiler to add the rule Type : Type
  2. Construct a contradiction and check it with the modified compiler

OK to be fair, in something like Agda you could use the compiler hacking they’ve already done and just say {-# OPTIONS --set-in-set #-} or whatever the flag is. The spirit of the development is the same though

In JonPRL, I’m just going to prove this as a regular implication. We have a proposition which internalizes membership and I’ll demonstrate not(member(U{i}; U{i})) is provable (U{i} is how we say Type in JonPRL). It’s the same logic as we had before.

Background on JonPRL

Before we can really get to the proof we want to talk about, we should go through some of the more advanced features of JonPRL we need to use.

JonPRL is a little different than most proof assistants, for example We can define a type of all closed terms in our language and whose equality is purely computational. This type is base. To prove that =(a; b; base) holds you have to prove ceq(a; b), the finest grain equality in JonPRL. Two terms are ceq if they

  1. Both diverge, or
  2. Run to the same outermost form and have ceq components

What’s particularly exciting is that you can substitute any term for any other term ceq to it, no matter at what type it’s being used and under what hypotheses. In fact, the reduce tactic (which performs beta reductions) can conceptually be thought of as substituting a bunch of terms for their weak-head-normal forms which are ceq to the original terms. The relevant literature behind this is found in Doug Howe’s “Equality in a Lazy Computation System”. There’s more in JonPRL in this regard, we also have the asymmetric version of ceq (called approx) but we won’t need it today.

Next, let’s talk about the image type. This is a type constructor with the following formation rule:

 H ⊢ A : U{i}        H ⊢ f : base
 —————————————————————————————————
      H ⊢ image(A; f) : U{i}

So here A is a type and f is anything. Things are going to be equal image if we can prove that they’re of the form f w and f w' where w = w' ∈ A. So image gives us the codomain (range) of a function. What’s pretty crazy about this is that it’s not just the range of some function A → B, we don’t really need a whole new type for that. It’s the range of literally any closed term we can apply. We can take the range of the Y combinator over pi types. We can take the range of lam(x. ⊥) over unit, anything we want!

This construct lets us define some really incredible things as a user of JonPRL. For example, the “squash” of a type is supposed to be a type which is occupied by <> (and only <>) if and only if there was an occupant of the original type. You can define these in HoTT with higher inductive types. Or, you can define these in this type theory as

    Operator squash : (0).
    [squash(A)] =def= [image(A; lam(x. <>))]

x ∈ squash(A) if and only if we can construct an a so that a ∈ A and lam(x. <>) a ~ x. Clearly x must be <> and we can construct such an a if and only if A is nonempty.

We can also define the set-union of two types. Something is supposed to be in the set union if and only if it’s in one or the other. Two define such a thing with an image type we have

    Operator union : (0).
    [union(A; B)] =def= [image((x : unit + unit) * decide(x; _.A; _.B); lam(x.snd(x)))]

This one is a bit more complicated. The domain of things we’re applying our function to this time is

    (x : unit + unit) * decide(x; _.A; _.B)

This is a dependent pair, sometimes called a Σ type. The first component is a boolean; if it is true the second component is of type A, and otherwise it’s of type B. So for every term of type A or B, there’s a term of this Σ type. In fact, we can recover that original term of type A or B by just grabbing the second component of the term! We don’t have to worry about the type of such an operation because we’re not creating something with a function type, just something in base.

unions let us define an absolutely critical admissible rule in our system. JonPRL has this propositional reflection of the equality judgment and membership, but in Martin-Löf’s type theory, membership is non-negatable. By this I mean that if we have some a so that a = a ∈ A doesn’t hold, we won’t be able to prove =(a; a; A) -> void. See in order to prove such a thing we first have to prove that =(a; b; A) -> void is a type, which means proving that =(a; a; A) is a type.

In order to prove that =(a; b; A) is a proposition we have to prove =(a; a; A), =(b; b; A), and =(A; A; U{i}). The process of proving these will actually also show that the corresponding judgments, a ∈ A, b ∈ A, and A ∈ U{i} hold.

However, in the case that a and b are the same term this is just the same as proving =(a; b; A)! So =(a; a; A) is a proposition only if it’s true. However, we can add a rule that says that =(a; b; A) is a proposition if a = a ∈ (A ∪ base) and similarly for b! This fixes our negatibility issue because we can just prove that =(a; a; base), something that may be true even if a is not equal in A. Before having a function take a member(...) was useless (member(a; A) is just thin sugar for =(a; a; A)! member(a; A) is a proposition if and only if a = a ∈ A holds, in other words, it’s a proposition if and only if it’s true! With this new rule, we can prove member(a; A) is a proposition if A ∈ U{i} and a ∈ base, a much weaker set of conditions that are almost always true. We can apply this special rule in JonPRL with eq-eq-base instead of just eq-cd like the rest of our equality rules.

The Main Result

Now let’s actually begin proving Russell’s paradox. To start with some notation.

    Infix 20 "∈" := member.
    Infix 40 "~" := ceq.
    Infix 60 "∪" := bunion.
    Prefix 40 "¬" := not.

This let’s us say a ∈ b instead of member(a; b). JonPRL recently grew this ability to add transparent notation to terms, it makes our theorems a lot prettier.

Next we define the central term to our proof:

    Operator Russell : ().
    [Russell] =def= [{x : U{i} | ¬ (x ∈ x)}]

Here we’ve defined Russell as shorthand for a subset type, in particular a subset of U{i} (the universe of types). x ∈ Russell if x ∈ U{i} and ¬ (x ∈ x). Now normally we won’t be able to prove that this is a type (specifically x ∈ x is going to be a problem), but in our case we’ll have some help from an assumption that U{i} ∈ U{i}.

Now we begin to define a small set of tactics that we’ll want. These tactics are really where the fiddly bits of using JonPRL’s tactic system come into play. If you’re just reading this for the intuition as to why Type ∈ Type is bad just skip this. You’ll still understand the construction even if you don’t understand these bits of the proof.

First we have a tactic which finds an occurrence of H : A + B in the context and eliminate it. This gives us two goals, one with an A and one with a B. To do this we use match, which gives us something like match goal with in Coq.

    Tactic break-plus {
      @{ [H : _ + _ |- _] => elim <H>; thin <H> }
    }.

Note the syntax [H : ... |- ...] to match on a sequent. In particular here we just have _ + _ and _. Next we have a tactic bunion-eq-right. It’s to help us work with bunions (unions). Basically it turns =(M; N; bunion(A; B)) into

    =(lam(x.snd(x)) <<>, M>; lam(x.snd(x)) <<>, N>; bunion(A; B))

This is actually helpful because it turns out that once we unfold bunion we have to prove that M and N are in an image type, remember that bunion is just a thin layer of sugar on top of image types. In order to prove something is in the image type it needs to be of the form f a where f in our case is lam(x. snd(x)).

This is done with

    Tactic bunion-eq-right {
      @{ [|- =(M; N; L ∪ R)] =>
           csubst [M ~ lam(x. snd(x)) <inr(<>), M>] [h.=(h;_;_)];
           aux { unfold <snd>; reduce; auto };
           csubst [N ~ lam(x. snd(x)) <inr(<>), N>] [h.=(_;h;_)];
           aux { unfold <snd>; reduce; auto };
      }
    }.

The key here is csubst. It takes a ceq as its first argument and a “targeting”. It then tries to replace each occurrence of the left side of the equality with the right. To find each occurrence the targeting maps a variable to each occurrence. We’re allowed to use wildcards in the targeting as well. It also relegates actually proving the equality into a new subgoal. It’s easy enough to prove so we demonstrate it with aux {unfold <snd>; reduce; auto}.

We only need to apply this tactic after eq-eq-base, this applies that rule I mentioned earlier about proving equalities to be well-formed in a much more liberal environment. Therefore we wrap those two tactics into one more convenient package.

    Tactic eq-base-tac {
      @{ [|- =(=(M; N; A); =(M'; N'; A'); _)] =>
           eq-eq-base; auto;
           bunion-eq-right; unfold <bunion>
       }
    }.

There is one last tactic in this series, this one to prove that member(X; X) ∈ U{i'} is well-formed (a type). It starts by unfolding member into =(=(X; X; X); =(X; X; X); U{i}) and then applying the new tactic. Then we do other things. These things aren’t pretty. I suggest we just ignore them.

    Tactic impredicativity-wf-tac {
      unfold <member>; eq-base-tac;
      eq-cd; ?{@{[|- =(_; _; base)] => auto}};
      eq-cd @i'; ?{break-plus}; reduce; auto
    }.

Finally we have a tactic to prove that if we have not(P) and P existing in the context proves void. This is another nice application match

    Tactic contradiction {
      unfold <not implies>;
      @{ [H : P -> void, H' : P |- void] =>
           elim <H> [H'];
           unfold <member>;
           auto
       }
    }.

We start by unfolding not and implies. This gives us P -> void and P. From there, we just apply one to the other giving us a void as we wanted.

We’re now ready to prove our theorem. We start with

    Theorem type-not-in-type : [¬ (U{i} ∈ U{i})] {
    }.

We now have the main subgoal

Remaining subgoals:

[main] ⊢ not(member(U{i}; U{i}))

We can start by unfold not and implies. Remember that not isn’t a built in thing, it’s just sugar. By unfolding it we get the more primitive form, something that actually apply the intro tactic to.

    {
      unfold <not implies>; intro
    }

Once unfolded, we’d get a goal along the lines of member(U{i}; U{i}) -> void. We immediately apply intro to this though. Now we have two subgoals; one is the result of applying intro, namely a hypothesis x : member(U{i}; U{i}) and a goal void. The second subgoal is the “well-formedness” obligation.

We have to prove that member(U{i}; U{i}) is a type in order to apply the intro tactic. This is a crucial difference between Coq-like systems and these proof-refinement logics. The process of demonstrating that what you’re proving is a proposition is intermingled with actually constructing the proof. It means you get to apply all the normal mathematical tools you have for proving things to be true in order to prove that they’re types. This gives us a lot of flexibility, but at the cost of sometimes annoying subgoals. They’re annotated with [aux] (as opposed to [main]). This means we can target them all at once using with the aux tactics.

To summarize that whole paragraph as JonPRL would say it, our proof state is

[main]
1. x : member(U{i}; U{i})
⊢ void

[aux] ⊢ member(member(U{i}; U{i}); U{i'})

Let’s get rid of that auxiliary subgoal using that impredictivity-wf-tac, this subgoal is in fact exactly what it was made for.

    {
      unfold <not implies>; intro
      aux { impredicativity-wf-tac };
    }

This picks off that [aux] goal leaving us with just

[main]
1. x : member(U{i}; U{i})
⊢ void

Now we need to prove some lemmas. They state that Russell is actually a type. This is possible to do here and only here because we’ll need to actually use x in the process of proving this. It’s a very nice example of what explicitly proving well-formedness can give you! After all, the process of demonstrating that Russell is a type is nontrivial and only possible in this hypothetical context, rather than just hoping that JonPRL is clever enough to figure that out for itself we get to demonstrate it locally.

We’re going to use the assert tactic to get these lemmas. This lets us state a term, prove it as a subgoal and use it as a hypothesis in the main goal. If you’re logically minded, it’s cut.

    {
      unfold <not implies>; intro;
      aux { impredicativity-wf-tac };

      assert [Russell ∈ U{i}] <russell-wf>;
    }

The thing in angle brackets is the name it will get in our hypothetical context for the main goal. This leaves us with two subgoals. The aux one being the assertion and the main one being allowed to assume it.

[aux]
1. x : member(U{i}; U{i})
⊢ member(Russell; U{i})

[main]
1. x : member(U{i}; U{i})
2. russell-wf : member(Russell; U{i})
⊢ void

We can prove this by basically working our way towards using impredicativity-wf-tac. We’ll use aux again to target the aux subgoal. We’ll start by unfolding everything and applying eq-cd.

    {
      unfold <not implies>; intro;
      aux { impredicativity-wf-tac };

      assert [Russell ∈ U{i}] <russell-wf>;
      aux {
        unfold <member Russell>; eq-cd; auto;
      };
    }

Remember that Russell is {x : U{i} | ¬ (x ∈ x)}

We just applied eq-cd to a subset type (Russell), so we get two subgoals. One says that U{i} is a type, one says that if x ∈ U{i} then ¬ (x ∈ x) is also a type. In essence this just says that a subset type is a type if both components are types. The former goal is quite straightforward so we applied auto and take care of it. Now we have one new subgoal to handle

[main]
1. x : =(U{i}; U{i}; U{i})
2. x' : U{i}
⊢ =(not(member(x'; x')); not(member(x'; x')); U{i})

[main]
1. x : member(U{i}; U{i})
2. russell-wf : member(Russell; U{i})
⊢ void

The second subgoal is just the rest of the proof, and the first subgoal is what we want to handle. It says that if we have a type x, then not(member(x; x)) is a type (albeit in ugly notation). To prove this we have to unfold not. So we’ll do this and apply eq-cd again.

    {
      unfold <not implies>; intro;
      aux { impredicativity-wf-tac };

      assert [Russell ∈ U{i}] <russell-wf>;
      aux {
        unfold <member Russell>; eq-cd; auto;
        unfold <not implies>; eq-cd; auto;
      };
    }

Remember that not(P) desugars to P -> void. Applying eq-cd is going to give us two subgoals, P is a type and void is a type. However, member(void; U{i}) is pretty easy to prove, so we apply auto again which takes care of one of our two new goals. Now we just have

[main]
1. x : =(U{i}; U{i}; U{i})
2. x' : U{i}
⊢ =(member(x'; x'); member(x'; x'); U{i})

[main]
1. x : member(U{i}; U{i})
2. russell-wf : member(Russell; U{i})
⊢ void

Now we’re getting to the root of the issue. We’re trying to prove that member(x'; x') is a type. This is happily handled by impredicativity-wf-tac which will use our assumption that U{i} ∈ U{i} because it’s smart like that.

    {
      unfold <not implies>; intro;
      aux { impredicativity-wf-tac };

      assert [Russell ∈ U{i}] <russell-wf>;
      aux {
        unfold <member Russell>; eq-cd; auto;
        unfold <not implies>; eq-cd; auto;
        impredicativity-wf-tac
      };
    }

Now we just have that main goal with the assumption russell-wf added.

[main]
1. x : member(U{i}; U{i})
2. russell-wf : member(Russell; U{i})
⊢ void

Now we have a similar well-formedness goal to assert and prove. We want to prove that ∈(Russell; Russell) is a type. This is easier though; we can prove it easily using impredicativity-wf-tac.

    {
      unfold <not implies>; intro;
      aux { impredicativity-wf-tac };

      assert [Russell ∈ U{i}] <russell-wf>;
      aux {
        unfold <member Russell>; eq-cd; auto;
        unfold <not implies>; eq-cd; auto;
        impredicativity-wf-tac
      };

      assert [(Russell ∈ Russell) ∈ U{i}] <russell-in-russell-wf>;
      aux { impredicativity-wf-tac; cum @i; auto };
    }

That cum @i is a quirk of impredicativity-wf-tac. It basically means that instead of proving =(...; ...; U{i'}) we can prove =(...; ...; U{i}) since U{i} is a universe below U{i'} and all universes are cumulative.

Our goal is now

[main]
1. x : member(U{i}; U{i})
2. russell-wf : member(Russell; U{i})
3. russell-in-russell-wf : member(member(Russell; Russell); U{i})
⊢ void

Ok, so now the reasoning can start now that we have all these well-formedness lemmas. Our proof sketch is basically as follows

  1. Prove that Russell ∈ Russell is false. This is because if Russell was in Russell then by definition of Russell it isn’t in Russell.
  2. Since not(Russell ∈ Russell) holds, then Russell ∈ Russell holds.
  3. Hilarity ensues.

Here’s the first assertion:

    {
      unfold <not implies>; intro;
      aux { impredicativity-wf-tac };

      assert [Russell ∈ U{i}] <russell-wf>;
      aux {
        unfold <member Russell>; eq-cd; auto;
        unfold <not implies>; eq-cd; auto;
        impredicativity-wf-tac
      };

      assert [(Russell ∈ Russell) ∈ U{i}] <russell-in-russell-wf>;
      aux { impredicativity-wf-tac; cum @i; auto };

      assert [¬ (Russell ∈ Russell)] <not-russell-in-russell>;
    }

Here are our subgoals:

[aux]
1. x : member(U{i}; U{i})
2. russell-wf : member(Russell; U{i})
3. russell-in-russell-wf : member(member(Russell; Russell); U{i})
⊢ not(member(Russell; Russell))

[main]
1. x : member(U{i}; U{i})
2. russell-wf : member(Russell; U{i})
3. russell-in-russell-wf : member(member(Russell; Russell); U{i})
4. russell-not-in-russell : not(member(Russell; Russell))
⊢ void

We want to prove that first one. To start, let’s unfold that not and move member(Russell; Russell) to the hypothesis and use it to prove void. We do this with intro.

    {
      unfold <not implies>; intro;
      aux { ... };

      assert [Russell ∈ U{i}] <russell-wf>;
      aux { ... };

      assert [(Russell ∈ Russell) ∈ U{i}] <russell-in-russell-wf>;
      aux { ... };

      assert [¬ (Russell ∈ Russell)] <not-russell-in-russell>;
      aux {
        unfold <not implies>;
        intro @i; aux {assumption};
      }
    }

Notice that the well-formedness goal that intro generated is handled by our assumption! After all, it’s just member(Russell; Russell) ∈ U{i}, we already proved it. Now our subgoals look like this

[main]
1. x : member(U{i}; U{i})
2. russell-wf : member(Russell; U{i})
3. russell-in-russell-wf : member(member(Russell; Russell); U{i})
4. x' : member(Russell; Russell)
⊢ void

[main]
1. x : member(U{i}; U{i})
2. russell-wf : member(Russell; U{i})
3. russell-in-russell-wf : member(member(Russell; Russell); U{i})
4. russell-not-in-russell : not(member(Russell; Russell))
⊢ void

Here’s our clever plan

  1. Since Russell ∈ Russell, there’s an X : Russell so that ceq(Russell; X) holds
  2. Since X : Russell, we can unfold it to say that X : {x ∈ U{i} | ¬ (x ∈ x)}
  3. We can apply the elimination principle for subset types to X and derive that ¬ (X ∈ X)
  4. Rewriting by ceq(Russell; X) gives ¬ (Russell; Russell)
  5. Now we have a contradiction

Let’s start explaining this to JonPRL by introducing that X (here called R). We’ll assert an R : Russell such that R ~ Russell. We do this using dependent pairs (here written (x : A) * B(x)).

    {
      unfold <not implies>; intro;
      aux { ... };

      assert [Russell ∈ U{i}] <russell-wf>;
      aux { ... };

      assert [(Russell ∈ Russell) ∈ U{i}] <russell-in-russell-wf>;
      aux { ... };

      assert [¬ (Russell ∈ Russell)] <not-russell-in-russell>;
      aux {
        unfold <not implies>;
        intro @i; aux {assumption};
        assert [(R : Russell) * R ~ Russell] <R-with-prop>;
        aux {
          intro [Russell] @i; auto
        };
      }
    }

We’ve proven this by intro. For proving dependent products we provide an explicit witness for the first component. Basically to prove (x : A) * B(x) we say intro [Foo]. We then have a goal Foo ∈ A and B(Foo). Since subgoals are fully independent of each other, we have to give the witness for the first component upfront. It’s a little awkward, Jon’s working on it :).

In this case we use intro [Russell]. After this we have to prove that this witness has type Russell and then prove the second component holds. Happily, auto takes care of both of these obligations so intro [Russell] @i; auto handles it all.

Now we promptly eliminate this pair. It gives us two new facts, that R : Russell and R ~ Russell hold.

    {
      unfold <not implies>; intro;
      aux { ... };

      assert [Russell ∈ U{i}] <russell-wf>;
      aux { ... };

      assert [(Russell ∈ Russell) ∈ U{i}] <russell-in-russell-wf>;
      aux { ... };

      assert [¬ (Russell ∈ Russell)] <not-russell-in-russell>;
      aux {
        unfold <not implies>;
        intro @i; aux {assumption};
        assert [(R : Russell) * R ~ Russell] <R-with-prop>;
        aux {
          intro [Russell] @i; auto
        };

        elim <R-with-prop>; thin <R-with-prop>
      }
    }

This leaves our goal as

[main]
1. x : member(U{i}; U{i})
2. russell-wf : member(Russell; U{i})
3. russell-in-russell-wf : member(member(Russell; Russell); U{i})
4. x' : member(Russell; Russell)
5. s : Russell
6. t : ceq(s; Russell)
⊢ void

[main]
1. x : member(U{i}; U{i})
2. russell-wf : member(Russell; U{i})
3. russell-in-russell-wf : member(member(Russell; Russell); U{i})
4. russell-not-in-russell : not(member(Russell; Russell))
⊢ void

Now let’s invert on the hypothesis that s : Russell; we want to use it to conclude that ¬ (s ∈ s) holds since that will give us ¬ (R ∈ R).

    {
      unfold <not implies>; intro;
      aux { ... };

      assert [Russell ∈ U{i}] <russell-wf>;
      aux { ... };

      assert [(Russell ∈ Russell) ∈ U{i}] <russell-in-russell-wf>;
      aux { ... };

      assert [¬ (Russell ∈ Russell)] <not-russell-in-russell>;
      aux {
        unfold <not implies>;
        intro @i; aux {assumption};
        assert [(R : Russell) * R ~ Russell] <R-with-prop>;
        aux {
          intro [Russell] @i; auto
        };

        elim <R-with-prop>; thin <R-with-prop>;
        unfold <Russell>; elim #5;
      }
    }

Now that we’ve unfolded all of those Russells our goal is a little bit harder to read, remember to mentally substitute {x : U{i} | not(member(x; x))} as Russell.

[main]
1. x : member(U{i}; U{i})
2. russell-wf : member({x:U{i} | not(member(x; x))}; U{i})
3. russell-in-russell-wf : member(member({x:U{i} | not(member(x; x))}; {x:U{i} | not(member(x; x))}); U{i})
4. x' : member({x:U{i} | not(member(x; x))}; {x:U{i} | not(member(x; x))})
5. s : {x:U{i} | not(member(x; x))}
6. x'' : U{i}
7. [t'] : not(member(x''; x''))
8. t : ceq(x''; {x:U{i} | not(member(x; x))})
⊢ void

[main]
1. x : member(U{i}; U{i})
2. russell-wf : member(Russell; U{i})
3. russell-in-russell-wf : member(member(Russell; Russell); U{i})
4. russell-not-in-russell : not(member(Russell; Russell))
⊢ void

Now we use #7 to derive that not(member(Russell; Russell)) holds.

    {
      unfold <not implies>; intro;
      aux { ... };

      assert [Russell ∈ U{i}] <russell-wf>;
      aux { ... };

      assert [(Russell ∈ Russell) ∈ U{i}] <russell-in-russell-wf>;
      aux { ... };

      assert [¬ (Russell ∈ Russell)] <not-russell-in-russell>;
      aux {
        unfold <not implies>;
        intro @i; aux {assumption};
        assert [(R : Russell) * R ~ Russell] <R-with-prop>;
        aux {
          intro [Russell] @i; auto
        };

        elim <R-with-prop>; thin <R-with-prop>;
        unfold <Russell>; elim #5;

        assert [¬ member(Russell; Russell)];
        aux {
          unfold <Russell>;
        };
      }
    }

This leaves us with 3 subgoals, the first one being the assertion.

[aux]
1. x : member(U{i}; U{i})
2. russell-wf : member({x:U{i} | not(member(x; x))}; U{i})
3. russell-in-russell-wf : member(member({x:U{i} | not(member(x; x))}; {x:U{i} | not(member(x; x))}); U{i})
4. x' : member({x:U{i} | not(member(x; x))}; {x:U{i} | not(member(x; x))})
5. s : {x:U{i} | not(member(x; x))}
6. x'' : U{i}
7. [t'] : not(member(x''; x''))
8. t : ceq(x''; {x:U{i} | not(member(x; x))})
⊢ not(member({x:U{i} | not(member(x; x))}; {x:U{i} | not(member(x; x))}))

[main]
1. x : member(U{i}; U{i})
2. russell-wf : member({x:U{i} | not(member(x; x))}; U{i})
3. russell-in-russell-wf : member(member({x:U{i} | not(member(x; x))}; {x:U{i} | not(member(x; x))}); U{i})
4. x' : member({x:U{i} | not(member(x; x))}; {x:U{i} | not(member(x; x))})
5. s : {x:U{i} | not(member(x; x))}
6. x'' : U{i}
7. [t'] : not(member(x''; x''))
8. t : ceq(x''; {x:U{i} | not(member(x; x))})
9. H : not(member(Russell; Russell))
⊢ void

[main]
1. x : member(U{i}; U{i})
2. russell-wf : member(Russell; U{i})
3. russell-in-russell-wf : member(member(Russell; Russell); U{i})
4. russell-not-in-russell : not(member(Russell; Russell))
⊢ void

Now to prove this, what we need to do is substitute the unfolded Russell for x''; from there it’s immediate by assumption. We perform the substitution with chyp-subst. This takes a direction in which to substitute, which hypothesis to use, and another targeting telling us where to apply the substitution.

    {
      unfold <not implies>; intro;
      aux { ... };

      assert [Russell ∈ U{i}] <russell-wf>;
      aux { ... };

      assert [(Russell ∈ Russell) ∈ U{i}] <russell-in-russell-wf>;
      aux { ... };

      assert [¬ (Russell ∈ Russell)] <not-russell-in-russell>;
      aux {
        unfold <not implies>;
        intro @i; aux {assumption};
        assert [(R : Russell) * R ~ Russell] <R-with-prop>;
        aux {
          intro [Russell] @i; auto
        };

        elim <R-with-prop>; thin <R-with-prop>;
        unfold <Russell>; elim #5;

        assert [¬ member(Russell; Russell)];
        aux {
          unfold <Russell>;
          chyp-subst ← #8 [h. ¬ (h ∈ h)];
        };
      }
    }

This leaves us with a much more tractable goal.

[main]
1. x : member(U{i}; U{i})
2. russell-wf : member({x:U{i} | not(member(x; x))}; U{i})
3. russell-in-russell-wf : member(member({x:U{i} | not(member(x; x))}; {x:U{i} | not(member(x; x))}); U{i})
4. x' : member({x:U{i} | not(member(x; x))}; {x:U{i} | not(member(x; x))})
5. s : {x:U{i} | not(member(x; x))}
6. x'' : U{i}
7. [t'] : not(member(x''; x''))
8. t : ceq(x''; {x:U{i} | not(member(x; x))})
⊢ not(member(x''; x''))

[main]
1. x : member(U{i}; U{i})
2. russell-wf : member({x:U{i} | not(member(x; x))}; U{i})
3. russell-in-russell-wf : member(member({x:U{i} | not(member(x; x))}; {x:U{i} | not(member(x; x))}); U{i})
4. x' : member({x:U{i} | not(member(x; x))}; {x:U{i} | not(member(x; x))})
5. s : {x:U{i} | not(member(x; x))}
6. x'' : U{i}
7. [t'] : not(member(x''; x''))
8. t : ceq(x''; {x:U{i} | not(member(x; x))})
9. H : not(member(Russell; Russell))
⊢ void

[main]
1. x : member(U{i}; U{i})
2. russell-wf : member(Russell; U{i})
3. russell-in-russell-wf : member(member(Russell; Russell); U{i})
4. russell-not-in-russell : not(member(Russell; Russell))
⊢ void

We’d like to just apply assumption but it’s not immediately applicable due to some technically details (basically we can only apply an assumption in a proof irrelevant context but we have to unfold Russell and introduce it to demonstrate that it’s irrelevant). So just read what’s left as a (very) convoluted assumption.

    {
      unfold <not implies>; intro;
      aux { ... };

      assert [Russell ∈ U{i}] <russell-wf>;
      aux { ... };

      assert [(Russell ∈ Russell) ∈ U{i}] <russell-in-russell-wf>;
      aux { ... };

      assert [¬ (Russell ∈ Russell)] <not-russell-in-russell>;
      aux {
        unfold <not implies>;
        intro @i; aux {assumption};
        assert [(R : Russell) * R ~ Russell] <R-with-prop>;
        aux {
          intro [Russell] @i; auto
        };

        elim <R-with-prop>; thin <R-with-prop>;
        unfold <Russell>; elim #5;

        assert [¬ (Russell; Russell)];
        aux {
          unfold <Russell>;
          chyp-subst ← #8 [h. ¬ (h ∈ h)];
          unfold <not implies>
          intro; aux { impredicativity-wf-tac };
          contradiction
        };
      }
    }

Now we’re almost through this assertion, our subgoals look like this (pay attention to 9 and 4)

[main]
1. x : member(U{i}; U{i})
2. russell-wf : member({x:U{i} | not(member(x; x))}; U{i})
3. russell-in-russell-wf : member(member({x:U{i} | not(member(x; x))}; {x:U{i} | not(member(x; x))}); U{i})
4. x' : member({x:U{i} | not(member(x; x))}; {x:U{i} | not(member(x; x))})
5. s : {x:U{i} | not(member(x; x))}
6. x'' : U{i}
7. [t'] : not(member(x''; x''))
8. t : ceq(x''; {x:U{i} | not(member(x; x))})
9. H : not(member(Russell; Russell))
⊢ void

[main]
1. x : member(U{i}; U{i})
2. russell-wf : member(Russell; U{i})
3. russell-in-russell-wf : member(member(Russell; Russell); U{i})
4. russell-not-in-russell : not(member(Russell; Russell))
⊢ void

Once we unfold that Russell we have an immediate contradiction so unfold <Russell>; contradiction solves it.

    {
      unfold <not implies>; intro;
      aux { ... };

      assert [Russell ∈ U{i}] <russell-wf>;
      aux { ... };

      assert [(Russell ∈ Russell) ∈ U{i}] <russell-in-russell-wf>;
      aux { ... };

      assert [¬ (Russell ∈ Russell)] <not-russell-in-russell>;
      aux {
        unfold <not implies>;
        intro @i; aux {assumption};
        assert [(R : Russell) * R ~ Russell] <R-with-prop>;
        aux {
          intro [Russell] @i; auto
        };

        elim <R-with-prop>; thin <R-with-prop>;
        unfold <Russell>; elim #5;

        assert [¬ (Russell; Russell)];
        aux {
          unfold <Russell>;
          chyp-subst ← #8 [h. ¬ (h ∈ h)];
          unfold <not implies>;
          intro; aux { impredicativity-wf-tac };
          contradiction
        };

        unfold <Russell>; contradiction
      }
    }

This takes care of this subgoal, so now we’re back on the main goal. This time though we have an extra hypothesis which will provide the leverage we need to prove our next assertion.

[main]
1. x : member(U{i}; U{i})
2. russell-wf : member(Russell; U{i})
3. russell-in-russell-wf : member(member(Russell; Russell); U{i})
4. russell-not-in-russell : not(member(Russell; Russell))
⊢ void

Now we’re going to claim that Russell is in fact a member of Russell. This will follow from the fact that we’ve proved already that Russell isn’t in Russell (yeah, it seems pretty paradoxical already).

    {
      unfold <not implies>; intro;
      aux { ... };

      assert [Russell ∈ U{i}] <russell-wf>;
      aux { ... };

      assert [(Russell ∈ Russell) ∈ U{i}] <russell-in-russell-wf>;
      aux { ... };

      assert [¬ (Russell ∈ Russell)] <not-russell-in-russell>;
      aux { ... };

      assert [Russell ∈ Russell];
   }

Giving us

[aux]
1. x : member(U{i}; U{i})
2. russell-wf : member(Russell; U{i})
3. russell-in-russell-wf : member(member(Russell; Russell); U{i})
4. russell-not-in-russell : not(member(Russell; Russell))
⊢ member(Russell; Russell)

[main]
1. x : member(U{i}; U{i})
2. russell-wf : member(Russell; U{i})
3. russell-in-russell-wf : member(member(Russell; Russell); U{i})
4. russell-not-in-russell : not(member(Russell; Russell))
5. H : member(Russell; Russell)
⊢ void

Proving this is pretty straightforward, we only have to demonstrate that not(Russell ∈ Russell) and Russell ∈ U{i}, both of which we have as assumptions. The rest of the proof is just more well-formedness goals.

First we unfold everything and apply eq-cd. This gives us 3 subgoals, the first two are Russell ∈ U{i} and ¬(Russell ∈ Russell). Since we have these as assumptions we’ll use main {assumption}. That will target both these goals and prove them immediately. Here by using main we avoid applying this to the well-formedness goal, which in this case actually isn’t the assumption.

    {
      unfold <not implies>; intro
      aux { ... };

      assert [Russell ∈ U{i}] <russell-wf>;
      aux { ... };

      assert [(Russell ∈ Russell) ∈ U{i}] <russell-in-russell-wf>;
      aux { ... };

      assert [¬ (Russell ∈ Russell)] <not-russell-in-russell>;
      aux { ... };

      assert [Russell ∈ Russell];
      aux {
        unfold <member Russell>; eq-cd;
        unfold <member>;

        main { assumption };
      };
    }

This just leaves us with one awful well-formedness goal requiring us to prove that not(=(x; x; x)) is a type if x is a type. We actually proved something similar back when we prove that Russell was well-formed. The proof is the same as then, just unfold, eq-cd and impredicativity-wf-tac. We use ?{!{auto}} to only apply auto in a subgoal where it immediately proves it. Here ?{} says “run this or do nothing” and !{} says “run this, if it succeeds stop, if it does anything else, fail”. This is not an interesting portion of the proof, don’t burn too many cycles trying to figure this out.

    {
      unfold <not implies>; intro
      aux { ... };

      assert [Russell ∈ U{i}] <russell-wf>;
      aux { ... };

      assert [(Russell ∈ Russell) ∈ U{i}] <russell-in-russell-wf>;
      aux { ... };

      assert [¬ (Russell ∈ Russell)] <not-russell-in-russell>;
      aux { ... };

      assert [Russell ∈ Russell] <russell-in-russell>;
      aux {
        unfold <member Russell>; eq-cd;
        unfold <member>;

        main { assumption };
        unfold <not implies>; eq-cd; ?{!{auto}};
        impredicativity-wf-tac;
      };
    }

Now we just have the final subgoal to prove. We’re actually in a position to do so now.

[main]
1. x : member(U{i}; U{i})
2. russell-wf : member(Russell; U{i})
3. russell-in-russell-wf : member(member(Russell; Russell); U{i})
4. russell-not-in-russell : not(member(Russell; Russell))
5. russell-in-russell : member(Russell; Russell)
⊢ void

Now that we’ve shown P and not(P) hold at the same time all we need to do is apply contradiction and we’re done.

    Theorem type-not-in-type [¬ (U{i} ∈ U{i})] {
      unfold <not implies>; intro
      aux { ... };

      assert [Russell ∈ U{i}] <russell-wf>;
      aux { ... };

      assert [(Russell ∈ Russell) ∈ U{i}] <russell-in-russell-wf>;
      aux { ... };

      assert [¬ (Russell ∈ Russell)] <not-russell-in-russell>;
      aux { ... };

      assert [Russell ∈ Russell] <russell-in-russell>;
      aux { ... };

      contradiction
    }.

And there you have it, a complete proof of Russell’s paradox fully formalized in JonPRL! We actually proved a slightly stronger result than just that the type of types cannot be in itself, we proved that at any point in the hierarchy of universes (the first of which is Type/*/whatever) if you tie it off, you’ll get a contradiction.

Wrap Up

I hope you found this proof interesting. Even if you’re not at all interested in JonPRL, it’s nice to see that allowing one to have U{i} ∈ U{i} or * :: * gives you the ability to have a type like Russell and with it, inhabit void. I also find it especially pleasing that we can prove something like this in JonPRL; it’s growing up so fast.

Thanks to Jon for greatly improving the original proof we had

comments powered by Disqus