[FOM] Structural set theory for proof assistants

[Josef Urban]

I had a very brief look at the post about structural set theory. I wonder
to what extent some of its features can be modeled by the Mizar
type/structure mechanisms already.

For example, the set of real numbers is "material" in Mizar - constructed
as Dedekind cuts. But it is also possible to use that construction just as
an existential witness for defining a general (opaque/structural) Mizar
type (structure) of objects that have the required properties of real
numbers, but we know nothing about their construction. And then carry out
all proofs about real numbers generally for any element of this type,
rather than for a particular construction of real numbers.

For me this has advantages of both worlds: the "material" layer of
witnesses is used (and needed) to "compile" everything all the way down to
the good old ZFC (or NBG, TG, etc) whenever we are not sure what the
abstract theories/structures are talking about and to tell us if there are
any models at all. And the structural layer allows generalization.

Josef


On Fri, May 3, 2019 at 8:49 PM Joshua Chen <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
> Web: https://joshchen.io
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20190506/1cdeddc0/attachment.html>