The paper offers a formalization of reasoning about distributed multi-agent systems. The presented propositional probabilistic temporal epistemic logic |$\textbf {PTEL}$| is developed in full detail: syntax, semantics, soundness and strong completeness theorems. As an example, we prove consistency of the blockchain protocol with respect to the given set of axioms expressed in the formal language of the logic. We explain how to extend |$\textbf {PTEL}$| to axiomatize the corresponding first-order logic.

We study a propositional probabilistic temporal epistemic logic |$\textbf {PTEL}$| with both future and past temporal operators, with non-rigid set of agents and the operators for agents’ knowledge and for common knowledge and with probabilities defined on the sets of runs and on the sets of possible worlds. A semantics is given by a class |${\scriptsize{\rm Mod}}$| of Kripke-like models with possible worlds. We prove decidability of |$\textbf {PTEL}$| by showing that checking satisfiability of a formula in |${\scriptsize{\rm Mod}}$| is (...) equivalent to checking its satisfiability in a finite set of finitely representable structures. The same procedure can be applied to the class of all synchronous |${\scriptsize{\rm Mod}}$|-models. We give an upper complexity bound for the satisfiability problem for |${\scriptsize{\rm Mod}}$|⁠. (shrink)

The main goal of this work is to present the proof-theoretical and model-theoretical approaches to probabilistic logics which allow reasoning about independence and probabilistic support. We extend the existing formalisms [14] to obtain several variants of probabilistic logics by adding the operators for independence and confirmation to the syntax. We axiomatize these logics, provide corresponding semantics, prove that the axiomatizations are sound and strongly complete, and discuss decidability issues.

We introduce a probabilistic extension of propositional 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.

In this article we present a p-adic valued probabilistic logic equation image which is a complete and decidable extension of classical propositional logic. The key feature of equation image lies in ability to formally express boundaries of probability values of classical formulas in the field equation image of p-adic numbers via classical connectives and modal-like operators of the form Kr, ρ. Namely, equation image is designed in such a way that the elementary probability sentences Kr, ρα actually do have their (...) intended meaning—the probability of propositional formula α is in the equation image-ball with the center r and the radius ρ. Due to modal nature of the operators Kr, ρ, it was natural to use the probability Kripke like models as equation image-structures, provided that probability functions range over equation image instead of equation image or equation image. (shrink)

In this article we present a p-adic valued probabilistic logic equation image which is a complete and decidable extension of classical propositional logic. The key feature of equation image lies in ability to formally express boundaries of probability values of classical formulas in the field equation image of p-adic numbers via classical connectives and modal-like operators of the form Kr, ρ. Namely, equation image is designed in such a way that the elementary probability sentences Kr, ρα actually do have their (...) intended meaning—the probability of propositional formula α is in the equation image-ball with the center r and the radius ρ. Due to modal nature of the operators Kr, ρ, it was natural to use the probability Kripke like models as equation image-structures, provided that probability functions range over equation image instead of equation image or equation image. (shrink)

In this paper we present two types of logics and \ ) where certain p-adic functions are associated to propositional formulas. Logics of the former type are p-adic valued probability logics. In each of these logics we use probability formulas K r,ρ α and D ρ α,β which enable us to make sentences of the form “the probability of α belongs to the p-adic ball with the center r and the radius ρ”, and “the p-adic distance between the probabilities of (...) α and β is less than or equal to ρ”, respectively. Logics of the later type formalize processes of thinking where information are coded by p-adic numbers. We use the same operators as above, but in this formalism K r,ρ α means “the p-adic code of the information α belongs to the p-adic ball with the center r and the radius ρ”, while D ρ α,β means “the p-adic distance between codes of α and β are less than or equal to ρ”. The corresponding strongly complete axiom systems are presented and decidability of the satisfiability problem for each logic is proved. (shrink)

