Skip to content
Playing around with axiomatic set theory in Coq
Coq Makefile
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
.gitignore
LICENSE
Makefile
README.md
aac.v
axioms.v
cardinal.v
classes.v
dedekind.v
functions.v
graph.v
lci.v
nnum_base.v
ordinal_arith.v
ordinals.v
qembed.v
qfrac.v
qtemp.v
quotient.v
raxioms.v
ring.v
tactics.v
utils1.v
zorn.v
ztemp.v

README.md

This is stuff I did as a master student to help me understand set theory and Coq at the same time. This was around 2012-2013.

Given the timing it's probably compatible with Coq 8.4 or maybe 8.3, I don't have either at hand to test.

I started from someone else's development and played with it as I liked. I didn't write down where I got it from, but since the shortened tactics (ir for intros, ap for apply, etc) and some lemma names survived my changes we can tell it was probably https://github.com/coq-contribs/cats-in-zfc (original author Carlos Simpson, see also paper https://arxiv.org/abs/math/0410224 and https://math.unice.fr/~carlos/old/indexFev07.html which has history from before the svn to git import). LICENSE is accordingly LGPL2.1.

Some differences:

  • cats-in-zfc has a mix of axiomatic ZFC and using Coq types as sets, i.e. they have Definition E := Type. and then some extra axioms on E. I have purely axiomatic E with Coq serving as the metatheory.

  • cats-in-zfc have some stuff in their notation.v to embed methods in their sets or something. I didn't understand it back then (and remember even less now) so I removed it and refactored or removed its users. (the previous point may not have been possible without this change by the way)

  • as indicated by the name cats-in-zfc is about categories. I didn't know or care about categories so I deleted those files. Instead I have some trivialities about numbers in set theory.

  • probably some other stuff that I forgot about.

You can’t perform that action at this time.