社交宣告逻辑的表列式演算

祝瑞


第19届全国现代逻辑学术研讨会
华东师范大学哲学学院
上海 2025.11

社交网络

信念分布

社交网络:

宣告:

结果

基本设定

信念 $B_{a}\theta$: 主体 a 相信命题θ。

行动 $\langle X\rangle\phi$: 公式φ 在行动 X 之后成立。
例如： $[a:\theta](B_{b}\gamma \wedge \neg B_{c}\gamma)$ 意味着：“在 $a$ 宣告 θ 后，$b$ 相信 γ，而 $c$ 不相信。”

表示 信念和宣告都是命题性的。

网络 网络是静态的 —— 在信念传播期间不会改变。

主体属性

  • 🧠 轻信的 (Gullible): 相信接收到的消息。
  • 🛡️ 保守的 (Conservative): 永不失去信念。
  • ⚙️ 逻辑全知的 (Logically omniscient): 相信他们信念的所有逻辑后果。

框架

语言 $\mathsf{A}$ 是一个有限的主体集合。 $\mathsf{Prop}$ 是命题变元的集合。 消息 (message) 定义如下
\[ \theta ::= p~|~\neg \theta~|~(\theta\wedge \theta)\] 我们定义 $L_{SAL}$ 语言中的公式 (formula) 如下
\[ \phi ::= B_{a} \theta~|~bFa~|~\neg\phi~|~(\phi\wedge\phi)~|~[a: \theta]\phi~|~\langle a! \theta\rangle\phi~|~\langle a! \rangle\phi \] 其中 $p\in \mathsf{Prop}$，$a \in A$，并且对于每个 $a$，在 $L_{SAL}$ 中都有一个模态算子 $B_{a}$。

指称 (Denotation)
\[V = 2^{\mathsf{Prop}} \\ \llbracket p \rrbracket = \{x \in V ~|~ p \in x \} \\ \llbracket \neg \theta \rrbracket = V \backslash \llbracket \theta \rrbracket \\ \llbracket (\theta_1 \wedge \theta_2) \rrbracket = \llbracket \theta_1\rrbracket \cap \llbracket\theta_2 \rrbracket\]
模型 (Model)
$~~~~~~~~(f, k)\vDash B_{a}\theta \Leftrightarrow k(a)\subseteq \llbracket \theta\rrbracket$
$~~~~~~~~(f, k)\vDash bFa \Leftrightarrow b \in f(a)$
$~~~~~~~~(f, k)\vDash [a:\theta] \phi \Leftrightarrow (f, [a:\theta]k)\vDash \phi$
其中 $[a:\theta]k(b) = \begin{cases} k(b)\cap \llbracket \theta \rrbracket~~~~ 如果~b\in f(a), \\ k(b)~~~~~~其他情况 \end{cases}$
$~~~~~~~~(f, k)\vDash \langle a!\theta\rangle \phi \Leftrightarrow [a:\theta](f, k)\vDash \phi~\&~k(a)\subseteq \llbracket \theta\rrbracket$
$~~~~~~~~(f, k)\vDash \langle a!\rangle\phi \Leftrightarrow \exists\theta (k(a) \subseteq \llbracket \theta\rrbracket~\&~[a :\theta](f, k) \vDash \phi)$

所有 $L_{SAL}$ 公式都可以等价地转换为否定范式 (Negation Normal Form, NNF) \[ \phi_{\neg} ::= B_{a} \theta \mid \neg B_{a} \theta \mid bFa \mid \neg bFa \mid (\phi \wedge \phi) \mid (\phi \vee \phi) \mid [a:\theta]\phi \mid \langle a!\theta\rangle \phi \mid [a!\theta]\phi \mid \langle a!\rangle \phi \mid [a!]\phi \]

表列式演算

公理系统的难处

"Hilbert-style systems are easy to define and admit a simple proof of the completeness theorem but they are difficult to use."
  ——Jon Barwise

$$ \color{white} \tiny \begin{aligned} E.g. &\vdash p\to p & \\ 1. & (p \to ((p \to p) \to p))\to &\\ ~&((p \to (p \to p)) \to (p \to p)) & \text{(A2)} \\ 2. & p \to ((p \to p) \to p) & \text{(A1)} \\ 3. & (p \to (p \to p)) \to (p \to p) & \text{(1, 2)} \\ 4. & p \to (p \to p) & \text{(A1)} \\ 5. & p \to p & \text{(3, 4)} \end{aligned} $$

表列的分析特性

  • 采用直观的树状结构表示推导过程。
  • 逐步分解公式为更简单的子公式。
  • 易于从末端开放的分支构造反模型。
p ∨ q ¬p p × q (Open)

