Skip to content

推理策略

Derivation chain position: Layer 2 — Scientific Ontology Propositional Operators → [this document] → Formalization Methodology → ...

本文档定义知识类型和推理策略。每种策略是 ↝（软蕴含）的微观结构还原。 依赖 03-propositional-operators.md 的算子定义和 ↝ 的引入。

本文档不涉及因子图或 BP — 这些属于 Layer 3（计算方法）。

Status: Target design

1. 知识类型

Gaia 中有三种基础知识对象类型。Claim 是唯一携带概率并参与推理计算的类型。

类型 先验 π 参与推理 角色
Claim（主张） 有 是 可证命题；唯一携带真值的类型
Setting（背景设定） 无 否 结构性前提，提供背景上下文
Question（问题） 无 否 开放性探索，动机性前提

关于 Template（模板）。 Template 是教学概念，不是 IR 层的独立 KnowledgeType：含自由变量的命题模式编译为 Claim with parameters=[...]（v0.5 IR 的"全称 claim"形态），由 deduction Strategy 实例化为封闭 claim。代码侧的实际枚举见 ../gaia-ir/02-gaia-ir.md §1.2 的 6 类 KnowledgeType（claim / note / composition / setting / question / context），其中 note / composition / context 是 v0.5 才补齐的非概率类型。

1.1 Claim（主张）

可判真的命题。携带先验概率 π ∈ (0,1)，参与概率推理。

Claim 是 Gaia 推理系统的核心承载对象 — 只有 Claim 拥有置信度（belief），只有 Claim 之间的关系参与 Bayes 推理。所有不确定性推理最终都发生在 Claim 之间。

示例： - "在月球真空中，羽毛和锤子以相同速率下落。" - "该样本在 90 K 以下表现出超导性。"

1.2 Setting（背景设定）

上下文假设。不携带先验，不参与概率推理。

Setting 为研究提供背景信息 — 研究现状、动机、已知的未解决挑战、近似方法或理论框架。Setting 可以作为推理的结构性前提参与命题网络拓扑（提供上下文），但不产生或接收概率更新。

示例： - 某个领域的研究现状 - 一组实验的动机和出发点

1.3 Question（问题）

开放探究。不携带先验，不参与概率推理。

Question 表达待研究的方向或未解决的科学问题。它可以作为推理的驱动性前提参与命题网络结构，但不参与概率计算。

示例： - 未解决的科学问题 - 后续调查目标

1.4 Template 作为 Claim with parameters

理论上的"Template"——含自由变量的命题模式——在 Gaia IR 中不是独立类型，而是 Claim(parameters=[...])（v0.5 IR 的"全称 claim"形态）。Template 的核心作用仍然是桥梁：将参数化命题实例化为具体的封闭 Claim，使其获得概率语义并参与推理。

示例： - falls_at_rate(x, medium)（参数化的物理定律） - "{method} can be applied in this {context}"（带变量的判断）

Template 到 Claim 的实例化是严格蕴含 → 的特例（确定性），由 deduction Strategy 承载（p=1.0），不需要 review 即可升格。

第一阶量化结构在 v0.5 已经有具体编程语言实现：authoring 层的 gaia.engine.lang.formula（Forall / Exists / PredicateSymbol / UserPredicate / Term）以 AST 形式表达 Template，propositional 化简则由 gaia.engine.ir.logic 完成；详见 ../gaia-lang/predicate-logic.md。

2. 推理策略：↝ 的微观结构

中心论点

在 03-propositional-operators.md 中，我们定义了软蕴含 ↝ 并指出：

↝ 是对一个未展开的严格约束子网络的摘要。

本节的核心任务是展示这一点如何在具体推理模式中实现。每一种推理策略都是一个标准展开模板 — 它将宏观的 ↝ 链接分解为一个由严格算子 {¬, ∧, →, ↔, ⊗} 和中间命题构成的命题网络。中间命题承载不确定的先验 π，而严格算子本身不含自由参数。

推理策略的三个层面：

  1. 宏观视图（macro view）： 一条 ↝ 链接的方向和含义
  2. 微观结构（micro-structure）： 展开后的命题网络（严格算子 + 中间命题 + 先验）
  3. Bayes 推导（derivation）： 从微观结构出发，用 Bayes 定律推导出宏观 ↝ 的有效统计量 (p₁, p₂)

