Frédéric Dambreville

Deterministic modal Bayesian Logic: derive the Bayesian inference within the modal logic T

Keywords: Probability, Bayesian inference, Conditional Logic, Modal Logic, Probabilistic Logic

In this paper a conditional logic is defined and studied. This conditional logic, DmBL, is constructed as a deterministic counterpart to the Bayesian conditional. The logic is unrestricted, so that any logical operations are allowed. A notion of logical independence is also defined within the logic itself. This logic is shown to be nontrivial and is not reduced to classical propositions. A model is constructed for the logic. Completeness results are proved. It is shown that any unconditioned probability can be extended to the whole logic DmBL. The Bayesian conditional is then recovered from the probabilistic DmBL. At last, it is shown why DmBL is compliant with Lewis' triviality.

Introduction

Bayesian inference is a powerful principle for modeling and manipulating probabilistic information. In many cases, Bayesian inference is considered as an optimal and legitimate rule for inferring such information.

• Bayesian filters for example, and their approximations by means of sequential Monte-Carlo, are typically regarded as optimal filters [START_REF] Arulampalam | A Tutorial on Particle Filters for On-line Non-linear/Non-Gaussian Bayesian Tracking[END_REF][START_REF] Oudjane | Improving regularised particle filters[END_REF][START_REF] Th | Hierarchical particle filter for bearings only tracking[END_REF],

• Bayesian networks are particularly powerful tools for modeling uncertain information, since they merge logical and independence priors, for reducing the complexity of the laws, with the possibility of learning [START_REF] Pearl | Bayesian Networks[END_REF][START_REF] Murphy | Dynamic Bayesian Networks: Representation, Inference and Learning[END_REF][START_REF] Dambreville | Cross-entropic learning of a machine for the decision in a partially observable universe[END_REF].

Although Bayesian inference is an established principle, it is recalled [START_REF] Jaynes | Probability Theory: The Logic of Science[END_REF] that it has been disputed until the middle of the XXth century, in particular by the frequencist community. What made the Bayesian inference established is chiefly a logical justification of the rule [START_REF] Cox | The Algebra of Probable Inference[END_REF][START_REF] Jaynes | Probability Theory: The Logic of Science[END_REF]. Some convergence with the frequencist interpretation achieved this acceptation. Cox derived the characteristics of Probability and of Bayesian conditional from hypothesized axioms about the probabilistic system, which themselves were reduced in terms of functional equations. Typical axioms are:

• The operation which maps the probability of a proposition to the probability of its negation is idempotent,

• The probability of A ∧ B depends only of the probability of A and of the probability of B given that A is true,

• The probability of a proposition is independent of the way it is deduced (consistency).

It is noticed that Cox interpretation has been criticized recently for some imprecision and reconsidered [START_REF] Brucq | Identical Foundation of Probability Theory and Fuzzy Set Theory[END_REF][START_REF] Brucq | Chapter 11 in Advances and Applications of DSmT for Information Fusion, Dezert & Smarandache editors[END_REF][START_REF] Halpern | A counterexample to theorems of Cox and Fine[END_REF].

In some sense, Cox justification of the Bayesian conditional is not entirely satisfactory, since it is implicit: it justifies the Bayesian conditional as the operator fulfilling some natural properties, but does not construct a full underlying logic priorly to the probability. The purpose of this paper is to construct an explicit logic for the Bayesian conditional as a conditional logic:

1. Build a (deterministic) conditional logic, priorly to any notion of probability. This logic will extend the classical propositional logic. It will contain a conditional operator (•|•), so that the conditional proposition (ψ|φ) could be built for any propositions φ and ψ, 2. Being given a probability p over the unconditioned propositions, derive the probabilistic Bayesian conditional from an extension p of the probability p over this conditional logic. More precisely, the Bayesian conditional will be derived by p(ψ|φ) = p (ψ|φ) .

The construction of an explicit underlying logic provides a better understanding of the Bayesian conditional, but will also make possible the comparison with other rules for manipulating probabilistic information, based on other logics [START_REF] Dambreville | Conflict Free Rule for Combining Evidences[END_REF].

It is known that the construction of such underlying logic is heavily constrained by Lewis' triviality [START_REF] Lewis | Probability of Conditionals and Conditional Probabilities[END_REF], which has shown some critical issues related to the notion of conditional probability; refer also to [START_REF] Hájek | Desire Beyond Belief[END_REF][START_REF] Hájek | What Conditional Probability Could Not Be[END_REF][START_REF] Van Fraassen | Probabilities of Conditionals[END_REF]. In particular, Lewis' result implies strong hypotheses about the nature of the conditionals. In most cases, the conditionals have to be constructed outside the space of unconditioned propositions. This result implied the way the logic of Bayesian conditional has been investigated. Many approaches do not distinguish the Bayesian conditional from probabilistic notions. This is particularly the case of the theory called Bayesian Logic [START_REF] Andersen | Bayesian Logic, Decision Support Systems[END_REF], which is an extension of probabilistic logic programming by the way of Bayesian conditioning. Other approaches like conditional logic or algebra result in the construction of conditional operators, which finally arise as abstraction independent of any probability. These logical constructions are approximating the Bayesian conditional or are constrained in use. The Bayesian inference is a rich notion. It is also evocated subsequently, how the Bayesian inference has been applied to the definition of default reasoning systems [START_REF] Bourne | Default reasoning using maximum entropy and variable strength defaults[END_REF].

Since Lewis' triviality is a fundamental reference in this work, it is introduced now. By the way, different logical approaches of the Bayesian conditional are evocated, and it is shown how these approaches avoid the triviality.

Lewis' triviality. Let Ω be the set of all events, and M be the set of measurable subsets of Ω. Let Pr (M) be the set of all probability measures defined on M. Lewis' triviality [START_REF] Lewis | Probability of Conditionals and Conditional Probabilities[END_REF] may be expressed as follows:

Let A, B ∈ M with ∅ B A Ω . Then, it is impossible to build a proposition (B|A) ∈ M such that π (B|A) = π(B|A)

∆ = π(A∩B) π(A)
for any π ∈ Pr (M) with 0 < π(B) < π(A) < 1 .

Lewis' triviality thus makes impossible the construction of a (Bayesian) conditional operator within the same Boolean space.

Proof. For any propositions C, D , define π C (D) = π(D|C) = π(C∩D) π(C) , when π(C) > 0. The proof of Lewis' result relies of the following calculus:

π((B|A)|C) = π C ((B|A)) = π C (B|A) = π C (A ∩ B) π C (A) = π(C∩A∩B) π(C) π(A∩C) π(C) = π(C ∩ A ∩ B) π(A ∩ C) = π(B|C ∩ A) . (1)
Denoting ∼ B = Ω \ B, it is inferred then:

π(B) π(A) = π(A ∩ B) π(A) = π(B|A) = π((B|A)) = π((B|A)|B)π(B) + π((B|A)| ∼ B)π(∼ B) = π(B|B ∩ A)π(B) + π(B| ∼ B ∩ A)π(∼ B) = 1 × π(B) + 0 × π(∼ B) = π(B) ,
which contradicts the hypotheses π(B) = 0 and π(A) = 1 .

222

In fact, the derivation (1) relies on the hypothesis that (B|A) ∈ M, which implies by definition of (B|A) the relation π

C (B|A) π C (A) = π C (B ∩ A) .
If the proposition (B|A) is outside M, it becomes necessary to build for any probability π its extension π over the outside propositions; in particular, it will be defined π (B|A) = π(B ∩A)/π(A), for any A, B ∈ M . In practice, there is no reason to have π C (D) = π (D|C) for D ∈ M ; then, the above triviality does not work anymore.

The property π C = π (•|C) is somewhat counter-intuitive. In particular, it means that conditionals are not conserved by conditional probabilities. However, it allows the construction of a conditional logic for the Bayesian conditional; our work provides an example of such construction.

Probabilistic logic and Bayesian logic. Probabilistic logic, as defined by Nilsson [START_REF] Nilsson | Probabilistic logic[END_REF][START_REF] Paass | Chapter 8 in Non-Standard Logics for Automated Reasoning[END_REF][START_REF] Pearl | Probabilistic Reasoning in Intelligent Systems[END_REF], has been widely studied in order to model and manipulate the uncertain information. It tracks back from the seminal work of Boole [START_REF] Boole | An Investigation of the Laws of Thought, on which are Founded the Mathematical Theories of Logic and Probabilities, Walton and Maberley[END_REF]. In probabilistic logic, the knowledge, while logically encoded by classical propositions, is expressed by means of constraints on the probability over these propositions. For example, the knowledge over the propositions A, B may be described by:

v 1 ≤ p(A) ≤ v 2 and v 3 ≤ p(A → B) ≤ v 4 , (2)
where A → B ≡ ¬A ∨ B and v i |1 ≤ i ≤ 4 are known bound over the probabilities. Equations like (2) turn out to be a linear set of constraints over p. In other words, it is then possible to characterize all the possible values for p by means of a linear system. For example, if our purpose is to know the possible values for p(B), we just have to solve:

   v 1 ≤ p(A ∧ B) + p(A ∧ ¬B) ≤ v 2 , v 3 ≤ p(A ∧ B) + p(¬A ∧ B) + p(¬A ∧ ¬B) ≤ v 4 , p(A ∧ B) + p(¬A ∧ B) = p(B) .
Notice that probabilistic logic by itself does not manipulate conditional probabilities or any notion of independence. Proposals for extending the probabilistic logic to conditionals has appeared rather early [START_REF] Adams | The Logic of Conditionals[END_REF], but Andersen and Hooker [START_REF] Andersen | Probabilistic Logic for Belief Nets[END_REF][START_REF] Andersen | Bayesian Logic, Decision Support Systems[END_REF] introduced an efficient modeling and solve of such problems. This new paradigm for manipulating Bayesian probabilistic constraints has been called Bayesian Logic.

For example, let us introduce a new proposition C to problem [START_REF] Andersen | Probabilistic Logic for Belief Nets[END_REF]. Assume now that the new system is characterized by a bound over the conditional probability p(C|A ∧ B) and by an independence hypothesis between A and B. The set of constraints could be rewritten as:

v 1 ≤ p(A) ≤ v 2 and v 3 ≤ p(A → B) ≤ v 4 , v 5 ≤ p(C|A ∧ B) ≤ v 6 and p(A ∧ B) = p(A)p(B) .
The constraint on p(C|A ∧ B) turns out to be linear, since it could be rewritten:

v 5 p(A ∧ B) ≤ p(C ∧ A ∧ B) ≤ v 6 p(A ∧ B) , but constraint p(A ∧ B) = p(A)p(B)
remains essentially a non-linear constraint. Constraints involving both conditional and non-conditional probabilities also generate non-linearity. In [START_REF] Andersen | Probabilistic Logic for Belief Nets[END_REF] and more thoroughly in [START_REF] Andersen | Bayesian Logic, Decision Support Systems[END_REF], Andersen and Hooker expose a methodology for solving these non-linear programs. In particular, the structure of the Bayesian Network is being used in order to reduce the number of non-linear constraints.

Bayesian Logic is a paradigm for solving probabilistic constraint programs, which involve Bayesian constraints. Since it does not construct the Bayesian conditional as a strict logical operator, this theory is not concerned by Lewis' triviality. Bayesian Logic departs fundamentally from our approach, since Deterministic modal Bayesian Logic intends to build the logic underlying the Bayesian conditional priorly to the notion of probability.

Conditional Event algebra. In Conditional Event Algebra [START_REF] Goodman | Mathematics of Data Fusion[END_REF][START_REF] Goodman | What is conditional algebra and why should you care?[END_REF][START_REF] Dubois | Special Issue on Conditional Event Algebra[END_REF][START_REF] Calabrese | An algebraic synthesis of the foundations of logic and probability[END_REF], the conditional could be seen as an external operator ( | ) , which maps pairs of unconditioned propositions toward an external Boolean space, while satisfying the properties related to the Bayesian conditional. There are numerous possible constructions of a CEA. In fact, most CEAs provide conditional rules which are richer than the strict Bayesian conditional. For example, the CEA, denoted DGNW [START_REF] Goodman | Mathematics of Data Fusion[END_REF], is characterized by the following properties:

(a|b) ∧ (c|d) = a ∧ b ∧ c ∧ d (¬a ∧ b) ∨ (¬c ∧ d) ∨ (b ∧ d) , (a|b) ∨ (c|d) = (a ∧ b) ∨ (c ∧ d) (a ∧ b) ∨ (c ∧ d) ∨ (b ∧ d) . (3)
Property (3) infers the general Bayesian rule:

(a|b ∧ c) ∧ (b|c) = (a ∧ b|c) ,
but also a Boolean morphism:

(a ∧ b|c) = (a|c) ∧ (b|c) and (a ∨ b|c) = (a|c) ∨ (b|c) .

Notice that the external space hypothesis is fundamental here, and it is not possible to write (a|Ω) = a where Ω is the set of all events. In particular, DGNW allows (a|b)∧(b|Ω) = (a∧b|Ω), but not (a|b) ∧ b = a ∧ b . Now, property (3) defines much more combinations than the strict Bayesian conditional. Indeed, the combination (a|b) ∧ (c|d) is reduced for any choice of a, b, c, d, which is not possible with a classical Bayesian combination.

