Some years ago, I was determined to write out that term and see what it looked like. It ended up sprawled across two lines and beta-reduced to itself in, I think, a loop of order 2. But I was making and correcting several mistakes as I went along, so I’m not entirely sure that I had it correct.

]]>Huh, okay. I guess that might do it. When you do have propositions-as-types, though, I’m pretty sure Girard’s paradox is a non-normalizing term.

]]>@Mike: I’m more-or-less just quoting Coquand’s 1986 paper. He also says it is “a formal system which is fundamentally the system $U$ of Girard”. The sense in which formulae are “provable” is defined inductively on the structure of formulae, rather than based on inhabitation of types – it looks like propositions-as-types is not in force here.

]]>Ooh, I just noticed there’s another “Coquand’s paradox”, which imports Russell’s paradox into type theory using W-types. The paper is The paradox of trees in type theory. And this one is really easy to code up in Coq:

```
Inductive tree : Type :=
| sup : forall A, (A -> tree) -> tree.
Definition normal (T : tree) : Type :=
match T with
| sup A subtrees => forall a:A, (T == subtrees a) -> Empty_set
end.
Definition R : tree := sup (sigT normal) pr1.
Lemma Rn : normal R.
Proof.
intros [T tn] rt.
exact (transport (!rt) tn (T;tn) rt).
Defined.
Definition oops : Empty_set := Rn (R;Rn) (idpath R).
```

And it compiles using the type-in-type patch! (-:

]]>@Sridhar #14: Yes, I think that’s right. Maybe the most accurate thing to say is that Coquand’s paradox contains Russell’s paradox as a subterm? There’s definitely also content in Coquand’s paradox that has nothing to do with Russell’s paradox.

]]>@Toby: Thanks, that’s good to know. Although I’m kind of sad to hear that it wasn’t a moment of epiphany as depicted in *Logicomix*. (-:

@Zhen: I don’t know for sure what the “calculus of Church with second-order types” means, but I don’t see how Girard’s paradox could be anything but a non-normalizable term. How else could you have a term of type false?

]]>@Mike: I agree, the notation is somewhat opaque. My understanding is the same as yours: *if* there is a normalisation theorem for the type theory, then *either* there is no universe type, or there is no term interpreting membership, or there is no term interpreting set comprehension. But this is not so different from set theory – Russell’s paradox applied to ZF refutes the existence of a universal set, while applied to NF it refutes naïve comprehension. Different conclusions, same argument.

I’m afraid I’m still lost as to Girard’s paradox though. According to Coquand, Girard’s paradox can be interpreted in the “calculus of Church with second-order types”, for which there *is* a normalisation theorem: so, apparently, it’s not about unnormalisable terms.

Where did he say that?

His autobiography, according to a page on *Cut the Knot*:

]]>At the end of the Lent Term, Alys and I went back to Femhurst, where I set to work to write out the logical deduction of mathematics which afterwards became

Principia Mathematica. I thought the work was nearly finished, but in the month of May I had an intellectual set-back almost as severe as the emotional set-back which I had had in February. Cantor had a proof that there is no greatest number, and it seemed to me that the number of all the things in the world ought to be the greatest possible. Accordingly, I examined his proof with some minuteness, and endeavoured to apply it to the class of all the things there are. This led me to consider those classes which are not members of themselves, and to ask whether the class of such classes is or is not a member of itself. I found that either answer implies its contradictory. At first I supposed that I should be able to overcome the contradiction quite easily, and that probably there was some trivial error in the reasoning. Gradually, however, it became clear that this was not the case. Burali-Forti had already discovered a similar contradiction, and it turned out on logical analysis that there was an affinity with the ancient Greek contradiction about Epimenides the Cretan, who said that all Cretans are liars. A contradiction essentially similar to that of Epimenides can be created by giving a person a piece of paper on which is written: 'The statement on the other side of this paper is false.' The person turns the paper over, and finds on the other side: 'The statement on the other side of this paper is true.' It seemed unworthy of a grown man to spend his time on such trivialities, but what was I to do? There was something wrong, since such contradictions were unavoidable on ordinary premises. Trivial or not, the matter was a challenge. Throughout the latter half of 1901 I supposed the solution would be easy, but by the end of that time I had concluded that it was a big job. I therefore decided to finishThe Principles of Mathematics, leaving the solution in abeyance. In the autumn Alys and I went back to Cambridge, as I had been invited to give two terms' lectures on mathematical logic. These lectures contained the outline ofPrincipia Mathematica, but without any method of dealing with the contradictions.

