Language: mono-sorted first order logic with equality
Extra-logical primitives: T,∈T,∈; the first signifies "the type of" and its a total one place function symbol, the second is set membership.
Informally every object in this theory is a set and it has a type, sets are extensional as usual, and sets are constructed after what I call as "limit type construction" which simply states that: any predicate that has an upper bound on the types of objects fulfilling it, can define a set! However here parameters in the set constructing formula cannot be higher than the type of the asserted set. This restriction is reminiscent of the "predicative" notion of set construction, that we can only construct sets from lower or equal typed sets! The idea is to parallel the "set formation" informal notion, that is sets are formed in stages, that lower stages (types) are formed before higher ones, and so we cannot form lower stages from higher ones because the latter ones are not formed yet! However this theory doesn't obey the full predicative notion in that it allows unrestricted quantifiers in the set constructing formula, so it only captures the predicative notion in a partial manner as it applies it to parameters only, a kind of parametric predicativity!
Define: x is a type ⟺∃k:T(k)=xx is a type ⟺∃k:T(k)=x
Define: ∀ type x ϕ(x)⟺∀x(x is a type→ϕ(x))∀ type x ϕ(x)⟺∀x(x is a type→ϕ(x))
A. Type axioms:
Restriction: x<y→x,y are types x<y→x,y are types
Asymmetric: x<y→y≮xx<y→y≮x
Transitive: x<y∧y<z→x<zx<y∧y<z→x<z
Connected: ∀ type x ∀ type y (x≠y⟺x<y∨y<x)∀ type x ∀ type y (x≠y⟺x<y∨y<x)
Well founded: ∃ type x ϕ⟹∃ type x(ϕ(x)∧∀ type y (ϕ(y)→x≤y))∃ type x ϕ⟹∃ type x(ϕ(x)∧∀ type y (ϕ(y)→x≤y))
Fixing: T(T(x))=T(x)T(T(x))=T(x)
Infinity: ∃t:∀s(∀k≤s(k≠0→∃l(k=S(l)))→s<t)∃t:∀s(∀k≤s(k≠0→∃l(k=S(l)))→s<t)
B. Set axioms:
Extensionality: ∀z(z∈x↔z∈y)→x=y∀z(z∈x↔z∈y)→x=y
Limit Type Construction: ∀t∀w⃗ [limϕ=t∧T(w⃗ )≤t⟹∃x∀y (y∈x↔ϕ)]∀t∀w→[limϕ=t∧T(w→)≤t⟹∃x∀y (y∈x↔ϕ)]
Where: limϕ=min l:∀y(ϕ→T(y)≤l)limϕ=min l:∀y(ϕ→T(y)≤l); and where ϕϕ is a formula that has the symbol yy occurring free, and all its parameters are among symbols of w⃗ w→ which are w1,..,wnw1,..,wn ; and T(w⃗ )≤tT(w→)≤t means T(w1)≤t ∧...∧ T(wn)≤tT(w1)≤t ∧...∧ T(wn)≤t
C. Type-set axioms:
Typing: T(x)=min t:∀y∈x(T(y)<t)T(x)=min t:∀y∈x(T(y)<t)
I just want to make a note that this method can show us a spectrum of theories, if we drop the condition of T(w⃗ )≤tT(w→)≤t from the antecedent of construction, we get a theory equivalent to Zermelo set theory, if we additionally restrict quantifiers in ϕϕ to be bounded by types, then I think we get MacLane set theory, if in the above approach we additionally add the condition of bounding quantifiers by types less than tt, then we get the a kind of predicative type theory, but I'm not sure of its strength. Anyhow I'm concerned with the above presented theory, so my question is:
is there a way to prove Cantor's theorem of uncountability of P(ω)P(ω) here?
The theory is presented here: