Logics for Reasoning about Knowledge and Conditional Probability

Epistemic logics are formal models designed in order to reason about the knowledge of agents and their knowledge of each other’s knowledge. During the last couple of decades, they have found applications in various fields such as game theory, the analysis of multi-agent systems in computer science and artificial intelligence [8, 9, 19]. In parallel, uncertain reasoning has emerged as one of the main fields in artificial intelligence, with many different tools developed for representing and reasoning with uncertain knowledge. A particular line of research concerns the formalization in terms of logic, and the questions of providing an axiomatization and decision procedure for probabilistic logic attracted the attention of researchers and triggered investigation about formal systems for probabilistic reasoning [1, 7, 10, 11, 15, 16]. Fagin and Halpern [6] emphasised the need for combining those two fields for many application areas, and in particular in distributed systems applications, when one wants to analyze randomized or probabilistic programs. They developed a joint framework for reasoning about knowledge and probability, proposed a complete axiomatization and investigated decidability of the framework. Based on the seminal paper by Fagin, Halpern and Meggido [7], they extended the propositional epistemic language with formulas which express linear combinations of probabilities, called linear weight formulas, i.e., the formulas of the form a1w(α1)+...+akw(αk) ≥ r, where aj ’s and r are rational numbers. They proposed a finitary axiomatization and proved weak completeness, using a small model theorem. In this talk, we propose two logics that extend the logic from [6] by also allowing formulas that can represent conditional probability. First we present a propositional logic for reasoning about knowledge and conditional probability from [2]. Then we discuss how to develop its first-order extension. Our languages contain both knowledge operators Ki (one for each agent i) and conditional probability formulas of the form a1wi(α1, β1) + ... + akwi(αk, βk) ≥ r. The expressions of the form wi(α, β) represent conditional probabilities that agent i places on events according to Kolmogorov definition: P(A|B) = P (A∩B) / P (B) if P(B) > 0, while P(A|B) is undefined when P(B) = 0. The corresponding semantics consists of enriched Kripke models, with a probability measure assigned to every agent in each world. Our main results are sound and strongly complete (every consistent set of formulas is satisfiable) axiomatizations for both logics. We prove strong completeness using an adaptation of Henkin’s construction, modifying some of our earlier methods [3, 5, 4, 15, 16]. Our axiom system contains infinitary rules of inference, whose premises and conclusions are in the form of so called k-nested implications. This form of infinitary rules is a technical solution already used in probabilistic, epistemic and temporal logics for obtaining various strong necessitation results [13, 14, 17, 18]. We also prove that our propositional logic is decidable, combining the method of filtration [12] and a reduction to a system of inequalities.