The Complexity of Satisfiability in Non-Iterated and Iterated Probabilistic Logics

TL;DR

This paper analyzes the computational complexity of satisfiability in non-iterated and iterated probabilistic logics, providing bounds based on the complexity of certain subformulas, with applications to classical propositional and justification logics.

Contribution

It establishes complexity bounds for satisfiability in probabilistic logics, considering nested and non-nested operators, and applies these bounds to classical propositional and justification logics.

Findings

Complexity bounds depend on subformula satisfiability

Tight bounds obtained for classical propositional logic

Results extend to justification logic

Abstract

Let L be some extension of classical propositional logic. The non-iterated probabilistic logic over L, is the logic PL that is defined by adding non-nested probabilistic operators in the language of L. For example in PL we can express a statement like "the probability of truthfulness of A is at 0.3" where A is a formula of L. The iterated probabilistic logic over L is the logic PPL, where the probabilistic operators may be iterated (nested). For example, in PPL we can express a statement like "this coin is counterfeit with probability 0.6". In this paper we investigate the influence of probabilistic operators in the complexity of satisfiability in PL and PPL. We obtain complexity bounds, for the aforementioned satisfiability problem, which are parameterized in the complexity of satisfiability of conjunctions of positive and negative formulas that have neither a probabilistic nor a classical operator as a top-connective. As an application of our results we obtain tight complexity bounds for the satisfiability problem in PL and PPL when L is classical propositional logic or justification logic.