Not signed in

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

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

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 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 internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure 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 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

1. • CommentRowNumber1.
   • CommentAuthorDavidRoberts
   • CommentTimeNov 1st 2012
   • (edited Nov 1st 2012)
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexAt [[well-founded relation]] we have the statement >Even in constructive predicative mathematics, (1) is strong enough to establish the [[Burali-Forti paradox]]. where (1) is >The relation $\prec$ has __no infinite descent__ (usually attributed to [[Pierre de Fermat]]) if there exists no [[sequence]] $\cdots \prec x_2 \prec x_1 \prec x_0$ in $S$. (Such a sequence is called an _infinite descending sequence_.) No reference is made to linear orders here. But what if I generalise from linear orders to [[well-quasi-order]]s? Can I, given a well-pointed topos $E$ with nno, show that the category of well-quasi-orders with the 'obvious inclusions' is large and has a faithful functor to the [[wide subcategory]] $E_\hookrightarrow$ of $E$ with the monomorphisms as arrows? I'm thinking of generalising the well-ordered class of ordinals $Ord \hookrightarrow Set_\hookrightarrow$. Ideally I'd like a large preorder, but I not confident this is possible.

   At well-founded relation we have the statement

   Even in constructive predicative mathematics, (1) is strong enough to establish the Burali-Forti paradox.

   where (1) is

   The relation $\prec$ has no infinite descent (usually attributed to Pierre de Fermat) if there exists no sequence $\cdots \prec x_2 \prec x_1 \prec x_0$ in $S$. (Such a sequence is called an infinite descending sequence.)

   No reference is made to linear orders here. But what if I generalise from linear orders to well-quasi-orders?

   Can I, given a well-pointed topos $E$ with nno, show that the category of well-quasi-orders with the ’obvious inclusions’ is large and has a faithful functor to the wide subcategory $E_\hookrightarrow$ of $E$ with the monomorphisms as arrows?

   I’m thinking of generalising the well-ordered class of ordinals $Ord \hookrightarrow Set_\hookrightarrow$.

   Ideally I’d like a large preorder, but I not confident this is possible.

2. • CommentRowNumber2.
   • CommentAuthorDavidRoberts
   • CommentTimeNov 1st 2012
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexThat being said, perhaps I'd just like a large linear order, represented faithfully in $E_\hookrightarrow$. Any thoughts?

   That being said, perhaps I’d just like a large linear order, represented faithfully in $E_\hookrightarrow$. Any thoughts?

3. • CommentRowNumber3.
   • CommentAuthorTobyBartels
   • CommentTimeNov 1st 2012
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexThe various definitions at [[well-quasi-order]] are not even all equivalent assuming intuitionistic logic; and since I don\'t really know what well-quasi-orders are for, I don\'t know which to use.

   The various definitions at well-quasi-order are not even all equivalent assuming intuitionistic logic; and since I don't really know what well-quasi-orders are for, I don't know which to use.

4. • CommentRowNumber4.
   • CommentAuthorDavidRoberts
   • CommentTimeNov 1st 2012
   • (edited Nov 1st 2012)
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexI do mean in classical logic, since my topos is well-pointed. And I'm not really after the well-quasi-order case specifically. If the well-ordered case works I'm happy. Maybe I should nut it out myself :-)

   I do mean in classical logic, since my topos is well-pointed. And I’m not really after the well-quasi-order case specifically. If the well-ordered case works I’m happy. Maybe I should nut it out myself :-)

5. • CommentRowNumber5.
   • CommentAuthorTobyBartels
   • CommentTimeNov 2nd 2012
   • (edited Nov 2nd 2012)
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexA [[well-pointed topos]] need not be boolean, but I guess that you're also using a classical meta-logic? >And I'm not really after the well-quasi-order case specifically. If the well-ordered case works I'm happy. I\'m not quite sure what the question is supposed to be then. If one defines a well order in the stack semantics of a $\PI$-$W$-pretopos $E$ as a linear order with no infinite descent, then there is no object of $E$ whose elements parametrise the well orders in $E$, and the proof is the Burali-Forti argument. In this sense, the category (actually poset) of well-orders in $E$ is large (relative to $E$).

   A well-pointed topos need not be boolean, but I guess that you’re also using a classical meta-logic?

   And I’m not really after the well-quasi-order case specifically. If the well-ordered case works I’m happy.

   I'm not quite sure what the question is supposed to be then. If one defines a well order in the stack semantics of a $\PI$-$W$-pretopos $E$ as a linear order with no infinite descent, then there is no object of $E$ whose elements parametrise the well orders in $E$, and the proof is the Burali-Forti argument. In this sense, the category (actually poset) of well-orders in $E$ is large (relative to $E$).

6. • CommentRowNumber6.
   • CommentAuthorDavidRoberts
   • CommentTimeNov 2nd 2012
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItex>I guess that you’re also using a classical meta-logic Yes. Sorry, should have said. >In this sense, the category (actually poset) of well-orders in E is large (relative to E). Ah, good. I need to hunt down a good reference that shows that all this can be done in a weak logical background, or at least one that I can point at and say 'it can be done'.

   I guess that you’re also using a classical meta-logic

   Yes. Sorry, should have said.

   In this sense, the category (actually poset) of well-orders in E is large (relative to E).

   Ah, good. I need to hunt down a good reference that shows that all this can be done in a weak logical background, or at least one that I can point at and say ’it can be done’.

7. • CommentRowNumber7.
   • CommentAuthorTobyBartels
   • CommentTimeNov 2nd 2012
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexI tried and failed earlier to remember where I first saw this construction done under the name of [[Girard's paradox]]. One would have to see what exactly Girard used.

   I tried and failed earlier to remember where I first saw this construction done under the name of Girard’s paradox. One would have to see what exactly Girard used.

8. • CommentRowNumber8.
   • CommentAuthorMike Shulman
   • CommentTimeNov 3rd 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI believe Girard used something like Martin-Lof dependent type theory. [Here](http://flint.cs.yale.edu/cs430/coq/library/Coq.Logic.Hurkens.html) is a page of Coq code implementing what is supposedly a "simplified" version of the paradox. I must admit to not being able to make much sense of it myself; I find it easier to just write down the paradox by hand in whatever system you want to be in.

   I believe Girard used something like Martin-Lof dependent type theory.

   Here is a page of Coq code implementing what is supposedly a “simplified” version of the paradox. I must admit to not being able to make much sense of it myself; I find it easier to just write down the paradox by hand in whatever system you want to be in.

9. • CommentRowNumber9.
   • CommentAuthorTobyBartels
   • CommentTimeNov 5th 2012
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexMy understanding is that initially Girard used exactly what was then Martin-Löf type theory, so Martin-Löf had to change what it was. But when I write ‘One would have to see what exactly Girard used.’, I mean that one would see which features of that type theory were essential.

   My understanding is that initially Girard used exactly what was then Martin-Löf type theory, so Martin-Löf had to change what it was.

   But when I write ‘One would have to see what exactly Girard used.’, I mean that one would see which features of that type theory were essential.