合同引理
| 合同引理 | |
|---|---|
| 术语名称 | 合同引理 |
| 英语名称 | |
合同引理指项在赋值下的值、谓词公式在赋值下的真值，都仅依赖于赋值对其中出现的符号的解释。
定理
对模型 [math]\displaystyle{ \mathfrak{A} = \left\langle A, I \right\rangle, \mathfrak{A}' = \left\langle A', I'\right\rangle }[/math] ，有任意两个分别在两个模型上的赋值 [math]\displaystyle{ \sigma,\tau }[/math] ：
- 若对项 [math]\displaystyle{ t }[/math] ，有所有 [math]\displaystyle{ t }[/math] 中出现的 [math]\displaystyle{ \mathcal{L} }[/math]-符号 [math]\displaystyle{ x }[/math] 都有 [math]\displaystyle{ x^\sigma = x^\tau }[/math] ，则 [math]\displaystyle{ t^\sigma = t^\tau }[/math] 。
- 若对公式 [math]\displaystyle{ \phi }[/math] ，有所有 [math]\displaystyle{ \phi }[/math] 中出现的非逻辑符号 [math]\displaystyle{ x }[/math] 都有 [math]\displaystyle{ x^\sigma = x^\tau }[/math] ，则 [math]\displaystyle{ \phi^\sigma = \phi^\tau }[/math] 。
| 证明论 | |
|---|---|
| 形式化公理系统（形式化、公理化） | |
| 推理系统 | Hilbert 风格/公理系统：Hilbert 表示 |
| Gentzen 风格-自然演绎系统： Gentzen 式自然演绎、 Fitch 式自然演绎、 Suppes–Lemmon 式自然演绎 | |
| Gentzen 风格-相继式演算： Gentzen 式相继式演算 | |
| 证明、演绎 | 演绎、可演绎、证明、可证明 |
| 命题、定理 | 公理/公理模式、定理、元定理、变形规则 |
| 推理规则性质 | 保存真实性、保存重言性 |
| 公理系统性质 | 可靠性、完备性/完全性、一致性、独立性 |