以下逐一给出九种推理策略的完整描述。

2.1 演绎（Deduction）

宏观视图： Premises ↝ Conclusion，推理可靠性 p₁ = 1。

作者声明此步为确定性推导 — 前提成立则结论必然成立。这是三段论 modus ponens 的直接表达。

微观结构：

A₁ ─┐
A₂ ─┤  ∧
 ⋮  ├───→ M ──→ C
Aₖ ─┘      (严格蕴含)
  • M = A₁ ∧ A₂ ∧ ... ∧ Aₖ（前提合取，确定性）
  • M → C（严格蕴含，P(M ∧ ¬C) = 0）

所有算子都是严格的，没有中间命题承载不确定先验。不确定性完全来自各前提 Aᵢ 的先验 π(Aᵢ)。

Bayes 推导：

考虑结论 C 在给定证据下的后验。

当 M = 1 时（所有前提成立）：

由严格蕴含 M → C，P(C=0 | M=1) = 0，因此：

P(C=1 | M=1) = 1

当 M = 0 时（至少一个前提不成立）：

M → C 不约束 M=0 的情况（参见 03-propositional-operators.md §2.1：M 为假时 C 的真值不受此蕴含关系限制）。C 回退到其先验，或由其他推理路径决定：

P(C=0 | M=0) = π(¬C)（如果没有其他推理路径支持 C）

这里要区分两层：

  • 局域 coarse summary 参数：若把这条严格蕴含关系压缩回单条 ↝，按照 03-propositional-operators.md §4.5 的最小 Jaynes/MaxEnt completion，应取 p₂ = 0.5
  • 整图中的节点级结果：若没有其他支撑路径，当前提缺席时，结论节点会回退到其先验，因此在具体图里常见 P(C=0|M=0) = π(¬C)

局域有效参数：

p₁ = 1，p₂ = 0.5

演绎是唯一一种宏观 ↝ 本身已经是严格的策略。展开前后结构不变 — 粗推理直接升级为严格蕴含。

注： Modus tollens（若 C 为假则 M 不全为真）不作为独立策略。它是 Bayes 定律在严格蕴含上的自然结果 — 当 C 的置信度降低时，通过 Bayes 更新，M 的置信度也随之降低。

示例： "所有金属在加热时膨胀"（A₁）∧ "铁是金属"（A₂）→ "铁在加热时膨胀"（C）。

2.2 溯因（Abduction）

宏观视图： Observation ↝ Hypothesis（认知方向：从证据到解释）。

观察到一个现象，推断最可能的假说。↝ 的方向是认知方向（epistemic direction）：从观测指向假说。

微观结构：

H ──┐
    ├──∨──→ D      D ↔ Obs
AltExp_Obs ─┘
  • D = H ∨ AltExp_Obs：现象 Obs 的解释联合。若假说成立，或存在其他可替代解释的机制，则该现象成立
  • AltExp_Obs：除 H 之外也能导致 Obs 的替代解释 / background explanation
  • D ↔ Obs：解释联合与实际观测等价（解释匹配观测）

关键说明： ↝ 的宏观方向（Obs → H）是认知方向 — 从证据推向解释。微观结构中的关键不只是 “H 能推出 Obs”，还包括 “不用 H 时 Obs 也可能由别的解释成立”。这正是溯因 uplift 的来源。

Bayes 推导：

目标：从 Obs 的观测值推导 H 的后验。

对 P(H=1 | Obs=1) 应用 Bayes 定律：

P(H=1 | Obs=1) = P(Obs=1 | H=1) · π(H) / P(Obs=1)

计算 P(Obs=1 | H=1)：

若 H=1：析取 H ∨ AltExp_Obs 强制 D=1，等价 D↔Obs 强制 Obs=1。因此：

P(Obs=1 | H=1) = 1

计算 P(Obs=1 | H=0)：

若 H=0：Obs 是否为真完全取决于替代解释 AltExp_Obs。因此：

P(Obs=1 | H=0) = π(AltExp_Obs)

代入全概率公式：

P(Obs=1) = P(Obs=1|H=1)·π(H) + P(Obs=1|H=0)·(1−π(H))
         = π(H) + π(AltExp_Obs)·(1−π(H))

因此：

