3.3 命题演算形式系统ND

3.3命题演算形式系统ND数理逻辑基础2026年4月第3章命题演算目录CONTENTS01ND系统的组成深入了解ND系统的公理和14条推理规则。02核心定义与推演实例学习演绎、定理的定义，并通过丰富的实例掌握ND的推演方法。03ND系统的元理论探讨ND系统的合理性与完备性，理解其理论基础。01ND系统的组成SYSTEMCOMPOSITIONOFND逻辑推理·系统架构公理与基础规则ND（自然演绎）系统的推理起点非常简洁，通过基础公理与两条关于假设的核心规则，构建了一个高度贴合人类直觉的逻辑推理框架。公理模式(AxiomSchema)Γ;A⊢A任何公式都能从自身和任意前提集合中推出，构成了推理系统最基础的起点。假设引入规则在前提集合中增加一个新的假设A，并不会推翻原有的结论B，支持我们引入临时条件进行推理。假设消除规则(Elimination)分情况证明的逻辑核心：无论假设A成立与否，结论B均成立，则B必然无条件成立。贴近直觉的推理模式

ND的规则设计高度模拟了人类在日常生活和数学证明中的自然思维方式，如反证法和分情况讨论，易于理解与上手。灵活的假设管理能力

通过引入和消除假设的规则组合，系统能灵活地处理各种复杂的条件推理，在保证逻辑严密性的同时保持了证明过程的简洁性。联结词规则：∨与∧合取(Conjunction)与析取(Disjunction)的引入与消除规则01.∨引入规则(∨-Introduction)直观解释：如果命题A为真，那么无论命题B的真假，“A或者B”的命题必然为真。02.∨消除规则(∨-Elimination)直观解释：分情况证明。若A和B分别都能推出结论C，且A与B中至少有一个为真，则C必为真。∧引入规则(Introduction)当且仅当A和B两个命题同时为真时，它们的合取式“A且B”才成立。∧消除规则(Elimination)如果合取式成立，则其中任意一个支命题都必然成立，可独立拆分使用。逻辑直觉(Intuition)合取与析取规则完全符合我们日常语言中的逻辑直觉。这些规则构成了经典命题逻辑中推理系统的基础支柱。联结词规则：→与¬蕴含与否定的引入与消除1.→引入规则(→-Introduction/演绎定理)直观理解：要证明A蕴含B，可以先“假设”A成立，在这个前提下若能证明B成立，则A→B得证。2.→消除规则(→-Elimination/分离规则)直观理解：即经典的“肯定前件”推理。若前提A为真且A能推出B，则结论B必然为真。这是最常用的推理形式之一。¬引入(反证法思想)如果假设A会导致同时推出B和非B（矛盾），那么原假设A不成立。¬消除从逻辑矛盾（A和非A同时成立）中可以推出任何命题。这体现了保持一致性的重要性。推理基石这四条规则构成了经典命题逻辑推理的核心基础。掌握它们不仅能理解逻辑系统的严密性，也是学习数学证明、编程逻辑和批判性思维的必备工具。联结词规则：¬¬与↔01/双重否定规则(DoubleNegation)¬¬引入(DNIntro)

¬¬消除(DNElim)

💡核心直觉：两个连续的否定符号可以互相抵消，逻辑值保持不变。例如：“并非不是A”等同于“A”。↔引入(BiconditionalIntro)要证明两个命题等价，必须证明它们能“互相推出”，即构成逻辑上的充分必要条件。↔消除(BiconditionalElim)一个等价关系可以被拆解为两个独立的单向蕴含式，在证明过程中按需使用其中一个方向。02核心定义与推演实例DEFINITIONSANDEXAMPLES核心定义：演绎与定理ND系统中关于定理和演绎的定义如下演绎结果在ND中，如果存在序列使得Γi⊢𝐴𝑖(1≤𝑖≤𝑚)或者是公理，或者是Γ𝑗⊢𝐴𝑗(𝑗<𝑖)，或者是使用推理规则导出的,

称𝐴为Γ的演绎结果（deductiveconsequence），即Γ⊢ND𝐴

。定理若前提集合Γ是空集，即⊢A，则称公式A是ND的定理。注：严谨的演绎序列要求每一步都必须有据可依，不能随意引入未定义的前提。推演实例1：证明排中律💡证明思路解析分情况证明(ProofbyCases)排中律断言：对于任意命题A，A与非A必有一个为真。我们无法直接证明，因此采用“分情况讨论”的策略：1.假设A为真，证明结论成立；

2.假设¬A为真，证明结论也成立；

3.既然两种穷尽所有可能性的情况都能导出结论，根据“假设消除规则”，结论必然恒真。目标：⊢A∨¬A策略：分别推导A⊢A∨¬A和¬A⊢A∨¬A，再消去假设。📜形式化证明序列(ProofSequence)1.A⊢A(公理)

2.A⊢A∨¬A(∨引入规则：对步骤1左析取引入¬A)

