Suppes-style sequent calculus for probability logic

Abstract

In order to treat the deduction relation proves in the context of probabilistic reasoning, we introduce a system LKprob(epsilon) making it possible to work with expressions of the form Gamma proves(n) Delta, a generalization of Gentzen's sequents Gamma proves Delta of classical propositional logic LK, with the intended meaning that 'the probability of the sequent Gamma proves Delta is greater than or equal to 1-n epsilon', for a given small real epsilon > 0 and any natural number n. The system LKprob(epsilon) can be considered a program inferring a conclusion of the form Gamma proves(n) A from a finite set of hypotheses of the same form Gamma(i) proves(ni) A(i) (1 LT = i LT = n). We prove that our system is sound and complete with respect to the Carnap-Popper-type probability models.