The counterpart of such nice properties is the necessity to restrict the conditional to unconditioned propositions. It is yet proposed in [START_REF] Goodman | Mathematics of Data Fusion[END_REF] a closure of DGNW:

(a|b) (c|d) = a (b ∧ ¬a ∧ ¬d) ∨ (b ∧ c ∧ d) , (5)
but this closure is not compatible with a probabilistic interpretation and fails to satisfy the intuitive relation P (a|b) (c|d) = P (a|b) ∧ (c|d) /P (c|d) . More generally, CEAs are practically restricted to only one level of conditioning, and usually avoid any interferences between unconditioned and conditioned propositions. These restrictions are also the way, by which CEAs avoid Lewis' triviality.

Conditional logics. Conditional is an ambiguous word, since there may be different meaning owing to the community. Even the classical inference, φ → ψ ≡ ¬φ ∨ ψ , is called material conditional. Despite classical inference is systematically used by mathematicians, its disjunctive definition makes it improper for some conditions of use. For example, it is known that it is by essence non-constructive, an issue which tracks back to the foundation of modern mathematic [START_REF] Van Heijenoort | From Frege to Gödel: A Source Book In Mathematical Logic 1879-1931[END_REF]. Somehow, the possibility to infer from the contradiction is also counter-intuitive; by the way, the Bayesian inference makes no sense, while inferring from the contradiction.

In the framework of Bayesian inference, we are interested in defining the law of a conditional independently of the factual state of the hypothesis. Thus, the Bayesian conditional could be related to the notion of Counterfactual conditional. The classical inference is actually not counterfactual, since it is by definition dependent of the hypothesis. From now on, the notion of conditional will refer to counterfactual conditionals, and related extensions.

A non-classical inference is often related to a modal paradigm. While first defining counterfactual conditionals (an example of such conditional, VCU, is detailed in section 3.2), the philosophers David Lewis and Robert Stalnaker [START_REF] Lewis | Counterfactuals[END_REF][START_REF] Stalnaker | Probability and conditionals[END_REF] based their model constructions on the possible world semantics of modal logic (other authors also consider Kripke model extensions [START_REF] Giordano | A Conditional Logic for Iterated Belief Revision[END_REF]). Stalnaker claimed that it was possible to construct such conditional, denoted >, within the universe of events, so as to match the probabilistic Bayesian conditional, i.e. p(A > B) = p(B|A) = p(A ∧ B)/p(A). Lewis answered negatively [START_REF] Lewis | Probability of Conditionals and Conditional Probabilities[END_REF] to this conjecture. However, this was not the end of the interaction between conditional logics and probabilities.

On the basis of the semantic, Lewis proposed an alternative interpretation of the probability p(A > B), called Imaging [START_REF] Lepage | A Many-valued Probabilistic Conditional Logic[END_REF].

It is not our purpose to detail these notions here, but we point out the following:

• The probabilistic interpretation of the conditional by imaging does not provide an interpretation of the probabilistic Bayesian conditional. Nevertheless, Stalnaker's conjecture could be weakened so as to overcome the triviality: as already explained in our previous discussion, the triviality could be avoided by constructing the conditionals outside the classical propositions space and extending the probability accordingly,

• The existing conditional logics are still rough approximations of the Bayesian conditional. This point will be discussed in details later. But for example, it seems that the negation operators of the existing conditional logics are usually relaxed, when compared to the Bayesian conditioning (refer to the logic VCU defined in section 3.2). Typically, a relation like ¬(φ > ψ) ≡ φ > ¬ψ , i.e. a logical counterpart of p(¬ψ|φ) = 1p(ψ|φ) , is not retrieved. It is noticed that the Bayesian inference is able of some kind of default reasoning, by adapting the belief of a proposition according to an hypothesis. In fact, the system P for default reasoning could be derived from a Bayesian interpretation [START_REF] Adams | The Logic of Conditionals[END_REF][START_REF] Finetti | Theory of probability : a critical introductory treatment[END_REF][START_REF] Bourne | Default reasoning using maximum entropy and variable strength defaults[END_REF]. The ε-semantic is particularly enlightening. Let us denote φ ⇒ ψ the default, which means "ψ is normally true, when φ holds true". Then let us interpret φ ⇒ ψ by the constraint p(ψ|φ) ≥ 1ε, where ε is an infinitesimal. 2 Now, it is deduced from the Bayesian inference:

p(η|φ ∧ ψ) = p(η|φ)-1 -p(ψ|φ) p(η|φ ∧ ¬ψ) p(ψ|φ) . (6)
From hypotheses φ ⇒ ψ and φ ⇒ η, it would come p(ψ|φ) ≥ 1ε 1 and p(η|φ) ≥ 1ε 2 , where ε 1 and ε 2 are infinitesimals, and then by [START_REF] Blackburn | Modal Logic (Cambridge Tracts in Theoretical Computer Science)[END_REF]:

p(η|φ ∧ ψ) ≥ 1 -ǫ 1 -ǫ 2 and φ ∧ ψ ⇒ η .
This deduction conduces to the well known Cautious Monotonicity rule:

CM : φ ⇒ ψ, φ ⇒ η φ ∧ ψ ⇒ η .
The rule CM already infers some default reasoning:

Assume b ⇒ f (birds normally fly), p ⇒ b (penguins normally are birds) and p ⇒ ¬f (penguins normally do not fly). Then by applying CM on p ⇒ b and p ⇒ ¬f , it comes p ∧ b ⇒ ¬f . The non-monotonic inference ⇒ is thus able to handle sub-cases.

From the infinitesimal probabilistic interpretation, the following rules of P are also deduced: Also related to the infinitesimal interpretation is the ranking of the models (typically, a rank is interpreted as an infinitesimal order). The ranking conditions the way the defaults are prioritized. There has been various extension of system P (alternative inferences, ranking methods). In some recent works, Lukasiewicz et al. [START_REF] Biazzo | Probabilistic Logic under Coherence, Model-Theoretic Probabilistic Logic, and Default Reasoning[END_REF] proposed a probabilistic extension of default reasonings (including system P ), which is not restricted to an infinitesimal probabilistic interpretation. Each default is then associated to an interval of constraint for its probability.

Id
Why a new conditional logic? The previous approaches and uses of the Bayesian logic imply restrictions or approximations to the logical interpretation of the Bayesian conditional. Bayesian logic does not provide a logical interpretation of the Bayesian conditional, but rather a methodology for solving the program related to a probabilistic Bayesian modeling. Conditional event algebras provide an interesting logical interpretation of the Bayesian conditional, but are highly constrained in their definition; from a logical viewpoint, the impossibility to handle or to combine multiple-levels conditionals constitutes a limitation in terms of the coherence of the models. Existing conditional logics are insufficient for characterizing the Bayesian conditional properly. The default reasoning systems and their interpretation by means of the probabilistic Bayesian inference are quite interesting and a source of inspiration, but they are mainly a consequence of the probabilistic Bayesian inference and account for the Bayesian conditional only partially. Our work intends to overcome these limitations, by constructing a new conditional logic which is in accordance with the Bayesian conditional. It is not our purpose, however, to enrich the Bayesian rule, as it is proposed in most CEA.

