Xinghan Liu
email: xinghan.liu@univ-toulouse.fr

Emiliano Lorini
email: emiliano.lorini@irit.fr

A Unified Logical Framework for Explanations in Classifier Systems

Recent years have witnessed a renewed interest in the explanation of classifier systems in the field of explainable AI (XAI). The standard approach is based on propositional logic. We present a modal language which supports reasoning about binary input classifiers and their properties. We study a family of classifier models, axiomatize it as two proof systems regarding the cardinality of the language and show completeness of our axiomatics. Moreover, we show that the satisfiability checking problem for our modal language is NEXPTIME-complete in the infinite-variable case, while it becomes polynomial in the finite-variable case. We moreover identify an interesting NP fragment of our language in the infinite-variable case. We leverage the language to formalize counterfactual conditional as well as a variety of notions of explanation including abductive, contrastive and counterfactual explanations, and biases. Finally, we present two extensions of our language: a dynamic extension by the notion of assignment enabling classifier change and an epistemic extension in which the classifier's uncertainty about the actual input 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][START_REF] Woodward | Explanation and invariance in the special sciences[END_REF] and are key aspects of AI-based systems given the importance of explaining the behavior and prediction of an artificial intelligent system. Classifier systems compute a given function in the context of a classification or prediction task. Artificial feedforward neural networks are special kinds of classifier systems aimed at learning or, at least approximating, the function mapping instances of the input data to their corresponding outputs. Explaining why a system has classified a given instance in a certain way is crucial for making the system intelligible and for finding biases in the classification process. This is the main target of explainable AI (XAI). Thus, a variety of notions have been defined and used to explain classifiers including abductive, contrastive and counterfactual explanations [START_REF] Biran | Explanation and justification in machine learning: A survey[END_REF][START_REF] Wachter | Counterfactual explanations without opening the black box: Automated decisions and the gdpr[END_REF][START_REF] Dhurandhar | Explanations based on the missing: Towards contrastive explanations with pertinent negatives[END_REF][START_REF] Ignatiev | Abductionbased explanations for machine learning models[END_REF][START_REF] Mittelstadt | Explaining explanations in AI[END_REF][START_REF] Miller | Explanation in artificial intelligence: Insights from the social sciences[END_REF][START_REF] Ramaravind | Explaining machine learning classifiers through diverse counterfactual explanations[END_REF][START_REF] Verma | Counterfactual explanations for machine learning: A review[END_REF][START_REF] Miller | Contrastive explanation: A structural-model approach[END_REF][START_REF] Mertes | Alterfactual explanations-the relevance of irrelevance for explaining ai systems[END_REF]. 1 Inputs of a classifier are called instances, i.e., valuations of all its variables/features/factors, and outputs are called classifications/predictions/decisions. 1When both input and output of the classifier are binary, it is just a Boolean function f : {0, 1} n -→ {0, 1}, and furthermore can be expressed by a propositional formula. This isomorphism between Boolean functions and logic has been known ever since the seminal work of Boole. Recently there has been a renewed interest in Boolean functions in the area of logic-based approaches to XAI [START_REF] Shih | Formal verification of bayesian network classifiers[END_REF][START_REF] Ignatiev | Abductionbased explanations for machine learning models[END_REF][START_REF] Darwiche | On the reasons behind decisions[END_REF][START_REF] Ignatiev | From contrastive to abductive explanations and back again[END_REF][START_REF] Shi | On tractable representations of binary neural networks[END_REF][START_REF] Audemard | On the computational intelligibility of boolean classifiers[END_REF][START_REF] Amgoud | Axiomatic foundations of explainability[END_REF]. They concentrate on local explanations, i.e., on explaining why an actual instance is classified in a certain way.

We argue that it is natural and fruitful to represent binary (input) classifiers and their explanations with the help of a modal language. To that end let us first explain the conceptual foundation of explanation in the context of classifiers, which is largely ignored in the recent literature.

What is an explanation? Despite subtle philosophical debates,2 by explanation people usually mean causal explanation, an answer to a "why" question in terms of "because". Then what is a causal explanation? Ever since the seminal deductive-nomological (D-N) model [START_REF] Hempel | Studies in the logic of explanation[END_REF], one can view it as a logical relation between an explanandum (the proposition being explained) and an explanans (the proposition explaining), which is itself expressible by a logical formula. According to the D-N model, a causal explanation of a certain fact should include a reference to the laws that are used for deducing it from a set of premises.

More recently Woodward & Hitchcock [52, p. 2, p. 17] (see also [START_REF] Woodward | Making Things Happen: a Theory of Causal Explanation[END_REF]Ch. 5 and 6]) proposed that causal explanations make reference to generalizations, or descriptions of dependency relations, which specify relationships between the explanans and explanandum variables. No need of being laws, such generalizations exhibit how the explanandum variable is counterfactually dependent on the explanans variables by relating changes in the value of the latter to changes in the value of the former. 3 According to Woodward & Hitchcock, a generalization used in a causal explanation is invariant under intervention insofar as it remains stable after changing the actual value of the variables cited in the explanation. 4We claim that existing notions of explanation leveraged in the XAI domain rest upon the idea of invariance under intervention. However, while Woodward & Hitchcock apply it to the notion of generalization, in the XAI domain it usually concerns the result of the classifier's decision to be explained. Another minor difference with Woodward & Hitchcock is terminological: when explaining the decision of a binary classifier system, the term 'perturbation' is commonly used instead of 'intervention'. But they both mean switching some features' values from the current ones to other ones. Let us outline it by introducing informally our running example.

Example 1 (Applicant Alice, informal). Alice applies for a loan. She is not male, she is employed, and she rents an apartment in the city center, which we note ¬male ∧ employed ∧ ¬owner ∧ center. The classifier f only accepts the application if the applicant is employed, and either is a male or owns a property. Hence, Alice's application is rejected.

In the XAI literature ¬male ∧ ¬owner is called an abductive explanation (AXp) [START_REF] Ignatiev | Abductionbased explanations for machine learning models[END_REF] or sufficient reason [START_REF] Darwiche | On the reasons behind decisions[END_REF] of the actual decision of rejecting Alice's application, because perturbing the values of the other features ('employment' and 'address' in this setting), while keeping the values of 'gender' or 'ownership' fixed, will not change the decision. More generally, for a term (a conjunction of literals) to be an abductive explanation of the classifier's actual decision, the classifier's decision should be invariant under perturbation on the variables not appearing in the term. 5On the contrary, ¬male is called a contrastive explanation (CXp) [START_REF] Ignatiev | From contrastive to abductive explanations and back again[END_REF], 6 because perturbing nothing but 'gender' will change the decision from rejecting the application to accepting it. Therefore, the "duality" between two notions rests on the fact that AXp answers a why-question by indicating that the classification would stay unchanged under intervention on variables other than 'gender' and 'ownership', whereas CXp answers a why not-question by indicating that the classification would change under intervention on 'gender'. More generally, for a term (a conjunction of literals) to be a contrastive explanation of the classifier's actual decision, the classifier's decision should be variant under perturbation on all variables appearing in the term, where 'variant' is assumed to be synonym of 'non-invariant'.

As Woodward [50,p. 225,footnote 5] clarifies:

[I]nvariance is a modal notion -it has to do with whether a relationship would remain stable under various hypothetical changes.

Therefore, following Woodward, the most natural way of modeling invariance is by means of a modal language whereby the notions of necessity and possibility can be represented. This is the approach we take in this work.

In particular, in order to model explanations in classifier systems, we use a modal language with a ceteris paribus (other things being equal) flavor. Indeed, the notion of invariance under intervention we consider presupposes that one intervenes on specific input features of the classifier, while keeping the values of the other input features unchanged (i.e., the values of the other input features being equal). So, for Alice's example we expect two modal formulas saying: a) 'gender' and 'ownership' keeping their actual values, changing other features' values necessarily does not affect the actual decision of rejecting Alice's application;

b) other features keeping their actual values, changing the value of 'gender' necessarily modifies the classifier's decision of rejecting Alice's application.

Specifically, we will extend the ceteris paribus modal logic introduced in [START_REF] Grossi | The ceteris paribus structure of logics of game forms[END_REF] by a finite set of atoms representing possible decisions/classifications of a classifier and axioms regarding them. The resulting logic is called BCL which stands for Binary input Classifier Logic, since the input variables of a classifier are assumed to be binary. One may roughly thinks of its models as S5 models supplemented with a classification function which allows us to fully represent a classifier system. Each state in the model corresponds to a possible input instance of the classifier. Moreover, the classification function induces a partition of the set of instances, where each part corresponds to a set of input instances which are classified equally by the classifier. We call these models classifier models. BCL and its extensions open up new vistas including (i) defining counterfactual conditionals and studying their relationship with the notions of abductive and contrastive explanation, (ii) modeling classifier dynamics through the use of formal semantics for logics of communication and change [START_REF] Van Benthem | Logics of communication and change[END_REF][START_REF] Hans Van Ditmarsch | Dynamic Epistemic Logic[END_REF], and (iii) viewing a classifier as an agent and representing its uncertainty about the actual instance to be classified through the use of epistemic logic [START_REF] Fagin | Reasoning about Knowledge[END_REF].