P(H=1 | Obs=1) = π(H) / [π(H) + π(AltExp_Obs)·(1−π(H))]

当 Obs=0 时：

等价 D↔Obs 强制 D=0。而 D = H ∨ AltExp_Obs，所以必须 H=0 且 AltExp_Obs=0。因此：

P(H=0 | Obs=0) = 1

有效参数：

p₁ = π(H) / [π(H) + π(AltExp_Obs)(1−π(H))]，p₂ = 1

溯因的有效参数解读： - p₁ < 1：观测为真不能确证假说（还有其他可能解释），p₁ 取决于假说先验 π(H) 和替代解释的基础概率 π(AltExp_Obs) - p₂ = 1：观测为假时假说确定为假（modus tollens — 假说蕴含的预测未实现，假说被否定）

示例： 假说 H = "该患者感染了流感"，观测 Obs = "该患者出现发热"，替代解释 AltExp_Obs = "存在其他原因导致发热"。发热出现后，流感假说的置信度上升；但上升幅度取决于“其他原因导致发热”本来有多常见。实验可靠性本身应单独建成 measurement likelihood，而不是直接并入 π(AltExp_Obs)。

2.3 归纳（Induction）

宏观视图： {Obs₁, Obs₂, ..., Obsₙ} ↝ Law（多个实例支持一般规律）。

微观结构：

Law ──┐
      ├──∨──→ D₁      D₁ ↔ Obs₁
AltExp₁ ─┘
Law ──┐
      ├──∨──→ D₂      D₂ ↔ Obs₂
AltExp₂ ─┘
  ⋮                     ⋮
Law ──┐
      ├──∨──→ Dₙ      Dₙ ↔ Obsₙ
AltExpₙ ─┘
  • Dᵢ = Law ∨ AltExpᵢ：第 i 个观测的解释联合。若规律成立，或存在该观测的其他解释，则 Obsᵢ 为真
  • AltExpᵢ：第 i 个观测的替代解释 / background explanation
  • Dᵢ ↔ Obsᵢ：解释联合与实际观测等价

归纳的微观结构是溯因的并行重复 — 每条 Law ∨ AltExpᵢ ↔ Obsᵢ 都是一个溯因单元。区别在于多个观测联合作用。

Bayes 推导：

假设各 AltExpᵢ 在 Law 给定后条件独立（这是归纳的标准假设）。

计算 P(all Obsᵢ=1 | Law=1)：

Law=1 时，每条析取都强制 Dᵢ=1，等价强制 Obsᵢ=1：

P(all Obsᵢ=1 | Law=1) = 1

计算 P(all Obsᵢ=1 | Law=0)：

Law=0 时，各 Obsᵢ 只由各自的替代解释 AltExpᵢ 决定。由条件独立：

P(all Obsᵢ=1 | Law=0) = ∏ᵢ π(AltExpᵢ)

简记 ∏ᵢ π(AltExpᵢ) = ∏ᵢ ρᵢ。

Bayes 更新：

P(Law=1 | all Obsᵢ=1) = π(Law) / [π(Law) + (1−π(Law))·∏ᵢ ρᵢ]

关键性质： 随着 n 增大，若每个 ρᵢ < 1，则乘积 ∏ᵢ ρᵢ → 0，后验 → 1。这就是归纳的力量 — 足够多的一致观测使规律几乎确定。

反例处理： 若某个 Obsⱼ = 0：

等价 Dⱼ ↔ Obsⱼ 强制 Dⱼ = 0。而 Dⱼ = Law ∨ AltExpⱼ，所以必须 Law = 0：

P(Law=0 | Obsⱼ=0) = 1

有效参数：

p₁ = π(Law) / [π(Law) + (1−π(Law))·∏ᵢ ρᵢ]，p₂ = 1

归纳的有效参数解读： - p₁ 随观测数 n 增大趋向 1：每个新的一致观测都压低分母中的乘积项，推高后验 - p₂ = 1：任何一个反例即刻推翻规律（modus tollens 是确定性的）

示例： Law = "所有天鹅都是白色的"，Obsᵢ 为实际观测，AltExpᵢ 表示“第 i 次观测在没有一般规律时也可能成立的替代解释”。每多观测一只白天鹅，规律的置信度上升；若任一观测为假，则规律在严格模型下被否定。

2.4 类比（Analogy）

