变形规则

在命题逻辑和谓词逻辑的推理中，使用的一些常见的命题逻辑的重言式或谓词逻辑中的有效式、重言等值公式（置换规则）、重言蕴含公式（推理规则）以及一些元定理。

基本规则

通常逻辑系统中的基本规则，但本身不一定是出现在形式化公理系统中的公理。

• 同一律(law of identity)

[math]\displaystyle{ \vdash P \rightarrow P }[/math]

• 矛盾律(law/principle of (non-)contradiction, LNC, PNC)

[math]\displaystyle{ \vdash \lnot (P \land \lnot P) }[/math]

• 排中律(law/principle of excluded middle, EM)

[math]\displaystyle{ \vdash P \lor \lnot P }[/math]

等值公式与置换规则

• 双重否定律(double negation, DN)

[math]\displaystyle{ P = \lnot \lnot P }[/math]

• 双重否定引入(double negation introduction)规则（[math]\displaystyle{ \lnot\lnot }[/math]-int）

[math]\displaystyle{ P \vdash \lnot \lnot P }[/math]

• 否定消去(negation elimination)规则（[math]\displaystyle{ \lnot }[/math]-elim）

[math]\displaystyle{ \lnot \lnot P \vdash P }[/math]

• 结合律(associativity)

[math]\displaystyle{ (P \land Q) \land R = P \land (Q \land R) }[/math]

[math]\displaystyle{ (P \lor Q) \lor R = P \lor (Q \lor R) }[/math]

[math]\displaystyle{ (P \leftrightarrow Q) \leftrightarrow R = P \lor (Q \lor R) }[/math]

• 结合律置换规则(Assoc)

[math]\displaystyle{ (P \land Q) \land R \dashv\vdash P \land (Q \land R) }[/math]

[math]\displaystyle{ (P \lor Q) \lor R \dashv\vdash P \lor (Q \lor R) }[/math]

• 交换律(commutativity)

[math]\displaystyle{ P \land Q = Q \land P }[/math]

[math]\displaystyle{ P \lor Q = Q \lor P }[/math]

[math]\displaystyle{ P \rightarrow (Q \rightarrow R) = Q \rightarrow (P \rightarrow R) }[/math]

[math]\displaystyle{ P \leftrightarrow Q = Q \leftrightarrow P }[/math]

• 交换律置换规则(Comm)

[math]\displaystyle{ P \land Q \vdash Q \land P }[/math]

[math]\displaystyle{ P \lor Q \vdash Q \lor P }[/math]

• 分配律(distributivity)

[math]\displaystyle{ P \land (Q \lor R) = (P \land Q) \lor (P \land R) }[/math]

[math]\displaystyle{ P \lor (Q \land R) = (P \lor Q) \land (P \lor R) }[/math]

[math]\displaystyle{ P \land (Q \land R) = (P \land Q) \land (P \land R) }[/math]

[math]\displaystyle{ P \lor (Q \lor R) = (P \lor Q) \lor (P \lor R) }[/math]

[math]\displaystyle{ P \rightarrow (Q \rightarrow R) = (P \rightarrow Q) \rightarrow (P \rightarrow R) }[/math]

[math]\displaystyle{ P \rightarrow (Q \leftrightarrow R) = (P \rightarrow Q) \leftrightarrow (P \rightarrow R) }[/math]

[math]\displaystyle{ P \rightarrow (Q \land R) = (P \rightarrow Q) \land (P \rightarrow R) }[/math]

[math]\displaystyle{ P \lor (Q \leftrightarrow R) = (P \lor Q) \leftrightarrow (P \lor R) }[/math]

• 双重分配律(double distribution)

[math]\displaystyle{ (P \land Q) \lor (R \land S) = ((P \lor R) \land (P \lor S)) \land ((Q \lor R) \land (Q \lor S)) }[/math]

[math]\displaystyle{ (P \lor Q) \land (R \lor S) = ((P \land R) \lor (P \land S)) \lor ((Q \land R) \lor (Q \land S)) }[/math]

• 分配律置换规则(Dist)

[math]\displaystyle{ P \land (Q \lor R) \dashv\vdash (P \land Q) \lor (P \land R) }[/math]

