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.
