计算机科学逻辑/逻辑

子 FO 逻辑

模态逻辑

模态逻辑通过对模态“可能性”和“必要性”的操作符扩展了命题逻辑。这些基本的模态操作符通常用 $\Box$ (或L) 表示必然，用 $\Diamond$ (或M) 表示可能。每个都可以通过以下方式从另一个定义

$\Diamond P\leftrightarrow \lnot \,\Box \,\lnot \,P.$

合取逻辑

合取逻辑是 FO 的一个片段，它被限制为由合取连接的原子 FO 表达式，这些表达式可以被存在量词所引导。它在数据库理论中尤为重要。

定义 CON

1. 原子
2. $\varphi \land \psi$
3. $\exists _{x}\varphi$

备注

1. 换句话说：CON 公式是由原子公式构建的（关系）FO 公式，它只使用合取和存在量化。
2. FO 的语义相应地适用于此。
3. 自由变量和绑定变量的“通常”概念也适用于此。
4. 形式为 $\exists _{x_{1}}...\exists _{x_{n}}\varphi _{1}\land ...\land \varphi _{m}$ 的公式，其中每个 φ 都是无量词的，被称为范式
5. 每个 CON 公式都等价于一个范式公式
6. 所有 CON 公式都是可满足的

例子

1. $\exists _{x}(\varphi (x,y)\land \psi (x,y))$ 有一个绑定变量 x 和一个自由变量 y。
2. $\exists _{x}(\varphi (x))\land \exists _{y}(\psi (y))$ 等价于 $\exists _{x}\exists _{y}(\varphi (x)\land \psi (y))$。后者被称为标准形式。

等式

此外，可以通过以下方式引入变量或常量之间的等式

• $x\equiv y$

例如，不总是可满足的。每个可满足的 CON 公式都等价于一个没有等式的公式。

高阶逻辑

不动点逻辑

不动点逻辑通过一个不动点算子来增强 FO 的语法，该算子是一种允许表达式递归的机制，从而提高了表达能力。这个想法与在命令式编程语言中添加 while 循环结构非常相似。

示例 闭包

闭包的说明

考虑图 G 的闭包。对于距离为一，我们有

$G(x,y)\,$

对于距离最大为二

$G(x,y)\lor \exists _{z}(G(x,z)\land G(z,y))$

因此，我们可以通过扩展此析取来进一步固定距离（仅此而已）。为了表达任意距离的闭包（对于大多数情况至关重要），可以使用以下方法引入递归

$\varphi (T)=G(x,y)\lor T(x,y)\lor \exists _{z}(T(x,z)\land G(z,y))$

其中 T 是直到某个 i 的闭包。因此 φ(T) 给出了直到 i + 1 的闭包。因此，可以定义一个序列

$J_{0}=\emptyset ;J_{i}=\varphi (J_{i-1}),i>0$

很明显，这给出了某个 k 的闭包，即序列收敛（即 J_k = J_k+j，对于所有 j > 0），并且它的极限是闭包。

在插图中，我们有一个初始图 G，如 (a) 所示，因此

(a) 为 $J_{1}=G(x,y)\,$

(b) 为 $J_{2}=G(x,y)\lor \exists _{z}(G(x,z)\land G(z,y)$

不动点 (c) 为

$J_{3}=G(x,y)\lor \exists _{z}(G(x,z)\land G(z,y))\lor \exists _{z}(\exists _{t}(G(x,t)\land G(t,z))\land G(z,y))$

因此 J₃ = J₄ = ... 。

♣

正如我们在本例中所看到的，递归可以用来表达任意长度的公式。但由于我们在这里始终处理的是有限的公式，因此必须为递归提供一些终止符。这个角色可以由不动点来扮演。在上面的例子中，这样的不动点存在。但并非总是如此，正如我们接下来看到的。

示例

待办事项 跳线

♣

正如我们在本例中所看到的，递归的不动点并不总是存在。因此，我们必须小心定义基于递归的逻辑。我们将 FO 扩展为 PFP，以处理存在不动点的情况。

部分不动点逻辑 (PFP)

待办事项

♣

上述假设不动点存在并不真正令人满意，因此现在可以考虑对递归进行限制，以确保在所有情况下都存在不动点。因此，引入了三个概念：递归的单调性、正性和膨胀性。

膨胀性不动点逻辑 (IFP)

概念

待办事项 生命游戏

定义

待办事项

最小不动点逻辑 (LFP)

概念

待办事项

定义

待办事项

♣

IFP 和 LFP 的比较

待办事项

♣