Before concluding this introduction, it is worth noting that a classifier system is a simple form of causal system whose only dependency relations are between the input variables and the single output variable. Unlike Bayesian networks or artificial neural networks, a classifier system does not include 'intermediate' endogenous variables that, at the same time, depend on the input variables and causally influence the output variable(s). Therefore, many distinctions and disputations addressed in the theory of causality and causal explanation do not emerge in our work. For example, the vital distinction between correlation and causality [START_REF] Pearl | Causality[END_REF], the criticism of ceteris paribus as natural law [START_REF] Woodward | Explanation and invariance in the special sciences[END_REF], and whether a causal explanation requires providing information about a causal history or causal chain of events [START_REF] Lewis | Causal explanation[END_REF]. All these subtleties only show up when the causal structure is complex, and hence collapse in a classifier system, which has only two layers (input-output).

Outline The paper is structured as follows. In Section 2 we introduce our modal language as well as its formal semantics using the notion of classifier model. In Section 3 two proof systems are given, BCL and 'weak' BCL (WBCL). We show they are sound and complete relative to the classifier system semantics with, respectively, finite-input and infinite-input variables. Section 4 presents a family of counterfactual conditional operators and elucidates their relevance for understanding the behavior of a classifier system. Section 5 is devoted to classifier explanation. We extend the existing notions of explanation for Boolean classifiers to binary input classifiers. The notions include AXp, CXp and bias in the field of XAI. We will see that in the binary input classifier setting their behaviors are subtler. Besides, their connection with counterfactual is studied. Finally, in Section 6 we present two extensions of our language: (i) a dynamic extension by the notion of assignment enabling classifier change and (ii) an epistemic extension in which the classifier's uncertainty about the actual input can be represented. Further possible researches are discussed in the conclusion. Main results are either proven in the appendix or pointed out as corollaries.

Compared to our conference paper presented at CLAR 2021 [START_REF] Liu | A logic for binary classifiers and their explanation[END_REF], we do not restrict anymore to the language with finite variables. Thus two proof systems instead of one have to be presented, because in the infinite-variable setting the "functionality" property of classifiers cannot be syntactically expressed in a finitary way. The assumption of complete domain is dropped partially for the same technical reason. As a result, we are able to represent partial classifiers which were not expressible in the framework presented in our CLAR 2021 paper. Completeness and complexity results have been refined and improved. Other parts also changed according to possibly infinite variables and incomplete domain.

A Language for Binary Classifiers

In this section we introduce a language for modeling binary (input) classifiers and its semantics. The language has a ceteris paribus nature that comes from the ceteris paribus operators of the form [X] it contains. They were first introduced in [17]. 7

Basic Language and Classifier Model

Let Atm 0 be a countable set of atomic propositions with elements noted p, q, . . . which are used to represent the value taken by an input variable (or feature). When referring to input variables/features we sometimes use the notation 'p' to distinguish it from the symbol p for atomic proposition. In this sense, the atomic proposition p should be read "the Boolean input variable 'p' takes value 1", while its negation ¬p should be read "the Boolean input variable 'p' takes value 0". We introduce a finite set Val to denote the output values (classifications, decisions) of the classifier. Elements of Val are also called classes in the jargon of classifiers. For this reason, we note them c, c ′ , . . . For any c ∈ Val , we call t(c) a decision atom, to be read as "the actual decision (or output) takes value c", and have Dec = {t(c) : c ∈ Val }. Finally, let Atm = Atm 0 ∪ Dec be the set of atomic formulas. Notice symbols c and p have different statuses: p is an atomic proposition representing an atomic fact, while c is not. This explains why c (an output value) and t(c) (an atomic formula representing the fact that the actual output has a certain value) are distinguished.

The modal language L(Atm) is hence defined by the following grammar:

φ ::= p | t(c) | ¬φ | φ ∧ φ | [X]φ,
where p ranges over Atm 0 , c ranges over Val , and X is a finite subset of Atm 0 which we note X ⊆ fin Atm 0 . The set of atomic formulas occurring in a formula φ is noted Atm(φ).

The formula [X]φ has to be read "φ is necessary all features in X being equal" or "φ is necessary regardless of the truth or falsity of the atoms in Atm 0 \ X". Operator ⟨X⟩ is the dual of [X] and is defined as usual: ⟨X⟩φ = def ¬[X]¬φ.

The language L(Atm) is interpreted relative to classifier models whose class is defined as follows.

Definition 1 (Classifier model). A classifier model (CM) is a tuple C = (S, f ) where:

• S ⊆ 2 Atm0 is a set of states or input instances, and

• f : S -→ Val
(C, s) |= p ⇐⇒ p ∈ s, (C, s) |= t(c) ⇐⇒ f (s) = c, (C, s) |= ¬φ ⇐⇒ (C, s) ̸ |= φ, (C, s) |= φ ∧ ψ ⇐⇒ (C, s) |= φ and (C, s) |= ψ, (C, s) |= [X]φ ⇐⇒ ∀s ′ ∈ S, if (s ∩ X) = (s ′ ∩ X)then (C, s ′ ) |= φ.
We can think of a pointed model (C, s) as a pair (s, c) of f with f (s) = c. Thus, c is the output of the input instance s according to f . The condition (s ∩ X) = (s ′ ∩ X), which induces an equivalence relation modulo X, indeed stipulates that s and s ′ are indistinguishable regarding the atoms (the features) in X. The formula [X]φ is true at a state s if φ is true at all states that are modulo-X equivalent to state s. It has the selectis paribus (SP) (selected things being equal) interpretation "features in X being equal, necessarily φ holds (under possible perturbation on the other features)". When Atm 0 is finite, [Atm 0 \X]φ has the standard ceteris paribus (CP) interpretation "features other than X being equal, necessarily φ holds (under possible perturbation of the features in X)". 8 When X = ∅, [∅] is the S5 universal modality since every state is modulo-∅ equivalent to all states.

A formula φ of L(Atm) is said to be satisfiable relative to the class CM if there exists a pointed classifier model (C, s) with C ∈ CM such that (C, s) |= φ. It is said to be valid relative to CM, noted |= CM φ, if ¬φ is not satisfiable relative to CM. Moreover, we say that that φ is valid in the classifier model

C = (S, f ), noted C |= φ, if (C, s) |= φ for every s ∈ S.
It is worth noting that every modality [X] can be defined by means of the universal modality [∅]. To show this, let us introduce the following abbreviation for every Y ⊆ X ⊆ fin Atm 0 :

cn Y ,X = def p∈Y p ∧ p∈X\Y ¬p.
cn Y ,X can be seen as the syntactic expression of a valuation on X, and therefore represents a set of states in a classifier model satisfying the valuation. We have the following validity for the class CM:

|= CM [X]φ ↔ Y ⊆X cn Y ,X → [∅](cn Y ,X → φ) . It means that [X]φ is true at state s, if and only if, for whatever Y ⊆ X, if s ∩ X = Y then for any state s ′ such that s ′ ∩ X = Y , φ is true at s ′ .
Let us close this section by formally introducing our running example.

Example 2 (Applicant Alice, formal). Let Atm = {male, center, employed, owner} ∪ {t(1), t(0)}, where 1 and 0 stand for accepted and rejected respectively. Suppose C = (S, f ) is a CM such that S = 2 Atm0 and

C |= t(1) ↔ ((male ∧ employed) ∨ (employed ∧ owner)) .
Consider the state s = {center, employed}. Then, s stands for the instance Alice and f for the classifier in Example 1 such that f (s) = 0. Now Alice is asking for explanations of the decision/classification, e.g., 1) which of her features (necessarily) lead to the current decision, 2) changing which features would make a difference, 3) perhaps most importantly, whether the decision for her is biased. In Section 5 we will show how to use the language L(Atm) and its semantics to answer these questions.

Discussion

In this subsection we discuss in more detail some subtleties of classifier models in relation with the modal language L(Atm) which is interpreted over them.

X-Completeness

In the definition of classifier model (Definition 1) given above, we stipulated that the set of states S does not necessarily include all possible input instances of a classifier. More generally, according to our definition, a classifier model could be incomplete with respect to a set of atoms X from Atm 0 , that is, there could be a truth assignment for the atoms in X which is not represented in the model. Incompleteness of a classifier model is justified by the fact that in certain domains of application hard constraints exist which prevent for some input instance to occur. For example, a hard constraint may impose that a male cannot be pregnant (i.e., all states in which atoms male and pregnant are true should be excluded from the model).

However, it is interesting to see how completeness of a classifier with respect to a finite set of features can be represented in our semantics. This is what the following definition specifies.

Definition 3 (X-completeness). Let C = (S, f ) be a classifier model and X ⊆ fin Atm 0 . Then, C is said to be X-complete, if ∀X ′ ⊆ X, ∃s ∈ S such that s ∩ X = X ′ .
In plain words, the definition means that any truth assignment for the atoms in X is represented by some state of the model. As the following proposition indicates, the class of X-complete CMs can be syntactically represented. The proof is straightforward and omitted.

