Abstract We introduce an extension of classical probabilistic propositional logic $\mathsf{LPP}_{1}$, understood as an extension of classical propositional calculus with real-valued probability functions and iterated probability operators, by incorporating similarity operators based on the Jaccard index. The binary operators $J_{\geqslant s}(\alpha ,\beta )$ and $J_{\leqslant s}(\alpha ,\beta )$ allow us to formally reason about the degree of similarity between propositions, defined through the ratio of the probability of their conjunction and the probability of their disjunction. This addition enriches the expressive power of probabilistic logic and provides a natural way to capture relationships between formulas that go beyond absolute probability. We present the syntax and semantics of the resulting system $\mathsf{LP}_{J}$, establish a sound and complete axiomatization, and prove decidability by reducing satisfiability problems to finite systems of linear inequalities over real closed fields. The logic thus provides a mathematically robust framework that combines probability and similarity, with potential applications in artificial intelligence, knowledge representation and decision-making, especially in contexts where clustering and comparison of structured knowledge are essential.

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.

The aim of this article is developing a formal system suitable for reasoning about the distance between propositional formulas. We introduce and study a formal language which is the extension of the classical propositional language obtained by adding new binary operators D ≤s and D ≥s , s ∈ Range, where Range is a fixed finite set. In our language it is allowed to make formulas of the form D ≤s ( α; β) with the intended meaning ’distance between formulas α and β is less than or equal to s’. The semantics of the proposed language consists of possible worlds with a distance function defined between sets of worlds.