Xinghan Liu

Emiliano Lorini

A Logic of "Black Box" Classifier Systems

Binary classifiers are traditionally studied by propositional logic (PL). PL can only represent them as white boxes, under the assumption that the underlying Boolean function is fully known. Binary classifiers used in practical applications and trained by machine learning are however opaque. They are usually described as black boxes. In this paper, we provide a product modal logic called PLC (Product modal Logic for binary input Classifier) in which the notion of "black box" is interpreted as the uncertainty over a set of classifiers. We give results about axiomatics and complexity of satisfiability checking for our logic. Moreover, we present a dynamic extension in which the process of acquiring new information about the actual classifier can be represented.

Introduction

The notions of explanation and explainability have been extensively investigated by philosophers [START_REF] Hempel | Studies in the logic of explanation[END_REF][START_REF] Kment | Counterfactuals and explanation[END_REF] and are key aspects of AI-based systems given the importance of explaining the behavior and prediction of an artificial intelligent system. A variety of notions of explanation for classifier systems have been discussed in the area of explainable AI (XAI). Since systems trained by machine learning are increasingly opaque, instead of studying specific models, the model-agnostic approach comes into focus. Namely, given a black box system or algorithm, we know nothing about how it works inside. Without opening the black box, we can query some (but not all) inputs and have some partial information about the system. Initially there were global model-agnostic explanations like partial dependence plots and global surrogate models. Recently LIME [START_REF] Ribeiro | Why should i trust you?" Explaining the predictions of any classifier[END_REF] and its followers e.g. SHAP [START_REF] Lundberg | A unified approach to interpreting model predictions[END_REF] and Anchors [22] have raised a local model-agnostic explanation approach, namely explaining why a given input is classified in a certain way. For a comprehensive overview of the research in this area see, e.g., [START_REF] Molnar | Interpretable machine learning[END_REF].