宏观视图： SourceConclusion ↝ TargetConclusion（源域结论迁移到目标域）。

核心不是物理上的相似性，而是一个显式的桥梁主张 — 声明源域与目标域在相关结构上可对应。

微观结构：

SourceLaw ──┐
             ├──∧──→ M ──→ TargetConclusion
BridgeClaim ─┘           (严格蕴含)
  • M = SourceLaw ∧ BridgeClaim（源域规律与桥梁主张合取）
  • M → TargetConclusion（严格蕴含：若源域规律成立且桥梁有效，则目标域结论成立）
  • BridgeClaim 是一个 Claim，声明"源域与目标域在相关结构上可对应"，携带先验 π(BridgeClaim)

不确定性不在蕴含本身，而在 BridgeClaim 是否成立。

Bayes 推导：

当 SourceLaw 已知为真时（π(SourceLaw) ≈ 1）：

M=1 当且仅当 BridgeClaim=1。因此：

P(Target=1 | Source=1) = P(M=1 | Source=1) = π(BridgeClaim)

由严格蕴含 M → Target，M=1 时 Target=1 确定。M=0 时 Target 回退到先验。

完整推导：

P(Target=1 | Source=1) = P(Target=1 | M=1)·P(M=1|Source=1) + P(Target=1 | M=0)·P(M=0|Source=1)
                       = 1 · π(BridgeClaim) + π(Target) · (1−π(BridgeClaim))

简化（当 π(Target) 较小时）：

P(Target=1 | Source=1) ≈ π(BridgeClaim)

当 Source=0 时：

M = Source ∧ BridgeClaim = 0（不论 BridgeClaim 取何值）。M=0 时蕴含不施加约束，Target 回退到先验：

P(Target=0 | Source=0) ≈ π(¬Target)

有效参数：

p₁ = π(BridgeClaim) + π(Target)·(1−π(BridgeClaim))，p₂ ≈ π(¬Target)

当 π(Target) 较小时简化为 p₁ ≈ π(BridgeClaim)。

类比的有效参数解读： - p₁ 主要取决于桥梁主张的先验 — 桥梁越可信，类比越强 - p₂ 取决于目标结论本身的先验 — 源域不成立时目标回退到基础水平

示例： SourceLaw = "药物 X 在小鼠模型中有效"，BridgeClaim = "小鼠模型的药效可迁移到人类"，TargetConclusion = "药物 X 在人类中有效"。类比的强度取决于 BridgeClaim 的先验 — 即动物模型到人类的可迁移性有多可信。

2.5 外推（Extrapolation）

宏观视图： KnownRange ↝ ExtendedRange（已知范围的规律延伸到新范围）。

外推与类比在结构上完全相同。区别在于语义：

  • 类比是跨域迁移 — 不同系统之间的结构对应
  • 外推是范围延伸 — 同一参数空间内从已知区域推向未知区域

微观结构：

KnownLaw ────┐
              ├──∧──→ M ──→ ExtendedConclusion
ContinuityClaim ─┘         (严格蕴含)
  • ContinuityClaim 声明"从已知范围到目标范围的延伸是合理的"（例如，物理规律在极端条件下仍然适用）

Bayes 推导：

与类比完全相同。有效参数取决于 ContinuityClaim 的先验。

有效参数：

p₁ = π(ContinuityClaim) + π(Extended)·(1−π(ContinuityClaim))，p₂ ≈ π(¬Extended)

示例： KnownLaw = "牛顿力学在日常速度下精确成立"，ContinuityClaim = "牛顿力学在接近光速的条件下仍然成立"，ExtendedConclusion = "牛顿力学预测的动能公式在接近光速时仍然正确"。ContinuityClaim 的先验很低（实际上被相对论否定），因此外推很弱。

2.6 归谬（Reductio ad Absurdum）

宏观视图： Contradiction ↝ ¬Hypothesis（导出矛盾，推翻假说）。

经典反证法：假设 P 成立，推导出与已知事实的矛盾，从而得出 ¬P。

微观结构：

P ──→ Q      Q ⊗ R      P ⊕ ¬P
 (严格蕴含)   (矛盾)     (互补)
  • P → Q：从假设 P 严格蕴含推论 Q
  • Q ⊗ R：推论 Q 与已知事实 R 矛盾（不能同时为真）
  • P ⊕ ¬P：P 和 ¬P 是真值互补（恰好一个为真）