3.¬A⊢¬A(公理)

4.¬A⊢A∨¬A(∨引入规则：对步骤3右析取引入A)

5.⊢A∨¬A(假设消除规则：结合步骤2和4，消去临时假设A和¬A)✅结论：排中律(LawofExcludedMiddle)得证。这表明在经典逻辑体系中，不存在既非真也非假的命题。推演实例2：证明德摩根律定理定义：证明逻辑等价式⊢¬(A∨B)↔¬A∧¬B，需分别证明左→右与右→左两个方向的蕴含式。证明思路(第一步)：先证左→右(⊢¬(A∨B)→(¬A∧¬B))。利用反证法：假设¬(A∨B)且A，推出矛盾得¬A；同理证¬B；最后利用合取引入规则得¬A∧¬B。证明序列(1-4)：1)¬(A∨B),A⊢A————————————————————(公理)2)¬(A∨B),A⊢A∨B———————————————————(∨引入规则1)3)¬(A∨B),A⊢¬(A∨B)————————————————(公理)4)¬(A∨B)⊢¬A——————————————————————(¬引入规则2,3)证明序列(5-7)：5)¬(A∨B)⊢¬B——————————————————————(同理可证，与步骤1-4对称)6)¬(A∨B)⊢¬A∧¬B————————————————(∧引入规则4,5)7)⊢¬(A∨B)→(¬A∧¬B)——————————(→引入规则6)注：完成左→右证明。反之右→左的证明思路类似。推演实例3：演绎等价¬A→B⊢⊣A∨B01/证明¬A→B⊢A∨B1)¬A→B,¬A⊢B(公理及蕴含消除规则)2)¬A→B,¬A⊢A∨B(析取引入规则，由1)可得)3)¬A→B,A⊢A∨B(公理及析取引入规则)4)¬A→B⊢A∨B(假设消除规则，综合2)与3))💡思路：分别假设A为假和为真，推导得出A∨B，最后消除假设。02/证明A∨B⊢¬A→BA∨B,B,¬A⊢B(公理)A∨B,B⊢¬A→B(蕴含引入)A∨B,A,¬A⊢B(矛盾消除)A∨B,A⊢¬A→B(蕴含引入)A∨B⊢A∨B(公理)A∨B⊢¬A→B(析取消去2)4)5))💡逻辑意义总结此等价关系揭示了“蕴含”与“析取”之间的转换规则。在自然演绎系统ND中，我们常利用这一性质将难以处理的蕴含式转换为更直观的析取式，反之亦然，从而简化证明路径。推演实例4：演绎等价A∧B⊢⊣¬(A→¬B)定理定义：在命题逻辑系统中，证明合取式A∧B与蕴含式的否定¬(A→¬B)是逻辑等价的。本页展示从左向右的推导：A∧B⊢¬(A→¬B)证明思路：假设前提A∧B和辅助假设A→¬B同时成立。利用逻辑消除规则推导出B和¬B，产生矛盾。根据否定引入规则，得出辅助假设为假，即¬(A→¬B)。推导步骤1-31)A∧B,A→¬B⊢A(公理及合取消除律∧E)2)A∧B,A→¬B⊢A→¬B(公理：前提引入)3)A∧B,A→¬B⊢¬B(蕴含消除律→E:由1,2推出)推导步骤4-5(结论)4)A∧B,A→¬B⊢B(公理及合取消除律∧E)5)A∧B⊢¬(A→¬B)(否定引入规则¬I:由3,4导出矛盾，否定辅助假设)注：通过矛盾法，成功证明从左至右的单向蕴含成立。推演实例5：PC公理在ND中的证明自然演绎形式系统（ND）的推演能力非常强大，足以证明命题演算形式系统（PC）的所有公理。下面展示了PC系统三条核心公理在ND中的证明思路。A1·蕴含公理⊢A→(B→A)1)A,B⊢A(公理)2)A⊢B→A(→引入规则1)

3)⊢A→(B→A)(→引入规则2)A2·蕴含分配公理⊢(A→(B→C))→((A→B)→(A→C))通过多次引入假设，交替运用蕴含消除与蕴含引入规则即可严谨得证。A3·反证公理⊢(¬A→¬B)→(B→A)引入假设并推导矛盾，配合使用否定引入与双重否定消除规则完成证明。推演能力等价性证明

上述推导表明，ND系统完全具备推导出PC系统所有公理的能力。这意味着在逻辑推演能力上，ND系统至少不弱于PC系统。核心结论

ND系统包含了PC系统的全部推演能力，且更符合人类的自然推理直觉，是更强大、灵活的逻辑推理工具。03ND系统的元理论METATHEORYOFND元理论：合理性与完备性定理3.19：ND是合理且完备的01/合理性(Soundness)如果Γ⊢A，则Γ⊨A。这意味着在ND系统中，我们通过推理规则推导出的任何结论，都在语义上是有效的。无论前提是什么，ND系统都不会让我们从真前提推导出“假”的结论，从而保证了推理工具