At the mathematical level, a binary classifier can be viewed as a Boolean function and is traditionally studied by propositional logic. Recent years have witnessed several logic-based approaches to local explanation of classifier systems [23,[START_REF] Darwiche | On the reasons behind decisions[END_REF][START_REF] Ignatiev | Abduction-based explanations for machine learning models[END_REF][START_REF] Ignatiev | From contrastive to abductive explanations and back again[END_REF][START_REF] Audemard | On the computational intelligibility of boolean classifiers[END_REF], e.g., computing prime implicants and abductive explanations of a given classification, and detecting biases in the classification process by means of the notion counterfactual explanation. But, all these logic-based approaches deal with "white box" classifiers, i.e., specific transparent models representable by propositional formulas. A limitation is that given a Boolean function f and a propositional formula φ, φ either fully expresses f or does not express f at all. This all-or-nothing nature makes it impossible to give a partial description of f , which is a natural way to represent a black box classifier.

The central idea of this paper is that a product modal logic is the proper way to represent a "black box" classifier. As we have shown in [START_REF] Liu | A logic for binary classifiers and their explanation[END_REF], it is natural to think of a classifier with binary inputs as a partition of an S5 Kripke model, where each possible state stands for an input instance. However, this only represents "white box" classifiers. We extend this semantics with a second dimension universally ranging over a set of possible classifiers, which results in a proper extension of the product modal logic S5 × S5 = S5 2 [START_REF] Gabbay | Many-dimensional modal logics: theory and applications[END_REF] we call PLC (Product modal Logic of binary-input Classifiers). The notion of black box is interpreted as an agent's uncertainty among those (white box) classifiers, as illustrated in Figure 1. A classifier associating color labels in {red, yellow, green} to input instances. We do not know its Boolean formula, since f0, f1, f2, f3 are all compatible with our partial knowledge of it. However, we know that the two input instances s0 and s3 are both classified as green.

The paper is structured as follows. Section 2 introduces the modal language and semantic model of PLC which we name multi-classifier model (MCM). Its axiomatics along with the completeness and complexity results for the satisfiability checking problem are given in Section 3. In Section 4, we will exemplify the logic's application by using it to represent the notion of black box and to formalize different notions of classifier explanation. A dynamic extension is given in Section 6 to capture the process of acquisition of new knowledge about the classifier. Some non-routine proofs are given in a technical annex at the end of the paper.

Language and Semantics

Let Atm 0 = {p, q, . . .} be a countable set of atomic propositions which intend to denote input variables (features) of a classifier. We introduce a finite set Val to denote the possible output values (classifications, decisions) of the classifier.

Elements of Val are noted x, y, . . . For any x ∈ Val , we call t(x) a decision atom, and have Dec = {t(x) : x ∈ Val }. 3 Finally let Atm = Atm 0 ∪ Dec.

The modal language L is defined by the following grammar:

φ ::= p | t(x) | ¬φ | φ 1 ∧ φ 2 | □ I φ | □ F φ,
where p ranges over Atm 0 and x ranges over Val . Formulas in L are interpreted relative to a pointed MCM as follows.

Definition 2 (Satisfaction relation). Let Γ = (S, Φ) be an MCM, s ∈ S and f ∈ Φ. Then,

(Γ, s, f ) |= p ⇐⇒ p ∈ s, (Γ, s, f ) |= t(x) ⇐⇒ f (s) = x, (Γ, s, f ) |= ¬φ ⇐⇒ (Γ, s, f ) ̸ |= φ, (Γ, s, f ) |= φ ∧ ψ ⇐⇒ (Γ, s, f ) |= φ and (Γ, s, f ) |= ψ, (Γ, s, f ) |= □ I φ ⇐⇒ ∀s ′ ∈ S : (Γ, s ′ , f ) |= φ, (Γ, s, f ) |= □ F φ ⇐⇒ ∀f ′ ∈ Φ : (Γ, s, f ′ ) |= φ.
Both □ I φ and □ F φ have standard modal reading but range over different sets.

□ I φ has to be read "φ necessarily holds for the actual function, regardless of the input instance", while its dual ♢ I φ = def ¬□ I ¬φ has to be read "φ possibly holds for the actual function, regardless of the input instance". Similarly, □ F φ has to be read "φ necessarily holds for the actual input instance, regardless of the function" and its dual ♢ F φ has to be read "φ possibly holds for the actual input instance, regardless of the function". Let X be a finite subset of Atm 0 . An important abbreviation is the following:

[X]φ = def Y ⊆X ( p∈Y ∧ p∈X\Y ¬p) → □ I (( p∈Y ∧ p∈X\Y ¬p) → φ) .
Complex as it seems, [X]φ means nothing but "φ necessarily holds, regardless of the values of the input variables outside X" or "φ necessarily holds, if the values of the input variables in X are kept fixed". It can be justified by checking that

(Γ, s, f ) |= [X]φ, if and only if ∀s ′ ∈ S, if s ∩ X = s ′ ∩ X then (Γ, s ′ , f ) |= φ.
Its dual ⟨X⟩φ = def ¬[X]¬φ has to be read "φ possibly holds, if the values of the input variables in X are kept fixed" '. These modalities have a ceteris paribus reading and were first introduced in [START_REF] Grossi | The ceteris paribus structure of logics of game forms[END_REF]. Similar modalities are used in existing logics of functional dependence [25,[START_REF] Baltag | A simple logic of functional dependence[END_REF].

A formula φ of L is said to be satisfiable relative to the class MCM if there exists a pointed multi-classifier model (Γ, s, f ) with Γ ∈ MCM such that (Γ, s, f ) |= φ. We say that that φ is valid in the multi-classifier model Γ = (S, Φ), noted Γ |= φ, if (Γ, s, f ) |= φ for every s ∈ S, f ∈ Φ. It is said to be valid relative to MCM, noted |= MCM φ, if ¬φ is not satisfiable relative to MCM.

Axiomatics and Complexity

In this section, we are going to present two axiomatics for the language L by distinguishing the finite-variable from the infinite-variable case. We will moreover give complexity results for satisfiability checking. Before, we are going to introduce an alternative Kripke semantics for the interpretation of the language L. It will allow us to use the standard canonical model technique for proving completeness. Indeed, this technique cannot be directly applied to MCMs.

Alternative Kripke Semantics

The crucial concept of the alternative semantics is multi-decision model (MDM). Definition 3. An MDM is a tuple M = W, ∼ □I , ∼ □F , V where:

-W is a set of worlds, -∼ □I and ∼ □F are equivalence relations on W , -V : W -→ 2 Atm is a valuation function, and which satisfies the following constraints, ∀w, v ∈ W , ∀x, y ∈ Val :

(C1) ∼ □I • ∼ □F =∼ □F • ∼ □I , (C2) if V Atm0 (w) = V Atm0 (v) and w ∼ □I v then V Dec (w) = V Dec (v), (C3) if w ∼ □F v then V Atm0 (w) = V Atm0 (v), (C4) if t(x) ∈ V (w) and x ̸ = y then t(y) ̸ ∈ V (w), (C5) ∃x ∈ Val such that t(x) ∈ V (w),
with V Y (w) = V (w) ∩ Y for every w ∈ W and for every Y ⊆ Atm, and • the standard composition operator for binary relations.

The class of multi-decision models is noted MDM.

An MDM M = (W, ∼ □I , ∼ □F , V ) is called finite if W is finite. The class of finite MDMs is noted finite-MDM.
Interpretation of formulas in L relative to a pointed MDM goes as follows. (We omit interpretations for ¬ and ∧ which are defined as usual.) Definition 4 (Satisfaction Relation). Let M = W, ∼ □I , ∼ □F , V be an MDM and let w ∈ W . Then, (M, w) |= q ⇐⇒ q ∈ V (w) for q ∈ Atm,

(M, w) |= □ I φ ⇐⇒ ∀v ∈ W, if w ∼ □I v then v |= φ, (M, w) |= □ F φ ⇐⇒ ∀v ∈ W, if w ∼ □F v then v |= φ.
Validity and satisfiability of formulas in L relative to class MDM (resp. finite-MDM) are defined in the usual way.

The most important result in this subsection is the semantic equivalence between MCM and MDM, regardless of Atm 0 being finite or infinite. Although a pointed MDM (M, w) looks like a pointed MCM (Γ, s, f ), it only approximates it. Indeed, unlike an MCM, an MDM M may be redundant, that is, (i) a classifier in M (i.e., a ∼ □I -equivalence class) may include multiple copies of the same input instance (i.e., of the same valuation for the atoms in Atm 0 ), or (ii) M may contain multiple copies of the same classifier (i.e., two identical ∼ □F -equivalence classes). Moreover, an MDM M may be "defective" insofar as (iii) the intersection between a classifier in M (i.e., a ∼ □I -equivalence class) and the set of all possible classifications of a given input instance by the classifiers in M (i.e., a ∼ □Fequivalence class) is not a singleton. What makes the proof of the following theorem non-trivial is transforming a possibly redundant or defective MDM into a non-redundant and non-defective one by preserving truth of formulas. A nonredundant and non-defective MDM is then isomorphic to an MCM. Theorem 1. Let φ ∈ L. Then, φ is satisfiable relative to the class MCM if and only if it is satisfiable relative to the class MDM.

Finite-Variable Case

We first consider the variant of the logic with finitely many propositional atoms in Atm 0 . For every finite X, Y ⊆ Atm 0 we define:

cn X,Y = def p∈X p ∧ p∈(Y \X) ¬p.
Definition 5 (Logic PLC). Let Atm 0 be finite. We define PLC as the extension of classical propositional logic given by axioms and rules of inference in Table 1.

Axioms AtLeast t(x) , AtMost t(x) and Funct guarantee that every input Y ⊆ Atm 0 , whose syntactic counterpart is cn Y ,Atm0 , has only one decision atom as output. Axioms K ■ , T ■ , 4 ■ and 5 ■ together with the rule of inference Nec ■ indicate that both modal operators □ F and □ I satisfy the principles of the modal logic S5. According to Axiom Comm, they moreover commute. This makes the logic meet the requirement of a product of two S5 modal logics, i.e., S5 2 [START_REF] Gabbay | Many-dimensional modal logics: theory and applications[END_REF]. Nevertheless, the existence of the two "independence" Axioms Indep □F,p and Indep □F,¬p indicates that PLC is stronger than S5 2 in general.

Soundness of PLC relative to MCM is a simple exercise. To prove the completeness result, we first need to show that PLC is complete relative to MDM, which is proven by the canonical model construction.

Theorem 2. Let Atm 0 be finite. Then, the logic PLC is sound and complete relative to the class MDM.

Our main result of this subsection becomes a corollary of Theorems 1 and 2.

Corollary 1. Let Atm 0 be finite. Then, the logic PLC is sound and complete relative to the class MCM.

■φ ∧ ■(φ → ψ) → ■ψ (K ■ ) ■φ → φ (T ■ ) ■φ → ■■φ (4 ■ ) ¬■φ → ■¬■φ (5 ■ ) □F□Iφ ↔ □I□Fφ (Comm) x∈Val t(x) (AtLeast t(x) ) t(x) → ¬t(y) if x ̸ = y (AtMost t(x) ) cnX,Atm 0 ∧ t(x) → □I cnX,Atm 0 → t(x) (Funct) p → □Fp (Indep □F,p ) ¬p → □F¬p (Indep □F,¬p ) φ ■φ (Nec ■ )
Table 1. Axioms and rules of inference, with ■ ∈ {□I, □F}

Infinite-Variable Case

We now move to the infinite-variable variant of our logic, under the assumption that the set Atm 0 is countably infinite. In order to obtain an axiomatics we just need to drop the "functionality" Axiom Funct of Table 1. Indeed, when Atm 0 is infinite, the construction cn X,Atm0 cannot be expressed in a finitary way.

Definition 6 (Logic WPLC). We define WPLC (Weak PLC) to be the extension of classical propositional logic given by Axioms K ■ , T ■ , 4 ■ , 5 ■ , Comm, AtLeast t(x) , AtMost t(x) , Indep □F,p and Indep □F,¬p , and the rule of inference Nec ■ in Table 1.

Soundness of the logic WPLC is a straightforward exercise. For completeness, we need to distinguish MDMs from quasi-MDMs that are obtained by removing the "functionality" Constraint C2 from Definition 3.

Definition 7 (Quasi-MDM). A quasi-MDM is a tuple M = (W, ∼ □I , ∼ □F , V )
where W , ∼ □I , ∼ □F and V are defined as in Definition 3 and which satisfies all constraints of Definition 3 except C2.

The class of quasi-MDMs is noted

QMDM. A quasi-MDM M = (W, ∼ □I , ∼ □F , V ) is said to be finite if W is finite.
The class of finite quasi-MDMs is noted finite-QMDM. Semantic interpretation of formulas in L relative to quasi-MDMs is analogous to semantic interpretation relative to MDMs given in Definition 4. Moreover, validity and satisfiability of formulas in L relative to class QMDM (resp. finite-QMDM) is again defined in the usual way.

The first crucial result of this subsection is that when Atm 0 is infinite the language L cannot distinguish finite MDMs from finite quasi-MDMs. Theorem 3. Let φ ∈ L with Atm 0 infinite. Then, φ is satisfiable relative to the class finite-MDM if and only if it is satisfiable relative to the class finite-QMDM.

The second result is that satisfiability for formulas in L relative to the class QMDM is equivalent to satisfiability relative to the class finite-QMDM.

Theorem 4. Let φ ∈ L. Then, φ is satisfiable relative to the class QMDM if and only if it is satisfiable relative to the class finite-QMDM.

The following theorem is provable by standard canonical model argument. Note that like Theorems 1 and 4, it does not rely on Atm 0 being infinite or finite.

Theorem 5. The logic WPLC is sound and complete relative to the class QMDM.

The fact that the logic WPLC is sound and complete relative to the class MCM is a direct corollary of Theorems 1, 3, 4 and 5.

Corollary 2. Let Atm 0 be infinite. Then, the logic WPLC is sound and complete relative to the class MCM.

Complexity Results

We now move to complexity of satisfiability checking. As for the axiomatics, we distinguish the finite-variable from the infinite-variable case. When Atm 0 is finite, the problem of verifying whether a formula is satisfiable is polynomial. The latter problem mirrors the satisfiability checking problem for the finite-variable modal logic S5 which is also known to be polynomial [START_REF] Halpern | The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic[END_REF]. Theorem 6. Let Atm 0 be finite. Then, checking satisfiability of L-formulas relative to the class MCM can be done in polynomial time.

When moving from the finite-variable to the infinite-variable case complexity of satisfiability checking increases, but the problem remains in NP.

Theorem 7. Let Atm 0 be infinite. Then, checking satisfiability of L-formulas relative to the class MCM is NP-complete.

Application

As mentioned, the □ F operator is interpreted as partial knowledge about the classifier properties. In this section, we are going to exemplify how to use it for representing abductive explanations of a black box classifier.

An Example of Classification Task

Consider a selection function which specifies whether a paper submitted to a conference is acceptable for presentation [START_REF] Amershi | Power to the people: The role of humans in interactive machine learning[END_REF] or not (0) depending on its feature profile composed of four input features: significance (si), originality (or), clarity of the presentation (cl) and fulfillment of the anonymity requirement (an). For the sake of simplicity, we assume each feature in a paper profile is binary: si means the paper is significant while ¬si means the paper is not significant, or means the paper is original while ¬or means the paper is not original, and so on. We say that a first paper profile dominates a second paper profile, if all conditions satisfied by the second profile are satisfied by the first profile, and there exists a condition satisfied by the first profile which is not satisfied by the second profile. For example if the first profile is si ∧ ¬or ∧ cl ∧ an and the second profile is si ∧ ¬or ∧ ¬cl ∧ an, then the first dominates the second.

The selection function is implemented in a classifier system that has to automatically split papers into two sets, the set of acceptable papers and the set of non-acceptable ones. We assume a certain agent (e.g., the author of a paper submitted to the conference) has only partial knowledge of the classifier system. In particular, she only knows that the classifier complies with the following three constraints: [START_REF] Amershi | Power to the people: The role of humans in interactive machine learning[END_REF] submissions that satisfy the four conditions should be automatically accepted, (2) if a first paper profile dominates a second paper profile and the second paper profile is acceptable, then the first paper profile should also be acceptable, and (3) submissions that violate the anonymity requirement should be automatically rejected. In this case, the classifier is a black box for the agent.

Example 1. The multi-classifier model (MCM) representing the previous situation is the tuple Γ = (S, Φ) such that S = 2 {si,or,cl,an} and

∀f ∈ F S , f ∈ Φ iff (i) ∀s ∈ S, if {si, or, cl, an} ⊆ s then f (s) = 1, (ii) ∀s, s ′ ∈ S, if s ⊂ s ′ and f (s) = 1 then f (s ′ ) = 1. (iii) ∀s ∈ S, if an ̸ ∈ s then f (s) = 0.
The agent does not know which function in Φ corresponds to the actual classifier, i.e., they are epistemically indistinguishable for her.

Explanations

Given space constraints, we exemplify explanations for white and black box classifiers by showing the dichotomy global vs. local explanation and the notion of abductive explanation based on prime implicant. Some notations and abbreviations are needed to formally represent them. Let λ denote a conjunction of literals, where a literal is an atom p or its negation ¬p. We write λ ⊆ λ ′ , call λ a part (subset) of λ ′ , if all literals in λ also occur in λ ′ ; and λ ⊂ λ ′ if λ ⊆ λ ′ but not λ ′ ⊆ λ. In the glossary of Boolean classifiers, s is called an instance, λ is called a term or property (of the instance). The set of terms is noted Term. Moreover, let Atm(φ) denote the atoms occurring in φ. Finally, notice that the abbreviations [X]φ and ⟨X⟩φ introduced in Section 2 will be used.

Let us start with prime implicant, a key concept in the theory of Boolean functions since [START_REF] Quine | A way to simplify truth functions[END_REF]. It can be presented in the language L(Atm) as follows:

PImp(λ, x) = def □ I λ → t(x) ∧ p∈Atm(λ) ⟨Atm(λ) \ {p}⟩¬t(x) .
The abbreviation PImp(λ, x) has to be read "λ is a prime implicant for the classification x". Roughly speaking, the latter means that (i) λ necessarily leads to the classification x (why λ is an implicant), and (ii) for any of its proper subsets λ ′ , possibly there is a state where λ ′ holds but the classification is different from x (why λ is prime).

Prime implicant counts as a "global" explanation, in the sense that it is a property of the classifier and holds at all its input instances. Partially, as a response to the local approach in model-agnostic methods, researchers from logic-based approaches in XAI focus on the "localized" prime implicant namely abductive explanation (AXp). 4 An abductive explanation is not only a prime implicant, but also a property of the actual instance. The notion of abductive explanation is expressed in L as follows:

AXp(λ, x) = def λ ∧ PImp(λ, x).
AXp(λ, x) just means that λ is an abductive explanation of the actual classification x. Let us instantiate the notions of prime implicant and abductive explanation in the paper example we introduced in Section 4.1. Meanwhile (Γ, s 1 , f 1 ) ̸ |= AXp(cl∧an, 1), because (Γ, s 1 , f 1 ) ̸ |= cl∧an. But consider s 2 = {si, cl, an} ∈ S. We have (Γ, s 2 , f 1 ) |= AXp(cl ∧ an, 1).

Now we investigate what happens when facing a black box model Γ = (S, Φ).

The agent has uncertainty about the actual classifier's properties. Therefore, it is interesting to draw the distinction between objective and subjective (or epistemic) explanation. Objective explanation coincides with the notion of explanation in the context of white box classifiers defined above. Subjective explanation refers to the agent's interpretation of the classifier and her explanation of the classifier's decision in the light of her partial knowledge.

We say the term λ is a subjective prime implicant for x, noted SubPImp(λ, x), if the agent knows that λ is a prime implicant for x, that is:

SubPImp(λ, x) = def □ F PImp(λ, x).
Similarly, we say λ is a subjective abductive explanation of the actual classification x, noted SubAXp(λ, x), if the agent knows that λ is an abductive explanation of the actual classification x, that is:

SubAXp(λ, x) = def □ F AXp(λ, x).
It is worth noting that in the case of a white box classifier, if the set of input instances S is finite, we can always find an abductive explanation of the actual classification. That is, for every Γ = (S, Φ) ∈ MCM, s ∈ S and f ∈ Φ:

if S is finite then ∃λ ∈ Term such that (Γ, s, f ) |= AXp λ, f (s) .
Nonetheless, this result cannot be generalized to the black box case. Indeed, as the following example shows, there is no guarantee for the existence of a subjective explanation of the actual classification. The problem is that the minimality condition can collapse when moving from objective to subjective explanation, since the agent can have more than one classifier in her epistemic state.

Example 3. Let Γ = (S, Φ), f 1 and s 1 be the same as in Example 2. There is no λ such that (Γ, s 1 , f 1 ) |= □ F AXp(λ, 1). To see this, consider f 2 s.t. ∀s ∈ S : f 2 (s) = 1 iff {si, an} ⊆ s. The function f 2 is syntactically expressed by the formula □ I (t(1) ↔ (si ∧ an)). Clearly f 2 ∈ Φ for it satisfies the three constraints. We have (Γ, s 1 , f 2 ) |= AXp(si ∧ an, 1). But there is no term which minimally explains both f 1 (s 1 ) and f 2 (s 1 ). Indeed, or ∧ an is not enough for explaining f 2 (s 1 ), si ∧ an is not enough for explaining f 1 (s 1 ), and si ∧ or ∧ an fails the minimality condition for both. Therefore, we have (Γ, s 1 , f 1 ) |=AXp(or ∧ an, 1) ∧ λ∈Term({si,or,cl,an}) ¬SubAXp(λ, 1).

However, this does not mean that the agent knows nothing about the classifier. For instance, she knows that violating the anonymity requirement is a prime implicant for rejection, that is, (Γ, s 1 , f 1 ) |= SubAXp(¬an, 0).

To sum up, the four notions of explanation we introduced can be organized in Table 2 along the two dimensions objective vs subjective and local vs global.

Local

Global Objective AXp(λ, x) PImp(λ, x) Subjective SubAXp(λ, x) SubPImp(λ, x) Table 2. Notions of prime implicant and abductive explanation

Dynamic Extension

Before concluding, we are going to present a simple dynamic extension of the language L by operators of the form [φ]. They describe the consequences of removing from the actual model all classifiers that do not globally satisfy the constraint φ. More generally, they allow us to model the process of gaining new knowledge about the classifier's properties. The extended modal language L dyn is defined by the following grammar:

φ ::= p | t(x) | ¬φ | φ 1 ∧ φ 2 | □ I φ | □ F φ | [φ]ψ,
where p ranges over Atm 0 and x ranges over Val .

The new formula [φ]ψ has to be read "ψ holds after having discarded all classifiers that do not globally satisfy the property φ". Notice the similar but different notations [X] and [φ]. For example, [{p}], [{p, q}] are abbreviations with ceteris paribus meaning, while [p], [p ∧ ¬q] are dynamic operators.

The interpretation of the operators [φ] relative to a pointed MCM (Γ, s, f ) with Γ = (S, Φ), s ∈ S and f ∈ Φ goes as follows:

(Γ, s, f ) |= [φ]ψ ⇐⇒ if (Γ, s, f ) |= □ I φ then (Γ φ , s, f ) |= ψ,
where Γ φ = (S φ , Φ φ ) is the MCM such that:

S φ = S, Φ φ = {f ′ ∈ Φ : ∀s ′ ∈ S, (Γ, s ′ , f ′ ) |= φ}.
The previous update semantics for the operator [φ] is reminiscent of the semantics of public announcement logic (PAL) [START_REF] Plaza | Logics of public communications[END_REF][START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF]. However, there is an important difference. While PAL has a one-dimensional state elimination semantics, our update semantics operates on a single dimension of the product in an MCM. In particular, it only removes classifiers that do not globally satisfy the constraint φ, without modifying the set S of input instances.

The logics D-PLC and D-WPLC (Dynamic PLC and D-WPLC) extend the logic PLC and WPLC by the dynamic operators [φ]. They are defined as follows.

Definition 8 (Logics D-PLC and D-WPLC). We define D-PLC (resp. D-WPLC) to be the extension of PLC (resp. WPLC) of Definition 5 (resp. Definition 6) generated by the following reduction axioms for the dynamic operators [φ]:

[φ]p ↔(□ I φ → p) [φ]t(x) ↔ □ I φ → t(x) [φ]¬ψ ↔(□ I φ → ¬[φ]ψ) [φ](ψ 1 ∧ ψ 2 ) ↔ [φ]ψ 1 ∧ [φ]ψ 2 [φ]□ I ψ ↔(□ I φ → □ I [φ]ψ) [φ]□ F ψ ↔(□ I φ → □ F [φ]ψ)
and the following rule of inference:

φ 1 ↔ φ 2 ψ ↔ ψ[φ 1 /φ 2 ] (RE)
It is a routine exercise to verify that the equivalences in Definition 8 are valid for the class MCM and that the rule of replacement of equivalents (RE) preserves validity. The completeness of D-PLC and D-WPLC for this class of models follows from Theorem 2 and Corollary 1, in view of the fact that the reduction axioms and the rule of replacement of proved equivalents can be used to find, for any L dyn -formula, a provably equivalent L-formula. Theorem 8. Let Atm 0 be finite. Then, the logic D-PLC is sound and complete relative to the class MCM.

Theorem 9. Let Atm 0 be infinite. Then, the logic D-WPLC is sound and complete relative to the class MCM.

The following decidability result is a consequence of Theorem 7 and the fact that via the reduction axioms in Definition 8 we can find a reduction of satisfiability checking of L dyn -formulas to satisfiability checking of L-formulas.

Theorem 10. Checking satisfiability of L dyn -formulas relative to MCM is decidable.

Let us end up with the paper example to illustrate to expressive power of our dynamic extension.

Example 4. Let Γ = (S, Φ), f 1 and s 1 be the same as in Example 2. We have

(Γ, s 1 , f 1 ) |= [(or ∧ an) → t(1)]□ F λ⊆(or∧an) AXp(λ, 1).
This means that after having discarded all classifiers which do not take (or ∧ an) as an implicant for acceptance of a paper, the agent knows that there must be a part of or ∧ an that abductively explains the acceptance of the paper s 1 .

Conclusion

We have presented a product modal logic which supports reasoning about (i) partial knowledge and uncertainty of a classifier's properties and, (ii) objective and subjective explanations of a classifier's decision. Moreover, we have studied a dynamic extension of the logic which allows us to represent the event of gaining new knowledge about the classifier's properties.

Our logic is intrinsically single-agent: it models the uncertainty of one agent about the actual classifier's properties. In future work, we plan to generalize our framework to the multi-agent setting. The extension would result in a multirelational product semantics in which every agent has her own epistemic indistinguishability relation which commutes with the input instance dimension (the equivalence relation ∼ □I in Definition 3 of MDM). We also plan to enrich this semantics with a knowledge update mechanism in the spirit of Section 5. This would allow us to represent exchange of information between agents with an explanatory purpose, which is named dialogical explanation by philosophers [24] and interactive explanation by researchers in the XAI domain [START_REF] Amershi | Power to the people: The role of humans in interactive machine learning[END_REF][START_REF] Miller | Explanation in artificial intelligence: insights from the social sciences[END_REF]. Proof. We start with the left-to-right direction of the proof. Let (Γ, s 0 , f 0 ) be a pointed MCM with Γ = (S, Φ), S ⊆ 2 Atm0 and Φ ⊆ F S such that (Γ, s 0 , f 0 ) |= φ.

We define the tuple M = W, ∼ □I , ∼ □F , V as follows:

-

W = {(s, f ) : s ∈ S and f ∈ Φ}, -∀(s, f ), (s ′ , f ′ ) ∈ W , (s, f ) ∼ □I (s ′ , f ′ ) iff f = f ′ -∀(s, f ), (s ′ , f ′ ) ∈ W , (s, f ) ∼ □F (s ′ , f ′ ) iff s = s ′ , -∀(s, f ) ∈ W , V (s, f ) = s ∪ {t(f (s))}.
It is routine exercise to verify that M so defined is an MDM. Moreover, by induction on the structure of φ, it is easy to prove that "(Γ, s, f ) |= φ iff M, (s, f ) |= φ" for every s ∈ S and f ∈ Φ. Thus, M, (s 0 , f 0 ) |= φ since (Γ, s 0 , f 0 ) |= φ.

Let us now prove the right-to-left direction. Let M = (W, ∼ □I , ∼ □F , V ) be an MDM and w 0 ∈ W such that (M, w 0 ) |= φ. Given v ∈ W , let |v| = {u ∈ W : v ∼ □I u and V (v) = V (u)}. We transform the MDM M into a tuple

M ′ = W ′ , ∼ ′ □I , ∼ ′ □F , V ′ such that: -W ′ = {|v| : v ∈ W }, -∀|v|, |u| ∈ W ′ , |v| ∼ □I |u| iff ∃v ′ ∈ |v|, u ′ ∈ |u| such that v ′ ∼ □I u ′ , -∀|v|, |u| ∈ W ′ , |v| ∼ ′ □F |u| iff ∃v ′ ∈ |v|, u ′ ∈ |u| such that v ′ ∼ □F u ′ , -∀|v| ∈ W ′ , V ′ (|v|) = V (v). Like what we did for V , let V ′ Y (|v|) = V ′ (|v|) ∩ Y for all Y ⊆ Atm.
It is a routine exercise to verify that M ′ is an MDM and, by induction on the structure of φ, that "(M, v) |= φ iff (M ′ , |v|) |= φ" for every v ∈ W . Thus, (M, |w 0 |) |= φ since (M, w 0 ) |= φ. Finally, because of Constraints C2 and C3 in Definition 3, the following property holds:

(C6) ∼ ′ □I ∩ ∼ ′ □F = id W ′ ,
where id W ′ is the identity relation on W ′ . Let W ′ / ∼ ′ □I be the quotient set of W ′ by the equivalence relation ∼ ′ □I . We note τ, τ ′ , . . . its elements. Given τ, τ

′ ∈ W ′ / ∼ ′ □I , we write τ ≈ F τ ′ if and only if, ∀|v| ∈ τ, ∀|u| ∈ τ ′ , if V ′ Atm0 (|v|) = V ′ Atm0 (|u|) then V ′ Dec (|v|) = V ′ Dec (|u|). Given |v|, |u| ∈ W ′ , we write |v| ≃ |u| if and only if ∃τ, τ ′ ∈ W ′ / ∼ ′ □I such that |v| ∈ τ, |u| ∈ τ ′ , τ ≈ F τ ′ and V ′ Atm0 (|v|) = V ′ Atm0 (|u|).
Clearly, ≈ F and ≃ are equivalence relations.

We are going to transform the MDM M ′ into an MDM which does not contain multiple copies of the same function and which satisfies the same formulas as M ′ . We define it to be a tuple

M ′′ = W ′′ , ∼ ′′ □I , ∼ ′′ □F , V ′′ such that: -W ′′ = {≃(|v|) : |v| ∈ W ′ }, -∀ ≃(|v|), ≃(|u|) ∈ W ′′ , ≃(|v|) ∼ ′′ □I ≃(|u|) iff ∃|v ′ | ∈≃(|v|), |u ′ | ∈≃(|u|) such that |v ′ | ∼ ′ □I |u ′ |, -∀ ≃(|v|), ≃(|u|) ∈ W ′′ , ≃(|v|) ∼ ′′ □F ≃(|u|) iff ∃|v ′ | ∈≃(|v|), |u ′ | ∈≃(|u|) such that |v ′ | ∼ ′ □F |u ′ |, -∀ ≃(|v|) ∈ W ′′ , V ′′ ≃(|v|) = V ′ (|v|).
Again, it is routine to verify that M ′′ is an MDM which satisfies the previous Constraint C6. Moreover, by induction on the structure of φ, it is easy to prove that "

(M ′ , |v|) |= φ iff M ′′ , ≃ (|v|) |= φ" for every |v| ∈ W ′ . Thus, M ′′ , ≃ (|w 0 |) |= φ since (M ′ , |w 0 |) |= φ.
We can easily build an MCM isomorphic to M ′′ .

A.2 Proof of Theorem 3

Proof. The left-to-right direction is trivial. We prove the right-to-left direction. Suppose Atm 0 is infinite. Moreover, let M = (W, ∼ □I , ∼ □F , V ) be a finite quasi-MDM and w 0 ∈ W such that (M, w 0 ) |= φ. Since Atm 0 is infinite and W is finite, we can define an injection g : W -→ Atm 0 \ Atm(φ). We define the tuple

M ′ = W ′ , ∼ ′ □I , ∼ ′ □F , V ′ as follows: -W ′ = W ; -∼ ′ □I =∼ □I -∼ ′ □F =∼ □F ; -for every w ∈ W ′ , V ′ (w) = V (w) \ {g(v) : v ∈ W and w ̸ = v} ∪ {g(w)}. It is routine to verify that M ′ is a finite MDM. Indeed, V ′ Atm0 (w) ̸ = V ′ Atm0 (v) for all w, v ∈ W ′ such that w ̸ = v.
This guarantees that M ′ satisfies the "functionality" constraint C2. Moreover, by induction on the structure of φ, it is straightforward to prove that "(M, v) |= φ iff (M ′ , v) |= φ" for every v ∈ W . The crucial point of the proof is that ∼ ′ □I =∼ □I and ∼ ′ □F =∼ □F . Thus, (M ′ , w 0 ) |= φ since (M, w 0 ) |= φ.

A.3 Proof of Theorem 4

Proof. The right-to-left direction is clear. We are going to prove the left-to-right direction by a filtration argument.

Let M = (W, ∼ □I , ∼ □F , V ) be a quasi-MDM and w 0 ∈ W such that (M, w 0 ) |= φ. It is routine to verify that (∼ □I ∪ ∼ □F ) * =∼ □I • ∼ □F =∼ □F • ∼ □I . Thus, we can define M ′ = (W ′ , ∼ ′ □I , ∼ ′ □F , V ′ ) to be the submodel of M generated from w 0 through the relation ∼ □I • ∼ □F . M ′ is a quasi-MDM and (M ′ , w 0 ) |= φ.

Let sf (φ) be the set of all subformulas of φ and let sf + (φ) = sf (φ) ∪ Dec. Moreover, for every v ∈ W ′ , let Θ(v) = ψ ∈ sf + (φ) : (M ′ , v) |= ψ . For every v, u ∈ W ′ , we define v ≃ u iff Θ(v) = Θ(u).

Moreover, we define

[v] = {u ∈ W ′ : v ≃ u}.
We construct a new model M ′′ = (W ′′ , ∼ ′′ □I , ∼ ′′ □F , V ′′ ) where: -

W ′′ = {[v] : v ∈ W ′ }; -[v] ∼ ′′ □I [u] iff ∀□ I ψ ∈ sf (φ), (M ′ , v) |= □ I ψ iff (M ′ , u) |= □ I ψ ; -[v] ∼ ′′ □F [u] iff ∀□ F ψ ∈ sf (φ), (M ′ , v) |= □ F ψ iff (M ′ , u) |= □ F ψ and ∀p ∈ sf (φ) ∩ Atm 0 , (M ′ , v) |= p iff (M ′ , u) |= p ; -V ′′ [v] = V ′ sf (φ)∩Atm0 (v) ∪ V ′ Dec (v). M ′′ is indeed a filtration, for it satisfies that if v ∼ ■ u, then [v] ∼ ■ [u];
and if ■ψ ∈ sf (φ) and (M ′ , v) |= ■ψ, then (M ′ , u) |= ψ, for ■ ∈ {□ I , □ F }. Additionally, the valuation function is defined in standard way.

To check that M ′′ is a finite quasi-MDM, we go through all constraints. For C1 a crucial fact is that M ′ generated from w 0 through ∼ □I • ∼ □F , viz. It is routine to verify that M ′′ = (W ′′ , ∼ ′′ □I , ∼ ′′ □F , V ′′ ) is a filtration of M ′ and is a finite quasi-MDM. Therefore, (M ′′ , [w 0 ]) |= φ.

A.4 Proof of Theorem 6

Proof. Suppose |Atm 0 | is finite. Then, the class MCM is bounded by some integer k. So, in order to determine whether a formula φ is satisfiable for the class MCM, it is sufficient to verify whether φ is satisfied in one of these MCMs. This verification takes a polynomial time in the size of φ since it is a repeated model checking and model checking in the product modal logic S5 2 is polynomial.

  Fig.1. A classifier associating color labels in {red, yellow, green} to input instances. We do not know its Boolean formula, since f0, f1, f2, f3 are all compatible with our partial knowledge of it. However, we know that the two input instances s0 and s3 are both classified as green.

Definition 1 .

 1 A multi-classifier model (MCM) is a pair Γ = (S, Φ) where S ⊆ 2 Atm0 and Φ ⊆ F S , with F S = Val S the set of functions with domain S and codomain Val . A pointed MCM is a triple (Γ, s, f ) where Γ = (S, Φ) is an MCM, s ∈ S and f ∈ Φ. The class of all multi-classifier models is noted MCM.

Example 2 .

 2 Take the MCM Γ = (S, Φ) in Example 1, and let s 1 = {si, or, an} ∈ S. Consider the function f 1 s.t. ∀s ∈ S : f 1 (s) = 1 iff an ∈ s and {or, cl} ∩ s ̸ = ∅. The function f 1 is syntactically expressed by the formula □ I t(1) ↔ ((or ∧ an) ∨ (cl ∧ an)) . Clearly f 1 ∈ Φ for it satisfies the three constraints. Hence, we have: (Γ, s 1 , f 1 ) |=AXp(or ∧ an, 1) ∧ PImp(or ∧ an, 1) ∧ PImp(cl ∧ an, 1).

  22. Ribeiro, M.T., Singh, S., Guestrin, C.: Anchors: High-precision model-agnostic explanations. In: Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence (AAAI-18). vol. 32 (2018) 23. Shih, A., Choi, A., Darwiche, A.: Formal verification of bayesian network classifiers. In: International Conference on Probabilistic Graphical Models. pp. 427-438. PMLR (2018) 24. Walton, D.: A new dialectical theory of explanation. Philosophical Explorations 7(1), 71-89 (2004) 25. Yang, F., Väänänen, J.: Propositional logics of dependence. Annals of Pure and Applied Logic 167(7), 557-589 (2016) A Technical Annex A.1 Proof of Theorem 1

  ∀v, u ∈ W ′ , v ∼ ′ □I • ∼ ′ □F u and v ∼ ′ □F • ∼ ′ □I u. To see that fact, by construction of M ′ we have w 0 ∼ ′ □I • ∼ ′ □F u and w 0 ∼ ′ □I • ∼ ′ □F v. This means w 0 ∼ ′ □I v 1 ∼ ′ □F v and w 0 ∼ ′ □I u 1 ∼ ′ □F u for some u 1 , v 1 ∈ W ′ ⊆ W . Then we have v 1 ∼ ′ □I • ∼ ′ □F u by the Euclidean of ∼ ′ □I . Then, since v 1 , u ∈ W and by C1 of M , we have v 1 ∼ □F v 2 ∼ □I u for some v 2 ∈ W . Since w 0 ∼ □I v 1 ∼ □F v 2 , we are sure that v 2 ∈ W ′ , which gives us v 1 ∼ ′ □F v 2 ∼ ′ □I u. So now we have v ∼ ′ □F v 1 ∼ ′ □F v 2 ∼ ′ □I u, and by Euclidean of ∼ ′ □F , we have v ∼ ′ □F • ∼ ′ □I u. The case of u ∼ ′ □I • ∼ ′ □F vis proven in the same way. C3 holds because of the definition of ∼ ′′ □F . C4, C5 hold, since V ′′ not only considers sf (φ) ∩ Atm 0 but also Dec.

Notice x is an output value rather than the output variable, which makes sense of the symbolic difference between p and t(x).

It has many names in literature: PI explanation [23], sufficient reason[START_REF] Darwiche | On the reasons behind decisions[END_REF]. We adopt the one from[START_REF] Ignatiev | Abduction-based explanations for machine learning models[END_REF] for its nice correspondence to contrastive explanation in[START_REF] Ignatiev | From contrastive to abductive explanations and back again[END_REF].

A.5 Proof of Theorem 7

Proof. The satisfiability problem of formulas in L relative to the class MCM is clearly NP-hard since there exists a polynomial-time reduction of SAT to it. As for membership, WPLC is a proper normal extension of the product modal logic S5 2 . It is proved in [START_REF] Bezhanishvili | All normal extensions of s5-squared are finitely axiomatizable[END_REF] (see also [START_REF] Bezhanishvili | All proper normal extensions of S5-square have the polynomial size model property[END_REF]) that all proper normal extensions of the product modal S5 2 are in NP. WPLC is moreover sound and complete relative to the class MCM (Corollary 2) which implies that checking whether a formula is consistent in the logic amounts to checking whether the formula is satisfiable relative to the class MCM. So, we can conclude that satisfiability checking of L-formulas in class MCM is in NP.

A.6 Proof of the validity of the sixth equivalence in Definition 8