命题逻辑

命题逻辑抽取的是组合结构，而不是把句子里的所有含义都形式化。把“用户已登录”记作 $p$ 后，系统只知道它是一个可以真假的基本命题；用户名、登录时间、谁进行了登录，都没有进入公式内部。

这种抽象让不同情境共享同一种推理。由“$p$ 成立”和“$p\to q$ 成立”推出 $q$，不依赖 $p,q$ 究竟表示门禁状态、电路信号还是某个数学断言。只要前提都为真，真值表就排除了结论为假的可能。

但日常的“如果”可能暗含因果、时间或相关性，材料蕴含 $\to$ 不自动表达这些内容。例如“报警开启就锁门”写作 $a\to l$，意思是在当前状态中不允许“报警开启而门未锁”。当报警没有开启时，这条约束不管门是否上锁，并没有声称“报警导致了锁门动作”。若要求“报警开启后的下一时刻门会上锁”，还须表示时间与状态变化，仅靠当前状态的两个真值不能表达“下一时刻”。

一条权限规则怎样接受检验 ​

令 $l$ 表示“已登录”，$a$ 表示“是管理员”，$e$ 表示“可以编辑”。规则“登录并且是管理员即可编辑”写作

先计算括号内的 $l\wedge a$，再把结果作为蕴含的前件。若 $l=1,a=1,e=0$，前件为真而后件为假，所以整条规则为假，准确暴露“合法用户却不能编辑”的违例。若另知 $l,a$ 都为真并且规则成立，便可推出 $e$。

若只知 $e$ 为真，却不能反推 $a$：取 $l=1,a=0,e=1$，原规则依然成立。规则只给出充分条件，没有断言只有管理员才能编辑。

若产品真正要求“可以编辑，当且仅当已登录且是管理员”，则应写 $e\leftrightarrow (l\wedge a)$。两个方向分别保证合法用户可以编辑，以及获得编辑权限的用户满足全部要求。把单向蕴含误写成双条件，会悄悄增加一半规范。

对单个蕴含，逆否式 $\mathrm{\neg }q\to \mathrm{\neg }p$ 与 $p\to q$ 等价，逆式 $q\to p$ 一般不等价。反推前件与利用逆否式，是两种不同的推理。

相同字母，括号不同 ​

比较 $\mathrm{\neg }(p\wedge q)$ 与 $(\mathrm{\neg }p)\wedge q$。前者只禁止两者同时为真，后者还要求 $q$ 为真。令 $p=q=0$，前者真而后者假，所以它们不等价。

正确的 De Morgan 等价式是

否定“两个条件都满足”，只需其中至少一个不满足，不要求两个都不满足。真值表在这里不仅用于验算，还能把自然语言里的否定范围变成明确的结构。

公式相同、等价与可满足 ​

$(p\wedge q)$ 与 $(q\wedge p)$ 是不同的公式，但在每个赋值下真值相同，因而逻辑等价。$p\vee \mathrm{\neg }p$ 在所有赋值下都真，称为永真式；$p\wedge \mathrm{\neg }p$ 在所有赋值下都假，称为矛盾式；存在至少一个使公式为真的赋值，便称公式可满足。

例如 $p$ 可满足，却不是永真式：赋值 $v(p)=1$ 是可满足性的见证，赋值 $w(p)=0$ 又是永真性的反例。同一公式接受这两种判断并不矛盾，因为前者只要求存在成功赋值，后者要求每个赋值都成功。某次观察发现 $p$ 为真，也不会把它变成逻辑定理。

语义后承与形式推导 ​

写作 $\mathrm{\Gamma }\models \phi$，表示每个使前提集合 $\mathrm{\Gamma }$ 中所有公式为真的赋值，也使 $\phi$ 为真。否定这种关系只需给出一个反模型：全部前提真，但结论假。上面的权限赋值就是“由可编辑反推管理员”的反模型。

写作 $\mathrm{\Gamma }⊢\phi$，则表示在指定证明系统中，存在从前提出发、按规则形成的有限推导。$\models$ 谈所有赋值，$⊢$ 谈可检查的证明对象。对经典命题逻辑的标准自然演绎系统，可靠性与完备性把两者连接起来，但这个连接是关于证明系统的定理，而不是两个符号的定义。[1]

有限前提下，还可以把推理有效性转成不可满足性。例如

等价于 $p\wedge (p\to q)\wedge \mathrm{\neg }q$ 不可满足。这让“证明结论必然成立”变成“搜索有没有前提全真、结论为假的情况”。

从真值表到求解器 ​

含 $n$ 个不同命题字母的有限公式只有 $2^n$ 种赋值，逐行枚举能够判定可满足性和永真性；但赋值数量随 $n$ 指数增长。SAT 求解器通常以合取范式可满足性理路CNF 可满足性问题CNF satisfiability · CNF-SAT给定有限个命题子句的合取，判定是否存在同时满足全部子句的布尔赋值。作为接口，利用公式结构搜索模型或排除整批赋值，不必总把真值表展开。最坏情形复杂性并不妨碍大量结构化实例被有效求解。转成合取范式时，引入辅助变量的编码通常保证等可满足性，不能直接当成扩展变量空间中逐赋值等价；应说明辅助变量与原变量之间的对应。

电路验证可以把输入位与门输出写成命题约束，再询问“规范违例是否可满足”；如果可满足，模型就是一个具体反例输入。布尔代数强调与这些真值运算对应的代数恒等式，命题逻辑则还明确区分公式、解释和推导。

若需要拆开“每个对象都满足某性质”中的对象和性质，就进入一阶逻辑理路一阶逻辑First-order logic · Predicate logic在命题逻辑上加入对象、关系、函数与量词的形式语言和模型语义。。允许零元关系符号的一阶语言包含一个命题片段：只用这些零元原子式和命题联结词，不使用个体量词或其他原子式。将命题字母解释为零元关系的真假，就逐公式保留了这里的真值语义；这是命题逻辑作为一阶逻辑特例的具体范围。命题逻辑本身没有个体变量与量词。一阶逻辑语法理路一阶逻辑语法First-order syntax以符号表、项、原子公式、联结词和量词归纳生成一阶公式的语法系统。把这些内部结构显式化；在有限论域中枚举量词可以得到命题编码，但不能据此把一般一阶推理视为有限真值表计算。直觉主义等逻辑改变推理原则时，也不能照搬这里的经典二值语义。这个表达能力上的包含关系，不要求学习命题逻辑之前先掌握一阶逻辑。

直觉主义命题逻辑理路直觉主义命题逻辑Intuitionistic propositional logic · IPC · IPL以构造性证明规则解释命题联结词、且不无条件接受排中律或双重否定消去的逻辑。沿用这些联结词的语法，却不把经典二值真值表当作其完整语义。这里的排中律与双重否定消去在那里不是一般定理；当前没有证据支持 $p$，也不等于已经证明 $\mathrm{\neg }p$。比较两者时，要同时固定证明规则与语义，而不只看公式拼写。