Tarski–Vaught 测试
| 塔斯基–沃特测试 | |
|---|---|
| 术语名称 | 塔斯基–沃特测试 |
| 英语名称 | Tarski–Vaught test |
| 别名 | Tarski–Vaught criterion, Tarski–Vaught theorem |
本条目没有一致可信的中文译名。
Tarski–Vaught 测试(Tarski–Vaught test)或Tarski–Vaught 标准(Tarski–Vaught criterion)是关于两个模型间初等子模型充要条件的定理，在较大的结构之间初等子结构的构造中经常使用。
定理
对语言 [math]\displaystyle{ \mathcal{L} }[/math] 的两个模型 [math]\displaystyle{ \mathfrak{A} }[/math] 和 [math]\displaystyle{ \mathfrak{B} }[/math] ，则初等子模型关系 [math]\displaystyle{ \mathfrak{A}\preceq\mathfrak{B} }[/math] 成立当且仅当： 对任意含有自由变元 [math]\displaystyle{ x_0,\cdots,x_n }[/math] 的公式 [math]\displaystyle{ \phi }[/math] 和任意 [math]\displaystyle{ a_0,\cdots,a_n\in A }[/math] ，若对某个 [math]\displaystyle{ b\in B }[/math] 有 [math]\displaystyle{ \mathfrak{B}\vDash\phi[a_0/x_0,\cdots,a_{i-1}/x_{i-1},b/x_i,a_{i+1}/x_{i+1},\cdots,a_n/x_n] }[/math] ，都存在 [math]\displaystyle{ a\in A }[/math] 满足 [math]\displaystyle{ \mathfrak{B}\vDash\phi[a_0/x_0,\cdots,a_{i-1}/x_{i-1},a/x_i,a_{i+1}/x_{i+1},\cdots,a_n/x_n] }[/math] 。
说明
尽管两个模型论域不同， [math]\displaystyle{ A\subseteq B }[/math] 由于初等子模型要求在两个模型中同时成立或同时不成立，对涉及 [math]\displaystyle{ B\setminus A }[/math] 的命题，必须有对应的只在 [math]\displaystyle{ A }[/math] 内成立的取值才能满足。这一定理说明了在只有一个变量取值在这个范围内时，必然可以保证在其他赋值不变的情况下存在这样的取值。