命题逻辑和一阶逻辑

2019-07-04 本文已影响0人闰秋

命题逻辑的语义

$\phi_1, \phi_2, ... \phi_n \vdash \psi$ 称为一个推理(sequent)，如果使用Natural Deduction的方式进行推导(derivation)，可以由 $\phi_1, \phi_2, ... \phi_n$ 得到 $\psi$ ，那么这个推理是有效的。
定义：

真值集合为 $\{T,F\}$ ，T为真，F为假
一个公式的估值(valuation)或模型(model)是指为公式中的每一个原子赋一个真值集合中的值
对于 $p \land q$ 这一公式而言， $\land$ 仅考虑p和q的真假值，并不考虑p和q代表什么。

soundness和completeness

对于合理的推理 $\vdash$ ，能否在真值表的语义下，保证当 $\phi_i$ 为T时， $\psi$ 不可能是F。

若 $\phi_1, \phi_2,...\phi_n \vdash \psi$ 中，当全 $\phi_1,\phi2,...\phi_i$ 部成立时， $\psi$ 也成立，则称 $\phi_1,\phi_2,...\phi_i$ 语义蕴含 $\psi$ 。

soundness：若 $i \vdash \psi$ 是合理的，则$$

completeness：若 $\phi_1, \phi_2, ... \phi_n \models \psi$ ，则是 $\phi_1, \phi_2,...\phi_n \vdash \psi$ 合理的

证明：太长不看

实际是想说：一个逻辑系统需要满足soundness和completeness的一致性。

一阶逻辑

signature：三个部分 $\mathcal{F},\mathcal{C}, \mathcal{P}$

分别是函数名、常数名、谓词名

一般省略 $\mathcal{C}$ ，因为其可看作无参数的 $\mathcal{F}$

一阶逻辑的公式中，两类：

项： $t::=\mathcal{F}/0 \mid \mathcal{C} \mid \mathcal{F(t_1,t_2,…t_n)}$ ，用于表达对象object
公式：
$\phi::=\mathcal{P}(t_1,t_2,…,t_n) \mid \lnot \phi \mid (\phi \land \phi) \mid (\phi \lor \phi) \mid (\phi \rightarrow \phi) \mid \forall x(\phi) \mid \exists x(\phi)$

一阶逻辑的语义：

proof-based logic：给出一个operative的，通过Natural Deduction方式的 $\vdash$ 证明

优点：一旦找到一个证明方式成功推导，即可证明 $\Gamma \models \psi$

缺点：难以证明 $\Gamma \not \models \psi$ ，需要遍历全部可能的证明方式，才能够得到结论

semantic-based logic：通过真值表验证 $\vdash$ 的正确性

优点：更容易证明 $\Gamma \not \models \psi$ ，只要找到一个左侧为T的assignment，而右侧为F即可

缺点：想要证明 $\models$ 更困难，需要遍历全部的真值组合。

一阶逻辑evaluate的难点：每一个变量都是一个可能的具体值的占位符

对 $\forall x\phi$ ，每个x， $\phi$ 都为真，则最终取值为真

对 $\exists x \phi$ ，找到一个x0， $\phi$ 为真，则最终取值为真

如果 $\phi$ 的结构为 $\land \lor \neg \rightarrow$ 等（解析树根节点），那么最终的真值可以按照各谓词公式的真假，遵循命题逻辑中的连接词运算进行求解

问题进一步转为求解 $P(t_i)$ 的真值。对此需要明确谓词常量的含义和term的含义。

$(\mathcal{F},\mathcal{P})$ 的模型 $\mathcal{M}$ ：

非空集合A，所有可能的具体取值全体集合
对每一个对无参函数 $f \in \mathcal{F}$ ， $f^\mathcal{M}$ 有一个A中对应的取值
对每一个元数>0的函数f， $f^\mathcal{M}$ 是一个映射，从 $A^n \rightarrow A$ ，A的n元组集合到A中某元素的映射
对每一个元数n>0的谓词常量P， $P^\mathcal{M}$ 是 $A^n$ 的子集。

例， $\mathcal{F} \stackrel{def}{==}\{i \}, \mathcal{P}\stackrel{def}{==}\{R,F \}$ ，R是二元谓词，F是一元谓词， $\mathcal{M}$ 包含：

A={a,b,c}，具体取值的全体
$i^\mathcal{M}=\{a\}$
无非0元函数
$R^\mathcal{M}$ 是 $A^2$ 的子集。 $A^2=\{(a,a),(b,a),(c,a),(a,b),(b,b),(c,b),(a,c),(b,c),(c,c)\}$

$R^\mathcal{M}$ 可以为 $\{(a,a),(a,b),(a,c),(b,c),(c,c)\}$

$F^1=\{a,b,c\}$ ，则 $F^M$ 可为 $\{b,c\}$

环境：将变量映射到具体值的look-up table
$给定\mathcal{F,P}的一个模型\mathcal{M}（按照上述方式给出），若\mathcal{M}\models_l \phi，则在l环境下，公式\phi被计算为真$
对于在l环境下的满足性定义：

$P(t_1,t_2,…t_n)$ ，根据l字典，将全部变量换为具体值，此时 $\mathcal{M}\models_l P(t_1,…,t_n) \iff (a_1,…,a_n)$ 均在 $P^{\mathcal{M}}$ 中
$\forall x \phi$ ：将公式 $\phi$ 中的每个x分别替换为模型A中的具体值，然后在根据字典，将其他变量换为具体值，如果每一次的替换都能满足，则 $\forall x \phi$ 也被该模型满足
存在性，类似上条，但对约束变量x的替换只需要找到一个在A中的具体值即可。
或且非蕴含的满足性分别检查单个公式的满足性得到T和F，再按照命题逻辑联结词真值表得到T和F。