Bayes 推导：

当 R=1 时（已知事实成立）：

Q ⊗ R 意味着 P(Q ∧ R) = 0。因此 R=1 时 Q 必为假：

Q = 0

P → Q 是严格蕴含。Q=0 时，由 modus tollens：

P = 0

P ⊕ ¬P 是互补关系。P=0 时：

¬P = 1

整个推导链是确定性的（所有算子均为严格），因此：

P(¬P=1 | R=1) = 1

当 R 的置信度不完全为 1 时：

推导的确定性取决于 R 的确信程度。若 R 的先验 π(R) < 1，则 ¬P 的后验不完全为 1，但 π(R) 越高，¬P 的置信度越高。

有效参数：

p₁ = 1（当所有链接严格时，矛盾确定性地推翻假说），p₂ 取决于 ¬P 的先验支持

归谬的有效参数解读： - p₁ = 1：矛盾被确认时，假说必然被推翻 - p₂：矛盾未被确认时，¬P 回退到其先验水平

注： 归谬需要互补关系 ⊕（定义见 03-propositional-operators.md §2.5）。在 Gaia IR 中，这一关系可直接用 Operator(operator=complement) 表达；具体 backend 如何 lower 它，属于下游实现问题，不反向约束 theory / IR 的定义。

示例： P = "√2 是有理数"，Q = "√2 可表示为 a/b（a、b 互素）"，R = "不存在同时为偶数的互素整数对"。从 P 推出 Q，展开后发现 Q 蕴含 a 和 b 都必须是偶数，这与 R 矛盾，因此 P 为假，¬P = "√2 是无理数" 成立。

2.7 排除（Elimination）

宏观视图： ExhaustiveContradictions ↝ RemainingCandidate（排除所有备选，幸存者为结论）。

微观结构：

假设有三个互相排斥且穷举的候选假说 H₁, H₂, H₃：

D ≡ (H₁ ∨ H₂ ∨ H₃)   （coverage / 穷尽性）

H₁ ⊗ E₁              （证据 E₁ 与假说 H₁ 矛盾）
H₂ ⊗ E₂              （证据 E₂ 与假说 H₂ 矛盾）

[D, E₁, Contra₁, E₂, Contra₂] ──→ H₃
  • D：正向的 coverage / exhaustiveness claim，表示列出的候选已覆盖当前讨论空间
  • Hᵢ ⊗ Eᵢ：各证据与对应候选矛盾；当 Eᵢ=1 时，对应候选不能成立
  • [D, E₁, Contra₁, E₂, Contra₂] → H₃：若 coverage 成立且其他候选都被成功排除，则幸存者 H₃ 必然成立

Bayes 推导：

当 E₁=1 且 E₂=1 时（排除性证据都成立）：

矛盾 H₁ ⊗ E₁ + E₁=1 → H₁=0，因此 Contra₁=1。

矛盾 H₂ ⊗ E₂ + E₂=1 → H₂=0，因此 Contra₂=1。

若 coverage D=1，则 H₁∨H₂∨H₃ 为真。又因 H₁=0 且 H₂=0，唯一剩余候选只能是 H₃。

于是 gate [D, E₁, Contra₁, E₂, Contra₂] 全为真，严格蕴含推出 H₃=1。

P(H₃=1 | E₁=1, E₂=1) = 1

整个推导是确定性的。

有效参数：

p₁ = 1（所有备选被排除时，幸存者确定成立），p₂ 取决于先验

排除的有效参数解读： - p₁ = 1：排除性证据完备时，幸存者必然成立（这依赖穷尽性假设的正确性） - p₂：若排除性证据未完全确认，幸存者回退到先验水平

最小例子： 三种可能的病因 H₁ = "细菌感染"、H₂ = "病毒感染"、H₃ = "自身免疫反应"。D = "这三类病因已覆盖当前鉴别诊断空间"。抗生素试验阴性排除 H₁（E₁），病毒检测阴性排除 H₂（E₂）。若 D 成立，则 H₃ 成立。

2.8 数学归纳（Mathematical Induction）

宏观视图： [Base, Step] ↝ Law（基础情形 + 归纳步骤 → 全称命题），p₁ = 1。