we can say that Russell’s paradox is a $\beta$-reduction of Cantor’s paradox.

And so we do, on Russell's paradox. Probably you wrote it too.

]]>@Zhen: Oh. I couldn’t make any sense of the notation in that paragraph. But I guess I see what he’s saying… *if* we could somehow in type theory obtain a universe type which is injected into by its power-type, then we could (unsurprisingly) reproduce Russell’s/Cantor’s paradox in that way — but if we could do that, it would result in a non-normalizing term of type Prop, which doesn’t exist by the normalization theorem, and hence we can’t do that. Is that right?

I’m afraid I still don’t get the point, though… Girard’s paradox *also* produces a non-normalizing term, so clearly the type theory in which it is formulated doesn’t *have* a normalization theorem. So what exactly is the point of mentioning the fact that some *other* consistent type theory is, in fact, consistent? It doesn’t seem to be making a point about why we use Burali-Forti rather than Russell to find a paradox in type theory, which is what I thought he was trying to say. But maybe that’s not what he was trying to say?

Re: 18, we can say that Russell’s paradox is a $\beta$-reduction of Cantor’s paradox.

Russell himself said he was led to his paradox by applying Cantor’s theorem to the set of all sets.

I’ve never heard that! Where did he say that?

]]>BTW, I noticed that Russell's paradox was the only member of category: paradox, so I added Cantor's paradox and Burali-Forti's paradox to it. (I'm not sure if Skolem's paradox belongs there; it's not one of the celebrated antinomies from the crisis of foundations.)

]]>I just wrote Cantor's Paradox.

As you can see, this paradox comes about by applying the *conclusion* of Cantor's Theorem to the set of all sets, and immediately noticing the contradiction. Then if you pass this through the *proof* of Cantor's Theorem, you get Russell's Paradox, which is simpler (since you needn't have proved Cantor's Theorem yet to spot the contradiction).

@Mike: Hurken’s formalisation of Russell’s paradox is in his paper, p. 271. As I understand it, the two assumptions are the existence of terms $\sigma$ and $\tau$ interpreting $\ni$ and set comprehension, and $\Delta \in \Delta$, where $\Delta$ is the Russell class, is the non-normalisable term of type Prop.

]]>I’ve not heard the term “Cantor’s paradox” before, but, sure, I would just as well call it that. What difference is there between Cantor’s paradox and Russell’s paradox? Russell himself said he was led to his paradox by applying Cantor’s theorem to the set of all sets.

]]>That makes it sound like it could just as easily be Cantor’s Paradox (which is also essentially the same as Russell’s).

]]>I believe Coquand’s paradox involves the double powerset en route to using the single powerset, and thus might as well be considered a sophisticated version of Russell’s paradox. That is, Coquand’s paradox starts by constructing an initial algebra (and thus a fixed point) for the double powerset functor, but one can’t stop the argument there. One then has to go further and show how this yields inconsistency. The finishing steps are by noting that we then have an injection from P(X) into P(P(X)) = X, which yields a surjection from X onto P(X), which in the familiar Cantorian way yields a fixed point of negation, which yields inconsistency. That part might as well be considered Russell’s paradox, no? (I suppose I view Russell’s paradox as just a way of looking at Cantor’s theorem)

]]>@Toby: I’m pretty sure that Coquand’s paradox involves the double powerset. If I’m right, then that’s a good reason why it’s different from Russell’s! (Even more different from Russell’s than Girard’s is from Burali-Forti’s.)

