3.2 命题演算形式系统PC

3.2命题演算形式系统PC计算机科学中的数理逻辑2026年4月第3章命题演算目录CONTENTS01PC系统的组成详细解析PC系统的语言构成和推理规则。02PC中的推理学习证明、定理、演绎等核心概念，并通过实例掌握推理方法。03PC的语义探讨PC系统的语义解释，建立语法与语义的联系。04关于PC的重要元定理深入理解合理性、一致性、完备性和紧致性等元理论性质。01PC系统的组成SYSTEMCOMPOSITIONOFPC形式系统·核心架构语言部分：符号与公式什么是PC的语言？PC（命题演算形式系统）的语言是一种严格定义的形式语言，不包含歧义。它的构成极其简洁，仅由两部分组成：语言部分和推理部分。语言部分基本符号集定义为：∑={(,),¬,→,p₁,p₂,p₃,⋯}公式的定义如下：推理部分：公理与规则PC系统的推理能力由三条公理模式和一条推理规则赋予，它们共同构成了形式推演的基石。A1·肯定后件律A→(B→A)这条公理表明，如果A为真，那么任何公式B都能推出A，体现了蕴含的单调性。A2·蕴含词分配律(A→(B→C))→((A→B)→(A→C))这条公理是蕴含词的分配律，是进行复杂逻辑推演的核心工具。A3·换位律(¬A→¬B)→(B→A)这条公理体现了逆否命题与原命题逻辑等价的思想，是反证法的基础。推理规则：分离规则(modusponens,rₘₚ)

