TLA+ 主页

本章介绍一些 TLA+ 基础逻辑知识。

1.1 命题逻辑

在命题逻辑中,TLA+ 使用合取、析取、否定、蕴含、相等五个运算符。

人们一般觉得蕴含难以理解。蕴含 → 的定义为:F → G 为真当且仅当 F 假或者 G 真。一个直观的解释是:

考虑 n>3 → n>1,该命题从语义判断自然是真的。我们考虑 n 不同取值时 F(此时为n>3)与 G(此时为n>1)的真假,对于 n = 0, 2, 4 的时候,可以验证这三种情况的真值表等价于 F 假或者 G 真。

在本书中,数学运算符的优先级高于这五者。这五者中,否定的优先级最高,然后是合取、析取,然后是蕴含、相等。合取、析取满足交换律、结合律。

重言式即恒为真的命题。F ≡ G 是重言式表示 F 等价于 G。

1.2 集合

集合包含有限或无限个元素,并由其包含的元素唯一确定。集合有交集、并集、差集、子集等运算符。

1.3 谓词逻辑

TLA+ 的谓词逻辑又引入了全称量词和存在量词,用于表达命题与集合中至少一个、全部元素的关系。

我们单独处理空集的语义,∃ x∈S: F 定义为至少一个 S 中的元素使得 F 为真。考虑到空集不包含元素,S 为空集时无论 F 是什么,∃ x∈S: F 恒为假。由量词的否定可以得到,无论 F 是什么(例如是 ¬F),∀ x∈∅: F 恒为真。

∃ x: F 是包含未绑定的 x 的公式,上文 ∃ x∈S: F 是绑定的 x 的公式。未绑定与绑定可以通过在 F 中加入 x∈S 的子公式进行转化。

全称量词是对合取的泛化,因为全称量词将公式 F 应用在每个元素上,每个 F(x) 都要为真,谓词公式才为真,这就是合取的含义。同样存在量词是对析取的泛化。

全称量词对合取有分配律,存在量词对析取有分配律。

1.4 公式与语言

公式只是可真可假的一段话,并不是在表达作者“认为其为真”。而在生活中,叙述一个公式常常意味着认为它为真。如何区分本书中的一个“公式”(例如“2*x > x”)是公式,还是“认为其为真”的陈述呢?可以通过把“公式”替换成一个常见名词判断。因为“认为公式为真”的陈述有动词,这样替换之后会缺少动词而产生语法错误。