数理逻辑及其 python 实现:6
Notes on 「Mathematical logic through python」
六、命题逻辑的语义完备性
The Tautology Theorem and the Completeness of Propositional Logic
我们回顾一下到为止的进展：
- 在第 4 章证明了可靠性定理,在给定的公理（infereneRule）都是可靠的情况下，
任何只采用这些公理的证明都是可靠的。
- 可靠性 (soundness) 的定义是，任何使得前提为真的模型在结论上也为真。
- 因此可靠性定理是一个从局部到全局的结论（数学归纳性质），我们只谈论了几条有限的推理规则（公理）的可靠性，却得到了用这些推理规则组成的任意长度的推理证明也是可靠的。
- 这同样是一个从语法到语义的性质，因为推理规则描述的纯粹是语法的变换， 只是词汇的替换或者顺序的改变，但由于变换规则的可靠从而确保了整个看似机械无意义的变换序列都是可靠的。
- 第 5 章引入了一致性，这是一个对证明中语法现象的描述，某个假设集合 A 与预设的逻辑公理系统是一致的，那么从假设集合 A 中无法导出形式上的矛盾命题：例如 I0 的否定 ~(p->p) 。
本章要处理的是 soundness 性质的对偶性质：给定任何 sound 的推理规则，该规则一定是可以被证明。
由于上一节已经建立了命题 f 可从 A 证明以及 A+{~f} 系统是不一致的等价关系，因此这种性质还可以用不一致性来阐明，在后文中会被详细探讨。
我们还是回到 "给定任何 sound 的推理规则，该规则一定是可以被证明" 这一论断，这是一个全称性质，需要覆盖所有 sound 的推理规则，为了能够进行这类全局性的归纳，我们需要对推理规则的表达方式进行一定的约定，或者说形式的统一，然后讨论这种形式的通用性质，从而证明所有形式都具有某种特点。 在第五章，所有公式就已经完全限制在只允许使用 ~ 和 -> 两个连接符了，而第 3 章证明了所有公式都可以转成 ~ 和 -> 形式，因此在符号上已经相对统一了。 另一个顾虑是推理规则中前提数量的问题，根据定义，推理规则可以有任意多个前提，它对应了任意多的假设。如果只有 1 个前提，比如 "[p] 得到 q" ，根据 deduction theorem, 可以把它转成无条件的 "[] 得到 p->q" 规则，如果有两个或以上前提，比如 "[p,q] 得到 r", 我们还没有定理可以把它统一化，当然直觉上看，这等价于 \( (p \& q) \to r \), 然后再把它转成 ~ 和 -> 表示。 在 T5.3 里提到，这种形式也可以转化为 (p->(q->r)) 形式, 二者真值表是一样的：
print_truth_table(Formula.parse('((p&q)->r)'))
| p | q | r | ((p&q)->r) | |---|---|---|------------| | F | F | F | T | | F | F | T | T | | F | T | F | T | | F | T | T | T | | T | F | F | T | | T | F | T | T | | T | T | F | F | | T | T | T | T |
print_truth_table(Formula.parse('(p->(q->r))'))
| p | q | r | (p->(q->r)) | |---|---|---|-------------| | F | F | F | T | | F | F | T | T | | F | T | F | T | | F | T | T | T | | T | F | F | T | | T | F | T | T | | T | T | F | F | | T | T | T | T |
如果有更多前提，都能写成类似 (p1->(p2->(p3->q)))) 的形式，我将其记为蕴含链形式。
我们可以通过 p->q 和 ~p|q 等价来推导出任意多个命题在这种形下与 (p1&…&pn)->q 的等价性，后者等价于 ~(p1&…&pn)|q 根据德摩根定律有 (~p1|~p2|…|pn)|q, 而根据 | 运算结合率，从右到左可以逐渐写成蕴含链形式。
因此所有推理规则都可以根据演绎定理转成以上蕴含链形式的无前提的定理，它就等价于静态的命题，而所有 sound 定理转成这类命题后实际都是恒真的（根据 sound 的定义），于是本章先证明所有（只包含 -> 和 ~ 的）恒真式都是可以被证明的，然后推广到所有 sound 的定理。
而要从恒真（语义层面）到能够证明（语法层面），需要一种逆向构造公式的过程，类似的问题在第二章构造 CNF 公式时遇到过，本章同样会用到相似的做法。
希尔伯特公理系统和公式标准化的说明
本章中使用到的所有公理如下：
#: Modus ponens / implication elimination
MP = InferenceRule([Formula.parse('p'), Formula.parse('(p->q)')],
Formula.parse('q'))
#: Self implication
I0 = InferenceRule([], Formula.parse('(p->p)'))
#: Implication introduction (right)
I1 = InferenceRule([], Formula.parse('(q->(p->q))'))
#: Self-distribution of implication
D = InferenceRule([], Formula.parse('((p->(q->r))->((p->q)->(p->r)))'))
# Axiomatic inference rules for not (and implies)
#: Implication introduction (left)
I2 = InferenceRule([], Formula.parse('(~p->(p->q))'))
#: Converse contraposition
N = InferenceRule([], Formula.parse('((~q->~p)->(p->q))'))
#: Negative-implication introduction
NI = InferenceRule([], Formula.parse('(p->(~q->~(p->q)))'))
#: Double-negation introduction
NN = InferenceRule([], Formula.parse('(p->~~p)'))
#: Resolution
R = InferenceRule([], Formula.parse('((q->p)->((~q->p)->p))'))
#: Large axiomatic system for implication and negation, consisting of `MP`,
#: `I0`, `I1`, `D`, `I2`, `N`, `NI`, `NN`, and `R`.
AXIOMATIC_SYSTEM = frozenset({MP, I0, I1, D, I2, N, NI, NN, R})
希尔伯特证明，只需要以下四条公理就可以推导出以上的所有公理，但为了方便，我们还是将以上所有公理直接作为推理规则使用
#: Hilbert axiomatic system for implication and negation, consisting of `MP`,
#: `I1`, `D`, and `N`.
HILBERT_AXIOMATIC_SYSTEM = frozenset({MP, I1, D, N})
T6.1 模型的捕获集合
捕获赋值的定义如下，我们根据模型构造出捕获集合，那么该捕获集合里所有的命题相对该模型来说都是真的，并且它们的蕴含链形式也是真的
Given an assignment of a Boolean value b to a variable name x, the formula that captures this assignment is the formula ‘x’ if b is True and is the formula ‘~x’ if b is False. Given a model {x1 : b1, x2 : b2, . . . , xn : bn}, where each xi is a variable name and each bi is a Boolean value, the set of formulas that captures this model is the set of the n formulas that capture the n assignments in the model.
definition 6.1 (Formula(s) Capturing Assignment)
以下是获得模型捕获集合的函数实现，后文将捕获集合记录为 C, 如果针对具体模型，则记录为 C(M)：
def formulas_capturing_model(model: Model) -> List[Formula]:
assert is_model(model)
# Task 6.1a
res = []
for v in sorted(model.keys()):
if model[v]:
res.append(Formula(v))
else:
res.append(Formula("~", Formula(v)))
return res
print(formulas_capturing_model({'p': False, 'q': True, 'r': True}))
[~p, q, r]
这是一种根据语义建立语法的逆向构造公式的简单手段，在 CNF 中也看到过类似做法，CNF 定理说的是，给定任何一个真值表，我们都可以构造一个唯一的 CNF 形式公式来实现这个真值表。现在我们想要的不单是从语义构造出公式，而是从语义构造出对公式的证明。
由于 C(M) 中的命题都是真的，那么将该集合作为前提的情况下，如果某个公式 f 相对于 M 是假，那么 C->~f 就是真，如果 f 相对于 M 是真，那么 C->f 就是真。 但我们想要的不是某个恒真的公式，而是对这些公式的证明。
我们先看最简单的命题 p, 它不是重言的，在两个可能模型 {p:True} 和 {p:False} 中的取值分别是真和假。
- {p:True} 的捕获集 C={p}, 以 C 作为前提我们可以直接得到 p 的证明。
- {p:False} 的捕获集 C={~p}, 此时 p 命题为假，因此正常来说，我们无法从恒真的捕获集 {~p} 证明出 p. 但我们知道，~p 是真的，于是可以证明命题 p 的反面 ~p 。
它说明，对于 p 这个非重言命题，如果它为真，我们可以直接从 C 给出证明，如果它为假，那么我们可以证明它的否定形式。
这有什么用呢？
对于非重言命题，给定使得该命题为真的模型，我们可以从其捕获集合证明出该命题，给定为假的模型，我们可以从其捕获集合证明出该命题的否定形式。如果是重言命题呢？重言意味着它没有对应为假的模型，于是我们从任何模型的捕获集出发 都能证明该命题，那么我们要做的就是把所有这些从不同捕获集出发的证明合并起来，最终得到从空假设集出发到重言命题 的证明，这就是给定任何重言命题都可以返回其推导过程的证明思路。
但我们只谈论了单变量命题 p, 而一般的命题都是复合的，比如 p->(~p->q), 因此我们需要一种与命题的复合方式相对应的证明的复合方式。
以 p->p 为例，我们还是有两个可能模型 {p:True} 和 {p:False}, 但 p->p 在其上都是真，而该命题是由 -> 连接的，这类命题为真的话，要么前提为假，要么结论为真。
- {p:True} 的捕获集 C={p}, 以 C 作为前提我们可以直接得到 p 的证明，由于 p->p 为真，我们检查发现其前提为真，这意味着它的结论一定为真，通过 I1 公理 '(q->(p->q))' 以及 MP 规则就可以构造出对 p->p 的证明。
- {p:False} 的捕获集 C={~p}, 这时候我们遇到了 p->p 为真的另外一个条件，即前提为假，那么我们可以去证明前提的反面 ~p, 根据公理 I2 '(~p->(p->q))' 以及 MP 规则可以得到 p->p 的证明。
这样，我们分别得到了从 {p} 以及 {~p} 到 p->p 的证明，根据演绎定理，我们实际得到了对 p->(p->p) 以及 ~p->(p->p) 的证明，再引入公理 R: ('((q->p)->((~q->p)->p))', 我们可以消除掉互为逆命题的前提，直接得到结论 (p->p)
以下是从模型（某个捕获集）证明公式的函数，下一节则是实现消解捕获集的函数。
def prove_in_model(formula: Formula, model:Model) -> Proof:
assert formula.operators().issubset({'->', '~'})
assert is_model(model)
# Task 6.1b
assumptions = formulas_capturing_model(model)
value = evaluate(formula, model)
if is_variable(formula.root):
if value:
statement = InferenceRule(assumptions, formula)
line = Proof.Line(formula)
return Proof(statement, AXIOMATIC_SYSTEM, [line])
else:
formula = Formula("~", formula)
statement = InferenceRule(assumptions, formula)
line = Proof.Line(formula)
return Proof(statement, AXIOMATIC_SYSTEM, [line])
if formula.root == '~':
if value:
return prove_in_model(formula.first, model)
else:
proof = prove_in_model(formula.first, model)
return prove_corollary(proof, Formula("~", formula), NN)
elif formula.root == '->':
if value:
v1, v2 = evaluate(formula.first, model), evaluate(formula.second, model)
if not v1: # p is false in p->q
proof = prove_in_model(formula.first, model)
return prove_corollary(proof, formula, I2)
else: # q is true in p->q
proof = prove_in_model(formula.second, model)
return prove_corollary(proof, formula, I1)
else:
proof1 = prove_in_model(formula.first, model)
proof2 = prove_in_model(formula.second, model)
return combine_proofs(proof1, proof2, Formula("~", formula), NI)
该函数算是一个比较精彩的递归，核心在于把所有公式只用 ~ 和 -> 连接，并且所有公理系统给出的也只有 ~ 和 ->, 这样，对于任何 evaluate 为 True 的公式和 model, 可以递归地去解析和构建证明。
T6.2 捕获集中假设的消解
reduce_assumption
T6.1 中证明了任何公式，在给定某个模型的情况下，如果为真，那么就可以写出从该模型捕获集合到该公式的证明，如果为假，则可以写出从模型捕获集合到该公式的否定的证明，也就是如下引理：
Let φ be a formula that only uses the operators ‘→’ and ‘~’. If φ evaluates to True in a given model M, then φ is provable via H from the set of formulas that captures M. If φ evaluates to False in M, then ‘~φ’ is provable via H from the set of formulas that captures M
lemma 6.1
由于恒真式在给定任何模型情况下都是真的，因此对于一个包括 n 个变量的恒真的式子，可以构造 \( 2^n \) 个捕获集，并据此写出 \( 2^{n} \) 个证明。但我们要的是对该公式无前提的证明，因为恒真就是无前提下恒为真，于是本节就要引出消解方式。
def reduce_assumption(proof_from_affirmation: Proof,
proof_from_negation: Proof) -> Proof:
"""
Examples:
If `proof_from_affirmation` is of ``['p', '~q', 'r'] ==> '(p&(r|~r))'``,
then `proof_from_negation` must be of
``['p', '~q', '~r'] ==> '(p&(r|~r))'`` and the returned proof is of
``['p', '~q'] ==> '(p&(r|~r))'``.
"""
assert proof_from_affirmation.is_valid()
assert proof_from_negation.is_valid()
assert proof_from_affirmation.statement.conclusion == \
proof_from_negation.statement.conclusion
assert len(proof_from_affirmation.statement.assumptions) > 0
assert len(proof_from_negation.statement.assumptions) > 0
assert proof_from_affirmation.statement.assumptions[:-1] == \
proof_from_negation.statement.assumptions[:-1]
assert Formula('~', proof_from_affirmation.statement.assumptions[-1]) == \
proof_from_negation.statement.assumptions[-1]
assert proof_from_affirmation.rules == proof_from_negation.rules
# Task 6.2
consequent = proof_from_affirmation.statement.conclusion
affirmation = remove_assumption(proof_from_affirmation)
negation = remove_assumption(proof_from_negation)
pq = affirmation.statement.conclusion
_pq = negation.statement.conclusion
return combine_proofs(affirmation, negation, consequent, R)
本题与 T5.4 remove_assumption 名字很像，实际基本都是基于后者，主要用到了公理 R: ('((q->p)->((~q->p)->p))'
T6.3 证明任意恒真表达式（公理）可被证明
准备：
from typing import Any, Callable, Dict, Iterator, Set, Type, TypeVar, cast
class frozendict(Dict[Any, Any]):
"""An immutable variant of the built-in `dict` class."""
def __init__(self, *args, **kwargs):
super().update(dict(*args, **kwargs))
def update(self, *args, **kwargs):
raise Exception('Cannot modify a frozendict')
__delattr__ = __delitem__ = __setattr__ = __setitem__ = clear = pop = \
popitem = setdefault = cast(Callable[..., Any], update)
对重言定理的证明，主要是在消解变量，给定 n 个变量的公式，要消解完需要 2**n 的 proof 合并操作。
以下函数是一个递归算法，给定的 model 中变量应该小于等于恒真式中的变量数，在等于的情况下，直接返回 prove_in_model 的结果，否则进行消解：
def prove_tautology(tautology: Formula, model: Model = frozendict()) -> Proof:
assert is_tautology(tautology)
assert tautology.operators().issubset({'->', '~'})
assert is_model(model)
assert sorted(tautology.variables())[:len(model)] == sorted(model.keys())
# Task 6.3a
tvars = sorted(tautology.variables())
mvars = sorted(model.keys())
if len(tvars) == len(mvars):
return prove_in_model(tautology, model)
pos = model.copy()
pos[tvars[len(model)]] = True
pos = prove_tautology(tautology, pos)
neg = model.copy()
neg[tvars[len(model)]] = False
neg = prove_tautology(tautology, neg)
return reduce_assumption(pos, neg)
proof = prove_tautology(Formula.parse('(~(p->p)->q)'))
print(proof.is_valid())
以上证明就有几百行。
以下是对任何公式的一个判断，如果该公式是恒真则返回证明，否则返回一个错误的 model, 需要遍历 all model 去判断是否重言（恒真）。
def proof_or_counterexample(formula: Formula) -> Union[Proof, Model]:
assert formula.operators().issubset({'->', '~'})
# Task 6.3b
for model in all_models(formula.variables()):
if not evaluate(formula, model):
return model
return prove_tautology(formula, {})
T6.4 证明任意定理可被证明
当前知道，所有恒真表达式（无前提定理）都可以被证明，那么这里就是把所有有前提的定理转为无前提定理：
def encode_as_formula(rule: InferenceRule) -> Formula:
# Task 6.4a
consequent = rule.conclusion
for assumption in reversed(rule.assumptions):
consequent = Formula("->", assumption, consequent)
return consequent
print(encode_as_formula(InferenceRule([Formula('p1'), Formula('p2'),
Formula('p3'), Formula('p4')],
Formula('q'))))
(p1->(p2->(p3->(p4->q))))
于是对任何定理都可以返回一个证明
def prove_sound_inference(rule: InferenceRule) -> Proof:
assert is_sound_inference(rule)
for formula in {rule.conclusion}.union(rule.assumptions):
assert formula.operators().issubset({'->', '~'})
# Task 6.4b
proof = prove_tautology(encode_as_formula(rule), {})
lines = list(proof.lines)
cur = len(lines)
for i, a in enumerate(rule.assumptions):
lines.append(Proof.Line(a))
lines.append(Proof.Line(lines[cur - 1].formula.second, MP, [cur, cur - 1]))
cur += 2
return Proof(rule, proof.rules, lines)
本节的函数实现证明了：
For any finite set of formulas A and any formula φ, it is the case that A |= φ if and only if A |-H φ.
theorem 6.2 (The Completeness Theorem for Finite Sets: “Provability” Version)
T6.5 用一致性来描述完备性
本节试图用一致性来描述完备性，即逻辑系统的一致性等价于该逻辑系统拥有一个（对应为真的）模型。
这种说法使得我们能谈论某个系统的性质，而不是具体的某个命题是否可以被证明。
接下来对比逻辑系统完备性多种不同的视角，从而引出一致性视角：
用命题的可证明性（语法）和蕴含性（语义）来表达：
如果逻辑公理和假设集合 A 蕴含了公式 f, 那么公式 f 一定能够从假设集合中根据公理规则推导出来。蕴含意味着对于在 A 上为真的模型，在 f 上也一定为真。
A 证明 f <--> A 蕴含 f
- 从左到右箭头的证明来自 soundness 定理。
- 从右到左箭头的证明来本章前文的实现，其核心是重言定理。
第五章证明了以下等价关系
A+{~f} 系统是不一致的 <--> A 证明出 f这里 A+{~f} 系统实际是指以 A+{~f} 作为假设集并且包含希尔伯特公理集的命题逻辑系统
- 从左到右方向箭头的证明基于演绎定理和逆否公理
- 从右到左箭头证明则是相对平凡的论述
结合这两重等价：
A+{~f} 系统是不一致的 <--> A 证明出 f <--> A 蕴含 f可以把中间对象拿掉：
A+{~f} 系统是不一致的 <--> A 蕴含 f但要清楚：
- 从左到右方向箭头来自于两个阶段的证明：第一阶段从不一致到可证主要基于演绎定理， 第二阶段基于 soundness 定理。
- 从右到左方向箭头同样来自两个阶段证明，但其核心是从可蕴含到可证是基于重言定理（继而基于演绎定理），
A 蕴含 f 意味着所有满足 A 的模型都满足 f, 那么所有不满足 f 的模型都不满足 A, 也就是所有满足 ~f 的模型都不满足 A, 因此 A+{~f} 系统是没有对应的真模型的。
A 蕴含 f -> A+{~f} 系统无模型反过来，如果 A+{~f} 系统无模型，那么要么就是没有任何模型能满足 A 系统，那么 A 蕴含 f 是自然成立的。 要么就是 A 系统原本有模型，加入 ~f 后无模型，这说明满足 A 的模型都不满足 ~f，那么根据集合论，满足 A 的模型自然就都满足 f 了，于是 A 蕴含 f 。这部分论述完全来自模型的语义世界（由于模型是用集合表示， 因此都是集合论保证的）
A 蕴含 f <-> A+{~f} 系统无模型于是：
A+{~f} 系统是不一致的 <--> A+{~f} 系统无模型现在我们可以说，如果 A+{~f} 系统无模型，那么 A+{~f} 系统是不一致的，注意这种说法实际，可以从 A 证明到 f
这个时候：
- 从左到右方向箭头来自三个阶段：第一阶段从不一致到可证是基于演绎定理和逆否公理， 第二阶段基于 soundness 定理，第三阶段基于模型的集合性质。
- 从右到左方向箭头同样来自三个阶段：先基于集合论性质，接着从可蕴含到可证是基于重言定理， 从可证到不一致则是比较平凡地论述。这是相对困难方向
两边都取否定：
A+{~f} 系统是一致的 <--> A+{~f} 系统有模型现在我们可以说，如果 A+{~f} 系统有模型，那么无法从 A 证明到 f
这个时候左右两个箭头的合法性基础反转了：
- 从左到右方向箭头来自三个阶段：先基于集合论性质，接着从可蕴含到可证是基于重言定理， 从可证到不一致则是比较平凡地论述。这是相对困难方向
- 从右到左方向箭头来自三个阶段： 第一阶段从不一致到可证是基于演绎定理和逆否公理， 第二阶段基于 soundness 定理，第三阶段基于模型的集合性质。
把 A+{~f} 看作一个大假设集，比如 S, 那么：
S 系统是一致的 <--> S 系统有模型
注意这句话彻底把某个具体命题 f 给隐藏了，它谈论的是逻辑系统的性质。
- 从左到右核心是基于重言定理
- 从右到左核心是基于 soundness 定理。
它们都用到了演绎定理。
还可以有
证明出 ~(p->p) <--> S 系统是不一致的 <--> S 系统没有模型
model_or_inconsistency 函数实现如下，它实际提供了另一种证明完备性（困难方向）的方式：
如果给定的 S 在语义检查中发现了模型，那么我们可以直接构造出一个这样的模型（因为模型空间虽然是指数级但至少是有限可遍历的），如果找不到这个模型，那么系统就是不一致的，从而可以证明任意一个公理的否定命题，这里选择的是 ~(p->p)。这种方式在谓词逻辑的完备性证明中会被使用。
def model_or_inconsistency(formulas: Sequence[Formula]) -> Union[Model, Proof]:
for formula in formulas:
assert formula.operators().issubset({'->', '~'})
# Task 6.5
variables = set()
for formula in formulas:
variables = variables | formula.variables()
for model in all_models(variables):
flag = True
for formula in formulas:
if not evaluate(formula, model):
flag = False
break
if flag:
return model
rule = InferenceRule(formulas, conclusion=Formula.parse("~(p->p)"))
return prove_sound_inference(rule)
这证明了：
A finite set of formulas has a model if and only if it is consistent with respect to H
theorem 6.3 (The Completeness Theorem for Finite Sets: “Consistency” Version)
最后不要忘记：
- 可证明性只有在突出 ~f 的时候才体现出来，并且是在不一致的语境下，即 A+{~f} 不一致或无模型那么可以有从 A 到 f 的证明。
- 如果 A+{~f} 一致，说明不能从 A 证明到 f
如果 A+{~f} 一致，我们不知道是否可以从 A 证明到 ~f, 比如假设 A 集合只有命题 1+1=2, f 是命题 "下雨了"，它们之间是独立的，但我们无法从 1+1=2 推导出下雨了，也无法推导出没有下雨。
这给公理集合的扩充留下了很多可以谈论却不容易谈论的问题，比如公理集中的命题是否是独立的？