Language: mono-sorted first order logic with equality
Extra-logical primitives: $T, \in, <$; the first signifies "the type of" and its a total one place function symbol, the second is set membership, the third denotes "strict smaller than" binary relation.
Define: $x \text { is a type } \iff \exists y: T(y)=x$
Define: $\forall \text { type } x \ \phi(x) \iff \forall x (x \text { is a type} \to \phi(x))$
*A. Type axioms:*
**Restriction:** $x < y \to x,y \text { are types }$
**Asymmetric:** $x < y \to y \not < x$
**Transitive:** $x < y \land y < z \to x < z$
**Connected:** $\forall \text { type } x \ \forall \text { type }y \ (x \neq y \iff x < y \lor y < x) $
**Well founded:** $\exists \text { type } x \ \phi \implies \exists \text { type } x (\phi(x) \land \forall \text { type y } (\phi(y) \to x \leq y)) $
**Fixing:** $T(T(x))=T(x) $
**Maximal:** $\exists t: \forall x [T(x) \leq t]$
Define: $t=t_{max} \iff \forall x (T(x) \leq t)$
**Infinity:** $\exists t < t_{max} :t \neq 0 \land \forall l < t \exists k (l < k < t)$
*B. Set axioms:*
**Extensionality:** $\forall z (z \in x \leftrightarrow z \in y) \to x=y $
**Typed Comprehension:** $\forall t \forall \vec{w} \exists x \forall y \ (y \in x \leftrightarrow y < t \land \phi )$
for any formula $\phi$ in which $x$ does not occur free.
**Choice:** as in ZC.
*C. Type-set axioms:*
**Typing:** $T(x) = \min \ t: \forall y \in x (T(y)<t)$
**Graduality:** $\forall t \forall x [\forall y \in x (T(y)=t) \to T(x) < t_{max}]$
/ Theory definition finished.
The above is what I think it to be the most complete exposition of set theory! The customary exposition of ZC (and its extensions) is deficient, it doesn't explicitly expose the most prominent feature after which it really avoid paradoxes, which in reality resides in a sort of a typed approach, though made implicit. There the ranks correspond to types here, so in reality ZC and extensions are typed theories but with types made implicit. So the full explicit exposition should be something the above. Types are important, we can manipulate them and have various fragments and extensions (like the parametric predicative fragment present here), so they ought to be made conspicuous! The sense of a hierarchy that ZC and its extensions seems to be motivated after, actually find itself naturally produced here after types, it can be seen to be more related to types rather than with mere sets!
Now for many technical (as well as natural) I think the most natural set theory is the above but without the axiom of infinity. The resulting theory would interpret second order arithmetic, and is capable of implementing most of ordinary mathematics. So it is that fragment that should be considered as the foundational theory of mathematics, and actually adding infinity to it, should be considered as a kind of large cardinal axiom! The latter step would enable it to cover larger and larger sector of "Logico-mathematical" stuff, what I would rather call as *Mathemalogic*, since its not just pure mathematics, there is much logic into it.
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, the third denotes "strict smaller than" binary relation.
Define: x is a type ⟺∃y:T(y)=xx is a type ⟺∃y:T(y)=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)
Maximal: ∃t:∀x[T(x)≤t]∃t:∀x[T(x)≤t]
Define: t=tmax⟺∀x(T(x)≤t)t=tmax⟺∀x(T(x)≤t)
Infinity: ∃t<tmax:t≠0∧∀l<t∃k(l<k<t)∃t<tmax:t≠0∧∀l<t∃k(l<k<t)
B. Set axioms:
Extensionality: ∀z(z∈x↔z∈y)→x=y∀z(z∈x↔z∈y)→x=y
Typed Comprehension: ∀t∀w⃗ ∃x∀y (y∈x↔y<t∧ϕ)∀t∀w→∃x∀y (y∈x↔y<t∧ϕ)
for any formula ϕϕ in which xx does not occur free.
Choice: as in ZC.
C. Type-set axioms:
Typing: T(x)=min t:∀y∈x(T(y)<t)T(x)=min t:∀y∈x(T(y)<t)
Graduality: ∀t∀x[∀y∈x(T(y)=t)→T(x)<tmax]∀t∀x[∀y∈x(T(y)=t)→T(x)<tmax]
/ Theory definition finished.
See:
Another version:
Language: first order logic with equality and its axiom and additionally the extra-logical primitives: ‘‘τ,<,∈", the first is a total unary function denoting is the type of, the rest are binary relations denoting, is lower than and set membership respectively.
Axioms:
Extensionality: ∀z(z∈x⇔z∈y)→x=y
Define: t is a type⟺∃x:t=τ(x)
Well ordering: <is a well-order on types
Idempotence: τ(τ(x))=τ(x)
Infinity: ∃t:lim<t
Atomicity: ∀type t:∀y(y∈t⟺y=t)
Typed Comprehension: ∀t∃x∀y(y∈x⟺τ(y)<t∧ϕ)
Typing: x not a type → τ(x)=mint:∀y∈x(t>τ(y))
Inaccessibility: if ff is a definable function, then:
∀x:¬∀type t∃y∈x(t<f(τ(y)))
Note: the expression ‘‘< is a well order on types"is the following axioms:
∀x∀y(x<y→x,y are types x<y→y≮xx<y<z→x<zx,y are types∧x≠y⟺x<y∨y<x)
∃type x(ϕ(x))→∃type x:ϕ(x)∧¬∃y(ϕ(y)∧y<x)ype x(ϕ(x))→∃type x:ϕ(x)∧¬∃y(ϕ(y)∧y<x)
the expression ‘‘lim<t"‘is:
∃a(a<t)∧∀a<t∃b<t(a<b)
the expressions ‘‘∀type x..;∃ type x.." stands for ∀x(x is a type →..) and ∃x(x is a type ∧..) respectively.
This is a theory ought to be interpretive of ZFC.
See: Type-set theory
A more fundamental approach taking into accout the genre of types being radically different form that of sets, is to have a bi-sorted theory:
Language: bi-sorted first order logic with equality and its axiom and additionally the extra-logical primitives: ‘‘τ,<,∈"‘, the first is a total unary function on sets denoting is the type of, the rest are binary relations denoting, is lower than and set membership respectively. Sorts are: the first sort in Greek for types, the second sort in ordinary English letters for sets. Syntatic restrictions include: τ only taking set symbols as first arguments but their images are type symbols, < only occur between type symbols, ∈ only occur between sets symbols.
Axioms:
Extensionality: ∀z(z∈X⇔z∈Y)→X=Y
Well ordering: <is a strict well-order on types, that is:
∀α∀β(α≮αα<β<z→α<z
α≠β→α<β∨β<α) ∃α(ϕ(α))→∃α:ϕ(α)∧¬∃β(ϕ(β)∧β<α)
Infinity: ∃λ:∃α(α<λ)∧∀α<λ∃β<λ(α<β)
Typed Comprehension: ∀α∃X∀y(y∈X⟺τ(y)<α∧ϕ)
Typing: τ(X)=minα:∀y∈X(α>τ(y))
Inaccessibility: if f is a definable function, then:
∀X:¬∀α∃y∈X(α≤f(y))
Where: α≤β≡dfα<β∨α=β
Now I think that this theory is a conservative extension over ZF , and over ZFC should Choice be added to it. Moreover, this theory is a naive capture of conceptions about types and sets and portrays a naive enmeshment between them, that it can by itself be considered as motivating the standard line of set theory.
A nice offshoot of this method of contemplating sets woven (knitted) by types is to have an extreme version of definability that is determined after types, that is
Type-Definability:
∀X∃θ∃α<θ∃φ:X={y∈ Vθ∣Vθ⊨φ(y,α)}WwwW
Where Vθ is the set of all sets of type <θ
This axiom can also be written as:
Type-Definability: ∀X∃θ∃α<θ∃ϕ:X={τ(y)<θ∣ϕθ(y,α)}
Where ϕθ means restricting all quantifiers in ϕ to <θtypes, that is ∀x:...∀x:... would turn to ∀x:τ(x)<θ→... and ∃x:...∃x:... would turn to ∃x:τ(x)<θ∧...
This is supposed to indirectly capture the idea
that every set is defined after a formula from
type parameters.
This is an extreme example of a Type-Set
enmeshment that that sort of theories would push
for.
Of course this would prove axiom of choice.
Another nice feature of this method is that we
know that if we don't allow the membership
symbols in axioms other than Comprehension
and typing. Then the strongest we can get is an
axiom of type inaccessibility, that is:
Type inaccessibility: if f is a definable function, then:
∀γ(¬∀ α∃β<γ:α≤f(β))
∀γ(¬∀ α∃β<γ:α≤f(β))
This would have V_omege_1 as its model.
So it cannot prove successor cardinals.
And it appears that it is the most that type theory
with the above restriction on axiomatization can do.
It is obvious that a simple loosining of this condition by generalizing the above axioms over every set X instead of just limiting it to types (and of course using the membership symbol) would lead to the axiom of Inaccessiblity given above, which would enact replacement and thus be of the same strength as ZF.
Of course if we only want to get the strength of Zermelo then we don't need the last axiom, we only need to change type comprehension to:
Typed Comprehension: ∀α∃!X∀y(y∈X⟺τ(y)≤ α∧ϕ)
Of course with this axiom, there is no need for
Extensionality. Actually, this is nearly logic, I mean
it can be considered as the logic of type and sets. And
So this is very rigorous.