查看“︁合同引理”︁的源代码

[[分类:证明论]]
{{InfoBox
|name=合同引理
|eng_name=
}}
'''合同引理'''指[[项（谓词逻辑）|项]]在[[赋值]]下的值、[[谓词公式]]在赋值下的真值，都仅依赖于赋值对其中出现的符号的解释。

== 定理 ==

对模型 <math>\mathfrak{A} = \left\langle A, I \right\rangle, \mathfrak{A}' = \left\langle A', I'\right\rangle</math> ，有任意两个分别在两个模型上的赋值 <math>\sigma,\tau</math> ：
# 若对项 <math>t</math> ，有所有 <math>t</math> 中出现的 <math>\mathcal{L}</math>-符号 <math>x</math> 都有 <math>x^\sigma = x^\tau</math> ，则 <math>t^\sigma = t^\tau</math> 。
# 若对公式 <math>\phi</math> ，有所有 <math>\phi</math> 中出现的非逻辑符号 <math>x</math> 都有 <math>x^\sigma = x^\tau</math> ，则 <math>\phi^\sigma = \phi^\tau</math> 。


{{证明论}}