查看“︁变形规则”︁的源代码

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

== 基本规则 ==

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

* '''[[同一律]]'''('''law of identity''')
: <math>\vdash P \rightarrow P</math>
* '''[[矛盾律]]'''('''law/principle of (non-)contradiction''', '''LNC''', '''PNC''')
: <math>\vdash \lnot (P \land \lnot P)</math>
* '''[[排中律]]'''('''law/principle of excluded middle''', '''EM''')
: <math>\vdash P \lor \lnot P</math>

== 等值公式与置换规则 ==

* '''[[双重否定式|双重否定律]]'''('''double negation''', '''DN''')
: <math>P = \lnot \lnot P</math>
:* 双重否定引入(double negation introduction)规则（'''<math>\lnot\lnot</math>-int'''）
:: <math>P \vdash \lnot \lnot P</math>
:* 否定消去(negation elimination)规则（'''<math>\lnot</math>-elim'''）
:: <math>\lnot \lnot P \vdash P</math>
* [[结合律]](associativity)
: <math>(P \land Q) \land R = P \land (Q \land R)</math>
: <math>(P \lor Q) \lor R = P \lor (Q \lor R)</math>
: <math>(P \leftrightarrow Q) \leftrightarrow R = P \lor (Q \lor R)</math>
:* 结合律置换规则('''Assoc''')
:: <math>(P \land Q) \land R \dashv\vdash P \land (Q \land R)</math>
:: <math>(P \lor Q) \lor R \dashv\vdash P \lor (Q \lor R)</math>
* [[交换律]](commutativity)
: <math>P \land Q = Q \land P</math>
: <math>P \lor Q = Q \lor P</math>
: <math>P \rightarrow (Q \rightarrow R) = Q \rightarrow (P \rightarrow R)</math>
: <math>P \leftrightarrow Q = Q \leftrightarrow P</math>
:* 交换律置换规则('''Comm''')
:: <math>P \land Q \vdash Q \land P</math>
:: <math>P \lor Q \vdash Q \lor P</math>
* [[分配律]](distributivity)
: <math>P \land (Q \lor R) = (P \land Q) \lor (P \land R)</math>
: <math>P \lor (Q \land R) = (P \lor Q) \land (P \lor R)</math>
: <math>P \land (Q \land R) = (P \land Q) \land (P \land R)</math>
: <math>P \lor (Q \lor R) = (P \lor Q) \lor (P \lor R)</math>
: <math>P \rightarrow (Q \rightarrow R) = (P \rightarrow Q) \rightarrow (P \rightarrow R)</math>
: <math>P \rightarrow (Q \leftrightarrow R) = (P \rightarrow Q) \leftrightarrow (P \rightarrow R)</math>
: <math>P \rightarrow (Q \land R) = (P \rightarrow Q) \land (P \rightarrow R)</math>
: <math>P \lor (Q \leftrightarrow R) = (P \lor Q) \leftrightarrow (P \lor R)</math>
:* 双重分配律(double distribution)
:: <math>(P \land Q) \lor (R \land S) = ((P \lor R) \land (P \lor S)) \land ((Q \lor R) \land (Q \lor S))</math>
:: <math>(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>P \land (Q \lor R) \dashv\vdash (P \land Q) \lor (P \land R)</math>
:: <math>P \lor (Q \land R) \dashv\vdash (P \lor Q) \land (P \lor R)</math>
:: <math>P \land (Q_1 \lor \dots \lor Q_n) \vdash (P \land Q_1) \lor \dots \lor (P \land Q_n)</math>
:: <math>P \lor (Q_1 \land \dots \land Q_n) \vdash (P \lor Q_1) \land \dots \land (P \lor Q_n)</math>
* 反演律/[[De Morgan 律（逻辑）|德摩根律]](De Morgan's law, '''DeM''')
: <math>\lnot (P \lor Q) = (\lnot P) \land (\lnot Q)</math>
: <math>\lnot (P \land Q) = (\lnot P) \lor (\lnot Q)</math>
:* 反演律置换规则
:: <math>\lnot (P \lor Q) \dashv\vdash (\lnot P) \land (\lnot Q)</math>
:: <math>\lnot (P \land Q) \dashv\vdash (\lnot P) \lor (\lnot Q)</math>
:: <math>P \lor Q \dashv\vdash \lnot ((\lnot P) \land (\lnot Q))</math>
:: <math>P \land Q \dashv\vdash \lnot ((\lnot P) \lor (\lnot Q))</math>
* [[幂等律]](idempotency)/重言(tautology)
: <math>P \lor P = P</math>
: <math>P \land P = P</math>
:* 重言置换规则('''Idem''')/同义重复规则('''Taut''')
:: <math>P \lor P \dashv\vdash P</math>
:: <math>P \land P \dashv\vdash P</math>
* [[吸收律]]
: <math>(P \land Q) \lor Q = Q</math>
: <math>(P \lor Q) \land Q = Q</math>
:* 吸收律置换规则
:: <math>(P \land Q) \lor Q \vdash Q</math>
:: <math>(P \lor Q) \land Q \vdash Q</math>
* 假言析取
: <math>P \rightarrow Q = (\lnot P) \or Q = \lnot (P \land \lnot Q)</math>
:* 蕴含置换规则 ('''conditional exchange''', '''CE''')
:: <math>P \rightarrow Q \dashv\vdash \lnot P \or Q</math>
* 蕴含互化
: <math>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>P \leftrightarrow Q \vdash (P \rightarrow Q) \land (Q \rightarrow P)</math>
:* 双蕴含引入规则 ('''biconditional introduction''', '''<math>\leftrightarrow</math>-int''')
:: <math>P \rightarrow Q, Q \rightarrow P \vdash P \leftrightarrow Q</math>
:* 双蕴含消去规则 ('''biconditional elimination''', '''<math>\leftrightarrow</math>-elim''')
:: <math>P \leftrightarrow Q \vdash P \rightarrow Q</math>
:; <math>P \leftrightarrow Q \vdash Q \rightarrow P</math>
* [[假言易位律]]/逆否命题
: <math>P \rightarrow Q = \lnot Q \rightarrow \lnot P</math>
:* 假言易位法则('''Contrap'''/'''Trans''')
:: <math>P \rightarrow Q \vdash \lnot Q \rightarrow \lnot P</math>
:: <math>\lnot P \rightarrow \lnot Q \vdash Q \rightarrow P</math>
* [[移出律]]
: <math>P \rightarrow (Q \rightarrow R) = (P \land Q) \rightarrow R</math>
:* 移出('''exportation''', '''Exp''')规则
:: <math>P \rightarrow (Q \rightarrow R) \Rightarrow (P \land Q) \rightarrow R</math>
:: <math>(P \land Q) \rightarrow R \Rightarrow P \rightarrow (Q \rightarrow R)</math>

涉及谓词逻辑的：

* 量词否定
: <math>\lnot \forall x \phi = \exists x \lnot \phi</math>
: <math>\lnot \exists x \phi = \forall x \lnot \phi</math>
: <math>\lnot \forall x \lnot \phi = \exists x \phi</math>
: <math>\lnot \exists x \lnot \phi = \forall x \phi</math>
:* 量词否定('''qualifier negation''', '''QN''' / '''De Morgan's law for quatifiers''', '''DMQ''' 或 '''QDeM''')规则
:: <math>\lnot \forall x \phi \dashv\vdash \exists x \lnot \phi</math>
:: <math>\lnot \exists x \phi \dashv\vdash \forall x \lnot \phi</math>
:: <math>\lnot \forall x \lnot \phi \dashv\vdash \exists x \phi</math>
:: <math>\lnot \exists x \lnot \phi \dashv\vdash \forall x \phi</math>
* 条件量词否定
: <math>\lnot \forall x (\phi \rightarrow \psi) = \exists x (\phi \land \lnot \psi)</math>
: <math>\lnot \exists x (\phi \land \psi) = \forall x (\phi \rightarrow \lnot \psi)</math>
: <math>\lnot \forall x (\phi \rightarrow \lnot \psi) = \exists x (\phi \land \psi)</math>
: <math>\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>\lnot \forall x (\phi \rightarrow \psi) \dashv\vdash \exists x (\phi \land \lnot \psi)</math>
:: <math>\lnot \exists x (\phi \land \psi) \dashv\vdash \forall x (\phi \rightarrow \lnot \psi)</math>
:: <math>\lnot \forall x (\phi \rightarrow \lnot \psi) \dashv\vdash \exists x (\phi \land \psi)</math>
:: <math>\lnot \exists x (\phi \land \lnot \psi) \dashv\vdash \forall x (\phi \rightarrow \psi)</math>

== 推理规则 ==

* 合取('''conjunction''', '''Conj''')/合取引入
: <math>P, Q \vdash P \land Q</math>
* 简化('''simplication''', '''Simp''')/合取消去
: <math>P \land Q \vdash P</math>
: <math>P \land Q \vdash Q</math>
* 附加('''addition''', '''Add''')/析取引入
: <math>P \vdash P \lor Q</math>
: <math>P \vdash Q \lor P</math>
* MP('''modus ponens''', '''MP''')/[[肯定前件]]('''affirming the antecedent''')/蕴含消去('''implication elimination''', <math>\rightarrow</math>-elim)
: <math>P \rightarrow Q, P \vdash Q</math>
:* 双条件 MP('''MP for the biconditional''', '''MPBC''')
:: <math>P \leftrightarrow Q, P \vdash Q</math>
:: <math>P \leftrightarrow Q, Q \vdash P</math>
* MT('''modus tollens''', '''MT''')/[[否定后件]]('''denying the consequent''')
: <math>P \rightarrow Q, \lnot Q \vdash \lnot P</math>
:* 双条件 MT('''MT for the biconditional''', '''MTBC''')
:: <math>P \leftrightarrow Q, \lnot P \vdash \lnot Q</math>
:: <math>P \leftrightarrow Q, \lnot Q \vdash \lnot P</math>
* [[假言三段论]]('''hypothetical syllogism''', '''HS''')
: <math>P \rightarrow Q, Q \rightarrow R \vdash P \rightarrow R</math>
* [[选言三段论]]('''disjunctive syllogism''', '''DS''')
: <math>(P \lor Q) \land \lnot P \vdash Q</math>
* [[二难推理]]('''dilemma''')/('''case argument''','''CA''')
: <math>P \lor Q, P \rightarrow R, Q \rightarrow R \vdash R</math>
:* 构成式二难推理/肯定二难推理
:: <math>P \lor Q, P \rightarrow R, Q \rightarrow S \vdash R \lor S</math>
:* 破斥式二难推理/否定二难推理
:: <math>P \rightarrow R, Q \rightarrow S, \lnot R \lor \lnot S \vdash \lnot P \lor \lnot Q</math>
* 归谬律('''RAA''')
: <math>P \rightarrow Q, P \rightarrow \lnot Q \vdash \lnot P</math>
: <math>\lnot P \rightarrow Q, \lnot P \rightarrow \lnot Q \vdash P</math>
* [[Peirce 律]]('''Peirce's law''')
: <math>P \rightarrow (Q \rightarrow P) \vdash P</math>

涉及谓词逻辑的

* [[全称特化|全称量词特指]]('''universal specification/instantiation''', '''US/UI''')/全称量词消去('''universal elimination''', '''<math>\forall</math>-elim''')
: <math>\forall x P \vdash P(t/x)</math> ，要求可自由代入
:* 广义全称特指
:: <math>\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>\exists</math>-int''')
: <math>P(t/x) \vdash \exists x P</math>，要求可自由代入
:* 广义存在推广
:: <math>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>\forall</math>-int''')
: 标记任意 <math>t</math> ，有 <math>P(t/x)</math> ，可推出 <math>\forall x P</math> ，要求可自由代入
:* 广义全称推广
:: 标记任意 <math>t_1, \dots, t_n</math> ，有 <math> P(t_1/x_1, \dots, t_n/x_n)</math> ，可推出 <math>\forall x_1 \dots \forall x_n P</math> ，要求可自由代入
* 存在量词特指('''existential specification/instantiation''')/存在量词消去('''existential introduction''', '''<math>\exists</math>-elim''')
: <math>\exists x P</math> ，标记特定 <math>t</math> ，可推出 <math>P(t/x)</math> ，要求可自由代入
:* 广义存在推广
:: <math>\exists x_1 \dots \exists x_n P</math> ，标记特定 <math>t_1, \dots, t_n</math> ，可推出 <math>P(t_1/x_1, \dots, t_n/x_n) \vdash </math> ，要求可自由代入
* 等词引入
: <math>\vdash t=t</math>
* 等词消去/等项替换
: <math>P(s/x), s=t \vdash P(t/x)</math>
: <math>P(s/x), t=s \vdash P(t/x)</math>
* 同类量词排列
: <math>\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>k_1 \dots k_n</math> 是 <math>1 \dots n</math> 的一个排列且 <math>\mathsf{Q} \in \{\forall, \exists\}</math> 。
* 空约束
: 若 <math>x</math> 不在 <math>\phi</math> 中自由出现，则 <math>\forall x \phi \dashv\vdash \phi</math> ，且 <math>\exists x \phi \dashv\vdash \phi</math> 。
* 量词的分配和提取
: <math>\forall x (\phi \land \psi) \dashv\vdash \forall x \phi \land \forall x \psi</math>
: <math>\exists x (\phi \land \psi) \vdash \exists x \phi \land \exists x \psi</math>
: <math>\forall x (\phi \lor \psi) \dashv \forall x \phi \lor \forall x \psi</math>
: <math>\exists x (\phi \lor \psi) \dashv\vdash \exists x \phi \lor \exists x \psi</math>
: <math>\forall x (\phi \rightarrow \psi) \vdash \forall x \phi \rightarrow \forall x \psi</math>
: <math>\forall x (\phi \leftrightarrow \psi) \dashv\vdash \forall x \phi \leftrightarrow \forall x \psi</math>

