证明φ(v)为Σ₂公式的等价条件及φ'(v)的自然选择

嘿，最近我在研读Ralf Schindler的集合论著作时，碰到了这么一个需要证明的结论：

公式φ(v)是Σ₂公式当且仅当存在公式φ'(v)，使得ZFC⊢∀v(φ(v)↔∃α R(α)⊨φ'(v))

现在我卡在了一个点上：φ'(v)有没有自然的选择？我自己尝试过令φ'(v)=∃α Sat(R(α), φ(v))（这里的Sat是满足关系的形式化），但没成功，想跟大家聊聊这个问题。

首先得说清楚我那个尝试为啥行不通：我用了形式化的满足关系Sat，把φ(v)当成了一个哥德尔编码后的公式对象，但实际上我们需要的φ'(v)是直接的集合论公式，不是编码后的表达式。

那自然的选择到底是什么呢？其实答案很直接——φ'(v)就取φ(v)本身，或者更准确地说，取φ(v)的标准Σ₂范式形式，具体来说：

• 如果φ(v)是Σ₂公式，那它可以写成标准形式∃x∀yψ(v,x,y)，其中ψ是Δ₀公式。此时φ'(v)就用这个标准形式的公式。

为啥这个选择可行？我们可以结合反射原理和Σ₂公式的绝对性来验证：

1. 假设φ(v)在V中成立，也就是∃x∀yψ(v,x,y)为真。根据Σ₂反射原理，对于包含v的某个R(β)，存在α>β使得R(α)反射这个Σ₂公式，也就是R(α)⊨∃x∀yψ(v,x,y)，即R(α)⊨φ'(v)。
2. 反过来，如果存在α使得R(α)⊨φ'(v)，由于Σ₂公式在传递模型中是向上绝对的（传递模型中的Σ₂真语句在V中也为真），所以V⊨φ(v)。

这样一来，ZFC就能证明∀v(φ(v)↔∃α R(α)⊨φ'(v))，完全符合要求。

反过来，如果存在这样的φ'(v)，那φ(v)必然是Σ₂公式：因为R(α)⊨φ'(v)这个表达式的复杂度可以被控制在Δ₁（如果φ'是Δ₀的话），加上前面的∃α，整个公式就是Σ₂的，而φ(v)和它等价，所以φ(v)也是Σ₂的。

总结一下，不用绕到形式化的Sat关系那里，直接取φ(v)本身（或者它的标准Σ₂范式）就是最自然的φ'(v)选择。

内容的提问来源于stack exchange，提问作者PIandpie