Note: whenever n appears undefined then it range over the set {1,2,3,...}, same applies to i.

Language: L(w1,w)

L= first order logic with identity "=" and membership "e".

Extensionality: (for all z. z e x <> z e y) > x=y

Formation of finites: Exist x1...xn phi> y=x1 or...or y=xn > Exist x for all y. y e x <> phi
where x is not free in phi.

Define: x is finite <> \/n Exist z1...zn for all y. y e x > y=z1 or ... or y=zn

Define: x is well founded finite<> x is finite & x is acyclic & x has limited depth

Define: x is acyclic<> /\n ~Exist x1...xn.  x e x1 & ... & xn-1 e xn & x=xn

Define: x has limited depth <> \/n (~Exist x1...xn. x1 e x2 & ...& xn-1 e xn & xn e x)

Define: x is hereditarily finite <> /\n for all x1..xn. x1 e x2 &...& xn-1 e xn & xn=x > x1 is finite

Universe of hereditarily finites:Exist x for all y. y e x <> y is well founded hereditarily finite set.

Define: x=W <> for all y. y e x <> (y is well founded finite & y is hereditarily finite)

So W is the set of all well founded hereditarily finite sets.

Separation: for n=0,1,2,... if phi is any finitary formula in which z is free and y not, in which w1...wn are
its sole parameters, then

for all x for all w1 e x...wn e x. Exist y. y={z| z e x & phi}

is an axiom.

Formation of higher Infinites: if {phi_1(z,w1..wm), phi_2(z,w1,..wm),....} is the set of all finitary formulas in L(w1,w)
with equality and membership in which z is free but y not free,having w1...wm as their sole parameters, then

for all x Exist Px for all y. y e Px <> y subset of x & \/m=0,1,2,3,... Exist w1 e x...wm e x. \/n=1,2,... y={z| z e x & phi_n(z,w1...wm)}

is an axiom.

So PW would be the set of all subsets of W that are definable by finitary formulas in a predicative manner, and it is provably countable!

Define (P_i):
P_1 W = W
P_i+1 W = P P_i W

Now each P_i W is provably countable!

Restriction: for all x. \/i x e P_i W

/ Theory definition finished.

Now the naturals can be defined as well founded finite ordinals, this is done by substituting the formula " z is transitive & for all m e z. m
is transitive"  in Separation with x=W, so we'll have the set of all finite well founded ordinals which is the set of all natural numbers N.

The set R of all reals is a subset of PW that is defined as the set of all subsets of N that are definable after finitary formulas with
parameters standing for well founded hereditarily finite sets. One can call it the set of all predicatively definable Reals. Higher Reals
can be defined in this manner as well.

If there is no obvious inconsistency with this theory then I tend to think it is a subset of second order arithmetic sufficient to 
formulate size-able amount of mathematics in it. 


Zuhair
June 21, 2012