4.2 一阶语言与一阶逻辑

4.2一阶谓词演算形式系统FC计算机科学中的数理逻辑2026年4月第4章一阶谓词演算目录CONTENTS01一阶语言学习一阶语言的符号表、项和公式的严格定义。02一阶逻辑掌握一阶逻辑系统FC的公理和推理规则。01一阶语言FIRST-ORDERLANGUAGE一阶逻辑·形式化语言一阶语言的符号表一阶谓词演算形式系统的语言也称一阶语言(first-orderlanguages)，它的符号表组成如下：个体变元v₁,v₂,v₃,⋯表示不确定的个体个体常元a₁,a₂,a₃,⋯表示确定的个体函词谓词逻辑符号¬,→,∀,(,)包括联结词、量词和辅助符号注：这些符号共同构成了书写一阶逻辑公式的字母表，缺一不可。项与公式的定义从符号到表达式的构建规则01/项(Term)由变元、常元、函词组成的表达式，代表个体域中的一个具体个体对象。基础条款：单个的变元（如x,y）和常元（如a,0）是项。归纳条款：如果t₁,t₂,...,tₙ是项，且f⁽ⁿ⁾是一个n元函词，那么f⁽ⁿ⁾(t₁,t₂,...,tₙ)也是项。终极条款：除有限次使用（1），（2）条款可确认为项的符号串外，没有别的东西是项。02/公式基础条款：对任意正整数n，如果t1,…，tn为项，那么P(n)t1t2…tn为公式，并称之为原子公式。归纳条款：如果A，B为公式，那么（┐A）,（A→B）,（

vA）（v为任一变元）均为公式。终极条款：除有限次使用（1），（2）条款可确认为公式的符号串外，没有别的东西是公式。重要语法概念(I)理解公式内部结构的关键辖域(Scope)量词后面受其管辖的最小公式部分。例如，∀v(A→B)中∀v的辖域是A→B。自由与约束变元变元的出现受量词约束则为约束变元，否则为自由变元。同一变元可在公式中既有自由又有约束出现。可代入性(Substitutable)称项t是对A中自由变元v可代入

(substitutable)的，如果A中v的任何自由出现都不在

u、u的辖域内，这里u是t中任一自由变元。逻辑正确性的基石

这些概念是保证代入操作合法性、避免逻辑错误的基础，也是构建严谨证明体系的前提。公式分析的核心工具

在一阶逻辑中，准确识别辖域与变元状态是分析公式语义、判定公式性质的必要步骤。重要语法概念(II)其他关键语法定义除了基本的公式定义外，在进行逻辑推演、公式变形以及定理证明的过程中，我们还需要熟练掌握以下几个核心语法概念。1.代入(Substitution)将公式A中自由变元v的所有出现替换为项t的过程。代入操作在逻辑推演中常用于实例化一般性命题。2.子公式(Subformula)一个公式中包含的、本身也是公式的连续部分。例如在公式(A∧B)→C中，A、B、C和(A∧B)都是其子公式。3.全称化(Generalization)在公式A前添加全称量词∀v，约束其自由变元v的过程。若对公式中的所有自由变元进行全称化，得到的公式被称为“全称封闭式”。02一阶逻辑FIRST-ORDERLOGIC一阶逻辑公理系统FC一阶逻辑系统FC下列公理模式及其所有全称化，这里A，B，C为FC的任意公式，v为任意变元，t为任意项。AX1&AX2AX3·全称分配律AX4&推理规则公理模式的特性

这里列出的均为“公理模式”而非单一公理，每一条都代表了一类结构相同的公式，保证了系统具有足够的表达能力来生成所有必要的逻辑公式。推理的基石

FC系统仅使用分离规则作为唯一的推理规则，配合上述四组公理，足以构建出强大的一阶逻辑系统，体现了公理化方法的简洁性与严谨性。FC定理证明示例(1)目标：证明⊢A→┐v┐A✅证明序列如下：

目标：证明⊢∀vA→A✅证明：由于项𝑣对𝐴中自由变元𝑣总是可代入的，∀vA→Avv为公理，而Avv即𝐴。因此∀vA→A。

FC重要元定理(I)揭示系统性质的关键逻辑工具01/全称推广规则(Generalization)如果⊢A，那么⊢∀vA这条规则建立了“定理”与“全称命题”之间的推导关系。直观上理解：如果一个公式A不依赖任何前提，本身就是定理，那么对于任意变元v，A对所有对象v都成立。注：该规则仅适用于A本身是定理的情况，不可随意用于依赖前提的推导中，否则会导致逻辑谬误。02/演绎定理(DeductionTheorem)Γ;A⊢B⇔Γ⊢A→B这是一阶逻辑中最重要的元定理之一，它将“在假设A下推出B”转化为“证明蕴含式A→B”，是证明复杂逻辑结论的核心手段。💡定理的核心价值这两个元定理共同构建了一阶逻辑的证明论基础：全称推广规则解决了“一般性”的断言问题，而演绎定理则解决了“条件推导”的简化问题，两者结合让我们可以高效地处理复杂的数学证明。FC重要元定理(II)实用的导出规则：扩展形式推理的工具箱01/HS导出规则(假言三段论){A→B,B→C}⊢A→C这条规则允许我们像串联电路一样，将两个蕴含式的逻辑链条连接起来，推导出一个新的蕴含式。它是传递性在逻辑系统中的直接体现，在长推理链中非常实用。02/反证规则(ReductioadAbsurdum)如果在前提集合Γ中加入假设A会导致逻辑矛盾（即Γ∪