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

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

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

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

2 相继式(Sequent)

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

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

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

3 推理规则(Inference Rule)

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

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

4 正向/反向推理

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

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

5 反向推理算法

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

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

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

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

6 基本推理规则

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

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

6.1 hypothesis规则

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

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

6.2 monotonicity规则

$$\frac{H⊢Q}{H,P⊢Q}$$

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

6.3 cut规则

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

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

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

7.1 命题逻辑语言

$$\begin{array}{rl}Predicate:=& \perp \\ & \top \\ & \neg Predicate\\ & Predicate\wedge Predicate\\ & Predicate\vee Predicate\\ & Predicate\Rightarrow Predicate\\ & Predicate\iff Predicate\end{array}$$

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

7.2 推理规则

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

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

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

8.1 谓词逻辑语言

$$\begin{array}{rl}Predicate:=& \perp \\ & \top \\ & \neg Predicate\\ & Predicate\wedge Predicate\\ & Predicate\vee Predicate\\ & Predicate\Rightarrow Predicate\\ & Predicate\iff Predicate\\ & Var\_List\cdot Predicate\\ & \\ Expression:=& Variable\\ & Expression\mapsto Expression\\ & \\ Variable:=& Identifier\\ & \\ Var\_List:=& Variable\\ & Variable,Var\_List\end{array}$$

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

8.2 全称量词的推理规则

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

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

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

8.3 存在量词的推理规则

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

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

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