Now we turn to the absolutness of the notion of constructibility. There is a formula Λ(x) which says that x is constructible, and which holds in L iff it holds in V. Λ(x) is not Δ0, nor is it absolute over all transitive classes, so some subtleties come into play. (It is absolute between models of ZF.)
At the heart of constructibility lies the notion of definability, in turn depending on satisfaction. This requires coding formulas as sets, much like the Gödel coding used in the proof the Gödel’s incompleteness theorem. I will lean heavily on corner bracket notation for this: ⌜φ⌝ stands for the Gödel set for the formula φ. For example, 〈⌜φ⌝,⌜ψ⌝〉 ↦⌜φ∧ψ⌝ stands for the function taking the Gödel sets for a pair of formulas to the Gödel set for their conjunction.
I will make a clear distinction between syntax and semantics, emphasize the role of names, give some related results for context, and handwave; I hope all this makes the discussion readable.
Some notation, using my conventions. Let a be any set.
| Symbol | Meaning | Example |
| ℒ(ZF) | Language of ZF | |
| ℒV(ZF) | ℒ(ZF) augmented with names for all sets | |
| ℒa(ZF) | ℒ(ZF) augmented with names for all elements of a | |
| ℰ | codes of formulas of ℒV(ZF) | ⌜φ(x̄,c̄)⌝ |
| ℰa | codes of formulas of ℒa(ZF) | ⌜φ(x̄,c̄)⌝ with c̄∈a |
| S | codes of sentences (closed formulas) of ℒV(ZF) | ⌜φ(c̄)⌝ |
| S(a) | codes of sentences of ℒa(ZF) | ⌜φ(c̄)⌝ with c̄∈a |
| M | codes of monadic formulas of ℒV(ZF) | ⌜φ(x,c̄)⌝ |
| M(a) | codes of monadic formulas of ℒa(ZF) | ⌜φ(x,c̄)⌝ with c̄∈a |
ℒ(ZF) has only one predicate symbol ‘∈’; I regard ‘=’ as a basic logical symbol. For ℒV(ZF), we could let sets name themselves. Since ℒ(ZF) has no (built-in) constants, name and constant are synonymous here.
It is illuminating to consider three results together, all concerning the “definability of truth”. There is a pure formula true(x,y) (in ℒ(ZF)) defining truth in the structure (a,∈) for sentences in ℒa(ZF). For any n∈ℕ, there is a pure formula truen(x) defining truth in (V,∈) for sentences in ℒV(ZF) of parsing depth at most n. But there is no pure formula true(x) defining truth in (V,∈) for sentences in ℒV(ZF). The formula for ℒa(ZF) is even Δ1ZF. Summarizing:
| Yes (Δ1ZF) | a⊧φ(c̄) iff V⊧true(a,⌜φ(c̄)⌝) (c̄∈a) |
| Yes | V⊧φ(c̄) iff V⊧truen(⌜φ(c̄)⌝) (depth≤n) |
| No | V⊧φ(c̄) iff V⊧true(⌜φ(c̄)⌝) |
(I’ve written a⊧ instead of (a,∈)⊧ for brevity, likewise for V.) The last result is known as Tarski’s theorem on the undefinability of truth. The first two are formalizations of Tarski’s definition of truth.
Induction and Functions
Before plunging into details, some preliminaries.
We’ll work with a function Va instead of a predicate true(a,−);
Va(⌜φ(c̄)⌝)=1 iff a⊧φ(c̄). Functions often have technical advantages over predicates.
Formally defining a function f means having a formula φ(x̄,y) for the relation f(x̄)=y. If φ is Δ1ZF, then we say that f has a Δ1ZF definition (likewise for Σ1 or Π1 or pure or whatever). Most authors require functions to have domains that are sets, so the word functional is often used when this restriction is dropped. Recall that a formula φ(x̄,y) is function-like over a transitive class K if it defines a functional defined on all of K.
As a reminder, Σ1 definitions are absolute upwards, Π1 absolute downwards. and Δ1ZF are absolute between models of ZF.
Example: the power set functional 𝒫(x) has a Π1 definition because y=𝒫(x) iff ∀z[z∈y↔z⊆x], and z⊆x is Δ0. The ordered pair functional 〈x,y〉 is Δ0 because
z=〈x,y〉 iff (∃u,v∈z)[z={u,v}∧u={x}∧v={x,y}]
and z=x×y is Δ0 because
| z=x×y iff | (∀p∈x)(∀q∈y)(∃u∈z)[u=〈p,q〉] |
| ∧(∀u∈z)(∃p∈x)(∃q∈y)[u=〈p,q〉] |
Special case: 0-ary functions, aka distinguished elements. The most important example is ω: w=ω iff w is transitive and the elements of w are linearly ordered under ∈, because Foundation then implies that w is well-ordered under ∈. So ω has a Δ0 definition.
Definition by transfinite induction preserves Σ1ZF-ness, Π1ZF-ness, and hence Δ1ZF-ness. Proof: Suppose the functional F(x) is Σ1ZF. Define F* by
| F*(0) | = ∅ |
| F*(α+1) | = F(F*(α)) |
| F*(λ) | = ⋃α<λF*(α) |
Then y=F*(α) iff there is a function f with domain α+1 such that f satisfies the inductive demands for all β≤α and y=f(α). Explicitly, but with some vernacular:
| α is an ordinal and |
| ∃f[f is a function with domain α+1 and |
| f(0)=∅ and |
| (∀β∈α+1) [f(β+1)=F(f(β))] and |
| (∀ limit λ∈α+1) [f(λ)=⋃β∈λf(β)] and |
| y=f(α)] |
Thus if F is Σ1ZF, so is F*. On the other hand, if F is Π1ZF, we use a formula saying that all functions f with domain α+1 and satisfying the inductive demands must have f(α)=y. Explicitly:
| α is an ordinal and |
| ∀f[f is a function with domain α+1 and |
| f(0)=∅ and |
| (∀β∈α+1)[f(β+1)=F(f(β))] and |
| (∀ limit λ∈α+1) f(λ)=⋃β∈λf(β)]→ |
| y=f(α)] |
We can ring variations on this theme. Extra parameters can come along for the ride, i.e., replace F(x) with F(x,ȳ) and F*(α) with F*(α,ȳ). We don’t have to start with F*(0)=∅, we can define a functional F*(α,a) where a is the initial value (i.e., F*(0,a)=a, F*(α+1,a)=F(F*(α,a)), etc.) We can include α as an additional argument to F, i.e., F*(α+1)=F(α,F*(α)). “Ordinary” inductions that only go up to ω preserve Σ1ZF/Π1ZF/Δ1ZF-ness because “being ω’’ is Δ0.
Example: the functional y=tc(x) (the transitive closure of x) is Δ1ZF because z∈x is Δ0 and tc has the inductive definition
| tc(0,x) | = x |
| tc(n+1,x) | = tc(n,x)∪⋃z∈xtc(n,z) |
| tc(ω,x) | = ⋃n∈ωtc(n,x) |
and tc(x)=tc(ω,x). Likewise rank is Δ1ZF, and more generally definitions by so-called ∈-induction preserve Σ1ZF/Π1ZF/Δ1ZF-ness.
For industrial-strength use, one can develop a whole calculus to determine places in the complexity hierarchy. But we need very little of this.
I’ve included the ZF superscript throughout; this sweeps away any concerns about the placement of bounded quantifiers.
Formalizing Syntax in ZF
To formalize syntax in ZF, we code the base layer in a somewhat arbitrary but straightforward manner. Then we throw (ordinary) induction at it.
For the base layer, we need codes for all the individuals, i.e., the variables and the names of elements of V. We could use 〈0,i〉 to code vi and 〈1,a〉 to code the name for a. But we don’t need to worry about those details, we’ll just write ⌜vi⌝ and ⌜a⌝.
Next, formulas. One can obviously code a formula as a finite sequence of codes of symbols and of individuals. But I think it’s cleaner to use a parse tree. We have the “tree-building” functionals
using ordered pairs and triples, with the last slot serving as “tag” to identify the type of each node (negation, conjunction, etc.) That makes it pretty obvious that these functionals are Δ0.
The functional a↦ℰa takes a set a and finds all codes of formulas where the names all refer to elements of a. Like practically everything in the realm of syntax, we induct on the depth of parse trees. It’s very similar to the definition of the transitive closure. We start with the base layer of atomic formulas, denoted ℰ0a. We want ℰa to satisfy the inductive condition
| y∈ℰa iff |
| y∈ℰ0a or |
| y=⌜¬φ⌝ with ⌜φ⌝∈ℰa or |
| y=⌜φ∧ψ⌝ with ⌜φ⌝,⌜ψ⌝∈ℰa or |
| y=⌜(∃vi)φ(vi)⌝ with ⌜φ(vi)⌝∈ℰa |
To fit this into the F, F* paradigm, we let F take a set x of codes of formulas, and throw in one application of any of the tree-building functionals. So x⊆F(x), and if ⌜φ⌝∈x then ⌜¬φ⌝∈F(x), etc. Next, F*(0)=ℰ0a, and F*(n+1) is defined inductively as F(F*(n)). It follows from the generalities on induction that ℰa is Δ1ZF.
The class ℰ of codes of all formulas in ℒV(ZF) is a proper class. It has a Σ1ZF definition: x∈ℰ iff ∃a[x∈ℰa].
It’s the same story for other aspects of syntax. For example, the substitution functional (⌜φ(x)⌝,⌜c⌝) ↦⌜φ(c)⌝ has a Δ1ZF definition.
Formalizing Truth in ZF
We turn our attention to the two truth predicates we can formalize in ZF (a⊧φ(c̄), and V⊧φ(c̄) for depth(φ)≤n) and the one we can’t (V⊧φ(c̄)).
For atomic sentences, the formalization is a breeze:
| true0(x) iff |
| (x=⌜c=d⌝∧c=d) |
| ∨(x=⌜c∈d⌝∧c∈d) |
Let’s start with the inductive definition we’d like for
V⊧φ(c̄):
| true(x) iff |
| x is atomic and true0(x) |
| ∨ x=⌜¬φ⌝ ∧ ¬true(⌜φ⌝) |
| ∨ x=⌜φ∧ψ⌝ ∧ true(⌜φ⌝) ∧ true(⌜ψ⌝) |
| ∨ x=⌜∃xφ(x)⌝ ∧ ∃d true(⌜φ(d)⌝) |
Because of the circularity, this doesn’t actually define a formula in ℒ(ZF); rather, it expresses the property we’d want the formula to have. Tarski’s theorem tells us that no such formula exists.
First modification:
| truen+1(x) abbreviates |
| x is atomic ∧ true0(x) |
| ∨x=⌜¬φ⌝∧ ¬truen(⌜φ⌝) |
| ∨x=⌜φ∧ψ⌝∧ truen(⌜φ⌝)∧truen(⌜ψ⌝) |
| ∨x=⌜∃xφ(x)⌝∧ ∃d truen(⌜φ(d)⌝) |
Imagine the right hand side expanded out repeatedly until we have a formula in ℒ(ZF). Put another way, the induction is outside ZF, although the longer and longer formulas belong to ZF.
Not just ever longer formulas: truen is ΣnZF, because of the ∃d embedded in it. (If we’d made ∀ fundamental and ∃ an abbreviation, then truen would be ΠnZF.)
As noted, V⊧φ iff V⊧truen(⌜φ⌝), provided φ has depth ≤n. For the second modification, we define a single formula true(x,y) such that a⊧φ(c̄) iff V⊧true(a,⌜φ(c̄)⌝). This time there is no restriction on the depth of φ(c̄), but we do demand that c̄∈a.
We handle the circularity just as we did for ℰa. Recall that S(a) is the set of codes of sentences of ℒa(ZF). Let Sn(a) be the codes for sentences of depth ≤n. Let Tn(a) be the set of all true sentences of Sn(a), i.e., all that are satisfied by (a,∈). We have an inductive definition of Tn(a).
T0(a) presents no issues: x∈T0(a) iff x is atomic and true0(x).
| x∈Tn+1(a) iff x∈Sn+1(a) and [ |
| x is atomic and x∈T0(a) |
| ∨ x=⌜¬φ⌝∧ ⌜φ⌝∉Tn(a) |
| ∨ x=⌜φ∧ψ⌝∧ ⌜φ⌝∈Tn(a) ∧ ⌜ψ⌝∈Tn(a) |
| ∨ x=⌜∃xφ(x)⌝∧ (∃d∈a)(⌜φ(d)⌝∈Tn(a))] |
It’s no sweat to turn this into a function F such that Tn+1(a)=F(Tn(a)) for all n∈ω. Moreover, F has a Δ0 definition, because all the tree-building functionals are Δ0. Note that the crucial existential quantifier, “(∃d∈a)’’, is now bounded. So we have a Δ1ZF definition of the set
T(a) of true sentences in S(a).
I’ve emphasized the parallels between ℰa and T(a). Now let’s highlight the differences. We defined the proper class ℰ via the equivalence x∈ℰ≡∃a(x∈ℰa). Why doesn’t this work for T⊆S, the proper class of true sentences about V? First hint of the problem: V⊧φ(c̄) and ∃a(a⊧φ(c̄)) are not equivalent, even when c̄∈a. We search for a culprit; the quantifier pleads guilty. Syntax doesn’t care about the scope of a quantifier ∃x—it’s just a node in the parse tree. But for semantics, the scope is central to the meaning. Put another way, when syntax examines the formula φ(x̄,c̄), it “sees” only the names explicitly present. Semantics considers all possible names when turning ∃xφ(x) into φ(d).
Absoluteness of L
Consider this list of relations.
- a⊧φ(c̄), with c̄∈a.
- y={x∈a:a⊧φ(x,c̄)}.
- y∈ℱ(a).
- y=ℱ(a).
- y∈Lα and y=Lα, where α is an ordinal.
- y∈L, that is, Λ(y)
These are all Δ1ZF except the last one. But y∈L is absolute between V and L. Proof:
- We’ve just seen that this is Δ1ZF, or rather, its equivalent
true(a,⌜φ(x,c̄)⌝) is. - y={x∈a:a⊧φ(x,c̄)} iff (∀z∈y)(a⊧φ(z,c̄)) and (∀z∈a)[(a⊧φ(z,c̄))→z∈y]. So this is Δ1ZF.
- y∈ℱ(a) iff there is a monadic formula φ(x,c̄) in ℒa(ZF) such that y={x∈a:a⊧φ(x,c̄)}. Recall that M(a) is the set of codes of such monadic formulas. So
y∈ℱ(a) iff(∃p∈M(a))[y={x∈a:true(a,p)}]
The new feature: instead of a true bounded quantifier, we have something of the form (∃u∈f(z))ψ(y,z,u) where f(z) and ψ are both Δ1ZF. But that’s equivalent to ∃v(∃u∈v)[v=f(u)∧ψ(y,z,u)], which is Σ1ZF. It’s also equivalent to ∀v[v=f(u)→(∃u∈v)ψ(y,z,u)], which is Π1ZF.
- y=ℱ(a) iff (∀z∈y)[z∈ℱ(a)]∧(∀z∈ℱ(a))[z∈y]. We can handle the “kind-of” bounded quantifier, (∀z∈ℱ(a)), much the same as we handled (∃p∈M(a)) in the previous item.
- Transfinite induction preserves Δ1ZF-ness.
- ∃α(y∈Lα). So y∈L is Σ1ZF. So Λ is upwards absolute from L to V. In the reverse direction, suppose V⊧Λ(s) for some s. Then for some ordinal α, V⊧s∈Lα. But L contains all ordinals, and being an ordinal is absolute, and Lα is absolute, so L⊧s∈Lα and hence Λ is downwards absolute from V to L.
This final item (6) is the goal of the whole argument. But as a matter of curiosity you might ask, is Λ downwards absolute between models of ZF? How about upwards and downwards absoluteness for transitive classes in general?
(1)–(6) are not Σ1, though they are Σ1ZF. We mentioned in post 22 that if you slap a bounded quantifier in front of a Σ1 formula, the result is upwards absolute between transitive classes. Using this, one can show that (1)–(6) are upwards absolute between transitive classes. So all these notions are upwards absolute between transitive classes.
We needed one feature of L, besides being a model of ZF, to establish downwards absoluteness from V: the fact that L contains all ordinals. Are there any standard models of ZF not containing all ordinals? The “yes” answer is one form of axiom SM. Using this, plus forcing, one can show Λ is not downwards absolute between models of ZF.
It’s much easier to show that Λ is not downwards absolute between transitive classes. Consider Lα+1 for some α. Suppose s has rank α, i.e., s∈Lα+1∖Lα. (For example, let s=α or s=Lα.) So s is constructible, but not constructible “in Lα+1’’. For if Lα+1⊧Λ(s), then Lα+1⊧∃β(s∈Lβ), i.e., s∈Lβ for some β≤α. But we assumed s had rank α.
Diagonal Argument 