## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorMike Shulman
• CommentTimeSep 20th 2012
• CommentRowNumber2.
• CommentAuthorZhen Lin
• CommentTimeSep 20th 2012

NF-ists like to point out that there’s a (Russellian) type-theoretic way of resolving the paradox. The gist of the claim seems to be the following:

1. An ordinal is defined to be an isomorphism class of well-ordered sets.
2. For each ordinal $\alpha$, the set $\{ \beta \in ON : \beta \lt \alpha \}$ is well-ordered; but its order type is $T^2 \alpha$, where $T$ is the type-raising operator. Note that $T^2 \alpha \ne \alpha$!
3. If $ON$ is well-ordered, then it has an order type $\Omega$. The paradoxical ordinal constructed by Burali-Forti’s argument, properly typed, is $T^2 \Omega + 1$, which is not obviously bigger than $\Omega$.

In fact, in NF, $\cdots \lt T^4 \Omega \lt T^2 \Omega \lt \Omega$. So we’ve traded one paradox for another…

• CommentRowNumber3.
• CommentAuthorMike Shulman
• CommentTimeSep 20th 2012

If you want to add something about that to the entry, feel free. I lost interest in NF when I found out that its category of sets is not cartesian closed. (-:

• CommentRowNumber4.
• CommentAuthorZhen Lin
• CommentTimeSep 20th 2012

I thought it was something worth pointing out, since type theory is mentioned on that page. (What exactly is Girard’s paradox? I’ve never seen a clear statement.) I thought the argument was quite interesting when I first heard it – because it says that the so-called paradox is nothing more than a typing error.

As for the of sets in NF – I think, really, we should think of them as well-behaved classes. After all, the category of classes in NBG is not obviously cartesian closed either. In fact, that’s exactly what Feferman does in the system in Enriched stratified systems for the foundations of category theory.

• CommentRowNumber5.
• CommentAuthorUrs
• CommentTimeSep 20th 2012

The inconsistency brought about by $\vdash Type : Type$ I would have expected to be discussed as/named after/related to Russell’s paradox, as there is no ordering involved. (?)

• CommentRowNumber6.
• CommentAuthorMike Shulman
• CommentTimeSep 20th 2012

@Zhen: As I said, feel free to add something. Note though that Russell’s ’type theory’ was rather different from what now goes by that name.

@Urs: I’m not sure what inconsistency you’re thinking of. The standard way to get an inconsistency from $Type:Type$ is Girard’s paradox, which is just Burali-Forti’s paradox, expressed in type theory (in the modern sense) rather than set theory.

There is another approach which might be called “Coquand’s paradox”, although I’m not sure if people do call it that. Thierry Coquand showed essentially that you can use impredicative quantification over $Type$ to build an initial algebra for the double-powerset endofunctor and then apply Lambek’s lemma and Cantor’s theorem. That’s certainly more closely related to Russell’s and Cantor’s paradoxes than Girard’s, but I don’t think I would give it the same name as either of them.

• CommentRowNumber7.
• CommentAuthorUrs
• CommentTimeSep 20th 2012
• (edited Sep 20th 2012)

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?

• CommentRowNumber8.
• CommentAuthorZhen Lin
• CommentTimeSep 20th 2012

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 provable equivalent to its negation.)

• CommentRowNumber9.
• CommentAuthorUrs
• CommentTimeSep 20th 2012

Ah, I see. Thanks.

• CommentRowNumber10.
• CommentAuthorMike Shulman
• CommentTimeSep 20th 2012

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?

• CommentRowNumber11.
• CommentAuthorZhen Lin
• CommentTimeSep 21st 2012

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!).

• CommentRowNumber12.
• CommentAuthorTobyBartels
• CommentTimeSep 21st 2012

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.)

• CommentRowNumber13.
• CommentAuthorMike Shulman
• CommentTimeSep 22nd 2012
• (edited Sep 22nd 2012)

@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?

• CommentRowNumber14.
• CommentAuthorSridharRamesh
• CommentTimeSep 22nd 2012
• (edited Sep 22nd 2012)

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)

• CommentRowNumber15.
• CommentAuthorTobyBartels
• CommentTimeSep 22nd 2012

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

• CommentRowNumber16.
• CommentAuthorSridharRamesh
• CommentTimeSep 22nd 2012
• (edited Sep 22nd 2012)

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.

• CommentRowNumber17.
• CommentAuthorZhen Lin
• CommentTimeSep 22nd 2012

@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.

• CommentRowNumber18.
• CommentAuthorTobyBartels
• CommentTimeSep 22nd 2012

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).

• CommentRowNumber19.
• CommentAuthorTobyBartels
• CommentTimeSep 22nd 2012
• (edited Sep 22nd 2012)

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.)

• CommentRowNumber20.
• CommentAuthorMike Shulman
• CommentTimeSep 22nd 2012

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?

• CommentRowNumber21.
• CommentAuthorMike Shulman
• CommentTimeSep 22nd 2012

@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?

• CommentRowNumber22.
• CommentAuthorTobyBartels
• CommentTimeSep 22nd 2012
• (edited Sep 22nd 2012)

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.

• CommentRowNumber23.
• CommentAuthorTobyBartels
• CommentTimeSep 22nd 2012

Where did he say that?

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

• CommentRowNumber24.
• CommentAuthorZhen Lin
• CommentTimeSep 22nd 2012

@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.

• CommentRowNumber25.
• CommentAuthorMike Shulman
• CommentTimeSep 22nd 2012

@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?

• CommentRowNumber26.
• CommentAuthorMike Shulman
• CommentTimeSep 22nd 2012

@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.

• CommentRowNumber27.
• CommentAuthorMike Shulman
• CommentTimeSep 22nd 2012

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! (-:

• CommentRowNumber28.
• CommentAuthorZhen Lin
• CommentTimeSep 23rd 2012

@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.

• CommentRowNumber29.
• CommentAuthorMike Shulman
• CommentTimeSep 23rd 2012

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.

• CommentRowNumber30.
• CommentAuthorTobyBartels
• CommentTimeSep 23rd 2012

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.