[Note! A more updated account on the following is present in the pdf article attached at he bottom of this page]
The following is a presentation of an axiom schema that generalizes some results from the hereditarily finite realm to the whole realm of sets.
The object language of our theory is: first order logic with identity and membership. The term "formula" shall be reserved here to mean a formula of the object language, so atomic formulas are of two kinds: x in y ; x=y.
A metaformula is an expression belonging to the metalanguage, so it ranges (i.e. is substituted by) formulas of the object language. We have two main kinds of atomic metaformulas, those are: Q(y,x1,..,xn) ; F!(y,x1,..,xn)
The first ranges over all formulas of the object language having y,x1,..,xn as the sole variable symbols occurring free in them.
The second ranges over all formulas of the object language of the form
([Exist!z Q(z,x1,..,xn)] & Q(y,x1,..,xn))
So it ranges over formulas defining functions.
Rules of formation of metaformulas:
If Q is metaformula then ¬Q is a metaformula
If Q,P are metaformulas then Q -- P is a metaformula
If Q(x1,..,xn) is a metaformula then qxi(Q(x1,..,xn)) for i=1 or i=2.. or i=n is a metaformula
If Q is a metaformula then renaming some or all of its variables in such a manner that all occurrences of the same variable are renamed by the same symbol, results in a metaformula.
If P is a formula and Q is a metaformula then P -- Q is a metaformula.
"--" denotes a binary logical connective and q denotes a quantifier symbol.
An "atomic expression" is an atomic formula or an atomic metaformula.
[Phi]B denotes bounding all quantifiers in Phi (or in formulas substituting Phi) by the set B.
Axiom scheme of Extrapolation: If phi is a formula of the object language having no more than two atomic formulas occurring in it, where the sole variable symbols occurring free in it are y,x1,..,xn; then if n=0,1,2 we have:
[For all x1..xn Exist x for all y (y in x <-> phi)]HF
->
For all x1..xn Exist x for all y (y in x <-> phi)
is an axiom.
Where HF is the set of all hereditarily finite sets.
Axiom scheme of Meta-Extrapolation: If phi is a metaformula having no more than two atomic expressions occurring in it where the sole variable symbols occurring free in it are y,x1,..,xn, then if every sentence substituting the metaformula:
[For all x1..xn Exist x for all y (y in x <-> phi)]HF, is a theorem,
then every sentence substituting the metaformula:
For all x1..xn Exist x for all y (y in x <-> phi)
is an axiom.
This straightforwardly proves all axioms of ZF-Regularity!
If we upgrade the above scheme to allow three occurrences of atomic expressions (preferably with a single occurrence of a metaformula) instead of just two, then there will be no need for the first Extrapolation axiom scheme, since we can have the following forms of replacement schemata:
For all A Exist B for all y (y in B <-> Exist x in A (y in F!(x)))
For all A Exist B for all y (y in B <-> Exist x C A (F!(y,x)))
where C is the known subset relation.
The first proves Empty set, Separation and Set Union.
The second proves Pairing and Power.
Of course the above schemata are to be added to a theory that can formalize the concept of hereditarily finite sets, an example of such theory would be the first order set theory with the following axioms:
1.Extensionality: as in Zermelo set theory.
2. Infinity: There exists a set that is closed under existence of singletons and Boolean unions, and has an empty element.
We denote any set satisfying the property of axiom of Infinity as: inductive set.
3. Inductive Separation: if X is an inductive set then there exist a set {y|y in X phi} for every formula phi.
HF would be defined as the intersection of all inductive sets.
This method does extrapolate FUNDAMENTAL "set" properties from the hereditarily finite set realm to the whole set realm, the naive*form of set construction and the question of what defining formula "phi" is to be used in it in order to construct sets is definitely a pure general question of set theory, not of finiteness or anything else, and limiting the size of the defining formulas not to exceed 2 atomic subformulae (i.e. atomic size* = 1 or =2) definitely restricts us to properties of sets, since property of finiteness need a lot of atomic formulas to be defined using sets, also limiting the schematic expression to having the defining expression not containing occurrences of atomic expressions more than an atomic formula and an atomic metaformula is also definitely a question about pure schematic comprehension over sets, since the metaformula part would range over the whole realm of formulas or of functions of the same arity and this would cast away any appeal to a particular concept whether that was finiteness or another particular aspect, and since the other formula is just a simple atomic formula, so this restriction does cast away any property other than that of constructing sets by individual axioms or schematically, which is a fundamental set property; so this method does address the "fundamental" aspect of properties extrapolated (transferred) to outside of the realm of hereditarily finite sets.
That ZF can be proved to be resulting from such a transfer of fundamental set properties from the hereditarily finite realm to the whole set realm is something that boosts our belief in consistency of ZF.
Zuhair Al-Johar
Aug. 26, 2016
* the naive form of set construction is the following:
for all x1..xn Exist x for all y (y in x <-> phi)
x1..xn are the parameters, x is the asserted set, y is the set builder variable and phi is the defining expression whether it is a formula or a metaformula.
*atomic size is the total number occurrences of atomic expressions in a formula or a metaformula, and here in both schemata it must not exceed 2.
Addendum:
Let "pure metaformula" mean a metaformula having all of its atomic expressions being metaformulas.
A schema of Pure meta-Extrapolation might be contemplated having the same form of schemata presented above with the only difference of its defining expression phi being a pure metaformula of any size.
I don't know if this is decidable, anyhow I think it would be safe.
Zuhair Al-Johar
Sept. 4, 2016