[FOM] Structural set theory for proof assistants

[Joshua Chen]

(CCing FOM list)

Thanks for writing Joj!

At the moment my mental model categorizes "set theory" as a theory
directly built on top of predicate logic (nth-order,
classical/intuitionistic/whatever), where the objects (sets, elements,
etc.) are things distinct from the formulas, as opposed to type theory
where the "sets" and the "formulas" are instances of the same concept.
In a sense, the basic logical approach is fundamentally different.

But I see your point, e.g. having separate universes "Set" and "Prop"
lets us reintroduce the set-formula distinction, classical reasoning can
be reintroduced via axioms, etc. Though, arguably, this setup is still
somewhat different to what a "working" mathematician unfamiliar with
type theory would intuitively use? In particular, "traditional"
(non-categorial) model theory doesn't seem to be a thing we can easily
apply to this setting anymore. It also feels like more overhead, but
that's maybe because I've only ever worked constructively when using it.
Perhaps my views will change with more familiarity..

It was nice to meet you at UniMath!

Best,
Josh

On 5/6/19 7:16 AM, Joseph Helfer wrote:
> Dear Josh,
>
> Type theory /is/ (a) structural set theory; Coq, Agda, etc. already do
> what you are asking about.
>
> No?
>
> Best,
> Joj
>
> On Fri, May 3, 2019 at 8:47 PM Joshua Chen <fom at joshchen.io
> <mailto:fom at joshchen.io>> wrote:
>
>     Dear FOM,
>
>     As part of my PhD I work with multiple proof assistants, and have
>     recently been wrangling with Mizar and its idiosyncracies. This got me
>     considering what a modern set theory-based proof assistant might do
>     differently, and in particular if, instead of material set theory, we
>     might choose to base such a system on structural set theory. 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.
>
>     Not being an expert, I'm posting here to ask:
>
>     Have structural set theories been considered as foundations for formal
>     *computer* mathematics before? Maybe some people who know the
>     details of
>     these foundations, and have perhaps tried to work out some mathematics
>     in them, could comment on the prospects of such an undertaking?
>     Even the
>     more recent developments in set-theoretic systems seem to mostly use
>     ZF(C), and I would like to know if this is a historical/cultural
>     accident, or if there is some deeper obstruction.
>
>     Best regards,
>
>     Josh
>
>     -- 
>     Joshua Chen
>
>     Computational Logic
>     Department of Computer Science
>     University of Innsbruck
>
>     Email: fom at joshchen.io <mailto:fom at joshchen.io>
>     Web: https://joshchen.io
>
>     _______________________________________________
>     FOM mailing list
>     FOM at cs.nyu.edu <mailto:FOM at cs.nyu.edu>
>     https://cs.nyu.edu/mailman/listinfo/fom
>
-- 
Joshua Chen

Computational Logic
Department of Computer Science
University of Innsbruck

Email: fom at joshchen.io
Web: https://joshchen.io

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20190506/25bb40d4/attachment.html>