Language: first order logic with identity and membership having infinitely many sorts and also non sorted variables.
Atomic formulas are of the following general forms:
for i=0,1,2,3,...; j=0,1,2,3,...
x_i = x_j ; x_i E x_j
x_i = y; y=x_i ; x_i E y , y E x_i,
x = y, x E y.
formula formation rules are the customary ones,
substitution rules are also the customary ones,
Inference rules:
1. Modus Ponens
2. Generalization by drop of indices.
Axioms: Identity axioms +
1. Sorting: for i=0,1,2,3,....
for all x_i Exist x_i+1 (x_i = x_i+1)
2. Extensionality: for i,j=0,1,2,3,...
for all x_i+1,y_i+1
(for all z_i (z_i E x_i+1 <-> z_i E y_i+1) -> x_i+1 = y_i+1)
3. Comprehension: for i=0,1,2,3,...; n=0,1,2,3,...,
if phi^i(y_i,w1_i,..,wn_i) is a formula in which all and only
symbols y_i,w1_i,..,wn_i occur free, and such that all of its bound variables are of sorts strictly below i+1, then:
for all w1_i,...,wn_i Exist x_i+1
for all y_i (y_i E x_i+1 <-> phi^i(y_i,w1_i,..,wn_i))
is an axiom
Define: for all y E x|phi(y) to mean for all y (y E x <-> phi(y))
Define: for i=0,1,2,....
2^^0 =1
2^^(i+1) = 2^(2^^i)
4. Exactness for i=0,1,2,3,...,n , for n=1,2,3,...,2^^i
Exist "exactly" x1_i,...,xn_i (x1_i =/=...=/=xn_i)
Rule of Generalization by drop of indices:
For n=0,1,2,3,...; IF phi(y,w1,..,wn) is a formula in which
all and only symbols y,w1,..,wn occur free, THEN
IF (for i=0,1,2,3,...; if phi(y,w1_i,..,wn_i) is the
formula obtained from phi(y,w1,..,wn) by indexing
all symbols w1,..,wn with i, and if phi^i(y_i,w1_i,...,wn_i)
is a formula obtained from phi(y,w1_i,..,wn_i) by indexing y with i and indexing all bound variables by naturals less than or equal i, we have:
[for all w1_i,...,wn_i Exist x_i+1:
for all y E x_i+1|phi(y,w1_i,...,wn_i) ^
for all y_i E x_i+1|phi^i(y_i,w1_i,..,wn_i)]
is a theorem)
THEN we infer that:
(for all w1,...,wn Exist x for all y E x|phi(y,w1,..,wn)
is a theorem)
/Theory definition finished.
It is nice to see how this theory avoids the known paradoxes, for example using formula y_i=y_i; y_i is an i-ordinal; ~y_i E y_i; y is well founded, y is 0 or an i_limit ordinal, etc.. all of those formulas would violate the antecedent of the generalization rule because clearly no x_i+1 set can contain all objects fulfilling those properties after drop of indices!
However a challenge to this method are formulas containing sub-formulas that might imply finiteness or infiniteness, however finiteness over the i_th sort is prevented by the predicative restriction (no sort strictly higher than i), and finiteness of objects of sorts lower than i would not give the same asserted x_i+1 set when indices are dropped (removed), so the frank cases of them are prevented, however there might be subtle ways in which finiteness or infiniteness can seep through that might eventually cause paradoxes.
It would be nice really to see if that theory can be interpreted in ZF?
However this theory clearly interpret ZF if axiom of infinity is added to it.
ANOTHER VERSION
An attempt to generalize some properties from the hereditarily finite realm "HF" to the whole world V of sets. The basic idea here is that any sentence of the form:
for all x1,...,xn exist x for all y (y in x <-> phi(y,x1,..,xn)),
that holds true over HF (i.e. when all of its quantifiers are bound to HF), if its defining expression "phi(y,x1,..,xn)" does not mention finiteness; then it holds true over V. Mentioning finiteness is formalized here as "having a subformula pi of phi such that:
"for all x (pi(x) -> x is finite) or for all x (pi(x) -> x is infinite)",
with the order of quantification of variables in pi being the same as that in phi.
where finiteness is defined as being bijective to a natural von Neumann ordinal in HF. Where a natural von Neumann ordinal is defined as a well founded transitive set of transitive sets, that do not have more than one empty set among its elements, that is a successor having every non empty element of it being a successor. HF is taken here to mean the minimal set closed under singletons and Boolean unions with the provision of existence of infinitely many empty sets (i.e. for n=1,2,3,...; if x1,...xn are empty then there exists xn+1 that is empty and not equal to any of them), while maintaining Extensionality over non empty sets. In a prior attempt I tried to define HF in the usual manner as the standard V_omega, however this failed! due to uniqueness of (zero or limit ordinals) in V_omega, and for similar reasons ordinals not having an n_th iterative predecessor would also be unique in V_omega. The addition of infinitely many empty sets here would (hopefully) serve to handle this objection.
This would prove all axioms of ZF-infinity-foundation-choice.
Zuhair Al-Johar
April 5 2017