算法与可判定性

  • 表列推导过程类似算法：按规则分解公式，分支选择有限。
  • 清晰体现证明的结构，有助于分析可判定性 (decidability)。
  • 易于通过编程实现自动化证明。

表列的结构

表列式证明的过程，就是一棵不断向下扩展的“树”。

一棵“树”是满足以下条件的节点集合：

  • 根节点 (Root)：有且仅有一个节点没有父节点，它是一切的起点。
  • 父节点 (Parent)：除根节点外，每个节点都有且仅有一个父节点。
  • 祖先与后代 (Ancestor / Descendant)：“是...的父节点的父节点...” 这种关系链构成了祖先与后代。
  • 无环性 (Acyclic)：一个节点永远不能是其自身的祖先。这是树最重要的特性。

✔ 这是一棵树

❌ 不是树 (存在多个根)

❌ 不是树 (共享子节点)

❌ 不是树 (存在循环)

表列规则

($[:]_{\wedge}$)
$[\vec{b:\gamma}](\phi\wedge\psi)$
↓
$[\vec{b:\gamma}]\phi$
$[\vec{b:\gamma}]\psi$
($[:]_{\vee}$)
$[\vec{b:\gamma}](\phi\vee\psi)$
↙ ↘
$[\vec{b:\gamma}]\phi$
$[\vec{b:\gamma}]\psi$
($[:]_{K}$)
$[\vec{b:\gamma}][a:\theta]B_{c}\epsilon$
↙ ↘
         
$[\vec{b:\gamma}] B_{c}\epsilon$
$[\vec{b:\gamma}] B_{c}(\theta\rightarrow\epsilon)$
$cFa$
($[:]_{\widetilde{K}}$)
$[\vec{b:\gamma}][a:\theta]\neg B_{c}\epsilon$
↙ ↘
$[\vec{b:\gamma}]\neg B_{c}(\theta\rightarrow\epsilon)$
$[\vec{b:\gamma}]\neg B_{c} \epsilon$
$\neg cFa$
($\langle !_{\theta}\rangle$)
$[\vec{b:\gamma}]\langle a!\theta\rangle\phi$
↓
$[\vec{b:\gamma}]B_{a}\theta$
$[\vec{b:\gamma}][ a:\theta]\phi$
($[!_{\theta}]$)
$[\vec{b:\gamma}][ a!\theta]\phi$
↙ ↘
$[\vec{b:\gamma}]\neg B_{a}\theta$
$[\vec{b:\gamma}][ a:\theta]\phi$
($\langle !\rangle$)
$[\vec{b:\gamma}]\langle a!\rangle\phi$
↓
$[\vec{b:\gamma}]\langle a!p\rangle\phi$
($[!]$)
$[\vec{b:\gamma}][ a!]\phi$
↓
$[\vec{b:\gamma}][ a!\theta]\phi$

其中 $[\vec{b:\gamma}]$ 是一个自由宣告算子序列或是空的，并且 $p$ 是一个新的原子消息，它不出现在该节点的任何祖先中。

闭合规则 一个表列分支 $\mathfrak{B}$ 是矛盾的 (contradictory)，如果它满足以下条件之一：
  1. 对于某个主体 $a$，该分支包含一个集合 $\{B_{a}\theta_1, \dots, B_{a}\theta_n, \neg B_{a}\theta\}$ (其中 $n \ge 0$)，使得 $\vdash_0 (\theta_1 \land \dots \land \theta_n) \to \theta$。
  2. 对于某些主体 $a, b$，该分支同时包含 $bFa$ 和 $\neg bFa$。

表列法定理证明

证明 $\langle a!p\rangle \neg B_c r \wedge B_c(p\rightarrow r) \to \neg cFa$。 推演其否命题：$\langle a!p\rangle \neg B_c r \wedge B_c(p\rightarrow r) \wedge cFa$

1. ⟨a!p⟩¬Bc r 2. Bc(p→r) 3. cFa 4. Ba p (依据 1) 5. [a:p]¬Bc r (依据 1) 6. ¬Bc(p→r) (依据 5) 7. ¬Bc r (依据 5) 8. ¬cFa (依据 5) × (矛盾 2, 6) × (矛盾 3, 8)

可靠性

表列规则保持可满足性 (Satisfaction Preserving)：

  • 🏛️非 $\langle!\rangle$ 柱式规则: 若模型 $m$ 满足某分支上的所有公式，则 $m$ 也满足应用这些规则后添加的新公式。
  • 🌿 分支规则: 若模型 $m$ 满足某分支上的所有公式，则 $m$ 必然满足应用分支规则后至少一个新分支上的所有公式。
  • 💎 规则$\langle !\rangle$: 若模型 $m$ 满足某分支上的所有公式，则可以构造一个新模型 $h_{p,\theta}[m]$。在该新模型中，$p$ 等价于 $\langle a!\rangle$ 的某个见证 $\theta$，并且新模型保持所有不含 $p$ 的公式的可满足性。严格证明参见 (Zhu, 2025)。

