Set-theoretic arguments often make use of the fact that a particular property 𝜑 is local, in the sense that instances of the property can be verified by checking certain facts in only a bounded part of the set-theoretic universe, such as inside some rank-initial segment 𝑉𝜃 or inside the collection 𝐻𝜅 of all sets of hereditary size less than 𝜅. It turns out that this concept is exactly equivalent to the property being Σ2 expressible in the language of set theory.

Theorem. For any assertion 𝜑 in the language of set theory, the following are equivalent:

1. 𝜑 is ZFC-provably equivalent to a Σ2 assertion.
2. 𝜑 is ZFC-provably equivalent to an assertion of the form “∃𝜃 𝑉𝜃 ⊧𝜓,” where 𝜓 is a statement of any complexity.
3. 𝜑 is ZFC-provably equivalent to an assertion of the form “∃𝜅 𝐻𝜅 ⊧𝜓,” where 𝜓 is a statement of any complexity.

Just to clarify, the Σ2 assertions in set theory are those of the form ∃𝑥 ∀𝑦 ⁢𝜑0⁡(𝑥,𝑦), where 𝜑0 has only bounded quantifiers. The set 𝑉𝜃 refers to the rank-initial segment of the set-theoretic universe, consisting of all sets of von Neumann rank less than 𝜃. The set 𝐻𝜅 consists of all sets of hereditary size less than 𝜅, that is, whose transitive closure has size less than 𝜅.

Proof. (3 →2) Since 𝐻𝜅 is correctly computed inside 𝑉𝜃 for any 𝜃 >𝜅, it follows that to assert that some 𝐻𝜅 satisfies 𝜓 is the same as to assert that some 𝑉𝜃 thinks that there is some cardinal 𝜅 such that 𝐻𝜅 satisfies 𝜓.

(2 →1) The statement ∃𝜃 𝑉𝜃 ⊧𝜓 is equivalent to the assertion ∃𝜃 ∃𝑥 ⁡(𝑥 =𝑉𝜃 ∧𝑥 ⊧𝜓). The claim that 𝑥 ⊧𝜓 involves only bounded quantifiers, since the quantifiers of 𝜓 become bounded by 𝑥. The claim that 𝑥 =𝑉𝜃 is Π1 in 𝑥 and 𝜃, since it is equivalent to saying that 𝑥 is transitive and the ordinals of 𝑥 are precisely 𝜃 and 𝑥 thinks every 𝑉𝛼 exists, plus a certain minimal set theory (so far this is just Δ0, since all quantifiers are bounded), plus, finally, the assertion that 𝑥 contains every subset of each of its elements. So altogether, the assertion that some 𝑉𝜃 satisfies 𝜓 has complexity Σ2 in the language of set theory.

(1 →3) This implication is a consequence of the following absoluteness lemma.

Lemma. (Levy) If 𝜅 is any uncountable cardinal, then 𝐻𝜅 ≺Σ1𝑉.

Proof. Suppose that 𝑥 ∈𝐻𝜅 and 𝑉 ⊧∃𝑦 ⁢𝜓⁡(𝑥,𝑦), where 𝜓 has only bounded quantifiers. Fix some such witness 𝑦, which exists inside some 𝐻𝛾 for perhaps much larger 𝛾. By the Löwenheim-Skolem theorem, there is 𝑋 ≺𝐻𝛾 with TC⁡({𝑥}) ⊂𝑋, 𝑦 ∈𝑋 and 𝑋 of size less than 𝜅. Let 𝜋 :𝑋 ≅𝑀 be the Mostowski collapse of 𝑋, so that 𝑀 is transitive, and since it has size less than 𝜅, it follows that 𝑀 ⊂𝐻𝜅. Since the transitive closure of {𝑥} was contained in 𝑋, it follows that 𝜋⁡(𝑥) =𝑥. Thus, since 𝑋 ⊧𝜓⁡(𝑥,𝑦) we conclude that 𝑀 ⊧𝜓⁡(𝑥,𝜋⁡(𝑦)) and so hence 𝜋⁡(𝑦) is a witness to 𝜓⁡(𝑥, ⋅) inside 𝐻𝜅, as desired. QED

Using the lemma, we now prove the remaining part of the theorem. Consider any Σ2 assertion ∃𝑥 ∀𝑦 ⁢𝜑0⁡(𝑥,𝑦), where 𝜑0 has only bounded quantifiers. This assertion is equivalent to ∃𝜅 𝐻𝜅 ⊧∃𝑥 ∀𝑦 ⁢𝜑0⁡(𝑥,𝑦), simply because if there is such a 𝜅 with 𝐻𝜅 having such an 𝑥, then by the lemma this 𝑥 works for all 𝑦 ∈𝑉 since 𝐻𝜅 ≺Σ1𝑉; and conversely, if there is an 𝑥 such that ∀𝑦 ⁢𝜑0⁡(𝑥,𝑦), then this will remain true inside any 𝐻𝜅 with 𝑥 ∈𝐻𝜅. QED

In light of the theorem, it makes sense to refer to the Σ2 properties as the locally verifiable properties, or perhaps as semi-local properties, since positive instances of Σ2 assertions can be verified in some sufficiently large 𝑉𝜃, without need for unbounded search. A truly local property, therefore, would be one such that positive and negative instances can be verified this way, and these would be precisely the Δ2 properties, whose positive and negative instances are locally verifiable.

Tighter concepts of locality are obtained by insisting that the property is not merely verified in some 𝑉𝜃, perhaps very large, but rather is verified in a 𝑉𝜃 where 𝜃 has a certain closeness to the parameters or instance of the property. For example, a cardinal 𝜅 is measurable just in case there is a 𝜅-complete nonprincipal ultrafilter on 𝜅, and this is verified inside 𝑉𝜅+2. Thus, the assertion “𝜅 is measurable,” has complexity Σ21 over 𝑉𝜅. One may similarly speak of Σ𝑛𝑚 or Σ𝛼𝑚 properties, to refer to properties that can be verified with Σ𝑚 assertions in 𝑉𝜅+𝛼. Alternatively, for any class function 𝑓 on the ordinals, one may speak of 𝑓-local properties, meaning a property that can be checked of 𝑥 ∈𝑉𝜃 by checking a property inside 𝑉𝑓⁡(𝜃).

This post was made in response to a question on MathOverflow.