Types
Theory of accumulative types:
Language is set language with additional primitives of a total one place function symbol τ, signifying "is the type of", and also a primitive binary relation symbol ‘‘<" on types, signifying "strictly less than".
Axioms:
a) Axioms about types:
1. Asymmetric: τ(x)<τ(y)→τ(y)≮τ(x)
2. Transitive: τ(x)<τ(y)<τ(z)→τ(x)<τ(z)
3. Connected: τ(x)≠τ(y)↔[τ(x)<τ(y)∨τ(y)<τ(x)]
4. Successor: ∀x∃y(τ(x)<τ(y)∧∄z(τ(x)<τ(z)<τ(y)))
5. Limit: ∃x[∃y(τ(y)<τ(x))∧∀z(τ(z)<τ(x)→∃u(τ(z)<τ(u)<τ(x)))]
b) Axioms about sets:
1. Extensionality: ∀z(z∈x↔z∈y)→x=y
2. Typed comprehension: for every set a and every formula ϕ in which x doesn't occur, there exists a set x of all sets whose types are strictly smaller than the type of a, that meets ϕ. That is, all closures of:
∀a∃x∀y [y∈x↔τ(y)<τ(a)∧ϕ]
, are axioms.
3. Assignment:
∀x[∀y∈x(τ(y)<τ(x))∧∀k(∀y∈x(τ(y)<τ(k))→τ(x)≤τ(k))]
Every set has the lowest possible type that is strictly larger than all types of its elements.
/ Theory definition finished.
Can this theory interpret Zermelo set theory?
If we add the following axiom scheme to axioms about types:
6. Well founded: ∃xϕ(x)→∃x[ϕ(x)∧∀y(ϕ(y)→τ(x)≤τ(y))], for every formula ϕ
Would that addition render Zermelo set theory a proper sub-theory of this theory? That is: all true sentences of Zermelo are theorems of this theory!