跳至内容
Topos Uranos

摘要

到目前为止,公式一直是由圆圈和圆盘组成的符号串,推演一直是对符号串的操作:关于它们的真假,什么也没有说过。本课赋予它们意义。一个赋值给每个变元指派两个真值之一,11(真)或 00(假),并以唯一的方式,通过对复杂度的递归,扩张到所有公式,而且只用一个条款:(φ↓ψ)(\varphi \downarrow \psi) 取值 11,恰好当 φ\varphi 和 ψ\psi 都取值 00 时。由这个条款和正式缩写,无须另作任何规定,就可以算出否定、析取、合取、蕴涵、双条件和不相容析取的值。一致引理用对复杂度的归纳证明,它保证一个公式的值只依赖于其变元的值;由此可知,真值表(共 2n2^n 行,对应 nn 个变元)包含了无穷多个赋值对这个公式所能说出的一切。由此定义满足、有效性、可满足性、矛盾式与偶然性,固定公式 ⊤\top 和 ⊥\bot,并提出判定有效性的问题,真值表解决这个问题的代价随变元个数呈指数增长。

学习目标

  1. 借助赋值的递归扩张计算一个公式在该赋值下的真值,并由正式缩写求出每个派生联结词的值。
  2. 用对复杂度的归纳证明一致引理,并借助它说明为什么一张 2n2^n 行的真值表足以研究一个含 nn 个变元的公式。
  3. 逐列构造真值表,把公式分类为有效式、偶然式或矛盾式,把公式集分类为可满足的或不可满足的,而不把 ⊭φ\not\models \varphi 与矛盾式混为一谈。
  4. 通过寻找否证一个公式的赋值来判定它是否有效,并估计真值表方法的代价如何随变元个数变化。

公式的意义

关于语言的单元在关于命题逻辑的语言的一课中构造了一个由两个符号组成的符号串的集合,关于演绎的单元则教会了如何用公理和规则从一些符号串得到另一些符号串。两者都没有谈到真:演绎系统按照形式变换符号,就像一台不懂自己在写什么的机器。然而,构造这种语言是为了表示陈述句,而关于自然语言的形式化的一课赋予了它们非形式的读法:(φ↓ψ)(\varphi \downarrow \psi) 在 φ\varphi 和 ψ\psi 都为假时为真,其余联结词的读法都由此得出。语义学把这些读法变成数学定义。

有两个决定为它奠基。第一个是二值原则:恰好有两个真值,记作 11(真)和 00(假),每个公式在每种情形下都取其中之一。第二个是真值函项性:复合公式的值只依赖于其成分的值,而不依赖于它的内容,因此变元的真假决定所有公式的真假。关于形式化的一课展示了这第二个决定的代价(因果、模态和时间都被排除在外);它的回报是:整个语言的语义由唯一一个条款得出,即初始联结词的条款。

此外还应指出,本单元完全在元语言中工作。“φ\varphi 在某某赋值下为真”或“φ\varphi 是重言式”这样的断言不是公式,而是关于公式的数学陈述,它们用通常的推理来证明,往往用对复杂度的归纳;它们不是本课程的系统中的推演。两个世界之间的关系,即一切可推演的都为真,而一切在本单元的精确意义下为真的都可推演,是元理论单元的主题。