Our logic, denoted Deterministic modal Bayesian Logic (DmBL), is constructed according to a modal background (system T). The conditional operator is defined in parallel to a relation of logical independence. This relation is defined within the logic, and not at a meta-level. The probabilistic Bayesian inference is recovered from the derived logical theorems and the logical independence. This process implies an extension of probability from the unconditioned logic toward DmBL. As a final result, a theorem is proved that guarantees the existence of such extension (Lewis' result is thus avoided).

Section 2 is dedicated to the definition of the Deterministic modal Bayesian Logic. The languages, axioms and rules are introduced. In section 3, several theorems of the logic are derived. A purely logical interpretation of Lewis' triviality is made, and DmBL is compared with other systems. A model for DmBL is constructed in section 4. A partial completeness theorem is derived. The extension of probabilities over DmBL is investigated in section 5.

The probabilistic Bayesian inference is recovered from this extension. The paper is then concluded.

Definition of the logics

Deterministic modal Bayesian Logic was first defined without modality as Deterministic Bayesian Logic in a previous version of this document [START_REF] Dambreville | Definition of a Deterministic Bayesian Logic[END_REF]. The non-modal definition is uneasy to handle. For this new modal definition, we have been inspired by the seminal work of Lewis [START_REF] Lewis | Counterfactuals[END_REF], and also by more recent works of Laura Giordano et al., which use the modality for specifying the conditional behavior [START_REF] Giordano | A Conditional Logic for Iterated Belief Revision[END_REF][START_REF] Giordano | Conditional Logic of Actions and Causation[END_REF]. The use of the modality is instrumental here; for this reason, modal appears in lower case in our terminology.

Modal logic is a powerful tool, but not intuitive at first sight. We thus decided to introduce the modality softly, by interpreting it (in part) from probabilistic considerations: modalities will be used in order to characterize properties generally true for any possible probability. Nevertheless, this instrumental use of modalities allows an abstraction which makes our construction independent to any notion of probability.

Introducing the modal notation. This paragraph intends to explain the intuition behind the subsequent modal definition of DmBL. Some generalizations are not justified here, but the axioms are extrapolated from results, which are easily proved.

The logic of a system is the collection of behaviors which are common to any instance of this system. Let us consider the example of probability on a finite (unconditioned) propositional space. For convenience, define P the set of strictly positive probabilities over this space, that is p ∈ P is such that p(φ) > 0 for any non-empty proposition φ : P = p p is a probability and ∀φ ≡ ⊥, p(φ) > 0 .

When the proposition φ is always true (i.e. φ is the set of all events), it is known that p(φ) = 1 for any possible probability p. This could be interpreted logically as follows:

⊢ φ implies ⊢ ∀p ∈ P, p(φ) = 1 . (7)
This is a typical logical relation related to the probabilities. Notice however that:

φ → ∀p ∈ P, p(φ) = 1 is false in general ,
because unless φ is always true, the property ∀p ∈ P, p(φ) = 1 is necessary false. 3It is also obvious that ∀p ∈ P, p(φ) = 1 infers φ (consider the cases ⊢ φ and φ) :

⊢ (∀p ∈ P, p(φ) = 1) → φ . ( 8
)
Another proposition is easily derived:

⊢ (∀p ∈ P, p(¬φ ∨ ψ) = 1) → (∀p ∈ P, p(φ) = 1) → (∀p ∈ P, p(ψ) = 1) . (9)
This last proposition could be considered as a modus ponens encoded by means of the probabilities (it is recalled that φ → ψ ≡ ¬φ ∨ ψ). Now, by using the abbreviation 2φ = ∀p ∈ P, p(φ) = 1 , the propositions ( 7), ( 8) and ( 9) are turned into:

⊢ φ implies ⊢ 2φ , ⊢ 2φ → φ , ⊢ 2(φ → ψ) → (2φ → 2ψ) .
These are exactly the modal axioms and rule of the system T of modal logic. System T is the backbone of our conditional logic, DmBL. Additional axioms are also introduced for characterizing the conditional (•|•). These axioms are extrapolated from unconditioned probabilistic characterizations. For example, it is proved for unconditioned propositions:

∀p ∈ P, p(φ) + p(ψ) = 1 implies φ ≡ ¬ψ . ( 10
)
Since it is also known that p(ψ|φ) + p(¬ψ|φ) = 1 for any p ∈ P, it will be assumed the axiom:

(ψ|φ) ≡ ¬(¬ψ|φ) . (11)
Of course, property [START_REF] Calabrese | An algebraic synthesis of the foundations of logic and probability[END_REF] normally holds for unconditioned propositions only, so that axiom [START_REF] Cox | The Algebra of Probable Inference[END_REF] comes in fact from an extrapolation of [START_REF] Calabrese | An algebraic synthesis of the foundations of logic and probability[END_REF].

Similarly, it is noticed that:

∀p ∈ P, p(φ) + p(ψ) ≤ p(η) + p(ζ) implies ⊢ (φ ∨ ψ) → (η ∨ ζ) . (12)
Since p(ψ|φ) + p(⊥) ≤ p(¬φ ∨ ψ) + p(⊥) for any p ∈ P, it will be assumed the axiom:

⊢ (ψ|φ) → (φ → ψ) . (13)
Since p(ψ ∨ η|φ) + p(⊥) ≤ p(ψ|φ) + p(η|φ) for any p ∈ P, it is also extrapolated that ⊢ (ψ ∨ η|φ) → (ψ|φ) ∨ (η|φ) . Then, by applying [START_REF] Cox | The Algebra of Probable Inference[END_REF], it comes:

⊢ (ψ → η|φ) → (ψ|φ) → (η|φ) , (14)
which constitutes a modus ponens for the conditional. Axioms ( 11), ( 13) and ( 14) are not completely new. In particular, they infer the Boolean morphism (4) of CEA. They are not fully implemented by the existing conditional logics, however.

In order to complete this introduction, it is also noticed that:

⊢ ∀p ∈ P, p(¬φ ∨ ψ) = 1 → (∀p ∈ P, p(φ) = 0) ∨ (∀p ∈ P, p(ψ|φ) = 1) . (15)
The interpretation and proof of ( 15) is simple: when φ is a "subset" of ψ, then either φ is empty or p(ψ|φ) = 1 for any strictly positive probability p. From (15), it is then extrapolated:

⊢ 2(φ → ψ) → 2¬φ ∨ 2(ψ|φ) . (16)
In fact, these extrapolated axioms imply constraints, when extending the probabilities p ∈ P over the conditioned propositions. This paper intends to prove that these constraints are actually valid, in regard to Lewis' triviality. It is now time for the logic definition.

Language. Let Θ = {θ i /i ∈ I} be a set of atomic propositions.

The language L C of the classical logic related to Θ is the smallest set such that:

Θ ⊂ L C ¬φ ∈ L C and φ → ψ ∈ L C for any φ, ψ ∈ L C
The language L T of the modal logic T related to Θ is the smallest set such that:

Θ ⊂ L T ¬φ ∈ L T , 2φ ∈ L T and φ → ψ ∈ L T for any φ, ψ ∈ L T
The language L of the Deterministic modal Bayesian Logic related to Θ is the smallest set such that:

Θ ⊂ L ¬φ ∈ L , 2φ ∈ L , φ → ψ ∈ L and (ψ|φ) ∈ L for any φ, ψ ∈ L
In the construction of the propositions, the unary operators have priority over the binary operators; for example ¬φ ∨ ψ = (¬φ) ∨ ψ . The following abbreviations are defined:

• φ ∨ ψ = ¬φ → ψ , φ ∧ ψ = ¬(¬φ ∨ ¬ψ) and φ ↔ ψ = (φ → ψ) ∧ (ψ → φ) ,
• It is chosen a proposition θ ∈ Θ, and it is then denoted ⊤ = θ → θ and ⊥ = ¬⊤ ,

• 3φ = ¬2¬φ , • ψ × φ = 2 (ψ|φ) ↔ ψ .
⊤ and ⊥ are idealistic notations for the tautology and the contradiction. The operator × describes the logical independence between propositions. The independence relation × and the conditional (|) are thus conjointly defined.

We also define abbreviations for the notion of proof:

• ⊢ φ means "φ is proved" , • φ ≡ ψ means ⊢ φ ↔ ψ.
The meta-relation ≡ is the logical equivalence.

Rules and axioms. The classical Logic C is characterized by the Modus ponens and the classical axioms c * described subsequently.

The modal Logic T is characterized by the Modus ponens, the classical axioms c * and the modal rule/axioms m * described subsequently (c.f. also [START_REF] Blackburn | Modal Logic (Cambridge Tracts in Theoretical Computer Science)[END_REF]).

The Deterministic modal Bayesian Logic , i.e. DmBL, is characterized by the Modus ponens, the classical axioms c * , the modal rule/axioms m * and the Bayesian axioms b * :

c1. ⊢ φ → (ψ → φ) , c2. ⊢ (η → (φ → ψ)) → ((η → φ) → (η → ψ)) , c3. ⊢ (¬φ → ¬ψ) → ((¬φ → ψ) → φ) , Modus ponens. ⊢ φ and ⊢ φ → ψ implies ⊢ ψ , m1. ⊢ φ implies ⊢ 2φ , m2. ⊢ 2(φ → ψ) → (2φ → 2ψ) , m3. ⊢ 2φ → φ , b1. ⊢ 2(φ → ψ) → 2¬φ ∨ 2(ψ|φ) , b2. ⊢ (ψ → η|φ) → (ψ|φ) → (η|φ) , b3. ⊢ (ψ|φ) → (φ → ψ) , b4. ¬(¬ψ|φ) ≡ (ψ|φ) , b5. (× is symmetric) : ψ × φ ≡ φ × ψ ,
DmBL * , a weakened version of DmBL, is defined by replacing b5 by the alternative axioms:

b5.weak.A. ψ × ¬φ ≡ ψ × φ , b5.weak.B. ⊢ 2(ψ ↔ η) → 2 (φ|ψ) ↔ (φ|η) .
The axioms m * and b1 to b4 have been introduced in the previous paragraph. The axiom b5 implements the symmetry of the logical independence. The specific notations ⊢ C , ⊢ T and ⊢ will be used for denoting a proof in C, T or DmBL/DmBL * respectively. The following section studies the logical consequences of the axioms.

Logical theorems and comparison with other systems

DmBL/DmBL * implies the classical and the T-system tautologies; the properties of classical logic and of the T-system are assumed without proof. Since both DmBL and DmBL * are studied, the possibly needed axioms b5 * are indicated in bracket.

Theorems

The proofs are done in appendix A. Next theorem is proved here as an example.

The full universe. ⊢ 2φ → (ψ × φ) . In particular (ψ|⊤) ≡ ψ .

Interpretation: a tautology is independent with any other proposition and its sub-universe is the whole universe.

Proof. From axiom b3, it comes ⊢ (ψ|φ) → (φ → ψ) and ⊢ (¬ψ|φ) → (φ → ¬ψ) . Then ⊢ φ → (ψ|φ) → ψ and ⊢ φ → (¬ψ|φ) → ¬ψ . Applying b4 yields ⊢ φ → (ψ|φ) ↔ ψ . It follows ⊢ 2φ → 2 (ψ|φ) ↔ ψ .
The remaining proof is obvious.

222

Axioms order. Axiom b5 implies b5.weak.A.

The empty universe [b5.weak.A]. ⊢ 2¬φ → (ψ × φ) . In particular (ψ|⊥) ≡ ψ .

Left equivalences. ⊢ 2(ψ ↔ η) → 2¬φ ∨ 2 (ψ|φ) ↔ (η|φ) . Corollary [b5.weak.A]. ⊢ 2(ψ ↔ η) → 2 (ψ|φ) ↔ (η|φ) . Corollary 2 [b5.weak.A]. ψ ≡ η implies (ψ|φ) ≡ (η|φ).
Proof is immediate from corollary.

Sub-universes are classical [b5.weak.A].

• (¬ψ|φ) ≡ ¬(ψ|φ) ,

• (ψ ∧ η|φ) ≡ (ψ|φ) ∧ (η|φ) ,

• (ψ ∨ η|φ) ≡ (ψ|φ) ∨ (η|φ) , • (ψ → η|φ) ≡ (ψ|φ) → (η|φ) .
Evaluating (⊤|•) and (⊥|•) [b5.weak.A]. Is proved ⊢ 2ψ → 2(ψ|φ) . In particular (⊤|φ) ≡ ⊤ and (⊥|φ) ≡ ⊥ .

Inference property. (ψ|φ) ∧ φ ≡ φ ∧ ψ .

Introspection. ⊢ 2¬φ ∨ 2(φ|φ) .

Interpretation: a non-empty proposition sees itself as ever true.

Notice that this property is compliant with (⊥|⊥) ≡ ⊥ .

Inter-independence [b5.weak.A]. ⊢ (ψ|φ) × φ .
Interpretation: a proposition is independent of its sub-universe.

Independence invariance [b5.weak.A].

⊢ (ψ × φ) → (¬ψ × φ) , ⊢ (ψ × φ) ∧ (η × φ) → (ψ ∧ η) × φ , ⊢ 2(ψ ↔ η) → (ψ × φ) ↔ (η × φ) . Narcissistic independence. ⊢ (φ × φ) → (2¬φ ∨ 2φ) .
Interpretation: a proposition independent with itself is either a tautology or a contradiction.

Independence and proof [b5.weak.A]. ⊢ (ψ × φ) → 2(φ ∨ ψ) → (2φ ∨ 2ψ) .
Interpretation: when propositions are independent and their disjunctions are sure, then at least one proposition is sure.

Independence and regularity [b5.weak.A].

⊢ (φ × η) ∧ (ψ × η) → 2 (φ ∧ η) → (ψ ∧ η) → 2¬η ∨ 2(φ → ψ) .
Interpretation: unless it is empty, a proposition may be removed from a logical equation, when it appears in the both sides and is independent with the equation components.

Corollary. ⊢ φ × η , ⊢ ψ × η , ⊢ 3η and φ ∧ η ≡ ψ ∧ η implies φ ≡ ψ .
Corollary 2. Being given ψ and φ such that ⊢ 3φ, the proposition (ψ|φ) is uniquely defined as the solution of equation X ∧ φ ≡ ψ ∧ φ (with unknown X) which is independent of φ.

Right equivalences [b5]. ⊢ 2(ψ ↔ η) → 2 (φ|ψ) ↔ (φ|η) (proved with b5 but without b5.weak.B).

Interpretation: equivalence is compliant with the conditioning.

Corollary. Axiom b5 implies b5.weak.B. In particular, DmBL * is weaker than DmBL.

Corollary of b5 or b5.weak.B. ψ ≡ η implies (φ|ψ) ≡ (φ|η).

Together with the properties of the system T and left equivalences, this last result implies that the equivalence relation ≡ is compliant with the logical operators of DmBL/DmBL * . In particular, replacing a sub-proposition with an equivalent sub-proposition within a theorem still makes a theorem.

Reduction rule [b5]. Axiom b5 implies φ (ψ|φ) ≡ φ . Markov Property [b5]. ⊢ t-2 τ =1 (φ t |φ t-1 ) × φ τ ∧ 3 t-1 τ =1 φ τ -→ 2 (φ t |φ t-1 ) ↔ φ t t-1 τ =1 φ τ .
Interpretation: the Markov property holds, when the conditioning is independent of the past and the past is possible.

Link between (η|ψ) φ and

(η|φ ∧ ψ) [b5]. It is derived: (η|ψ) φ ∧ φ ∧ ψ ≡ (η|ψ) ∧ φ ∧ ψ ≡ φ ∧ ψ ∧ η ≡ (η|φ ∧ ψ) ∧ (φ ∧ ψ) .
This is a quite limited result and it is tempting to assume the additional axiom " (η|ψ) φ ≡ (η|φ∧ψ) ( * )" . There is a really critical point here, since axiom ( * ) implies actually a logical counterpart to Lewis' triviality :

Let (η|ψ) φ ≡ (η|φ ∧ ψ) ( * ) be assumed as an axiom. Then ⊢ 3(φ ∧ ψ) → 2(φ ↔ ψ) ∨ (φ × ψ) .
Interpretation: if φ and ψ are not exclusive and not equivalent, then they are independent. This is irrelevant and forbids the use of axiom ( * ).

Some comparisons with other systems

Conditional Event Algebra. As explained in introduction, CEAs characterize the conditional by means of an external operator. The conditional are limited to only one level of conditioning, but consequently, the combination rules of the conditionals are richer than for the strict Bayesian conditionals. On the contrary, DmBL handles several level of conditioning, but is not addressed to provide richer combinations than the strict Bayesian conditionals. Thus, DmBL implements the necessary Bayesian properties:

• In DmBL, the conditioning constitutes a Boolean morphism (sub-universes are classical). The property (4) of the CEA DGNW [START_REF] Goodman | Mathematics of Data Fusion[END_REF] is thus recovered and generalized,

• The Bayesian inference p(ψ|φ)p(φ) = p(φ ∧ ψ) is derived from the extension of probability (section 5) by means of the theorems (ψ|φ) ∧ φ ≡ φ ∧ ψ and ⊢ (ψ|φ) × φ .

DGNW also provides the relation (a|b ∧ c) ∧ (b|c) = (a ∧ b|c) , which is related to the general Bayesian inference p(a|b ∧ c)p(b|c) = p(a ∧ b|c) . The general Bayesian inference is a direct consequence of the Bayesian inference, and thus can be derived from DmBL too. But is there a logical counterpart in DmBL to the general Bayesian inference? This logical counterpart would be expressed by means of a double proposition:

⊢ (η|φ ∧ ψ) × (ψ|φ) and (η|φ ∧ ψ) ∧ (ψ|φ) ≡ (ψ ∧ η|φ) .
At this time, we are not able to decide if these propositions are derived from DmBL or are even compatible with DmBL.

Comparison with an existing conditional logic. The axioms of the conditional logic VCU (VCU is an abbreviation for the axioms system) [START_REF] Lewis | Counterfactuals[END_REF] are considered here and compared to DmBL. This example is representative of the difference with the other conditional logics.

Theorems derived in section 3.1 are referred to.

Axioms and rules of VCU:

(Ax.1) φ > φ has a partial counterpart in DmBL, i.e. ⊢ 2¬φ ∨ 2(φ|φ) (theorem). (Ax.2) (¬φ > φ) → (ψ > φ) becomes ⊢ (φ|¬φ) → (φ|ψ) (derived from theorems). (Ax.3) (φ > ¬ψ) ∨ (((φ ∧ ψ) > ξ) ↔ (φ > (ψ → ξ))) has no obvious counterpart in DmBL. (Ax.4) (φ > ψ) → (φ → ψ) is exactly b3. (Ax.5) (φ ∧ ψ) → (φ > ψ) is a subcase of φ ∧ ψ ≡ φ ∧ (ψ|φ) (inference theorem). (Ax.6) (¬φ > φ) → ¬(¬φ > φ) > (¬φ > φ) becomes ⊢ (φ|¬φ) → (φ|¬φ) ¬(φ|¬φ) (derived from theorems).
(CR) Counterfactual rule. This is a multiple-task rule. First, it allows the introduction of tautologies inside a conditional, secondly, it implies some linearity of the conditional with ∧ :

Being proved (ξ 1 ∧. . .∧ξ n ) → ψ , it is proved ((φ > ξ 1 )∧. . .∧(φ > ξ n )) → (φ > ψ)
. This rule is recovered in DmBL from the fact that sub-universes are classical :

⊢ (ξ 1 ∧ . . . ∧ ξ n ) → ψ implies ⊢ ((ξ 1 |φ) ∧ . . . ∧ (ξ n |φ)) → (ψ|φ) .
It is noteworthy that Ax.1 and CR, with n = 1 and ξ 1 = φ, infer the rule:

Being proved φ → ψ, it is proved φ > ψ . ( 17
)
It appears that Ax.2, Ax.4, Ax.5, Ax.6 and CR are recovered in DmBL, Ax.1 is weakened in DmBL and Ax.3 is not implemented in DmBL.

Conversely, b3 is implemented by VCU. b2 is not implemented by VCU, but it could be shown that VCU completed by b4 implies b2. b4 is not implemented by VCU. b1 is obtained from [START_REF] Finetti | Theory of probability : a critical introductory treatment[END_REF], while weakened by 2¬φ. b5 is related to the notion of logical independence, which is not considered within VCU. Then we have to point out three fundamental distinctions of DmBL compared to VCU:

1. In DmBL, the negation commutes with the conditional (b4). More generally, subuniverses are classical in DmBL, 2. In DmBL, the deductions on the conditionals are often weakened by the hypothesis that the condition is not empty; for example, 2¬φ in rule b1, or theorem ⊢ (φ|φ) ∨ 2¬φ , 3. DmBL manipulates a notion of logical independence of the propositions.

In fact, point 1 (commutation of the negation) makes point 2 (deduction weakened by the non-empty condition hypothesis) necessary. For example, ⊥ > ⊤ is derived from [START_REF] Finetti | Theory of probability : a critical introductory treatment[END_REF]; by using both Ax.1 and the negation commutation, it is then deduced:

⊤ ≡ ⊥ > ⊥ ≡ ⊥ > ¬⊤ ≡ ¬(⊥ > ⊤) ≡ ¬⊤ ≡ ⊥ , (18)
which is impossible. Notice that this deduction is also done in DmBL, if we replace the "weakened" theorem ⊢ 2¬φ ∨ 2(φ|φ) by the "strong" theorem ⊢ (φ|φ) .

This example, based on VCU and DmBL, illustrates a fundamental difference between DmBL and other conditional logics. DmBL considers ⊥ as a singularity, and will be cautious with this case when inferring conditionals. This principle is not just a logical artifact. In fact, it is also deeply related to the notion of logical independence, as it appears in the proof of theorem Independence and proof.

Models

Toward a Model

In this paragraph, it is discussed about the link between Kripke models [START_REF] Blackburn | Modal Logic (Cambridge Tracts in Theoretical Computer Science)[END_REF][START_REF] Giordano | A Conditional Logic for Iterated Belief Revision[END_REF][START_REF] Giordano | Conditional Logic of Actions and Causation[END_REF] for DmBL/DmBL * and a more basic structure called conditional models.

From now on, P(W ) denotes the set of all subsets of set W .

Definition. A Kripke model for DmBL (respectively DmBL * ) is a quadruplet (W, R, H, f ), where W is a set of worlds, R ⊂ W × W is an accessibility relation, H : L -→ P(W ) is an assignment function, f : H(L) × H(L) -→ P(W ) is a conditioning function, and verifying:

• H(¬φ) = W \ H(φ) and H(φ → ψ) = W \ H(φ) ∪ H(ψ) , • H(2φ) = t ∈ W ∀u ∈ W, (t, u) ∈ R ⇒ u ∈ H(φ) , • H (ψ|φ) = f H(ψ), H(φ) ,
• H(φ) = W for any φ such that ⊢ φ is an axiom of the form m3, b1, b2, b3, b4, or b5 (respectively b5.weak.A and b5.weak.B).

It is noticed that the rules and axioms c * , modus ponens, m1 and m2 and are compliant with the model by construction.

β2. f (B ∪ C, A) ⊂ f (B, A) ∪ f (C, A) , for any A, B, C ∈ M , β3. A ∩ f (B, A) ⊂ B , for any A, B ∈ M , β4. f (W \ B, A) = W \ f (B, A) , for any A, B ∈ M , β5. f (B, A) = B implies f (A, B) = A (respectively β5w. f (B, A) = B implies f (B, W \ A) = B) , for any A, B ∈ M ) .
Remarks. A conditional model does not implement the modalities. In both models, the function f is the representation of the conditional (|) .