反驳与推导 若从一个公式集合 $H$ 出发构造的表列的所有分支都闭合，则称该表列为 $H$ 的一个反驳表列。我们称前提集合 $H$ 可推导出 $\phi$（记作 $H\vdash \phi$），是说 $H\cup \{\neg\phi\}$ 存在一个反驳表列。

引理 如果公式集合 $H$ 存在一个反驳表列，则 $H$ 是不可满足的，即 $H$ 没有模型。

可靠性定理 该表列系统是可靠的，即对于任意公式集合 $H$ 和公式 $\phi$，若 $H\vdash \phi$，则 $H\vDash \phi$。

开分支

推演：$\{[a:p]\langle b!q\rangle B_c r, [b!q] \neg B_c r, [a:r]\neg B_c r\}$

1. [a:p]⟨b!q⟩Bc r 2. [b!q]¬Bc r 3. [a:r]¬Bc r 4. ¬Bb q (根据 2) 5. [b:q]¬Bc r (根据 2) 6. ¬Bc(r→r) (根据 3) 7. ¬Bc r (根据 3) 8. ¬cFa (根据 3) 12. [a:p]Bb q (根据 1) 13. [a:p][b:q]Bc r (根据 1) 14. Bb q (根据 12) 15. Bb (p→q) (根据 12) 16. bFa (根据 12) × (矛盾 4, 14) 17. [a:p]Bc r (13) 18. [a:p]Bc (q→r) (13) 19. cFb (13) 20. Bc r (16) 21. cFa (16) × (矛盾 20, 7) × (矛盾 21, 8) 22. Bc (q→r) (18) 23. cFa (18) ✓ 开放 × (矛盾 23, 8) × (矛盾 6) 9. ¬Bc(r→r) (根据 3) 10. ¬Bc r (根据 3) 11. ¬cFa (根据 3) × (矛盾 9)

反模型

开放分支 (模型定义):
k(b) ⊆ ⟦p→q⟧
k(c) ⊆ ⟦q→r⟧
f(a) = {b} (bFa)
f(b) = {c} (cFb)

社交网络 (固定的):

(结果)

完全性

完结表列 (Finished Tableau) 不含 $[a!]$ 算子的公式在表列展开过程中复杂度会降低，因而存在有穷表列并且是可判定的。然而，若包含 $[a!]$ 算子且无法构造反驳表列，则存在无限表列完结地展开所有可能性。

非紧致性 (Non-compactness) 已知 $\mathsf{SAL}$ 逻辑是非紧致的 (Xiong & Ågotnes, 2020)。例如，考虑以下无穷公式集合：
\[\{\langle a!\rangle B_{b}p \wedge \neg B_{b} p \}\cup \{\neg B_{a}\theta ~|~ \theta \text{ 不是重言式 (tautology)}\}\]

非贪婪集合 (Non-greedy Set) 一个公式集合 $H$ 被称为是贪婪的，如果它所涉及的命题变元集合是余有穷的。否则，$H$ 是非贪婪的。

完全性定理 该表列系统对于非贪婪集合是完全的，即对于任意非贪婪公式集合 $H$ 和公式 $\phi$，若 $H\vDash \phi$，则 $H\vdash \phi$。

参考文献

  • Keisler, H. J., J. Robbin and A. Miller (1996). Mathematical logic and computability,
  • Balbiani, P. et al. (2008). “Knowable as Known after an Announcement.”
  • Hansen, J. U. (2010). “Terminating tableaux for dynamic epistemic logics.”
  • Balbiani, P. et al. (2010). “Tableaux for public announcement logic.”
  • Seligman, J., F. Liu, & P. Girard (2013). “Facebook and the Epistemic Logic of Friendship.”
  • Kuijer, B. (2015). “Unsoundness of R□.”
  • Christoff, Z. (2016). “Dynamic Logics of Networks.”
  • Xiong, Z. et al. (2017). “Towards a Logic of Tweeting.”
  • Xiong, Z. & T. Ågotnes (2020). “Arbitrary Propositional Network Announcement Logic.”
  • van Ditmarsch, H. & T. French (2022). “Quantifying over Boolean Announcements.”
  • Zhu, R. (2025). “A finitary axiomatization of arbitrary social announcement logic.”

对完成社交宣告逻辑以及本表列系统较为重要的文献资料。