@Zhen: Again you managed to pick out the sentence in Coquand’s paper that made no sense to me. I agree that intuitively there is something “non-normalizing” about Russell’s paradox, but I don’t have any idea how to formalize Russell’s paradox in type theory at all, lacking a global $\in$. Hurkens was formalizing Burali-Forti–Girard’s paradox, right, not Russell’s? Is there some *precise* sense in which Russell’s paradox could be regarded as “a non-normal term of type Prop” — or is Coquand just speaking informally, saing “term of type Prop” to refer to the “propositions” in a *non-type-theoretic* foundational system?

I believe that I read somebody (possibly it was Paul Taylor) claiming that Coquand’s paradox was indeed Russell’s paradox in the context of type theory and should be called such. Presumably this same reasoning would lead one to call Girard’s paradox Burali-Forti’s, which I would not do, so I’m not advocating that.

But I thought that this involved the (covariant) *single*-power-set functor. (After all, the set of all well-founded pure sets, to which Russell’s paradox applies, *is* the initial algebra of that.)

Perhaps Hurkin means this comment of Coquand:

What about consistency? We have to note that the result of Girard about normalisation property of the second-order λ-calculus shows that there can be no paradox like Russell’s. Indeed, this paradox lays upon the existence of a non-normal term of type Prop.

It appears to me that, at least in Hurkin’s formalisation, Russell’s argument produces a non-normalisable term ($\Delta \in \Delta$) – so Girard’s normalisation theorem implies Russell’s paradox must be type-theoretically invalid. But this only shows that there do not exist terms $\sigma : \mathcal{U} \to (\mathcal{U} \to Prop)$ (corresponding to the $\ni$ relation) or $\tau : (\mathcal{U} \to Prop) \to \mathcal{U}$ (corresponding to set comprehension) such that $\sigma (\tau X)$ β-reduces to $X$. It’s far from obvious to me that this is the only way to formalise Russell’s paradox, but maybe that’s just because I don’t understand type theory (either Russellian or modern!).

]]>Urs, I’m afraid I may be to blame for your confusion. When introducing type theory to mathematicians, I’ve gotten into the habit of saying “well, of course $Type:Type$ leads to paradoxes, so we use a hierarchy of universes” and moving on. I do this because (a) I think it’s intuitively *plausible* to a mathematician familiar with set-theoretic paradoxes that $Type:Type$ would be subject to similar ones, and (b) I don’t want to spend a lot of time talking about paradoxes. But it could give the wrong impression that all of the set-theoretic paradoxes apply verbatim in type theory, which is certainly not the case.

As far as I can tell, Hurkin’s paper is “simplified” in the formal sense that $\beta$-reduction can be called “simplification” — from the point of view of a human reader, it might be called “complicated-ified”. At root Girard’s paradox is really just Burali-Forti’s paradox, which is quite simple.

However, as noted by Coquand (1986), Russell’s paradox cannot be formalised in this way since each proposition has a normal form.

It’s funny that you should quote this! Just last night I was puzzling over this statement trying to make any sense at all out of it. I looked through the paper by Coquand that he’s referring to and didn’t find anything that looked to me to be at all related. And I can’t guess in what way each proposition having a normal form would have to do with formalizing Russell’s paradox, either. Does it make sense to you? Can you enlighten me?

]]>Ah, I see. Thanks.

]]>Russell’s paradox is fundamentally about set comprehension and *non-membership*: just having a universal set isn’t enough to produce an inconsistency.

Hurken’s paper presents a “simplified” version of Girard’s paradox, but I’m afraid it still goes over my head! He also mentions Russell’s paradox:

]]>However, as noted by Coquand (1986), Russell’s paradox cannot be formalised in this way since each proposition has a normal form. (Of course, in an inconsistent system each proposition is

provableequivalent to its negation.)

Mike, all I mean is that Burali-Forti is about “the ordered thing of all ordered things”, while “Type : Type” is just speaking about “the thing of all things” without any mentioning of orderings. That’s more like the “set of all sets” in Russell’s paradox.

But I gather the statement is that Girard happened to prove that $Type : Type$ is inconsistent, which a priori does not involve any orders, by invoking some auxiliary ordering for technical reasons? Is that what’s going on?

]]>