In this article we propose an extension to the typed natural deduction calculus TNDPQ to model verification of individual fairness and intersectionality in probabilistic classifiers. Their interpretation is obtained by formulating specific conditions for the application of the structural rule of Weakening. Such restrictions are given by causal labels used to check for conditional independence between protected and target variables. 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 individual 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). 1We 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 .
JX | ∀( : ∈ X ∧ : ∈ X
→ = )} Σ = { A ∪ X | A ∈ ΣA ∧ 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. In this paper, we focus only on the atomic fragment and provide a criterion to verify individual fairness for a probabilistic classifier via structural properties. Moreover, we address the issue of intersectionality, showing a solution through an extension of the original language with causal relations.
Individual fairness has diferent non-equivalent definitions in the literature. A first simplified characterization of individual fairness is as follows: Definition 2.1 (Individual Fairness (IF)). A classifier is individually fair regarding a set of protected attributes if it gives the same outputs to Data Points difering only for the values of those attributes. Formally, f̂︀ is IF regarding the set of protected attributes {1, . . . , } if for every X ∈ ΣX and pair of n-tuples of values 1 , . . . , and 1 , . . . , , f̂︀( X, : 1 , . . . , : ) = f̂︀( X, : 1 , . . . , : ). 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.
Given definition 2.1, in TNDPQ a classifier is IF regarding the set of protected attributes {1, . . . , } if the ground sequents describing the classifier are such that X, : 1 , . . . , : ⃒⃒ ∼ : if X, : 1 , . . . , : ⃒⃒ ∼ : , for every ∈ V, , ∈ V , and X ∈ ΣX.
We consider IF as the best way of approximating fairness through unawareness when we have to evaluate opaque systems: Definition 2.2 (Fairness through Unawareness (FtU)). A classifier is fair through unawareness regarding a protected attribute as long as this attribute is not explicitly used in the decision-making process.
Indeed, while FtU is clearly an intensional notion, which can be properly evaluated only by looking at the implemented program, IF can be evaluated just by looking at the inputs and outputs of the machine. For this reason, we cannot directly evaluate FtU for opaque systems, and IF emerges as a good substitute.
However, there is a problem. Although intersectionality holds for FtU, it fails for IF.3 Observation 2.1 (Intersectionality fails for IF). A classifier that is IF with respect to protected attribute 1 and protected attribute 2 (separately) may not be IF regarding the set {1, 2}.
Proof. To prove failure of intersectionality, we just have to show that for some classifier f̂︀, for every X ∈ ΣX, for every pair of values 1 and 1 in V1 , and for every pair of values 2 and 2 in V2 f̂︀( X, 1 : 1 ) = f̂︀( X, 1 : 1 ) f̂︀( X, 2 : 2 ) = f̂︀( X, 2 : 2 ) but for some pair of sets of values 1 , 2 and 1 , 2
f̂︀( X, 1 : 1 , 2 : 2 ) ̸= f̂︀( X, 1 : 1 , 2 : 2 ) We will show that such a classifier is not only theoretically possible, but even quite common when ML systems are trained using Data Sets of a specific kind.
For simplicity, assume that 1 and 2 have only two possible outputs each (respectively 11 and 12 , and 21 and 22 ). Let us consider an ML system implementing a learning algorithm with no restriction on protected attributes. The system is not FtU regarding these attributes, but can be IF if it is trained using a fair Data Set: that is, a Data Set in which all the Data Points sharing the same value of the non-protected attributes but possibly difering for those of 1 or 2 share the same value of the target variable. In our case, let us assume that the Data Set is fair in this sense and focus on the specific Data Points in table 1: these are all the Data Points that satisfy a specific X ∈ ΣX, with the ratio expressing how many of them give value to target variable . We can observe, by looking at the table, that the Data Points are fair when 1 and 2 are considered separately, and biased when 1 and 2 are considered together. Hence, the ML system will not learn to be IF regarding {1, 2}. As an example: X, 1 : 11 , 2 : 21 ⃒ ⃒ ∼
: 0.90 X, 1 : 11 , 2 : 22 ⃒⃒ ∼ : 0.75 Note that a diferent probability associated with just one value of is suficient to disprove IF for the set of variables {1, 2} and so the proof is complete.
Lack of intersectionality is even more serious than it could seem. Indeed, if intersectionality fails,
fairness can be gerrymandered by cherry picking protected attributes, so this property contributes to
make IF relevant even if the focus is only on single protected attributes [
Since IF and intersectionality require that the probability of a sequent does not change when diferent values are attributed to protected variables, both these properties can be seen as equivalent to a restricted rule of Weakening:4
|∼ : * (2) , : |∼ : Hence, since TNDPQ is non-monotonic, we need to provide the condition under which this rule is valid, in order to deal with IF and intersectionality. As an example, the following inference establishes IF regarding the protected attribute gender (variable .) and an instance of intersectionality in case also marital status ( ) is considered protected: : 27, : + , . : ℎ⊥ ⃒⃒ ∼ : 27, . : , : + , . : ℎ⊥ ⃒⃒ ∼ ( : | : , ) = ( : | ) Therefore, what we need is a criterion of conditional independence.
In a logic that ignores the relations between the elements of , conditional independence can be
decided only using brute-force methods, i.e. by checking statistical correlations for all values of any
variable. Moreover, we have no way of distinguishing good correlations from spurious ones which may
emerge due to biases in the Training Set. In contrast, a system extended with the basic vocabulary of
causal graphs [
Two nodes which are one the immediate cause of the other are mutually dependent. While for two
nodes which are not directly connected, dependence is defined in three steps [
To express the criteria for conditional independence and thus for the applicability of the rule of
Weakening, we need to internalize the causal notions in our calculus TNDPQ. For this purpose, we use
the methodology of labeled calculi [
j i j k i k (a) Chain: and are depen- (b) Fork: and are dependent, dent, but independent condi- but independent conditional tional on . on .
k j (c) Collider: and are dependent conditional on or any of its descendant, independent otherwise. Path with Intermediate Nodes ♢ = a path exists between and passing through non-colliders and colliders or sets of their descendants . then, we reformulate TNDPQ sequents by extending their left-hand side with causal relations: ◁f̂︀ , ⃒⃒⃒ ∼ : (3) 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 existing paths in the resulting graph and is derivable as the closure of ◁f under the rules in table 2.
̂︀
To see how these rules work, consider the figure 2. The rules for mediate causal relations are used to identify the descendants of colliders. In this case, applying reflexive cause and transitive cause we obtain: 1 ▶{1,1,1} 1, 3 ▶{3,3,3} 3, and 3 ▶{3,3,3} 3. The rules chain, fork, and collider are used to represent triplets of nodes between and , with the rule for collider representing also the descendants. Chains and forks are stored in the superscript: 1 ♢ {2} 3, 3 ♢ {4} . The colliders are stored in the subscript, together with the set of their descendants: ♢ {1,{1,1,1}} 2, 2 ♢ {3,{3,3,3}} 4, and 2 ♢ {3,{3,3,3}} 4.5 Transitivity is used to combine these triplets to construct the paths between and . In this case, we have two paths: ♢ {{21,,4{}1,1,1},3,{3,3,3}} , and ♢ {{21,,4{}1,1,1},3,{3,3,3}} .6 Note that in this calculus variables play the same role as labels in labeled calculi, with ◁f making ̂︀ explicit accessibility relations. As an example, the sequent expressing that the probability that a 27 years old person with a gross annual income of 40.000 receives a loan is 60%, is formulated as follows: ◁ , ◁ , ◁ , ◁ , : 27, : 40 |∼
With these technical tools in place, we formulate an applicability criterion for the Weakening rule in equation 4: 5Notice that the collider occurs both by itself and in the set of its descendants: its occurrence as collider is needed for the rule of transitivity, and its occurrence in the set of its descendants is needed for the condition of applicability of the rule (4). 6We focus only on the maximal sets of descendants, although technically also the paths containing only some of the descendants are constructible. Notice that this does not cause problems with the conditions of rule (4). Collider ◁ , ◁ , ▶ ⊢ ♢ {,}
Transitivity* ♢ , ♢ ⊢ ♢ ∪∪ ⃒ ◁f̂︀ , ⃒⃒ ∼
⃒ ◁f̂︀ , , : ⃒⃒ ∼ Condition1: ̸ ◁ and ̸ ◁ ; Condition2: For every ♢ in ♢ f̂︀ , either ∩ ̸= ∅ or ∃ ∈ (∃ ∈ ∧ ∩ = ∅). Hence, to decide whether Weakening can be applied, we check both ◁f and ♢ f to evaluate conditional independence. In particular, the first condition requires that protected̂︀variablê︀and target variable are not one the direct cause of the other, and the second condition requires that, for every path connecting them, blocks it, by containing at least one non-collider or by not containing a collider and all of its descendants. Note that this rule can be used to decide both IF in general and intersectionality, which corresponds to cases in which already contains a protected attribute. More precisely, what is obtained by checking the admissibility of an instance of Weakening is an evaluation of fairness (and possibly intersectionality) of the classifier, when a specific set of attributes are used to decide a target variable. Figure 3 shows a simple example of application of this rule.
Age
GAI
◁f̂︀ , : 27, : 40 ⃒⃒⃒ ∼ ◁f̂︀ , : 27, : 40, : ⃒⃒⃒ ∼
(b) Application of with attribute receving value (married).
The satisfaction of the conditions can be observed from the causal graph, and is derivable from the set ◁f̂︀.
This work focuses on formal tools to check fairness of probabilistic classifiers. We have shown that, without taking into account the causal relations between the features of the classifier, intersectional fairness is not guaranteed. The proposed typed natural deduction calculus TNDPQ has labels representing causal relations, and it provides a criterion of applicability for the rule of Weakening that establishes both fairness and intersectionality. An extension using causal labels to express counterfactual fairness is left for further work.
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.