ARQNL 2026

A Sound and Weakly Complete
Tableau System for
Social Announcement Logic

Dr. Rui Zhu (祝瑞)

University of Auckland (Graduated in May 2026)

6th International Workshop on Automated Reasoning in Quantified Non-Classical Logics
24 July 2026 · Online talk

Motivation

Social Announcements

Can we build a logic for reasoning about communication constrained by social-network structure?

Genie is blue

🡹

 If Genie is blue, he has long eyelashes.

🡸

If Genie is blue, then he has a perfectly round head.

❓❓❓

If there is a blue creature with a perfectly round head, then it must be me!

The logic

Three kinds of social announcement

Free

$[a:\theta]\varphi$

After agent $a$ sends $\theta$ to its followers, $\varphi$ holds.

No precondition.

Explicit sincere

$\langle a!\theta\rangle\varphi$

Agent $a$ believes the message $\theta$, announces it, and then $\varphi$ holds.

Arbitrary sincere

$\langle a!\rangle\varphi$

There is some propositional message believed by $a$ whose announcement makes $\varphi$ true.

Formal setup

Framework

Language of SAL. Let $\mathsf A$ be a finite set of agents and $\mathsf{Prop}$ the set of propositional variables. A message is generated by \[L_{\mathsf{msg}} \owns\theta ::= p\mid\neg\theta\mid(\theta\wedge\theta).\] The language $L_{\mathsf{SAL}}$ is generated by \[\phi ::= B_a\theta\mid\neg\phi\mid(\phi\wedge\phi)\mid[a:\theta]\phi\mid\langle a!\theta\rangle\phi\mid\langle a!\rangle\phi.\]

Denotation $\llbracket\cdot\rrbracket: L_{\mathsf{msg}}\to 2^{V}$

\[\begin{aligned} V&=2^{\mathsf{Prop}},\\ \llbracket p\rrbracket&=\{x\in V\mid p\in x\},\\ \llbracket\neg\theta\rrbracket&=V\setminus\llbracket\theta\rrbracket,\\ \llbracket\theta_1\wedge\theta_2\rrbracket&=\llbracket\theta_1\rrbracket\cap\llbracket\theta_2\rrbracket. \end{aligned}\]

Model $M = (f, k)$

\[\begin{aligned} (f,k)\vDash B_a\theta &\iff k(a)\subseteq\llbracket\theta\rrbracket,\\ (f,k)\vDash[a:\theta]\phi &\iff(f,[a:\theta]k)\vDash\phi,\\ [a:\theta]k(b)&=\begin{cases}k(b)\cap\llbracket\theta\rrbracket,&b\in f(a),\\k(b),&\text{otherwise},\end{cases}\\ (f,k)\vDash\langle a!\theta\rangle\phi &\iff k(a)\subseteq\llbracket\theta\rrbracket\ \&\ (f,[a:\theta]k)\vDash\phi,\\ (f,k)\vDash\langle a!\rangle\phi &\iff \exists\theta\,[k(a)\subseteq\llbracket\theta\rrbracket\ \&\ (f,[a:\theta]k)\vDash\phi]. \end{aligned}\]

Semantics

Models, satisfaction, and model change

Network $f$

Epistemic distribution $k$

After $a$ announces $r$

Satisfaction

Before:
$M\vDash B_a(p\wedge r)$ and $M\nvDash B_a q$.
$M\vDash B_bp$ and $M\nvDash B_br$.
$M\vDash B_{c}\neg q$ and $M\nvDash B_{c}p$.
$M\vDash B_{d}(q \vee r)$ and $M\nvDash B_{d}r$ .

After:
$[a:r]M\vDash B_br\wedge B_cp\wedge\neg B_dr$.

Hilbert system

Base system: $\mathsf{FSAL}$

