定性默认推理与概率的逻辑研究及一阶线性逻辑证明搜索

### 定性默认推理与概率的逻辑研究及一阶线性逻辑证明搜索 #### 概率定性默认推理逻辑机构的构建 在定性默认推理与概率的研究中，我们可以从 InstC 和 InstK 推导出大步概率的机构 InstS 的各个组成部分： - **签名（SigS）**：SigS = SigB，即签名为命题签名。 - **模型（ModS）**：ModS(Σ) 是从 ModC(Σ) 中通过限制到大步概率分布 PBS(Σ) 得到的全子范畴。对于每个签名态射 ϕ : Σ → Σ′，函子 ModS(ϕ) 是 ModC(ϕ) 对 ModS(Σ′) 和 ModS(Σ) 的限制和余限制。 - **语句（SenS）**：SenS = SenK，即语句为 InstK 中的条件语句，并带有相应的语句翻译。 - **满足关系（|=S）**：对应于特定条件，满足关系定义为：P |=S,Σ (B|A) 当且仅当 P(AB) > P(AB)。 命题 1 指出，InstS = ⟨SigS, ModS, SenS, |=S ⟩ 是一个机构。通过引理 1 和 2 以及 ϕ 的单射性，可以验证 ModS(ϕ) 是良定义的，即能将 Σ′ 上的大步概率分布映射到 Σ 上的大步概率分布。同时，满足定义 1 中的满足条件，即 P ′ |=S,Σ′ SenS(ϕ)(B|A) 当且仅当 ModS(ϕ)(P ′) |=S,Σ (B|A)。 #### 序数逻辑与概率定性逻辑的关系 我们将序数和定性概率条件逻辑都形式化为机构后，可以使用机构态射来研究它们之间的形式逻辑关系。InstK 和 InstS 具有相同的语法，由命题签名 SigK = SigS = SigB 和条件语句 SenK = SenS 提供，但在语义上有所不同，分别由模型函子 ModK 和 ModS 以及满足关系 |=K 和 |=S 定义。 命题 2 表明，不存在从 InstK 到 InstS 的机构态射 ⟨idSigB, idSenK, β ⟩。假设存在这样的机构态射，会得出与 InstS 性质矛盾的结果。 然而，从 InstS 到 InstK 的机构态射是可行的。通过定义自然变换 β : ModS =⇒ ModK，将每个大步概率 P ∈ ModS(Σ) 关联到一个全预序 RP ∈ ModK(Σ)，即 ω1 ⪯RP ω2 当且仅当 P(ω1) ⩾ P(ω2)。命题 3 指出，⟨idSigB, idSenK, βS/K ⟩: InstS → InstK 是从 InstS 到 InstK 的唯一机构态射，这表明大步概率分布足以实现定性条件推理，并且使基于大步概率的概率推理与基于全预序的定性推理完全兼容。 我们还考虑了更一般的问题，即哪些概率分布的子类 ModQ(Σ) 适合构建机构 InstQ，并允许从 InstQ 到 InstK 的态射。命题 4 给出了答案，概率分布 P 需满足特定性质，如性质 (4)、(6) 以及对于所有 ω1, ω2 ∈ Ω，P(ω1) = P(ω2) 当且仅当 ω1 = ω2，或者对于所有 ω ∈ ΩΣ\{ω1, ω2}，P(ω) > P(ω1) = P(ω2)。 以下是相关内容的流程图： ```mermaid graph LR A[构建 InstS 机构] --> B[确定 SigS、ModS、SenS、|=S] B --> C[证明 InstS 是机构] D[研究逻辑关系] --> E[比较 InstK 和 InstS] E --> F[证明无 InstK 到 InstS 的态射] E --> G[证明有 InstS 到 InstK 的态射] H[考虑一般问题] --> ```