A Proof System with Causal Labels (Part I): checking Individual Fairness and Intersectionality

TL;DR

The paper tackles verifying individual fairness and intersectionality in probabilistic classifiers for opaque systems. It extends the TNDPQ proof system with causal labels and a conditional-independence based Weakening criterion, encoding causal relations via predicates and a path calculus to decide when Weakening is admissible. This yields a formal method to check IF and intersectionality on data points $\sigma$ through ground sequents and a causal graph, with the key independence condition $P(t:\delta \mid a:\alpha, \sigma) = P(t:\delta \mid \sigma)$. The authors demonstrate that ignoring causal structure can break intersectionality and propose this as a principled approach to fairness verification, with extensions to counterfactual fairness discussed for future work.

Abstract

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.

Figures (3)

• Figure 1: Elementary compositions of nodes in causal graphs and criteria of conditional independence.
• Figure 2: Paths between nodes $a$ and $t$.
• Figure 3: Example of application of Weakening.

Theorems & Definitions (5)

• Definition 2.1: Individual Fairness (IF)
• Definition 2.2: Fairness through Unawareness (FtU)
• proof
• Definition 3.1: Conditional Independence
• Definition 3.2: Causal Graph