Hi Scott, I'm not sure which axiomatization you're talking about, I found a Coq paper with an axiomatization of the hereditarily finite sets <https://www.ps.uni-saarland.de/Publications/documents/SmolkaStark_2016_Hereditarily.pdf> which I believe can be done very similarly to set.mm, using wff's and setvar's, but defining an "adjunction" predicate instead of the membership predicate, and formulating the axioms with those. That paper does not include any axiom about equality, but you'll probably need some axiom of the form ` |- ( x = y -> ( x . z ) = ( y . z ) ) `
In any case, Mario is also using *terms* in his HOL database <http://us2.metamath.org:88/holuni/mmhol.html#axioms>. BR, _ Thierry -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/8f88631e-08cb-4c0c-99aa-b39a1a2b3e56%40gmx.net.