Model transfer. Let (W, M, h, f ) be a conditional model for DmBL (respectively DmBL * ). Let R = W × W and define H by:

• H(θ) = h(θ) for any θ ∈ Θ , • H(¬φ) = W \ H(φ) and H(φ → ψ) = W \ H(φ) ∪ H(ψ) , • H(φ) = W ⇒ H(2φ) = W and H(φ) = W ⇒ H(2φ) = ∅ , • H (ψ|φ) = f H(ψ), H(φ) .
Then (W, R, H, f ) is a Kripke model for DmBL (respectively DmBL * ).

The proof is easy, but tedious. It is detailed in appendix B.

Conditional models are defined from the classical and conditional operators only. In fact, such models have been set first for a non-modal construction of the Bayesian logic [START_REF] Dambreville | Definition of a Deterministic Bayesian Logic[END_REF]. In this paper a free conditional model is constructed for DmBL * , with completeness results. The conditional model is translated into a DmBL * Kripke model. The derived model is of course not complete for DmBL * in regards to the modalities, but the completeness still holds in regards to the conditional operator. The model transfer property also suggests that the conditional operator is not constructed from the modal operator: it is even possible to construct (|) when 2 is trivial in the model (R = W × W implies H(φ) = W or H(2φ) = ∅) .

In section 5, a model for DmBL is also derived but not constructed. This model of DmBL is non-trivial (it is possible to extend any unconditioned probability over this model), but no completeness result is provided.

Construction of a free conditional model for DmBL *

In the sequel, Θ is assumed to be finite. A free conditional model for DmBL * will be constructed as a limit of partial models. These models are constructed recursively, based on the iteration of (|) on any propositions.

Definition of partial models

In this section are constructed a sequence (Ω n , M n , h n , f n , Λ n ) n∈IN and a sequence of one-toone morphisms (µ n ) n∈IN such that:

• M n is a Boolean sub-algebra of P(Ω n ), h n : Θ → M n and f n : M n × M n → M n , (f n will be partially defined)

• µ n : M n → M n+1 is such that µ n (A ∩ B) = µ n (A) ∩ µ n (B), µ n (Ω n \ A) = Ω n+1 \ µ n (A)
and ∀θ ∈ Θ, h n+1 (θ) = µ n h n (θ) , (as a consequence, µ n is a Boolean morphism)

• For any A, B ∈ M n such that f n (B, A) is defined, then f n+1 µ n (B), µ n (A) is defined and f n+1 µ n (B), µ n (A) = µ n f n (B, A) ,
• Λ n is a list of elements of M n , which is used as a task list of the construction (refer to the subsequent paragraphs).

Remark. The functions f n represent the partial construction of (|) . The morphisms µ n characterize the "inclusion" of the partial models.

In a subsequent section, a conditional model Ω ∞ , M ∞ , h ∞ , f ∞ will be defined as the limit of (Ω n , M n , h n , f n ) n∈IN associated to (µ n ) n∈IN .

Notations and definitions. For any

A ∈ M n , it is defined ∼ A = Ω n \ A .
Any singleton {ω} may be denoted ω if the context is not ambiguous.

For any m > n and A ∈ M n , it is defined

A [m] = µ m-1 • . . . • µ n (A) .
The Cartesian product of sets A and B is denoted A × B ; the functions id and T are defined over pairs by id(x, y) = (x, y) and T (x, y) = (y, x) ; for a set of pairs C, the abbreviation (id ∪ T )(C) = id(C) ∪ T (C) is also used.

Initialization. Define (Ω 0 , M 0 , h 0 , f 0 , Λ 0 ) by:

• Ω 0 = {0, 1} Θ , • M 0 = P(Ω 0 ), • ∀θ ∈ Θ, h 0 (θ) = (δ τ ) τ ∈Θ ∈ Ω 0 δ θ = 1 , • f 0 (A, ∅) = f 0 (A, Ω 0 ) = A for any A ∈ M 0 , • Λ 0 = (s 0 , f 0 , λ 0 ) is a list defined by s 0 = 0, f 0 = card(M 0 ) -2 and λ 0 is a one-to-one mapping from [[s 0 , f 0 -1]] to M 0 \ {∅, Ω 0 } , such that λ 0 (2t) =∼ λ 0 (2t + 1) , ∀t .
Step

n to step n + 1. Let (Ω k , M k , h k , f k , Λ k ) 0≤k≤n
and the one-to-one morphisms (µ k ) 0≤k≤n-1 be constructed.

Notice that λ n (s n ) =∼ λ n (s n + 1) by construction of Λ n . Define b n = λ n (s n ) . Then, construct the set I n and the sequences Γ n (i), Π n (i)| i∈In according to the cases:

Case 0. There is m < n such that {b m[n] , ∼ b m[n] } = {b n , ∼ b n } . Then, notice that b n = b m[n]
by the subsequent construction of Λ . Let ν be the greatest of such m; then define Setting. (Ω n+1 , M n+1 , h n+1 , f n+1 , Λ n+1 ) and µ n are defined by:

I n = µ ν (b ν )× ∼ µ ν (b ν ) , Π n (ω, ω ′ ) = f n (ω ′ [n] , ∼ b n ) ∩ ω [n] and Γ n (ω, ω ′ ) = f n (ω [n] , b n ) ∩ ω ′ [n]
• µ n (A) = i∈In A ∩ Π n (i) × Γ n (i) ∪ A ∩ Γ n (i) × Π n (i) for any A ∈ M n , • Ω n+1 = µ n (Ω n ) , • ∀θ ∈ Θ, h n+1 (θ) = µ n h n (θ) , • M n+1 = P(Ω n+1 ) , • f n+1 (A, ∅) = f n+1 (A, Ω n+1 ) = A for any A ∈ M n+1 , • For any A ∈ M n \ {b n , ∼ b n , ∅, Ω n } and any B ∈ M n such that f n (B, A) is defined, then f n+1 µ n (B), µ n (A) is defined and f n+1 µ n (B), µ n (A) = µ n f n (B, A) , • For any A ∈ M n+1 , set f n+1 A, µ n (b n ) = (id ∪ T ) A ∩ i∈In Π n (i) × Γ n (i) and f n+1 A, ∼ µ n (b n ) = (id ∪ T ) A ∩ i∈In Γ n (i) × Π n (i) ,
• Λ n+1 = (s n+1 , f n+1 , λ n+1 ) is such that:

-

s n+1 = s n + 2 = 2n + 2, f n+1 = s n+1 + card(M n+1 ) -2 , -λ n+1 is a one-to-one mapping from [[s n+1 , f n+1 -1]] to M n+1 \ {∅, Ω n+1 } , -λ n+1 (t) = µ n λ n (t) for any t ∈ [[s n+1 , f n -1]] , -λ n+1 (2t) =∼ λ n+1 (2t + 1) , ∀t and λ n+1 (f n+1 -2) = µ n (b n ) .
This definition ensures a cyclic and full construction of

f (•, b n ) and f (•, ∼ b n ). 4
The first steps of the model construction are illustrated by a simple example in appendix F.

Short explanation of the model. In fact, (ω,

ω ′ ) ∈ Π n (i) × Γ n (i) should be interpreted as ω ∧ (ω ′ |¬b n ), while (ω ′ , ω) ∈ Γ n (i) × Π n (i) should be interpreted as ω ′ ∧ (ω|b n ).
The reader should compare this construction to the proof of completeness in appendix D for a better comprehension of the mechanisms of the model.

Properties of (Ω

n , M n , h n , f n , Λ n , µ n ) n∈IN
It is proved recursively:

• µ µ n : M n → M n+1 is a one-to-one Boolean morphism, • f If A, B ∈ M n and f n (B, A) is defined, then f n+1 µ n (B), µ n (A) = µ n f n (B, A) , β1. Let A, B ∈ M n such that f n (B, A) is defined. Then A ⊂ B and A = ∅ imply f n (B, A) = Ω n , β2. Let A, B, C ∈ M n such that f n (B, A), f n (C, A) and f n (B ∪ C, A) are defined. Then f n (B ∪ C, A) = f n (B, A) ∪ f n (C, A) , β3. Let A, B ∈ M n such that f n (B, A) is defined. Then A ∩ f n (B, A) = A ∩ B , β4. Let A, B ∈ M n such that f n (B, A) and f n (∼ B, A) are defined. Then f n (∼ B, A) =∼ f n (B, A) , β5w. Let A, B ∈ M n such that f n (B, A) and f n (B, ∼ A) are defined. Then f n (B, A) = B implies f n (B, ∼ A) = B .
Proofs are given in appendix C.

Limit

The limit Ω ∞ , M ∞ , h ∞ , f ∞ is defined as follows:

• Set Ω ∞ = (ω n | n∈IN ) ∈ n∈IN Ω n ∀n ∈ IN, ω n+1 ∈ µ n (ω n ) ;
Useful definitions:

-For any n ∈ IN and any

