关于第一章和第三章内容的补充

形式化方法命题逻辑与谓词逻辑第一章与第三章核心内容补充讲义Contents讲义目录本讲义涵盖命题逻辑与谓词逻辑的核心理论体系及形式化应用实践。01命题逻辑基础概念与运算体系02命题逻辑的推理证明与范式转换03谓词逻辑的量化体系与语义分析04逻辑转换方法与形式化应用实践CHAPTER01命题逻辑基础概念与运算体系从命题的定义到复合公式的构造与求值PropositionalLogic命题的定义与基本特征命题是形式化逻辑的最小语义单元，其严格定义为"可判定真假的陈述句"——这一精确性是后续所有逻辑推理和程序验证的根基。01有且仅有一个确定真值（T或F）的陈述句，排除疑问句、祈使句及语义模糊表达。这是命题逻辑的基本要求，确保每个命题在特定解释下具有唯一确定的真值。T/F02不可再分解的最小命题单元，用p、q、r等小写字母表示，是构造复杂逻辑表达式的基石。原子命题的真值独立于其他命题，构成逻辑演算的基本对象。p·q·r03由简单命题通过逻辑联结词组合，真值完全由各子命题真值与联结词语义规则决定。常见联结词包括与、或、非、蕴含和等价，它们定义了命题之间的逻辑关系。联结词04为软件规格说明、协议验证和程序正确性证明提供严格的数学语义基础。命题逻辑是形式化方法的核心工具，广泛应用于计算机科学的理论研究与工程实践。形式化方法PropositionalConnectives五种基本命题联结词命题联结词是构造复合命题的基本工具，五种联结词构成了命题逻辑的完整运算体系。其中蕴涵运算的"前假则真"规则是初学者的常见误区。¬否定一元运算符，将命题真值取反。¬T=F，¬F=T，是唯一的一元联结词。在逻辑电路中对应NOT门，是最基础的逻辑运算单元。NEGATION·一元∧合取二元运算符，对应"并且"语义。p∧q为真当且仅当p和q同时为真。具有交换律和结合律，对应逻辑电路中的AND门。CONJUNCTION·二元∨析取二元运算符，对应可兼"或者"。p∨q为假当且仅当p和q同时为假。具有交换律和结合律，对应逻辑电路中的OR门。DISJUNCTION·二元→蕴涵p→q仅当p=T且q=F时为假。前件为假时蕴涵式恒为真，称为"空真"。这是命题逻辑中最易产生误解的联结词。IMPLICATION·空真↔等价p↔q为真当且仅当p和q真值相同，等价于双向蕴涵的组合。具有自反性、对称性和传递性，是逻辑等价关系的基础。EQUIVALENCE·双向LOGIC·FORMALSYNTAX命题公式的运算优先级运算符优先级规则确保命题公式的语义唯一性和无歧义性。在形式化规范中，优先级层次从一元运算到二元运算逐级递减，括号具有最高优先权。工程实践中推荐"宁多不少"的括号使用策略以保证可读性。¬P1·最高否定一元运算符，紧密绑定其后的命题变元或括号表达式UNARY∧P2合取二元运算符中优先级最高，体现"并且"更强的逻辑结合力AND∨P3析取优先级低于合取，p∨q∧r理解为p∨(q∧r)OR→↔P4·最低蕴涵与等价优先级最低，通常作为公式的最外层逻辑关系IMPLIES()OVERRIDE括号覆盖打破默认优先级层次，工程实践建议显式加括号消除歧义EXPLICITFORMALMETHODS·TRUTHTABLE真值表的构造与应用真值表通过穷举所有变量赋值组合来完整刻画命题公式的语义行为，是判定公式类型的终极方法。但其指数级的规模增长（n个变量对应2n行）决定了它仅适用于小规模公式，大规模验证需要借助等值演算与推理规则。构造规则：n个命题变元产生2n行赋值组合，按二进制递增排列确保不遗漏，每行计算各子公式直至最终结果判定永真式（重言式）：若公式在所有赋值下均为真，则该公式为永真式，如p∨¬p在真值表中恒为T判定矛盾式：若公式在所有赋值下均为假，则该公式为矛盾式，如p∧¬p在真值表中恒为F判定可满足式：若存在至少一种赋值使公式为真，则该公式可满足，永真式是可满足式的特例工程局限：5个变量即需32行，10个变量需1024行，因此真值表更适合教学演示和小规模验证，大规模场景需符号化方法高校课堂教学场景PROPOSITIONALLOGIC·CLASSIFICATION命题公式的分类体系命题公式按真值表行为分为永真式、矛盾式和可满足式三类，其中永真式是可满足式的特例。在形式化验证中，证明某个系统性质为永真式意味着该性质在所有可能的执行路径下都成立，这是最高级别的安全性保证。◆永真式（重言式）在所有2n种赋值下真值均为T，如p∨¬p（排中律）、p→p（自反律），代表无条件成立的逻辑真理。永真式是逻辑推理的基石，任何有效的论证都可以转化为永真式。Tautology恒真

