Axiomatic ZFC

Hello, all!
Is this meaningful way to do ZFC set theory “from inside” in Coq? https://pastebin.com/cauVSRf1

Also, I can’t find a way to prove last theorem named ‘subset_of_singleton’. Is it because I’m not clever enough or maybe I have made a mistake somewhere before? Thanks in advance.

There are antecedents.

You can have a look at https://github.com/coq-contribs/cats-in-zfc (the first files are in order axioms.v tactics.v and set_theory.v, read tactics.v just to know what the tactics in the others mean). The pdf in that repo looks like it’s broken, get it from https://arxiv.org/abs/math/0410224 instead.

Years ago I played around with it and made it more axiomatic (eg instead of Definition E := Type. for the type of sets I have Axiom E : Type., so you have to use the ZF axioms on it instead of inductive types etc), you can have a look at https://github.com/SkySkimmer/ZF (quality not guaranteed, doesn’t compile with current Coq).

Also, I can’t find a way to prove last theorem named ‘subset_of_singleton’. Is it because I’m not clever enough or maybe I have made a mistake somewhere before? Thanks in advance.

You have excluded middle (classical logic) so you can ask whether {a} belongs to x. The answer lets you know if x is supposed to be empty or {{a}}. Proceed from there.

BTW consider using more informative theorem names than E1214 or T3.

1 Like

There’s a formalization in HoTT, most of this (quotients, …) should also work if you use classical logic.
The main idea is to encode sets-as-trees using W-types.


The approach is described in the HoTT book.

Another overview:
https://www.ps.uni-saarland.de/settheory.html

1 Like

There’s also http://www.lix.polytechnique.fr/~barras/proofs/sets/ (https://doi.org/10.6092/issn.1972-5787/1695)

1 Like

Thank you all for the answers!

Thank you, it helped!

Definitely will make better theorem names in future. It was the first iteration with exercises and theorems taken from some book (E were exercises, T - some theorems).

Hi! :v:

Just a remark that the natural axiomatisation of ZFC in a dependent type theory you follow is in fact stronger than the usual formulation as a first-order theory. Since your replacement axiom quantifies over all relations and not only the first-order definable ones, it only admits the standard models V_\kappa for \kappa inaccessible.

That the models of this higher-order axiomatisation only differ in height has been observed by Zermelo in his 1930 paper “Über Grenzzahlen und Mengenbereiche” and we have formalised the result in Coq (https://link.springer.com/article/10.1007%2Fs10817-018-9480-6). Our development also contains model constructions a la Aczel/Werner/Barras for the first \omega inaccessibles.

If you are interested in the first-order model theory of ZFC, I guess you’ll have to make the syntax explicit and weaken the replacement axiom accordingly. This has for instance been done in Lean to get a model contradicting the axiom of choice (https://arxiv.org/abs/1904.10570).

1 Like

The abstract says the paper is about the Continuum Hypothesis.
Forcing can naturally be presented using higher order logic (toposes) and it even works for higher toposes (“models of HoTT”), so another route is also available. In fact, this is related to the various “translations” of type theory studied in Nantes.