{"id":"b918720c-87a9-4abd-9b97-78afa723907d","arxiv_id":"2504.12546","paper_version":2,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"Safe anonymous public announcements are shown to be exactly public announcements of a new safety modality, with a complete axiomatization and expressivity equivalence among the resulting languages.","lead":"This paper adds a formal model of anonymous public announcements to public announcement logic, distinguishing accidental (pseudo-anonymous) from intentional (safe) announcements. It proves the accidental kind reduces to standard epistemic logic and the safe kind to a new safety modality with a sound and complete axiom system.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Lemma 9's group-assignment function f is defined with arbitrary G⊆N, but the proof of (2) needs f(Δ)∈N3; as printed, the completeness proof has a gap.","rationale":"Reading the paper in good faith, the central reduction in Lemma 3 is sound: the bisimulation between Mϕ‡ and M▲ϕ! is correctly argued, and the fixed-point property of ▲ (Mix) supplies the needed triples of agents. The expressivity comparisons and the slogan 'safe anonymous announcements are exactly public announcements of safety' follow cleanly. The modeling limitation flagged by the reader (no coalitional or distributed knowledge) is explicitly acknowledged in Section 5 and is a boundary of the intended notion, not an internal inconsistency. The single concrete defect I found is in the proof of completeness: Lemma 9 allows f to assign arbitrary subsets G⊆N even though the group-assignment machinery and the proof of (2) require f(Δ)∈N3. This makes the printed proof of Theorem 1 incomplete at a central point. The repair is immediate (choose a triple, which always exists by Mix), so I recommend conditional acceptance rather than rejection; the reader did not identify this issue, hence the disagreement on the weakest assumption.","tokens_in":19976,"tokens_out":39751,"duration_ms":415661,"concrete_test":"Re-verify Lemma 9 with f redefined as: f(Δ) = some H∈N3 such that E_H▲ϕ∈Δ, and ∅ otherwise; existence of H follows from Mix whenever ▲ϕ∈Δ. Then re-run the derivation of (2): for G=f(Δ)∈N3, the universal statement 'for every G∈N3 there is i_G∈G...' applies, and the contradiction argument using Δ∼_{i_G}Θ goes through. If this repaired proof verifies, the defect is a typo; if it fails, completeness requires a deeper fix.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"Theorem 1 (completeness of S▲) depends on Lemma 9, whose proof defines a candidate assignment f by 'f(Δ) = G if E_G▲ϕ ∈ Δ for some G⊆N', choosing arbitrarily among such G. This conflicts with the earlier definition of a group assignment function, which requires f(Δ) ∈ N3 (a triple) whenever f(Δ) is nonempty. The conflict is load-bearing in the proof of (2): after deriving 'for every G∈N3 there is i_G∈G such that Δ∧◇K_{i_G}¬χ is consistent', the proof sets G = f(Δ) and applies that universal statement. If the arbitrary choice made f(Δ) a singleton or pair, the instantiation is invalid. The same issue threatens the left-to-right direction, where f is used to produce f-consistent paths; the path argument in Lemma 8 only works when f supplies triples, because the nested negation of ▲_nϕ quantifies over triples. The gap is local and repairable: whenever E_G▲ϕ holds, the Mix axiom guarantees existence of a triple H with E_H(ϕ∧▲ϕ), hence E_H▲ϕ, so one may define f(Δ) to be some H∈N3. With that correction the proof goes through, but as printed the completeness theorem is not fully established.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper formalizes anonymous public announcements in the DEL tradition, distinguishing pseudo-anonymous announcements [ϕ†] (no assumption about the announcer's intention) from intentional safe announcements [ϕ‡] (common knowledge of the intention to stay anonymous). The pseudo-anonymous operator is shown to be reducible to epistemic logic via action models, and L† and L! are shown to be update incomparable. The central contribution is a new safety modality ▲, defined as a greatest fixpoint over triples of agents, together with the results that [ϕ‡]ψ is equivalent to the public announcement of safety [▲ϕ!]ψ (Lemma 3), that the languages L‡▲, L‡, and L▲ are equally expressive (Corollary 2), and that the proof system S▲ is sound and complete for L▲ (Proposition 3 and Theorem 1).","tokens_in":20272,"tokens_out":8646,"duration_ms":84092,"significance":"If the results stand, the paper provides a clean and useful DEL-based account of anonymous communication, a novel non-normal safety modality, and a complete axiomatization via a canonical-model argument adapted from common knowledge. The expressivity hierarchy and the fixpoint characterization are elegant, and the reduction of safe anonymous announcements to public announcements of safety is a particularly appealing simplification. The paper carefully separates pseudo- from intentional anonymity and connects the framework to k-anonymity and the Russian Cards problem. The proofs are mostly standard and the paper is honest about its assumptions, explicitly listing distributed knowledge and self-referential announcements as future work. One load-bearing step in the completeness proof, however, needs repair before Theorem 1 is fully established; this is the basis of my major comment.","major_comments":[{"comment":"In Lemma 9, the candidate group assignment f is defined by 'f(Δ)=G if E_G▲ϕ∈Δ for some G⊆N' (and similarly in the left-to-right direction), with an arbitrary choice among such G. This conflicts with the definition of a group assignment function before Lemma 8, which requires f(Δ)∈N3 or f(Δ)=∅. The conflict is load-bearing in the proof of (2): after establishing 'for every G∈N3 there is i_G∈G such that Δ∧◇K_{i_G}¬χ is consistent', the proof instantiates with G=f(Δ); if the arbitrary choice produced a singleton or pair, that instantiation is invalid. The same problem affects the use of f-consistent paths in the left-to-right direction, where the path argument in Lemma 8 relies on f assigning triples. The gap is local and repairable: from Δ⊢▲ϕ, the Mix axiom gives E_H▲ϕ for some H∈N3, so f(Δ) can be defined to choose such a triple. As printed, however, Theorem 1 is not fully established.","section":"Section 4.2.2, Lemma 9 and the definition of group assignment function before Lemma 8"}],"minor_comments":[{"comment":"The clause '(s,a)∼′_c (t,b) iff s∼_c b and a=c iff b=c' should read 's∼_c t' instead of 's∼_c b'; as written it compares a state with an agent.","section":"Definition 11"},{"comment":"In the Back direction, the names c and d are reused both as the case parameter and as members of the triple guaranteed by ▲ϕ, which makes the argument unnecessarily hard to follow; renaming the triple members would improve clarity.","section":"Lemma 3, proof"},{"comment":"The reduction argument is compressed: the claim that the AML reduction axioms remain valid in AML▲− and that the process terminates in L▲ is stated rather than proved. This is standard, but a short explanation of why ▲ never appears in the scope of a dynamic modality during the reduction would help.","section":"Lemma 4"},{"comment":"In the formula ϕ := r∧ bKa q∧ bKbKa(¬q∧r)∧Kb p, the symbol 'b' before K_a appears to be a rendering of the diamond ◇_b; this should be typeset consistently to avoid confusion.","section":"Section 3.2, Proposition 2"}],"recommendation":"major_revision","confidential_remarks":"The gap in Lemma 9 is easily fixable along the lines indicated in the major comment, and the rest of the paper is strong and convincing. I would be happy to see a revised version; if the authors repair the definition of f in Lemma 9 to always return triples when nonempty, the completeness proof should go through. The main concern is purely that the proof as printed does not yet fully establish Theorem 1."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"First thing to know: this is a solid DEL paper, not a breakthrough, but it gives a clean logical handle on anonymous public communication. The authors introduce pseudo-anonymous announcements [φ†], intentional anonymous announcements [φ‡], and a safety modality ▲ defined as a greatest fixpoint. Their headline result is Lemma 3: [φ‡]ψ is equivalent to [▲φ!]ψ—a safe anonymous announcement is just a public announcement of safety. That is a nice compression of the Russian Cards intuition, and it is backed by an expressivity chain L‡▲≈L‡≈L▲ and a complete axiomatization S▲.\n\nWhat is actually new: the pseudo-anonymous action model (union over agents with precondition K_aφ), the safety fixpoint over triples, and the update-expressivity incomparability with PAL (Proposition 2). The semantics is well motivated with examples, and the paper is honest about what it does not do—coalition attacks via distributed knowledge are listed as future work. The citation pattern looks appropriate, including the Russian Cards problem and previous work on 'somebody knows'.\n\nThe soft spot you need to know about: Lemma 9, which supports the completeness theorem, has a genuine gap as printed. In the left-to-right direction, f(Δ) is defined as an arbitrary G⊆N with E_G▲φ∈Δ, but the definition of a group assignment function and the proof of the right-to-left direction require f(Δ) to be a triple. The right-to-left proof instantiates a universal over N3 with G=f(Δ); if the arbitrary choice picked a singleton or pair, that step is invalid. The stress-test note is right about this. The good news is the fix is local and obvious: the Mix axiom guarantees a triple exists with E_H▲φ, so define f to pick such a triple. With that correction, the proof goes through. But as it stands, the completeness theorem is not fully established. Other issues are minor: Definition 11 has a typo (s∼_c b should be s∼_c t), Lemma 4 is a sketch, and Proposition 2 is compressed. None of those threaten the main story.\n\nBottom line: this deserves a serious referee. The core ideas are sound, the gap is repairable, and the paper would be a useful addition to the DEL literature. I would suggest asking the authors to fix Lemma 9 and tighten the sketches before publication.","headline":"Worth reading and worth refereeing: the core reduction is clean, but the completeness proof has a small but genuine gap in Lemma 9 that the authors need to fix.","tokens_in":20759,"tokens_out":4252,"would_cite":true,"duration_ms":39728,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":null,"created_at":"2026-08-16T12:29:08.754359+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":null,"supporting_citations":[],"review_version":1}