查看“︁初等嵌入”︁的源代码

非平凡初等嵌入

设M、N为传递类且满足ZF⁻不含幂集公理的ZF

映射j:M→N为初等嵌入当且仅当对所有一阶公式φ(x₁,…,xₙ)及所有a₁,…,aₙ∈M都有

M⊨φ[a₁,…,aₙ]⇔N⊨φ[j(a₁),…,j(aₙ)]

该嵌入称为非平凡当且仅当存在x∈M使j(x)≠x

临界点

对非平凡初等嵌入j:M→N必存在最小序数κ使j(κ)≠κ

记crit(j)=κ

共尾性

嵌入j:M→N称为共尾当且仅当对所有y∈N存在x∈M使y∈j(x)

若M满足ZF且N⊆M则任何初等嵌入都是共尾的

Kunen定理

在ZFC框架下不存在非平凡初等嵌入j:V→V其中V为全集

更具体地Kunen中证明对任意序数λ不存在非平凡初等嵌入j:V{λ+2}→V{λ+2}使V满足ZFC