Proposition 1. Let C = (S, f ) be a CM and X ⊆ fin Atm 0 . C is X-complete if and only if ∀s ∈ S, we have (C, s) |= Comp(X), with Comp(X) = def X ′ ⊆X ⟨∅⟩cn X ′ ,X .
X-Definiteness In certain situations, there might be a portion of the feature space which is irrelevant for the classifier's decision. For example, in the Alice's example the fact of renting an apartment in the city center (the feature center) plays no role in the classification. In this case, we say that the classifier is definite with respect to the subset of features {male, employed, owner}.

More generally, a classifier is said to be definite with respect to a set of features X if its decision is only determined by the variables in X, that is to say, the variables in the complementary set Atm 0 \ X play no role in the classifier's decision. In other words, the classifier is said to be X-definite if its decision is independent of the variables in Atm 0 \ X.

The following definition introduces the concept of X-definiteness formally.

Definition 4 (X-definiteness). Let C = (S, f ) be a classifier model and

X ⊆ fin Atm 0 . Then, C is said to be X-definite, if ∀s, s ′ ∈ S, if s ∩ X = s ′ ∩ X then f (s) = f (s ′ ).
X-definiteness is tightly related to the notion of dependence studied in (propositional) dependence logic [START_REF] Yang | Propositional logics of dependence[END_REF]. The latter focuses on so-called dependence atoms of the form =(X, q) where q is a propositional variable and X is a finite set of propositional variables. The latter expresses the fact that the truth value of the propositional variable q only depends on the truth values of the propositional variables in X. It turns out that dependence atoms can be expressed in our ceteris paribus modal language L(Atm) as abbreviations:

=(X, q) = def [∅] (q → [X]q) ∧ (¬q → [X]¬q) .
Interestingly, the notion of X-definiteness is expressible in our modal language by means of the dependence atoms. This is what the following proposition indicates.

Proposition 2. Let C = (S, f ) be a CM and X ⊆ fin Atm 0 . C is X-definite if and only if ∀s ∈ S, (C, s) |= Defin(X) with

Defin(X) = def c∈Val = X, t(c) .
We conclude this section by mentioning some remarkable properties of Xdefiniteness. The first fact to be noticed is that X-definiteness is upward closed.

Fact 1. For every C ∈ CM and X ⊆ Y ⊆ fin Atm 0 , if C is X-definite then C is Y -definite too.
Secondly, X-definiteness for some X ⊆ fin Atm 0 is guaranteed in the finitevariable case.

Fact 2. For every C ∈ CM, if Atm 0 is finite then C is Atm 0 -definite.
This does not hold in the infinite case.

Fact 3. If Atm 0 is countably infinite and |Val | > 1 then there exists C ∈ CM such that, for all X ⊆ fin Atm 0 , C is not X-definite.
The previous fact is witnessed by any CM C = (S, f ) such that

• S = 2 Atm0 , • f (Atm 0 ) = 1, • ∀s ∈ S, if |Atm 0 △s| = 1 then f (s) = 0,
where Dec = {0, 1} and △ denotes symmetric difference, viz., s△s ′ = (s \ s ′ ) ∪ (s ′ \ s). It is easy to show that a CM so defined is not X-definite for any X ⊆ fin Atm 0 .

Axiomatization and Complexity

In this section, we provide axiomatics for our logical setting. We distinguish the finite-variable from the infinite-variable case. We moreover prove complexity results for satisfiability checking for both cases. But before, we will first introduce an alternative Kripke semantics for the interpretation of the language L(Atm). It will allow us to use the standard canonical model technique for proving completeness. Indeed, this technique cannot be directly applied to CMs in the infinite-variable case since our modal language is not expressive enough to capture the "functionality" property of CMs when Atm 0 is infinite. We think it would be possible to apply the canonical model argument directly to CMs in the finite-variable case. But we leave this to future work.

Alternative Kripke Semantics

In our alternative semantics the concept of classifier model is replaced by the following concept of decision model. It is a multi-relational Kripke structure with one accessibility relation per finite set of atoms plus a number of constraints over the accessibility relations and the valuation function for the atomic propositions.

Definition 5 (Decision model). A decision model (DM) is a tuple

M = W, (≡ X ) X⊆ fin Atm0 , V such that W is a set of possible worlds, V : W -→ 2 Atm
(C1) w ≡ X v iff V X (w) = V X (v), (C2) V Dec (w) ̸ = ∅, (C3) if t(c), t(c ′ ) ∈ V (w) then c = c ′ , (C4) if V Atm0 (w) = V Atm0 (v) then V Dec (w) = V Dec (v); where V X (w) abbreviates V (w) ∩ X. The class of DMs is noted DM. A DM W, (≡ X ) X⊆ fin Atm0 , V is called finite if W is finite. The class of finite-DM is noted finite-DM.
The interpretation of formulas in L(Atm) relative to a pointed DM goes as follows.

Definition 6 (Satisfaction relation). Let W, (≡ X ) X⊆ fin Atm0 , V be a DM and let w ∈ W . Then,

(M, w) |= p ⇐⇒ p ∈ V (w), (M, w) |= t(c) ⇐⇒ t(c) ∈ V (w), (M, w) |= ¬φ ⇐⇒ (M, w) ̸ |= φ, (M, w) |= φ ∧ ψ ⇐⇒ (M, w) |= φ and (M, w) |= ψ, (M, w) |= [X]φ ⇐⇒ ∀v ∈ W, if w ≡ X v then v |= φ.
Validity and satisfiability of formulas in L(Atm) relative to class DM (resp. finite-DM) is defined in the usual way.

The following theorem appears obvious, since it only has to do with the matter whether the decision function (classifier) f is given as a constituent of the model or induced from the model. Notice that it holds regardless of Atm 0 being finite or countably infinite.

Theorem 1. Let φ ∈ L(Atm). Then, φ is satisfiable relative to the class CM if and only if it is satisfiable relative to the class DM.

Axiomatization: Finite-Variable Case

In this section we provide a sound and complete axiomatics for the language L(Atm) relative to the formal semantics defined above under the assumption that the set of atomic propositions Atm 0 is finite. Definition 7 (Logic BCL). We define BCL (Binary Classifier Logic) to be the extension of classical propositional logic given by the following axioms and rules of inference:

[∅]φ ∧ [∅](φ → ψ) → [∅]ψ (K [∅] ) [∅]φ → φ (T [∅] ) [∅]φ → [∅][∅]φ (4 [∅] ) φ → [∅]⟨∅⟩φ (B [∅] ) [X]φ ↔ Y ⊆X cn Y ,X → [∅](cn Y ,X → φ) (Red [∅] ) c∈Val t(c) (AtLeast) t(c) → ¬t(c ′ ) if c ̸ = c ′ (AtMost) Y ⊆ fin Atm0 cn Y ,Atm0 ∧ t(c) → [∅] cn Y ,Atm0 → t(c) (Funct) φ → ψ, φ ψ (MP) φ [∅]φ (Nec [∅] )
It can be seen that [∅] is an S5 style modal operator, Red [∅] reduces any [X] to [∅]. AtLeast, AtMost, Funct represent the decision function syntactically and that every expression cn Y ,Atm0 maps to some unique t(c).

A decision model can contain two copies of the same input instance, while a classifier model cannot. Thus, Theorem 1 above shows that our modal language is not powerful enough to capture this difference between CMs and DMs. Axiom Funct intervenes in the finite-variable case to guarantee that two copies of the same input instance (that may exist in a DM) have the same output value. The expression cn Y ,Atm0 used in the axiom is an instance of the abbreviation we defined in Section 2.1. It represents a specific input instance. Notice that this abbreviation is only legal when Atm 0 is finite. Otherwise it would be the abbreviation of an infinite conjunction which is not allowed, since our modal language is finitary.

The proof of the following theorem is entirely standard and based on a canonical model argument.

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

The main result of this subsection is now a corollary of Theorems 1 and 2.

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

Axiomatization: Infinite-Variable Case

In Section 3.2, we have assumed that the set of atomic propositions Atm 0 representing input features is finite. In this section, we drop this assumption and prove completeness of the resulting logic.

An essential feature of the logic BCL is the "functionality" Axiom Funct. Such an axiom cannot be represented in a finitary way when assuming that the set Atm 0 is countably infinite. For this reason, it has to be dismissed and the logic weakened.

Definition 8 (Logic WBCL). The logic WBCL (Weak BCL) is defined by all principles of logic BCL given in Definition 7 except Axiom Funct.

In order to obtain the completeness of WBCL relative to the class CM, besides decision models (DMs), we need additionally quasi-decision models (QDMs).

Definition 9 (Quasi-DM). A quasi-DM is a tuple M = W, (≡ X ) X⊆ fin Atm0 , V where W , (≡ X ) X⊆ fin Atm0 and V are defined as in Definition 5 and which satisfies all constraints of Definition 5 except C4. The class of quasi-DMs is noted QDM.

A quasi-DM W, (≡ X ) X⊆ fin Atm0 , V is said to be finite if W is finite. The class of finite quasi-DMs is noted finite-QDM.