== 元定理 ==

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

* 子集超集
: <math>\Gamma \vdash \phi</math> ，则存在有限子集 <math>\Delta</math> 使得 <math>\Delta \vdash \phi</math>
: <math>\Gamma \vdash \phi</math> ， <math>\Gamma \subseteq \Delta</math> ，则 <math>\Delta \vdash \phi</math>
* [[切消定理]]('''cut-elimination theorem''', '''Cut''')
: <math>\Gamma, \phi \vdash \psi</math> 且 <math>\Delta \vdash \phi</math> ，则 <math>\Gamma, \Delta \vdash \psi</math>
: <math>\Gamma, \phi_1, \dots \phi_m \vdash \psi</math> 且对每个 <math>i = 0, \dots, m</math> 都有 <math>\Delta \vdash \phi_i</math> ，则 <math>\Gamma, \Delta \vdash \psi</math>
* （可证关系的）传递性('''transivity''', '''Tran''')
: <math>\Gamma \vdash \phi</math> 且 <math>\phi \vdash \psi</math> ，则 <math>\Gamma \vdash \psi</math>
: <math>\chi \vdash \phi</math> 且 <math>\phi \vdash \psi</math> ，则 <math>\chi \vdash \psi</math>
* [[分离规则]]/肯定前件('''modus ponens''', '''MP''')
: <math>\Gamma \vdash \phi</math> 且 <math>\Delta \vdash \phi \rightarrow \psi</math> ，则 <math>\Gamma, \Delta \vdash \psi</math>
:* MPBC
* 否定后件('''modus tollens''', '''MT''')
: <math>\Gamma \vdash \lnot \psi</math> 且 <math>\Delta \vdash \phi \rightarrow \psi</math> ，则 <math>\Gamma, \Delta \vdash \lnot \phi</math>
:* MTBC
* [[演绎定理]]('''deduction theorem''', '''DT''')
: <math>\Gamma, \phi \vdash \psi</math> 当且仅当 <math>\Gamma \vdash \phi \rightarrow \psi</math>
* 分情况论证('''case argument''', '''CA''')
: <math>\Gamma, \phi \vdash \chi</math> 且 <math>\Delta, \psi \vdash \chi'</math> ，则 <math>\Gamma, \Delta, \phi \lor \psi \vdash \chi \lor \chi'</math>
:* 特例
:: <math>\Gamma, \phi \vdash \chi</math> 且 <math>\Delta, \psi \vdash \chi</math> ，则 <math>\Gamma, \Delta, \phi \lor \psi \vdash \chi</math>
:: <math>\Gamma, \phi \vdash \chi</math> ，则 <math>\Gamma, \phi \lor \psi \vdash \chi \lor \psi</math> ， <math>\Gamma, \psi \lor \phi \vdash \psi \lor \chi</math>
:: <math>\Gamma, \phi \vdash \chi</math> 且 <math>\Delta, \lnot \phi \vdash \chi</math> ，则 <math>\Gamma, \Delta \vdash \chi</math>
* 简单归谬律('''SRAA''')
: <math>\Gamma, \phi \vdash \lnot \phi</math> ，则 <math>\Gamma \vdash \lnot \phi</math>
: <math>\Gamma, \lnot \phi \vdash \phi</math> ，则 <math>\Gamma \vdash \phi</math>
* [[爆炸律]]('''principle of explosion''', '''ex falso [sequitur] quodlibet''', '''EFQ''', '''ex contradictione [sequitur] quodlibet''', '''ECQ''')/不一致效果('''Inconsistency Effect''', '''IE''')
: <math>\phi, \lnot \phi \vdash \psi</math>
: <math>\Gamma \vdash \phi</math> 且 <math>\Delta \vdash \lnot \phi</math> ，则 <math>\Gamma, \Delta \vdash \psi</math>
* 双条件证明（'''biconditional proof''', '''BCP'''）
: <math>\Gamma, \phi \vdash \psi</math> 且 <math>\Delta, \psi \vdash \phi</math> ，则 <math>\Gamma, \Delta \vdash \phi \leftrightarrow \psi</math>
* 等值置换('''RE''')
: <math>\Gamma \vdash \phi \leftrightarrow \psi</math> ，则 <math>\Gamma \vdash \chi(\phi/p) \rightarrow \chi(\psi/p)</math>
:* 推广
:: <math>\Gamma \vdash \phi \rightarrow \psi</math> 、 <math>\Delta \vdash \psi \rightarrow \phi</math> 且 <math>\Theta \vdash \chi(\phi/p)</math> ，则 <math>\Gamma, \Delta, \Theta \vdash \chi(\psi/p)</math>


{{证明论}}