【Event-B学习笔记】1：相继式(Sequent)和推理规则(Inference Rule)

1 关于"谓词"和"命题"的理解

刚接触的时候对Event-B资料里大篇幅使用"谓词"这个词（而不是"命题"）感到非常疑惑，在我以往的印象里，类似"大于"，“小于”，"是一只猫"这种表述关系的是叫谓词，其中前两个是二元谓词，最后一个是一个一元谓词。

现在理解下来，Event-B里的谓词确实就应该叫"谓词"，而不是"命题"。试想$2>3$2>3是一个命题（假命题），这没什么问题，但是$n>3$n>3是命题吗？这是我一直以来的理解错误，而且是个很基本的错误。$n>3$n>3这样的东西不是命题，因为命题一定是可以判断真假的陈述句。那么如何归类它呢，其实$n>3$n>3就只是一个一元谓词（也不应该叫"命题公式"），这和$m \in Cat$m∈Cat是谓词而不是命题是一样的道理。

因为Event-B里面大量使用了表示变量的值之间的关系的数学式，称它们为谓词无可厚非，有几个变量就是几元谓词了。也不应该认为这是"广义的谓词定义"，其实这就是谓词的定义，没什么广义狭义之分。

2 相继式(Sequent)

相继式用来表示证明的目标，具有如下结构：
$H \vdash G$H⊢G

• $H$H是一个有穷的谓词集合，称为假设(hypothes)，可以为空集。
• $G$G是一个谓词，称为目标(goal)。
• 符号$\vdash$⊢表示推导出(entail)。注意这个符号不能理解成蕴含，相继式不是谓词，如果$\vdash$⊢换成$\Rightarrow$⇒那就成了谓词了。

这里还要特别区分一下$\vdash$⊢（推导出、满足）和$\Rightarrow$⇒（蕴含）的语义。$a \Rightarrow b$a⇒b是一个谓词（如果$a$a和$b$b都有具体的意义那就是一个命题公式），这是可真可假的。但是$a \vdash b$a⊢b没有真假的概念，就是表述这样一件事。

3 推理规则(Inference Rule)

推理规则是基于相继式的，是上下两部分的推理结构：
$\frac{A}{C}$CA​

其中$A$A是一个相继式的集合，可以为空集，表示推理的前件(antecedents)。$C$C是一条相继式，表示推论(consequnet)。推理规则$\frac{A}{C}$CA​表示如果$A$A中的所有相继式都能得到证明，则可以得到相继式$C$C的证明。

4 正向/反向推理

正向推理：证明$A$A中的每一条，将附属得到$C$C的证明。
反向推理：如果要证明$C$C，一个充分（但不必要）的办法就是证明$A$A中的每一条。

这只是在说期望通过推理得到结果的两种不同的"认知过程"，Event-B里更多使用反向推理。

5 反向推理算法

如要证明相继式$S$S，初始知识是一个推理规则的集合$\mathcal{T}$T，接下来需要一个相继式容器$K$K，初始$K=\{S\}$K={S}。

当$K$K不为空，从$\mathcal{T}$T中寻找$\frac{A}{C}$CA​使得$C \in K$C∈K，然后将$K$K中的$C$C删掉，再把$A$A中所有相继式加到$K$K中。

如果在某次循环找不到$C \in K$C∈K的$\frac{A}{C} \in \mathcal{T}$CA​∈T了，说明是证不出来的。如果最终$K$K为空集了，那么就说明可以证明出来。这是因为反向推理的出口就是那些$\frac{}{C}$C​的推理规则（前件是空集，不写出），即已知成立的相继式$C$C，待证明的相继式经过有限步替换成了若干个空，证明就完成了。

这个过程可以表达成一棵证明树，树的叶子是已知成立的相继式（就是无前件的推理规则的后件），树根是待证明的相继式，而结点的父子关系根据匹配推理规则建立。

6 基本推理规则

基本推理规则不受"语言"的限制，例如里面没有一阶逻辑的与或非蕴含之类的符号，也没有其它"语言"里的符号。不管用什么语言、什么逻辑系统，这些推理规则都是成立的。

下面描述推理规则时候，对里面涉及的相继式的描述，$\vdash$⊢总是最后结合的，因为它是连接左侧的谓词集合和右侧的谓词的，如$H,P \vdash P$H,P⊢P其实就是$\{H,P\} \vdash P${H,P}⊢P。

6.1 hypothesis规则

$\frac{}{H,P \vdash P}$H,P⊢P​

前提里包含结论，相继式直接就是可证明的。

6.2 monotonicity规则

$\frac{H \vdash Q}{H,P \vdash Q}$H,P⊢QH⊢Q​