若公式A和公式A→B均成立，则可推出公式B成立。这是PC系统唯一的推理规则，是驱动所有证明的“核心引擎”。02PC中的推理REASONINGINPC基本定义：证明、定理与演绎形式推理的核心概念：1.证明(Proof)一个公式序列，其中每个公式要么是公理，要么是由前面的公式通过分离规则得到。2.定理(Theorem)如果一个公式A存在一个证明，则称A为定理，记作⊢ₚcA。3.演绎(Deduction)在证明的基础上，允许使用一个额外的公式集Γ作为前提进行推导。4.演绎结果(Consequence)若公式A存在以Γ为前提的演绎，则称A是Γ的演绎结果，记作Γ⊢ₚcA。注：这些定义构成了命题演算（PC）中逻辑推导的基础，区分了从公理出发和从假设出发的不同推导模式。推理示例：证明A→A是定理💡证明思路这是命题演算形式系统PC中最基础的定理之一，虽然直觉上显而易见，但在形式系统中必须严格遵循公理和推理规则。我们的目标是构造一个有限的公式序列，使得序列的最后一项恰好是公式A→A。为此，我们巧妙地组合使用公理A1和公理A2，并两次应用分离规则(ModusPonens,rₘₚ)来完成推导。🎯待证目标：⊢ₚcA→A证明工具：公理A1、公理A2、分离规则(rₘₚ)📝证明序列(ProofSequence)1.(A→((A→A)→A))→((A→(A→A))→(A→A))(公理A2)2.A→((A→A)→A)(公理A1)3.(A→(A→A))→(A→A)(对1,2应用分离规则rₘₚ)4.A→(A→A)(公理A1)5.A→A(对3,4应用分离规则rₘₚ)✅结论：公式序列最后一项即为目标公式，因此定理A→A在PC中得证。推理示例：证明⊢ₚc¬B→(B→A)证明：证明公式¬B→(B→A)是命题演算形式系统PC的定理。其逻辑含义为：从一个假的前提（矛盾）可以推导出任何结论。证明思路：该证明严格遵循PC的推理规则，巧妙结合公理A1、A2、A3，并多次应用分离规则推导出最终结论，完整展示了PC处理逻辑否定与蕴含关系的能力。证明序列(Step1-4)：1.¬B→(¬A→¬B)——公理A12.(¬A→¬B)→(B→A)——公理A33.((¬A→¬B)→(B→A))→(¬B→((¬A→¬B)→(B→A)))——公理A14.¬B→((¬A→¬B)→(B→A))——分离规则rₘₚ(2,3)证明序列(Step5-7)：5.(¬B→(¬A→¬B)→(B→A))→((¬B→(¬A→¬B))→(¬B→(B→A)))——公理A26.(¬B→(¬A→¬B))→(¬B→(B→A))——分离规则rₘₚ(4,5)7.¬B→(B→A)——分离规则rₘₚ(1,6)（得证）03PC的语义SEMANTICSOFPC语法与语义的初步联系01/公理的永真性PC的语义：联结词意义的规定、真值指派、命题真值意义的规定、永真式、逻辑等价、逻辑蕴涵的概念PC的三条公理A1,A2,A3都是永真式(tautology)。无论其中的命题变元被赋予什么真值，整个公式的真值永远为真。这一性质至关重要，它保证了我们推理的出发点是绝对可靠的，为整个演绎系统奠定了坚实的逻辑基础。02/分离规则的保真性分离规则(ModusPonens,MP)具有保真性(truth-preserving)。语义上，如果前提A和A→B都为真，那么结论B也必然为真。这意味着我们的推理过程在逻辑上是严密的，不会从真的前提推导出假的结论。💡重要推论：公理的永真性+分离规则的保真性➔PC系统中推导出的任何定理，都必然是逻辑上的永真式。04关于PC的重要元定理METATHEOREMSOFPC基本元定理：合理性与一致性PC系统的基石：元理论性质命题演算形式系统PC是构建经典逻辑大厦的基石。它通过有限的公理模式和推理规则，定义了从前提到结论的语法推导关系。对PC的元理论分析，关注系统本身的可靠性与完备性，旨在回答“系统推导是否可信？”与“系统能力是否足够？”的根本问题。形式系统的核心追求一个理想的形式系统应当兼具“一致性”（不自相矛盾）与“完全性”（能刻画所有真命题）。然而，PC系统的元定理揭示了：它虽可靠且无矛盾，但在表达力上存在局限性。1.合理性定理(Soundness)若Γ⊢A，则Γ⊨A。语法上可推导的结论，在语义上必然为真。这保证了PC系统的推导不会产生任何“逻辑错误”的结论。2.PC的一致性(Consistency)不存在公式A，使得A和¬A同时是PC的定理。这确保了系统内部的逻辑无矛盾性，是所有形式系统必须满足的底线要求。3.PC的不完全性(Incompleteness)存在公式A(如单一命题变元p₁)，使得A和¬A都不是PC的定理。这说明PC的定理集是不完备的，无法仅凭系统内部公理判定所有命题的真假。完备性定理(Completeness)▍定理定义：PC系统的完备性PC是完备的(complete)，即对任意公式集Γ和公式A，若Γ⊨A（语义有效），则Γ⊢A（语法可证）。特别地，任何永真式都是PC的定理。▍证明思路：反证法假设Γ├A不成立，导出矛盾（1）Γ不能演绎出A，则Γ

{┐A}仍一致（引理3.1)（2）一致的公式集必可满足（3）找出同时弄真Γ中所有公式和┐A的指派，与Γ╞A矛盾怎样找一致公式集的弄真指派（1）先将公式集扩充至一致、完全（引理3.2)（2）建立公式到{0,1}的映射，使扩充后公式集中的所有公式为真，其他公式一律为假（3）证明该映射与联结词不矛盾（引理3.3、3.4）紧致性定理(Compactness)定义与定理定义：形式系统FS具有紧致性，如果对FS的任一公式集Γ满足：若Γ的所有有穷子集都是可满足的，那么Γ本身也是可满足的。核心定理：经典命题演算形式系统PC)具有紧致性。证明思路：反证法+完备性定理将“可满足性”转化为“一致性”问题，利用有限性导出矛盾。1.