FORMATION SET THEORY
Language: first-order logic with identity and membership
Axioms: in addition to ID axioms and Extensionality, we have:
1. Empty set exists (denote it by 0)
2. for every ordinal n (a well-founded transitive set of transitive sets) there exists a set I_n of unordered pairs of elements of n and power sets, such that for every elements m,m+1 of n there exists a set z such that there exists sets {0}, {m,z}, {m+1, P(z)} that are elements of I_n, and such that no distinct elements of I_n share the same element of n as an element of them.
3. For every ordinal n exists UU(I_n)
Define: x is the n_th iterative power of 0 <-> Exist y (y=I_n ^ x=UU(I_n))
where U signifies set union
4. for every ordinal n, there exists a set of all ordinal subsets of the n_th iterative power of 0.
5. There exists a union set of all finite iterative powers of 0.
6. for every set x there exists an ordinal n such that x in the n_th iterative power of 0.
Define (Rank): i=Rank(x) <->
x subset_of the i_th iterative power of 0 ^
for all j (x subset_of the j_th iterative power of 0 -> i subset_of j)
i.e. the rank of a set is the ordinal index of the least iterative power of 0 having x as a subset of.
7. Predicative Formation: if phi^n(y) is a formula in which (y,z1,..,zm) are the sole free variables occurring in it, and such that all quantifiers in phi are of ranks smaller than n (i.e. of the forms: All x (Rank(x)<n ->); Exists x (Rank(x) < n ^)), then
for every ordinal n
(All z1,..,zn have ranks =< n ^
for all y (phi^n(y) -> y < n) ^
not exist ordinal d < n for all y (phi^n(y) -> y < d)
->
Exist x (rank(x) = n ^ for all y (y in x <-> phi^n(y)))
is an axiom.
A stricter version is not to allow parameters to have ranks equal to the asserted sets, with the exception of parameters bounding a quantified variable in phi^n(y), which can be of the same rank of the asserted set.
/Theory definition finished.
Another form of the theory having the same general grounds
N for Number, T for Type (a one place FUNCTION), < for is strictly smaller than.
Axioms
x < y -> N(x),N(y)
Define y > x iff x < y
Exist x (N(x) for all y (N(y) -> y >=x)
For all xy, for all m<x -> m<y -> x=<y
x < y -> not y < x
x < y , y < z -> x < z
for all x Exist y (x<y ^ ~ exist z x < z < y)
N(0), N(w)
0 < w for all x < w -> S(x)<w
for all x (0 < x ^ for all y < x -> S(y) < x -> x=<w)
Omega rule:
phi(i)
phi(Sn(i)) for each n=1,2,3,.......
_______________________________
for all x>=i ,x<w phi
phi(w+i)
phi(Sn(w+i)) -> for each n=1,2,3,...
------------------------------------------
for all x>=w+i, phi(x)
Extensionality: as in Zermelo
phi(y) is a formula in which every quantifier Ax, Ex is followed by (T(x)<n ->...),(T(x)<n ^ ...) respectively
and in which y,x1,..,xm are its sole free variables, then
for all x1,...xm [
T(x1)<n,...,T(xm)<n ^
for all y (phi(y) -> T(y)<n) ^
for all k (for all y(phi(y) ->T(y)<k) -> n=<k)
->
Exist x (T(x)=n ^ for all y (y in x <-> phi(y))]
is an axiom.
--------------------------------------------------------------------
Another form of this theory with a more strict typed milieu.
I'm trying to coin a predicative type theory of a special kind, a real predicative type theory.
IDEA: the basic types are meta-theoretic in the usual manner written as superscripts. we have 0,1,2,3,..., w, w+1, w+2,.... types and the metatheoretic relations of <,> = and =/= are understood in the standard manner.
Now we have two kinds of typing here, one is symbolized by ordinary superscripts like x^3 (the symbol ^ indicating superscript as in Latex), x^3 is a variable symbol ranging over type 3 objects. All types of that sort are DISJOINT. Those types I call as "Basic types". However, there is another sort of typing which I call as "accumulative types", here this is symbolized as x^<3, those variables with italic superscripts denote the union of all basic types below the italicised superscript, so x^<3 range over all of what x^0, x^1, x^2 range over and only over those. Another example x^<w which does range over all and only objects of the natural type.
There are no special syntactical restriction other than every variable must be indexed with superscript whether in basic type or in accumulative type ways.
Axioms:
[1] for i=1,2,3,..., w, w+1,...; for j=0,1,2,3,...,i
for all x^j Exists x^<i (x^i = x^j)
[2] for i=1,2,3,.... , for j=i, i+1, i+2,...,w, w+1, w+2,...
for all x^j ~Exists x^<i (x^i = x^j)
[3] for i=w,w+1, w+2,....., for j=i, i+1, i+2,.....
for all x^j ~Exists x^<i (x^i = x^j)
[4] for i=1,2,3,...., w, w+1,w+2,.....
Exists x^<i (x^<i E x^i)
[5] for j>=i:
~Exists x^j (x^j E x^i)
[6] for i=/=j
~ x^i = x^j
[7] for j=1,2,3,.......,w,w+1,w+2,....
for all z^<j (z^<j E x^j <-> z^<j E y^j) -> x^j = y^j
[8] for i=0,1,2,3,......w,w+1,.... ; for j<i
for x^i ~Exists x^j for all x^<i (x^<i E x^i -> x^<i = x^j)
[9] Predicative formation: if phi^i is a formula in which all bound quantifiers
are of accumulative type ^<i or basic type ^j for j<i and in which y^jr, z1^jr,..,zm^jr
are all of its free variables,
for jr=0,1,2,3,...,i-1 , r=0,1,2,3,...,m
for all z1^j1,...,zm^jm (~for all y^<i (Phi(y^<i) -> exists x^<i-1 (y^<i = x^<i-1) )
-> exists x^i for all y^<i (y^<i E x^i <-> phi(y^<i))
is an axiom.
jr=0,1,2,3..., r=1,2,,,m
for all z1^j1,...,zm^jm for all y^<w (Phi(y^<w) -> exists x^<w (Phi(x^<w) ^ y^w within (x^<w) )
-> exists x^w for all y^<w(y^<w E x^w <-> phi(y^<w)))
is an axiom.
Define y^i within (x^i) <-> for all k^i[ (for all p^<i, q^<i(p^<i E q^<iEk^i -> q^<i E k^i)
^ for all m^<i E x^i (m^<i E k^i) -> z^<i E k^i).
----------------------------------------------
Another theory is the following:
1) For i ≠ j; i,j=0,1,2,3,…..
xi ≠ xj
2) for j>=i; i,j=0,1,2,3,……,
xj ∉ xi
3) for i=1,2,3,….
∀ xj<i (xj<i ∈ zi ⇔ xj<i ∈ yi) ⇒ zi = yi
4) for i=1,2,3,.............
∀xi ∃xi-1 (xi-1 ∈ xi)
5) for i=1,2,3,...; if φ is a formula in which all of its bounded variables
have types less than i, and in which only u1j<i ,..., unj<i occur as parameters,
then:
∀u1j<i ,..., ∀unj<i
[∃yi-1 φ(yi-1) ⇒ ∃xi ∀yj<i (yj<i ∈ xi ⇔ φ(yj<i))]
is an axiom.
A less strict version is to allow parameters to be of the same type of the asserted set, i.e the parameter string will be: ∀u1j=<i ,..., ∀unj=<i
other versions can be done in a language that does not allow identity to be symbolized between variables of different types, nor membership of a higher type variable in an equal or lower type variable, so all those will be forbidden from the language, and we can even delete axiom 4, so what we are left with from the above axioms is only the extensionality and comprehension axiom plus the following ones
6) ∃x0 ∀y0: ~ S(y0)=x0
7) S(x0)=S(y0) ⇒ x0= y0
8) Induction over type zero objects.
/ Theory definition finished.
A kind of predicative type theory with sets having members of lower types provided that there is at least one element of the immediately prior type.
So this theory can be abbreviated to the following:
Language: omega multi-sorted first-order logic, syntactical restrictions involves not allowing formulas of the form x^i = x^j if i=/=j, nor allowing formulas of the form x^i E x^j if i=>j, so we only allow x^i E x^j if i<j.
The least type allowed is type zero, so no variable is indexed by negative types and so occurrence of a symbol indexed with 0 is not allowed on the right of the membership symbol E. Also the successor symbol is unary function symbol restricted to type zero variables, Also we add the constant
symbol O.
Axioms:
[1] Extensionality: for i=1,2,3,…
∀x^j<i (x^j<i ∈ z^i ⇔ x^j<i ∈ y^i) ⇒ z^i = y^i
[2] Comprehension: for i=1,2,3,...; if φ is a formula in which all of its bounded variables have types less than i, and in which only u1^j<i ,..., un^j<i occur as parameters, then:
∀u1^j<i ,..., ∀un^j<i
[∃y^i-1 φ(y^i-1) ⇒ ∃x^i ∀y^j<i (y^j<i ∈ x^i ⇔ φ(y^j<i))]
A less strict version is to allow parameters to be of the same type of the asserted set, i.e the parameter string will be: ∀u1^j=<i ,..., ∀un^j=<i
An even less strict version is to remove the
restriction on the left and thus converting it to the usual type theory but extended with set over lower types.
[3] Zero: ∀x^0 [~ S(x^0)=O]
[4] Succession: ∀x^0 ∀y^0 [S(x^0)=S(y^0) ⇒ x^0 = y^0]
[5] Induction: if φ is a formula, then
φ(O) ^ ∀x^0[φ(x^0) ⇒ φ(S(x^0))] ⇒ ∀y^0[φ(y^0)]
/ Theory definition finished.
In order to clarify matters, the superscript j<i refers to all types lower than i. so y^j<i is meant to be substituted by every object belonging to a type strictly lower than i. Of course, it can be eliminated completely as:
∀y^j<i [φ(y^j<i)] ⇔ ∀y^1..∀y^i-1 [φ(y^1) /\ ../\ φ(y^i-1)]
A kind of predicative type theory with sets having members of lower types
provided that there is at least one element of the immediately prior type.
It extends PA with predicatively constructed tiers of sets. I'm not sure if Feferman's arithmetic can be interpreted here?
I think that such a theory is very robust. I'm not sure of its strength really. Cantor's argument for uncountability of the reals is blocked
by this strict predicative approach, so all sets can be imaged to be definable after a parameter free formula, and thus all sets are countable.
Zuhair
____________________________________________
This is my favorite kind of PREDICATIVE type theory, I think it is stronger than Russell's ordinary predicative type theory since it allows intersectional definitions. This theory is more like the constructible universe of Godel up to Lw+w
Language: omega multi-sorted first-order logic, syntactical restrictions involves not allowing formulas of the form x^i = x^j if i=/=j, nor allowing formulas of the form x^i E x^j if i=>j, so we only allow x^i E x^j if i<j.
The least type allowed is type zero, so no variable is indexed by negative types and so occurrence of a symbol indexed with 0 is not allowed on the right of the membership symbol E. there is also another kind of sorting denoted by superscript (j<i) where i>0, so x^(j<i) is taken to range over all of what x^j for j<i range over. Here with this kind of sorting there is a syntactical restriction only on identity between those kinds of sorting and the prior kind, so x^(j<i)=x^k is only allowed when k<i, otherwise there is no syntactical restriction, so x^(j<n) E x^(j<m) is allowed for all n>0 and all m>1, similarily x^(j<n)=x^(j<m) is allowed for all n,m>0. Also the successor symbol which is a unary function symbol is restricted to type zero variables. Also, we add the constant symbol O which denotes a type zero object.
Axioms:
[1] Sorting: for i=1,2,3,..., j<i
for all x^j Exists x^(j<i) [x^j = x^(j<i)]
[2] Extensionality: for i=1,2,3,…
∀x^(j<i) [x^(j<i) ∈ z^i ⇔ x^(j<i) ∈ y^i] ⇒ z^i = y^i
[3] Comprehension: for i=1,2,3,...; if φ^i is a formula in which all of its variables have types less than i, then all closures of:
∃x^i ∀y^(j<i) [y^(j<i) ∈ x^i ⇔ φ^i]
are axioms.
A less strict version is to allow parameters to be of type i or type j<(i+1)
[4] Zero: ∀x^0 [~ S(x^0)=O]
[5] Succession: ∀x^0 ∀y^0 [S(x^0)=S(y^0) ⇒ x^0 = y^0]
[6] Induction: if φ is a formula, then
φ(O) ^ ∀x^0[φ(x^0) ⇒ φ(S(x^0))] ⇒ ∀y^0[φ(y^0)]
/ Theory definition finished.
This theory though predicative yet still it doesn't forbid intersectional
definitions that ordinary predicative theories forbid. So this theory can
prove all axioms of PA.
The nice thing about this system is that it can be extended to having infinite types like
w, w+1, w+2,....
Here, in this case, I don't think we'll be needing any of the last three axioms since I think PA would be interpretable in it (not so sure).
Now if we don't want to extend the system to a one which contains meta-theoretic limit ordinals, then actually we can remove all syntactical restrictions, and make types overlap each other, i.e. whatever substitute x^i will substitute x^i+n, but the converse is not true, i.e. it is not the case that whatever substitute x^i+n will substitute x^i. We speak about this issue as:
[1] Sorting: for all x^i Exists x^i+n (x^i=x^i+n)
Now every symbol using (j<i) as a type will be replaced by i-1 in the above axioms.
However, this will not be sufficient if we want to extend the system with meta-theoretic limit ordinals.
___________________________________
Language: omega multi-sorted first-order logic, syntactical restrictions involves not allowing formulas of the form x^i = x^j if i=/=j, nor allowing formulas of the form x^i E x^j if i>=j, so we only allow x^i E x^j if i<j.
The least type allowed is type zero, so no variable is indexed by negative types and so occurrence of a symbol indexed with 0 is not allowed on the right of the membership symbol E. there is also another kind of sorting denoted by superscript (j<i) where i>0, so x^(j<i) is taken to range over all of what x^j for j<i range over. Here with this kind of sorting there is a syntactical restriction only on identity between those kinds of sorting and the prior kind, so x^(j<i)=x^k is only allowed when k<i, otherwise there is no syntactical restriction, so x^(j<n) E x^(j<m) is allowed for all n>0 and all m>1, similarily x^(j<n)=x^(j<m) is allowed for all n,m>0, what is not allowed is to have x^i+n E x^(j=<i), but the opposite is allowed i.e. x^(j<i) E x^k is allowed for whatever k,i>0 are. Also the successor symbol which is a unary function symbol is restricted to type zero variables. Also, we add the constant symbol O which denotes a type zero object.
Axioms:
[1] Sorting: for i=1,2,3,...,w,w+1,w+2,...; j<i
for all x^j Exists x^(j<i) [x^j = x^(j<i)]
[2] Extensionality: for i=1,2,3,...,w,w+1,w+2,...
∀x^(j<i) [x^(j<i) ∈ z^i ⇔ x^(j<i) ∈ y^i] ⇒ z^i = y^i
[3] Comprehension: for i=1,2,3,...,w,w+1,w+2,...;
if φ^i is a formula in which all of its variables
have types less than i, then all closures of:
∃x^i ∀y^(j<i) [y^(j<i) ∈ x^i ⇔ φ^i]
are axioms.
/Theory definition finished.
The idea is that this is a very weakly predicative theory, it literally adheres merely to what predicativity is! I think that it can interpret the whole of PA, and also, provides tiers of sets over it that are predicatively defined.
Definitions by intersections can be carried out here.
Cantors' argument of uncountability cannot be proved here since the diagonal
would be of a higher type than the elements of the diagonalized power set. Possibly the constructible universe of Godel below Lw+w is a model of this
theory.
Zuhair
9/10/2017