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 bundle bundles calculus categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex-geometry computable-mathematics computer-science constructive constructive-mathematics cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundations functional-analysis functor galois-theory gauge-theory gebra geometric-quantization geometry graph graphs gravity 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 limit limits linear linear-algebra locale localization logic manifolds mathematics measure-theory modal-logic model model-category-theory monads monoidal monoidal-category-theory morphism motives motivic-cohomology multicategories nonassociative noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics planar 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 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).
    • CommentRowNumber1.
    • CommentAuthorTobyBartels
    • CommentTimeJan 19th 2014

    I got an email which is really more for Mike than for me. Maybe Mike got it too, but in case not, I repost it here:

    I teach an introductory axiomatic set theory class at the University of Warwick. We cover the basics of Zermelo set theory. In particular, this is material set theory. Over the years I've become acquainted with alternate structural presentations such as ETCS. Now and again I have looked at the SEAR page on nLab. Some students from my class have approached me in connection with our undergraduate summer research programme. It occurred to me that it might be instructive for them to see what would be involves in redeveloping the matierial from our course from such an alternative viewpoint. I don't believe there is an ETCS based text, although Lawvere-Rosebrugh's Sets for Mathematics is a step in that direction. Perhaps SEAR would represent a more comfortable middle ground. I've been unable to locate any SEAR materials beyond what I find at nLab. Is there any existing work that my students should be made aware of?

    The course in question seems to be this one; in any case, the email came from the instructor listed there, from the email address given on the page for that instructor.

    • CommentRowNumber2.
    • CommentAuthorspitters
    • CommentTimeDec 15th 2015

    The SEAR page claims that SEAR is a dependent type theory. However, it seems that dependently sorted theory is more accurate. Is that correct?

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeDec 15th 2015

    What’s the difference?

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeDec 15th 2015

    Oh, are you saying that rather than being a type theory itself, it is a theory formulated in a dependent type theory? Yes, that’s true; I probably didn’t know the lingo as well when I wrote that.

    • CommentRowNumber5.
    • CommentAuthorspitters
    • CommentTimeDec 15th 2015

    There seem to be no notable type formers in SEAR. FOLDS might be an appropriate setting?

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeDec 16th 2015

    Yes, it can be formulated in FOLDS.

    • CommentRowNumber7.
    • CommentAuthorDavidRoberts
    • CommentTimeDec 18th 2015

    Bas, what was the end result of talking to Freek about SEAR? (Moving discussion here from G+ for better inclusivity)

    • CommentRowNumber8.
    • CommentAuthorspitters
    • CommentTimeDec 21st 2015

    No real result, but I can repeat here what I said there:

    Chatting a bit with Freek Wiedijk. It looks like formalization of SEAR in the logical framework should have a similar size as ZFC. It’s a nice exercise to do this in LF for anyone that’s looking for a fun project.

    One question is whether SEAR can easily be build on top of Mizar, this turns out to be difficult, as all types there need to be inhabited.

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeDec 21st 2015

    Can’t you just add a dummy element to a possibly-empty type to make it nonempty?

    • CommentRowNumber10.
    • CommentAuthorspitters
    • CommentTimeDec 22nd 2015

    Yes, I believe that should be possible. However, Mizar’s automation will be less useful in this case, IIUC.

    • CommentRowNumber11.
    • CommentAuthorspitters
    • CommentTimeJan 6th 2016

    One possibility would be to try and produce a file like the Mizar axioms for Grothendieck Tarski, but for SEAR. IIUC Mizar has a classical dependently sorted first order logic at its core, but there all the sorts need to be inhabited. So, a direct encoding is not possible. It’s probably more interesting to do this in isabelle, or metamath, or another LF.