Abstract We develop a system of basic probability reasoning founded on two great logical concepts, Gentzen’s natural deduction systems and Carnap–Popper probability of sentences. Our system makes it possible to manipulate with probabilized sentences and justify their causal relationships: if probabilities of sentences $A$ and $B$ are in $[r,1]$ and $[s,1]$, respectively, then the probability of sentence $C$ belongs to $[t,1]$, i.e. $A^{r},B^{s}\vdash C^{t}$, for $r,s,t\in [0,1]$. We prove that our system is sound and complete with respect to the traditional Carnap–Popper type probability semantics. This approach opens up a new perspective of proof-theoretic treatment of sentence probability, potentially allowing immediate algorithmic use of the pure syntactic convenience of natural deductions in programming.

In order to treat the deduction relation ⊢ in the context of probabilistic reasoning, we introduce a system LKprob(ε) making it possible to work with expressions of the form Γ⊢nΔ⁠, a generalization of Gentzen's sequents Γ⊢Δ of classical propositional logic LK⁠, with the intended meaning that ‘the probability of the sequent Γ⊢Δ is greater than or equal to 1−nε’, for a given small real ε>0 and any natural number n⁠. The system LKprob(ε) can be considered a program inferring a conclusion of the form Γ⊢nA from a finite set of hypotheses of the same form Γi⊢niAi(1≤i≤n)⁠. We prove that our system is sound and complete with respect to the Carnap–Popper–type probability models.