Semantic interpretation of formulas in L(Atm) relative to quasi-DMs is analogous to semantic interpretation relative to DMs given in Definition 6. Moreover, validity and satisfiability of formulas in L(Atm) relative to class QDM (resp. finite-QDM) is again defined in the usual way.

We are going to show the equivalence between QDM and CM step by step. The following theorem is proven by filtration. Theorem 3. Let Atm 0 be countably infinite and φ ∈ L(Atm). Then, φ is satisfiable relative to the class QDM if and only if φ is satisfiable relative to the class finite-QDM.

Then, let us establish the crucial fact that, in the infinite-variable case, the language L(Atm) cannot distinguish finite-DMs from finite-QDMs. We are going to prove that any formula φ satisfiable in a finite-QDM M is also satisfiable in some finite-DM M ′ . Since the only condition to worry is C4, we just need to transform the valuation function of M to guarantee that C4 holds while still satisfying φ. Theorem 4. Let Atm 0 be countably infinite and φ ∈ L(Atm). Then, φ is satisfiable relative to the class finite-QDM if and only if φ is satisfiable relative to the class finite-DM.

Recall Theorem 1 shows that L(Atm) can not distinguish between CMs and DMs regardless of Atm 0 being finite or infinite. Thus, we obtain the desired equivalence between model classes QDM and CM in the infinite-variable case, as a corollary of Theorems 1, 3 and 4. This fact is highlighted by Figure 1. More generally, Figure 1 shows that when Atm 0 is countably infinite the five semantics for the modal language L(Atm) are all equivalent, since from every node in the graph we can reach all other nodes. Theorem 5. Let Atm 0 be countably infinite and φ ∈ L(Atm). Then, φ is satisfiable relative to the class QDM if and only if φ is satisfiable relative to the class CM.

As a consequence, we are in position of proving that the logic WBCL is also sound and complete for the corresponding classifier model semantics, under the infinite-variable assumption. The only missing block is the following completeness theorem. The proof is similar to the proof of Theorem 2 (with the only difference that the canonical QDM does not need to satisfy C4), and omitted. Theorem 6. Let Atm 0 be countably infinite. Then, the logic WBCL is sound and complete relative to the class QDM.

The main result of this subsection turns out to be a direct corollary of Theorems 5 and 6.

Corollary 2. Let Atm 0 be countably infinite. Then, the logic WBCL is sound and complete relative to the class CM.

Complexity Results

Let us now move from axiomatics to complexity issues. Our first result is about complexity of checking satisfiability for formulas in L(Atm) relative to the class CM when Atm 0 is finite and fixed. It is in line with the satisfiability checking problem of the modal logic S5 which is known to be polynomial in the finitevariable case [START_REF] Joseph | The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic[END_REF]. Theorem 7. Let Atm 0 be finite and fixed. Then, checking satisfiability of formulas in L(Atm) relative to CM can be done in polynomial time.

As the following theorem indicates, the satisfiability checking problem becomes intractable when dropping the finite-variable assumption. Theorem 8. Let Atm 0 be countably infinite. Then, checking satisfiability of formulas in L(Atm) relative to CM is NEXPTIME-complete.

Let us consider the following fragment L {[∅]} (Atm) of the language L(Atm) where only the universal modality [∅] is allowed: Clearly, satisfiability checking for formulas in L {[∅]} (Atm) remains polynomial when there are only finitely many primitive propositions. As the following theorem indicates, complexity decreases from NEXPTIME to NP when restricting to the fragment L {[∅]} (Atm) under the infinite-variable assumption.

φ ::= p | t(c) | ¬φ | φ ∧ φ | [∅]φ.
Theorem 9. Let Atm 0 be countably infinite. Then, checking satisfiability of formulas in L {[∅]} (Atm) relative to CM is NP-complete.

The complexity results of this section are summarized in Table 1.

Fixed finite variables Infinite variables Fragment

L {[∅]} (Atm) Polynomial NP-complete Full language L(Atm) Polynomial NEXPTIME-complete

Counterfactual Conditional

In this section we investigate a simple notion of counterfactual conditional for binary classifiers, inspired from Lewis' notion [START_REF] Lewis | Counterfactuals[END_REF]. In Section 5, we will elucidate its connection with the notion of explanation. We start our analysis by defining the following notion of similarity between states in a classifier model relative to a finite set of features X.

Definition 10 (Similarity between states). Let C = (S, f ) be a classifier model, s, s ′ ∈ S and X ⊆ fin Atm 0 . The similarity between s and s ′ in S relative to the set of features X, noted sim C (s,s ′ ,X), is defined as follows:

sim C (s,s ′ ,X) = |{p ∈ X : (C, s) |= p iff (C, s ′ ) |= p}|.
A dual notion of distance between worlds can defined from the previous notion of similarity:

dist C (s,s ′ ,X) = |X| -sim C (s,s ′ ,X).
This notion of distance is in accordance with [START_REF] Dalal | Investigations into a theory of knowledge base revision: preliminary report[END_REF] in knowledge revision. 9 The following definition introduces the notion of counterfactual conditional as an abbreviation. It is a form of relativized conditional, i.e., a conditional with respect to a finite set of features. 10 Definition 11 (Counterfactual conditional). We write φ ⇒ X ψ to mean that "if φ was true then ψ would be true, relative to the set of features X" and define it as follows:

φ ⇒ X ψ = def 0≤k≤|X| maxSim(φ,X,k) → Y ⊆X:|Y |=k [Y ](φ → ψ) , with maxSim(φ,X,k) = def Y ⊆X:|Y |=k ⟨Y ⟩φ ∧ Y ⊆X:k<|Y | [Y ]¬φ.
As the following proposition highlights, the previous definition of counterfactual conditional is in line with Lewis' view: the conditional holds if all closest worlds to the actual world in which the antecedent is true satisfy the consequent of the conditional. 9 There are other options besides measuring distance by cardinality, e.g., distance in sense of subset relation as [START_REF] Borgida | Language features for flexible handling of exceptions in information systems[END_REF]. We will consider them in further research. 10 A similar approach to conditional is presented in [START_REF] Girard | Ceteris paribus logic in counterfactual reasoning[END_REF]. They also refine Lewis' semantics for counterfactuals by selecting the closest worlds according to not only the actual world and antecedent, but also a set of formulas noted Γ. The main technical difference is that they allow any counterfactual-free formula as a member of Γ, while in our setting X only contains atomic formulas.

For notational convenience, we simply write φ ⇒ ψ instead of φ ⇒ Atm0 ψ, when Atm 0 is finite. Formula φ ⇒ ψ captures the standard notion of conditional of conditional logic. One can show that ⇒ satisfies all semantic conditions of Lewis' logic VC. 11 However, when Atm 0 is infinite, φ ⇒ ψ is not a well-formed formula since it ranges over an infinite set of atoms. In that case φ ⇒ X ψ has to be always indexed by some finite X.

The interesting aspect of the previous notion of counterfactual conditional is that it can be used to represent a binary classifier's approximate decision for a given instance. Let us suppose the set of decision values Val includes a special symbol ? meaning that the classifier has no sufficient information enabling it to classify an instance in a precise way. More compactly, ? is interpreted as that the classifier abstains from making a precise decision. In this situation, the classifier can try to make an approximate decision: it considers the closest instances to the actual instance for which it has sufficient information to make a decision and checks whether the decision is uniform among all such instances. In other words, c is the classifier's approximate classification of (or decision for) the actual instance relative to the set of features X, noted apprDec(X,c), if and only if "if a precise decision was made relative to the set of features X, then this decision would be c". Formally:

apprDec(X,c) = def c ′ ∈Val:c ′ ̸ =? t(c ′ ) ⇒ X t(c).
The following proposition provides two interesting validities. Proposition 4. Let Atm 0 be finite, c, c ′ ∈ Val \ {?}. Then,

|= CM apprDec(X, c) → ¬apprDec(X, c ′ ) if c ̸ = c ′ , |= CM t(c) → apprDec(Atm 0 , c).
According to the first validity, a classifier cannot make two different approximate decisions relative to a fixed set of features X.

According to the second validity, if the classifier is able to make a precise decision for a given instance, then its approximate decision coincides with it. This second validity works since the actual state/instance is the only closest state/instance to itself. Therefore, it the actual state/instance has a precise classification c, all its closest states/instances also have it.

It is worth noting that the following formula is not valid relative to the class CM:

c∈Val\{?} apprDec(X, c).
This means that a classifier may be unable to approximately classify the actual instance. The reason is that there could be different closest states to the actual one with different classifications.

Explanations and Biases

In this section, we are going to formalize some existing notions of explanation of classifiers in our logic, and deepen the current study from a (finitely) Boolean setting to a multi-valued output, partial domain and possibly infinite-variable setting. For this purpose it is necessary to introduce the following notations.

Let λ denote a conjunction of finitely many 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 λ ′ ⊆ λ. By convention ⊤ is a term of zero conjuncts. In particular, suppose λ is cn X,Y for some X ⊆ Y ⊆ fin Atm 0 , then λ will denote the conjunction resulting from "flipping" (or "perturbing") all literals of λ, i.e., cn Y \X,Y .

