Logical formalization of Bayesian concepts of confirmation

Abstract

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 concepts 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., μ(A|B) > μ(A)), which correspond to the classificatory concept (“A is confirmed by B”) [10]. Up to now, only the classificatory concept of confirmation is logically formalized, in our previous work [4]. In this paper, we formalize the quantitative concept of confirmation, first within a propositional logical framework LPPconf 1, and then using its first-order extension LFOPconf 1. We focus on the most standard (according to Eells and Fitelson [8]) measure of degree of confirmation, called difference measure: c(A, B) = μ(A|B) − μ(A). Our formal languages extend classical (propositional/first order) logic with the unary probabilistic operators of the form P≥r (P≥rα reads “the probability of α is at least r”), where r ranges over the set of rational numbers from the unit interval [15], and the binary operators c≥r and c≤r, which we semantically interpret using the difference measure. The corresponding semantics consists of a special type of Kripke models, with probability measures defined over the worlds. Our main results are sound and strongly complete (every consistent set of formulas is satisfiable) axiomatizations for the logics. We prove completeness using a modification of Henkin’s construction. Since the logics are not compact, in order to obtain the strong variant of completeness, we use infinitary inference rules. An obvious alternative to an infinitary axiomatization is to develop a finitary system which would be weakly complete (”a formula is a theorem iff it is valid”). However, already for the logics which need to express conditional probabilities, that task turned out to be very hard to accomplish. Fagin, Halpern and Meggido [9] faced problems when they tried to represent conditional probabilities via a logical language with polynomial weight formulas that allow products of terms (e.g., w(p1 ∧ p2) · (w(p1) + w(p2)) ≥ w(p1) · w(p2) represents the sentence “the conditional probability of p2 given p1 plus the conditional probability of p1 given p2 is at least 1”). They observed that even for obtaining the weak completeness additional expressiveness is needed, and they introduced a first-order language such that variables can appear in formulas. As an alternative, the researchers from the field of probability logic use the infinitary approaches [3] and fuzzy approaches [13]. In the case of first-order probability logics the situation is even worse, since the set of valid formulas of the considered logics is not recursively enumerable [1, 11]. As a consequence, no finitary axiomatization, which would be even weakly complete, is possible. From the technical point of view, we modify some of our earlier methods presented in [5, 6, 7, 14, 16, 17]. We point out that our formal languages are countable and all formulas are finite, while only proofs are allowed to be infinite. However, for some restrictions of the logics we provide finitary axiomatic systems. We also prove that our propositional logic LPPconf 1 is decidable.