Reasoning About Degrees of Confirmation

Abstract

We present a probabilistic logic for reasoning about degrees of confirmation. We provide a sound and strongly complete axiomatization for the logic. We show that the problem of deciding satisfiability is in PSPACE.

1 Introduction

In the last several decades, different tools are developed for representing and reasoning with uncertain knowledge, including probability as a dominant representation of uncertainty. One particular line of research concerns the formalization in terms of probabilistic logic. The modern development in this field started with Keisler’s seminal work on probabilistic quantifiers [21]. After Nilsson [23] gave a procedure for probabilistic entailment which, given probabilities of premises, calculates bounds on the probabilities of the conclusion, researchers from the areas of logic, computer science and artificial intelligence started investigations about formal systems for probabilistic reasoning and provided several languages, axiomatizations and decision procedures for various probabilistic logics [3, 10, 12, 13, 15,16,17,18,19, 24, 25]. Those logics extend the classical (propositional or first order) calculus with expressions that speak about probability, while formulas remain true or false. They allow one to formalize statements of the form “the probability of $\alpha$ is at least a half.” The corresponding probability operators behave like modal operators and the corresponding semantics consists of special types of Kripke models, with indistinguishability relations replaced with probability measures defined over the worlds.

This paper contributes to the field by proposing a logical formalization of the Bayesian measure of confirmation (or evidential support). Although contemporary Bayesian confirmation theorists investigated degrees of confirmation developing a variety of different probability-based measures, that field attracted little attention from the logical side, probably because of complexity of a potential formal language that would be adequate to capture those measures. In Carnap’s book [2], one of the main tasks is “the explication of certain concepts which are connected with the scientific procedure of confirming or disconfirming hypotheses with the help of observations and which we therefore will briefly call concepts of confirmation”. Carnap distinguished three different semantical concepts of confirmation: the classificatory concept (“a hypothesis A is confirmed by an evidence B”), the comparative concept (“A is confirmed by B at least as strongly as C is confirmed by D”) and the quantitative concept of confirmation. The third one, one of the basic concept of inductive logic, is formalized by a numerical function c which maps pairs of sentences to the reals, where c(A, B) is the degree of confirmation of the hypothesis A on the basis of the evidence B.

Bayesian epistemology proposes various candidate functions for measuring the degree of confirmation c(A, B), defined in terms of subjective probability. They all agree in the following qualitative way: $c(A,B)>0$ iff the posterior probability of A on the evidence B is greater than the prior probability of A (i.e., $\mu (A | B)>\mu (A)$), which correspond to the classificatory concept (“A is confirmed byB”) [14]. Up to now, only the classificatory concept of confirmation is logically formalized, in our previous work [6].

In this paper, we formalize the quantitative concept of confirmation. We focus on the most standard¹ measure of degree of confirmation, called difference measure:

$$ c(A,B)=\mu (A | B)-\mu (A). $$

Our formal language extends propositional logic with the unary probabilistic operators of the form $P_{\ge r}$ ($P_{\ge r}\alpha$ reads “the probability of $\alpha$ is at least r”), where r ranges over the set of rational numbers from the unit interval [24], and the binary operators $c_{\ge r}$ and $c_{\le r}$, which we semantically interpret using the difference measure. The corresponding semantics consists of special types of Kripke models , with probability measures defined over the worlds.

Our main result is a sound and strongly complete (every consistent set of formulas is satisfiable) axiomatization for the logic. We prove completeness using a modification of Henkin’s construction. Since the logic is not compact, in order to obtain strong variant of completeness, we use infinitary inference rules. From the technical point of view, we modify some of our earlier developed methods presented in [4, 5, 7,8,9, 22, 26, 27, 29]. We point out that our languages are countable and formulas are finite, while only proofs are allowed to be infinite. We also prove that our logic is decidable and we present complexity results.

Many measures on confirmation have been proposed over years. We point out that it was not our intention to take sides. We simply chose the difference measure because of its popularity. However, we discuss in Sect. 7 that our axiomatization technique can be easily modified to incorporate other measures of confirmation.

The contents of this paper are as follows. In Sect. 2 we recall the basic notions of probability. In Sect. 3 we present the syntax and semantics of our logic and defined the satisfaction relation. In Sect. 4 we propose an axiomatization for the logic, and we prove its soundness. In Sect. 5 we prove that the axiomatization is strongly complete with respect to the proposed semantics. In Sect. 6 we present complexity results for the problem of deciding satisfiability. We conclude in Sect. 7.

2 Preliminaries

Let us introduce some basic probabilistic notions that will be use in this paper.

For a nonempty set $W\ne \emptyset$, we say that $H\subseteq 2^W$ is an algebra of subsets of W, if the following conditions hold:

• 1. $W\in H$,

• 2. if $A\in H$, then $W\setminus A\in H$, and

• 3. if $A,B\in H$, then $A\cup B\in H$.

For a given algebra H of subsets of W, a function $\mu :H\longrightarrow [0,1]$ is a finitely additive probability measure, if it satisfies the following properties:

• 1. $\mu (W)=1$,

• 2. $\mu (A\cup B)=\mu (A)+\mu (B)$, whenever $A\cap B=\emptyset$.

For W, H and $\mu$ described above, the triple $\langle W, H, \mu \rangle$ is called a finitely additive probability space. The elements of H are called measurable sets.

For a probability measure $\mu$, conditional probability is defined in the following way:

$$\mu (A|B)= \left\{ {\begin{array}{ll} {\frac{\mu (A\cap B)}{\mu (B)},} &{} {\mu (B)>0} \\ {\text {undefined},} &{} {\mu (B)=0.} \\ \end{array} } \right. $$

Note that, as a consequence of this definition, the difference measure $c(A,B)=\mu (A | B)-\mu (A)$ is also not defined when $\mu (B)=0$.

3 The Logic $\mathrm {LPP_2^{conf}}$: Syntax and Semantics

In this section we introduce the set of formulas of the logic $\mathrm {LPP_2^{conf}}$, and the class of semantical structures in which those formulas evaluated.

3.1 Syntax

Let $\mathcal P=\{p,q,r,\dots \}$ be a denumerable set of propositional letters. For given rational numbers a and b such that $a<b$, let $[a,b]_Q$ denotes the set $[a,b]\cap \mathcal {Q}$. The language of the logic $\mathrm {LPP_2^{conf}}$ consists of

• the elements of set $\mathcal P$,

• classical propositional connectives $\lnot$ and $\wedge$,

• the list of unary probability operators of the form $P_{\ge r}$, for every $r\in [0,1]_{Q}$,

• the list of binary probability operators of the form $c_{\ge r}$, for every $r\in [-1,1]_{Q}$, and

• the list of binary probability operators of the form $c_{\le r}$, for every $r\in [-1,1]_{Q}$.

Note that we use conjunction and negation as primitive connectives. The other propositional connectives, $\vee$, $\rightarrow$ and $\leftrightarrow$, are introduced as abbreviations, in the usual way.

The introduced language is used to define two types of formulas of $\mathrm {LPP_2^{conf}}$. First, we have the set of classical propositional formulas over $\mathcal {P}$, denoted here by $For_C$. We will denote the propositional formulas by $\alpha$, $\beta$ and $\gamma$, possibly with subscripts. We denote the satisfiability relation of the classical propositional logic by $\models _{C}$. Now we define the second type of formulas.

Definition 1 (Probabilistic formula)

A basic probabilistic formula is any formula of the form: $P_{\ge r}\alpha$ $c_{\ge r}(\alpha ,\beta )$, $c_{\le r}(\alpha ,\beta )$, where $\alpha ,\beta \in For_C$.

A probabilistic formula is a Boolean combination of basic probabilistic formulas. We denote with $For_P$ the set of all probabilistic formulas and denote arbitrary probabilistic formulas by $\phi$ and $\psi$, possibly with subscripts.

Intuitively, $P_{\ge r}\alpha$ means that the probability that $\alpha$ is true is greater or equal to r, while $c_{\ge r}(\alpha ,\beta )$ ($c_{\le r}(\alpha ,\beta )$) means that the formula $\beta$ confirms the formula $\alpha$ with the degree at least r (at most r, respectively).

Example 1

The meaning of the formula

$$ c_{\ge \frac{1}{2}}(\alpha ,\beta ) \rightarrow c_{\le 0}(\lnot \alpha ,\beta )$$

is that if $\beta$ confirms $\alpha$ to the degree $\frac{1}{2}$, then the degree that $\beta$ confirms the negation of $\alpha$ is less or equal to zero.

The other types of probabilistic operators are usually defined as follows: $P_{<s}\alpha$ is $\lnot P_{\ge s}\alpha$, $P_{\le s}\alpha$ is $P_{\ge 1-s} \lnot \alpha$, $P_{> s}\alpha$ is $\lnot P_{\le s}\alpha$, and $P_{= s}\alpha$ is $P_{\ge s}\alpha \wedge P_{\le s}\alpha$. We use the following abbreviations to introduce other types of confirmation operators:

• $c_=(\alpha ,\beta )$ is $c_\ge (\alpha ,\beta )\wedge c_\le (\alpha ,\beta )$,

• $c_>(\alpha ,\beta )$ is $c_\ge (\alpha ,\beta )\wedge \lnot c_{\le }(\alpha ,\beta )$ and

• $c_<(\alpha ,\beta )$ is $c_\le (\alpha ,\beta )\wedge \lnot c_\ge (\alpha ,\beta )$.

Also, we denote both $\alpha \wedge \lnot \alpha$ and $\phi \wedge \lnot \phi$ by $\bot$ (and similarly for $\top$), letting the context determine the meaning.

One might think that $c_<(\alpha ,\beta )$ might be defined simply as $\lnot c_\ge (\alpha ,\beta )$, in an analogous way as $P_{<s}$ is introduced. However, we will see that this does not hold under our satisfiability relation.

By a formula of $\mathrm {LPP_2^{conf}}$ we mean either a classical of probabilistic formula.

Definition 2

(Formula of $\mathrm {LPP_2^{conf}}$). The set of formulas of $\mathrm {LPP_2^{conf}}$ is

$$For_{\mathrm {LPP_2^{conf}}} = For_C \cup For_P.$$

We denote arbitrary formulas by $\rho$ and $\sigma$ (possibly with subscripts).

Thus, no mixing of pure propositional formulas and probability formulas is allowed.

Example 2

The expression

$$(\beta \rightarrow \alpha ) \rightarrow c_{\ge 0}(\alpha ,\beta )$$

is not a formula of the logic $\mathrm {LPP_2^{conf}}$.

3.2 Semantics of $\mathrm {LPP_2^{conf}}$

Now we define the structures in which we evaluate the formulas from $For_{\mathrm {LPP_2^{conf}}}$.

Definition 3

($\mathrm {LPP_2^{conf}}$-structure). An $\mathrm {LPP_2^{conf}}$-structure is tuple $(W,H,\mu ,v)$ where:

• 1. W is a non- empty set of objects called worlds.

• 2. $v: W\times \mathcal {P}\rightarrow \{ true,false\}$ assigns to each world $w\in W$ a two-valued evaluation $v(w,\cdot )$ of the propositional letters; it is then extended to all elements of $For_C$ in the usual way.

• 3. H is an algebra of subsets of W, such that

  $$\{ w\in W \ | \ v(w,\alpha )=true\}\in H,$$

  for every formula $\alpha \in For_{\mathrm {LPP_2^{conf}}}$.

• 4. $\mu :H\longrightarrow [0,1]$ is a finitely additive measure.

We denote with ${\mathcal M}(\mathrm {LPP_{2}^{conf}})$ the class of all $\mathrm {LPP_2^{conf}}$-structures.

Note that, according to Definition 3, the set of all worlds of an $\mathrm {LPP_2^{conf}}$-structure M in which a classical propositional formula $\alpha$ has the values true is a measurable set. This requirement is crucial to ensure correctness of satisfiability relation. In order to relax the notation, we denote the mentioned set of worlds, $\{ w\in W \ | \ v(w,\alpha )=true\}$, simply by $[\alpha ]_M$. Thus, $[\alpha ]_M\in H$ for every $M\in {\mathcal M}(\mathrm {LPP_{2}^{conf}})$ and every $\alpha \in For_C$. Also, we write $[\alpha ]$ instead of $[\alpha ]_M$ when M is clear from the context.

Next we define the satisfiability of a formula in an $\mathrm {LPP_2^{conf}}$-structure.

Definition 4 (Satisfiability)

Let $M\in {\mathcal M}(\mathrm {LPP_{2}^{conf}})$. The satisfiability relation $\models$ is defined recursively as follows:

• 1. $M \models \alpha$ iff $v(w,\alpha )=true$ for every $w\in W$,

• 2. $M\models P_{\ge r}\alpha$ if $\mu ([\alpha ])\ge r$,

• 3. $M\models c_{\ge r} (\alpha ,\beta )$ if $\mu ([\beta ])>0$ and $\mu ([\alpha ]|[\beta ])-\mu ([\alpha ])\ge r$,

• 4. $M\models c_{\le r} (\alpha ,\beta )$ if $\mu ([\beta ])>0$ and $\mu ([\alpha ]|[\beta ])-\mu ([\alpha ])\le r$,

• 5. $M\models \lnot \phi$ iff $M\not \models \phi$,

• 6. $M\models \phi \wedge \psi$ iff $M\models \phi$ and $M\models \psi$.

According to Definition 4, a classical formula $\alpha$ holds in an $\mathrm {LPP_2^{conf}}$-structure M only if it holds in every world of M, and therefore represent certain information. In that case, the probability value of $[\alpha ]_M$ has to be equal to 1, which will be ensured in the axiomatization by a variant of Necessitation rule.

Using Definition 4 and properties of reals, it is easy to obtain satisfiability for the other types of operators. For example,

• $M\models c_{< r}(\alpha , \beta )$ if $\mu ([\beta ])>0$ and $\mu ([\alpha ]|[\beta ])-\mu ([\alpha ])< r$

holds. Now it is obvious that the operator $c_<$ is not equivalent to “negation of $c_{\ge }$,” i.e., $M\not \models c_{\ge r}(\alpha , \beta )$ does not imply $M\models c_{< r}(\alpha , \beta )$, the reason is that $c([\alpha ],[\beta ])$ might simply be undefined in M (if $\mu ([\beta ])=0$).

At the end of this section, we define some basic semantical notions.

Definition 5 (Model)

For an $M\in {\mathcal M}(\mathrm {LPP_{2}^{conf}})$ and a set of formulas T, we say that M is a model of T and write $M \models T$ iff $M \models \rho$ for every $\rho \in T$. T is satisfiable, if there is $M\in {\mathcal M}(\mathrm {LPP_{2}^{conf}})$ such that $M \models T$.

Now we define the notion of entailment relation between formulas.

Definition 6 (Entailment)

We say that a set of formulas T entails a formula $\rho$ and write $T \models \rho$, if all models of T are models of $\rho$. Furthermore, $\rho$ is valid if $\emptyset \models \rho$.

4 Axiomatization of $\mathrm {LPP_2^{conf}}$

In this section we present an axiomatization of our logic, which we denote $Ax(\mathrm {LPP_2^{conf}})$. The axiom system $Ax(\mathrm {LPP_2^{conf}})$ contains ten axiom schemes and five inference rules. In the following axiomatization, we assume that all the formulas respect Definition 1. For example, we consider only those instances of A9 and A10 for which $s(r+t)\le 1$.

Axiom schemes:

• (A1) All instances of classical propositional tautologies for both $For_C$ and $For_P$.

• (A2) $P_{\ge 0}\alpha$

• (A3) $P_{\leqslant r}\alpha \rightarrow P_{< s}\alpha$ whenever $r< s$

• (A4) $P_{<r}\alpha \rightarrow P_{\leqslant r}\alpha$

• (A5) $(P_{\ge r}\alpha \wedge P_{\ge s}\beta \wedge P_{\ge 1}(\lnot \alpha \vee \lnot \beta )) \rightarrow P_{\ge r+s }(\alpha \vee \beta )$

• (A6) $(P_{\leqslant r}\alpha \wedge P_{<s}\beta )\rightarrow P_{<r+s}(\alpha \vee \beta )$

• (A7) $c_{\ge r}(\alpha ,\beta )\rightarrow P_{> 0}\beta$

• (A8) $c_{\le r}(\alpha ,\beta )\rightarrow P_{> 0}\beta$

• (A9) $(P_{\ge t}\alpha \wedge P_{\ge s}\beta \wedge c_{\ge r}(\alpha ,\beta ))\rightarrow P_{\ge s(r+t)}(\alpha \wedge \beta )$

• (A10) $(P_{\le t}\alpha \wedge P_{\le s}\beta \wedge c_{\le r}(\alpha ,\beta ))\rightarrow P_{\le s(r+t)}(\alpha \wedge \beta )$

Inference rules:

• (R1) From $\{ \rho ,\rho \rightarrow \sigma \}$ infer $\sigma$

• (R2) From $\alpha$ infer $P_{\ge 1} \alpha$.

• (R3) From the set of premises $\{ \phi \rightarrow P_{\ge r-\frac{1}{k}}\alpha \ | \ k\in \mathbb N, k\ge \frac{1}{r} \}$ infer $\phi \rightarrow P_{\ge r}\alpha .$

• (R4) From the set of premises

  $$\{\phi \rightarrow P_{>0}\beta \}\cup \{\phi \rightarrow ((P_{\ge t}\alpha \wedge P_{\ge s}\beta )\rightarrow P_{\ge s(r+t)}(\alpha \wedge \beta ))| t,s\in [0,1]_Q\}$$

  infer $\phi \rightarrow c_{\ge r}(\alpha ,\beta )$.

• (R5) From the set of premises

  $$\{\phi \rightarrow P_{>0}\beta \}\cup \{\phi \rightarrow ((P_{\le t}\alpha \wedge P_{\le s}\beta )\rightarrow P_{\le s(r+t)}(\alpha \wedge \beta ))\ | \ t,s\in [0,1]_Q\}$$

  infer $\phi \rightarrow c_{\le r}(\alpha ,\beta )$.

Let us briefly comment on the axiomatization $Ax(\mathrm {LPP_2^{conf}})$. The axioms A1–A6 and the inference rules R1–R3 form the axiom system for the logic $\mathrm LPP_2$ from [24]. The rule R3 is the so-called Archimedean rule. It ensures that the ranges of probability measures do not take non-standard values (in the sense of non-standard analysis). Intuitively, it claims that if probability is approximately close to r, then it must be r. The axioms A7 and A9, together with the rule R4 properly capture the third condition of Definition 4. Similarly, A8, A10 and R5 properly capture the fourth condition of Definition 4.

The rules R3-R5 are infinitary inference rules. The necessity of employing such rules comes form the non-compactness phenomena. Indeed, it is known that in real-valued probabilistic logic there exist inconsistent infinite sets of formulas, such that every finite subset is consistent. As pointed out in [20], one consequence of that fact is that any finitary axiomatization would not be strongly complete.

Let us now define some basic notions of proof theory.

Definition 7 (Proof, theorem)

Let $T\subseteq For_\mathrm {LPP_2^{conf}}$ be a set of formulas. We write $T\vdash _{Ax(\mathrm {LPP_2^{conf}})}\rho$, and we say that $\rho$ is deducible from T, if there is an at most countable sequence of formulas $\rho _0,\rho _1,...,\rho _n$, such that every $\rho _i$ is an axiom or a formula from T, or it is derived from the preceding formulas by an inference rule. The sequence $\rho _0,\rho _1,...,\rho$ is a proof of $\rho$ from T. We write $\vdash$ instead of $\vdash _{Ax_\mathrm {LPP_2^{conf}}}$ when it is clear from context.

We say that $\rho$ is a theorem of $Ax(\mathrm {LPP_2^{conf}})$, and write $\vdash \rho$, if $\emptyset \vdash \rho$.

Note that the length of a proof might be any countable successor ordinal.

Definition 8 (Consistency)

A set of formulas T is inconsistent if there a formula $\phi \in For_P$ such that $T\vdash \phi \wedge \lnot \phi$, otherwise it is consistent.

T is maximally consistent set (mcs) if it is consistent and every proper superset of T is inconsistent.

At the end of this section, we show that the axiom system $Ax(\mathrm {LPP_2^{conf}})$ is sound.

Theorem 1 (Soundness)

The axiomatization $Ax(\mathrm {LPP_2^{conf}})$ is sound with respect to the class of structures ${\mathcal M}(\mathrm {LPP_{2}^{conf}})$.

Proof

We need to show that every instance of an axiom scheme holds in every structure, and that the inference rules preserve the validity. Let us consider the axioms A7 and A9 and the rule R4. For A7, assume that $M\in {\mathcal M}(\mathrm {LPP_{2}^{conf}})$ is a structure such that $M\models c_{\ge r}(\alpha ,\beta )$, then $\mu ([\beta ])>0$, so $M\models P_{>0}\beta$. Now let us consider A9. Suppose that $M\models (P_{\ge t}\alpha \wedge P_{\ge s}\beta )\wedge c_{\ge r}(\alpha ,\beta )$. Then $\mu ([\alpha ])\ge t$, $\mu ([\beta ])\ge s$, $\mu ([\beta ])\ge 0$ and $\mu ([\alpha ]|[\beta ])-\mu ([\alpha ])\ge r$ i.e., $\mu ([\alpha \wedge \beta ])\ge \mu ([\beta ])(r+\mu ([\alpha ])$. This means that $\mu ([\alpha \wedge \beta ])\ge s(r+t)$. Therefore, $M\models P_{\ge s(r+t)}(\alpha \wedge \beta )$.

Now let us consider R4. In order to show that it preserves validity, assume that $M\models \{\phi \rightarrow P_{>0}\beta \}\cup \{\phi \rightarrow ((P_{\ge t}\alpha \wedge P_{\ge s}\beta )\rightarrow P_{\ge s(r+t)}(\alpha \wedge \beta ))\ | \ t,s\in [0,1]_Q\}$. If $M\not \models \phi$, we have $M\models \phi \rightarrow c_{\ge r}(\alpha ,\beta )$. Now suppose that $M\models \phi$. Then $M\models P_{>0}\beta$, i.e $\mu ([\beta ])>0$, and $M\models (P_{\ge t}\alpha \wedge P_{\ge s}\beta )\rightarrow P_{\ge s(r+t)}(\alpha \wedge \beta ))$ for all $t,s\in [0,1]_Q$. If the numbers $t,s\in [0,1]_Q$ are such that $t\le \mu ([\alpha ])$ and $s\le \mu ([\beta ])$, then $M\models P_{\ge t}\alpha \wedge P_{\ge s}\beta$, so $M\models P_{\ge s(r+t)}(\alpha \wedge \beta )$ , i.e., $\mu ([\alpha \wedge \beta ])\ge s(r+t)$. Using the fact that rationals numbers are dense in reals, we conclude $\mu ([\alpha \wedge \beta ])\ge \mu ([\beta ])(r+\mu ([\alpha ]))$ i.e., $\mu ([\alpha ]|[\beta ])-\mu ([\alpha ])\ge r$, so with $\mu ([\beta ])>0$, $M\models c_{\ge r}(\alpha ,\beta )$. Thus, $M\models \phi \rightarrow c_{\ge r}(\alpha ,\beta )$.    $\square$

5 Completeness of $Ax(\mathrm {LPP_2^{conf}})$

In this section we show that the axiomatization $Ax(\mathrm {LPP_2^{conf}})$ is strongly complete for the logic $\mathrm {LPP_2^{conf}}$, i.e., we prove that every consistent set of formulas has a model. Completeness is proved in several steps, along the lines of Henkin construction. First, we prove that the deduction theorem holds for $Ax(\mathrm {LPP_2^{conf}})$, using the implicative form of the infinitary rules. Then we use the deduction theorem to show that we can extend an arbitrary consistent set of formulas T to a maximal consistent set (Lindenbaum’s theorem). The standard technique needs to be adapted in presence of infinitary inference rules. Third, we use the maximal consistent set to construct a canonical model. Finally, we show that the canonical model is indeed a model of T.

5.1 Lindenbaum’s Theorem

We start by showing that the Deduction theorem holds.

Theorem 2 (Deduction theorem)

Let T be a set of formulas, and suppose that $\rho$ and $\sigma$ are two formulas such that either $\rho ,\sigma \in For_C$ or $\rho , \sigma \in For_P$. Then

$$\begin{aligned} T,\rho \vdash \sigma \ iff\ T\vdash \rho \rightarrow \sigma . \end{aligned}$$

Proof

The case when $\rho ,\sigma \in For_C$ is a consequence of the fact that $Ax(\mathrm {LPP_2^{conf}})$ extends classical propositional calculus. Let us consider the case when $\rho , \sigma \in For_P$. Here we will consider the nontrivial direction – from left to right, i.e., that $T,\phi \vdash \psi$ implies $T\vdash \phi \rightarrow \psi$. So, let us assume that $T,\phi \vdash \psi$. We proceed by the length of the inference. Here we only focus on the case when $\psi$ is obtained by the rule R4, while the cases of applications of other infinitary rules can be handled in a similar way. Suppose that $\psi$ is the formula $\phi _1\rightarrow c_{\ge r}(\alpha ,\beta )$, obtained from the set of premises $\{\phi _1\rightarrow P_{>0}\beta \}\cup \{\phi _1\rightarrow ((P_{\ge t}\alpha \wedge P_{\ge s}\beta )\rightarrow P_{\ge s(r+t)}(\alpha \wedge \beta ))\ | \ t,s\in [0,1]_Q\}.$ By induction hypothesis

• $T\vdash \phi \rightarrow (\phi _1\rightarrow P_{>0}\beta ),$ and

• $T\vdash \phi \rightarrow (\phi _1\rightarrow ((P_{\ge t}\alpha \wedge P_{\ge s}\beta )\rightarrow P_{\ge s(r+t)}(\alpha \wedge \beta )))$, for every $t,s\in [0,1]_Q.$

Then, by propositional reasoning we have

• $T\vdash (\phi \wedge \phi _1)\rightarrow P_{>0}\beta ,$ and

• $T\vdash (\phi \wedge \phi _1)\rightarrow ((P_{\ge t}\alpha \wedge P_{\ge s}\beta )\rightarrow P_{\ge s(r+t)}(\alpha \wedge \beta ))$ for every $t,s\in [0,1]_Q$.

Applying R4 we obtain

• $T\vdash (\phi \wedge \phi _1)\rightarrow c_{\ge r}(\alpha ,\beta ).$

Using A1 and R1 we obtain

• $T\vdash \phi \rightarrow (\phi _1\rightarrow c_{\ge r}(\alpha ,\beta ))$

• $T\vdash \phi \rightarrow \psi$.   $\square$

Now we can prove the key step toward completeness.

Theorem 3 (Lindenbaum’s Theorem)

Every consistent set of formulas can be extended to a maximal consistent set.

Proof

Let T be an arbitrary consistent set of formulas. Assume that $\{\rho _i\ | \ i=0,1,2,...\}$ is an enumeration of all formulas from $For_\mathrm {LPP_2^{conf}}$; it includes both non-probabilistic and probabilistic formulas. We construct $T^*$ recursively, in the following way:

• 1. $T_0=T$.

• 2. If the formula $\rho _i$ is consistent with $T_i$, then $T_{i+1}=T_i\cup \{\rho _i\}$.

• 3. If the formula $\rho _i$ is not consistent with $T_i$, then there are four cases:

  • (a) If $\rho =\phi \rightarrow P_{\ge r}\alpha$, then

    $$T_{i+1}=T_i\cup \{\phi \rightarrow P_{<r-\frac{1}{k}}\alpha \},$$

    where k is a positive integer such that $r-\frac{1}{k}\ge 0$ and $T_{i+1}$ is consistent.

  • (b) If $\rho _i=\phi \rightarrow c_{\ge r}(\alpha ,\beta )$, then $T_{i+1}=T_i\cup \{\psi _i\}$ where :

    $$\psi _i= \left\{ {\begin{array}{ll} {\phi \rightarrow P_{=0}\beta ,} &{} {T_i\cup \{\phi \rightarrow P_{=0}\beta \}\not \vdash \bot } \\ {\phi \rightarrow (P_{\ge t}\alpha \wedge P_{\ge s}\beta \wedge P_{<s(r+t)}(\alpha ,\beta )),} &{} {T_i\cup \{\phi \rightarrow P_{=0}\beta \}\vdash \bot } \\ \end{array} } \right. $$

    and t and s are two rational numbers from the unit interval such that $T_{i+1}$ is consistent.

  • (c) If $\rho _i=\phi \rightarrow c_{\le r}(\alpha ,\beta )$, then $T_{i+1}=T_i\cup \{\psi _i\}$ where:

    $$\psi _i= \left\{ {\begin{array}{ll} {\phi \rightarrow P_{=0}\beta ,} &{} {T_i\cup \{\phi \rightarrow P_{=0}\beta \}\not \vdash \bot } \\ {\phi \rightarrow (P_{\le t}\alpha \wedge P_{\le s}\beta \wedge P_{>s(r+t)}(\alpha ,\beta )),} &{} {T_i\cup \{\phi \rightarrow P_{=0}\beta \}\vdash \bot } \\ \end{array} } \right. $$

    and t and s are two rational numbers from the unit interval such that $T_{i+1}$ is consistent.

  • (d) Otherwise, $T_{i+1}=T_i.$

• 4. $T^*=\bigcup ^\infty _{n=0}T_n.$

First, using Theorem 2 one can prove that the set $T^*$ is correctly defined, i.e., there exist k, t and s from the steps 3(a)-3(b) of the construction. Here, we will consider the step 3(b), other two steps can be shown in a similar way.

Let us assume that $T\cup \{\phi \rightarrow c_{\ge r}(\alpha ,\beta )\}$ is inconsistent. Then the set $T\cup \{c_{\ge r}(\alpha ,\beta )\}$ is inconsistent as well. From Theorem 2 we obtain $T\vdash \lnot c_{\ge r}(\alpha ,\beta )$. Now suppose that the set $T\cup \{\phi \rightarrow P_{=0}\beta \}$ is inconsistent, and that the set $T\cup \{\phi \rightarrow (P_{\ge t}\alpha \wedge P_{\ge s}\beta \wedge P_{< s(r+t)}(\alpha ,\beta ))\}$ is inconsistent for every t and s. By Theorem 2, we obtain that $T\vdash P_{>0}\beta$ and $T\vdash \lnot (P_{\ge t}\alpha \wedge P_{\ge s}\beta \wedge P_{< s(r+t)}(\alpha ,\beta )),$ for every t and s. Consequently,

$$T\vdash \top \rightarrow P_{>0}\beta $$

and

$$T\vdash \top \rightarrow ((P_{\ge t}\alpha \wedge P_{\ge s}\beta )\rightarrow P_{\ge s(r+t)}(\alpha ,\beta )),$$

for all t and s, so from R4 we derive

$$T\vdash \top \rightarrow c_{\ge r}(\alpha ,\beta ).$$

Note that this contradicts with our assumption that $T\cup \{ c_{\ge r}(\alpha ,\beta )\}$ is an inconsistent set. Thus, there are rational numbers t and s such that the set

$$T\cup \{\phi \rightarrow (P_{\ge t}\alpha \wedge P_{\ge s}\beta \wedge P_{< s(r+t)}(\alpha ,\beta ))\}$$

is consistent.

Next we prove that $T^*$ is a maximally consistent set. Note that every $T_i$ is consistent by the construction. This still doesn’t imply consistency of $T^*=\bigcup ^\infty _{n=0}T_n,$ because of the presence of the infinitary rules. In order to prove the consistency of $T^*$, we first show that it is deductively closed. If the formula $\rho$ is an instance of some axiom, then $\rho \in T^*$ by construction of $T^*$. Next we prove that $T^*$ is closed under the inference rules. Here we show that $T^*$ is closed under the rule R4; the other cases are similar.

First we show that for every $\phi \in For_P$ either $\phi \in T^*$ or $\lnot \phi \in T^*$ holds. Let i and j be the nonnegative integers such that $\rho _i=\phi$ and $\rho _j=\lnot \phi$. From Theorem 2, it follows that either $\phi$ or $\lnot \phi$ is consistent with $T_{max\{i,j\}}$. Then either $\phi \in T_{i+1}$ or $\lnot \phi \in T_{j+1}$, so either $\phi \in T^*$ or $\lnot \phi \in T^*$.

Let us show that $T^*$ is closed under the inference rule R4. Assume that

$$\phi \rightarrow P_{>0}\beta ,\phi \rightarrow ((P_{\ge t}\alpha \wedge P_{\ge s}\beta )\rightarrow P_{\ge s(r+t)}(\alpha ,\beta ))\in T^*$$

for all $r,s\in [0,1]_Q$. We need to show that $\phi \rightarrow c_{\ge r}(\alpha ,\beta )\in T^*$. Assume that $\phi \rightarrow c_{\ge r}(\alpha ,\beta )\not \in T^*$. Then, by maximality of $T^*$, $\lnot (\phi \rightarrow c_{\ge r}(\alpha ,\beta ))\in T^*$. Thus, $\phi \in T^*$, so there is i such that $\phi \in T_i$. Let j be a nonnegative integer such that $\rho _j=\phi \rightarrow c_{\ge r}(\alpha ,\beta )$. By the step 3(b) of the construction ot $T^*$, $\phi \rightarrow P_{=0}\beta \in T_{j+1},$ or there are $t',s'\in [0,1]_Q$ such that $\phi \rightarrow (P_{\ge t'}\alpha \wedge P_{\ge s'}\beta \wedge P_{<s'(r+t')}(\alpha ,\beta ))\in T_{j+1}$. Suppose that $\phi \rightarrow P_{=0}\beta \in T_{j+1}$, and let k be the nonnegative integer such that $\rho _k=\phi \rightarrow P_{>0}\beta$. Then

$$T_{\max \{i,k+1\}}\vdash P_{>0}\beta .$$

Note that we also have $T_{\max \{i,j+1\}}\vdash P_{=0}\beta .$ Consequently, $T_{\max \{i,j+1,k+1\}}\vdash \bot$, a contradiction.

Now suppose that $\phi \rightarrow (P_{\ge t'}\alpha \wedge P_{\ge s'}\beta \wedge P_{<s'(r+t')}(\alpha ,\beta ))\in T_{j+1}$, where $t',s'\in [0,1]_Q$. Let $k'$ be the nonnegative integer such that $\rho _{k'}=\phi \rightarrow ((P_{\ge t'}\alpha \wedge P_{\ge s'}\beta )\rightarrow P_{\ge s'(r+t')}(\alpha ,\beta ))$. Then $T_{\max \{i,k'+1\}}\vdash (P_{\ge t'}\alpha \wedge P_{\ge s'}\beta )\rightarrow P_{\ge s'(r+t')}(\alpha ,\beta ).$ On the other hand,

$$T_{\max \{i,j+1\}}\vdash P_{\ge t'}\alpha \wedge P_{\ge s'}\beta \wedge P_{<s'(r+t')}(\alpha ,\beta ).$$

Thus, $T_{\max \{i,j+1,k'+1\}}\vdash \bot$, a contradiction. Consequently, the set $T^*$ is deductively closed.

From deductive closedness of $T^*$ we can prove that it is consistent. Indeed, if $T^*$ is inconsistent, there is a formula $\phi \in For_P$ such that $T^*\vdash \phi \wedge \lnot \phi$. But then there is a nonnegative integer i such that $\phi \wedge \lnot \phi \in T_i$, a contradiction.    $\square$

5.2 Canonical Model

Now we are ready to prove our main result: the axiomatization $Ax(\mathrm {LPP_2^{conf}})$ is strongly complete for the class of models ${\mathcal M}(\mathrm {LPP_{2}^{conf}})$. For a given consistent set T, we actually build a structure which is a model of its maximal consistent superset $T^*$. Recall that the existence of such superset is provided by Theorem 3.

Definition 9 (Canonical model)

Let $T^*$ be a mcs of formulas. The canonical model $M_{T^*}=(W,H,\mu ,v)$ is defined as follows:

• $W=\{ w \ |\ w$ is a classical propositional interpretation such that $w\models _{C}T^*\cap For_C\}$,

• $H=\{ [\alpha ] \ | \ \alpha \in For_C\}$, where $[\alpha ]=\{ w\in W \ | \ w\models _{C}\alpha \}$,

• $\mu : H\rightarrow [0,1]$ such that $\mu ([\alpha ])=\sup \{ r\in [0,1]_Q \ | \ T^*\vdash P_{\ge r} \alpha \}$,

• for every world w and every propositional letter $p\in \mathcal {P},v(w,p)= true$ iff $w\models _{C}p$.

It can be checked that this definition is correct, and that $M_{T^*} \in {\mathcal M}(\mathrm {LPP_{2}^{conf}})$ for every mcs $T^*$. The proof is pretty much the same as the proof of the corresponding result for the logic $\mathrm LPP_2$ [24], so we omit it here.

Now we formulate the completeness theorem for our logic.²

Theorem 4

(Strong completeness of $\mathrm {LPP_2^{conf}}$). A set of formulas T is consistent iff there is an $M\in {\mathcal M}(\mathrm {LPP_{2}^{conf}})$, such that $M\models T$.

Proof

Note that the direction form right to left follows from Theorem 1. For the other direction, suppose that T is a consistent set of formulas. By Theorem 3, there is a maximally consistent superset $T^*$ of T, which we can use to construct the canonical model $M_{T^*}$. We need to show that $M_{T^*}$ is a model of $T^*$. It is sufficient to show that $\rho \in T^*$ iff $M_{T^*}\models \rho$, for every formula $\rho \in For_\mathrm {LPP_2^{conf}}$. In the case when $\rho$ is a propositional formula, that follows from the construction of $M_{T^*}$ and the completeness theorem for propositional logic. In the case when $\rho$ is a probabilistic formula $\phi$, we use induction on the complexity of the formulas. The cases when $\phi$ is a conjunction or a negation are straightforward. The case when $\phi$ is $P_{\ge r}\alpha$ is essentially the same as in [24].

Let $\phi$ be of the form $c_{\ge r}(\alpha ,\beta )$.

$(\Rightarrow )$ Assume that $c_{\ge r}(\alpha ,\beta )\in T^*$. Let $\{ t_n\ | \ n\in \mathbf {N}\}$ and $\{ s_n\ | \ n\in \mathbf {N}\}$ be two strictly increasing sequences of numbers from $[0,1]_Q$, such that $lim_{n\rightarrow \infty }t_n=\mu ([\alpha ])$ and $lim_{n\rightarrow \infty }s_n=\mu ([\beta ])$. Let n be any number from $\mathbf {N}$. Then $T^*\vdash P_{\ge t_n}\alpha \wedge P_{\ge s_n}\beta$. Using the assumption $c_{\ge r}(\alpha ,\beta )\in T^*$, the axioms A7 and A9 and propositional reasoning, we obtain $T^*\vdash P_{>0}\beta$ and $T^*\vdash P_{\ge s_n(r+t_n)}(\alpha \wedge \beta )$. Finally, by Definition 9 we have $\mu ([\beta ])>0$ and $\mu ([\alpha \wedge \beta ])\ge lim_{n\rightarrow \infty }s_n(r+t_n)=\mu ([\beta ])(r+\mu ([\alpha ])),$ i.e.,

$$\mu ([\beta ])>0$$

and

$$\mu ([\alpha ]|[\beta ])-\mu ([\alpha ])\ge r.$$

$(\Leftarrow )$ Now assume that $\mu ([\beta ])>0$ and $\mu ([\alpha ]|[\beta ])-\mu ([\alpha ])\ge r$, i.e., $\mu ([\alpha \wedge \beta ])\ge \mu ([\beta ])(r+\mu ([\alpha ])).$ We will show that

$$T^*\vdash P_{>0}\beta $$

and

$$T^*\vdash (P_{\ge t}\alpha \wedge P_{\ge s}\beta )\rightarrow P_{\ge s(r+t)}(\alpha \wedge \beta )\text { for all } t,s\in [0,1]_Q.$$

Suppose that $T^*\not \vdash P_{>0}\beta$. By maximality $T^*\vdash P_{=0}\beta$, i.e., $\mu ([\beta ])=0$, a contradiction. So we have that $T^*\vdash P_{>0}\beta$.

If $t>\mu ([\alpha ])$ or $s>\mu ([\beta ])$, then $T^*\not \vdash P_{\ge t}\alpha \wedge P_{\ge s}\beta$. By maximality of $T^*$, $T^*\vdash \lnot (P_{\ge t}\alpha \wedge P_{\ge s}\beta )$, and consequently $T^*\vdash (P_{\ge t}\alpha \wedge P_{\ge s}\beta )\rightarrow P_{\ge s(r+t)}(\alpha \wedge \beta )$. If $t\le \mu ([\alpha ])$ and $s\le \mu ([\beta ])$, then $s(r+t)\le \mu ([\alpha \wedge \beta ])$ by assumption, so $T^*\vdash P_{\ge s(r+t)}(\alpha \wedge \beta )$ by Definition 9. Now the result follows from the fact that $T^*$ is deductively close.

The case when $\phi$ us $c_{\le r}(\alpha ,\beta )$ can be proved in a similar way.    $\square$

6 Decidability

In this section, we discuss decidability of $\mathrm {LPP_2^{conf}}$. We distinguish two cases, since we have two types of formulas. We start with propositional formulas.

Theorem 5

The problem of deciding whether a formula from $For_C$ is satisfiable in an $\mathrm {LPP_2^{conf}}$ structure is NP-complete.

Proof

This result follows straightforwardly from the same complexity result for propositional formulas under the classical semantics. Indeed, if $\alpha$ is propositionally unsatisfiable, then, according to our definition of satisfiability, $\alpha$ also does not hold in any model from ${\mathcal M}(\mathrm {LPP_{2}^{conf}})$, since $v(w,\alpha )=false$ for every world w. For the other direction, note that if $\alpha$ is propositionally satisfiable, then it is satisfied in the model $(W,H,\mu ,v)$, where $W=\{ w \}$ (which uniquely determines $H=\{\emptyset , W \}$ and $\mu (\emptyset )=0$, $\mu (W)=1$), with $v(w,\cdot )$ being an evaluation function such that $v(w,\alpha )=true$.    $\square$

Let us now turn to the probabilistic formulas.

Theorem 6

There is a PSPACE procedure deciding whether a formula from $For_P$ is satisfiable in an $\mathrm {LPP_2^{conf}}$ structure.

Proof

Here we use the complexity result of Fagin, Halpern and Megiddo about polynomial weight formulas [13]. Those formulas are Boolean combinations of polynomial equations and inequalities, with integer coefficients and with variables of the form $w(\alpha )$, where $\alpha \in For_C$ and w stands for “weight” (probability). For example $(3 w(p)w(p\vee q)+w(q\rightarrow p)\ge 2) \wedge 5w(q)\ge 1$ is a polynomial weight formula. Those formulas are evaluated in a Kripke structure with a probability measure over possible worlds, just like in our logic. A PSPACE decision procedure for satisfiability of polynomial weight formulas is proposed in [13]. In short, the authors reduce the problem to a problem in the quantifier-free theory of real closed fields and then apply Canny’s decision procedure from [1]. Instead of repeating the same strategy for our logic, we rather translate the formulas of our language to polynomial weight formulas, and then apply the procedure from [13]. Our simple translation has two steps. First, we use the mapping f, defined recursively as follows

• $f(P_{\ge r} \alpha ) = w(\alpha )\ge r$,

• $f(c_{\ge r} (\alpha ,\beta )) = w(\beta )\ge 0 \wedge w(\alpha \wedge \beta )-w(\alpha )w(\beta )\ge r w(\beta )$,

• $f(c_{\le r} (\alpha ,\beta )) = w(\beta )\ge 0 \wedge w(\alpha \wedge \beta )-w(\alpha )w(\beta )\le r w(\beta )$,

• $f(\varphi \wedge \psi )=f(\varphi ) \wedge f(\psi ),$

• $f(\lnot \varphi )=\lnot f(\varphi ).$

Note that we need to further transform the obtained formulas, since polynomial weight formulas allow only integer coefficients. For that reason, we apply the function g, whose role is to clear the denominators. Instead of giving a formal definition, we illustrate how g works in practice. (We assume that the rational constants are given in form of fractions using coprime integers.) For example, if $\theta$ is the formula

$$ w(p)w(p\rightarrow q)\ge \frac{2}{3} \vee w(q)\le \frac{4}{5}, $$

then $g(\theta )$ is

$$ 3w(p)w(p\rightarrow q)\ge 2 \vee 5w(q)\le 4. $$

Obviously, a formula $\varphi \in For_P$ is satisfiable iff $g(f(\varphi ))$ is a satisfiable polynomial weight formula. Thus, our result follows.    $\square$

7 Conclusion

In this paper we presented the probabilistic logic $\mathrm {LPP_2^{conf}}$ which allows reasoning about degrees of confirmation. The language contains both classical propositional formulas and probabilistic formulas, and it extends the language of $\mathrm LPP_2$ [24] with the binary operators that model measure of confirmation. We proposed an axiomatization for the logic and prove strong completeness. Since the logic is not compact, the axiomatization contains infinitary rules of inference. We also proved that the problem of deciding whether a probabilistic formula of our logic is satisfiable is in PSPACE.

There are two avenues for further research. First, it would be interesting to see if a more expressive language could be built on top of this logic. For example, nesting of probability operators would allow expressions of the form $c_{\ge r} (\alpha ,P_{\ge s}\beta )$, which model the situation in which probabilistic boundaries of one formula confirms (to some degree) another formula. Another interesting direction would be a first order extension, in which we could express the statements like $(\forall x)c_{\ge r} (\alpha (x),\beta (x))$.

Second, in this paper we modeled the difference measure. We chose this measure simply because it is most standard measure of confirmation. However, we can easily adapt the technique developed here to capture the other popular measures from the literature (see, for example, [28]). For example, Carnap’s relevance measure

$$\mu (A\wedge B)-P(A)P(B)$$

can be axiomatized by replacing A7-A10 and R4 and R5 with the following axiom schemes and inference rules:

• (A7’) $(P_{\ge t}\alpha \wedge P_{\ge s}\beta \wedge c_{\ge r}(\alpha ,\beta ))\rightarrow P_{\ge r+st}(\alpha \wedge \beta )$

• (A8’) $(P_{\le t}\alpha \wedge P_{\le s}\beta \wedge c_{\le r}(\alpha ,\beta ))\rightarrow P_{\le r+st}(\alpha \wedge \beta )$

• (R4’) From the set of premises

  $$\{\phi \rightarrow ((P_{\ge t}\alpha \wedge P_{\ge s}\beta )\rightarrow P_{\ge r+st}(\alpha \wedge \beta )) \ | \ t,s\in [0,1]_Q\}$$

  infer $\phi \rightarrow c_{\ge r}(\alpha ,\beta )$.

• (R5’) From the set of premises

  $$\{\phi \rightarrow ((P_{\le t}\alpha \wedge P_{\le s}\beta )\rightarrow P_{\le r+st}(\alpha \wedge \beta ))\ | \ t,s\in [0,1]_Q\}$$

  infer $\phi \rightarrow c_{\le r}(\alpha ,\beta )$.

For axiomatizing Carnap’s relevance measure we need only eight axiom schemes. Note that we can also apply the similar technique for axiomatizing log-ratio measure

$$c(\alpha ,\beta )=\log \big [ \frac{P(\alpha |\beta )}{P(\alpha )}\big ],$$

but the decidability results are not clear. In that case, we cannot translate a formula to an existential sentence in the first-order language of fields, as we have done in Sect. 6, so we cannot apply the procedure from [13].