A propositional logic is defined which in addition to propositional language contains a list of probabilistic operators of the form P ≥s (with the intended meaning ‘‘the probability is at least s’’). The axioms and rules syntactically determine that ranges of probabilities in the corresponding models are always finite. The completeness theorem is proved. It is shown that completeness cannot be generalized to arbitrary theories.

We offer an alternative approach to the existing methods for intuitionistic formalization of reasoning about probability. In terms of Kripke models, each possible world is equipped with a structure of the form $$\langle H, \mu \rangle $$ that needs not be a probability space. More precisely, though H needs not be a Boolean algebra, the corresponding monotone function (we call it measure) $$\mu : H \longrightarrow [0,1]_{\mathbb {Q}}$$ satisfies the following condition: if $$\alpha $$, $$\beta $$, $$\alpha \wedge \beta $$, (...) $$\alpha \vee \beta \in H$$, then $$\mu (\alpha \vee \beta ) = \mu (\alpha ) + \mu (\beta ) - \mu (\alpha \wedge \beta )$$. Since the range of $$\mu $$ is the set $$[0,1]_{\mathbb {Q}}$$ of rational numbers from the real unit interval, our logic is not compact. In order to obtain a strong complete axiomatization, we introduce an infinitary inference rule with a countable set of premises. The main technical results are the proofs of strong completeness and decidability. (shrink)

In this paper we present two families of probability logics (denoted _QLP_ and \(QLP^{ORT}\) ) suitable for reasoning about quantum observations. Assume that \(\alpha \) means “O = a”. The notion of measuring of an observable _O_ can be expressed using formulas of the form \(\square \lozenge \alpha \) which intuitively means “if we measure _O_ we obtain \(\alpha \) ”. In that way, instead of non-distributive structures (i.e., non-distributive lattices), it is possible to relay on classical logic extended with (...) the corresponding modal laws for the modal logic \({\textbf{B}}\). We consider probability formulas of the form \(CS_{z_{1},\rho _{1}; \ldots ; z_{m},\rho _{m}} \square \lozenge \alpha \) related to an observable _O_ and a possible world (vector) _w_: if _a_ is an eigenvalue of _O_, \(w_{1}\),..., \(w_{m}\) form a base of a closed subspace of the considered Hilbert space which corresponds to eigenvalue _a_, and if _w_ is a linear combination of the basis vectors such that \(w=c_{1}\cdot w_{1}+ \cdots + c_{m}\cdot w_{m}\) for some \(c_{i}\in {\mathbb {C}}\), then \(\Vert c_{1}-z_{1}\Vert \le \rho _{1}\),..., \(\Vert c_{m}-z_{m}\Vert \le \rho _{m}\), and the probability of obtaining _a_ while measuring _O_ in the state _w_ is equal to \(\Sigma _{i=1}^{m}\Vert c_{i}\Vert ^{2}\). Formulas are interpreted in reflexive and symmetric Kripke models equipped with probability distributions over families of subsets of possible worlds that are orthocomplemented lattices, while for \(QLP^{ORT}\) also satisfy ortomodularity. We give infinitary axiomatizations, prove the corresponding soundness and strong completeness theorems, and also decidability for _QLP_-logics. (shrink)

We present a propositional and a first-order logic for reasoning about higher-order upper and lower probabilities. We provide sound and complete axiomatizations for the logics and we prove decidability in the propositional case. Furthermore, we show that the introduced logics generalize some existing probability logics.

We present a propositional and a first-order logic for reasoning about higher-order upper and lower probabilities. We provide sound and complete axiomatizations for the logics and we prove decidability in the propositional case. Furthermore, we show that the introduced logics generalize some existing probability logics.

We give a sound and complete axiomatization of a probabilistic extension of intuitionistic logic. Reasoning with probability operators is also intuitionistic (in contradistinction to other works on this topic), i.e., measure functions used for modeling probability operators are partial functions. Finally, we present a decision procedure for our logic, which is a combination of linear programming and an intuitionistic tableaux method.