Proposal for two changes to the set axioms of set.mm
ML
These changes would have the disadvantage of moving the database a bit further away from the textbook presentation of ZFC, but I think the upsides are large enough to make the change worth it.
---
The first change is to replace the Axiom of Pairing with the Axiom of Adjunction. The Axiom of Adjunction asserts that for any two sets x and y, ( x u. { y } ) is a set, and can be stated this way:
```
|- E. z A. w ( w e. z <-> ( w e. x \/ w = y ) )
```
The combination of the axioms of Extensionality, Empty Set, and Adjunction is known under various names, but here I will refer to it as Adjunctive Set Theory (AST). AST is known to be mutually interpretable with Robinson arithmetic[1], a weak fragment of Peano Arithmetic which is still strong enough that Godel's incompleteness theorems apply to it.
Adding the Axiom Scheme of Separation to AST gives General Set Theory (GST), a theory known to be mutually interpretable with Peano arithmetic[2].
It should also be noted that the Axiom of Pairing requires the Axiom of Union in order to prove Adjunction, so adding Adjunction also helps avoid Union, which will be especially important later on.
---
The second change is to modify the Axiom of Infinity. The standard version of the axiom says that there exists a set which contains the empty set and which is closed under the successor operation. The new version would instead assert that it is closed under adjunction.
In other words, the axiom would change from this:
```
ax-inf2
|- E. x ( E. y ( y e. x /\ A. z -. z e. y ) /\
A. y ( y e. x -> E. z ( z e. x /\ A. w ( w e. z <-> ( w e. y \/ w = y ) ) ) ) )
zfinf2 (with abbreviations)
|- E. x ( (/) e. x /\ A. y e. x suc y e. x )
```
To this:
```
ax-inf3
|- E. x ( E. y ( y e. x /\ A. z -. z e. y ) /\
A. y A. v ( ( y e. x /\ v e. x ) -> E. z ( z e. x /\ A. w ( w e. z <-> ( w e. y \/ w = v ) ) ) ) )
zfinf3 (with abbreviations)
|- E. x ( (/) e. x /\ A. y e. x A. z e. x ( y u. { z } ) e. x )
```
The modified axiom can be thought of saying "the class of all hereditarily finite sets is a set", or "in the von Neumann hierarchy of sets[3], V_om (step omega) is a set".
I will call GST plus this modified Axiom of Infinity "IST". IST has equivalent strength to Second-order arithmetic.
One of the very nice advantages of this is that if two sets x and y are hereditarily finite, then so is the Kuratowski ordered pair <. x , y >. . This means that ( V_om X. V_om ) is a subset of V_om, and IST proves that all relations on V_om are sets, including relations on the natural numbers _om . Using the standard Axiom of Infinity, it is not possible to prove this without using the Axiom Scheme of Replacement.
Note that from the point of view of consistency strength, the modified Axiom of Infinity is not stronger than the standard one: using encodings of pairs of natural numbers as numbers, it is possible to prove that "relations" on the natural numbers exist as subsets of _om . But while in English it is easy to handwave away the precise method of encoding pairs of numbers and relations, in a formal system like Metamath where no detail can be omitted, encoding pairs and relations this way would entail a massive amount of extra work, which this modified axiom allows us to avoid entirely.
---
If we add the Axiom of Power Set to IST, we get a new theory, which I will call PST. Notably, PST is mutually interpretable with Zermelo set theory (ZF without Replacement), but avoids the Axiom of Union!
Since IST proves that V_om exists, using the Axiom of Power Set, we can prove V_( _om +o n ) exists for every natural number n . Therefore V_( _om +o _om ) is a definable class, which is known to be a model of Zermelo set theory[4]. This demonstates that Zermelo set theory is interpretable by PST. I believe that the reverse direction is more or less the same, except that it requires some contortions to encode hereditarily finite sets as natural numbers.
---
At this point, we have seen four simple set theories of increasing consistency strength, each one building on the last by adding one axiom. These are AST, which has the axioms of Extensionality, Empty Set, and Adjunction, and gives us Robinson arithmetic; GST, which adds the Axiom Scheme of Separation and gives us Peano arithmetic; IST, which adds the modified Axiom of Infinity and gives us Second-order arithmetic; and PST, which adds the Axiom of Power Set and gives us Zermelo set theory.
Of course, adding the axioms of Union and Replacement to PST gives us back ZF (minus Regularity), which gives us a fifth tier of consistency strength. And as usual, Regularity and Choice can be used or avoided as desired in any of these theories.
To sum up the advantages, these two changes provide a hierarchy of theories with fine-grained control over consistency strength. Each level of this hierarchy builds on the last, so all theorems from the previous level of the hierarchy automatically transfer over to all later levels. In addition, the modified Axiom of Infinity allows us to either avoid many cases of Replacement, or to avoid the large amount of work that encoding pairs and relations as numbers would entail.
For these reasons, I think these changes would be beneficial to Metamath. But regardless of how this proposal turns out, if you have read this far, thanks for reading, and I hope it was educational in some way.
[1] https://en.wikipedia.org/wiki/Axiom_of_Adjunction#Interpretability_of_arithmetic
[2] https://en.wikipedia.org/wiki/General_set_theory#Axioms
[3] https://en.wikipedia.org/wiki/Von_Neumann_universe
[4] https://en.wikipedia.org/wiki/Zermelo_set_theory#The_aim_of_Zermelo's_paper
Jim Kingdon
Looks like interesting material which would be nice to have in set.mm (in a mathbox or otherwise) one way or another.
In fact we seem to have something on the topic already at
https://us.metamath.org/mpeuni/ax-bj-adj.html although I didn't
look into detail on what is currently in set.mm.
The discussion of how we treat alternate axioms in set.mm gets a little into the weeds of what the tools can do and how we structure things, so let's start with ax-pr . This is not an axiom in the sense of being listed at https://us.metamath.org/mpeuni/mmset.html#staxioms - it is proved from other axioms at https://us.metamath.org/mpeuni/axpr.html and in fact those are tied together in a machine-parseable way via "$( $j restatement 'ax-pr' of 'axpr'; $)"
So basically there isn't a need for "two changes to the set-theoretic axioms of set.mm" but instead this sort of exploration can be done in sections analogous to "Other axiomatizations related to classical propositional calculus" (currently at https://us.metamath.org/mpeuni/mmtheorems17.html#mm1616b ), "Other axiomatizations related to classical predicate calculus" ( currently at https://us.metamath.org/mpeuni/mmtheorems27.html#mm2655b ), "ZFC Axioms in primitive form" (currently at https://us.metamath.org/mpeuni/mmtheorems356.html#mm35561s ), "ZFC Axioms with no distinct variable requirements" (currently at https://us.metamath.org/mpeuni/mmtheorems107.html#mm10637b ), etc.
Doing this in a dedicated section is especially appealing insofar
as the treatment diverges from "the textbook presentation of ZFC"
(although referring to "textbook presentation" can be a bit hard
here as textbooks tend to differ from each other, especially on
minor notational details but also on things like whether pairing
is an axiom or a theorem).
--
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 metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/76558c28-e589-46c1-aea0-60f800202e0cn%40googlegroups.com.
ML
> In fact we seem to have something on the topic already at https://us.metamath.org/mpeuni/ax-bj-adj.html although I didn't look into detail on what is currently in set.mm.