In the glossary of Boolean classifiers, λ is called a term or property (of an instance). The set of terms is noted Term. We use Term(X) to denote all terms whose atoms are in X. Additionally, to define the notion of bias we distinguish the set of protected features PF ⊆ Atm 0 , like 'gender' and 'race', and the set of non-protected features NF = Atm 0 \ PF.

Notice that in this section the cardinality of Atm 0 matters. Notions and results in Section 5.1 (without special instruction) apply to both Atm 0 finite and Atm 0 countably infinite. On the contrary, in Sections 5.2 and 5.3, we restrict to the case Atm 0 finite, which is due to the use of formulas [Atm 0 \ X]φ, [NF]φ and [PF]φ there. We clarify it here instead of clarifying it below repeatedly.

Prime Implicant and Abductive Explanation

We are in position to formalize the notion of prime implicant, which plays a fundamental role in the theory of Boolean functions since [START_REF] Quine | A way to simplify truth functions[END_REF].

Definition 12 (Prime implicant (PImp)). We write PImp(λ, c) to mean that λ is a prime implicant for c and define it as follows:

PImp(λ, c) = def [∅] λ → t(c) ∧ p∈Atm(λ) ⟨Atm(λ) \ {p}⟩¬t(c) .
It is a proper extension of the definition of prime implicant in the Boolean setting since it is a term λ such that 1) it necessarily implies the actual classification (why it is called an implicant); 2) any of its proper subsets fails to necessarily imply the actual classification (why it is called prime). Notice that being a prime implicant is a global property of the classifier, though we formalize it by means of a pointed model. The syntactic abbreviation for prime implicant can be better understood by observing that for a given CM C = (S, f ) and s ∈ S, we have:

(C, s) |= PImp(λ, c) iff (i) ∀s ′ ∈ S, if (C, s ′ ) |= λ then (C, s ′ ) |= t(c); and (ii) ∀λ ′ ⊂ λ, ∃s ′ ∈ S such that (C, s ′ ) |= λ ′ ∧ ¬t(c).
To explain the actual classification of a given input, some XAI researchers consider prime implicants which are actually true. We use the terminology by [START_REF] Ignatiev | Abductionbased explanations for machine learning models[END_REF] and call them abductive explanations (AXp).

Definition 13 (Abductive explanation (AXp)). We write AXp(λ, c) to mean that λ abductively explains the decision c and define it as follows:

AXp(λ, c) = def λ ∧ PImp(λ, c).
AXp is a local explanation, because λ is not only a prime implicant for the classification, but also a property of the actual instance to be classified. AXp can be expanded to highlight its connection with the notion of variance/invariance. Proposition 5. Let λ ∈ Term and c ∈ Val . Then, we have the following validity:

|= CM AXp(λ, c) ↔ λ ∧ [Atm(λ)]t(c) ∧ p∈Atm(λ) ⟨Atm(λ) \ {p}⟩¬t(c) .
The formula [Atm(λ)]t(c) expresses the idea of invariance under intervention (perturbation): as long as the explanans variables are kept fixed, namely the variables in λ, any perturbation on the other variables does not change the explanandum, namely classification c.

Many names besides AXp are found in literature, e.g., PI-explanation [41] and sufficient reason [START_REF] Darwiche | On the reasons behind decisions[END_REF]. Darwiche and Hirth in [START_REF] Darwiche | On the reasons behind decisions[END_REF] proved that any decision has a sufficient reason in the Boolean setting. The result is not a surprise, for a Boolean function always has a prime implicant, since by definition the arity of a Boolean function is always finite. However, since we allow functions with infinitely many variables, AXps are not guaranteed to exist in general. The statement can be proved by exhibiting the same infinite countermodel as in Fact 3 in Section 2.2. However, if a CM is X-definite for some X ⊆ fin Atm 0 , then every state has an AXp, even when the CM is infinite.

Proposition 6. Let C = (S, f ) ∈ CM and X ⊆ fin Atm 0 . If C is X-definite then ∀s ∈ S, ∃λ ∈ Term such that (C, s) |= AXp λ, f (s) .
Lastly, let us continue with the Alice example.

Example 3. Recall the state of Alice s = {center, employed}. We have (C, s) |= AXp(¬male ∧ ¬owner, 0), namely that Alice's being female and not owning a property abductively explains the rejection of her application.

Contrastive Explanation (CXp)

AXp is a minimal part of the actual instance guaranteeing the current decision. A natural counterpart of AXp is contrastive explanation (CXp, named in [START_REF] Ignatiev | From contrastive to abductive explanations and back again[END_REF]). Definition 14 (Contrastive explanation (CXp)). We write CXp(λ, c) to mean that λ contrastively explains the decision c and define it as follows:

CXp(λ, c) = def λ ∧ ⟨Atm 0 \ Atm(λ)⟩¬t(c)∧ p∈Atm(λ) [(Atm 0 \ Atm(λ)) ∪ {p}]t(c).
The definition says nothing but 1) λ is part of the actual input instance; 2) if the values of all variables in λ are changed while the values of the other variables are kept fixed, then the actual classification may change; 3) the classification will not change, if the variables outside λ and at least one variable in λ keep their actual values. The latter captures a form of necessity: when the values of the variables outside λ are kept fixed, all variables in λ should be necessarily perturbed to change the actual classification.

The syntactic abbreviation for contrastive explanation can be better understood by observing that for a given CM C = (S, f ) and s ∈ S, we have:

(C, s) |= CXp(λ, c) iff (i) (C, s) |= λ; (ii) ∃s ′ ∈ S s.t. s△s ′ = Atm(λ) and (C, s ′ ) |= ¬t(c); and (iii) ∀s ′ ∈ S, if s△s ′ ⊂ Atm(λ) then (C, s ′ ) |= t(c).
CXp has a counterfactual flavor since it answers to question: would the classification differ from the actual one, if the values of all variables in the explanans were different? So, there seems to be a connection with the notion of counterfactual conditional we introduced in Section 4. Actually in XAI, many researchers consider contrastive explanation and counterfactual explanation either closely related [START_REF] Verma | Counterfactual explanations for machine learning: A review[END_REF] or even interchangeable [START_REF] Sokol | Counterfactual explanations of machine learning predictions: opportunities and challenges for ai safety[END_REF]. The following proposition sheds light on this point. Proposition 7. Let λ be a term and let l be a literal. Then, we have the following two validities:

|= CM CXp(λ, c) → t(c) ∧ λ ⇒ ¬t(c) , |= CM CXp(l, c) ↔ t(c) ∧ ¬l ⇒ ¬t(c) .
According to the first validity, in the general case contrastive explanation implies counterfactual explanation. According to the second validity, when the explanans is a literal (a single-conjunct term), contrastive explanation coincides with counterfactual explanation. In particular, literal l contrastively explains the decision c if and only if (i) the actual decision is c and (ii) if literal l was perturbed, then the decision would be different from c. In other words, in the "atomic" case CXp is the same as counterfactual explanation.

Note that the right-to-left direction of the first validity does not necessarily hold. To see this, it is sufficient to suppose that Atm 0 = {p, q} and Dec = {0, 1} and to consider the CM (S, f ) such that S = 2 Atm0 with f {p, q} = 0 and

f {p} = f {q} = f ∅ = 1.
It is easy to check that in the model so defined we have

C, {p, q} |= t(0) ∧ p ∧ q ⇒ ¬t(0) , but at the same time, C, {p, q} |= ¬CXp(p ∧ q, 0).
The problem is that the model fails to satisfy the necessity condition of contrastive explanation: it is not necessary to perturb both literals in p ∧ q to change the actual decision from 0 to 1, it is sufficient to perturb one of them. We can conclude that CXp is a special kind of counterfactual explanation with the additional requirement of necessity for the explanans.

Example 4. In Alice's case, we have (C, s) |= CXp(¬male, 0)∧CXp(¬owner, 0). This means that both Alice's being female and not owning property contrastively explain the rejection. Moreover, we have (C, s) |= (¬male ∨ ¬owner) ⇒ t(1), namely if Alice was a male or an owner (of an immobile property), then her application would have been accepted.

Moreover, since the feature 'gender' is hard to change, owing a property is the (relatively) actionable explanation for Alice, 12 if she intends to comply with the classifier's decision. But surely Alice has another option, i.e., alleging the classifier as biased. As we will see in the next subsection, an application of CXp is to detect decision biases in a classifier.

Decision Bias

A primary goal of XAI is to detect and avoid biases. Bias is understood as making decision with respect to some protected features, e.g., 'race', 'gender' and 'age'.

There is a widely accepted notion of decision bias in the setting of Boolean functions which can be represented in our Example 2 (see [START_REF] Darwiche | On the reasons behind decisions[END_REF][START_REF] Ignatiev | Towards formal fairness in machine learning[END_REF]). Intuitively, the rejection for Alice is biased if there is another applicant, say Bob, who only differs from Alice on the protected feature 'gender', but gets accepted.

Definition 15 (Decision bias). We write Bias(c) to mean that the decision c is biased and define it as follows:

Bias(c) = def t(c) ∧ ⟨NF⟩¬t(c).
The definition says that the decision c is biased at a given state s, if (i) f (s) = c, and (ii) ∃s ′ ∈ S such that s△s ′ ⊆ PF and f (s ′ ) ̸ = c. The latter, in plain words, requires another instance s ′ , which only differs from s on some protected features, but obtains a different classification.

As we stated, CXp can be used to detect decision biases. The following result makes the statement precise.

Proposition 8. We have the following validity:

|= CM Bias(c) ↔ Atm(λ)⊆PF CXp(λ, c).
Let us end up the whole section by answering the last question regarding Alice raised at the end of Section 2.1.

Example 5. Split Atm 0 in Example 2 into PF = {male, center} and NF = {employed, owner}. We then have (C, s) |= Bias(0) ∧ CXp(male, 0) ∧ ¬male ⇒ t(1) . The decision for Alice is biased since 'gender' is the protected feature which contrastively explains the rejection, and if Alice was male, her application would have been accepted.

Extensions

In this section, we briefly discuss two interesting extensions of our logical framework and analysis of binary classifiers. Their full development is left for future work.

Dynamic Extension

The first extension we want to discuss consists in adding to the language L(Atm) dynamic operators of the form [c := φ] with c ∈ Val , where c := φ is a kind of assignment in the sense of [START_REF] Van Benthem | Logics of communication and change[END_REF][START_REF] Hans P Van Ditmarsch | Dynamic epistemic logic with assignment[END_REF] and the formula [c := φ]ψ has to be read "ψ holds after every decision is set to c in context φ". The resulting language, noted L dyn (Atm), is defined by the following grammar:

f c:=φ (s ′ ) = c if (C, s ′ ) |= φ, f (s ′ ) otherwise.
Intuitively, the operation c := φ consists in globally classifying all instances satisfying φ with value c.

Dynamic operators [c := φ] are useful for modeling a classifier's revision. Specifically, new knowledge can be injected into the classifier thereby leading to a change in its classification. For example, the classifier could learn that if an object is a furniture, has one or more legs and has a flat top, then it is a table. This is captured by the following assignment:

table := objIsFurniture ∧ objHasLegs ∧ objHasFlatTop.
An application of dynamic change is to model the training process of a classifier, together with counterfactual conditionals with "?" in Section 4. Suppose at the beginning we have a CM C = (S, f ) which is totally ignorant, i.e., ∀s ∈ S, f (s) =?. We then prepare to train the classifier. The training set consists of pairs (s 1 , x 1 ), (s 2 , x 2 ) . . . (s n , x n ) where ∀i ∈ {1, . . . , n}, s i ∈ S, x i ∈ (Val \{?}) and ∀j ∈ {1, . . . , n}, i ̸ = j implies s i ̸ = s j . We train the classifier by revising it with [x 1 := s 1 ] . . . [x n := s n ] one by one. Obviously the order does not matter here. In other words, we re-classify some states. With a bit abuse of notation, let C train = (S, f train ) denote the model resulting from the series of revisions. We finish training by inducing the final model C † = (S, f † ) from C train , where ∀s ∈ S, f † (s) = c, if (C train , s) |= apprDec(Atm 0 ,c), otherwise f † (s) = f train (s). This is an example of modeling a special case of the so-called k-nearest neighbour (KNN) classification in machine learning [START_REF] Cunningham | K-nearest neighbour classifiers -a tutorial[END_REF], where the distance is measured by cardinality. If a new case/instance has to be classified, we see how the most similar cases to the new case were classified. If all of them (k of them in the case of KNN) were classified using the same category, we put the new case into that category.

The logics BCL-DC and WBCL-DC (BCL and WBCL with Decision Change) extend the logic BCL and WBCL by the dynamic operators [c := φ]. They are defined as follows.

Definition 16 (Logics BCL-DC and WBCL-DC). We define BCL-DC (resp. WBCL-DC) to be the extension of BCL (resp. WBCL) of Definition 7 (resp. Definition 8) generated by the following reduction axioms for the dynamic operators [c := φ]:

[c := φ]t(c) ↔ φ ∨ t(c) [c := φ]t(c ′ ) ↔ ¬φ ∧ t(c ′ ) if c ̸ = c ′ [c := φ]p ↔p [c := φ]¬ψ ↔¬[c := φ]ψ [c := φ](ψ 1 ∧ ψ 2 ) ↔ [c := φ]ψ 1 ∧ [c := φ]ψ 2 [c := φ][X]ψ ↔[X][c := φ]ψ
and the following rule of inference:

φ 1 ↔ φ 2 ψ ↔ ψ[φ 1 /φ 2 ] (RE)
It is routine exercise to verify that the equivalences in Definition 16 are valid for the class CM and that the rule of replacement of equivalents (RE) preserves validity. The completeness of BCL-DC (resp. WBCL-DC) for this class of models under the finite-variable assumptions (resp. infinite-variable assumption) follows from Corollary 1 (resp. Corollary 2), 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 10. Let Atm 0 be finite. Then, the logic BCL-DC is sound and complete relative to the class CM. Theorem 11. Let Atm 0 be countably infinite. Then, the logic WBCL-DC is sound and complete relative to the class CM.

The following complexity results are consequences of Theorems 7 and 8 and the fact that via the reduction axioms in Definition 8 we can find a polynomial reduction of satisfiability checking for formulas in L dyn to satisfiability checking for formulas in L.

Theorem 12. Let Atm 0 be finite and fixed. Then, checking satisfiability of formulas in L dyn (Atm) relative to CM can be done in polynomial time.

Theorem 13. Let Atm 0 be countably infinite. Then, checking satisfiability of formulas in L dyn (Atm) relative to CM is NEXPTIME-complete.

Epistemic Extension

In the second extension we suppose that a classifier is an agent which has to classify what it perceives. The agent could have uncertainty about the actual instance to be classified since it cannot see all its input features.

In order to represent the agent's epistemic state and uncertainty, we introduce an epistemic modality of the form K which is used to represent what the agent knows in the light of what it sees. Similar notions of visibility-based knowledge can be found in [START_REF] Charrier | Building epistemic logic from observations and public announcements[END_REF][START_REF] Van | Knowledge and control[END_REF][START_REF] Herzig | A poor man's epistemic logic based on propositional assignment and higher-order observation[END_REF][START_REF] Wiebe Van Der Hoek | A logic of revelation and concealment[END_REF].

The language for our epistemic extension is noted L epi (Atm) and defined by the following grammar:

φ ::= p | t(c) | ¬φ | φ ∧ φ | [X]φ | Kφ,
where p ranges over Atm 0 , c ranges over Val , and X ⊆ fin Atm 0 .

In order to interpret the new modality K, we have to enrich classifier models with an epistemic component. Clearly, the relation ∼ so defined is an equivalence relation. According to the previous definition, the agent cannot distinguish between two states s and s ′ , noted s ∼ s ′ , if and only if the truth values of the visible variables are the same at s and s ′ .

The interpretation for formulas in L epi (Atm) extends the interpretation for formulas in L(Atm) given in Definition 2 by the following condition for the epistemic operator:

(E, s) |= Kφ ⇐⇒ ∀s ′ ∈ S : if s ∼ s ′ then (E, s ′ ) |= φ.
As the following theorem indicates, the complexity result of Section 3.2 for the finite-variable case generalizes to the epistemic extension. Theorem 14. Let Atm 0 be finite. Then, checking satisfiability of formulas in L epi (Atm) relative to ECM can be done in polynomial time.

In order to illustrate the intuition behind the epistemic modality K we go back to the example of the application for a loan to a bank. Example 6. Suppose the application is submitted through an online system which has to automatically decide whether it is acceptable or not. In his/her application, an applicant has to specify a value for each feature. Moreover, suppose the system receives an incomplete application: the applicant has only indicated that she is female, owns an apartment and lives in the city center, but she has forgotten to specify whether she has an employment or not. In this case, the value of the employement variable is not "visible" to the system. In formal terms, we extend the CM given in Example 2 by the visibility set Obs = {male, center, owner} to obtain a ECM E = (S, f, Obs). It is easy to check that the following holds: E, {center, employed, owner} |= ¬K t(0) ∧ ¬K t(1). This means that, on the basis of its partial knowledge of the applicant's identity, the system does not know what to decide. However, the system knows that if turns out that the applicant is employed then its application should be accepted: E, {center, employed, owner} |= K employed → t(1) .

Finally, the classifier knows that if turns out that the applicant is employed, then the fact that she is employed and that she owns a property will abductively explain the decision to accept her application: E, {center, employed, owner} |= K employed → AXp(employed ∧ owner, 1) .

Conclusion

We have introduced a modal language and a formal semantics that enable us to capture the ceteris paribus nature of binary classifiers. We have formalized in the language a variety of notions which are relevant for understanding a classifier's behavior including counterfactual conditional, abductive and contrastive explanation, bias. We have provided two extensions that support reasoning about classifier change and a classifier's uncertainty about the actual instance to be classified. We have also offered axiomatics and complexity results for our logical setting.

