Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Logics with probabilistic team semantics and the Boolean negation

Miika Hannula, Minna Hirvonen, Juha Kontinen, Yasir Mahmood, Arne Meier, Jonni Virtema

TL;DR

This paper analyzes logics in probabilistic team semantics that incorporate Boolean negation, focusing on probabilistic independence logic with negation and the FOPT framework. It establishes that FO(⊥⊥_c, ∼) and SO_R(+,×) are equi-expressive, and introduces entropy atoms to connect probabilistic dependencies with information-theoretic measures, situating these logics within second-order frameworks over real-structure models. The authors map the complexity of satisfiability, validity, and model checking across these logics, showing PSPACE-completeness for FOPT, EXPSPACE/NEXPTIME/3-EXPSPACE hardness for richer logics, and providing translations that relate probabilistic team semantics to metafinite and real-number logics. Overall, the work clarifies the expressive power and computational boundaries of probabilistic team logics with negation, and points to entropy-based dependency notions as fruitful directions for further study. The results deepen the theoretical understanding of how probabilistic dependence concepts can be captured and manipulated within logically rigorous, computationally characterized frameworks.

Abstract

We study the expressivity and the complexity of various logics in probabilistic team semantics with the Boolean negation. In particular, we study the extension of probabilistic independence logic with the Boolean negation, and a recently introduced logic FOPT. We give a comprehensive picture of the relative expressivity of these logics together with the most studied logics in probabilistic team semantics setting, as well as relating their expressivity to a numerical variant of second-order logic. In addition, we introduce novel entropy atoms and show that the extension of first-order logic by entropy atoms subsumes probabilistic independence logic. Finally, we obtain some results on the complexity of model checking, validity, and satisfiability of our logics.

Logics with probabilistic team semantics and the Boolean negation

TL;DR

This paper analyzes logics in probabilistic team semantics that incorporate Boolean negation, focusing on probabilistic independence logic with negation and the FOPT framework. It establishes that FO(⊥⊥_c, ∼) and SO_R(+,×) are equi-expressive, and introduces entropy atoms to connect probabilistic dependencies with information-theoretic measures, situating these logics within second-order frameworks over real-structure models. The authors map the complexity of satisfiability, validity, and model checking across these logics, showing PSPACE-completeness for FOPT, EXPSPACE/NEXPTIME/3-EXPSPACE hardness for richer logics, and providing translations that relate probabilistic team semantics to metafinite and real-number logics. Overall, the work clarifies the expressive power and computational boundaries of probabilistic team logics with negation, and points to entropy-based dependency notions as fruitful directions for further study. The results deepen the theoretical understanding of how probabilistic dependence concepts can be captured and manipulated within logically rigorous, computationally characterized frameworks.

Abstract

We study the expressivity and the complexity of various logics in probabilistic team semantics with the Boolean negation. In particular, we study the extension of probabilistic independence logic with the Boolean negation, and a recently introduced logic FOPT. We give a comprehensive picture of the relative expressivity of these logics together with the most studied logics in probabilistic team semantics setting, as well as relating their expressivity to a numerical variant of second-order logic. In addition, we introduce novel entropy atoms and show that the extension of first-order logic by entropy atoms subsumes probabilistic independence logic. Finally, we obtain some results on the complexity of model checking, validity, and satisfiability of our logics.
Paper Structure (11 sections, 25 theorems, 28 equations, 1 figure, 1 table)

This paper contains 11 sections, 25 theorems, 28 equations, 1 figure, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Probabilistic team semantics
  4. Probabilistic independence logic with Boolean negation
  5. Metafinite logics
  6. Equi-expressivity of ${\mathrm{FO}}(\perp\!\!\!\perp_{\mathrm{c}},\sim)$ and ${\mathrm{SO}}_{\mathbb{R}}(+,\times)$
  7. Probabilistic logics and entropy atoms
  8. Logic for first-order probabilistic dependecies
  9. Complexity of satisfiability, validity and model checking
  10. Conclusion
  11. Acknowledgements

Key Result

proposition thmcounterproposition

Let $\phi$ be any ${\mathrm{FO}}(\perp\!\!\!\perp_{\mathrm{c}},\sim)[\tau]$-formula. Then for any set of variables $V$, any $\tau$-structure $\mathcal{A}$, and any probabilistic team $\mathbb{X}\colon X\to[0,1]$ such that $\operatorname{Fr}(\phi)\subseteq V\subseteq D$,

Figures (1)

  • Figure 1: Landscape of relevant logics as well as relation to some complexity classes. Note that for the complexity classes, finite ordered structures are required. Single arrows indicate inclusions and double arrows indicate strict inclusions.

Theorems & Definitions (45)

  • proposition thmcounterproposition: Locality, DHKMV18
  • proposition thmcounterproposition: DurandHKMV18
  • proposition thmcounterproposition: HannulaHKKV19
  • proposition thmcounterproposition
  • proof
  • definition thmcounterdefinition: $\mathbb{R}$-structures
  • proposition thmcounterproposition
  • proof
  • proposition thmcounterproposition
  • proof
  • ...and 35 more