数学归纳法从两个前提确定性地证明全称命题：基础情形 P(0) 成立，且归纳步骤 P(n)→P(n+1) 成立，则 ∀n.P(n)。

与经验归纳的根本区别： 经验归纳（§2.3）从有限实例逐步积累信心，p₁ < 1；数学归纳从两条前提获得确定性证明，p₁ = 1。两者虽共享"归纳"之名，但推理机制完全不同。

经验归纳 数学归纳
确信来源 证据积累（实例越多越可信） 论证结构（两条前提即可证明）
确定性 p₁ < 1，随 n 趋向 1 p₁ = 1
反例处理 反例削弱规律的 belief 不存在反例（若存在则归纳步骤有误）

微观结构：

Base ────┐
          ├──∧──→ M ──→ Law
Step ────┘         (严格蕴含)
  • Base = P(0)（基础情形成立，一个 Claim）
  • Step = "∀n. P(n) → P(n+1)"（归纳步骤声明，一个 Claim）
  • M = Base ∧ Step（两个前提合取，确定性）
  • M → Law（严格蕴含：数学归纳公理保证，若 Base 和 Step 都成立，则全称命题 Law 成立）

微观结构与演绎（§2.1）形式完全相同。区别在于语义：演绎的前提和结论都是具体命题，而数学归纳的结论是全称命题（∀n.P(n)），归纳步骤本身也是全称声明。

Bayes 推导：

与演绎完全相同 — (Base ∧ Step) → Law 是一条严格蕴含。

当 M = 1 时（Base 和 Step 都成立）：

P(Law=1 | M=1) = 1

当 M = 0 时（至少一个前提不成立）：

P(Law=0 | M=0) = π(¬Law)

这里同样要区分两层：

  • 局域 coarse summary 参数：若把整个归纳证明压缩回单条 ↝，其严格蕴含骨架对应的局域 completion 仍是 p₂ = 0.5
  • 整图中的节点级结果：若缺少 Base 或 Step，且不存在其他支撑路径，则全称结论节点回退到其先验，表现为 P(Law=0|M=0) = π(¬Law)

局域有效参数：

p₁ = 1，p₂ = 0.5

数学归纳的关键不在概率计算（与演绎相同），而在归纳步骤的正确性。Step 声称"对任意 n，P(n)→P(n+1)"——这是一个需要证明的命题，其 belief 取决于证明的质量。如果归纳步骤有漏洞（Step 的 belief 降低），反向消息压低 Law 的 belief，正确反映了"归纳步骤有漏洞则结论不可靠"。

注： 这里要区分 P(n) 和 ∀n.P(n)：

  • P(n) 是带自由变量的 Template
  • ∀n.P(n) 是对该 Template 做全称闭包后得到的Claim

因此，数学归纳中的 Law 和 Step 都应视为 Claim，可以合法携带 π 与 belief。真正的 future work 不是 "Template 参与 BP"，而是量词 / 绑定变量如何在 Gaia IR 中显式表示。

示例： Base = "当 n=1 时，1 = 1×2/2 成立"，Step = "若 1+2+...+k = k(k+1)/2，则 1+2+...+k+(k+1) = (k+1)(k+2)/2"，Law = "∀n ≥ 1，1+2+...+n = n(n+1)/2"。两条前提（直接验证 + 代数推导）确定性地证明全称命题。

2.9 分情况讨论（Case Analysis）

宏观视图： [A₁∨...∨Aₖ, {Proofs}] ↝ C（穷尽情形划分 + 逐案论证 → 结论），p₁ = 1。

将问题按穷尽的情形划分，在每个情形下分别证明结论成立。这是数学证明中最常用的技术之一。

与排除法的对比： 排除法（§2.7）和分情况讨论都依赖穷尽的情形划分，但推理机制相反：

分情况讨论 排除法
方法 每个 case 下正面推出 C 否定除 survivor 外的所有 case
结论 外部命题 C（不是 case 之一） case 之一（survivor）
性质 建设性（constructive） 破坏性（destructive）

微观结构：

A₁ ∨ A₂ ∨ ... ∨ Aₖ     (穷尽析取)

A₁ ∧ P₁ ──→ C           (严格蕴含)
A₂ ∧ P₂ ──→ C           (严格蕴含)
  ⋮