Name	Axiom / rule
$\mathsf{Taut}$	All substitution instances of propositional tautologies
$\mathsf{K}_{\top}$	$B_a\theta$ whenever $\theta$ is a propositional tautology
$\mathsf{K}_B$	$B_a(\theta\to\gamma)\to(B_a\theta\to B_a\gamma)$
$\mathsf{K}_{[:]}$	$[a:\theta](\varphi\to\psi)\to([a:\theta]\varphi\to[a:\theta]\psi)$
$\mathsf{[:]Dual}$	$\neg[a:\theta]\varphi\leftrightarrow[a:\theta]\neg\varphi$
$\mathsf{UMon}$	$B_b\chi\to[a:\theta]B_b\chi$
$\mathsf{SDMon}$	$[a:\theta]B_b\chi\to B_b(\theta\to\chi)$
$\mathsf{RDMon}$	$[a:\gamma]\neg B_b\gamma\to([a:\theta]B_b\chi\to B_b\chi)$
$\mathsf{MP}$	From $\varphi\to\psi$ and $\varphi$, infer $\psi$.
$\mathsf{[:]Nec}$	From $\varphi$, infer $[a:\theta]\varphi$.

Explicit sincerity is reduced by $\langle a!\theta\rangle\varphi\leftrightarrow B_a\theta\wedge[a:\theta]\varphi$.

Full SAL

Finitary axioms for arbitrary sincere announcements

Name	Axiom / rule
$\mathsf K_!$	$[a!](\phi\to\psi)\to([a!]\phi\to[a!]\psi)$
$\mathsf{A!_I}$	$\langle a!\theta\rangle\phi\to\langle a!\rangle\phi$
$\mathsf{Red_!}$	$\langle a!\theta\rangle\phi\leftrightarrow B_a\theta\wedge[a:\theta]\phi$
$\mathsf{Dual_!}$	$\neg[a!]\phi\leftrightarrow\langle a!\rangle\neg\phi$
$\mathsf{Nec_!}$	From $\phi$, infer $[a!]\phi$.
$\mathsf{A!_D}$	From $\langle a!p\rangle\phi\to\psi$, infer $\langle a!\rangle\phi\to\psi$, with $p$ fresh.

Why the fresh rule?

$$\{\langle a!\rangle B_bp\wedge\neg B_bp\}\cup\{\neg B_a\theta\mid\theta\text{ non-tautological}\}$$

SAL is non-compact : the soundness of $\mathsf{A!_D}$ cannot be obtained by a standard compactness argument. Xiong and Ågotnes (2020) therefore use an infinitary system.

Zhu (2025) developed a two-stage model-transformation technique to prove the soundness of $\mathsf{A!_D}$, thereby yielding a finitary axiomatization of SAL.

In the present paper: the same technique validates the $\langle!\rangle$ tableau rule.

Why tableaux?

From an axiomatic system to an analytic tree calculus

Shorter proofs: decompose a target formula directly instead of searching for a Hilbert derivation.
Countermodels: a finished open branch records the network and belief constraints needed for a satisfying model.
Decidability analysis: termination becomes a precise question about formula complexity, fresh witnesses, and message representatives.

Preprocessing. Convert formulas to negation normal form. Network literals $bFa$ and $\neg bFa$ are carried as stable atoms because announcements never change $f$; this avoids repeatedly decomposing trivial network updates.

Tableau calculus

Eight non-trivial extension rules

$[:]_{\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\to\epsilon)$
$cFa$

$[:]_{\widetilde K}$$[\vec{b:\gamma}][a:\theta]\neg B_c\epsilon$

↙ ↘

