Subformula Property

定义 Definition

子公式性质：在证明论（尤其是序列演算 sequent calculus）中，指一种“良好行为”性质——若某个公式可被证明，则存在一个证明，其中出现的每个公式都是结论（或前提与结论）中某个公式的子公式。它常用于说明证明具有“分析性”（analytic），并支持一致性、可判定性或切消去（cut-elimination）等结果。
（在不同系统/表述下，子公式性质的精确范围可能略有差异。）

发音 Pronunciation (IPA)

/ˌsʌbˈfɔːrmjʊlə ˈprɑːpərti/

例句 Examples

The subformula property helps keep proofs focused on the goal.
子公式性质有助于让证明始终聚焦于目标公式。

In sequent calculus, cut-elimination often implies the subformula property, ensuring that no “new” formulas are introduced beyond those already present in the statement being proved.
在序列演算中，切消去通常蕴含子公式性质，从而保证证明过程中不会引入超出待证陈述之外的“新”公式。

词源 Etymology

sub-（“下、次级、在……之下”）+ formula（“公式/形式化表达”）构成 subformula（“子公式”）；property 来自拉丁语 proprietas，意为“性质/特性”。合起来表示“关于子公式的性质”：证明中出现的公式受结论（及相关前提）所“约束”。

相关词 Related Words

• Analytic
• Cut-Elimination
• Sequent
• Sequent Calculus
• Normalization
• Proof Theory
• Gentzen System
• Consistency

文学与经典著作 Literary Works

• Gerhard Gentzen, Investigations into Logical Deduction（提出与序列演算、切消去相关的核心思想，常与子公式性质一起讨论）
• Jean-Yves Girard, Proof Theory and Logical Complexity（证明论经典，涉及分析性与相关性质）
• S. C. Kleene, Introduction to Metamathematics（元数学/证明论入门经典，涵盖相关主题）
• A. S. Troelstra & H. Schwichtenberg, Basic Proof Theory（系统讲解切消去、规范化与子公式性质等）
• J.-P. van Benthem, Logic in Games（虽非专门讨论该性质，但涉及证明与逻辑结构的分析性视角）