Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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.
The SEAR page claims that SEAR is a dependent type theory. However, it seems that dependently sorted theory is more accurate. Is that correct?
What’s the difference?
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.
There seem to be no notable type formers in SEAR. FOLDS might be an appropriate setting?
Yes, it can be formulated in FOLDS.
Bas, what was the end result of talking to Freek about SEAR? (Moving discussion here from G+ for better inclusivity)
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.
Can’t you just add a dummy element to a possibly-empty type to make it nonempty?
Yes, I believe that should be possible. However, Mizar’s automation will be less useful in this case, IIUC.
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.
1 to 11 of 11