最近的Research牵涉到一些时态逻辑的东西，但推式子的时候反而发现一些很简单的一阶逻辑结论之前都没注意到，感觉自己白学了。
首先是这个
(\exists x. P(x)) \to Q \iff \forall x.P(x) \to Q
很奇怪，为什么“任意”放进括号里就变成“存在”了呢？其实这也很好解释，比如右式可以解释为“如果书架上存在一本历史书，今天就举办历史读书会”，左式可以解释为“对于书架上的任意一本书，如果它是历史书，今天就举办历史读书会”，这二者显然说的是同一件事，但隐含的条件是“举办历史读书会”这件事并不描述特定的某本书的性质，也就是要求x不在Q中自由出现。
这个现实生活中的解释是chatgpt给的，但有趣的是，如果你问它上面两个式子等不等价，它会硬说不等价；但如果你强行告诉它二者等价，它能给你很多生动形象的解释。
当然，证明也很简单，把蕴含化成析取的形式就行了：
\begin{aligned}
(\exists x. P(x)) \to Q &\iff \neg(\exists x. P(x)) \lor Q \\
&\iff (\forall x. \neg P(x)) \lor Q \\
&\iff \forall x. \neg P(x) \lor Q \\
&\iff \forall x. P(x) \to Q
\end{aligned}
另一个结论是这样的，我们用\llbracket P \rrbracket来表示满足谓词P的所有个体的集合，那么会有
\begin{gathered}
\forall x \in \llbracket P \rrbracket, Q(x) &\iff \forall x. P(x) \to Q(x) \\
\exists x \in \llbracket P \rrbracket, Q(x) &\iff \exists x. P(x) \land Q(x) \\
\end{gathered}
你会惊奇的发现，全称量词版本的化出来是蕴含，而存在量词化出来是合取。这也很好解释，比如第一行说的是，“对任意一本中国历史书，它一定是历史书”和“对任意一本书，如果它是中国历史书，它一定是历史书”这两句话意思是一样的。第二行说的是，“存在一本历史书，它也是地理书”和“存在一本书，它既是历史类也是地理类”这两句话意思是一样的。如果我们从集合的角度看P和Q，那么一种说的是二者的包含关系，另一种说的是二者有非空交集。
想到这些是因为，近期Research的一个前置工作解决了这样一个问题：给定一个程序，找到一个描述该程序的行为的规约。换言之，就是找到这个程序满足的某些性质，比如程序\mathsf{reverse}将列表l_0反转为l_1，那l_0和l_1长度相等就是一个合法的性质。事实上这相当于为程序找一个上近似：虽然反转前后的两个列表一定长度相同，但长度相同的两个列表并不一定互为反转。
那我们不难想到其对偶的下近似问题，
- 对于任意程序的输出，它都满足某性质（上近似）
- 对于任意满足性质的值，它都可以作为程序的输出（下近似）
这里就和Hoare Logic与Incorrectness Logic的关系很像。更进一步，如果程序是非确定性的，我们又可以对上下近似分别考虑“任意”和“存在”的两个版本，某种意义上对应着Computational Tree Logic里的”Inevitably”和”Possibly”，
- 存在一个程序的输出，它满足某性质
- 存在满足性质的一个值，它可以作为程序的输出
乍一看似乎有四个可以做的问题，真正做到了举一反三（x），但其实后两个问题说的是同一件事，因为存在量词化出来是合取。简单来说这里只讨论了两个集合的三种关系，A包含B，B包含A，A和B有非空交集。
看来逻辑还是得好好学学，只可惜pku哲学系逻辑学双学位开的太晚了（x）。
发表回复