A ∈ M n , A ∞ = (ω k | k∈IN ) ∈ Ω ∞ ω n ∈ A . The subset A ∞ is a mapping of A within Ω ∞ . It is noticed that this mapping is invariant with µ, i.e. (A [m] ) ∞ = A ∞ for m > n , -For any n ∈ IN , M n:∞ = A ∞ A ∈ M n . The structure M n:∞ is an isomorphic mapping of the structure M n within Ω ∞ . It is noticed that (M n:∞ | n∈IN ) is a monotonic sequence, i.e. M n:∞ ⊂ M n+1:∞ , • Set M ∞ = n∈IN M n:∞ , • Set h ∞ (θ) = h 0 (θ) ∞ for any θ ∈ Θ , • Let A, B ∈ M ∞ . Then there is n and a, b ∈ M n such that A = a ∞ , B = b ∞ and f n (b, a) is defined (subsequent proposition). Set f ∞ (B, A) = f n (b, a) ∞ .
This definition is justified by the following propositions:

Proposition 1. For any n ∈ IN, m > n and A ∈ M n , (A [m] ) ∞ = A ∞ . Proof. By definition of Ω ∞ , (A [m] ) ∞ = (ω k | k∈IN ) ∈ Ω ∞ ω m ∈ A [m] = (ω k | k∈IN ) ∈ Ω ∞ ω n ∈ A = A ∞ . 222 Corollary M n:∞ ⊂ M n+1:∞ . Proposition 2. M n:∞ is a Boolean subalgebra of P(Ω ∞ ) and is isomorph to M n by the morphism A → A ∞ . As a consequence, M ∞ is a Boolean subalgebra of P(Ω ∞ ) .
Proof is obvious from the definition of M n:∞ .

From now on, M n will be considered as a subalgebra of P(Ω ∞ ).

Proposition 3. Let A, B ∈ M ∞ . Then there is n and a, b ∈ M n such that A = a ∞ , B = b ∞ and f n (b, a) is defined. Proof. Since (M k:∞ | k∈IN ) is a monotonic sequence , there is m ∈ IN such that A, B ∈ M m:∞ . Let a, b ∈ M m be such that A = a ∞ and B = b ∞ . By definition of the list Λ m , there is p ∈ [[s m , f m -1]] such that λ p = a . As a consequence, f p+1 (b [p+1] , a [p+1] ) exists. But then hold A = (a [p+1] ) ∞ and B = (b [p+1] ) ∞ .
Finally n = p + 1 answers to the proposition.

222

Proposition 4. The definition of f ∞ does not depend on the choice of n.

Proof. Let n, m > n, a, b ∈ M n and c, d ∈ M m such that A = a ∞ = c ∞ and B = b ∞ = d ∞ . Assume also that f n (b, a) and f m (d, c) exist. Then (a [m] ) ∞ = c ∞ and (b [m] ) ∞ = d ∞ . Since M m and M m:∞ are isomorph, it follows a [m] = c and b [m] = d . But it is derived from • f that f m (b [m] , a [m] ) = f n (b, a) [m] . Finally f n (b, a) ∞ = f m (d, c) ∞ . 222 Proposition 5. Ω ∞ , M ∞ , h ∞ , f ∞ verifies β1,
Ω ∞ , M ∞ , h ∞ , f ∞ . This Kripke model is denoted B = Ω ∞ , R B , H B , f ∞ .

Completeness for the conditional operator

It is above the scope of this work to construct a model of DmBL * , which is complete for both the modal and the conditional operators. However, it is shown here that B is a model of DmBL * , which is complete for the conditional operator.

(φ) = Ω ∞ .
Proof is done in appendix D .

Proposition 2 expresses that B is complete for the conditional operator.

Coherence properties

The model B clearly shows that DmBL * is coherent. It also demonstrates that the conditional operator (|) is not trivial. Since (Ω ∞ , H B ) is a complete model for C, DmBL * is an extension of the classical logic: ⊢ φ implies ⊢ C φ, for any φ ∈ L C . But a stronger property holds:

Non-distortion. Let φ ∈ L C . Assume that ⊢ 2φ ∨ 2¬φ in DmBL * . Then ⊢ C φ or ⊢ C ¬φ.
Interpretation: DmBL * does not "distort" the classical propositions. More precisely, a property like ⊢ 2φ ∨ 2¬φ would add some knowledge about φ, since it says that either φ or ¬φ is "sure". But the non-distortion just tells that such property is impossible unless there is a trivial knowledge about φ within the classical logic.

Proof. Assume ⊢ 2φ ∨ 2¬φ . Since B is a model for DmBL * , it comes H B (2φ ∨ 2¬φ) = Ω ∞ . Then H B (2φ) ∪ H B (2¬φ) = Ω ∞ . Since H B (2ψ) = ∅ or Ω ∞ for any ψ ∈ L , it comes H B (2φ) = Ω ∞ or H B (2¬φ) = Ω ∞ . At last, H B (φ) = Ω ∞ or H B (¬φ) = Ω ∞ . But (Ω ∞ , H B ) is a complete Boolean model for C , which implies ⊢ C φ or ⊢ C ¬φ .

222

Another non-distortion property is derived subsequently in the context of probabilistic DmBL * .

5 Extension of probability Probabilities are classically defined over measurable sets. However, this is only a manner to model the notion of probability, which is essentially an additive measure of the belief of logical propositions [START_REF] Paass | Chapter 8 in Non-Standard Logics for Automated Reasoning[END_REF]. Probability could be defined without reference to the measure theory, at least when the propositions are countable. The notion of probability is explained now within a strict propositional formalism. Conditional probabilities are excluded from this definition, but the notion of independence is considered.

Intuitively, a probability over a space of logical propositions is a measure of belief which is additive (disjoint propositions are adding their chances) and increasing with the propositions. This measure should be zeroed for the contradiction and set to 1 for the tautology. Moreover, a probability is a multiplicative measure for independent propositions.

Definition for classical propositions. A probability π over C is a IR + valued function such that for any propositions φ and ψ of L C :

Equivalence. φ ≡ C ψ implies π(φ) = π(ψ) , Additivity. π(φ ∧ ψ) + π(φ ∨ ψ) = π(φ) + π(ψ) , Coherence. π(⊥) = 0 , Finiteness. π(⊤) = 1 .
Property. The coherence and additivity imply the increase of π:

Increase. π(φ ∧ ψ) ≤ π(φ) .
Proof. Since φ ≡ C (φ ∧ ψ) ∨ (φ ∧ ¬ψ) and (φ ∧ ψ) ∧ (φ ∧ ¬ψ) ≡ C ⊥, the additivity implies:

π(φ) + π(⊥) = π(φ ∧ ψ) + π(φ ∧ ¬ψ) .
From the coherence π(⊥) = 0 , it is deduced π(φ) = π(φ ∧ ψ) + π(φ ∧ ¬ψ) . Since π is non-negatively valued, π(φ) ≥ π(φ ∧ ψ) .

222

Definition for DmBL/DmBL * . In this case, we have to deal with independence notions.

A probability P over DmBL/DmBL * is a IR + valued function, which verifies (replace ≡ C by ≡ and π by P ) equivalence, additivity, coherence, finiteness and:

Multiplicativity. ⊢ φ × ψ implies P (φ ∧ ψ) = P (φ)P (ψ) .
for any propositions φ and ψ of L .

Probability extension over DmBL *

Property. Let π be a probability defined over C , the classical logic, such that π(φ) > 0 for any φ ≡ C ⊥. Then, there is a (multiplicative) probability π defined over DmBL * such that π(φ) = π(φ) for any classical proposition φ ∈ L C .

Remark: this is another non-distortion property, since the construction of DmBL * puts no constraint over probabilistic classical propositions.

Proof is done in appendix E.

Corollary. Let π be a probability defined over C . Then, there is a (multiplicative) probability π defined over DmBL * such that π(φ) = π(φ) for any φ ∈ L C .

Proof. Let Σ = θ∈Θ ǫ θ ǫ ∈ θ∈Θ {θ, ¬θ} . For any real number e > 0 , define the probability π e over L C by:

∀σ ∈ Σ , π e (σ) = e card(Σ) + (1 -e)π(σ) .
Let π e be the extension of π e over DmBL * as constructed in appendix E. By E.2.3 , there is a rational function R φ such that π e (φ) = R φ (e) for any φ ∈ L . Now 0 ≤ R φ (e) ≤ 1 ; since R φ (e) is rational and bounded, lim e→0+ R φ (e) exists. Define π(φ) = lim e→0+ R φ (e) , for any φ ∈ L.

The additivity, coherence, finiteness and multiplicativity are obviously inherited by π.

At last, it is clear that π(σ) = π(σ) for any σ ∈ Σ .

222

Model and probability extension for DmBL

Let K be the set of all (multiplicative) probabilities P over DmBL * such that P (φ) > 0 for any φ ≡ ⊥ , and define the sequences K(φ) = (P (φ)) P ∈K for any φ ∈ L . Then define

L K = K(L) = K(φ) φ ∈ L ; The space L K is thus a subset of IR + K .
The operators ¬, ∧ and (|) are canonically implied over L K :5

¬K(φ) = K(¬φ) , K(φ) ∧ K(ψ) = K(φ ∧ ψ) and K(ψ) K(φ) = K (ψ|φ) .
Since any P ∈ K verifies the equivalence property, it comes K(φ) = K(ψ) when φ ≡ ψ in DmBL * . As a direct consequence, L K , ¬, ∧, (|) is a conditional-like model of DmBL * (the structure is a Boolean algebra but not derived from set operators. This is the only difference with conditional models).

Property. L K , ¬, ∧, (|) is a conditional-like model of DmBL.

Proof. Let P ∈ K ; P is multiplicative. Since ⊢ (ψ|φ) × φ and (ψ|φ) ∧ φ ≡ ψ ∧ φ in DmBL * , it comes P (ψ|φ) P (φ) = P (ψ ∧ φ) . Now assume K(ψ) K(φ) = K(ψ) , with ψ ≡ ⊥ . Then K (ψ|φ) = K(ψ), and P (ψ|φ) = P (ψ) for any P ∈ K . Then P (φ) = P (ψ∧φ) P (ψ|φ)

= P (ψ∧φ) P (ψ) = P (φ|ψ) for any P ∈ K , and K(φ) K(ψ) = K (φ|ψ) = K(φ) . Since moreover (φ|⊥) ≡ φ and (⊥|φ) ≡ ⊥ in DmBL * , the model verifies β5 .

222

Notice that it was only needed the equivalence and multiplicative properties for the elements of K . It is thus possible to construct a more general model by relaxing K .

Probability extension. For any K(φ) ∈ L K and any P ∈ K , define the IR + -valued mapping P K(φ) = P (φ) (this mapping, a projection, is indeed well defined). By construction, P is naturally a multiplicative probability over L K . Moreover, the probability extensions defined in appendix E are also elements of K . As a consequence, the deductions of section 5.2 are still working for L K . The extension property is thus derived: Let π be a probability defined over C . Then, there is a (multiplicative) probability π defined over DmBL such that π(φ) = π(φ) for any φ ∈ L C . In this model, the value of

Non

H(2φ) is either K(⊥) or K(⊤) . Then, H(2φ ∨ 2¬φ) = K(⊤) implies H(2φ) = K(⊤) or H(2¬φ) = K(⊤) . Then H(φ) = K(⊤) or H(¬φ) = K(⊤) .
It follows ∀P ∈ K , P (φ) = 1 or ∀P ∈ K , P (¬φ) = 1 , and by the probability extension: ∀π , π(φ) = 1 or ∀π , π(¬φ) = 1 , where π denotes any probability over C . At last, ⊢ C φ or ⊢ C ¬φ .

222

Properties of the conditional

Bayes inference. Assume a (multiplicative) probability P defined over DmBL/DmBL * . Define P (ψ|φ) as an abbreviation for P (ψ|φ) . Then:

P (ψ|φ)P (φ) = P (φ ∧ ψ) .
Proof. A consequence of (ψ|φ) ∧ φ ≡ φ ∧ ψ and ⊢ (ψ|φ) × φ .

222

As a corollary, it is also deduced P (ψ|φ) (η|ζ) P (η|ζ) = P (ψ|φ) ∧ (η|ζ) . It is recalled that the closure of CEA DGNW fails on this relation (refer to the introduction).

About Lewis' triviality. The previous extension theorems have shown that for any probability π defined over C , it is possible to construct a (multiplicative) probability π over DmBL which extends π. This result by itself shows that DmBL avoids Lewis' triviality. But a deeper explanation seems necessary.

Assume φ ∈ L C and define the probability π φ over C by π φ = π(•|φ) . Let π φ be the extension of π φ over DmBL. It happens that π φ = π(•|φ) , which implies that Lewis' triviality does not work anymore. It is noticed that although π(•|φ) is a probability over DmBL in the classical meaning (it is additive, coherent and finite), it is not necessarily multiplicative.

Conditional probabilities do not maintain the logical independence and the conditioning.

This limitation is unavoidable: otherwise the derivation (1) of the triviality is possible, even if (ψ|φ) is not equivalent to a classical proposition.

Conclusion

In this contribution, the conditional logics DmBL and DmBL * , a slight relaxation of DmBL, have been defined and studied. These logics have been introduced as an abstraction and extrapolation of general probabilistic properties. DmBL and DmBL * implement the essential ingredients of the Bayesian inference, including the classical nature to the sub-universe, the inference property and a related concept of logical independence. For this reason, DmBL and DmBL * extend and refine the existing logical approaches of the Bayesian inference.

