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).
On 8/3/25 17:43, 'ML' via Metamath wrote:
I would like to propose two changes to the set-theoretic axioms of
set.mm, in order to help reduce axiom usage and provide more
fine-grained control over the consistency strength of the theory being
worked in.
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
--
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 visit
https://groups.google.com/d/msgid/metamath/76558c28-e589-46c1-aea0-60f800202e0cn%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/76558c28-e589-46c1-aea0-60f800202e0cn%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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 visit
https://groups.google.com/d/msgid/metamath/eca4a5e4-7445-46c4-ac04-c0c28a452c5c%40panix.com.
