Not signed in

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

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorsaolof
   • CommentTimeSep 28th 2021
   • PermaLink
   Author: saolof
   Format: TextA few basic questions: 1) Is there a formalization of SEAR anywhere, like for example as a Coq/Agda/Lean library or the like? Just being able to see a fully formalized version & proving the basic theorems would help a lot. As I understand it, full SEAR requires some kind of dependent types in order to express indexed families of sets, and "property" as expressed in the nLab needs some kind of definition? 2) If you remove replacement to get the ETCS-like fragment, can the axioms be expressed purely in first order logic? Or does it still need some form of type theory? What gets lost, other than not being able to formulate products of an arbitrary number of non-isomorphic sets? 3) (possibly trivial but not immediately obvious since I have a hazy understanding of what is allowed by the axioms) In that first order fragment, is it provable that the lattice of relations from A to B is complete, since infinite conjunctions and disjunctions are generally not allowed?

   A few basic questions:
   
   1) Is there a formalization of SEAR anywhere, like for example as a Coq/Agda/Lean library or the like? Just being able to see a fully formalized version & proving the basic theorems would help a lot. As I understand it, full SEAR requires some kind of dependent types in order to express indexed families of sets, and "property" as expressed in the nLab needs some kind of definition?
   
   2) If you remove replacement to get the ETCS-like fragment, can the axioms be expressed purely in first order logic? Or does it still need some form of type theory? What gets lost, other than not being able to formulate products of an arbitrary number of non-isomorphic sets?
   
   3) (possibly trivial but not immediately obvious since I have a hazy understanding of what is allowed by the axioms) In that first order fragment, is it provable that the lattice of relations from A to B is complete, since infinite conjunctions and disjunctions are generally not allowed?
2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeSep 29th 2021
   • PermaLink
   Author: Urs
   Format: MarkdownItex> Is there a formalization of SEAR anywhere, like for example as a Coq/Agda/Lean library or the like? In 2019 some Joshua Chen wrote on FOM ([here](https://cs.nyu.edu/pipermail/fom/2019-May/021536.html)): > I've started a formalization of Mike Shulman's SEAR in Isabelle on top of triply-sorted first-order logic, and will be experimenting to see how much mathematics I can formalize in this.

   Is there a formalization of SEAR anywhere, like for example as a Coq/Agda/Lean library or the like?

   In 2019 some Joshua Chen wrote on FOM (here):

   I’ve started a formalization of Mike Shulman’s SEAR in Isabelle on top of triply-sorted first-order logic, and will be experimenting to see how much mathematics I can formalize in this.

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeOct 3rd 2021
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexSEAR is written in dependently typed first-order logic, whether or not you include replacement. The dependent types have nothing to do with families of sets, which are expressed in SEAR using relations or bundles just as they are in ETCS, but only with the fact that the type of elements of a set and the type of relations between two sets are dependent on the type of sets. Properties are just first-order formulas. Replacement/collection is irrelevant for *internal* completeness of the lattice of relations, which is always provable just as it is in any elementary topos. (Some helpful recent discussion of replacement, and what it means and doesn't mean, is at [Tom's recent cafe post](https://golem.ph.utexas.edu/category/2021/07/large_sets_12.html) and the ensuing discussion in the comments.) I don't know of any completed formalization of SEAR.

   SEAR is written in dependently typed first-order logic, whether or not you include replacement. The dependent types have nothing to do with families of sets, which are expressed in SEAR using relations or bundles just as they are in ETCS, but only with the fact that the type of elements of a set and the type of relations between two sets are dependent on the type of sets. Properties are just first-order formulas.

   Replacement/collection is irrelevant for internal completeness of the lattice of relations, which is always provable just as it is in any elementary topos. (Some helpful recent discussion of replacement, and what it means and doesn’t mean, is at Tom’s recent cafe post and the ensuing discussion in the comments.)

   I don’t know of any completed formalization of SEAR.