The logics are coherent and non-trivial. A model has been constructed for the logic DmBL * , which is complete in regards to the conditionals. It has been shown that any probability over the classical propositions could be extended to DmBL/DmBL * , in compliance with the independence relation. Then, the probabilistic Bayesian rule has been recovered from DmBL/DmBL * .

There are still many open questions. For example, it is certainly possible to bring some enrichment to the conditional of DmBL, by means of additional axioms. Is it possible to recover some specific equivalences of other existing systems? From the strict logical viewpoint, the Deterministic modal Bayesian Logic offers also some interesting properties. For example, the notion of independence in DmBL have nice logical consequences in the deductions (e.g. regularity with an inference). This property should be of interest in mathematical logic.

Now it has been shown ⊢ 2¬φ → 2 (Ξ|φ) ↔ Ξ , and considering Ξ = ψ, η or ψ ∧ η, it is implied

⊢ 2¬φ → 2 (ψ ∧ η|φ) → (ψ|φ) ∧ (η|φ) .
At last ⊢ 2 (ψ ∧ η|φ) → (ψ|φ) ∧ (η|φ) and then ⊢ (ψ ∧ η|φ) → (ψ|φ) ∧ (η|φ) .

The second theorem is then proved.

Third theorem is a consequence of the first and second theorems.

Last theorem is a consequence of the first and third theorems.

Evaluating (⊤|•) and (⊥|•) .

From ⊢ 2ψ → 2(φ → ψ) and b1, it comes ⊢ 2ψ → 2¬φ ∨ 2(ψ|φ) . Now ⊢ 2¬φ → 2 (ψ|φ) ↔ ψ , and consequently ⊢ 2ψ → 2(ψ|φ) .

Inference property.

From b3 it comes ⊢ (¬ψ|φ) → (φ → ¬ψ) . Then ⊢ ¬(φ → ¬ψ) → ¬(¬ψ|φ) and ⊢ (φ ∧ ψ) → (ψ|φ) .

At last ⊢ (φ ∧ ψ) → (ψ|φ) ∧ φ . Conversely ⊢ (ψ|φ) → (φ → ψ) implies ⊢ (ψ|φ) ∧ φ → (φ → ψ) ∧ φ .
Since (φ → ψ) ∧ φ ≡ φ ∧ ψ , the converse is proved.

Introspection.

Obvious from ⊢ φ → φ and b1 .

Inter-independence.

It is proved:

(ψ|φ) φ ∧ (φ|φ) ≡ (ψ|φ) ∧ φ φ ≡ (φ ∧ ψ|φ) ≡ (ψ|φ) ∧ (φ|φ) .

As a consequence ⊢ (φ|φ) → (ψ|φ) φ ↔ (ψ|φ) .

Then ⊢ 2(φ|φ) → (ψ|φ) × φ . Now ⊢ 2¬φ ∨ 2(φ|φ) and ⊢ 2¬φ → (ψ|φ) × φ from previous results.

At last ⊢ (ψ|φ) × φ .

Independence invariance.

First theorem comes from the deduction:

(ψ × φ) ≡ 2 (ψ|φ) ↔ ψ ≡ 2 ¬(ψ|φ) ↔ ¬ψ ≡ 2 (¬ψ|φ) ↔ ¬ψ ≡ (¬ψ × φ) .
The second theorem is also derived from similar deductions:

⊢ 2 (ψ|φ) ↔ ψ ∧ (η|φ) ↔ η → 2 (ψ|φ) ∧ (η|φ) ↔ (ψ ∧ η) and then ⊢ 2 (ψ|φ) ↔ ψ ∧ (η|φ) ↔ η → 2 (ψ ∧ η|φ) ↔ (ψ ∧ η) .
Now, let prove the third theorem.

The Left equivalences theorem implies

⊢ 2(ψ ↔ η) → 2 (ψ|φ) ↔ (η|φ) ∧ (ψ ↔ η) . Since ⊢ (α ↔ β) ∧ (γ ↔ δ) → (α ↔ γ) ↔ (β ↔ δ) , it is deduced ⊢ 2(ψ ↔ η) → 2 (ψ|φ) ↔ ψ ↔ (η|φ) ↔ η . At last ⊢ 2(ψ ↔ η) → 2 (ψ|φ) ↔ ψ ↔ 2 (η|φ) ↔ η .
Narcissistic independence.

From ⊢ φ → φ it is deduced ⊢ 2¬φ ∨ 2(φ|φ) .
From definition, it is derived ⊢ (φ × φ) → 2 (φ|φ) → φ and then ⊢ (φ × φ) → 2(φ|φ) → 2φ .

It is thus deduced ⊢ (φ × φ) → (2¬φ ∨ 2φ) .

Independence and proof.

Combining ⊢ (φ ∨ ψ) → (¬φ → ψ) with b1 implies ⊢ 2(φ ∨ ψ) → 2φ ∨ 2(ψ|¬φ) . From b5.weak.A, it comes ⊢ (ψ × φ) → 2 (ψ|¬φ) ↔ ψ . As a consequence ⊢ (φ × ψ) → 2(φ ∨ ψ) → (2φ ∨ 2ψ) .
Independence and regularity.

Proof of the main theorem.

It is easy to prove (φ ∧ η) → (ψ ∧ η) ≡ ¬η ∨ (φ → ψ) . Then ⊢ 2 (φ ∧ η) → (ψ ∧ η) → 2 ¬η ∨ (φ → ψ) . Now ⊢ (φ × η) ∧ (ψ × η) → (φ → ψ) × ¬η
, by independence invariance and b5.weak.A. The proof is achieved by means of the preceding property, independence and proof.

Proof of Corollary 2.

Assume ⊢ X × φ and ⊢ 3φ.

Since ⊢ (ψ|φ) × φ and ψ ∧ φ ≡ (ψ|φ) ∧ φ, it is deduced from X ∧ φ ≡ ψ ∧ φ that X ≡ (ψ|φ).

Right equivalences.

First notice that all previous properties are obtained without b5.weak.B.

From (φ|ψ) ∧ ψ ≡ φ ∧ ψ, (φ|η) ∧ η ≡ φ ∧ η and ⊢ (ψ ↔ η) → (φ ∧ ψ) ↔ (φ ∧ η) , it is deduced ⊢ (ψ ↔ η) → (φ|ψ) ∧ ψ ↔ (φ|η) ∧ η .
Then ⊢ (ψ ↔ η) → (φ|ψ) ∧ ψ ↔ (φ|η) ∧ ψ and finally:

⊢ 2(ψ ↔ η) → 2 (φ|ψ) ∧ ψ ↔ (φ|η) ∧ ψ . Now ⊢ (φ|ψ) × ψ and ⊢ (φ|η) × η . Since ⊢ 2(ψ ↔ η) → η × (φ|η) ↔ ψ × (φ|η) , it comes ⊢ 2(ψ ↔ η) → (φ|η) × ψ by b5. Finally ⊢ 2(ψ ↔ η) → (φ|ψ) × ψ ∧ (φ|η) × ψ ∧ 2 (φ|ψ) ∧ ψ ↔ (φ|η) ∧ ψ . Applying the regularity, it comes ⊢ 2(ψ ↔ η) → 2¬ψ ∨ 2 (φ|ψ) ↔ (φ|η) . Now ⊢ 2(ψ ↔ η) → (2¬ψ ↔ 2¬η) and ⊢ 2¬Ξ → 2 (φ|Ξ) ↔ φ for Ξ = ψ or η. It is deduced ⊢ 2¬ψ ∧ 2(ψ ↔ η) → 2 (φ|ψ) ↔ (φ|η)
, thus completing the proof.

Reduction rule.

Since ⊢ (ψ|φ) × φ, b5 implies ⊢ φ × (ψ|φ) and ⊢ 2 φ (ψ|φ) ↔ φ .

Markov Property.

Since ⊢ (φt|φt-1)

× φt-1, it comes ⊢ t-2 τ =1 (φt|φt-1) × φτ → t-1 τ =1 (φt|φt-1) × φτ . Then ⊢ t-2 τ =1 (φt|φt-1) × φτ → (φt|φt-1) × t-1 τ =1 φτ . Now, (φt|φt-1) ∧ t-1 τ =1 φτ ≡ t τ =1 φτ ≡ φt t-1 τ =1 φτ ∧ t-1 τ =1 φτ . Since ⊢ φt t-1 τ =1 φτ × t-1 τ =1
φτ , the proof is achieved by applying the regularity.

Link between (η|ψ) φ and (η|φ ∧ ψ).

Proof of the logical counterpart to Lewis' triviality.

Since ¬(φ → ψ) ≡ φ ∧ ¬ψ , it is equivalent to prove:

⊢ 3(φ ∧ ψ) ∧ 3(¬ψ ∧ φ) ∨ 3(¬φ ∧ ψ) → (φ × ψ) . Since × is symmetric, it is sufficient to prove ⊢ 3(φ ∧ ψ) ∧ 3(¬ψ ∧ φ) → (φ × ψ) .
The introspection property implies ⊢ 3(φ ∧ ψ) → 2(φ ∧ ψ|φ ∧ ψ), denoted (a), and

⊢ 3(¬ψ ∧ φ) → 2(¬ψ ∧ φ|¬ψ ∧ φ) . It is thus deduced ⊢ 3(φ ∧ ψ) → 2 (ψ|ψ ∧ φ) ↔ (ψ|ψ ∧ φ) ∧ (ψ ∧ φ|ψ ∧ φ)
, denoted (b), and