Aₖ ∧ Pₖ ──→ C           (严格蕴含)
  • A₁∨...∨Aₖ 是穷尽性声明（至少一个情形成立）
  • Pᵢ 是在情形 Aᵢ 下推出 C 的论证（各自独立的 Claim）
  • (Aᵢ ∧ Pᵢ) → C 是每个情形下的严格蕴含

Bayes 推导：

设 D 表示穷尽性声明 A₁∨...∨Aₖ 成立。

当 D = 1 且所有 Pᵢ 的 belief 为 1 时：

穷尽性保证至少存在某个 j 使得 Aⱼ = 1。对应的严格蕴含 (Aⱼ ∧ Pⱼ) → C 中，Aⱼ = 1 且 Pⱼ = 1，故 C = 1：

P(C=1 | D=1, all Pᵢ=1) = 1

当 D = 0 时（穷尽性不成立）：

可能没有任何 Aᵢ 为真，没有蕴含链活跃，C 回退到先验：

P(C=0 | D=0) = π(¬C)

这里同样要区分两层：

  • 局域 coarse summary 参数：若把整个分情况证明压缩回单条 ↝，其严格骨架在局域层的 completion 仍对应 p₂ = 0.5
  • 整图中的节点级结果：若穷尽性不成立且没有其他支撑路径，则结论节点回退到其先验，表现为 P(C=0|D=0) = π(¬C)

局域有效参数：

p₁ = 1，p₂ = 0.5

分情况讨论的有效参数解读： - p₁ = 1：穷尽性成立且各案论证完备时，结论确定 - p₂ = 0.5：作为局域 summary，穷尽性不成立时该压缩链本身不再提供额外信息；在具体图里，结论节点随后会回退到先验

穷尽性的关键性： 与排除法相同，分情况讨论的有效性依赖穷尽性声明的正确性。穷尽性通常来自数学结构（奇偶性、正负零）、定义穷举或逻辑排中律。穷尽性声明本身可以是一个需要论证的 Claim（先验 < 1），也可以是不证自明的 Setting。

在 scientific reasoning 中，关键通常不是显式列出一个 OtherCase，而是判断“当前列出的这些情形是否足以覆盖此次推理所需的讨论空间”。因此更小、更稳的建模方式是保留一个正向的 coverage / exhaustiveness claim，并把其不确定性体现在该 claim 自身的信念上；若无法建立这种 coverage，就不应把这条结构当成 strict case analysis。

注： 分情况讨论需要析取（∨）来表达穷尽性。析取可通过 De Morgan 律从 {¬, ∧} 派生：A ∨ B ≡ ¬(¬A ∧ ¬B)，因此不引入新的理论原语。在 Gaia IR 中，这一关系可直接用 Operator(operator=disjunction) 表达；具体 backend 是否把它实现为独立 runtime factor，属于 lowering / 执行层问题，不影响 theory / IR 语义。

示例： 证明 "n²+n 对所有自然数 n 都是偶数"。A₁ = "n 是偶数"，A₂ = "n 是奇数"（穷尽性：每个自然数要么奇要么偶）。P₁ = "若 n=2k，则 n²+n = 2(2k²+k)，是偶数"，P₂ = "若 n=2k+1，则 n²+n = 2(2k+1)(k+1)，是偶数"。两种情形下结论都成立。

3. 总结

3.1 策略一览

策略 宏观 ↝ 方向 微观结构 有效 p₁ 有效 p₂
演绎 M ↝ C ∧ + → 1 0.5
溯因 Obs ↝ H Obs ≡ (H ∨ AltExp_Obs) π(H)/[π(H)+π(AltExp_Obs)(1−π(H))] 1
归纳 {Obsᵢ} ↝ Law Obsᵢ ≡ (Law ∨ AltExpᵢ) π(Law)/[π(Law)+(1−π(Law))∏π(AltExpᵢ)] 1
类比 Source ↝ Target [Source, Bridge] → Target π(Bridge)+π(Target)(1−π(Bridge)) π(¬Target)
外推 Known ↝ Extended [Known, Continuity] → Extended π(Continuity)+π(Ext)(1−π(Cont)) π(¬Ext)
归谬 Contradiction ↝ ¬P P→Q + Q⊗R + P⊕¬P 1 先验依赖
排除 Eliminations ↝ Survivor ∨ + ⊗ + coverage → 1 先验依赖
数学归纳 [Base, Step] ↝ Law ∧ + → 1 0.5
分情况讨论 [A₁∨...∨Aₖ, {Pᵢ}] ↝ C ∨ + k 条 → 1 0.5