矛盾式（永假式）在所有赋值下真值均为F，如p∧¬p（矛盾律），代表逻辑上不可能成立的命题组合。矛盾式是逻辑谬误的极端形式，任何包含矛盾式的理论系统都将面临崩溃。Contradiction恒假●可满足式至少存在一种赋值使公式为T，涵盖永真式和偶真式（contingent），是公式可被"满足"的最低条件。可满足性问题（SAT）是计算机科学的核心难题，具有广泛的实际应用价值。Satisfiable⊂集合关系永真式⊂可满足式，矛盾式与可满足式互斥；偶真式（非永真的可满足式）是实际系统性质最常见的公式类型。理解这一层次结构有助于准确判断公式在逻辑空间中的位置。Subset✓验证意义程序验证的目标通常是证明系统规范为永真式（所有执行路径都满足安全性），或证明某性质可满足（存在合法执行路径）。这一分类为软件可靠性提供了形式化的理论基础。VerificationLOGIC·EQUIVALENCE基本等值式与恒等变换基本等值式构成了命题逻辑的代数变换规则体系，是公式化简、范式转换和逻辑推理的核心工具。双重否定律¬¬p⇔p经典逻辑基本公理，但在直觉主义逻辑中不成立，体现经典与非经典逻辑的根本分歧。该等值式表明：对命题的两次否定等价于原命题本身，是逻辑证明中常用的化简手段。Axiom·公理幂等律p∧p⇔pp∨p⇔p重复的合取或析取运算可化简为单次运算，在布尔代数优化中有直接应用。幂等性意味着同一命题的多次逻辑运算不改变真值，是电路简化的理论基础。Boolean·布尔德摩根律¬(p∧q)⇔¬p∨¬q¬(p∨q)⇔¬p∧¬q否定穿透括号时联结词翻转，是逻辑表达式化简的核心规则。合取与析取在否定下互为对偶，该律在数字电路设计和程序条件优化中广泛使用。CoreRule·核心蕴涵等值式p→q⇔¬p∨q将蕴涵关系转化为析取运算，是消除蕴涵符号、范式转换的第一步。该等值式揭示了蕴涵的真值条件：仅当前件真而后件假时，蕴涵式为假。Transform·转换分配律p∧(q∨r)⇔(p∧q)∨(p∧r)p∨(q∧r)⇔(p∨q)∧(p∨r)析取对合取的分配律与代数中乘法分配律具有对称性。两种形式互为对偶，是展开复杂公式、提取公因子进行逻辑优化的关键依据。Duality·对偶Chapter02命题逻辑的推理证明与范式转换从等值演算到自然推理系统，从析取范式到主范式构造METHODOLOGY等值演算方法与推导技巧等值演算是通过逐步应用基本等值式对命题公式进行恒等变换的系统方法，每一步替换都保持公式真值不变。它是连接基础逻辑理论与实际工程应用的桥梁，在电路化简、查询优化和自动化推理等领域有直接应用价值。01演算基本流程：从原始公式出发，逐步应用等值式进行替换，每一步标注所用等值式名称，直至得到最简或目标形式02消除蕴涵与等价：用蕴涵等值式p→q⇔¬p∨q和等价等值式消除→和↔，将公式统一为仅含¬、∧、∨的基本形式03内移否定号：反复应用德摩根律将否定号从外层逐步内移至命题变元前，消除括号前的否定，得到否定范式04化简与合并：利用幂等律、吸收律、分配律等化简冗余项，如p∧(p∨q)⇔p可直接吸收，减少公式复杂度05验证技巧：演算完成后可用特殊赋值法快速检验——选取一组赋值代入原式和结果式，若真值不同则演算过程必有错误NORMALFORMS析取范式与合取范式范式是命题公式的标准化表示形式：析取范式（DNF）为合取式的析取，合取范式（CNF）为析取式的合取。CNF是SAT求解器和自动化验证工具的标准输入格式，而DNF在逻辑电路设计中有直观应用。任何公式均可转化为等价范式，但可能面临指数级膨胀。01析取范式（DNF）：形如(A₁∧B₁)∨(A₂∧B₂)∨…的结构，每个合取子句代表一种使公式为真的赋值组合∨-FORM02合取范式（CNF）：形如(A₁∨B₁)∧(A₂∨B₂)∧…的结构，每个析取子句代表一个必须满足的约束条件∧-FORM03范式存在定理：任何命题公式都存在等价的DNF和CNF形式，可通过等值演算系统性构造THEOREM04转化步骤：消除→和↔→内移否定号（德摩根律）→应用分配律展开为标准和式或积式PIPELINE05工程挑战：公式转化可能导致子句数指数级增长，如n变量异或运算的CNF需要2ⁿ⁻¹个子句，这是SAT问题NP完全性的体现2ⁿ⁻¹NORMALFORM主析取范式与主合取范式主范式具有唯一性定理保证，为判断公式等价性提供标准化方法。极小项n个变量的合取式，每个变量以原形或否定形式恰好出现一次，对应真值表中一行赋值mi极大项n个变量的析取式，每个变量以原形或否定形式恰好出现一次，与极小项互为对偶Mi主析取范式所有使公式为真的极小项的析取，唯一对应真值表中结果为T的行Σmi主合取范式所有使公式为假的极大项的合取，唯一对应真值表中结果为F的行ΠMi唯一性定理变量序确定时主范式唯一，两公式等价当且仅当主范式完全相同等价判据NaturalDeduction自然推理系统的基本推理规则自然推理系统通过一组单向推理规则模拟人类逻辑推导过程，从已知前提逐步推出结论。假言推理（MP）和拒取式（MT）是最基本的两条规则，它们与假言三段论、构造性二难等规则共同构成了命题逻辑推理的完整工具体系。01假言推理（ModusPonens）：由p和p→q推出q，最基本的"肯定前件推肯定后件"规则，几乎每个证明都会用到MP02拒取式（ModusTollens）：由¬q和p→q推出¬p，通过否定后件来否定前件，是反证法的核心推理步骤MT03假言三段论（HypotheticalSyllogism）：由p→q和q→r推出p→r，实现蕴涵关系的传递链构造，可串联多个推理步骤HS04析取三段论：由¬p和p∨q推出q，在已知一个析取支为假时确定另一个析取支为真DS05构造性二难：由p→r、q→r和p∨q推出r，无论哪种情况都能得到相同结论，是分情况讨论的形式化表达CDProofMethodology推理证明的方法论体系三大方法各有侧重——直接证明正向推导，间接证明利用逆否等价，归谬法假设否定推导矛盾——在复杂证明中经常组合使用。直接证明法列出所有前提，按推理规则逐步推导中间结论，最终到达目标结论，每一步标注所用规则和依据的前提编号正向推导间接证明法利用p→q⇔¬q→¬p的等值关系，将原命题转化为逆否命题进行证明，适用于直接推导困难的情形逆否等价归谬法假设目标结论的否定为附加前提，若能推导出矛盾形式，则证明原结论必然成立推导矛盾附加前提法要证A→B，可将A作为附加前提加入已知条件，只需推导出B即可完成证明（CP规则）CP规则策略选择优先尝试直接证明，推导受阻时考虑归谬法或间接法，复杂定理通常需要多种方法嵌套使用嵌套组合CHAPTER03谓词逻辑的量化体系与语义分析从命题逻辑的局限到谓词逻辑的表达力飞跃PropositionalvsPredicateLogic命题逻辑的局限与谓词逻辑的引入命题逻辑将每个命题视为不可分割的原子单元，无法分析命题内部的谓词-个体结构，因此无法表达量化关系和进行涉及个体性质的推理。谓词逻辑通过引入谓词、个体常元/变元和量化器，使逻辑系统能够深入到命题内部结构，表达力得到本质提升。01原子性局限命题逻辑将命题视为不可再分的整体，无法识别不同命题之间的共享语义成分，如"苏格拉底"和"人"的概念关联。02三段论失效"所有人都会死"+"苏格拉底是人"→"苏格拉底会死"，在命题逻辑中无法验证有效性，三个命题被编码为无关原子p,q,r。03无法表达量化"存在一个素数是偶数"、"所有程序都可以被优化"等涉及"存在"和"所有"的陈述超出了命题逻辑的表达能力。04谓词逻辑方案引入谓词（描述性质和关系）、个体（表示对象）和量化器（表达"所有"与"存在"），深入命题内部结构。谓词逻辑通过分析主词与谓词的关系，将简单命题分解为个体与性质的复合结构，从而揭示传统三段论的有效性基础，使逻辑推理从表层符号操作深入到语义内容分析。05表达力层级谓词逻辑严格强于命题逻辑——命题逻辑的所有内容都可以在谓词逻辑中表达，反之则不成立。这一层级差异体现在：谓词逻辑能够处理无穷域上的推理，支持数学归纳法等形式化证明，为计算机科学、人工智能和数学基础提供了不可或缺的逻辑工具。PredicateLogic·Fundamentals个体、谓词与命题函数谓词逻辑的三个基础构件是个体、谓词和命题函数。命题函数本身不具有确定真值，必须通过赋值或量化才能转化为命题。个体常元表示论域中确定的具体对象，用小写字母a,b,c或具名常量表示，在推理过程中取值保持不变s,0个体变元表示论域中任意对象，取值范围由论域决定，是量化操作的目标，可被全称量词或存在量词约束x,y,z一元谓词描述单个个体的性质或特征，谓词名用大写字母标识，将个体映射到真值集合M(x)多元谓词描述多个个体之间的关系，n元谓词对应n个个体参数，用于表达对象间的复杂关联G(x,y)命题函数含自由变元的谓词表达式，当变元x取定值a时，P(a)才成为具有确定真值的命题P(x)→P(a)PredicateLogic·Quantifiers全称量词与存在量词全称量词（∀）和存在量词（∃）是谓词逻辑的核心扩展，使逻辑系统能够表达"所有"和"存在"两类量化关系。全称量词通常与蕴涵搭配表达"所有A都是B"的全称命题，存在量词通常与合取搭配表达"存在A且B"的存在命题，这种搭配模式是正确形式化自然语言的关键。全称量词∀xP(x)表示论域D中每个个体都满足谓词P，其语义等价于有限合取P(d₁)∧P(d₂)∧…∧P(dₙ)，体现"所有"的完全覆盖性。Universal∀存在量词∃xP(x)表示论域D中至少存在一个个体满足P，其语义等价于有限析取P(d₁)∨P(d₂)∨…∨P(dₙ)，表达"存在"的部分满足性。Existential∃量词辖域量词的作用范围由紧随其后的括号或公式确定，如∀x(P(x)→Q(x))中(P(x)→Q(x))为辖域。辖域决定量词约束变元的有效范围。Scope{}标准搭配全称命题采用∀x(P→Q)表达"所有P都是Q"，存在命题采用∃x(P∧Q)表达"存在P且Q"。蕴涵与合取的区分选择是形式化的关键技巧。Pattern→∧常见错误∀x(P∧Q)意为"所有个体同时满足P和Q"而非"所有P都是Q"；∃x(P→Q)通常不是正确形式，因空真问题导致表达力丧失。WarningFORMALMETHODS自然语言的谓词逻辑形式化自然语言到谓词逻辑的翻译是形式化方法的核心技能，需要依次确定论域、识别谓词、选择量词和组装公式四个步骤。同一语句在不同论域下可能有不同的形式化表达。01确定论域明确讨论对象的范围，如"所有人"、"所有自然数"或"所有程序"，论域的选择决定后续谓词设计的复杂度论域02识别谓词从句子中提取性质描述（一元谓词）和关系描述（多元谓词），如"学生"→S(x)、"选课"→C(x,y)谓词03确定量词识别"所有/每一个"对应∀、"存在/某个"对应∃，注意嵌套量词的顺序直接影响语义量词04组装公式按量词搭配规则组合——全称用→、存在用∧，注意括号标注辖域，确保结构与语义一致辖域05论域敏感性"所有学生都及格"在论域=学生时为∀xP(x)，论域=所有人时为∀x(S(x)→P(x))敏感性PredicateLogic·Semantics谓词公式的语义与解释谓词逻辑的语义通过"解释"赋予公式确定的真值，包括论域指定、常元映射和谓词关系定义三个部分。01解释的构成—一个解释I=(D,·)由非空论域D和解释函数·组成，D规定讨论范围，·将符号映射为D中的具体语义对象I=(D,·)02常元解释—将每个个体常元映射为D中的一个确定元素，如常元a在解释I下映射为D中的某个特定对象a→d∈D03谓词解释—将n元谓词映射为D上的n元关系，即Dⁿ的子集，如二元谓词L(x,y)在D={1,2,3}下可解释为"小于"关系Dⁿ子集04公式求值—在给定解释I和变量赋值σ下，递归计算项的值、原子公式的真值，再按联结词和量词规则逐层计算复合公式的真值递归求值05模型与可满足性—解释I使公式φ为真时称I为φ的模型，存在模型的公式为可满足式，所有解释下均为真的公式为有效式I⊨φPREDICATELOGIC·EQUIVALENCES谓词逻辑的核心等值式谓词逻辑的等值式体系在命题逻辑基础上扩展了量词变换规则，其中量词否定等值式和量词辖域变换规则是最核心的两组，是化为前束范式与构建定理证明器的理论基础。01·量词否定¬∀xP(x)⇔∃x¬P(x)，¬∃xP(x)⇔∀x¬P(x)：'并非所有都'等价于'存在不'，'不存在'等价于'所有都不'。量词德摩根律02·辖域收缩∀x(A(x)∧B)⇔∀xA(x)∧B，当B不含自由变元x时，可将不受量词约束的子公式移出量词辖域。B不含自由变元03·辖域扩张∃x(A(x)∨B)⇔∃xA(x)∨B，与收缩规则对偶，用于简化嵌套量词结构。收缩规则对偶04·量词分配∀x(A∧B)⇔∀xA∧∀xB成立，但∀x(A∨B)⇔∀xA∨∀xB不成立，后者蕴含前者但不可逆。∧可分配·∨不可逆05蕴涵中的量词：∀x(A(x)→B)⇔∃xA(x)→B（B不含x），全称量词在蕴涵前件中转化为存在量词，这是初学者常犯错误的地方。PredicateLogic·NormalForm前束范式及其构造方法前束范式将所有量词集中到公式最前端，形成"量词前缀+无量词母式"的标准结构，是谓词逻辑推理和自动化证明的标准输入格式。01定义形如Q₁x₁Q₂x₂…QₙxₙM的公式，其中Qi为∀或∃，M为不含量词的母式（矩阵），所有量词辖域延伸至公式末尾。02消除联结词去除→和↔联结词，用¬、∧、∨替代，再运用德摩根律将否定号内移至原子公式前。03量词前移运用量词辖域收缩与扩张规则，将量词逐步向公式前端移动，注意移动过程中量词可能的翻转（∀变∃或反之）。04变元改名当两个量词约束同名变元导致辖域冲突时，使用约束变元改名规则消除歧义，如∀xP(x)∨∀xQ(x)改为∀xP(x)∨∀yQ(y)。05存在性与非唯一性任何谓词公式都存在等价的前束范式，但前束范式不唯一——量词排列顺序和变元命名可有不同的等价选择。PREDICATELOGIC·NATURALDEDUCTION量词推理规则：全称指定与存在指定量词推理规则是谓词逻辑自然推理系统的核心扩展，全称指定（UI）从全称命题推导特定实例，存在指定（EI）从存在命题引入见证元素。EI规则要求引入的常元必须是全新的，这一限制条件是保证推理有效性的关键约束。01全称指定（UI/US）：由∀xA(x)可推出A(c)，其中c为论域中任意个体常元或变元，体现「既然所有都满足，特定的也满足」。∀→实例02UI使用要点：c可以是任意常元或变元，不要求是新的；可多次应用UI规则对同一全称公式取不同的实例。c任意03存在指定（EI/ES）：由∃xA(x)可推出A(c)，其中c必须是为该存在命题新引入的常元（Skolem常元），之前未在证明中出现。∃→见证04EI的关键限制：c必须是全新常元，若c已在上下文中出现则可能引入错误假设——如从∃xP(x)和∃xQ(x)不能直接推出P(c)∧Q(c)。c全新05应用顺序原则：同一证明中应先应用EI再应用UI，因为EI引入的新常元可被后续UI使用，反之则可能违反EI的新鲜性要求。EI→UIQUANTIFIERINFERENCE量词推理规则：全称推广与存在推广全称推广从任意个体推导全称命题，存在推广从特定个体推导存在命题；UG条件最严格，四规则配合构成完整推理工具。全称推广UG由A(c)推出∀xA(x)，c必须是任意选取的个体，不能由EI引入。这是量词推理中最核心的推广规则。A(c)→∀xA(x)UG限制条件c不能出现在前提中作为特定常元，不能是EI产物，否则以偏概全。严格限制确保推理的有效性。防止以偏概全存在推广EG由A(c)推出∃xA(x)，c可为任意常元，无特殊限制，最安全。只要找到一个实例即可断言存在。A(c)→∃xA(x)配合策略EI消存在量词→UI消全称量词→命题推理→UG或EG恢复量词。四规则形成完整的推理链条。EI→UI→推理→UG/EG典型证明模式∀x(P→Q),∃xP⊢∃xQ：EI得P(a)，UI得P(a)→Q(a)，MP得Q(a)，EG完成。展示完整的演绎过程。EI→UI→MP→EGPredicateLogic谓词逻辑的综合推理证明谓词逻辑的综合推理证明将量词推理规则与命题逻辑推理方法有机结合，通过"消量词→命题推理→恢复量词"的三段式流程完成证明。规则应用的顺序至关重要：EI先于UI、命题推理居中、UG/EG收尾，违反顺序可能导致推理无效。01直接证明流程列出前提→按EI先于UI的顺序消去量词→命题逻辑推导（MP、MT等）→用UG或EG恢复量词→得到结论02归谬法应用假设结论否定为附加前提，利用量词否定等值式展开（¬∀xP(x)→∃x¬P(x)），推导至矛盾03间接证明法将目标结论取逆否，如证∀x(P(x)→Q(x))可证∀x(¬Q(x)→¬P(x))，逆否方向推理路径更清晰04规则顺序铁律同一证明中EI必须在UI之前应用（对同一常元），否则UI选取的常元可能不是EI所指个体，推理无效05常见错误案例∃xP(x)与∃xQ(x)用同一常元c做EI得P(c)∧Q(c)是错误的——两个存在量词可能指代不同个体，须用不同常元CorePipeline消量词→命题推理→恢复量词EI→UI→MP/MT→UG/EGChapter04逻辑转换方法与形式化应用实践命题逻辑与谓词逻辑的互转技巧及在软件验证中的落地应用LogicTransformation命题逻辑与谓词逻辑的互转方法在有限论域下，谓词逻辑公式可系统展开为命题逻辑公式：全称量词展开为合取、存在量词展开为析取。反之，当命题逻辑的原子性假设不再适用时，需识别内部的谓词结构并引入量化器。谓词→命题展开论域D={d₁,…,dₙ}时，全称量词展开为合取、存在量词展开为析取，量词被完全消除。∀xP(x)⇔P(d₁)∧…∧P(dₙ)多量词展开顺序∀x∃yR(x,y)在D={a,b}下先展∀得∃yR(a,y)∧∃yR(b,y)，再展∃完成。D={a,b}命题→谓词升级多个命题共享内部结构时，引入谓词和个体进行抽象。共享谓词量化器引入判据出现"所有/每个/任意"引入∀，出现"存在/某个"引入∃。∀·∃有限模型检测无限状态系统转化为有限论域公式，交由SAT求解器自动验证。SATSolverPredicateLogic约束变元、自由变元与改名规则谓词公式中的变元分为约束变元（被量词绑定）和自由变元（未被量化），二者的区分直接影响公式的语义和真值。约束变元改名规则保证在不改变公式含义的前提下消除命名冲突，是进行前束范式转换和公式等价变换的必要技术。约束变元出现在量词辖域内且与量词同名的变元，如∀xP(x)中的x，取值由量词决定，不代表特定对象。∀xP(x)自由变元未被任何量词约束的变元，如P(x,y)中y自由，公式真值依赖外部赋值，类似程序中的输入参数。Input改名规则∀xP(x)⇔∀yP(x/y)，新变元y不能是公式中已有的自由变元或其他约束变元，避免变量捕获。x→y操作细节替换须同时修改量词变元和辖域内所有同名约束出现，如∀x(P(x)∧Q(x,y))改为∀z(P(z)∧Q(z,y))。x→z错误警示∀x∃xP(x)中∃x遮蔽外层∀x，改名时不能改为内层已有变元，须先确认作用域层级再操作。ScopeFormalSpecification谓词逻辑在软件规范说明中的应用谓词逻辑为软件系统提供精确、无歧义的规范描述能力，通过前置条件、后置条件和不变式的三元组结构，可以严格定义程序的正确性行为。01前置条件（Precondition）—用谓词公式描述程序执行前输入必须满足的条件，如排序程序的输入为「长度n≥1的整型数组」02后置条件（Postcondition）—用谓词公式描述程序执行后输出必须满足的性质，如排序结果需满足∀i(1≤i<n→B[i]≤B[i+1])∧Permutation(A,B)03循环不变式（LoopInvariant）—用谓词公式描述循环每次迭代前后都保持为真的性质，是证明循环正确性的关键中间断言04Hoare三元组{P}S{Q}—将前置条件P、程序语句S和后置条件Q组合为形式化规范，表示「若P成立且S终止，则执行S后Q成立」05实例——二分查找规范—Precondition为数组有序∀i(0≤i<n-1→A[i]≤A[i+1])，Postcondition为(key∈A→A[result]=key)∧(key∉A→result=-1)PredicateLogic×Database谓词逻辑在