⊢ 3(¬ψ ∧ φ) → 2 (ψ|¬ψ ∧ φ) ↔ (ψ|¬ψ ∧ φ) ∧ (¬ψ ∧ φ|¬ψ ∧ φ) .
From the deduction (ψ|¬ψ ∧ φ) ∧ (¬ψ • Compliance with m3 is obtained from the fact that R is reflexive.

∧ φ|¬ψ ∧ φ) ≡ (⊥|¬ψ ∧ φ) ≡ ⊥, it is derived ⊢ 3(¬ψ ∧ φ) → 2 (ψ|¬ψ ∧ φ) ↔ ⊥ , denoted (c). From the deduction (ψ|ψ ∧ φ) ∧ (ψ ∧ φ|ψ ∧ φ) ≡ (ψ ∧ φ|ψ ∧ φ), (
• Proof of H 2(φ → ψ) → 2¬φ ∨ 2(ψ|φ) = W , i.e. compliance with b1. By definition, H 2(φ → ψ) → 2¬φ∨2(ψ|φ) = H 2(ψ|φ) ∪H(2¬φ)∪ W \H 2(φ → ψ) . Cases H 2(φ → ψ) = ∅ or H(2¬φ) = W then imply H 2(φ → ψ) → 2¬φ ∨ 2(ψ|φ) = W . Otherwise H 2(φ → ψ) = ∅ and H(2¬φ) = W , thus implying H(φ → ψ) = W and H(¬φ) = W .
It is deduced H(φ) ⊂ H(ψ) and H(φ) = ∅ , and then f H(ψ), H(φ) = W by using β1.

Finally H 2(ψ|φ) = W and again H 2(φ → ψ) → 2¬φ ∨ 2(ψ|φ) = W .
• Proof of H ¬(¬ψ|φ) ↔ (ψ|φ) = W , i.e. compliance with b4.

It is deduced

H (¬ψ|φ) = f H(¬ψ), H(φ) = f W \ H(ψ), H(φ) = W \ f H(ψ), H(φ) =
W \ H (ψ|φ) , by using β4.

Then

H (¬ψ|φ) ∩ W \ H (ψ|φ) ∪ W \ H (¬ψ|φ) ∩ H (ψ|φ) = W .
And finally H ¬(¬ψ|φ) ↔ (ψ|φ) = W .

• Proof of H (ψ → η|φ) → (ψ|φ) → (η|φ) = W , i.e. compliance with b2.

By β2, it is deduced

H (ψ → η|φ) = f H(ψ → η), H(φ) = f H(¬ψ) ∪ H(η), H(φ) ⊂ f H(¬ψ), H(φ) ∪ f H(η), H(φ) = H (¬ψ|φ) ∪ H (η|φ) = H ¬(ψ|φ) ∪ H (η|φ) . Then H (ψ → η|φ) → (ψ|φ) → (η|φ) = W . • Proof of H (ψ|φ) → (φ → ψ) = W , i.
(ψ), W \ H(φ) = H(ψ) . Then H (ψ|φ) ↔ ψ = W if and only if H (ψ|¬φ) ↔ ψ = W .
As a consequence, H 2 (ψ|φ) ↔ ψ = H 2 (ψ|¬φ) ↔ ψ and the result. C Proof: properties of (

• Proof of H 2(ψ ↔ η) → 2 (φ|ψ) ↔ (φ|η) = W , i.
Ω n , M n , h n , f n , Λ n , µ n ) n∈IN
To be proved:

•µ µn : Mn → Mn+1 is a one-to-one Boolean morphism , The proof is recursive and needs to consider the two cases in the definition of (µn, fn) .

The properties β * are obvious for n = 0, since f0 is only defined by f ( A, ∅) = f0(A, Ω0) = A . From now on, it is assumed that β * hold true for k ≤ n, and that •µ and • f hold true for k ≤ n -1 . The subsequent paragraphs establish the proof of β * for n + 1 and the proof of •µ and • f for n.

Preliminary remark. It is noticed that β2 and β4 imply:

β6 : fn(B ∩ C, A) = fn(B, A) ∩ fn(C, A) .
C.1 Lemma.

i∈In Πn(i) = bn and i∈In Γn(i) =∼ bn ; in particular, Πn(i) ∩ Γn(j) = ∅ for any i, j ∈ In . Moreover Πn(i) ∩ Πn(j) = Γn(i) ∩ Γn(j) = ∅ for any i, j ∈ In such that i = j .

Proof. The proof is obvious for case 1. Now, let consider case 0. By definition i∈In Πn

(i) = ω∈µν (bν ) ω [n] ∩ ω ′ ∈∼µν (bν ) fn(ω ′ [n]
, ∼ bn) . By recursion hypothesis over β1 it comes fn(∼ bn, ∼ bn) = Ωn . Then by β2 , i∈In Πn(i) = bn ∩ fn(∼ bn, ∼ bn) = bn ∩ Ωn = bn .

For any ω1, ω2 ∈∼ µν(bν ) such that ω1 = ω2 , it comes by β6 (deduced from β2 and β4) :

fn(ω 1[n] , ∼ bn) ∩ fn(ω 2[n] , ∼ bn) = fn(ω 1[n] ∩ ω 2[n] , ∼ bn) = fn(∅, ∼ bn) = ∅ .
Finally Πn(i) ∩ Πn(j) = ∅ for any i, j ∈ In such that i = j .

The results are similarly proved for Γn . Both corollary are obvious from the definition.

C.2 Proof of • µ

The following properties (whose proofs are immediate) will be useful:

ℓ1. (A ∪ B) × C = (A × C) ∪ (B × C) and A × (B ∪ C) = (A × B) ∪ (A × C) , for any A, B, C , ℓ2. (A ∩ B) × C = (A × C) ∩ (B × C) and A × (B ∩ C) = (A × B) ∩ (A × C) , for any A, B, C , ℓ3. C ∩ D = ∅ implies (C × A) ∩ (D × B) = (A × C) ∩ (B × D) = ∅ , for any A, B, C, D , ℓ4. (A ∪ B) ∩ (C ∪ D) = ∅ implies (A ∩ B) ∪ (C ∩ D) = (A ∪ C) ∩ (B ∪ D) , for any A, B, C, D . ℓ5. (A ∪ B) ∩ (C ∪ D) = ∅ and A ∪ C = B ∪ D imply A = B and C = D , for any A, B, C, D . ℓ6. C ∩ D = ∅ implies (C ∪ D) \ (A ∩ C) ∪ (B ∩ D) = (C \ A) ∪ (D \ B) , for any A, B, C, D . Proof of µ n (Ω n ) = Ω n+1 and µ n (∅) = ∅ . Immediate from the definitions. Proof of µ n (A ∩ B) = µ n (A) ∩ µ n (B)
. By applying ℓ2, it is deduced:

µn(A ∩ B) = i∈In A ∩ Πn(i) × Γn(i) ∩ B ∩ Πn(i) × Γn(i) ∪ i∈In A ∩ Γn(i) × Πn(i) ∩ B ∩ Γn(i) × Πn(i) .
By lemma C.1, and applying ℓ3 and ℓ4, it is deduced:

µn(A ∩ B) = i∈In A ∩ Πn(i) × Γn(i) ∪ A ∩ Γn(i) × Πn(i) ∩ i∈In B ∩ Πn(i) × Γn(i) ∪ B ∩ Γn(i) × Πn(i) = µn(A) ∩ µn(B) . Proof of µ n (A ∪ B) = µ n (A) ∪ µ n (B) . Obviously deduced from ℓ1.
µ n is one-to-one. Assume µn(A) = µn(B) ; then:

i∈In A ∩ Πn(i) × Γn(i) ∪ A ∩ Γn(i) × Πn(i) = i∈In B ∩ Πn(i) × Γn(i) ∪ B ∩ Γn(i) × Πn(i) .
By lemma C.1, and applying ℓ2, ℓ3 and ℓ5, it is deduced for any i ∈ In :

A ∩ Πn(i) × Γn(i) = B ∩ Πn(i) × Γn(i) and A ∩ Γn(i) × Πn(i) = B ∩ Γn(i) × Πn(i) .
Finally A ∩ Πn(i) = B ∩ Πn(i) and A ∩ Γn(i) = B ∩ Γn(i) for any i ∈ In , and:

A ∩ i∈In Πn(i) ∪ Γn(i) = B ∩ i∈In Πn(i) ∪ Γn(i) .
A = B is deduced by applying the lemma.

Conclusion.

The previous results imply that µn is a one-to-one Boolean morphism. The true difficulties come from the cases A = bn or A =∼ bn . Subsequently, it is assumed A = bn ; the case A =∼ bn is quite similar.

It comes:

fn+1 µn(B), µn(bn) = (id∪T ) µn(B)∩ i∈In Πn(i)×Γn(i) = (id∪T ) i∈In B∩Πn(i) ×Γn(i) .
The existence of fn(B, bn) necessary implies the case 0 , and there is

C ∈ Mν+1 such that B = C [n] . By recursion hypotheses •µ, it comes B ∩ ω [n] = (C ∩ ω) [n] = ω [n] if ω ∈ C , = ∅ if ω ∈ C . Moreover, fn(ω [n] , bn) ∩ fn(B, bn) = fn(ω [n] ∩ B, bn) = fn(ω [n] , bn) if ω ∈ C , = ∅ if ω ∈ C . As a consequence i∈In B ∩ Πn(i) × Γn(i) = i∈In Πn(i) × fn(B, bn) ∩ Γn(i) . By β3, B ∩ ω [n] = B ∩ bn ∩ ω [n] = fn(B, bn) ∩ bn ∩ ω [n] = fn(B, bn) ∩ ω [n] for any ω ∈ µν (bν) .
As a consequence i∈In B ∩ Πn(i) × Γn(i) = i∈In fn(B, bn) ∩ Πn(i) × Γn(i) .

By applying the both results, it comes:

fn+1 µn(B), µn(bn) = i∈In fn(B, bn) ∩ Πn(i) × Γn(i) ∪ i∈In fn(B, bn) ∩ Γn(i) × Πn(i) .
And by definition of µn, it is finally deduced fn+1 µn(B), µn(bn) = µn fn(B, bn) .

C.4 Proof of β1

For A ∈ {µn(bn), ∼ µn(bn), ∅, Ωn+1}, the propriety is inherited from n by applying • f . The property is also obvious for A ∈ {∅, Ωn+1} . The difficulty comes from A = µn(bn) or A =∼ µn(bn) ; then notice that A = ∅ by construction.

It is now hypothesized A = µn(bn) ⊂ B ; the case A =∼ µn(bn) is quite similar.

Then T µn(bn) ⊂ T (B) and by lemma, corollary 1&2:

C.5 Proof of β2

For A ∈ {µn(bn), ∼ µn(bn), ∅, Ωn+1}, the propriety is inherited from n by applying • f . The property is also obvious for A ∈ {∅, Ωn+1} . The property is then immediate for A ∈ {µn(bn), ∼ µn(bn)} , since T (B1 ∪ B2) = T (B1) ∪ T (B2).

C.6 Proof of β3

For A ∈ {µn(bn), ∼ µn(bn), ∅, Ωn+1}, the propriety is inherited from n by applying • f . The property is also obvious for A ∈ {∅, Ωn+1} . The difficulty comes from A ∈ {µn(bn), ∼ µn(bn)}.

It is now hypothesized A = µn(bn) ; the case A =∼ µn(bn) is quite similar. The result is immediate from corollary 2 of lemma.

C.7 Proof of β4

For A ∈ {µn(bn), ∼ µn(bn), ∅, Ωn+1}, the propriety is inherited from n by applying • f . The property is also obvious for A ∈ {∅, Ωn+1} . The difficulty comes from A ∈ {µn(bn), ∼ µn(bn)} .

It is now hypothesized A = µn(bn) ; the case A =∼ µn(bn) is quite similar. From now on, let L b = φ ∈ L / φ is constructed without 2 or 3 .

In fact, it will be proved:

(HB)≡ is a Boolean isomorphism between (L b )≡ and M∞ ,

where (L b )≡ is the set of equivalence classes of L b and (HB)≡ is inferred from HB .

The proof is based on a recursive construction of L b similar to the definition of M∞ .

Construction. Assume the sequence (Ωn, Mn, hn, fn, Λn, µn)n∈IN being constructed.

The sequence (Ln)n∈IN is defined by: The following property is proved recursively in the next paragraphs:

• L0 = LC , • Ln+1
There is a generating partition Σn of Ln such that card(Σn) ≤ card(Ωn) . Proof of [START_REF] Giordano | Conditional Logic of Actions and Causation[END_REF] for n = 0. It is obvious, since (M0:∞, HB) is a complete model for LC .

True for n implies true for n + 1.

The recursion hypothesis implies that (HB)≡ is an isomorphism between (Ln)≡ and Mn:∞ . Define then βn ∈ (Ln)≡ such that (HB)≡(βn) = bn . Then, the two construction cases of (Ωn, Mn, hn, fn, Λn)n∈IN are considered: From previously, it is know that Σn+1 contains elements of the form σ ∧ (σ ′ |¬βn) or σ ′ ∧ (σ|βn) with (σ, σ ′ ) ∈ Bn × Bn ; but the construction at step ν + 1 implies additional constraints, to be specified.

E Probability extension

To be proved:

Let π be a probability defined over C , such that π(φ) > 0 for any φ ≡C ⊥. Then, there is a (multiplicative) probability π defined over DmBL * such that ∀φ ∈ LC , π(φ) = π(φ) .

The construction of π is a recursion based on the definition of (Ωn, Mn, hn, fn, Λn, µn)n∈IN .

E.1 Construction

The probabilities Pn|n∈IN are defined over Mn:∞ by: Pn(A∞) = ω∈A Pn ω∞ for any A ∈ Mn , and:

Initialization.

For ω = δ θ | θ∈Θ ∈ Ω0 and τ ∈ Θ, define τω = τ if δτ = 1 and τω = ¬τ if δτ = 0 .

Then set P0 ω∞ = π θ∈Θ θω for any ω ∈ Ω0 .

From n to n+1. For any (ω, ω ′ ) ∈ Πn(i) × Γn(i) , set:

Pn+1 (ω, ω ′ )∞ = Pn(ω∞)Pn(ω ′ ∞ ) Pn Γn(i)∞ and Pn+1 (ω ′ , ω)∞ = Pn(ω∞)Pn(ω ′ ∞ ) Pn Πn(i)∞ .
An example of construction is given in appendix F.

Notation. For m ≤ n and A ∈ Mm, the probability Pn(A∞) is denoted Pn(A) for simplicity.

Definition 2 .

 2 A conditional model for DmBL (respectively DmBL * ) is a quadruplet (W, M, h, f ) such that W is a set of worlds, M ⊂ P(W ) is a set of admissible propositions, h : Θ -→ M is an assignment function, f : M × M -→ M is a conditioning function, and verifying: • M is a Boolean sub-algebra of P(W ), i.e. A∩B ∈ M and W \A ∈ M for any A, B ∈ M , β1. A ⊂ B and A = ∅ imply f (B, A) = W , for any A, B ∈ M ,

Case 1 .

 1 for any (ω, ω ′ ) ∈ I n . † † Remark: case 0 means that the construction of f (•, b n ) and of f (•, ∼ b n ) has already begun over the propositions of M ν+1 . Case 0 does not hold; Define I n = {b n } , Π n (i) = i and Γ n (i) =∼ i for any i ∈ I n . Remark: case 1 means that f (•, b n ) and f (•, ∼ b n ) are constructed for the first time.

  -distortion. Let φ be a classical proposition. Assume that ⊢ 2φ ∨ 2¬φ in DmBL. Then ⊢ C φ or ⊢ C ¬φ. Proof. Consider the Kripke model for DmBL derived from the conditional model L K , ¬, ∧, (|) .

  a) and (b), it comes ⊢ 3(φ ∧ ψ) → 2 (ψ|ψ ∧ φ)) ↔ ⊤ , denoted (d). Now (ψ|φ) ≡ (ψ|φ) ∧ ψ ∨ (ψ|φ) ∧ ¬ψ ≡ (ψ|φ) ψ ∧ ψ ∨ (ψ|φ) ¬ψ ∧ ¬ψ , and by applying axiom ( * ), (ψ|φ)≡ (ψ|φ ∧ ψ) ∧ ψ ∨ (ψ|φ ∧ ¬ψ) ∧ ¬ψ . Then ⊢ 3(¬ψ ∧ φ) ∧ 3(φ ∧ ψ) → 2 (ψ|φ) ↔ (⊤ ∧ ψ) ∨ (⊥ ∧ ¬ψ) by (c) and (d). At last ⊢ 3(¬ψ ∧ φ) ∧ 3(φ ∧ ψ) → 2 (ψ|φ) ↔ ψ .B Proof: model transferFirst notice that the above construction of H is possible for any proposition φ ∈ L, since it is always obtainedH(φ) ∈ M . Now, R = W × W implies H(2φ) = t ∈ W ∀u ∈ W, (t, u) ∈ R ⇒ u ∈ H(φ), so that (W, R, H, f ) is actually a Kripke model. Let verify the compliance with m3, b1, b2, b3, b4 and b5 (resp. b5.weak. * ).

  e. compliance with b5.weak.B. Assume first H(ψ) = H(η) . It comes H(ψ ↔ η) = W and H 2(ψ ↔ η) = ∅ . Assume now H(ψ) = H(η) . Then H (φ|ψ) = H (φ|η) and H 2 (φ|ψ) ↔ (φ|η) = H (φ|ψ) ↔ (φ|η) = W .At last, both cases imply the result.

