数理逻辑及其 python 实现:4
Notes on 「Mathematical logic through python」
四、命题逻辑的演绎证明
本章引入了 Proof, InferenceRule 这些语法上的操作对象，同时引入了它们的语义特点（是否 sound），并且最终证明了 soundness 定理（从语法连接到语义）
An inference rule is composed of a list of zero or more propositional formulas called the assumptions of the rule and one additional propositional formula called the conclusion of the rule.
definition 4.1 (Inference Rule)
首先定义推理规则类 InferenceRule, 它包括 assumptions （tuple of formula 或者空 tuple） 和 conclusion 对象。
class InferenceRule:
assumptions: Tuple[Formula, ...]
conclusion: Formula
def __init__(self, assumptions: Sequence[Formula], conclusion: Formula):
self.assumptions = tuple(assumptions)
self.conclusion = conclusion
def __repr__(self) -> str:
return str([str(assumption) for assumption in self.assumptions]) + \
' ==> ' + "'" + str(self.conclusion) + "'"
def __eq__(self, other: object) -> bool:
return isinstance(other, InferenceRule) and \
self.assumptions == other.assumptions and \
self.conclusion == other.conclusion
def __ne__(self, other: object) -> bool:
return not self == other
def __hash__(self) -> int:
return hash(str(self))
assumptions 就是一组公式或者是空集，conclusion 则是一个公式（Formula）
推理规则可以让我们进行演绎(deduce)，或者说是生成公式，可以把推理规则看作是字符串（公式）生成模板或函数。
T4.1 从推理规则中取出变量
遍历 assumptions 以及 conclusion 中所有公式, 调用各个公式的 variables() 函数，然后合并各变量
def inf_variables(self) -> Set[str]:
# Task 4.1
res = set()
for assumption in self.assumptions:
res |= assumption.variables()
res |= self.conclusion.variables()
return res
InferenceRule.variables = inf_variables
为什么要提取变量？主要目的是构造模型，并检查证明中是否有错误的公式
T4.2 模型和推理规则的关系
We say that a set of assumption formulas A entails a conclusion formula φ if every model that satisfies all the assumptions in A also satisfies φ. We denote this by A |= φ.
We say that the inference rule whose assumptions are the elements of the set A and whose conclusion is φ is sound(truth-preserving ) if A |= φ.
definition 4.2 (Entailment; Soundness)
以上对推理规则可靠性（也称保真性）的定义是纯语义上的，因为只涉及到命题和 model 之间的关系，如果某推理规则是可靠的：
- 所有使得前提为真的 model 在结论中都为真
- 或者没有任何 model 使得前提为真
- 或者前提为空但 conclusion 恒真
以上语义的描述和逻辑运算符 -> 非常像，但它是动态的生成规则，而 -> 是静态的公式连接符号。在后文中会证明这两者是等价的。正如在第一章第一节提到，命题逻辑发明的一个重要原因就是研究 "蕴含", 而蕴含通过 -> 符号以及该符号的语义定义体现在了逻辑表达式中，也通过对推理规则的 soundness 体现在了推理过程中，不过：
- 推理规则一般不用"真"或"假"来分类：推理规则的“真”是用 sound 来表示（可以称为可靠或者保真）
- 公式才用真和假来表示；
比如以下的对推理规则语义检查函数，它返回的也是 True 和 False, 但这里的 True 表示的是该推理规则在某个模型下。
def evaluate_inference(rule: InferenceRule, model: Model) -> bool:
assert is_model(model)
# Task 4.2
for formula in rule.assumptions:
if not evaluate(formula, model):
return True
return evaluate(rule.conclusion, model)
注意：在以上代码中，根据 soundness 的定义，我们只关心符合 assumptions 的 model, 因此如果 model 使得推理规则中的某个 assumption 为 Fasle, 那么它就不会被作为验证推理规则是否为 soundness 的候选模型了，因此这里认为该推理规则在该模型下是 True，这个“隐性”的性质直接使得推理的语义和 imply 非常相似
T4.3 验证推理规则的 soundness
由于 soundness 是通过语义定义的，因此检查某个推理规则是否是 sound 的方式就是遍历整个语义空间，看是否在所有模型下，推理规则的前提都蕴含着结论
def is_sound_inference(rule: InferenceRule) -> bool:
for model in all_models(rule.variables()):
if not evaluate_inference(rule, model):
return False
return True
这与验证 (p&q&r)->z 形式的 formula 是否是 tautlogy 的算法是类似的。假设推理规则涉及 n 个变量，那么得到 2**n 个 model
T4.4 推理规则的实例化
本章开头提过，推理规则是一种模版，大部分情况下需要实例化才能使用起来（严重依赖替换规则）
An inference rule β is a specialization of an inference rule α if there exist a number of formulas φ1, . . . , φn and a matching number of variable names v1, . . . , vn, such that β is obtained from α by (simultaneously) substituting the formula φi for each occurrence of the variable name vi in all of the assumptions of α (while maintaining the order of the assumptions) as well as in its conclusion.
definition 4.3 (Specialization)
由于实现了公式的实例化，因此只要遍历 InferenceRule 对象中各公式进行变量替换即可：
def inf_specialize(self, specialization_map: SpecializationMap) -> \
InferenceRule:
for variable in specialization_map:
assert is_variable(variable)
# Task 4.4
new_assumptions = []
for assumption in self.assumptions:
new_assumptions.append(assumption.substitute_variables(specialization_map))
new_conclusion = self.conclusion.substitute_variables(specialization_map)
return InferenceRule(new_assumptions, new_conclusion)
InferenceRule.specialize = inf_specialize
注意我们只需要变量替换，而不需要操作符替换
T4.5 实例化逆向工程
本问题是为了实现判断当前推理规则是否是另外一个推理规则的实例，类似 python 中的 isinstance 函数。
算法上看，这相当于比较两个推理规则是否同构，首先二者必须满足 assumption 数量一致，接着检查所有 assumption （排列顺序默认是一致的）和结论公式的语法树，逐一比较两棵树（或者有向无环图）是否在"骨架"上同构：
- 比如 p^q 和 (a|b)^q 可以看作是同构的，因为它们都是一个 ^ 结构，只不过前者左分支是 p, 后者左分支是 (a|b)。
因此这个任务分解成：
- 成对遍历推理规则中各公式
- 对各对公式进行树比较，并且抽取出变量替换表，
- 然后合并替换表，合并时这些不同映射表应该是一致的，也就是说，如果两个公式中都对 p 进行了替换，那它们的替换的对象必须一样，比如如果前提公式中变量 p 被实例化成了 q^r, 那么结论中的变量 p 也应该被实例化成 q^r. Task 4.5a 是合并函数的实现：
@staticmethod
def inf_merge_specialization_maps(
specialization_map1: Union[SpecializationMap, None],
specialization_map2: Union[SpecializationMap, None]) -> \
Union[SpecializationMap, None]:
if specialization_map1 is not None:
for variable in specialization_map1:
assert is_variable(variable)
if specialization_map2 is not None:
for variable in specialization_map2:
assert is_variable(variable)
# Task 4.5a
if specialization_map1 is None:
return None
if specialization_map2 is None:
return None
merged = {}
for var in specialization_map1:
f = specialization_map2.get(var, specialization_map1[var])
if specialization_map1[var] != f:
return None
else:
merged[var] = specialization_map1[var]
for var in specialization_map2:
if var not in merged:
merged[var] = specialization_map2[var]
return merged
InferenceRule._merge_specialization_maps = inf_merge_specialization_maps
Task 4.5b 是对两个树递归做同构判断, 如果同构, 则返回映射表, 否则返回 None：
@staticmethod
def inf_formula_specialization_map(general: Formula, specialization: Formula) \
-> Union[SpecializationMap, None]:
# Task 4.5b
if is_variable(general.root):
return {general.root: specialization}
if is_constant(general.root) and general.root == specialization.root:
return {}
if general.root != specialization.root:
return None
first_map = None
if hasattr(general, "first"):
if not hasattr(specialization, "first"):
return None
first_map = InferenceRule._formula_specialization_map(general.first,
specialization.first)
if hasattr(general, "second"):
if not hasattr(specialization, "second"):
return None
second_map = InferenceRule._formula_specialization_map(general.second,
specialization.second)
return InferenceRule._merge_specialization_maps(first_map, second_map)
return first_map
InferenceRule._formula_specialization_map = inf_formula_specialization_map
注意只在遍历最后的叶子节点开始搜集映射表，然后在递归返回的时候向上合并，类似后序遍历算法。
Task 4.5c 是做更高层的判断，比如两个推理规则的 assumptions 数量是否一样：
def inf_specialization_map(self, specialization: InferenceRule) -> \
Union[SpecializationMap, None]:
# Task 4.5c
res = {}
if len(self.assumptions) != len(specialization.assumptions):
return None
for general, spec_formula in zip(self.assumptions, specialization.assumptions):
smap = InferenceRule._formula_specialization_map(general, spec_formula)
res = InferenceRule._merge_specialization_maps(res, smap)
if not res:
return None
smap = InferenceRule._formula_specialization_map(self.conclusion,
specialization.conclusion)
res = InferenceRule._merge_specialization_maps(res, smap)
return res
InferenceRule.specialization_map = inf_specialization_map
由于这种分解的清晰性，最后 is_specialization_map 非常精简：
def inf_is_specialization_of(self, general: InferenceRule) -> bool:
print("self, general:", self, general)
return general.specialization_map(self) is not None
InferenceRule.is_specialization_of = inf_is_specialization_of
这个 Task 提供了一个很好地问题分解后实现的案例。
T4.6 检查证明（Proof）是否有效
本节引入了另一个重要对象：证明； 它包括：
- 要证明的对象 statement, 这是一个推理规则；
- 证明中使用到的推理规则 rules
- 以及整个证明的路径 lines, 这是一个由 Proof.Line 对象组成的序列，而 Proof.Line 本质是公式，但它还需要别的辅助信息，包括推导出这条公式所用的推理规则以及它所依赖的前提（是一个 int 数组，表示之前的 line 的下标）
class Proof:
statement: InferenceRule
rules: FrozenSet[InferenceRule]
lines: Tuple[Proof.Line, ...]
def __init__(self, statement: InferenceRule,
rules: AbstractSet[InferenceRule],
lines: Sequence[Proof.Line]):
self.statement = statement
self.rules = frozenset(rules)
self.lines = tuple(lines)
def __repr__(self) -> str:
r = 'Proof of ' + str(self.statement) + ' via inference rules:\n'
for rule in self.rules:
r += ' ' + str(rule) + '\n'
r += 'Lines:\n'
for i in range(len(self.lines)):
r += ('%3d) ' % i) + str(self.lines[i]) + '\n'
r += "QED\n"
return r
class Line:
formula: Formula
rule: Optional[InferenceRule]
assumptions: Optional[Tuple[int, ...]]
def __init__(self, formula: Formula,
rule: Optional[InferenceRule] = None,
assumptions: Optional[Sequence[int]] = None):
assert (rule is None and assumptions is None) or \
(rule is not None and assumptions is not None)
self.formula = formula
self.rule = rule
if assumptions is not None:
self.assumptions = tuple(assumptions)
def __repr__(self) -> str:
if self.rule is None:
return str(self.formula)
else:
r = str(self.formula) + ' (Inference Rule ' + str(self.rule)
if len(self.assumptions) == 1:
r += ' on line ' + str(self.assumptions[0])
elif len(self.assumptions) > 1:
r += ' on lines ' + ','.join(map(str, self.assumptions))
r += ')'
return r
def is_assumption(self) -> bool:
return self.rule is None
接着定义可证明性：
Given a formula \(\phi\), a set of formulas A, and a set of inference rules R, a proof via R of the inference rule having conclusion \(\phi\) and assumptions A, or simply a proof via R of the conclusion \(\phi\) from the assumptions A, is a list of formulas whose last formula is \(\phi\), such that each of the formulas in the list is either in A or the conclusion of a specialization of a rule in R such that the assumptions of this specialization are preceding formulas in the list.
We say that the inference rule having assumptions A and conclusion \(\phi\) is provable via R, or simply that \(\phi\) is provable from A via R, if there exists a proof of that rule via R. We denote this by \( A\vdash_{R} \phi \)
definition 4.4 (Proof; Provability)
对其中提到符号再做一些解释：
我们可以说通过前提命题集合 A 以及推理规则 R 能够证明出结论 \( \phi \), 也可以说通过推理规则 R 可以证明 A 和 \( \phi \) 组成的推理规则（Proof 类中的 statement）：
x_rule = InferenceRule(A, phi)
- 推理规则 R 是逻辑系统中预设的，它是一堆保真的推理模板，比如可以有不带前提的： InferenceRule({}, "p|~p") ， 其结论就是一个重言式； 或者带前提的 InferenceRule({'p,p->q'}, "q");
- \( A\vdash_{R} \phi \) 也会写成 A |-R phi, 表示的是，可以借助 R 从公式集合 A 中推导出公式 phi, 在实际应用中 A 是具体场景里的公式集合，可以看作带有外部知识的公理，比如"红灯->停车" 以及 "红灯" 。 这时候要证明“停车”就需要实例化推理规则 InferenceRule({'p,p->q'}, "q"); 为 InferenceRule({'红灯,红灯->停车'}, "停车"), 再应用这条规则得到 “停车” 这个结论。或者说我们证明了 InferenceRule({'红灯,红灯->停车'}, "停车") 推理规则是 sound 的。
以上定义是纯粹语法上的（因为没有提到任何 model 或者可满足相关字眼），它完全是字符串规则变换，在没有语义加入的情况下我们可以检查这个证明是否有效（ valid ），即便推理规则是错误的，valid 也是可检查的。比如有推理规则说如果出现 p 就可以生成 q, 那么如果公理中有 p, 就可以通过这个规则得到 q, 这个证明是有效的。
以下实现的函数是给定证明行的编号，从中提取出推理规则实例，比如以上例子里有一行的结论是 q, 它需要依赖 p, 因此这一行的 assumptions 中应该有 p 的编号，那么得到本行结论的推理规则实例就是 InferenceRule([p], q)
def rule_for_line(self, line_number: int) -> Union[InferenceRule, None]:
assert line_number < len(self.lines)
# Task 4.6a
line = self.lines[line_number]
conclusion = line.formula
assumptions = []
if hasattr(line, "assumptions"):
for i in line.assumptions:
assumptions.append(self.lines[i].formula)
return InferenceRule(assumptions, conclusion)
return None
Proof.rule_for_line = rule_for_line
接着根据推理规则检查本次推理是否合法，上一个函数得到的是推理规则的实例，而 line.rule 对象保存的是推理规则模版，因此我们要判断这个实例是否是该模版的实例：
def is_line_valid(self, line_number: int) -> bool:
assert line_number < len(self.lines)
# Task 4.6b
line = self.lines[line_number]
rule = self.rule_for_line(line_number)
if rule is None:
if line.formula in self.statement.assumptions:
return True
return False
if not all(i < line_number for i in line.assumptions):
return False
print(line_number ,rule, rule.is_specialization_of(line.rule))
return line.rule in self.rules and rule.is_specialization_of(line.rule)
Proof.is_line_valid = is_line_valid
最后检查每条 line 是否有效，并且检查最后一条 line 的结论是否和证明的 statment 中的结论一样：
def is_valid(self) -> bool:
# Task 4.6c
if not self.lines:
return False
for i in range(len(self.lines)):
if not self.is_line_valid(i):
#print(f"{i} line {self.lines[i]} is not valid")
return False
return self.lines[-1].formula == self.statement.conclusion
Proof.is_valid = is_valid
T4.7 证明 ‘(p&q)’ 可以推出 ‘(q&p)’
首先这个结果看上去很"显然", 这种显然实际来自于语义层面，因为我们定义过 p&q 的真值表，容易发现 q&p 真值表和它一样。
实际上可以直接根据语义构造出一个推理规则：前提是 (p&q), 结论是 (q&p), 可靠的基础推理规则都是通过语义构造的，但本小节的目的是用 demo 例子去熟悉 Proof 类，于是作者选择的推理规则是
- [x,y] 能推出 (x&y)
- (x&y) 能推出 y
- (x&y) 能推出 x
#: Conjunction introduction inference rule
A_RULE = InferenceRule([Formula.parse('x'), Formula.parse('y')],
Formula.parse('(x&y)'))
#: Conjunction elimination (right) inference rule
AE1_RULE = InferenceRule([Formula.parse('(x&y)')],Formula.parse('y'))
#: Conjunction elimination (left) inference rule
AE2_RULE = InferenceRule([Formula.parse('(x&y)')],Formula.parse('x'))
然后从纯符号变换，即语法角度去证明给定前提 (p&q) 的情况下能得到 (q&p) ，这需要的识别符号上相似性的注意力，因此并非显然。
def prove_and_commutativity() -> Proof:
# Task 4.7
assumptions = (Formula.parse('(p&q)'), )
conclusion = Formula.parse('(q&p)')
statement = InferenceRule(assumptions, conclusion)
rules = [A_RULE, AE1_RULE, AE2_RULE]
line0 = Proof.Line(assumptions[0], None, None)
line1 = Proof.Line(Formula.parse("q"), AE1_RULE, [0])
line2 = Proof.Line(Formula.parse("p"), AE2_RULE, [0])
line3 = Proof.Line(Formula.parse("(q&p)"), A_RULE, [1, 2])
lines = [line0, line1, line2, line3]
return Proof(statement, rules, lines)
可以验证其是否有效
print(prove_and_commutativity())
Proof of ['(p&q)'] ==> '(q&p)' via inference rules: ['(x&y)'] ==> 'x' ['x', 'y'] ==> '(x&y)' ['(x&y)'] ==> 'y' Lines: 0) (p&q) 1) q (Inference Rule ['(x&y)'] ==> 'y' on line 0) 2) p (Inference Rule ['(x&y)'] ==> 'x' on line 0) 3) (q&p) (Inference Rule ['x', 'y'] ==> '(x&y)' on lines 1,2) QED
prove_and_commutativity().is_valid()
self, general: ['(p&q)'] ==> 'q' ['(x&y)'] ==> 'y' 1 ['(p&q)'] ==> 'q' True self, general: ['(p&q)'] ==> 'q' ['(x&y)'] ==> 'y' self, general: ['(p&q)'] ==> 'p' ['(x&y)'] ==> 'x' 2 ['(p&q)'] ==> 'p' True self, general: ['(p&q)'] ==> 'p' ['(x&y)'] ==> 'x' self, general: ['q', 'p'] ==> '(q&p)' ['x', 'y'] ==> '(x&y)' 3 ['q', 'p'] ==> '(q&p)' True self, general: ['q', 'p'] ==> '(q&p)' ['x', 'y'] ==> '(x&y)' True
T4.8 证明无条件下就可以推出 p->p
本节继续证明一个（语义上）看上去非常"显然"的定理，不过本题给出的推理规则在形式上与 p->p 结论的接近程度没有上一题那么明显，人在思考的时候需要一点试探和回溯。
使用到了以下三个推理规则：
#: Modus ponens / implication elimination
MP = InferenceRule([Formula.parse('p'), Formula.parse('(p->q)')],
Formula.parse('q'))
#: 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)))'))
这些规则以及要证明的 I0 规则都只用到了 ->
def prove_I0() -> Proof:
assumptions = ()
conclusion = Formula.parse('(p->p)')
statement = InferenceRule(assumptions, conclusion)
rules = [MP, I1, D]
sub0 = Formula.parse('((p->((p->p)->p))->((p->(p->p))->(p->p)))')
line0 = Proof.Line(sub0, D, [])
line1 = Proof.Line(Formula.parse('(p->((p->p)->p))'), I1, [])
line2 = Proof.Line(Formula.parse("((p->(p->p))->(p->p))"), MP, [1, 0])
line3 = Proof.Line(Formula.parse("(p->(p->p))"), I1, [])
line4 = Proof.Line(Formula.parse("(p->p)"), MP, [3, 2])
lines = [line0, line1, line2, line3, line4]
return Proof(statement, rules, lines)
prove_I0().is_valid()
self, general: [] ==> '((p->((p->p)->p))->((p->(p->p))->(p->p)))' [] ==> '((p->(q->r))->((p->q)->(p->r)))' 0 [] ==> '((p->((p->p)->p))->((p->(p->p))->(p->p)))' True self, general: [] ==> '((p->((p->p)->p))->((p->(p->p))->(p->p)))' [] ==> '((p->(q->r))->((p->q)->(p->r)))' self, general: [] ==> '(p->((p->p)->p))' [] ==> '(q->(p->q))' 1 [] ==> '(p->((p->p)->p))' True self, general: [] ==> '(p->((p->p)->p))' [] ==> '(q->(p->q))' self, general: ['(p->((p->p)->p))', '((p->((p->p)->p))->((p->(p->p))->(p->p)))'] ==> '((p->(p->p))->(p->p))' ['p', '(p->q)'] ==> 'q' 2 ['(p->((p->p)->p))', '((p->((p->p)->p))->((p->(p->p))->(p->p)))'] ==> '((p->(p->p))->(p->p))' True self, general: ['(p->((p->p)->p))', '((p->((p->p)->p))->((p->(p->p))->(p->p)))'] ==> '((p->(p->p))->(p->p))' ['p', '(p->q)'] ==> 'q' self, general: [] ==> '(p->(p->p))' [] ==> '(q->(p->q))' 3 [] ==> '(p->(p->p))' True self, general: [] ==> '(p->(p->p))' [] ==> '(q->(p->q))' self, general: ['(p->(p->p))', '((p->(p->p))->(p->p))'] ==> '(p->p)' ['p', '(p->q)'] ==> 'q' 4 ['(p->(p->p))', '((p->(p->p))->(p->p))'] ==> '(p->p)' True self, general: ['(p->(p->p))', '((p->(p->p))->(p->p))'] ==> '(p->p)' ['p', '(p->q)'] ==> 'q'
True
可以看到，本题通过语法上的证明比用语义上用真值表复杂多了，但对于变量很多的公式，用语义真值表直接去判断几乎是不可行的，就只能用证明方法了。
T4.9 替换规则在单步执行中的 soundness
前文知道，证明过程是这样的：给定前提集合 A 和结论 phi, 去推理规则 R 里寻找一个模板，其前提应该在结构上和 A 中的某个命题同构，而其结论和 phi 同构，这样只需要对推理规则按照 A 和 phi 的内容实例化，向前一步推理就证明成功了。
但实际中不太可能这么简单，结论 phi 不会直接和推理规则里模板的结论同构，于是要依靠某种识别符号之间距离的注意力或直觉去启发搜索，不断实例化 R 中的某些模板得到中间结论（称为引理，定理等），一步一步接近 phi 。
那么这个过程中，很重要的就是确保“实例化”是可靠的，这样只要规则是可靠的（sound），经过替换规则实例化之后的具体规则也是可靠的，从而单步证明是可靠的。
soundness 是语义层面的，因此证明也要是语义层面的，以下用的是逆否命题来说明，给定一个会令实例化后的具体推理规则失效的模型，那么将模型中的变量替换成推理模板中的变量，就得到一个让该推理规则模板失效的模型，所以只要推理模板是可靠的，实例化的推理规则肯定也是可靠的。
def rule_nonsoundness_from_specialization_nonsoundness(
general: InferenceRule, specialization: InferenceRule, model: Model) \
-> Model:
assert specialization.is_specialization_of(general)
assert not evaluate_inference(specialization, model)
# Task 4.9
smap = general.specialization_map(specialization)
gmodel = {}
for var, formula in smap.items():
gmodel[var] = evaluate(formula, model)
return gmodel
Every specialization of a sound inference rule is itself sound as well.
lemma 4.1 (Specialization Soundness)
这里看到，替换规则是更”元“层面的操作，推理规则可以让公式（命题）生成更多命题，替换规则可以让推理规则生成更多推理规则。
T4.10 命题逻辑的 soundness
上节证明了实例化（替换）操作的可靠性，这相当于解决了证明过程中垂直方向（宏替换）的可靠性，本节把证明的水平方向（函数执行）的可靠性也补充上：
def nonsound_rule_of_nonsound_proof(proof: Proof, model: Model) -> \
Tuple[InferenceRule, Model]:
assert proof.is_valid()
assert not evaluate_inference(proof.statement, model)
# Task 4.10
for i in range(len(proof.lines)):
specialization = proof.rule_for_line(i)
if specialization:
if not evaluate_inference(specialization, model):
general = proof.lines[i].rule
gmodel = rule_nonsoundness_from_specialization_nonsoundness(general, specialization, model)
return (general, gmodel)
return None
以上函数中，参数 proof 是 valid 的，但结论相对 model 来说是错的，那么必然某个（些）推理规则是不可靠的
相当于用反证法证明以下定理：
Any inference rule that is provable via (only) sound inference rules is itself sound as well. That is, if R contains only sound inference rules, and if A |-R φ, then A |= φ.
theorem 4.1 (The Soundness Theorem for Propositional Logic)
不用反证法要证明 soundness 的话，要用类似递归（递推，数学归纳法）的方式，给定一个使得 assumption 为 true 的 model, 对于证明的一行，由于当前行使用的 inference rule 是 soundness, 因此本行的结论就是 True。
对比 valid(有效性) 和 sound(可靠性) 两个概念：
- valid 是纯语法上的，它检查的是证明中每一步是否符合语法，即是否符合推理规则（可以是不可靠的规则）中的生成机制。如果证明中每个步骤都是 valid 的，那么整个证明对象 Proof 也是 valid 的。
- sound 是纯语义上的，它检查的是推理规则中前提和结论与模型可满足性的关系。
- 如果证明中每一步使用的都是 sound 的推理规则，并且证明步骤是 valid 的，那么整个证明也是 sound 的。这是 soundness 定理，可以看到该定理实际有内在的 valid 要求。
- 由于逻辑系统包括语法和语义的定义，以及一组初始的推理规则（公理）， 因此如果公理都是 sound 的，那么整个逻辑系统也是 sound 的。
- 所以说，valid 可以修饰证明或者证明步骤，是纯语法的；sound 可以修饰推理规则、证明以及整个逻辑系统。 sound 修饰推理规则时，只涉及到语义描述，但修饰证明以及逻辑系统时，需要 valid 性质作为条件支持。
公式、公理和推理规则的异同
虽然大部分逻辑书或者数学书一般会把公理、定理看作是自明或被证明为真的公式，本书中，公理，定理，引理都属于推理规则 (InferenceRule 对象)，而不属于公式 (Formula)。
比如说 "(p->p)" 是一个 Formula，但如果要把它作为公理，那么应该包装成 InferenceRule 对象，这在书本里称为 I0 公理
I0 = InferenceRule([], Formula.parse('(p->p)'))
变成推理规则后，它不再是原来的"静态"的公式，而是一种接近函数的动态对象。 在本文里，我有时候会用 "无条件地生成 p->p" 来描述这个推理规则。
推理规则还可以用符号替换（类比编程中宏替换）来转换成其他推理规则，比如以上 I0 还可以变成：
InferenceRule([], Formula.parse('(r->r)'))
这样，相当于我们又得到了一个新的公式生成机制，即 ”无条件地生成 r->r”，也就是说，要使用推理规则，先要以模版（宏或类）的视角去实例化它，然后以函数的视角去调用它，调用的参数需要从 assumption 或已经证明的中间公式中选择。
另外，通过生成规则得到的结果虽然是一个公式（字符串），但它只有和前提组合在一起才有完整语义，即真理或者定理是推理规则对象（InferenceRule）而不是 Formula，因为任何有意义的推理结果都是有前提假设的，公理也是 InferenceRule, 它们一般是没有前提的推理规则。
比如说，公式 r 作为假设, 同时有公理 I1, "可以从 q 产生 (p->q) ", 该规则实例化后，结合假设公式 r 我们能够得到公式 (p->r), 但 (p->r) 是没有真假的，只有 "可以从 r 产生 (p->r)" 这条新的推理规则才是 sound 的，这才能称为定理：
assumption1 = Formula("r")
I1 = InferenceRule([], Formula.parse('(q->(p->q))'))
theorem1 = InferenceRule([assumption1], Formula.parse('(p->r)'))