这是单调性，在可证相继式里增加前提，得到的相继式还是可证的。

6.3 cut规则

$\frac{H \vdash P \ \ \ \ \ \ H,P \vdash Q}{H \vdash Q}$H⊢QH⊢P      H,P⊢Q​
谓词集合（上面的$\{H,P\}${H,P}）可以通过使用可证相继式（上面的$H \vdash P$H⊢P）进行约减（约减成了$\{P\}${P}）。

这里的$P$P反映了数学中的引理(lemma)，要从$H$H证明$Q$Q，数学资料里常常先给出一个引理$P$P，然后借用引理可以把$Q$Q证出来，最后再证明$H$H可以推导出这个引理$P$P，就完成了证明过程。

7 适用于命题逻辑语言下的推理规则

7.1 命题逻辑语言

$\begin{aligned} Predicate := & \bot \\ & \top \\ & \neg Predicate \\ & Predicate \wedge Predicate \\ & Predicate \vee Predicate \\ & Predicate \Rightarrow Predicate \\ & Predicate \Leftrightarrow Predicate \end{aligned}$Predicate:=​⊥⊤¬PredicatePredicate∧PredicatePredicate∨PredicatePredicate⇒PredicatePredicate⇔Predicate​

为避免二义性，结合时先$\neg$¬再$\wedge$∧、$\vee$∨最后$\Rightarrow$⇒、$\Leftrightarrow$⇔。并且$\wedge$∧和$\vee$∨是左结合的，而$\Rightarrow$⇒和$\Leftrightarrow$⇔是不结合的（连续使用必须加括号）。

7.2 推理规则

注意这些推理规则的命名上有后缀_L和_R，可以称为左规则和右规则（未必都只有一条，只是命题逻辑这里恰好左一条右一条）。左规则总是变换相继式的假设部分（$\vdash$⊢左侧），右规则总是变换相继式的目标（$\vdash$⊢右侧）。

从之前的3条基本推理规则，和这10条适用于命题逻辑的规则，还能得到一些推导出的常用规则，为了证明方面也被内置到系统里，这里不说明。

8 适用于谓词逻辑语言下的推理规则

8.1 谓词逻辑语言

$\begin{aligned} Predicate := & \bot \\ & \top \\ & \neg Predicate \\ & Predicate \wedge Predicate \\ & Predicate \vee Predicate \\ & Predicate \Rightarrow Predicate \\ & Predicate \Leftrightarrow Predicate \\ & Var\_List \cdot Predicate \\ \\ Expression := & Variable \\ & Expression \mapsto Expression \\ \\ Variable := & Identifier \\ \\ Var\_List := & Variable \\ & Variable, Var\_List \end{aligned}$Predicate:=Expression:=Variable:=Var_List:=​⊥⊤¬PredicatePredicate∧PredicatePredicate∨PredicatePredicate⇒PredicatePredicate⇔PredicateVar_List⋅PredicateVariableExpression↦ExpressionIdentifierVariableVariable,Var_List​

注意这里$Expression \mapsto Expression$Expression↦Expression是一个表达式对偶，它是两集合笛卡尔积中的元素，如$x \in X$x∈X和$y \in Y$y∈Y，有$x \mapsto y \in X \times Y$x↦y∈X×Y。表达式对偶构成了映射集合中的元素，它也是表达式的一种。

8.2 全称量词的推理规则

注意单个变量$x$x也是表达式的一种。下面这条ALL_L是说如果前提里有对任意$x$x的$P$P了，那么单独的$P(E)$P(E)就可以约去了，因为已经包含在对任意$x$x的$P$P里。

从反向推理的角度解读，就是当相继式的假设部分中有全称量词$\forall x \cdot P(x)$∀x⋅P(x)时，可以增加一个用$E$E代替任意的$x$x而得到的$P(E)$P(E)到相继式的假设部分中去。

下面这条ALL_R中$x$x在相继式假设集合$H$H中不能自由出现（副条件），所以可以给它加上全称量词约束。

8.3 存在量词的推理规则

下面这条XST_L中，$x$x在集合$H$H中不是自由出现的（副条件），这样在相继式前提部分的$P(x)$P(x)就可以自己加个存在量词约束。

下面这条XST_R是说既然相继式的结论能找到一个$P(E)$P(E)，那么就说明存在一个表达式$x$x使$P(x)$P(x)能代替$P(E)$P(E)作为结论，显然至少只要让$x=E$x=E就行了。

从反向推理的角度解读，就是当相继式的结论部分中有存在量词$\exist x \cdot P(x)$∃x⋅P(x)时，就需要能找到一个表达式$E$E代替存在的的$x$x而得到的$P(E)$P(E)来换掉相继式的结论部分。