We believe that the complexity results presented in the paper are exploitable in practice. We have shown that satisfiability checking in the basic setting and in its dynamic and epistemic extension is polynomial when finitely many variables are assumed. In the infinite-variable setting, it becomes NEXPTIME-complete and NP-complete when restricting to the language in which the only primitive modal operator is the universal modality [∅]. In future work, we plan (i) to find a number of satisfiability preserving translations from our modal languages to the modal logic S5 and then from S5 to propositional logic using existing techniques [START_REF] Caridroit | A SAT-based approach for solving the modal logic s5-satisfiability problem[END_REF], and (ii) to exploit SAT solvers for automated verification and generation of explanations and biases in binary classifiers.

Another direction of future research is the generalization of the epistemic extension given in Section 6.2 to the multi-agent case. The idea is to conceive classifiers as agents and to be able to represent both the agents' uncertainty about the instance to be classified and their knowledge and uncertainty about other agents' knowledge and uncertainty (i.e., higher-order knowledge and uncertainty). Similarly, we plan to investigate more in depth classifier dynamics we briefly discussed in Section 6.1. The idea is to see them as learning dynamics. Based on this idea, we plan to study the problem of finding a sequence of update operations guaranteeing that the classifier will be able to make approximate decisions for a given set of instances.

Finally, all classifiers we handle in this paper are essentially "white box", in the sense that we have perfect knowledge of them, so that we can compute their explanations. However, "black box" classifiers are the most interesting ones to XAI. In [START_REF] Liu | A logic of "black box" classifier systems[END_REF] we conceived a "black box" classifier as an agent's uncertainty among many possible "white box" classifiers. We represented it by extending our language with a modal operator ranging over all possible functions which are compatible with the agent's partial knowledge. All notions of explanation we defined in this paper can be generalized to the "black box" setting. However, there are some important differences between the two settings. For instance, in a "black box" classifier AXp does not always exist, as we showed in [START_REF] Liu | A logic of "black box" classifier systems[END_REF], which contradicts Proposition 6.

A.14 Proof of Proposition 8

Proof. We show that for any C = (S, f ) ∈ CM, both directions are satisfied in (C, s) for some s ∈ S. The right to left direction is obvious, since from the antecedent we know there is a property λ ′ s.

A.15 Proof of Theorem 14

Proof. Suppose |Atm 0 | is finite. As in the proof of Theorem 7, we can show that the size of the model class ECM is bounded by some fixed integer. Thus, in order to determine whether a formula φ L epi (Atm) is satisfiable for this class, it is sufficient to repeat model checking a number of times which is bounded by some integer. Model checking for the language L epi (Atm) with respect to a pointed ECM is polynomial.

  is a decision (or classification) function. The class of classifier models is noted CM. A pointed classifier model is a pair (C, s) with C = (S, f ) a classifier model and s ∈ S. Formulas in L(Atm) are interpreted relative to a pointed classifier model, as follows. Definition 2 (Satisfaction relation). Let (C, s) be a pointed classifier model with C = (S, f ) and s ∈ S. Then:

  is a valuation function for atomic formulas, and ∀w, v ∈ W, c, c ′ ∈ Val the following constraints are satisfied:

Figure 1 :

 1 Figure 1: Relations between semantics for the modal language L(Atm). An arrow means that satisfiability relative to the first class of structures implies satisfiability relative to the second class of structures. Full arrows correspond to the results stated in Theorems 1, 3 and 4. Dotted arrows denote relations that follow straightforwardly given the inclusion between classes of structures. The bidirectional arrows connecting node 3 with node 4 and node 4 with node 5 only apply to the infinite-variable case.

Proposition 3 .

 3 Let C = (S, f ) be a classifier model, s ∈ S and X ⊆ fin Atm 0 . Then, (C, s) |= φ ⇒ X ψ if and only if closest C (s,φ,X) ⊆ ||ψ|| C , where closest C (s,φ,X) = arg max s ′ ∈||φ|| C sim C (s,s ′ ,X), and for every φ ∈ L(Atm): ||φ|| C = {s ∈ S : (C, s) |= φ}.

Fact 4 .

 4 Let Atm 0 be countably infinite and |Val | > 1. Then, there exists some C = (S, f ), s ∈ S, such that ∃c ∈ Val , ∀λ ∈ Term, (C, s) |= ¬AXp(λ, c).

φ

  ::= p | t(c) | ¬φ | φ ∧ φ | [X]φ | [c := φ]ψ, where p ranges over Atm 0 , c ranges over Val , and X ⊆ fin Atm 0 . The interpretation of formula [c := φ]ψ relative to a pointed classifier model (C, s) with C = (S, f ) goes as follows: (C, s) |= [c := φ]ψ ⇐⇒ (C c:=φ , s) |= ψ, where C c:=φ = (S, f c:=φ ) is the updated classifier model where, for every s ′ ∈ S:

Definition 17 (

 17 Epistemic classifier model). An epistemic classifier model (ECM) is a tuple E = (S, f, Obs) where C = (S, f ) is a classifier model and Obs ⊆ Atm 0 is the set of atomic propositions that are visible to the agent. The class of ECMs is noted ECM. Given an ECM E = (S, f, Obs), we can define an epistemic indistinguishability relation which represents the agent's uncertainty about the actual input instance. Definition 18 (Epistemic indistinguishability relation). Let E = (S, f, Obs) be an ECM. Then, ∼ is the binary relation on S such that, for all s, s ′ ∈ S: s ∼ s ′ if and only if (s ∩ Obs) = (s ′ ∩ Obs).

  to show (C, s) |= λ ⇒ ¬t(c). By the antecedent, ∃s ′ ∈ S, s.t. s△s ′ = Atm(λ) and f (s′ ) ̸ = c. It is not hard to show that closest C (s,λ,Atm) = {s ′ }. Therefore (C, s) |= λ ⇒ ¬t(c), since closest C (s,λ,Atm 0 ) ⊆ ||¬t(c)|| C .For the second validity, the right direction is a special case of the first validity. To show the left direction, from the antecedent we have ∃s ′ ∈ S, s.t. s ′ △s = Atm(l) and {s ′ } = closest C (s,l,Atm 0 ). Hence (C, s) |= l∧⟨Atm 0 \Atm(l)⟩¬t(c)∧[Atm 0 ]t(c), which is by definition (C, s) |= CXp(l, c).

  t. ∃s ′ ∈ S, s△s ′ = Atm(λ ′ ) ⊆ PF and (C, s ′ ) |= ¬t(c), which means (C, s) |= Bias(c). The other direction is proven by contraposition. Suppose for any λ s.t. Atm(λ) ⊆ PF, (C, s) |= ¬CXp(λ, c), then it means ∀s ′ ∈ S, if s△s ′ = Atm(λ), then f (s ′ ) = c, which means (C, s) |= ¬Bias(c).

Table 1 :

 1 Summary of complexity results

We use them as synonyms through the paper. Another set of synonyms is perturbation/intervention/manipulation. The variety of terminology is unfortunate.

2 E.g., whether all explanations are causal, whether metaphysical explanation/grounding should be distinguished from causal

explanation.[START_REF] Baltag | A simple logic of functional dependence[END_REF] Using the notion of counterfactual dependence for reasoning about natural laws and causality traces back to[START_REF] Goodman | Fact, fiction, and forecast[END_REF][START_REF] Lewis | Counterfactual dependence and time's arrow[END_REF][START_REF] Lewis | Causation[END_REF]. The focus nowadays, e.g.[START_REF] Woodward | Explanation and invariance in the special sciences[END_REF][START_REF] Joseph Y Halpern | Actual causality[END_REF], is on the use of counterfactuals for modeling the notion of actual cause in order to test (rather than

define) causality.[START_REF] Biran | Explanation and justification in machine learning: A survey[END_REF] Woodward & Hitchcock also discuss invariance with respect to the background conditions not figuring in the relationship between explanans and explanandum. Nonetheless, they consider this type of invariance less central to causal explanation.

AXp satisfies an additional restriction of minimality that will be elucidated at a later stage: an AXp is a 'minimal' term for which the classifier's actual decision is invariant under perturbation.

We prefer the notation AXp used by Ignatiev et al.[START_REF] Ignatiev | Abductionbased explanations for machine learning models[END_REF][START_REF] Ignatiev | From contrastive to abductive explanations and back again[END_REF] for its connection with CXp.

More recently, similar operators have been used in the context of the logic of functional dependence by Baltag & van Benthem[START_REF] Baltag | A simple logic of functional dependence[END_REF].

We thank Giovanni Sartor for drawing the distinction between CP and SP.

A remarkable fact is that not all ⇒ X satisfy the strong centering condition, which says that the actual world is the only closest world when the antecedent is already true there. To see it, consider a toy classifier model (C, s) such that S = {s, s ′ , s ′′ , s ′′′ } with s = {p, q}, s ′ = {p}, s ′′ = {q}, s ′′′ = ∅. We have closest C (s,p,{p}) = {s, s ′ }, rather than closest C (s,p,{p}) = {s}.