$[\vec{b:\gamma}]\neg B_c(\theta\to\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$
$p$ fresh on all ancestors

$[!]$$[\vec{b:\gamma}][a!]\phi$

↓

$[\vec{b:\gamma}][a!\theta]\phi$
fairly, for every message $\theta$

Belief closure. A branch closes if it contains $B_a\theta_1,\ldots,B_a\theta_n,\neg B_a\chi$ and $\vdash_0(\theta_1\wedge\cdots\wedge\theta_n)\to\chi$.

Network closure. A branch closes if it contains both $bFa$ and $\neg bFa$.

Proof search

A finished tableau tells us

$$\text{Every branch is contradictory}\quad\Longrightarrow\quad H\text{ is unsatisfiable}. $$

$$\mathfrak B\text{ is finished and open}\quad\Longrightarrow\quad M_{\mathfrak B}\vDash\mathfrak B.$$

A closed tableau (confutation) is a certificate of contradiction.
A finished open branch is a finite description of a countermodel.

Example 1

A confutation

Prove $\langle a!p\rangle\neg B_c r\wedge B_c(p\to r)\to\neg cFa$ by expanding its negation.

Example 2

An open branch and its countermodel

Start with $H=\{[a:p]B_bq,\neg B_bq,B_ar\}$.

$f_{\mathcal{B}}(a) = \{b : bFa \in\mathcal{B} \} ~~~~~~ k_{\mathcal{B}}(a) = \bigcap\{\llbracket \theta\rrbracket : B_{a}\theta \in\mathcal{B} \} $

Metatheory

Main results of the tableau calculus

Soundness

If a finite tableau closes every branch from $H$, then $H$ is unsatisfiable.

Model production

Every finished open branch determines a model satisfying all formulas on that branch.

Weak completeness

If $\vDash\varphi$, then a tableau for $\{\neg\varphi\}$ closes.

No strong completeness claim is made for arbitrary premise sets, because full SAL is non-compact.

Decidability I

Finite vocabulary, terminating tableau

Restrict vocabulary

$P=\mathsf{At}(\varphi)$

Work only with the propositional variables occurring in the input formula.

Preserve truth

$M\vDash\varphi \iff M{\upharpoonright}P\vDash\varphi$

The $P$-reduct preserves the relevant FSAL formulas and explicit updates.

Run tableau

The tableau terminates over $P$. A finished open branch directly yields a P-model satisfying the branch.

Therefore, satisfiability for $\mathsf{FSAL}$ and $\mathsf{ESAL}$ is decidable.

Decidability of full SAL

Fresh propositions may be semantically necessary

$$\chi=\langle a!\rangle B_bp\wedge\neg B_bp\wedge\neg B_ap\wedge\neg B_a\neg p.$$

Only the input atom $p$

Agent $a$ must keep both $p$-valuations possible. Every $p$-formula believed by $a$ is therefore tautological, so it cannot make $b$ believe $p$.

Add one fresh atom $q$

Agent $a$ sincerely announces $q$. Follower $b$ then retains only the world $\{p,q\}$ and comes to believe $p$, although $q$ never occurs in $\chi$.

Can this process be bounded effectively for every input formula?

Conclusion

Takeaways

SAL combines network-directed free updates with fixed and arbitrary sincere announcements.

The tableau calculus is sound, weakly complete, and directly supports countermodel extraction.

FSAL and ESAL admit terminating tableaux; full SAL requires an effective finite-representative theorem.

References and resources

Selected references

Balbiani, P. et al. (2010). “Tableaux for Public Announcement Logic.”
Seligman, J., F. Liu, and P. Girard (2013). “Facebook and the Epistemic Logic of Friendship.”
Christoff, Z. (2016). “Dynamic Logics of Networks.”
Xiong, Z. et al. (2017). “Towards a Logic of Tweeting.”
Xiong, Z. and T. Ågotnes (2020). “Arbitrary Propositional Network Announcement Logic.”
van Ditmarsch, H. and T. French (2022). “Quantifying over Boolean Announcements.”
Zhu, R. (2025). “A Finitary Axiomatization of Arbitrary Social Announcement Logic.” LORI proceedings.
Zhu, R. (2026). “A Sound and Weakly Complete Tableau System for Social Announcement Logic.”

Browser-based SAL simulator / tableau prototype

Open the Tableau Proof Assistant for SAL

https://raycaesar.github.io/Ray.github.io/tree/tree.html

This deck uses local Reveal.js files plus KaTeX and TikZJax for mathematical rendering; it can be opened from the slides repository or GitHub Pages.

QR code for the SAL Tableau Proof Assistant

A Sound and Weakly CompleteTableau System forSocial Announcement Logic