•

  f fn+1 µn(B), µn(A) = µn fn(B, A) ,β1. A ⊂ B and A = ∅ imply fn(B, A) = Ωn , β2. fn(B ∪ C, A) = fn(B, A) ∪ fn(C, A) , β3. A ∩ fn(B, A) = A ∩ B , β4. fn(∼ B, A) =∼ fn(B, A) , β5w. fn(B, A) = B implies fn(B, ∼ A) = B ,being assumed A, B, C ∈ Mn , and fn(•, •) defined for the considered cases.

222 Corollary 1 .

 1 µn(bn) = T (∼ µn(bn)) = i∈In Πn(i) × Γn(i) and ∼ µn(bn) = T (µn(bn)) = i∈In Γn(i) × Πn(i) .

Corollary 2 .

 2 fn+1 C, µn(bn) = C ∩ µn(bn) ∪ T (C)∩ ∼ µn(bn) and fn+1 C, ∼ µn(bn) = T (C) ∩ µn(bn) ∪ C∩ ∼ µn(bn) .

C. 3

 3 Proof of • f By definition, the result holds true for any A ∈ Mn \ {∅, Ωn, bn, ∼ bn} . It is also true for A = ∅ or A = Ωn , since fn+1 µn(B), µn(∅) = fn+1 µn(B), ∅ = µn(B) = µn fn(B, ∅) and similarly fn+1 µn(B), µn(Ωn) = fn+1 µn(B), Ωn+1 = µn(B) = µn fn(B, Ωn) .

  fn+1 B, µn(bn) = B ∩ µn(bn) ∪ T (B)∩ ∼ µn(bn) = µn(bn)∪ ∼ µn(bn) = Ωn+1 .

By corollary 2

 2 of lemma, fn+1 ∼ B, µn(bn) = µn(bn) \ B ∪ ∼ µn(bn) \ T (B) . By ℓ6, fn+1 ∼ B, µn(bn) =∼ B ∩ µn(bn) ∪ T (B)∩ ∼ µn(bn) =∼ fn+1 B, µn(bn) . C.8 Lemma 2. Let C ∈ Mn+1 . Then: fn+1 fn+1 C, µn(bn) , µn(bn) = fn+1 fn+1 C, µn(bn) , ∼ µn(bn) = fn+1 C, µn(bn) and fn+1 fn+1 C, ∼ µn(bn) , µn(bn) = fn+1 fn+1 C, ∼ µn(bn) , ∼ µn(bn) = fn+1 C, ∼ µn(bn) . Proof. The result is derived for fn+1 C, µn(bn) ; it is quite similar for fn+1 C, ∼ µn(bn) . By corollary 2 of lemma, fn+1 C, µn(bn) = C ∩ µn(bn) ∪ T (C)∩ ∼ µn(bn) . Since T fn+1 C, µn(bn) = fn+1 C, µn(bn) by definition, the proof is done by corollary 2. 222 Corollary. As a direct consequence, fn+1 fn+1(B, A), A = fn+1 fn+1(B, A), ∼ A = fn+1(B, A) , whenever fn+1(B, A) exists. C.9 Proof of β5w Assume fn+1(B, A) and fn+1(B, ∼ A) exist and fn+1(B, A) = B . By corollary of lemma 2, fn+1(B, ∼ A) = fn+1 fn+1(B, A), ∼ A = fn+1(B, A) = B .D Proof: completeness for the conditional operatorTo be proved:Let φ ∈ L be constructed without 2 or 3 . Then ⊢ φ in DmBL * if and only if HB(φ) = Ω∞ .

  ⊂ L b is the set generated by Ln, the classical operators, the conditionals (•|φ) and (•|¬φ) where φ ∈ Ln and HB(φ) = bn . A set Σn ⊂ (Ln)≡ is called a generating partition of Ln, if it verifies: ∀φ ∈ (Ln)≡ , ∃S ⊂ Σn , σ∈S σ = φ and σ ∧ σ ′ = ⊥ for any σ, σ ′ ∈ Σn such that σ = σ ′ .

( 20 )

 20 Since (HB)≡ is by construction an onto morphism from (Ln)≡ to Mn:∞ , (20) implies that (HB)≡ is a Boolean isomorphism between (Ln)≡ and Mn:∞ . The cyclic definition of Λn then implies L b = ∪n∈IN(Ln)≡ and (19) is deduced.

  It is known that (•|βn) ¬βn = (•|βn) and (•|¬βn) βn = (•|¬βn) .Then, since sub-universes are classical,Σn+1 = σ ∧ (σ ′ |βn) ∧ (σ ′′ |¬βn) / σ, σ ′ , σ ′′ ∈ Σn \ {⊥} . Now, denote Bn = σ ∈ Σn σ ∧ βn = σ and Bn = σ ∈ Σn σ ∧ ¬βn = σ . It comes that (σ ′ |βn) = (σ ′′ |¬βn) = ⊥ for σ ′ ∈ Bn and σ ′′ ∈ Bn . Moreover σ ∧ (σ ′ |βn) ∧ (σ ′′ |¬βn) = ⊥ for σ ∈ {σ ′ ,σ ′′ } ; on the other hand, σ ∧ (σ|βn) = σ for σ ∈ Bn , and σ ∧ (σ|¬βn) = σ for σ ∈ Bn .

Case 1 .

 1 Then, Σn+1 = σ∈Bn σ ′ ∈Bn σ ∧ (σ ′ |¬βn), σ ′ ∧ (σ|βn) , owing to above discussion. As a consequence, card(Σn+1) ≤ 2card(Bn)card(Bn) = 2card(bn)card(∼ bn) = card(Ωn+1) . Case 0. In this case, βn = βν . Define Cν = {σ ∈ Σν+1/σ ∧ βν = σ} and Cν = {σ ∈ Σν+1/σ ∧ ¬βν = σ} . Define also D[φ] = {σ ∈ Σn/σ ∧ φ = σ} for any φ ∈ (Lν+1)≡ .

  Let consider especially the case σ ∧ (σ ′ |¬βn); case σ ′ ∧ (σ|βn) is quite similar. Notice that there is (τ,τ ′ ) ∈ Cν × Cν such that σ ∈ D[τ ] ∩ D[(τ ′ |¬βν )] , and (θ, θ ′ ) ∈ Cν × Cν such that σ ′ ∈ D[θ] ∩ D[(θ ′ |βν )] . Now, τ ∧ (τ ′ |¬βν ) ∧ θ ∧ (θ ′ |βν ) ¬βν = τ ∧ (θ ′ |βν ) ∧ (τ ′ ∧ θ|¬βν ) = ⊥ unless τ = θ ′ and τ ′ = θ .As a consequence, it is deduced:σ ∧ (σ ′ |¬βn) = ⊥ implies ∃(τ, θ) ∈ Cν × Cν , (σ, σ ′ ) ∈ D[τ ] ∩ D[(θ|¬βν )] × D[θ] ∩ D[(τ |βν )] .Similarly, it is deduced:σ ′ ∧ (σ|βn) = ⊥ implies ∃(θ, τ ) ∈ Cν × Cν , (σ ′ , σ) ∈ D[θ] ∩ D[(τ |βν )] × D[τ ] ∩ D[(θ|¬βν )] . At last card(Σn+1) ≤ (τ,θ)∈Cν ×Cν 2 card D[τ ] ∩ D[(θ|¬βν )] card D[θ] ∩ D[(τ |βν )]= i∈In 2 card Πn(i) card Γn(i) = card(Ωn+1) .

  Proposition 1. By construction, (Ω ∞ , H B ) is a complete model for the classical logic C, when H B is restricted to the propositions of L C . Proposition 2. Let φ ∈ L be a proposition constructed without 2 or 3 . Then ⊢ φ in DmBL * if and only if H B

  e. compliance with b3.

	Immediate from β3, i.e. H(φ) ∩ f H(ψ), H(φ) ⊂ H(ψ) .
	Case DmBL.
	• Proof of H 2 (ψ|φ) ↔ ψ ↔ 2 (φ|ψ) ↔ φ	= W , i.e. compliance with b5.
	By β5, f H(ψ), H(φ) = H(ψ) if and only if f H(φ), H(ψ) = H(φ) .
	Case DmBL * .

Then H (ψ|φ) ↔ ψ = W if and only if H (φ|ψ) ↔ φ = W . As a consequence, H 2 (ψ|φ) ↔ ψ = H 2 (φ|ψ) ↔ φ

and the result.

• Proof of H 2 (ψ|φ) ↔ ψ ↔ 2 (ψ|¬φ) ↔ ψ = W , i.e.

compliance with b5.weak.A. By β5w, f H(ψ), H(φ) = H(ψ) if and only if f H

This property could also be related to the Boolean morphism (4) of CEA.

Notice that the definition of ⇒ is a meta-definition (or also a second-order definition) .

In first order logic, being able to prove B when hypothesizing A implies that A → B is proved (assumption discharge). On this second order example, the assumption discharge does not work anymore!

In regards to the mapping µ, the list Λ n+1 is the list Λn plus any propositions of M n+1 \ {∅, Ω n+1 } which are not/no more listed in Λn .

The operators ∨ and → are derived from ∧ and ¬ as usually; modalities are not considered.

A Proof: the logical theorems Axioms order.

From b5, it is deduced ψ × ¬φ ≡ ¬φ × ψ . Now ¬φ × ψ ≡ 2 (¬φ|ψ) ↔ ¬φ ≡ 2 ¬(φ|ψ) ↔ ¬φ ≡ 2 (φ|ψ) ↔ φ ≡ φ × ψ by b4. By applying b5 again, it comes ψ × ¬φ ≡ ψ × φ .

The empty universe.

It is deduced ⊢ 2¬φ → (ψ × ¬φ) and then ⊢ 2¬φ → (ψ × φ) by b5.weak.A.

The remaining proof is obvious.

Left equivalences.

Proof of the main theorem.

Since ψ and η are exchangeable, the theorem is deduced.

Proof of the corollary.

It has been proved

The corollary is then deduced from the main proposition.

Sub-universes are classical.

The first theorem is a consequence of axiom b4.

From axiom b2 , it is deduced

E.2 Properties.

E.2.1 Proposition 1

Pn ⊂ Pn+1 , i.e. Pn+1(A) = Pn(A) for any A ∈ Mn .

and then:

Derived from P0(Ω∞) = π(⊤) = 1 which is obvious.

Corollary of the corollary. Pn is indeed a probability in the classical meaning.

Additivity, coherence are obtained by construction. Finiteness comes from the corollary.

Pn Πn(i)

, for any A ∈ Mn+1 .

These propositions are proved recursively.

Proof of 1. Obvious in case 1; the difficulty arises for case 0.

Assume now case 0, and let (ω, ω ′ ) ∈ In , i.e. ω ∈ µν (bν) and ω ′ ∈∼ µν (bν ).

Then

Pn f ν+1 ω ′ ,∼µν (bν ) ∩ω

, by the recursion hypothesis over 2, and finally

Pn Πn(i)

= Pn fν+1 ω ′ , ∼ µν (bν) ∩ fν+1 ω, µν (bν) .

Similarly, it is derived

Pn Γn(i)

Then

Pn Πn(i)

Pn(∼bn) and the result is deduced from Pn(bn) + Pn(∼ bn) = 1.

Proof of 2. Since Pn+1 T (ω) = Pn+1(ω)

Pn Γn(i)

for ω ∈ i∈In Πn(i) × Γn(i) , it comes:

Pn(bn) =

Pn+1 µn(bn) ∩ A Pn(bn) .

Proof of 3. Similar to 2.

222

E.2.3 Conclusion.

Define P∞ = n∈IN Pn , that is ∀n ∈ IN, ∀A ∈ Mn:∞ , P∞(A) = Pn(A) . By inheritance from Pn, P∞ is a probability over M∞, which verifies the property: Then, ⊢ φ × ψ implies (ψ|φ) ≡ ψ and finally π(φ ∧ ψ) = π(φ)π(ψ) .

At last, π verifies the multiplicativity.

π is a (multiplicative) probability over DmBL * .

Rational structure of π . Let Σ = θ∈Θ ǫ θ ǫ ∈ θ∈Θ {θ, ¬θ} . For any φ ∈ L , there is a rational function R φ :

The proof is obvious from the construction.

F Conditional model: first steps of construction

In this paragraph, the objects Ω k , f k , Λ k , µ k-1 | k=0,1 , i.e. one iteration, are explicitly constructed, as well as the associated probability extensions P0, P1 (c.f. appendix E). It is assumed that Ω0 = {a, b, c} . This hypothesis cannot hold actually, but the case is sufficiently simple to be handled, and sufficiently complex to be illustrative. Only the case 1 of the construction is considered. Case 0 is intractable in a true example. For simplicity, µ k (A) and A are identified.