[FOM] Simple Para-Type Theory "SPT".

[Zuhair Abdul Ghafoor Al-Johar]

The following theory is defined with the aim of being equi-consistent with
TSTU+infinity. It doesn't use typed language, nor any restriction on 
quantifiers, and it is defined in first order logic with equality and
membership, so its defined in the same language of Z. The ontology of this
theory is that of sets and ur-elements, the later are defined as distinct 
empty objects. Extensionality of this theory is the same as in NFU, i.e.
any two non empty sets are equal if and only if they have the same 
members. The structure of the theory is very simple, we have infinitely
many empty objects, the set of all those objects is the base tier, then 
upper tiers of sets are constructed by a special sort of powering starting
from the base tier. Separation holds as in Zermelo's. All sets belong to 
some tier.


Axioms: 

1.Extensionality: as in NFU

2.Base: Exist x. for all y. y in x iff not Exist z. z in y

Define: x=O iff for all y. y in x iff not Exist z. z in y

3.Power: for all s. Exist x. for all y. y in x iff y is non empty subset of s

Define: P(s)=x iff for all y. y in x iff y is non empty subset of s

4.Separation: as in Z.

5.Axiom of Regularity: for all x. Exist i. x in P_i (O).

where P_i (O) is defined recursively as:

P_i (O) = O, when i=0
P_i (O) = P( P_i-1(O)), for every natural number i>0.

natural numbers are defined in the usual way done in type theories.

Necessary forms of Choice can be added to the above theory.

 Since most ordinary mathematics can be implemented in TST(U)+infinity.
Then if the above theory is equi-consistent with TSTU+infinity, then it 
can be used to implement ordinary mathematics. The basic merit of this 
theory is that it has simpler structure than typed theories and NFU, it
doesn't use any typed language, Extensionality is very simple compared to
those used in type theories, there is no restriction at all on quantifiers
in formulas, and the structure of the theory is dead simple. It is also 
strictly weaker than Z, so it is safer as far as the question of 
consistency of these theories is concerned.

Zuhair