Reasoning About Group Polarization: From Semantic Games to Sequent Systems

TL;DR

The paper develops a game-theoretic and proof-theoretic framework for formal reasoning about group polarization within the modal logic $PNL$, introducing a semantic game that aligns with Kripke semantics and supports dynamic network reasoning. It then extends to a disjunctive game that aggregates truth across all models, proving adequacy results and deriving a cut-free labeled sequent calculus $oldsymbol{DS}$ (and $oldsymbol{DS}^{cc}$) that mirrors winning strategies. A key innovation is the finite representation of strategies via substitution and fresh nominals, enabling a direct correspondence between strategies and proofs. Dynamic extensions (dPNL) with global link-adding and local link-change modalities are proposed, together with a relational-context sequent system $oldsymbol{dDS}$ to handle model updates. Overall, the work provides a mechanizable, modular approach to reasoning about polarization in networks, with a prototypical tool and clear avenues for future relaxation of symmetry and resource-bbounded reasoning.

Abstract

Group polarization, the phenomenon where individuals become more extreme after interacting, has been gaining attention, especially with the rise of social media shaping people's opinions. Recent interest has emerged in formal reasoning about group polarization using logical systems. In this work we consider the modal logic PNL that captures the notion of agents agreeing or disagreeing on a given topic. Our contribution involves enhancing PNL with advanced formal reasoning techniques, instead of relying on axiomatic systems for analyzing group polarization. To achieve this, we introduce a semantic game tailored for (hybrid) extensions of PNL. This game fosters dynamic reasoning about concrete network models, aligning with our goal of strengthening PNL's effectiveness in studying group polarization. We show how this semantic game leads to a provability game by systemically exploring the truth in all models. This leads to the first cut-free sequent systems for some variants of PNL. Using polarization of formulas, the proposed calculi can be modularly adapted to consider different frame properties of the underlying model.

Figures (6)

• Figure 1: Kripke semantics for PNLDBLP:journals/logcom/PedersenSA21.
• Figure 2: Semantic game given a PNL-model $\mathbb{M}$.
• Figure 3: Rules for the disjunctive game.
• Figure 4: The proof system $\mathbf{DS}$. In the rule init, $\phi_{el}$ denotes an elementary formula. In the rules $(L_{\Diamond^\pm})_1$, $(L_{\Diamond^\pm})_2$, and $(R_{[A]})$, the nominal $j$ is fresh.The rule $R_{\meddiamondminus}$ has the proviso that $i\neq j$. The system $\mathbf{DS}^\textbf{cc}$ also includes the rule $cc$ for reasoning about collectively connected systems.
• Figure 5: Rules for dPNL adding/changing modalities. The rules for $\langle\mathop{\mathrm{\wedge\mkern-15mu\wedge}}\limits\pm\rangle$, and the rules $\mathbf{P}_{\langle\ominus\rangle}$ and $\mathbf{O}_{\langle\ominus\rangle}$ are similar and omitted. The global addition modalities do not necessarily add a new link. In $\mathbf{P}_{\langle \mathop{\mathrm{\wedge\mkern-15mu\wedge}}\limits+ \rangle }$, I (and You in $\mathbf{O}_{\langle \mathop{\mathrm{\wedge\mkern-15mu\wedge}}\limits+ \rangle }$) always have a choice, say $(\mathsf{a},\mathsf{a})\notin \mathsf{R}^{-}$.

Theorems & Definitions (30)

• Lemma 1
• Remark 1
• Definition 1
• Example 1
• Proposition 1
• Definition 2
• Theorem 1
• Proposition 2
• Definition 3
• Definition 4: Disjunctive game