For the significance of actionability in XAI, see e.g.[START_REF] Sokol | Counterfactual explanations of machine learning predictions: opportunities and challenges for ai safety[END_REF].

Acknwoledgments

This work is supported by the ANR-3IA Artificial and Natural Intelligence Toulouse Institute (ANITI).

A Tecnical annex

This technical annex contains a selection of proofs of the results given in the paper.

A.1 Proof of Proposition 2

Proof. Suppose C is X-definite but (C, s) |= ¬Defin(X), which means that ∃c ∈ Val s.t. (C, s) |= ¬ =(X, t(c)). W.l.o.g., we assume that (C, s) |= ¬[∅](¬t(c) → [X]¬t(c)). That is to say, ∃s ′ ∈ S, s.t. f (s ′ ) ̸ = c but (C, s ′ ) |= ⟨X⟩t(c). The latter indicates that ∃s ′′ ∈ S, s.t. s ′′ ∩ X = s ′ ∩ X but f (s ′′ ) = c, which violates X-definiteness.

Let (C, s) |= Defin(X), and assume f (s) c Then since (C, s)

A.2 Proof of Theorem 1

Proof. For the left to right direction, given a CM C = (S, f ) and s 0 ∈ S s.t. (C, s 0 ) |= φ, we construct a DM M ♭ = (W ♭ , (≡ ♭ X ) X⊆ fin Atm0 , V ♭ ) as follows

It is easy to check that M ♭ is indeed a DM and (M ♭ , s 0 ) |= φ.

For the other direction, given a DM W, (≡ X ) X⊆ fin Atm0 , V and w 0 ∈ W s.t. (M, w 0 ) |= φ, we construct a CM C ♯ = (S ♯ , f ♯ ) as follows

A.3 Proof of Theorem 2

Proof. The proof is conducted by constructing the canonical model.

Definition 19 (Theory).

A set of formulas Γ is said to be a BCL-theory if it contains all theorems of BCL and is closed under MP and Nec [∅] . It is said to be a consistent BCL-theory if it is a theory and ⊥ / ∈ Γ. It is said to be a maximal consistent BCL-theory (MCT for short), if it is a consistent theory and for all consistent theory Γ ′ , if Γ ⊆ Γ ′ then Γ = Γ ′ .

Lemma 1 (Lindenbaum-type). Let ∆ be a consistent BCL-theory and φ / ∈ ∆ Then, there is a maximal consistent BCL-theory Γ s.t. ∆ ⊆ Γ and φ / ∈ Γ.

The proof is standard and omitted (see, e.g. [5, p. 197] ).

Definition 20 (Canonical model). The canonical decision model

) is defined as follows

We omit the superscript c whenever there is no misunderstanding.

∈ Γ, then by the maximality of Γ and Red [∅] , we have

Since Γ is maximally consistent, there is exactly one Z ⊆ X s.t. cn Z,X ∈ Γ. By MP we have [∅](cn Z,X → φ) ∈ Γ, and by K [∅] and MP we have φ ∈ Γ. But than Γ is inconsistent, since φ∧¬φ ∈ Γ. Hence the supposition fails, which means [X]φ → φ ∈ Γ.

Lemma 3. The canonical model M is indeed a decision model.

Proof. Check the conditions one by one. For C1, we need show Γ ≡ c X ∆, if ∀p, p ∈ V (Γ) ∩ X implies p ∈ V (∆). Suppose not, then w.l.o.g. we have some q ∈ V (Γ) ∩ X, q / ∈ V (∆), by maximality of ∆ namely ¬q ∈ ∆. However, we have [q]q ∈ Γ, for q → [q]q is a theorem, and by definition of ≡ c X , [q]q ∈ ∆, hence q ∈ ∆, since [q]q → q ∈ ∆. But now we have a contradiction. C2-4 hold obviously due to axioms AtLeast, AtMost, Def and Funct respectively.

The proof is following the same line in e.g. [5, p. 198-199] and omitted.

Proof. By induction on φ. We only show the interesting case when φ takes the form [X]ψ.

For

For =⇒ direction, suppose not, namely [X]ψ / ∈ Γ. Then consider a theory

Now the completeness of DM w.r.t. BCL is a corollary of Lemma 3 and 5.

A.4 Proof of Theorem 3

Proof. Let W, (≡ X ) X⊆ fin Atm0 , V be a QDM and

Let sf (φ) be the set of all subformulas of φ and let sf

M ′ is indeed a filtration. We need show that it satisfies the two conditions.

1

Moreover, M ′ is a finite-QDM. For C1 it is given as the definition of V ′ . C2 and C3 hold because of sf + (φ) = sf (φ) ∪ Dec.

Finally, we need prove (M,

Then by definitions of V ′ and ≃ we have w 0 ≡ X v, by induction hypothesis (M, v) |= ψ.

A.5 Proof of Theorem 4

Proof. The right to left direction is obvious since any finite-DM is a finite-QDM. For the other direction, suppose there is a finite-QDM W, (≡ X ) X⊆ fin Atm0 , V and w ∈ W s.t. (M, w) |= φ. Since Atm 0 is infinite, we can construct an injection ι : W -→ Atm 0 \ Atm(φ). Then, we construct a finite-DM

It is easy to check that M ′ is indeed a finite-DM. By induction we show that (M ′ , w) |= φ. When φ is some p, we have V (w) = V ′ (w) since the injection ι has nothing to do with φ. The case of t(c) is the same. The Boolean cases are straightforward. Finally when φ takes form [X]ψ. Again since ι does not change valuation in φ, we have ∀v

A.6 Proof of Theorem 7

Proof. Suppose Atm 0 is finite and fixed. In order to determine whether a formula φ is satisfiable for the class CM, we are going to verify whether φ is satisfied in each CM, by doing this sequentially one CM after the other. The corresponding algorithm runs in polynomial time in the size of φ since: (i) there is a finite, constant number of CMs and (ii) model checking for the language L(Atm) relative to a pointed CM is polynomial. This means that, when Atm 0 is finite and fixed, satisfiability checking has the same complexity as model checking. Regarding (i), the finite, constant number of CMs in the class CM is S⊆2 Atm 0 |Val | |S| . Indeed, for every S ⊆ 2 Atm0 , we consider the number of functions from S to Val . Regarding (ii), it is easy to build a model checking algorithm running in polynomial time. It is sufficient to adapt the well-known "labelling" model checking algorithm for the basic multimodal logics and CTL [START_REF] Clarke | Model checking[END_REF]. The general idea of the algorithm is to label the states of a finite model step-by-step with sub-formulas of the formula φ to be checked, starting from the smallest ones, the atomic propositions appearing in φ. At each step, a formula should be added as a label to just those states of the model at which it is true.

A.7 Proof of Theorem 8

Proof. As for NEXPTIME-hardness, in [START_REF] Grossi | The ceteris paribus structure of logics of game forms[END_REF] the following ceteris paribus modal language, noted L CP (Prop), is considered with Prop a countable set of atomic propositions:

where p ranges over Prop and X is a finite set of atomic propositions from Prop. Formulas for this language are interpreted relative to a simple model S ⊆ 2 Atm0 and a state s ∈ S in the expected way as follows (we omit boolean cases since they are interpreted in the usual way): (S, s) As for membership, let tr be the following translation from the language L(Atm) to the language L CP Atm 0 ∪ {p t(c) : c ∈ Val } :

By induction on the structure of φ, it is routine to verify that φ ∈ L(Atm) is satisfiable for the class QDM of Definition 9 if and only if [∅] φ 1 ∧ φ 2 ∧ tr(φ) is satisfiable for the class SM of simple models, with

Hence, by Theorem 5 we have that, when Atm 0 is countably infinite, φ ∈ L(Atm) is satisfiable for the class CM of classifier models if and only if [∅] φ 1 ∧ φ 2 ∧tr(φ) is satisfiable for the class SM of simple models. Since the translation tr is linear and satisfiability checking for formulas in L CP Atm 0 ∪ {p t(c) : c ∈ Val } relative to the class SM is in NEXPTIME in the infinite-variable case [17, Lemma 2 and Corollary 1], checking satisfiability of formulas in L(Atm) relative to the class CM is in NEXPTIME too, with Atm 0 countably infinite.

A.8 Proof of Theorem 9

Proof. NP-hardness follows from the NP-harndess of propositional logic.

In order to prove NP-membership, we can use the translation given in the proof of Theorem 8 to give a polynomial reduction of satisfiability checking of formulas in L {[∅]} (Atm) relative to CM to satisfiability checking in the modal logic S5. The latter problem is known to be in NP in the infinite-variable case [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF].

A.9 Proof of Proposition 3

Proof. For the right direction, we have closest C (s,φ,X) ⊆ ||ψ|| C from the antecedent. Suppose towards a contradiction that the consequent does not hold. Then, ∃k ∈ {0, . .

which contradicts the antecedent. To see that, notice the second conjunct is because of (C, s * ) |= φ ∧ ¬ψ, and the first conjunct because of sim C (s,s * ,X) = k * and s * ∈ closest C (s,φ,X).

A.10 Proof of Proposition 4

Proof. The first validity is obvious, since