3.2 结构观察

确定性 vs 不确定性。 九种策略分为三类：

  • 确定性策略（p₁ = 1）：演绎、归谬、排除、数学归纳、分情况讨论 — 展开后的命题网络完全由严格算子构成
  • 不确定性策略（p₁ < 1）：溯因、归纳 — 不确定性来自接口层的替代解释 claim（AltExp_*）先验，而不是私有中间节点
  • 桥梁依赖策略（p₁ 取决于桥梁先验）：类比、外推 — 不确定性集中在桥梁主张上

p₂ 的模式。 值得注意的是，溯因和归纳的 p₂ = 1（观测为假时确定性地否定假说/规律），这来自严格蕴含的 modus tollens。而类比和外推的 p₂ 取决于目标结论的先验。演绎、数学归纳和分情况讨论若压缩成局域 ↝ summary，则其最小 Jaynes/MaxEnt completion 给出 p₂ = 0.5；在具体图里，当前提缺席时结论节点会进一步回退到先验。

归纳是并行溯因。 归纳的微观结构由 n 个独立的溯因单元组成。每增加一个一致的观测，分母中的乘积项缩小，后验趋向 1。这量化了"多个独立证据的累积效应"。

数学归纳 vs 演绎。 数学归纳在概率计算上与演绎完全相同（(Base ∧ Step) → Law，p₁ = 1）。将其列为独立策略是因为：(1) 避免与经验归纳的名称混淆，(2) 归纳步骤的"∀n"语义是独特的论证模式，(3) 其底层依赖 Template P(n)，但结论 ∀n.P(n) 本身是由 Template 闭包得到的 Claim。

分情况讨论 vs 排除。 两者共享穷尽性前提，但证明方向相反 — 分情况讨论在每个 case 下建设性地推出 C，排除法破坏性地否定非 survivor。逻辑上 [¬H₁∧¬H₂]→H₃ 等价于 H₁∨H₂∨H₃（De Morgan），但证明路径的差异决定了不同的 formal / operator 结构。

↝ 方向 vs 微观结构方向。 溯因和归纳的宏观 ↝ 方向（Obs → H / Law）与微观解释结构方向（H ∨ AltExp_Obs → Obs）不同。这不是矛盾 — 宏观方向是认知方向（从证据到结论），微观方向是说明“哪些解释能产生该现象”。Bayes 定律正是将这种解释竞争结构转化为认知推理（P(H | Obs)）的桥梁。

3.3 Gaia IR 对齐说明

当前 theory 与 Gaia IR 的对齐关系如下：

结构 Gaia IR 状态 说明
⊕（互补） 已支持 可直接用 Operator(operator=complement) 表达
∨（析取） 已支持 可直接用 Operator(operator=disjunction) 表达
量词 / 绑定变量表示 仍待补完 P(n) 是 Template，但 ∀n.P(n) 与 ∀n(P(n)→P(n+1)) 仍需要更明确的 quantified claim 表示

因此，当前真正剩余的 Gaia IR 表达问题主要集中在量词 / 绑定变量，而不是 complement 或 disjunction 这类命题算子本身。

交叉引用

  • 上游：
  • 03-propositional-operators.md — 最小原料 {¬, ∧, π}、派生算子、关系类型、软蕴含 ↝ 的定义与理论地位
  • 01-plausible-reasoning.md — Cox 定理、Bayes 定律、弱三段论
  • 下游：
  • 05-formalization-methodology.md — 科学文本 → 命题网络的具体方法论，使用本文档定义的策略作为展开模板
  • 计算层：
  • 06-factor-graphs.md — 本文档的命题网络在计算层映射为因子图，算子映射为势函数。本文档只定义概率语义，不涉及计算方法。

参考文献

  • Jaynes, E.T. Probability Theory: The Logic of Science (2003)
  • Peirce, C.S. "Deduction, Induction, and Hypothesis" (1878) — 三种推理模式的经典分类
  • Polya, G. Mathematics and Plausible Reasoning (1954) — 类比和归纳的数学基础