Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: Burali-Forti's paradox

Bottom of Page

1 to 30 of 30

  1.  
    • 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 {β∈ON:β<α}\{ \beta \in ON : \beta \lt \alpha \} is well-ordered; but its order type is T 2αT^2 \alpha, where TT is the type-raising operator. Note that T 2α≠αT^2 \alpha \ne \alpha!
    3. If ONON is well-ordered, then it has an order type Ω\Omega. The paradoxical ordinal constructed by Burali-Forti’s argument, properly typed, is T 2Ω+1T^2 \Omega + 1, which is not obviously bigger than Ω\Omega.

    In fact, in NF, ⋯<T 4Ω<T 2Ω<Ω\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 ⊢Type:Type\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:TypeType: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 TypeType 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:TypeType : 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:TypeType: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:TypeType: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 σ:𝒰→(𝒰→Prop)\sigma : \mathcal{U} \to (\mathcal{U} \to Prop) (corresponding to the ∋\ni relation) or τ:(𝒰→Prop)→𝒰\tau : (\mathcal{U} \to Prop) \to \mathcal{U} (corresponding to set comprehension) such that σ(τX)\sigma (\tau X) β-reduces to XX. 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

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

    • 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:

    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 finish The 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 of Principia Mathematica, but without any method of dealing with the contradictions.

    • 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 UU 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.

1 to 30 of 30

  1.