Sequent calculus for classical logic probabilized (Q1712933)

This paper presents a proof-theoretic study on a logic of probability. It introduces a Gentzen-type system \textbf{LKprob}, which is a probabilistic modification of Gentzen's sequent calculus \textbf{LK}. \textbf{LKprob} manipulates sequents of the form \(\Gamma \vdash^b_a \Delta\) to be read as ``the probability of truthfulness of a sequent \(\Gamma \vdash \Delta\) is in the interval \([a, b]\)''. The author characterizes this system as ``a kind of the interval-valued probability sequent calculus'', which allows to construct ``logical inferences dealing with probabilities''. The axioms of the systems are \(\Gamma \vdash^1_0 \Delta\), \(\vdash^0_0\), \(A \vdash^1_1 A\) for any \(\Gamma, \Delta, A\). By calculating probabilities, some additional empirical axioms of the form \(\Gamma \vdash^{b_{i}}_{a_{i}} \Delta\) can be accepted, based, say, on some statistical research. Extending \textbf{LKprob} by such empirical axioms results in a theory suitable for probabilistic reasoning over certain empirical data. \textbf{LKprob}-theory can be equipped with a probabilistic model, which essentially is a map from the set of sequents into a finite subset of reals \([0, 1]\) closed under addition and containing 0 and 1. Soundness and completeness for \textbf{LKprob} with respect to this semantics are proved.