In this article we propose an extension to the typed natural deduction calculus TNDPQ to model verification of counterfactual fairness in probabilistic classifiers. This is obtained formulating specific structural conditions for causal labels and checking that evaluation is robust under their variation. The calculus TPTND (Trustworthy Probabilistic Typed Natural Deduction [1, 2]) is designed to evaluate post-hoc the trustworthiness of the behavior of opaque systems. The system is implemented for verification of dataframes in the tool BRIO [ 3, 4]. In [5], we introduced TNDPQ (Typed Natural Deduction for Probabilistic Queries), a variation of the previous system in which a probabilistic output is associated to a target variable when a Data Point - consisting of a list of values attributions for a set of variables - is provided. In this paper, we extend this system with tools to verify counterfactual fairness of classifiers. We start with a formal definition of classifiers. Let A be a set of protected variables 1, . . . , , X be a (disjoint) set of non-protected variables 1, . . . , and be a target variable. Moreover, let V be a set of values 1 , 2 , . . . , that can receive, V the set of all V , V be a set of values 1 , 2 , . . . , that can receive, V the set of all V , and V the set 1, 2, . . . , of values that can receive. Let us use 1, . . . , to denote elements of A ∪ X (that is, variables regardless of their protected or unprotected status), and 1 , . . . , to denote the values that can receive. We use : (respectively : ) to express the judgment that variable receives value (respectively, variable receives value ), and : 11 , . . . , to express the probabilistic judgment that 1, . . . , are all the possible values that variable can receive and that, for 1 ≤ ≤ , it receives value with probability .1 We use JA for the set of all the judgments about protected variables, JX for the set of all the judgments about non-protected variables, and JP for the set of all probabilistic judgments. Moreover, we use A to express a set of judgments about protected variables such that each element of A receives at most one value, X to express a set of judgments about non-protected variables such that each element of X receives at most one value, ΣA to refer to the set of all A, and ΣX to refer to the set of all X. is used to express the union of a A and a X, and Σ is used to refer to the set of all . More formally:
ΣA = { A ⊆
JA | ∀( : ∈ A ∧ : ∈ A → = )} 7th International Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis (OVERLAY 2025), October 26, 2025, Bologna, Italy * Corresponding author. †These authors contributed equally. $ leonardo.ceragioli@unimi.it (L. Ceragioli); giuseppe.primiero@unimi.it (G. Primiero) 0000-0001-5250-9720 (L. Ceragioli); 0000-0003-3264-7100 (G. Primiero)
© 2025 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). 1 We assume that the values for (also for the elements of A and X but this is irrelevant here) are all mutually exclusive, and so ∑︀
=1 = 1. Note that we make no assumption regarding whether ∈ A ∪ X and so on whether V = V or V = V for some . ΣX = { X ⊆
JX | ∀( : ∈ X ∧ : ∈ X A classifier f̂︀ ∈ F̂︀ is a function from Σ to JP, where each ∈ Σ describes a Data Point, that is what we know about a subject, and the probabilistic judgment : 11 , . . . , in JP represents the output of the classifier regarding the probability distribution of the possible values for the target variable .
TNDPQ is a proof system working with sequents describing the result of queries for classifiers. More
precisely, each classifier f̂︀ is characterized by a set of ground sequents of the form:2
|∼
For readability reasons, the sequents focus on only one possible value for the target variable at a time. In
[
TNDPQ was initially designed to investigate the preservation of trustworthiness under the
composition of logically simpler queries and then extended with causal labels to verify individual and
intersectional fairness for a probabilistic classifier via structural properties, see [
Counterfactual fairness requires that a subject would not have been treated diferently had their
protected attributes been diferent [
As an example, we could wonder whether the probability of receiving a loan in the previous example would have still been 60%, had the subject been a woman? If we do not consider the connections between the features, this question just corresponds to whether or not the following sequent is derivable in the system:3 : 27, . : , : + , . : ℎ⊥, : 65 ⃒⃒⃒ ∼ However, when causal relations are taken into account, it is a trivial observation that gender influences other features (both directly and indirectly). For example, both through objective physical diferences and prejudices, gender influences job opportunities, and therefore the counterpart of a subject having a diferent gender would probably not have the same . This makes the individuation of the Data Point ′ a lot more complicated.
Hence, assessing counterfactual situations CF requires some more precise formal tools. The usual
approaches are: possible worlds semantics [
MS: div
(b) Graph of Counterfactual Data Point after intervention assigning to .
(a) Graph of Factual Data Point
We first consider how counterfactual situations are dealt with in causal models, and then internalize both causal relations and the characterization of counterfactuals in our calculus TNDPQ. For the purposes of this work, we define causal graphs as follows: Definition 3.1 (Causal Graph). A causal graph is an acyclic directed graph with nodes representing events (variables receiving values) and edges representing immediate causal relations.
By closing edges under transitivity, we obtain the notion of mediate cause. For purely formal reasons, we close the notion of cause under reflexivity as well. The usual extension of deterministic causal graphs with functions to compute the value of a node on the basis of those of all the immediate parent nodes is here expressed by sequents like in equation 1.4
As already shown, to capture counterfactuals one cannot just change the protected attribute and leave
all other variables fixed: the properties of the subject that do not depend on the protected variable need
to be identified and kept fixed. For this, the usual approach (followed, for example, in [
According to this usual approach, the protected variable can be either exogenous (such as gender) or endogenous (such as marital status, which, for example, depends on gender: there are more widows than widowers). When the protected variable is endogenous, we erase all the edges that enter it, since we want to assign its value ad arbitrium.
In summary, to capture counterfactual situations, the usual approach prescribes to intervene on the
graph as follows [
1. impose some value to the protected variable; 2Technically, we should add a subscript in the equation specifying the classifier we are focusing on. However, this will not be needed here, since we will not compare outputs of diferent classifiers. 3Note that this would make counterfactual and individual fairness indistinguishable from one another. 4However, note that in causal models the function does not assign value in a probabilistic way and probabilities come in play only at a later stage. On the contrary, our equations are probabilistic in the strictest sense.
2. keep all the (other) exogenous variables fixed; 3. erase all the edges that enter in the protected variable; 4. calculate the values of the endogenous variables (particularly of the target), using those of the exogenous variables.
The third point is relevant only when the protected variable is not exogenous; otherwise, it is vacuously satisfied. Now, to check CF we just need to control whether the resulting value of the target variable is the same.
We slightly modify this approach to apply it to ML classifiers. The assignment of a value to the target variable depends on the selection of a set of exogenous variables, so we have to be sure to work with an adequate set of such variables. Moreover, while in causal models we can require to have a suficiently vast set of exogenous variables, we cannot ask the same regarding the set of entries of a classifier, which we cannot change. For this reason, instead of relying only on the exogenous variables, we will use all and only the variables that are not (direct or indirect) efects of the protected one, and ignore all the others. This will allow to use all the factual information that remains valid in the counterfactual situation in order to derive the counterfactual classification. An example of the graphs corresponding to a factual and a counterfactual Data Point is shown in figure 1.
To express the fact that a Data Point is the counterfactual of another, we need to internalize both causal
relations and interventions in our calculus TNDPQ. For this purpose, we use the methodology of labeled
calculi [
Mediate Causal Relations ▶ = is a mediate cause of , with intermediate causes . Intervention on Data Point [◁f , ]( : ) = an intervention assigning the value to variable is operated on the Data Pô︀int and its associated graph ◁f.5 ̂︀ Then, we reformulate TNDPQ sequents by extending their left-hand side:
◁f̂︀ , ⃒⃒⃒ ∼ : [◁f̂︀ , ]( : ) ⃒⃒⃒ ∼ : (2)
Let us use to indicate the set of variables that occur in . We use ◁f to indicate all the immediate causal relations among features in the classifier. ▶f denotes all the mêd︀iate causal relations in the resulting graph and is derivable as the closure of ◁f û︀nder reflexivity and transitivity. We will ̂︀ use ◁′f̂︀ and ▶′f̂︀ respectively for diferent sets of direct and indirect causal relations. Hence, the first sequent of equation 2 is a sequent that gives an output for the target in the actual situation (that is, ), also specifying the immediate causal relations that hold between the features of the classifier ( ◁f), ̂︀ while the second is a hypersequent that gives an output for the target in the counterfactual situation resulting from ◁f , by the intervention that assigns to . We call the variable of intervention. Although ◁f is n̂︀ot actually used by the classifier to evaluate , it is relevant in the calculus to check whether a D̂a︀ta Point is the counterfactual of another.
Example 1 (Factual and Counterfactual sequents). The following sequents express, respectively, that the probability of receiving a loan for a 27 years old person with a gross annual income of 40.000 is 60%, and that it would have been 50% had them been 35 years old: ◁ , ◁ , ◁ , ◁ , : 27, : 40 |∼ 5Notice that we focus on interventions on protected variables, although interventions on unprotected variables could also be studied. While sequents describing actual decisions of a classifier, such as the one on the left of equation 2, are assumptions of TNDPQ, those describing counterfactual decisions, such as the one on the right of the equation, are derivable. To derive them, we start with a plausible sequent for the counterfactual, which can be obtained using only the features that do not depend on the variable of intervention to run the classifier:
◁′f̂︀ , ′ ⃒⃒⃒ ∼ : Let us call this the counterfactual candidate. Then, we apply the rule C-Weakening in table 1, adding [◁f̂︀ , ]( : ). The resulting hypersequent [◁f̂︀ , ]( : ) ◁′f̂︀ , ′ ⃒⃒⃒ ∼ : can be interpreted as saying that the classifier assigns probability to the value assignment : for the Data Point ′, which we regard as a counterfactual candidate for the Data Point after intervention assigning to the value . The formulas ◁f̂︀ and ◁′f̂︀ represent, respectively, the graph describing the causal relations between the variables of the classifier and the same graph after the intervention.
If ◁′ , ′ is really the counterfactual of ◁f, after intervention ( : ), by applying the rules of Cut f̂︀ ̂︀ in table 1 we end with a sequent of the form: ⃒ [◁f̂︀ , ]( : ) ⃒⃒ ∼ : More precisely, the rule -Cut erases : from the premise, that is, the value assignment to the protected variable imposed by the intervention. Hence, if the counterfactual candidate contains : , it can be erased. The rule ◁-Cut erases ◁ , under the condition that ̸= , enabling the erasure of all direct causal relations that do not enter the protected variable. The rule -Cut erases : , that is, the assignment of value given to by the original Data Point, under the condition that is not a consequence of . This is established by checking ▶f, that is, the set of mediate causal relations resulting from the graph before intervention. Hence, all t̂h︀ e assignments of values to the variables that are not consequences of the protected variable in the original graph can be erased.
The label of these rules refers to the fact that they can be seen as contractions of Cut applications of the following kind:6 [◁′f̂︀ , ′]( : ) ⃒⃒⃒ ∼
⃒ : 1 ◁f̂︀ , , : ⃒⃒ ∼
⃒ [◁′f̂︀ , ′]( : ), ◁f̂︀ , ⃒⃒ ∼ : Where the first premise says that in the counterfactual Data Point obtained from ◁′f , ′ by the interven̂︀ tion ( : ), variable receives the value with probability 1 (that is, with certainty), and the second premise gives the probability of : in the counterfactual candidate. ◁-Cut and -Cut are contractions of similar Cut applications. 6See note 1 for the occurrence of as target variable.
If by applying all these rules we can erase all the formulas in the counterfactual candidate, then this is really the Data Point corresponding to the counterfactual of the factual Data Point. Now, all we have to do to check CF is to compare the probabilities and . This can be done either by requiring their identity or by requiring a threshold on their diference.
Example 2 (Evaluation of CF for a classifier) . Let us use ◁f for the causal relations resulting from graph ̂︀ (a) of figure 1 and ◁′f for the causal relations resulting from graph (b) of the same figure. Moreover, let us ̂︀ assume that the following sequent describe decisions of a classifier: ◁f̂︀ , . : , : , : 1100, : 65, . : ℎ, : 5 ⃒⃒⃒ ∼ [◁f̂︀ , . : , : , : 1100, : 65, . : ℎ, : 5]( : ) ⃒⃒⃒ ∼ The derivation can be constructed as follows, using [. . .] for [◁f , . : , : , : 1100, : ̂︀ 65, . : ℎ, : 5] and relying only on the rules in table 1:
◁′f̂︀ , . : , : , : 1100, . : ℎ ⃒⃒⃒ ∼ : 0.60 [. . .]( : ), ◁′f̂︀ , . : , : , : 1100, . : ℎ ⃒⃒⃒ ∼ : 0.60 [. . .]( : ), ◁′f̂︀ , . : , : 1100, . : ℎ ⃒⃒⃒ ∼ : 0.60 ◁-Cut [. . .]( : ) , . : , : 1100, . : ℎ |∼ : 0.60 C-W -Cut [◁f̂︀ , . : , : , : 1100, : 65, . : ℎ, : 5]( : ) ⃒⃒⃒ ∼ : 0.60 -Cut Moreover, since the probability that the variable receives value is the same in both sequents, this application of the classifier satisfies CF.
This work focuses on formal tools to check counterfactual fairness of probabilistic classifiers. We have seen how causal models allow to formalize counterfactuals, and argued that a modified version of their approach is suitable to test fairness for classifiers. We have proposed a typed natural deduction calculus TNDPQ extended with labels representing causal relations and expressions for interventions to internalize this approach.
This research was supported by the Ministero dell’Università e della Ricerca (MUR) through PRIN 2022 Project SMARTEST – Simulation of Probabilistic Systems for the Age of the Digital Twin (20223E8Y4X), and through the Project “Departments of Excellence 2023-2027” awarded to the Department of Philosophy “Piero Martinetti” of the University of Milan.
During the preparation of this work, the authors used Grammarly in order to: Grammar and spelling check. After using these tool, the authors reviewed and edited the content as needed and take full responsibility for the publication’s content.