A probabilistic extension of intuitionistic logic

Abstract

We introduce a probabilistic extension of prepositional intuitionistic logic. The logic allows making statements such as P ≥s α, with the intended meaning "the probability of truthfulness of α is at least s". We describe the corresponding class of models, which are Kripke models with a naturally arising notion of probability, and give a sound and complete infinitary axiomatic system. We prove that the logic is decidable.