REVIEW 5 major objections 8 minor 19 references
Inferentialist Public Announcement Logic: Base-extension Semantics
T0 review · 5 major / 8 minor · reviewed 2026-08-12 · deepseek-v4-flash
Pith's one-line read This paper presents a base-extension semantics for public announcement logic and proves it sound and complete with respect to the PAL axiomatic system.
desk verdict Genuinely new base-extension semantics for PAL with a real conceptual payoff, but the completeness proof has an unlicensed step and the key update lemma is sketched—worth refereeing, needs repair. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The machinery is the notion of a modal relation on bases (Definition 11), a binary relation $R_a$ between bases satisfying conditions (a)--(d) that control interaction with the subset relation and separate consistent from inconsistent bases; together with update sets (Definition 14), which add reachability and finiteness structure so that updates can always be performed. Announcements act on these relations: Definition 17 defines an effective update $R'_A$ of $R_A$ by $\phi$ at $B$ as an update set on an extended atom language whose reachable base pairs mirror the old relation restricted to bases supporting $\phi$, and Definition 24 constructs such an update explicitly using new atoms $p_\emptyset,p_i$ and the function $\delta_{\pi^+}$. The support relation (Definition 18) then evaluates $[\phi]\psi$ by quantifying over supersets and effective updates. This construction carries the soundness proof because Lemma 6 and Lemma 7 guarantee the updated relations are still modal relations and genuinely effective.
What would settle it
A concrete way to test the claim would be to take a small update set (for example, bases $B',C',B,C$ with $\phi$ holding at $B',B,C$ but not $C'$, as in the paper's Figure 9), compute the relation $R^+_{a|\phi}$ of Definition 24, and check directly whether it satisfies the Euclidean condition and conditions (c) and (d) of Definition 11 for all subsets and supersets; a single failure would refute Lemma 6 and collapse the soundness theorem. Alternatively, one could search for a PAL formula that is valid in the Kripke semantics but not supported by the base-extension semantics, which would refute Theorem 4.
Extended reading notes
Core claim
The paper claims that for every formula $\phi$ of PAL, $\vdash\phi$ iff $\Vdash\phi$: the arguments in the paper establish soundness (Theorem 3, every provable formula is supported at every base under every update set) and completeness (Theorem 4, every supported formula is provable in the PAL axiomatization, via the standard translation $t$ from PAL to S5 combined with S5 completeness). The key move is to treat an announcement $[\phi]$ not as deleting bases but as transforming the modal relations $R_a$ into a family of possible 'effective updates' $R_a|_{\phi}^{B}$, depending on the base $B$ at which the announcement is evaluated. Announcements therefore cease to be partial functions in this semantics, yet Lemma 8 shows all effective updates agree on formulae in the original language, so announcement validity is still well defined.
Load-bearing premise
The paper assumes that the explicit update construction of Definition 24, applied to any existing update set at a base where the announced formula holds, always produces relations satisfying the four modal-relation conditions of Definition 11 and the update-set conditions of Definition 14; the proof of this (Lemma 6) is a sketch, with the Euclidean case left as 'analogous'.
Editorial extensions
If this is right
- The base-extension semantics for PAL is sound and complete, so proof-theoretic validity captures the full dynamic logic of truthful public announcements.
- Announcements in this semantics are not unique updates: the same announcement at different bases produces different modal relations, but Lemma 8 ensures that any choice of effective update gives the same verdict on formulae in the original language.
- The card-game and muddy-children analyses provide minimal base set-ups: any extension of those bases preserves the expected conclusions, and the muddy-children case shows that 'not muddy' must be positively supported rather than merely absent.
- The completeness proof by translation gives a compositional reduction of PAL back to S5, so the dynamic announcement axioms are exactly what is needed to eliminate announcement operators in the base-extension setting.
Reading between the lines
- If soundness and completeness hold for PAL, the same update-relations technology is a plausible starting point for action model logic, where agents' uncertainty about which action occurred could be encoded as uncertainty between candidate modal relations.
- The dependence of effective updates on the base suggests an intensional notion of informational equivalence: two updates can be semantically equivalent for the original language while differing on atoms added during the update; making this precise could connect to unsuccessful announcements and common knowledge.
- The authors' explicit positive encoding of negative facts in the muddy children example invites a testable modelling principle: in base-extension models of epistemic puzzles, every frame assumption that a modeller would 'build into' the Kripke valuation must appear as base rules or positive support conditions, otherwise announcements misfire.
- It would be a natural extension to check whether the muddy-children observation scales: for $n$ children and $m$ muddy children, requiring explicit support of all negated $m_j$ at the appropriate bases should let the $m$-step solution be reproduced in this semantics.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper develops a base-extension semantics (B-eS) for public announcement logic (PAL). Extending the authors' earlier B-eS for multi-agent S5, it evaluates formulas at bases (sets of atomic rules) connected by 'modal relations', and it interprets announcements [φ]ψ as updates of those modal relations rather than as deletions of worlds. Because restricting a modal relation to bases that agree on φ need not yield a modal relation, the authors introduce 'effective updates' (Definition 17) and allow the same announcement to produce several possible updated relation sets, so that [φ] is a genuinely box-like operator. The main theorems are Theorem 3 (soundness: ⊢φ implies ⊩φ) and Theorem 4 (completeness: ⊩φ implies ⊢φ), the latter via a translation t: PAL → S5. The paper closes with an analysis of the three-player card game and the muddy children puzzle; a distinctive claim is that the muddy-children reasoning requires bases to support negative information ('Anne is not muddy') rather than merely failing to support 'Anne is muddy'.
Significance. If the technical results can be repaired, this is the first base-extension semantics for a dynamic epistemic logic and a nontrivial extension of proof-theoretic semantics from static modal logics to epistemic actions. The innovation of evaluating announcements against a set of 'effective updates' is well motivated by the concrete failure example in Section 5 and gives announcements a genuinely intensional reading. The two case studies are a strength: Propositions 2 and 3 turn the muddy-children example into testable claims about which base rules must be explicit, and the authors are careful to disclaim strong minimality. There are no machine-checked proofs or executable artifacts; the paper's value is conceptual, and its central claims are currently gated because the completeness proof contains an unlicensed step and the update construction (Lemma 6) is verified only in sketch form.
major comments (5)
- [Section 5, proof of Theorem 4] The proof of Theorem 4, the completeness of the base-extension semantics for PAL, is circular as written. After assuming ⊩φ, the proof states 'By Theorem 3 and Lemma 21, we get ⊢φ↔t(φ)'. Theorem 3 is soundness (⊢ψ ⇒ ⊩ψ), and Lemma 21 gives only the semantic equivalence ⊩φ↔t(φ); their conjunction licenses at most ⊩t(φ), never ⊢φ↔t(φ). To conclude ⊢φ from ⊢S5 t(φ), the syntactic translation lemma ⊢PAL φ↔t(φ) is required, and it is neither stated nor proved; it cannot be derived from the semantic lemma without assuming the very completeness that Theorem 4 is meant to establish. The repair is straightforward and the infrastructure is present: the axioms of Definition 8 are biconditionals, and the complexity inequalities of Lemma 20 are exactly those needed for an induction on c(φ) (Definition 26) proving ⊢PAL φ↔t(φ). The proof of Theorem 4 should be rewritten around this syntactic lemma. Note also that citing Theorem 1 for the S5 completeness of t(φ) is imprecise: since PAL-validity of announcement-free formulas is stated relative to update sets (Definition 15), Theorem 2 is the relevant completeness result, and the coincidence of the two validity notions on announcement-free formulas should be stated explicitly.
- [Section 5, Lemma 6 and Definitions 20–24] Lemma 6 is the linchpin of the update semantics: it asserts that the relation R+_{A|φ} built in Definition 24 is an S5-modal relation and an update set, and it underpins Corollary 1, Lemma 7, Lemma 17, and hence the soundness of the announcement axioms. As written, its proof is a sketch with several unverifiable steps. (a) The Euclidean case is dismissed with 'follows analogously'; because clause (3) of Definition 24 requires compatibility of two bijections f and g, the Euclidean composition argument needs to be written out as it is (partially) for transitivity. (b) In the proof of modal-relation condition (c) of Definition 11, the text writes δπ+(B+) = {δ | δ ⊂ S*_{A|φ} and B+ ∈ δ}, but Definition 23 defines the elements of δπ+(·) as collections of blocks π+_i of π+; under the definition as written, the displayed identity is not meaningful, and neither is the instruction to obtain C′ 'by simply adding rules'. (c) The verification of the update-set condition claims that (C′′−r), ((C′′−r)−r′), and (C′′−r′) belong to π+_i, but membership in π+_i requires membership in the domain/range of S*_{a|φ}; the proof does not show that removing rules from bases in S*_{a|φ} preserves this membership, which is precisely where condition (d) of Definition 11 must be invoked. (d) The proof uses the symbol δw(C′), which is never defined in the main text. The construction of Definitions 21–24 and the verification of Lemma 6 should be presented in full.
- [Definition 18, clause for Kaφ with non-empty Δ] The definition of support for Kaφ after an announcement is type-incoherent as written. The clause reads: 'if Δ is non-empty, then for all C⊇B, R′_A∈RA|ΔC, updates C+ of C and C′ s.t. R′_aC+C′, ⊩^Δ_{C′,RA}φ'. By Definition 17, R′_a is a relation on the extended base set Ω_{P′}, so the target C′ is an updated base in Ω_{P′}; but the support relation in the conclusion is evaluated with the original update set RA, which is defined on Ω_P. The support relation of Definition 18 is only defined for bases in the language of the ambient update set, so the clause as written has no defined meaning. The intended reading is presumably ⊩^Δ_{C′,R′_A}φ, which would be consistent with Lemma 8 (where support after an effective update is evaluated with the updated relations in the subscript); alternatively the paper must explain how RA is extended to Ω_{P′} and why the choice of the particular effective update does not matter. Because the proof of the announcement-and-knowledge axiom in Lemma 18 unpacks this clause directly, the definition and that proof need to be aligned and stated precisely.
- [Section 5, Lemma 17] Lemma 17, the equivalence used to prove the announcement-and-knowledge axiom [φ]K_aψ ↔ φ→K_a[φ]ψ in Lemma 18, is not proved as written. The two conditions are stated with different and partially implicit quantifier structures, and neither direction is checked against Definition 17 clause 3. In the direction from 1 to 2, the proof derives from (1) a particular pair C⊇B and D with R_aCD, applies condition (d) to obtain X⊆D with R_aBX, and then concludes the universal statement 'for all X s.t. R_aBX and Y⊇X, if ⊩_{Y,RA}φ then ⊩^φ_{Y,RA}ψ'; the step from the particular D to the universal quantification over all Y⊇X is not justified, and the proof never passes from the given X of (2) to the C,D of (1). In the direction from 2 to 1, the proof starts from X (with R_aBX) and Y⊇X, obtains C⊇B with R_aCY by symmetry and condition (c), and asserts that an effective update R′_A connects C+ and Y+; by Definition 17 clause 3 this requires ⊩_{C,RA}φ in addition to R_aCY and ⊩_{Y,RA}φ, which is not established. A correct proof of 2→1 would instead apply condition (d) to R_aCD with the subset B⊆C, yielding X⊆D with R_aBX, and then invoke (2) with Y=D using ⊩_{D,RA}φ, which is available from Definition 17 clause 3. Please restate Lemma 17 with explicit quantifier prefixes and supply both directions.
- [Section 4 (Theorems 1–2) and Appendix A] The soundness and completeness theorems of this paper rest on the S5 base-extension results, but the proof layer below Lemma 6 is not fully available to the reader. Theorem 1 is imported from the authors' companion paper [7]; Theorem 2, the update-set variant that the PAL semantics actually uses, delegates both directions to [7], with the update-set adaptation of one direction relegated to Appendix A. The appendix is itself a sketch: it repeats the hand-wave 'The Euclidean case follows analogously', it invokes an undefined atom q_w ('By Lemma 5, we know there is a maximally-consistent C ⊇ A_w s.t. ⊩C q_w'), and the verification of the final update-set clause for sub- and supersets is compressed into a single paragraph whose key claim (reachable bases must have δ_W of equal length) is asserted rather than proved. Since Theorem 4 applies S5 completeness to the translation t(φ) and since Lemma 6's proof explicitly mimics the appendix construction, the completeness chain is only as solid as this appendix. The authors should either re-prove the S5 update-set results in full or restructure the presentation so that the foundational layer is self-contained and verifiable.
minor comments (8)
- [Section 1, third paragraph] Two consecutive sentences refer to 'the first [6]' and 'the second [6]', although they describe two different papers; the second citation should presumably be [7].
- [Reference list, item [1]] The Baltag–Moss–Solecki entry is corrupted: 'S/suppress lawomir Solecki' should read 'Sławomir Solecki'.
- [Definitions 12, 15, and 18] The clause for implication is written as '⊩_{B,RA} ϕ→ψ iff ϕ ⊩_{B,RA} ψ', which silently invokes the nonempty-Γ clause (with Γ={ϕ}) defined only afterwards; reordering the clauses, or writing '{ϕ} ⊩_{B,RA} ψ', would remove a real source of confusion.
- [Definition 18, final validity clause] The last sentence of Definition 18 quantifies over 'sets of S5-modal relations RA', although both the opening of that definition and Definition 15 restrict attention to update sets; this appears to be a slip.
- [Section 6.1, Proposition 1] The conclusion of Proposition 1 is written with the turnstile '⊢B012,RA [¬1a]Kc(0a∧1b∧2c)'; since the claim is about support at a base, the symbol should be '⊩B012,RA'.
- [Section 5, Lemma 20] The proof of Lemma 20 contains typographical errors: 'c([ϕ]ψ→χ)' should read 'c([ϕ](ψ→χ))', and 'c([ϕ][ψ]χ) = (2+c(ϕ))×((2+c(ψ))×c(χ)' together with the following displayed line are missing closing parentheses.
- [Section 2.2 and Section 5] The text contains a number of small language slips, e.g., 'any formula that is false on a Kripke modal' (should be 'Kripke model'), 'so used to proof the same' (should be 'prove'), and Lemma 14 begins 'We proof this by induction' (should be 'prove').
- [Definition 22] The definition of C+ (the update of a base) is barely comprehensible as printed; the ranges of the indices in 'p′_0,...,p′_i ⇒ p_∅' and in '{p_1,...,p_n}\{p_k}' and the role of the added rules should be explained in prose, since this construction is the heart of Lemma 6.
Circularity Check
Theorem 4's completeness proof is circular: it converts the semantic equivalence ⊩ϕ↔t(ϕ) into the syntactic equivalence ⊢ϕ↔t(ϕ) using a soundness theorem that only licenses the reverse direction.
-
other
[Section 5, proof of Theorem 4]
"Assume ⊩ ϕ. By Theorem 3 and Lemma 21, we get ⊢ ϕ↔ t(ϕ). Since t(ϕ) does not contain any announcement formulae andS5 is complete (see Theorem 1), we have⊢S5 t(ϕ). Since PAL is an extension of S5, we also have ⊢t(ϕ) and so⊢ϕ."
Theorem 3 is the soundness direction only: it licenses passing from ⊢ψ to ⊩ψ. Lemma 21 supplies only the semantic biconditional ⊩ϕ↔t(ϕ). From these two facts one cannot infer the syntactic biconditional ⊢ϕ↔t(ϕ); doing so is exactly to invoke the completeness statement being proved, namely that semantic validity implies provability. The later appeal to S5 completeness for t(ϕ) does not help, because without ⊢PAL ϕ↔t(ϕ) the provability of t(ϕ) does not transfer to ϕ. The paper does not prove ⊢PAL ϕ↔t(ϕ) separately, so the main completeness theorem is not established as written; the argument reduces to its own target. The gap is repairable by an induction using Definition 26 and Lemma 20, but the text as it stands is circular.
full rationale
The paper contains substantial new PAL-specific content—effective updates, support clauses for announcements, and the worked examples—so this is not a bare renaming of a known result, and the standard translation from PAL to S5 is a legitimate strategy. However, the proof of Theorem 4 contains a genuine circular step: after assuming ⊩ϕ, it claims that Theorem 3 and Lemma 21 yield ⊢ϕ↔t(ϕ). Theorem 3 is only soundness (⊢⇒⊩), and Lemma 21 gives only the semantic biconditional; the move to the syntactic biconditional is precisely the completeness direction the theorem is supposed to establish. Without an independent proof of ⊢PAL ϕ↔t(ϕ), the main completeness claim is unproven as written. Other concerns are not circular in the same way: the reliance on the authors' earlier S5 completeness theorem [7] is a load-bearing citation, but it concerns S5 rather than the PAL target, and the appendix adapts that construction rather than assuming the present result. The sketchiness of Lemma 6 is a completeness gap rather than a circularity. Overall, the central derivation has a circular step, but the surrounding framework has independent content, so the score is high but not maximal.
Assumptions & free parameters
assumptions (3)
- standard math The axiomatic system for S5 (Definition 4) is sound and complete with respect to S5 Kripke semantics.
- domain assumption The base-extension semantics for S5 (with and without update sets) is sound and complete, as established in [7].
- domain assumption Every base in an update set has a finite partition πB satisfying the conditions of Definition 14.
invented entities (3)
-
Effective update R_A|φB
-
Updated bases C+ (Definition 22)
-
δπ+ function (Definition 23)
Cite this review
Pith. "Pith review of Inferentialist Public Announcement Logic: Base-extension Semantics." pith.science (2026). https://pith.science/paper/HNV5PBUL
@misc{pith2026241115775,
author = {Pith},
title = {Pith review of: Inferentialist Public Announcement Logic: Base-extension Semantics},
year = {2026},
howpublished = {\url{https://pith.science/paper/HNV5PBUL}},
note = {Machine review of arXiv:2411.15775}
}
abstract
Proof-theoretic semantics, and base-extension semantics in particular, can be seen as a logical realization of inferentialism, in which the meaning of expressions is understood through their use. We present a base-extension semantics for public announcement logic, building on earlier work giving a base-extension semantics for the modal logic $S5$, which in turn builds on earlier such work for $K$, $KT$, $K4$, and $S4$. These analyses rely on a notion of `modal relation' on bases. The main difficulty in extending the existing B-eS for $S5$ to public announcement logic is to account announcements of the form $[\psi]\phi$, which, in this setting, update the modal relations on bases. We provide a detailed analysis of two classical examples, namely the three-player card game and the muddy children puzzle. These examples illustrate how the inferentialist perspective requires fully explicit information about the state of the participating agents.
Reference graph
Works this paper leans on
-
[7]
Timo Eckhardt and David J. Pym. Base-extension semantics for S5 modal logic. Logic Journal of the IGPL , 2025
work page 2025
-
[1]
Moss, and S/suppress lawomir Solecki
Alexandru Baltag, Lawrence S. Moss, and S/suppress lawomir Solecki. The Logic of Public Announcements, Common Knowledge, and Private Suspicions. In I. Gilboa, edi- tor, Proceedings of the 7th Conference on Theoretical Aspects of Rationality and Knowledge, pages 43–56, 1998
work page 1998
-
[2]
Making It Explicit: Reasoning, Representing, and Discursive Commitment
Robert Brandom. Making It Explicit: Reasoning, Representing, and Discursive Commitment. Harvard University Press, Cambridge, Mass., 1994
work page 1994
-
[3]
Articulating reasons: An introduction to inferentialism
Robert Brandom. Articulating reasons: An introduction to inferentialism . Harvard University Press, 2009
work page 2009
-
[4]
Hans van Ditmarsch, Wiebe van der Hoek, and Barteld Kooi. Dynamic Epistemic Logic. Springer Publishing Company, Incorporated, 1st edition, 2007
work page 2007
-
[5]
The logical basis of metaphysics
Michael Dummett. The logical basis of metaphysics . Duckworth, London, 1991
work page 1991
-
[6]
Timo Eckhardt and David J. Pym. Base-extension semantics for modal logic. Logic Journal of the IGPL , 2024
work page 2024
-
[8]
On an inferential semantics for classical logic
David Makinson. On an inferential semantics for classical logic. Logic Journal of the IGPL, 22(1):147–154, 2014
work page 2014
Show all 19 references
-
[9]
Meyer, J.-J. Ch. and Hoek, W. van der.Epistemic Logic for AI and Computer Sci- ence. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1995
1995
-
[10]
Completeness in Proof-Theoretic Semantics , pages 231–251
Thomas Piecha. Completeness in Proof-Theoretic Semantics , pages 231–251. Springer International Publishing, Cham, 2016
2016
-
[11]
The definitional view of atomic systems in proof-theoretic semantics
Thomas Piecha and Peter Schroeder-Heister. The definitional view of atomic systems in proof-theoretic semantics. In The Logica Yearbook 2016. Universit¨ at T¨ ubingen, 2017
2016
-
[12]
Incompleteness of intuitionistic propositional logic with respect to proof-theoretic semantics
Thomas Piecha and Peter Schroeder-Heister. Incompleteness of intuitionistic propositional logic with respect to proof-theoretic semantics. Studia Logica, 107(1):233–246, 2019
2019
-
[13]
Ideas and results in proof theory
Dag Prawitz. Ideas and results in proof theory. In J.E. Fenstad, editor, Proceed- ings of the Second Scandinavian Logic Symposium, volume 63 of Studies in Logic and the Foundations of Mathematics , pages 235–307. Elsevier, 1971
1971
-
[14]
Meaning approached via proofs
Dag Prawitz. Meaning approached via proofs. Synthese, 148:507–524, 2006
2006
-
[15]
An Inferentialist Interpretation of Classical Logic
Tor Sandqvist. An Inferentialist Interpretation of Classical Logic. Uppsala prints and preprints in philosophy. Univ., Department of Philosophy, 2005
2005
-
[16]
Classical logic without bivalence
Tor Sandqvist. Classical logic without bivalence. Analysis, 69(2):211–218, 2009
2009
-
[17]
Base-extension semantics for intuitionistic sentential logic
Tor Sandqvist. Base-extension semantics for intuitionistic sentential logic. Logic Journal of the IGPL , 23(5):719–731, 2015
2015
-
[18]
Validity concepts in proof-theoretic semantics
Peter Schroeder-Heister. Validity concepts in proof-theoretic semantics. Synthese, 148(3):525–571, 2006
2006
-
[19]
Proof-Theoretic versus Model-Theoretic Consequence
Peter Schroeder-Heister. Proof-Theoretic versus Model-Theoretic Consequence. In Michal Pelis, editor, The Logica Yearbook 2007. Filosofia, 2008. 40 A Proof Details Elided in Main Text This construction is an adaptation of the proof of Soundness for S5 base-extension semantics ...
2007
Reviewed August 12, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.