The Logic ILP for Intuitionistic Reasoning About Probability

We offer an alternative approach to the existing methods for intuitionistic formalization of reasoning about probability. In terms of Kripke models, each possible world is equipped with a structure of the form < H, mu > that needs not be a probability space. More precisely, though H needs not be a Boolean algebra, the corresponding monotone function (we call it measure) mu : H -> [0, 1] (Q) satisfies the following condition: if alpha,beta, alpha Lambda beta, alpha Lambda beta is an element of H, then mu(alpha V beta) = mu(alpha) + mu(beta) - mu(alpha Lambda ss). Since the range of mu is the set [0, 1] Q of rational numbers from the real unit interval, our logic is not compact. In order to obtain a strong complete axiomatization, we introduce an infinitary inference rule with a countable set of premises. The main technical results are the proofs of strong completeness and decidability.

Automated summary

The paper introduces a new approach to intuitionistic formalization of reasoning about probability, utilizing Kripke models and a measure function satisfying specific conditions. In order to achieve strong completeness, an infinitary inference rule with a countable set of premises is introduced. The main technical results are proofs of strong completeness and decidability.