Since Leitgeb’s class theory has a universal class, the set axiom separation will not hold in it.
The universal class turns out to be grounded on Leitgeb’s definition of groundedness.
Let φ be ‘x ∈ x’. To show this ersatz class to be ungrounded, assume for the sake of contradiction that φ ∈ Φ lf. Hence, for some α + 1, φ ∈ Φ α + 1 and φ ∉ Φ α. Hence, φ depends on Φ α × Φ α. That is, for any sets X and Y, if X ∩ Φ α × Φ α = Y ∩ Φ α × Φ α then $\text{\textit{Ext}}_X(\phi)=\text{\textit{Ext}}_Y(\phi)$. Now, since by assumption φ ∉ Φ α, ⟨φ, φ⟩ ∉ Φ α × Φ α. Hence {⟨φ, φ⟩} ∩ Φ α × Φ α = ∅ × ∅ ∩ Φ α × Φ α. However, $\text{\textit{Ext}}_{\{\langle\phi,\phi\rangle\}}(\phi)=\{\phi\}\neq\emptyset=\text{\textit{Ext}}_\emptyset\times\emptyset(\phi)$, contradiction. Therefore, φ ∉ Φ lf. In other words, φ is ungrounded.
Since ⟨ψ, φ⟩ ∈ Γ α is defined by a conjunction of a Π 11 predicate (‘φ ∈ D - 1(dm(X))’) and a Δ 11-predicate (‘$\text{\textit{Val}}_\Delta(\phi)=1$’), the operator that builds up the sequence (Γ )α is Π 11.
Hence, by Spector’s theorem ,1 Finally, by a general result due to Kleene we obtainDo I need to define the monotone operator explicitly, in order to apply Spector’s theorem, or does a monotonically increasing sequence such as (Γ )α suffice? I need to ascertain that the operator is Π 11. Hence, I need to know a Π 11 definition of it. Q: Any monotonically increasing sequence is built up by a monotone operator? ↩