[math]\displaystyle{ P \lor (Q \land R) \dashv\vdash (P \lor Q) \land (P \lor R) }[/math]

[math]\displaystyle{ P \land (Q_1 \lor \dots \lor Q_n) \vdash (P \land Q_1) \lor \dots \lor (P \land Q_n) }[/math]

[math]\displaystyle{ P \lor (Q_1 \land \dots \land Q_n) \vdash (P \lor Q_1) \land \dots \land (P \lor Q_n) }[/math]

• 反演律/德摩根律(De Morgan's law, DeM)

[math]\displaystyle{ \lnot (P \lor Q) = (\lnot P) \land (\lnot Q) }[/math]

[math]\displaystyle{ \lnot (P \land Q) = (\lnot P) \lor (\lnot Q) }[/math]

• 反演律置换规则

[math]\displaystyle{ \lnot (P \lor Q) \dashv\vdash (\lnot P) \land (\lnot Q) }[/math]

[math]\displaystyle{ \lnot (P \land Q) \dashv\vdash (\lnot P) \lor (\lnot Q) }[/math]

[math]\displaystyle{ P \lor Q \dashv\vdash \lnot ((\lnot P) \land (\lnot Q)) }[/math]

[math]\displaystyle{ P \land Q \dashv\vdash \lnot ((\lnot P) \lor (\lnot Q)) }[/math]

• 幂等律(idempotency)/重言(tautology)

[math]\displaystyle{ P \lor P = P }[/math]

[math]\displaystyle{ P \land P = P }[/math]

• 重言置换规则(Idem)/同义重复规则(Taut)

[math]\displaystyle{ P \lor P \dashv\vdash P }[/math]

[math]\displaystyle{ P \land P \dashv\vdash P }[/math]

• 吸收律

[math]\displaystyle{ (P \land Q) \lor Q = Q }[/math]

[math]\displaystyle{ (P \lor Q) \land Q = Q }[/math]

• 吸收律置换规则

[math]\displaystyle{ (P \land Q) \lor Q \vdash Q }[/math]

[math]\displaystyle{ (P \lor Q) \land Q \vdash Q }[/math]

• 假言析取

[math]\displaystyle{ P \rightarrow Q = (\lnot P) \or Q = \lnot (P \land \lnot Q) }[/math]

• 蕴含置换规则 (conditional exchange, CE)

[math]\displaystyle{ P \rightarrow Q \dashv\vdash \lnot P \or Q }[/math]

• 蕴含互化

[math]\displaystyle{ P \leftrightarrow Q = (P \rightarrow Q) \land (Q \rightarrow P) = (P \land Q) \lor ((\lnot P) \land (\lnot Q)) = (P \lor (\lnot Q)) \land ((\lnot P) \lor Q) }[/math]

• 双蕴含置换规则 (biconditional exchange, BE)

[math]\displaystyle{ P \leftrightarrow Q \vdash (P \rightarrow Q) \land (Q \rightarrow P) }[/math]

• 双蕴含引入规则 (biconditional introduction, [math]\displaystyle{ \leftrightarrow }[/math]-int)

[math]\displaystyle{ P \rightarrow Q, Q \rightarrow P \vdash P \leftrightarrow Q }[/math]

• 双蕴含消去规则 (biconditional elimination, [math]\displaystyle{ \leftrightarrow }[/math]-elim)

[math]\displaystyle{ P \leftrightarrow Q \vdash P \rightarrow Q }[/math]

[math]\displaystyle{ P \leftrightarrow Q \vdash Q \rightarrow P }[/math]

• 假言易位律/逆否命题

[math]\displaystyle{ P \rightarrow Q = \lnot Q \rightarrow \lnot P }[/math]

• 假言易位法则(Contrap/Trans)

[math]\displaystyle{ P \rightarrow Q \vdash \lnot Q \rightarrow \lnot P }[/math]

[math]\displaystyle{ \lnot P \rightarrow \lnot Q \vdash Q \rightarrow P }[/math]

• 移出律

[math]\displaystyle{ P \rightarrow (Q \rightarrow R) = (P \land Q) \rightarrow R }[/math]

• 移出(exportation, Exp)规则

[math]\displaystyle{ P \rightarrow (Q \rightarrow R) \Rightarrow (P \land Q) \rightarrow R }[/math]

[math]\displaystyle{ (P \land Q) \rightarrow R \Rightarrow P \rightarrow (Q \rightarrow R) }[/math]

涉及谓词逻辑的：

• 量词否定

[math]\displaystyle{ \lnot \forall x \phi = \exists x \lnot \phi }[/math]

[math]\displaystyle{ \lnot \exists x \phi = \forall x \lnot \phi }[/math]

[math]\displaystyle{ \lnot \forall x \lnot \phi = \exists x \phi }[/math]

[math]\displaystyle{ \lnot \exists x \lnot \phi = \forall x \phi }[/math]

• 量词否定(qualifier negation, QN / De Morgan's law for quatifiers, DMQ 或 QDeM)规则

[math]\displaystyle{ \lnot \forall x \phi \dashv\vdash \exists x \lnot \phi }[/math]

[math]\displaystyle{ \lnot \exists x \phi \dashv\vdash \forall x \lnot \phi }[/math]

[math]\displaystyle{ \lnot \forall x \lnot \phi \dashv\vdash \exists x \phi }[/math]

[math]\displaystyle{ \lnot \exists x \lnot \phi \dashv\vdash \forall x \phi }[/math]

• 条件量词否定

[math]\displaystyle{ \lnot \forall x (\phi \rightarrow \psi) = \exists x (\phi \land \lnot \psi) }[/math]

[math]\displaystyle{ \lnot \exists x (\phi \land \psi) = \forall x (\phi \rightarrow \lnot \psi) }[/math]

[math]\displaystyle{ \lnot \forall x (\phi \rightarrow \lnot \psi) = \exists x (\phi \land \psi) }[/math]

[math]\displaystyle{ \lnot \exists x (\phi \land \lnot \psi) = \forall x (\phi \rightarrow \psi) }[/math]

• 条件量词否定(conditional qualifier negation, CQN / conditional De Morgan's law for quatifiers, CDMQ 或 CQDeM)规则

[math]\displaystyle{ \lnot \forall x (\phi \rightarrow \psi) \dashv\vdash \exists x (\phi \land \lnot \psi) }[/math]

[math]\displaystyle{ \lnot \exists x (\phi \land \psi) \dashv\vdash \forall x (\phi \rightarrow \lnot \psi) }[/math]

[math]\displaystyle{ \lnot \forall x (\phi \rightarrow \lnot \psi) \dashv\vdash \exists x (\phi \land \psi) }[/math]

[math]\displaystyle{ \lnot \exists x (\phi \land \lnot \psi) \dashv\vdash \forall x (\phi \rightarrow \psi) }[/math]

推理规则

• 合取(conjunction, Conj)/合取引入

[math]\displaystyle{ P, Q \vdash P \land Q }[/math]

• 简化(simplication, Simp)/合取消去

[math]\displaystyle{ P \land Q \vdash P }[/math]

[math]\displaystyle{ P \land Q \vdash Q }[/math]

• 附加(addition, Add)/析取引入

[math]\displaystyle{ P \vdash P \lor Q }[/math]

[math]\displaystyle{ P \vdash Q \lor P }[/math]

• MP(modus ponens, MP)/肯定前件(affirming the antecedent)/蕴含消去(implication elimination, [math]\displaystyle{ \rightarrow }[/math]-elim)

[math]\displaystyle{ P \rightarrow Q, P \vdash Q }[/math]

• 双条件 MP(MP for the biconditional, MPBC)

[math]\displaystyle{ P \leftrightarrow Q, P \vdash Q }[/math]

[math]\displaystyle{ P \leftrightarrow Q, Q \vdash P }[/math]

• MT(modus tollens, MT)/否定后件(denying the consequent)

[math]\displaystyle{ P \rightarrow Q, \lnot Q \vdash \lnot P }[/math]

• 双条件 MT(MT for the biconditional, MTBC)

[math]\displaystyle{ P \leftrightarrow Q, \lnot P \vdash \lnot Q }[/math]

[math]\displaystyle{ P \leftrightarrow Q, \lnot Q \vdash \lnot P }[/math]

• 假言三段论(hypothetical syllogism, HS)

[math]\displaystyle{ P \rightarrow Q, Q \rightarrow R \vdash P \rightarrow R }[/math]

• 选言三段论(disjunctive syllogism, DS)

[math]\displaystyle{ (P \lor Q) \land \lnot P \vdash Q }[/math]

• 二难推理(dilemma)/(case argument,CA)

[math]\displaystyle{ P \lor Q, P \rightarrow R, Q \rightarrow R \vdash R }[/math]

• 构成式二难推理/肯定二难推理

[math]\displaystyle{ P \lor Q, P \rightarrow R, Q \rightarrow S \vdash R \lor S }[/math]

• 破斥式二难推理/否定二难推理

[math]\displaystyle{ P \rightarrow R, Q \rightarrow S, \lnot R \lor \lnot S \vdash \lnot P \lor \lnot Q }[/math]

• 归谬律(RAA)

[math]\displaystyle{ P \rightarrow Q, P \rightarrow \lnot Q \vdash \lnot P }[/math]

[math]\displaystyle{ \lnot P \rightarrow Q, \lnot P \rightarrow \lnot Q \vdash P }[/math]

• Pierce 律(Pierce's law)

[math]\displaystyle{ P \rightarrow (Q \rightarrow P) \vdash P }[/math]

涉及谓词逻辑的

• 全称量词特指(universal specification/instantiation, US/UI)/全称量词消去(universal elimination, [math]\displaystyle{ \forall }[/math]-elim)

[math]\displaystyle{ \forall x P \vdash P(t/x) }[/math] ，要求可自由代入

• 广义全称特指

[math]\displaystyle{ \forall x_1 \dots \forall x_n P \vdash P(t_1/x_1, \dots, t_n/x_n) }[/math] ，要求可自由代入

• 存在量词推广(existential generalization, EG)/存在量词引入(existential introduction, [math]\displaystyle{ \exists }[/math]-int)

[math]\displaystyle{ P(t/x) \vdash \exists x P }[/math]，要求可自由代入

• 广义存在推广

[math]\displaystyle{ P(t_1/x_1, \dots, t_n/x_n) \vdash \exists x_1 \dots \exists x_n P }[/math] ，要求可自由代入

• 全称量词推广(universal generalization, UG)/全称量词引入(universal elimination, [math]\displaystyle{ \forall }[/math]-int)

标记任意 [math]\displaystyle{ t }[/math] ，有 [math]\displaystyle{ P(t/x) }[/math] ，可推出 [math]\displaystyle{ \forall x P }[/math] ，要求可自由代入

• 广义全称推广

标记任意 [math]\displaystyle{ t_1, \dots, t_n }[/math] ，有 [math]\displaystyle{ P(t_1/x_1, \dots, t_n/x_n) }[/math] ，可推出 [math]\displaystyle{ \forall x_1 \dots \forall x_n P }[/math] ，要求可自由代入

• 存在量词特指(existential specification/instantiation)/存在量词消去(existential introduction, [math]\displaystyle{ \exists }[/math]-elim)

[math]\displaystyle{ \exists x P }[/math] ，标记特定 [math]\displaystyle{ t }[/math] ，可推出 [math]\displaystyle{ P(t/x) }[/math] ，要求可自由代入

• 广义存在推广

[math]\displaystyle{ \exists x_1 \dots \exists x_n P }[/math] ，标记特定 [math]\displaystyle{ t_1, \dots, t_n }[/math] ，可推出 [math]\displaystyle{ P(t_1/x_1, \dots, t_n/x_n) \vdash }[/math] ，要求可自由代入

• 等词引入

[math]\displaystyle{ \vdash t=t }[/math]

• 等词消去/等项替换

[math]\displaystyle{ P(s/x), s=t \vdash P(t/x) }[/math]

[math]\displaystyle{ P(s/x), t=s \vdash P(t/x) }[/math]

• 同类量词排列

[math]\displaystyle{ \vdash \mathsf{Q} x_1 \dots \mathsf{Q} x_n \phi \rightarrow \mathsf{Q} x_{k_1} \dots \mathsf{Q} x_{k_n} \phi }[/math] ，其中 [math]\displaystyle{ k_1 \dots k_n }[/math] 是 [math]\displaystyle{ 1 \dots n }[/math] 的一个排列且 [math]\displaystyle{ \mathsf{Q} \in \{\forall, \exists\} }[/math] 。

• 空约束

若 [math]\displaystyle{ x }[/math] 不在 [math]\displaystyle{ \phi }[/math] 中自由出现，则 [math]\displaystyle{ \forall x \phi \dashv\vdash \phi }[/math] ，且 [math]\displaystyle{ \exists x \phi \dashv\vdash \phi }[/math] 。

• 量词的分配和提取

[math]\displaystyle{ \forall x (\phi \land \psi) \dashv\vdash \forall x \phi \land \forall x \psi }[/math]

[math]\displaystyle{ \exists x (\phi \land \psi) \vdash \exists x \phi \land \exists x \psi }[/math]

[math]\displaystyle{ \forall x (\phi \lor \psi) \dashv \forall x \phi \lor \forall x \psi }[/math]

[math]\displaystyle{ \exists x (\phi \lor \psi) \dashv\vdash \exists x \phi \lor \exists x \psi }[/math]

[math]\displaystyle{ \forall x (\phi \rightarrow \psi) \vdash \forall x \phi \rightarrow \forall x \psi }[/math]

[math]\displaystyle{ \forall x (\phi \leftrightarrow \psi) \dashv\vdash \forall x \phi \leftrightarrow \forall x \psi }[/math]

元定理

在古典逻辑中，分离规则 mp 下，可以确认关于可演绎性有以下元定理。 但其中部分元命题可能不是非古典逻辑中的元定理。

• 子集超集

[math]\displaystyle{ \Gamma \vdash \phi }[/math] ，则存在有限子集 [math]\displaystyle{ \Delta }[/math] 使得 [math]\displaystyle{ \Delta \vdash \phi }[/math]

[math]\displaystyle{ \Gamma \vdash \phi }[/math] ， [math]\displaystyle{ \Gamma \subseteq \Delta }[/math] ，则 [math]\displaystyle{ \Delta \vdash \phi }[/math]

• 切消定理(cut-elimination theorem, Cut)

[math]\displaystyle{ \Gamma, \phi \vdash \psi }[/math] 且 [math]\displaystyle{ \Delta \vdash \phi }[/math] ，则 [math]\displaystyle{ \Gamma, \Delta \vdash \psi }[/math]

[math]\displaystyle{ \Gamma, \phi_1, \dots \phi_m \vdash \psi }[/math] 且对每个 [math]\displaystyle{ i = 0, \dots, m }[/math] 都有 [math]\displaystyle{ \Delta \vdash \phi_i }[/math] ，则 [math]\displaystyle{ \Gamma, \Delta \vdash \psi }[/math]

• （可证关系的）传递性(transivity, Tran)

[math]\displaystyle{ \Gamma \vdash \phi }[/math] 且 [math]\displaystyle{ \phi \vdash \psi }[/math] ，则 [math]\displaystyle{ \Gamma \vdash \psi }[/math]

[math]\displaystyle{ \chi \vdash \phi }[/math] 且 [math]\displaystyle{ \phi \vdash \psi }[/math] ，则 [math]\displaystyle{ \chi \vdash \psi }[/math]

• 分离规则/肯定前件(modus ponens, MP)

[math]\displaystyle{ \Gamma \vdash \phi }[/math] 且 [math]\displaystyle{ \Delta \vdash \phi \rightarrow \psi }[/math] ，则 [math]\displaystyle{ \Gamma, \Delta \vdash \psi }[/math]

• MPBC

• 否定后件(modus tollens, MT)

[math]\displaystyle{ \Gamma \vdash \lnot \psi }[/math] 且 [math]\displaystyle{ \Delta \vdash \phi \rightarrow \psi }[/math] ，则 [math]\displaystyle{ \Gamma, \Delta \vdash \lnot \phi }[/math]

• MTBC

• 演绎定理(deduction theorem, DT)

[math]\displaystyle{ \Gamma, \phi \vdash \psi }[/math] 当且仅当 [math]\displaystyle{ \Gamma \vdash \phi \rightarrow \psi }[/math]

• 分情况论证(case argument, CA)

[math]\displaystyle{ \Gamma, \phi \vdash \chi }[/math] 且 [math]\displaystyle{ \Delta, \psi \vdash \chi' }[/math] ，则 [math]\displaystyle{ \Gamma, \Delta, \phi \lor \psi \vdash \chi \lor \chi' }[/math]

• 特例

[math]\displaystyle{ \Gamma, \phi \vdash \chi }[/math] 且 [math]\displaystyle{ \Delta, \psi \vdash \chi }[/math] ，则 [math]\displaystyle{ \Gamma, \Delta, \phi \lor \psi \vdash \chi }[/math]

[math]\displaystyle{ \Gamma, \phi \vdash \chi }[/math] ，则 [math]\displaystyle{ \Gamma, \phi \lor \psi \vdash \chi \lor \psi }[/math] ， [math]\displaystyle{ \Gamma, \psi \lor \phi \vdash \psi \lor \chi }[/math]

[math]\displaystyle{ \Gamma, \phi \vdash \chi }[/math] 且 [math]\displaystyle{ \Delta, \lnot \phi \vdash \chi }[/math] ，则 [math]\displaystyle{ \Gamma, \Delta \vdash \chi }[/math]

• 简单归谬律(SRAA)

[math]\displaystyle{ \Gamma, \phi \vdash \lnot \phi }[/math] ，则 [math]\displaystyle{ \Gamma \vdash \lnot \phi }[/math]

[math]\displaystyle{ \Gamma, \lnot \phi \vdash \phi }[/math] ，则 [math]\displaystyle{ \Gamma \vdash \phi }[/math]

• 爆炸律(principle of explosion, ex falso [sequitur] quodlibet, EFQ, ex contradictione [sequitur] quodlibet, ECQ)/不一致效果(Inconsistency Effect, IE)

[math]\displaystyle{ \phi, \lnot \phi \vdash \psi }[/math]

[math]\displaystyle{ \Gamma \vdash \phi }[/math] 且 [math]\displaystyle{ \Delta \vdash \lnot \phi }[/math] ，则 [math]\displaystyle{ \Gamma, \Delta \vdash \psi }[/math]

• 双条件证明（biconditional proof, BCP）

[math]\displaystyle{ \Gamma, \phi \vdash \psi }[/math] 且 [math]\displaystyle{ \Delta, \psi \vdash \phi }[/math] ，则 [math]\displaystyle{ \Gamma, \Delta \vdash \phi \leftrightarrow \psi }[/math]

• 等值置换(RE)

[math]\displaystyle{ \Gamma \vdash \phi \leftrightarrow \psi }[/math] ，则 [math]\displaystyle{ \Gamma \vdash \chi(\phi/p) \rightarrow \chi(\psi/p) }[/math]

• 推广

[math]\displaystyle{ \Gamma \vdash \phi \rightarrow \psi }[/math] 、 [math]\displaystyle{ \Delta \vdash \psi \rightarrow \phi }[/math] 且 [math]\displaystyle{ \Theta \vdash \chi(\phi/p) }[/math] ，则 [math]\displaystyle{ \Gamma, \Delta, \Theta \vdash \chi(\psi/p) }[/math]

证明论
形式化公理系统（形式化、公理化）
推理系统	Hilbert 风格/公理系统：Hilbert 表示
	Gentzen 风格-自然演绎系统： Gentzen 式自然演绎、 Fitch 式自然演绎、 Suppes–Lemmon 式自然演绎
	Gentzen 风格-相继式演算： Gentzen 式相继式演算
证明、演绎	演绎、可演绎、证明、可证明
命题、定理	公理/公理模式、定理、元定理、变形规则
推理规则性质	保存真实性、保存重言性
公理系统性质	可靠性、完备性/完全性、一致性、独立性