Balancing Reconstruction and Editing Quality of GAN Inversion
for Real Image Editing with StyleGAN Prior Latent Space

Kai Katsumata

The University of Tokyo, Japan

Duc Minh Vo

The University of Tokyo, Japan

Bei Liu

Microsoft Research Asia, China

Hideki Nakayama

The University of Tokyo, Japan

The exploration of the latent space in StyleGANs and GAN inversion exemplify impressive real-world image editing, yet the trade-off between reconstruction quality and editing quality remains an open problem.
In this study, we revisit StyleGANs' hyperspherical prior $\ZS$ and $\ZPS$ and
integrate them into seminal GAN inversion methods to improve editing quality. Besides faithful reconstruction, our extensions achieve sophisticated editing quality with the aid of the StyleGAN prior.
We project the real images into the proposed space to obtain the inverted codes, by which we then move along $\ZPS$, enabling semantic editing without sacrificing image quality.
Comprehensive experiments
show that $\ZPS$ can replace the most commonly-used $\WS$, $\WPS$, and $\SSp$ spaces while preserving reconstruction quality,
resulting in reduced distortion of edited images.

§ INTRODUCTION

The combination of GAN inversion [1, 2, 7, 5, 15, 25, 14, 29, 3, 28] and latent space editing [16, 6, 18] enables us to edit a wide range of image attributes such as aging, expression, and light condition, by applying editing operations [16, 6, 18] to inverted latent codes.
To this end, many methods
[1, 2, 7, 5] aiming to find the latent code of StyleGANs [11, 12, 9, 10] that generates a given image have been developed. Recent efforts [21, 7, 5, 22] improves
reconstruction quality of both in-domain and out-of-domain images.

One of remaining challenges of GAN inversion is the trade-off between reconstruction quality and perceptual quality of the edited images.
Popular latent spaces such as $\WS$ [12], $\WPS$ [1], and $\SSp$ [22] improve reconstruction quality, yet the low-quality edited image is unavoidable.
Recent attempts (, SAM [14], PTI [15], and $\PS$ [30]) aim to maintain the perceptual quality during semantic editing.
However, since they use transformed spaces such as $\WS$ or $\WPS$, namely unbounded space with unknown boundaries, the shape of such space is too complex to edit.
Such an unbounded embedding space cannot guarantee that the edited embedding is always present in the embedding space, resulting in distortion after editing.
Unlike typically used spaces, StyleGAN's prior space $\ZS$ is a bounded embedding space, meaning that it is rich in editing quality while poor in reconstruction quality.
To address the mentioned challenge, one solution is to flexibly use the rich embedding space and the original latent space, which is our main target.

To begin with, we revisit the original latent space $\ZS$, which can be easily editable. Since the latent code $\z \in \ZS$ is sampled from the hypersphere,
the latent code can move on $\ZS$ with closed operations.
To maintain the reconstruction quality while leveraging the robust nature of $\ZS$, we first extend $\ZS$ to $\ZPS$ and then combine $\ZPS$ with a feature space $\FS$ in the output of an intermediate layer in the StyleGAN generator, proposing an alternative space namely $\FZS$.
Our proposed $\FZS$ space achieves excellent reconstruction performance due to the use of the feature space $\FS$ and increases editing quality with the aid of the hyperspherical prior of the original latent space $\ZPS$, simultaneously. Here, editing quality denotes the perceptual quality of images after performing editing operations in the latent space.

Qualitative and quantitative evaluations show that our method maintains image quality after performing editing operations without sacrificing reconstruction quality.
We futher demonstrate that the our method can be applied to many cutting-edge GAN inversion methods.

$\mathcal{F}/\mathcal{W}^{+}$ space [7]

$\mathcal{F}/\mathcal{Z}^{+}$ space (ours)

Latent spaces of StyleGANs. The space $\FWS$
leads to the faithful reconstruction. Using $\ZPS$ instead of $\WPS$, $\FZS$ does not sacrifice reconstruction quality with the aid of $\FS$.
The base code $\f$ is an intermediate output of the StyleGAN generator with spatial dimensions, and
the detail code $\wmpls$ or $\zmpls$ is a subset of
$\wpls$ or $\zpls$ and the inputs of the upper stages of the generator. The optimizing codes are highlighted in blue.

§ APPROACH

In this section, we first review various latent spaces for GAN inversion
and their pros and cons.
Then, we introduce the integration of $\ZPS$ into cutting-edge GAN inversion methods for improving editing quality while maintaining reconstruction quality.

§.§ Analysis of StyleGAN Spaces

LPIPS loss     0.05944     0.06785     0.06728     0.07973     0.09912

1.2em$\mathcal{F}\!/\!\mathcal{S}$ [26]

LPIPS loss     0.10868     0.07482     0.43191     0.12273     $\textbf{0.07196}$

LPIPS loss     0.06573     0.07567     0.08897     0.08939     0.11237

LPIPS loss     $\textbf{0.05315}$     $\textbf{0.06540}$     $\textbf{0.06563}$     $\textbf{0.07737}$     0.09158

Comparison of inverted images with different latent spaces.
$\FZS$ achieves high-quality reconstructions on par $\FWS$ and $\FSS$ qualitatively and quantitatively.

Quantitative comparison of reconstruction quality. Our $\FZS$ yields performance comparable to $\FWS(\PNS)$.

Space     $\mathcal{Z}$     $\mathcal{Z}^{+}$     $\mathcal{W}^{+} (P_N)$     $\mathcal{W}^{+}$
MSE     0.18149     0.12117      0.11965     0.04872

SSIM      0.61155     0.68930      0.68190     0.76101
Space     $\mathcal{F}\!/\!\mathcal{Z}$     $\mathcal{F}\!/\!\mathcal{Z}^{+}$ (Ours)    $\mathcal{F}\!/\!\mathcal{W}^{+} \!(P_N)$[7]      IDInvert[28]
MSE     0.02679     $\textbf{0.01742}$     $\textbf{0.01743}$     0.02155

SSIM     0.78965     $\textbf{0.81477}$       $\textbf{0.81479}$     0.64993

target     inversion     2|cdirection 1     2c|direction 2     target     inversion     2cdirection 1     2c|direction 2

Editing comparison with GANSpace directions. Although the spaces with $\WPS$ fail to preserve the structure of generated faces, our spaces properly preserve them.

$\ZS$ and $\ZPS$ Space.
The generator $G: \ZS \to \X$ learns to map a simple distribution, called latent space $\ZS$, to the image space,
where $\x \in \X$ is an image, and $\z \in \ZS$ is uniformly sampled from a hypersphere.
The primitive latent code of the StyleGAN family is with $512$ dimensions.

AgileGAN [19] and StyleAlign [23] employ the extended space $\ZPS$, which provides a different latent code from $\ZS$ for each layer.
AgileGAN [19] and StyleAlign [23] note that $\ZS$ and $\ZPS$
have high editing quality and low reconstruction quality, and they are not suit for GAN inversion.

$\WS$, $\WPS$, and $\SSp$ Space.
StyleGANs also use the intermediate latent space $\WS$ where each $\w \in \WS$ is transformed from $\z \in \ZS$ by using a mapping network.
Thereafter, [1, 2] introduced $\WPS$ space, achieving lower reconstruction loss by allowing to control of details of images.
Each element $\wpls$ in $\WPS$ is defined as $\wpls\! = \{\w_i\}_{i=1}^{N}$, where $\w_i\in\WS$, and $N$ is the number of layers in generator that takes $\w$
as input.
$\SSp$ space [22] is spanned by style parameters, which is transformed from $\w \in \WS$ using different learned affine transformations for each layer of the generator.

Although the spaces derive faithful reconstruction quality, distortions and artifacts may appear in edited images [24, 30, 19].
This is because the embeddings with these spaces for the images may not correspond appropriately to $\ZPS$, the StyleGAN prior,
and the space cannot guarantee that the edited latent code reaches the original space.

$\PPNS$ Space.
Zhu [30] introduced a normalized space $\PNS$ by whitening the logit output of the final linear layer of the mapping network.
Since the normalized space $\PNS$ can be approximated to Gaussian distribution,
penalizing the distance between the latent code and the mean of $\PNS$ locates the latent code to the high-density region.
It also can be extended to $\PPNS$ by using $\WPS$.
In the normalized spaces, editing operations are performed on $\WS$ or $\WPS$ space.

$\FWS$ and $\FSS$ Space. Kang [7] proposed $\FWS$ space
(<ref>), consisting of the $\FS$ and $\WPS$ spaces, and the space also investigated in SAM [14] and Barbershop [29].
The coarse-scale feature map $\f \in \FS$ is an intermediate output of a generator before taking detail codes $\wmpls = \{\w_i\}_{i=M}^{N}$.
An element $\fw = (\f, \wmpls)$ of $\FWS$ consists of a base code $\f$ and a detail code $\wmpls$.
The information of a noise input and bottom latent codes $\{\w_i\}_{i=1}^{M-1}$ is contained in $\f$, and $\f$ controls the geometric information.
Kang [7] uses $\PPNS$.
$\FSS$ space [26] combines $\FS$ and $\SSp$ [22].
Since they use unbounded spaces for latent editing, they have the issue of editing quality like $\WPS$.

$\FWS$ [7]

$\mathcal{F}\!/\!\mathcal{S}$ [26]

$\FWS$ [7]

$\mathcal{F}\!/\!\mathcal{S}$ [26]

Editing comparison with InterfaceGAN [17] directions.

Quantitative comparison of the identity similarity between target and edited images. Light-colored lines indicate the individual results. Deep-colored lines indicate the average similarity.
$\FZS$ shows high editing quality.

§.§ Overall Concept

Overall, there is still no existing latent space that can guarantee both reconstruction quality and editing quality. As discussed in [13, 30, 19, 24], leveraging $\ZS$ or $\ZPS$ spaces lead to high editing quality in exchange for reconstruction quality.
PULSE [13] discussed the importance of
considering a manifold of a latent space, which controls content quality. Following this discussion, Zhu [30] uses regularization on the deactivated $\WS$ becase they cannot use $\ZS$ space with sufficient reconstruction quality.
To greatly benefit from considering the latent manifold, we employ bounded latent codes. Since we know the shape of $\ZS$,
we completely utilize the information of the distribution of $\ZS$.
To overcome their limitations, we employ an auxiliary space to improve reconstruction quality while using $\ZPS$.
Since current cutting-edge GAN inversion methods still have over-capacity, we can replace their latent spaces
to $\ZPS$ without sacrifing reconstruction quality.

The space with $\ZPS$ has the desirable properties required for GAN inversion: high reconstruction quality and high editing quality.
The high reconstruction capacity of the space is attributed to the auxiliary space, and the high editing quality is attributed to the primitive space $\ZS$.

§.§ GAN inversion with Z+ space

To demonstrate the effectiveness of the use of $\ZPS$,
we replace $\WS$ or $\WPS$ in BDInvert [7], SAM [14], and PTI [15].
BDInvert [7] and SAM [14] use $\FWS$ space.
PTI [15] uses $\WS$ and fine-tunes the generator to enhance reconstruction quality and increase the density of the inverted neighborhood.
For example, for BDInvert [7] we replace $\FWS$ with $\ZPS$ and present the $\FZS$ space shown in <ref>.
The space $\FZS$ cosists of $\FS$ and $\ZPS$, and each elements $\fz \in \FZS$ is defined as $\fz = (\f, \zmpls)$, where $\zmpls = \{\z_i\}_{i=M}^{N}$.
To optimize a latent code along $\ZPS$ or $\ZS$,
we retract the latent codes to the surface of the hypersphere of radius $\sqrt{512}$ each iteration by using:

\begin{align}
\z_i = \sqrt{512}\z_i/|\z_i|,
\end{align}

where $\z_i \in \zmpls$. We follow the optimization algorithms of the base methods (, BDInvert, SAM, and PTI).

§ EXPERIMENTS

We evaluate the latent spaces from two aspects: reconstruction quality and editing quality.
For the reconstruction quality comparison, we verify that our space is not inferior to the compared spaces.
For the comparison of editing quality, we show that our space preserves the perceptual quality of edited images better than the other spaces.

Reconstruction quality comparison.
We first compare the reconstruction performance
using a StyleGAN2 model pre-trained on FFHQ [11].
<Ref> shows the reconstructed results and LPIPS loss for five benchmark images on the four compared latent spaces.
All methods reconstruct them well because $\FS$ magnifies the capacity of the latent space.
The LPIPS loss of our $\FZS$ space is comparable to that of $\FWS$.
<Ref> shows that the inverted images of $\FZS$ and $\FWS$ are almost the same as the target images.

For quantitative comparison,
<ref> reports the average of MSE loss and SSIM over 50 random images from CelebA-HQ [8].
The results of $\FZS$ are competitive with those of $\FWS(P_N)$, as shown by a non-inferiority test with a margin of $1\times10^{-8}$, yielding p-values of .002983 for MSE and .001609 for SSIM.
The $\FWS(P_N)$ space, however, results in less realistic edited images as seen later.

inversion     edited        inversion    edited

Edited results on the LSUN Cat dataset with StyleGAN1. Editing on our $\FZS$ space
preserves the image content (cat).

Editing quality comparison.
<Ref> shows editing results with
GANSpace [6].
For each direction, two images with intensities of -2 and 2 are plotted.
$\FWS(P_N)$ and $\FWS$ lack the image quality after performing editing operation (, lacking face parts or are adding waterdrops).
Meanwhile, our $\FZS$ and $\FZ$ spaces
consistently preserve image quality after semantic editing.
We also compare editing results with interfaceGAN. As shown in <ref>, we can see that our method relaxes
the distortions of edited images more than the competing methods.

Finally, we evaluate the editing quality quantitatively.
We use MTCNN [27] as face detector and InceptionResNet V1 [20] trained on VGGFace2 [4] as feature extractor.
To compute identity similarity, we use cosine similarity. For each method, we plot the identity similarities between the original inputs and the edited images with each editing step size in <ref>.
We plot 12 lines for each method (four targets $\times$ three directions).
The figure shows that our space preserves the identity of target images after editing with even a strong intensity unlike $\FWS(\PNS)$.
We also conduct the editing quality evaluation on 50 CelebA-HQ samples with five directions and eleven step sizes. The average identity similarity of $\FZS$ is 0.373, whereas that of $\FWS$ is 0.327.
It demonstrates that $\FZS$ maintains the perceptual quality of edited image well.

Editing comparison on another dataset.
We evaluate the effectiveness of $\FZS$ on another GAN model.
<Ref> shows the edited results with StyleGAN 1 pretrained on LSUN Cat.
Although $\FWS(\PNS)$ completely corrupts the cat's face in the edited image, our method maintains it.

LPIPS     $0.1249$     $0.1083$     $0.3031$      $0.1249$      $0.0638$

w/ $\ZPS$

LPIPS     $0.1095$     $0.0852$      $0.3017$     $0.1230$     $0.0626$

LPIPS     $0.2111$     $0.1169$     $0.3802$     $0.0809$     $0.0609$

w/ $\ZPS$

LPIPS      $0.1987$     $0.1247$      $0.3838$     $0.0793$     $0.0584$

Reconstruction comparisons on SAM and PTI. The 1st and 3rd rows are inverted results of PTI and SAM. The 2nd and 4th rows are results of the methods that use $\ZPS$ instead of $\WS$ or $\WPS$. It indicates we can replace original latent space to $\ZPS$ without loosing reconstruction quality to improve editing quality.

inversion     eyeglass     smile     0     inversion     eyeglass     smile

3cSAM [14] w/ $\ZPS$        3cSAM [14]

inversion    age    smile       inversion    age    smile

3cPTI [15] w/ $\ZPS$        3cPTI [15]

Editing comparison on SAM and PTI. By replacing $\WPS$ or $\WS$ to $\ZPS$ avoid harming perceptual quality of edited images.

Integration $\ZPS$ into other GAN inversion methods.
We further demonstrate the effectiveness of our $\ZPS$ space. <Ref> shows reconstructed images by PTI [15], SAM [14], and $\ZPS$ version of them. We can see that the use of $\ZPS$ on PTI and SAM does not sacrifice reconstruction performance.
<Ref> shows that integrating $\ZPS$ space into seminal GAN inversion methods relaxes editing distortions.

§ CONCLUSION

We revisit $\ZS$ space for GAN inversion to yield a better trade-off between reconstruction quality and editing quality. We integrate bounded latent space $\ZPS$ with the hyperspherical prior instead of $\WPS$ into the space with rich representative capacity, resulting in the presented space (, $\FZS$). Our thorough experiments on PTI, SAM, $\FWS$, and $\FSS$ demonstrate that we can preserve perceptual quality of edited images while maintaining sufficient reconstruction quality on par with baseline methods by replacing unbounded space (, $\WPS$) to $\ZPS$.

[1]
Rameen Abdal, Yipeng Qin, and Peter Wonka.
Image2stylegan: How to embed images into the stylegan latent space?
In ICCV, pages 4432–4441, 2019.

[2]
Rameen Abdal, Yipeng Qin, and Peter Wonka.
Image2stylegan++: How to edit the embedded images?
In CVPR, pages 8296–8305, 2020.

[3]
Amit H Bermano, Rinon Gal, Yuval Alaluf, Ron Mokady, Yotam Nitzan, Omer Tov,
Oren Patashnik, and Daniel Cohen-Or.
State-of-the-art in the architecture, methods and applications of
In Computer Graphics Forum, volume 41, pages 591–611, 2022.

[4]
Qiong Cao, Li Shen, Weidi Xie, Omkar M Parkhi, and Andrew Zisserman.
Vggface2: A dataset for recognising faces across pose and age.
In 2018 13th IEEE international conference on automatic face &
gesture recognition (FG 2018), pages 67–74. IEEE, 2018.

[5]
Qianli Feng, Viraj Shah, Raghudeep Gadde, Pietro Perona, and Aleix Martinez.
Near perfect gan inversion.
arXiv preprint arXiv:2202.11833, 2022.

[6]
Erik Härkönen, Aaron Hertzmann, Jaakko Lehtinen, and Sylvain Paris.
Ganspace: Discovering interpretable gan controls.
In NeurIPS, volume 33, pages 9841–9850, 2020.

[7]
Kyoungkook Kang, Seongtae Kim, and Sunghyun Cho.
Gan inversion for out-of-range images with geometric transformations.
In ICCV, pages 13941–13949, 2021.

[8]
Tero Karras, Timo Aila, Samuli Laine, and Jaakko Lehtinen.
Progressive growing of gans for improved quality, stability, and
In ICLR, 2018.

[9]
Tero Karras, Miika Aittala, Janne Hellsten, Samuli Laine, Jaakko Lehtinen, and
Timo Aila.
Training generative adversarial networks with limited data.
NeurIPS, 33:12104–12114, 2020.

[10]
Tero Karras, Miika Aittala, Samuli Laine, Erik Härkönen, Janne
Hellsten, Jaakko Lehtinen, and Timo Aila.
Alias-free generative adversarial networks.
NeurIPS, 34:852–863, 2021.

[11]
Tero Karras, Samuli Laine, and Timo Aila.
A style-based generator architecture for generative adversarial
In CVPR, pages 4401–4410, 2019.

[12]
Tero Karras, Samuli Laine, Miika Aittala, Janne Hellsten, Jaakko Lehtinen, and
Timo Aila.
Analyzing and improving the image quality of stylegan.
In CVPR, pages 8110–8119, 2020.

[13]
Sachit Menon, Alexandru Damian, Shijia Hu, Nikhil Ravi, and Cynthia Rudin.
Pulse: Self-supervised photo upsampling via latent space exploration
of generative models.
In CVPR, pages 2437–2445, 2020.

[14]
Gaurav Parmar, Yijun Li, Jingwan Lu, Richard Zhang, Jun-Yan Zhu, and
Krishna Kumar Singh.
Spatially-adaptive multilayer selection for gan inversion and
In CVPR, pages 11399–11409, 2022.

[15]
Daniel Roich, Ron Mokady, Amit H Bermano, and Daniel Cohen-Or.
Pivotal tuning for latent-based editing of real images.
arXiv preprint arXiv:2106.05744, 2021.

[16]
Yujun Shen, Jinjin Gu, Xiaoou Tang, and Bolei Zhou.
Interpreting the latent space of gans for semantic face editing.
In CVPR, pages 9243–9252, 2020.

[17]
Yujun Shen, Ceyuan Yang, Xiaoou Tang, and Bolei Zhou.
Interfacegan: Interpreting the disentangled face representation
learned by gans.
IEEE TPAMI, 44(4):2004–2018, 2020.

[18]
Yujun Shen and Bolei Zhou.
Closed-form factorization of latent semantics in gans.
In CVPR, pages 1532–1540, 2021.

[19]
Guoxian Song, Linjie Luo, Jing Liu, Wan-Chun Ma, Chunpong Lai, Chuanxia Zheng,
and Tat-Jen Cham.
Agilegan: stylizing portraits by inversion-consistent transfer
ACM TOG, 40(4):1–13, 2021.

[20]
Christian Szegedy, Sergey Ioffe, Vincent Vanhoucke, and Alexander A Alemi.
Inception-v4, inception-resnet and the impact of residual connections
on learning.
In AAAI, 2017.

[21]
Omer Tov, Yuval Alaluf, Yotam Nitzan, Or Patashnik, and Daniel Cohen-Or.
Designing an encoder for stylegan image manipulation.
ACM TOG, 40(4):1–14, 2021.

[22]
Zongze Wu, Dani Lischinski, and Eli Shechtman.
Stylespace analysis: Disentangled controls for stylegan image
In CVPR, 2021.

[23]
Zongze Wu, Yotam Nitzan, Eli Shechtman, and Dani Lischinski.
Stylealign: Analysis and applications of aligned stylegan models.
arXiv preprint arXiv:2110.11323, 2021.

[24]
Jonas Wulff and Antonio Torralba.
Improving inversion and generation diversity in stylegan using a
gaussianized latent space.
arXiv preprint arXiv:2009.06529, 2020.

[25]
Weihao Xia, Yulun Zhang, Yujiu Yang, Jing-Hao Xue, Bolei Zhou, and Ming-Hsuan
Gan inversion: A survey.
IEEE TPAMI, 2022.

[26]
Xu Yao, Alasdair Newson, Yann Gousseau, and Pierre Hellier.
A style-based gan encoder for high fidelity reconstruction of images
and videos.
In ECCV, pages 581–597, 2022.

[27]
Kaipeng Zhang, Zhanpeng Zhang, Zhifeng Li, and Yu Qiao.
Joint face detection and alignment using multitask cascaded
convolutional networks.
IEEE Sign. Process. Letters, 23(10):1499–1503, 2016.

[28]
Jiapeng Zhu, Yujun Shen, Deli Zhao, and Bolei Zhou.
In-domain gan inversion for real image editing.
In ECCV, pages 592–608. Springer, 2020.

[29]
Peihao Zhu, Rameen Abdal, John Femiani, and Peter Wonka.
Barbershop: Gan-based image compositing using segmentation masks.
arXiv preprint arXiv:2106.01505, 2021.

[30]
Peihao Zhu, Rameen Abdal, Yipeng Qin, John Femiani, and Peter Wonka.
Improved stylegan embedding: Where are the good latents?
arXiv preprint arXiv:2012.09036, 2020.


# Toward A Logical Theory Of Fairness and Bias

VAISHAK BELLE

###### Abstract

Fairness in machine learning is of considerable interest in recent years owing
to the propensity of algorithms trained on historical data to amplify and
perpetuate historical biases. In this paper, we argue for a formal
reconstruction of fairness definitions, not so much to replace existing
definitions but to ground their application in an epistemic setting and allow
for rich environmental modelling. Consequently we look into three notions:
fairness through unawareness, demographic parity and counterfactual fairness,
and formalise these in the epistemic situation calculus.

###### keywords:

Logic, Fairness, Bias, Situation Calculus, Knowledge, Action

introduction

##  1 Introduction

Machine Learning techniques have become pervasive across a range of different
applications, and are the source of considerable excitement but also debate.
For example, they are now widely used in areas as disparate as recidivism
prediction, consumer credit-risk analysis and insurance pricing (Chouldechova
2017; Khandani et al. 2010). In some of these applications, the prevalence of
machine learning techniques has raised concerns about the potential for
learned algorithms to become biased against certain groups. This issue is of
particular concern in cases when algorithms are used to make decisions that
could have far-reaching consequences for individuals (for example in
recidivism prediction) (Chouldechova 2017; Angwin et al. 2016). Attributes
which the algorithm should be “fair” with respect to are typically referred to
as _protected_ attributes. The values to these are often hidden from the view
of the decision maker (whether automated or human). There are multiple
different potential fields that might qualify as protected attributes in a
given situation, including ethnicity, sex, age, nationality and marital status
(Zemel et al. 2013). Ideally, such attributes should not affect any prediction
made by “fair” algorithms. However, even in cases where it is clear which
attributes should be protected, there are multiple (and often mutually
exclusive) definitions of what it means for an algorithm to be unbiased with
respect to these attributes, and there is disagreement within the academic
community on what is most appropriate (Dwork et al. 2011; Kusner et al. 2017;
Zafar et al. 2017a).

However, even amid pressing concerns that algorithms currently in use may
exhibit racial biases, there remains a lack of agreement about how to
effectively implement fairness, given the complex socio-technical situations
that such applications are deployed in and the background knowledge and
context needed to assess the impact of outcomes (e.g., denying a loan to
someone in need).

To address such issues broadly, an interesting argument has been championed by
the symbolic community: by assuming a rich enough understanding of the
application domain, we can encode machine ethics in a formal language. Of
course, with recent advances in statistical relational learning, neuro-
symbolic AI and inductive logic programming (Raedt et al. 2016; Muggleton et
al. 2012), it is possible to integrate low-level pattern recognition based on
sensory data with high-level formal specifications. For example, the _Hera_
project (Lindner et al. 2017) allows for the implementation of several kinds
of (rule-based) moral theory to be captured. _Geneth_ (Anderson and Anderson
2014) uses inductive logic programming to create generalised moral principles
from the judgements of ethicists about particular ethical dilemmas, with the
system’s performance being evaluated using an _ethical Turing test_. On the
formalisation side, study of moral concepts has long been a favored topic in
the knowledge representation community (Conway and Gawronski 2013; Alexander
and Moore 2016; Czelakowski 1997; Hooker and Kim 2018), that can be further
coupled against notions of beliefs, desires and intentions (Broersen et al.
2001; Georgeff et al. 1998). Finally, closer to the thrust of this paper,
(Pagnucco et al. 2021) formalize consequentialist and deontological ethical
principles in terms of “desirable” states in the epistemic situation calculus,
and (Classen and Delgrande 2020) formalize obligations using situation
calculus programs.

contributions

##  2 Contributions

Our thesis, in essence, is this: complementing the vibrant work in the ML
community, it is worthwhile to study ethical notions in formal languages. This
serves three broad objectives:

  1. 1.

We can identify what the system needs to know versus what is simply true
(Reiter 2001a; Halpern and Moses 2014) and better articulate how this
knowledge should impact the agent’s choices. It is worth remarking that
epistemic logic has served as the foundation for investigating the impact of
knowledge on plans and protocols (Levesque 1996; Lespérance et al. 2000;
Halpern et al. 2009).

  2. 2.

We implicitly understand that we can further condition actions against
background knowledge (such as ontologies and databases), as well as notions
such as intentions and obligations (Sardina and Lespérance 2010).

  3. 3.

We can position the system’s actions not simply as a single-shot decision or
prediction, as is usual in the ML literature, but as a sequence of complex
events that depend on observations and can involve loops and recursion: that
is, in the form of programs (Levesque et al. 1997).

It would beyond the scope of a single paper to illustrate the interplay
between the three objectives except in some particular application scenario.
Thus, we focus on the interplay between A and C in the sense of advocating a
“research agenda,” rather than a single technical result, or a demonstration
of a single application. In particular, what we seek to do is a formal
reconstruction of some fairness definitions, not so much to replace existing
definitions but to ground their application in an epistemic, dynamic setting.
Consequently we look into three notions: fairness through unawareness,
demographic parity and counterfactual fairness, and formalise these in the
epistemic situation calculus (Scherl and Levesque 2003; Lakemeyer and Levesque
2011). In particular, our contributions are as follows:

  * •

Consider the notion of fairness through unawareness (FTU) in machine learning.
Here, a “fair” classifier is one that predicts outputs by not using any
information about protected attributes. In a dynamic setting, imagine a
(virtual or physical) robot that is acting in service of some objective
$\phi.$ For example, in a loan setting, which is classically treated as a
static model in machine learning, we can expect intelligent automated agents
to carry out many operations: check the yearly budget of the bank to determine
the total amount to be loaned, rank applicants based on risk, determine the
impact of recession, and ultimately synthesize a plan to achieve $\phi$ (loan
approval), but by virtue of FTU, it should never be the case that the agent
has had access to protected information. In this paper, we provide a simple
but general definition to capture that idea, in a manner that distinguishes
what is true from what is known by the agent.

  * •

Analogously, consider the notion of demographic parity (DP). It is understood
as a classifier that is equally likely to make a positive prediction
regardless of the value of the protected attribute. For example, the
proportion of men who are granted loans equals the proportion of women granted
loans. So, if $\phi(x)$ is the granting of a loan to individual $x,$ how do we
capture the notion that the agent has synthesized a plan that achieves
$\phi(x)$ for both males as well as females? What would it look like for
planning agents that want to conform to both FTU and DP? What if, instead of
DP, we wished to only look at those granted loans, and among this group, we
did not want the classifier to discriminate based on the individual’s gender?
For all these cases, we provide definitions in terms of the agent’s mental
state and action sequences that the agent knows will achieve $\phi(x)$
(Levesque 1996).

  * •

Finally, counterfactual fairness insists that the prediction should not differ
if the individual’s protected attributes take on a different value. For a
planning agent to ensure this, we would need to make sure that _deleting_
facts about the current value for an individual $x$’s protected attribute and
_adding_ a different value still achieves $\phi(x)$ after the sequence. We
characterize this using the notion of _forgetting_ because we permit, in
general, any arbitrary first-order theory for the initial knowledge base, and
not just a database interpreted under the closed-world assumption.

These definitions can be seen to realize a specification for “fair” cognitive
robots: that is, reasoning and planning agents (Lakemeyer and Levesque 2007)
that ensure through the course of their acting that, say, they never gain
knowledge about the protected attributes of individuals, and guarantee that
individuals are not discriminated based on values to these attributes.

It should be clear that our definitions are loosely inspired by the ML
notions. And so our formalisation do not argue for one definition over
another, nor challenge any existing definition. We do, however, believe that
studying the effects of these definitions in a dynamic setting provides a
richer context to evaluate their appropriateness. Moreover, a formalisation
such as ours lends itself to various types of implementations. For example,
the synthesis of (epistemic) programs and plans (Wang and Zhang 2005; Baral et
al. 2017; Muise et al. 2015; Classen et al. 2008; McIlraith and Son 2002) that
achieve goals in socio-technical applications in a fair manner is an
worthwhile research agenda. Likewise, enforcing fairness constraints while
factoring for the relationships between individuals in social networks
(Farnadi et al. 2018), or otherwise contextualising attributes against other
concepts in a relational knowledge base (Aziz et al. 2018; Fu et al. 2020) are
also worthwhile. By stipulating an account in quantified logic, it becomes
possible to further unify such proposals in a dynamic setting.

Logic and fairness. Let us briefly remark on closely related efforts. At the
outset, note that although there has been considerable work on formalizing
moral rules, there is no work (as far as we are aware) on the formalization of
fairness and bias in a _dynamic epistemic_ setting, where we need to explicate
the interaction between actions, plans and meta-beliefs. However, there is
some work that tackles epistemic and logical aspects.

For example, the work of (Kawamoto 2019) considers a statistical epistemic
logic and its use for the formalisation of statistical accuracy as well as
fairness, including the criterion of equality of opportunity. There are a few
key differences to our work: that work is motivated by a probabilistic
reconstruction of prediction systems by appealing to distance measures, and so
knowledge is defined in terms of accessibility between worlds that are close
enough. The language, moreover, allows for “measurement” variables that are
interpreted statistically. In contrast, our account is not (yet)
probabilistic, and if our account were to be extended in that fashion, the
most obvious version would reason about degrees of belief (Bacchus et al.
1999; Belle and Lakemeyer 2017); see (Bacchus et al. 1996) for discussions on
the differences between statistical belief and degrees of belief. Moreover,
our account is dynamic, allowing for explicit modalities operators for actions
and programs. Consequently, our definitions are about studying how, say, the
agent remains ignorant about protected attributes when executing a plan.

Be that as it may, the work of (Kawamoto 2019) leads to an account where
fairness can be expressed as a logical property using predicates for protected
attributes, remarkably similar in spirit to our approach if one were to ignore
actions. This should, in the very least, suggest that such attempts are very
promising, and for the future, it would be worthwhile to conduct a deeper
investigation on how these formalisation attempts can be synthesized to obtain
a general probabilistic logical account that combines the strength of dynamic
epistemic languages and statistical measures. (In a related vein to (Kawamoto
2019), (Liu and Lorini 2022) seek to axiomatize ML sytems for the purpose of
explanations in a modal logic.) An entirely complementary effort is the use of
logic for verifying fair models (Ignatiev et al. 2020), where existing
definitions and classifiers are encoded using logical functions and
satisfiability modulo theories.

To summarize, all these differ from our work in that we are attempting to
understand the interplay between bias, action and knowledge, and not really
interested in capturing classifiers as objects in our language. Thus, our
work, as discussed above, can be seen as setting the stage for _“fair”
cognitive robots_. There is benefit to unifying these streams, which we leave
to the future.

sec:reconstructing_the_epistemic_situation_calculus

##  3 A logic for knowledge and action

We now introduce the logic ${\mathcal{}E}{\mathcal{}S}$ (Lakemeyer and
Levesque 2004).111Our choice of language may seem unusual, but it is worth
noting that this language is a modal syntactic variant of the classical
epistemic situation that is better geared for reasoning about knowledge
(Lakemeyer and Levesque 2011). But more importantly, it can be shown that
reasoning about actions and knowledge reduces to first-order reasoning via the
so-called regression and representation theorems (Lakemeyer and Levesque
2004). (For space reasons, we do not discuss such matters further here.) There
are, of course, many works explicating the links between the situation
calculus and logic programming; see, for example, (Lee and Palla 2012). See
also works that link the situation calculus to planning, such as (Classen et
al. 2008; Belle 2022; Sardina et al. 2004; Baier et al. 2007). The non-modal
fragment of ${\mathcal{}E}{\mathcal{}S}$ consists of standard first-order
logic with $=$. That is, connectives $\left\\{\land,\forall,\neg\right\\}$,
syntactic abbreviations $\left\\{\exists,\equiv,\supset\right\\}$ defined from
those connectives, and a supply of variables variables
$\left\\{x,y,\ldots,u,v,\ldots\right\\}$. Different to the standard syntax,
however, is the inclusion of (countably many) _standard names_ (or simply,
names) for both objects and actions ${\mathcal{}R},$ which will allow a
simple, substitutional interpretation for $\forall$ and $\exists.$ These can
be thought of as special extra constants that satisfy the unique name
assumption and an infinitary version of domain closure.

Like in the situation calculus, to model immutable properties, we assume rigid
predicates and functions, such as _IsPlant(x)_ and _father(x)_ respectively.
To model changing properties, ${\mathcal{}E}{\mathcal{}S}$ includes fluent
predicates and functions of every arity, such as _Broken(x)_ and _height(x)_.
Note that there is no longer a situation term as an argument in these symbols
to distinguish the fluents from the rigids. For example,
${\mathcal{}E}{\mathcal{}S}$ also includes distinguished fluent predicates
${\mathit{P}oss}$ and ${\mathit{S}F}{}$ to model the executability of actions
and capture sensing outcomes respectively, but they are unary predicates (that
is, in contrast to the classical situation calculus (Reiter 2001b) because
they no longer include situation terms.) Terms and formulas are constructed as
usual. The set of ground atoms ${\mathcal{}P}$ are obtained, as usual, from
names and predicates.

There are four modal operators in ${\mathcal{}E}{\mathcal{}S}$:
$[a],\Box,\mathitbf{K}$ and $\mathitbf{O}.$ For any formula $\alpha,$ we read
$[a]\alpha,\Box\alpha$ and $\mathitbf{K}\alpha$ as “$\alpha$ holds after $a$”,
“$\alpha$ holds after any sequence of actions” and “$\alpha$ is known,”
respectively. Moreover, $\mathitbf{O}\alpha$ is to be read as “$\alpha$ is
only-known.” Given a sequence $\delta=a_{1}\cdots a_{k},$ we write
$[\delta]\alpha$ to mean $[a_{1}]\cdots[a_{k}]\alpha.$

In classical situation calculus parlance, we would use $[a]\alpha$ to capture
successor situations as properties that are true after an action in terms of
the current state of affairs. Together with the $\Box$ modality, which allows
to capture quantification over situations and histories, basic action theories
can be defined. Like in the classical approach, one is interested in the
entailments of the basic action theory.

Semantics. Recall that in the simplest setup of the possible-worlds semantics,
worlds mapped propositions to $\left\\{0,1\right\\}$, capturing the (current)
state of affairs. ${\mathcal{}E}{\mathcal{}S}$ is based on the very same idea,
but extended to dynamical systems. So, suppose a world maps ${\mathcal{}P}$
and ${\mathcal{}Z}$ to $\left\\{0,1\right\\}$.222We need to extend the mapping
to additionally interpret fluent functions and rigid symbols, omitted here for
simplicity. Here, ${\mathcal{}Z}$ is the set of all finite sequences of action
names, including the empty sequence $\langle\rangle.$ Let ${\mathcal{}W}$ be
the set of all worlds, and $e\subseteq{\mathcal{}W}$ be the _epistemic state_.
By a _model_ , we mean a triple $(e,w,z)$ where $z\in{\mathcal{}Z}.$
Intuitively, each world can be thought of as a situation calculus tree,
denoting the properties true initially but also after every sequence of
actions. ${\mathcal{}W}$ is then the set of all such trees. Given a triple
$(e,w,z)$, $w$ denotes the real world, and $z$ the actions executed so far.

To account for how knowledge changes after (noise-free) sensing, one defines
$w^{\prime}\sim_{z}w$, which is to be read as saying “$w^{\prime}$ and $w$
agree on the sensing for $z$”, as follows:

  * •

if $z=\langle\rangle,$ $w^{\prime}\sim_{z}w$ for every $w^{\prime}$; and

  * •

$w^{\prime}\sim_{z\cdot a}w$ iff $w^{\prime}\sim_{z}w,$
$w^{\prime}[{\mathit{P}oss}(a),z]=1$ and
$w^{\prime}[{\mathit{S}F}(a),z]=w[{\mathit{S}F}(a),z].$

This is saying that initially, we would consider all worlds compatible, but
after actions, we would need the world $w^{\prime}$ to agree on the
executability of actions performed so far as well as agree on sensing
outcomes. The reader might notice that this is clearly a reworking of the
successor state axiom for the knowledge fluent in (Scherl and Levesque 2003).

With this, we get a simply account for truth. We define the satisfaction of
formulas wrt (with respect to) the triple $(e,w,z)$, and the semantics is
defined inductively:

  * •

$e,w,z\models p$ iff $p$ is an atom and $w[p,z]=1$;

  * •

$e,w,z\models\alpha\land\beta$ iff $e,w,z\models\alpha$ and
$e,w,z\models\beta;$

  * •

$e,w,z\models\neg\alpha$ iff $e,w,z\not\models\alpha;$

  * •

$e,w,z\models\forall x\alpha$ iff $e,w,z\models\alpha^{x}_{n}$ for all
$n\in{\mathcal{}R};$

  * •

$e,w,z\models[a]\alpha$ iff $e,w,z\cdot a\models\alpha;$

  * •

$e,w,z\models\Box\alpha$ iff $e,w,z\cdot z^{\prime}\models\alpha$ for all
$z^{\prime}\in{\mathcal{}Z}$;

  * •

$e,w,z\models\mathitbf{K}\alpha$ iff for all $w^{\prime}\sim_{z}w,$ if
$w^{\prime}\in e,$ $e,w^{\prime},z\models\alpha$; and

  * •

$e,w,z\models\mathitbf{O}\alpha$ iff for all $w^{\prime}\sim_{z}w,$
$w^{\prime}\in e,$ iff $e,w^{\prime},z\models\alpha$.

We write $\Sigma\models\alpha$ (read as “$\Sigma$ entails $\alpha$”) to mean
for every $M=(e,w,\langle\rangle)$, if $M\models\alpha^{\prime}$ for all
$\alpha^{\prime}\in\Sigma,$ then $M\models\alpha.$ We write $\models\alpha$
(read as “$\alpha$ is valid”) to mean $\left\\{\right\\}\models\alpha.$

Properties. sub:properties Let us first begin by observing that given a model
$(e,w,z),$ we do not require $w\in e.$ It is easy to show that if we
stipulated the inclusion of the real world in the epistemic state,
$\mathitbf{K}\alpha\supset\alpha$ would be true. That is, suppose
$\mathitbf{K}\alpha.$ By the definition above, $w$ is surely compatible with
itself after any $z$, and so $\alpha$ must hold at $w.$ Analogously,
properties regarding knowledge can be proven with comparatively simpler
arguments in a modal framework, in relation to the classical epistemic
situation calculus. Valid properties include:

  1. 1.

$\Box(\mathitbf{K}(\alpha)\land\mathitbf{K}(\alpha\supset\beta)\supset\mathitbf{K}(\beta))$;

  2. 2.

$\Box(\mathitbf{K}(\alpha)\supset\mathitbf{K}(\mathitbf{K}(\alpha)));$

  3. 3.

$\Box(\neg\mathitbf{K}(\alpha)\supset\mathitbf{K}(\neg\mathitbf{K}(\alpha)))$;

  4. 4.

$\Box(\forall x.\leavevmode\nobreak\
\mathitbf{K}(\alpha)\supset\mathitbf{K}(\forall x.\leavevmode\nobreak\
\alpha))$; and

  5. 5.

$\Box(\exists x.\leavevmode\nobreak\
\mathitbf{K}(\alpha)\supset\mathitbf{K}(\exists x.\leavevmode\nobreak\
\alpha)).$

Note that such properties hold over all possible action sequences, which
explains the presence of the $\Box$ operator on the outside. The first is
about the closure of modus ponens within the epistemic modality. The second
and third are on positive and negative introspection. The last two reason
about quantification outside the epistemic modality, and what that means in
terms of the agent’s knowledge. For example, item 5 says that if there is some
individual $n$ such that the agent knows $Teacher(n)$, it follows that the
agent believes $\exists xTeacher(x)$ to be true. This may seem obvious, but
note that the property is really saying that the existence of an individual in
some possible world implies that such an individual exists in all accessible
worlds. It is because there is a fixed domain of discourse that these
properties come out true; they are referred to a the Barcan formula.

As seen above, the logic ${\mathcal{}E}{\mathcal{}S}$ allows for a simple
definition of the notion of only-knowing in the presence of actions (Levesque
1990), which allows one to capture both the beliefs as well as the non-beliefs
of the agent. Using the modal operator $\mathitbf{O}$ for only-knowing, it can
be shown that $\mathitbf{O}\alpha\models\mathitbf{K}\beta$ if
$\alpha\models\beta$ but $\mathitbf{O}\alpha\models\neg\mathitbf{K}\beta$ if
$\alpha\not\models\beta$ for any non-modal $\left\\{\alpha,\beta\right\\}.$
That is, only-knowing a knowledge base also means knowing everything entailed
by that knowledge base. Conversely, it also means not believing everything
that is not entailed by the knowledge base. In that sense, $\mathitbf{K}$ can
be seen as an “at least” epistemic operator, and $\mathitbf{O}$ captures both
at least and “at most” knowing. This can be powerful to ensure, for example,
that the agent provably does not know protected attributes.

We will now consider the axiomatization of a basic action theory in
${\mathcal{}E}{\mathcal{}S}$. But before explaining how successor state axioms
are written, one might wonder whether a successor state axiom for
$\mathitbf{K}$ is needed, as one would for $Knows$ in the epistemic situation
calculus. It turns out because the compatibility of the worlds already
accounted for the executability of actions and sensing outcomes in accessible
worlds, such an axiom is actually a property of the logic:

$\models\Box[a]\mathitbf{K}(\alpha)\equiv({\mathit{S}F}(a)\land\mathitbf{K}({\mathit{S}F}(a)\supset[a]\alpha))\leavevmode\nobreak\
\lor\\\
(\neg{\mathit{S}F}(a)\land\mathitbf{K}(\neg{\mathit{S}F}(a)\supset[a]\alpha)).$

(As is usual, free variables are implicitly quantified from the outside.)
Thus, what will be known after an action is understood in terms of what was
known previously together with the sensing outcome. The example below will
further clarify how $SF$ works.

Basic Action Theories. To axiomatize the domain, we consider the analogue of
the basic action theory in the situation calculus (Reiter 2001b). It consists
of:

  * •

axioms that describe what is true in the initial states, as well as what is
known initially;

  * •

precondition axioms that describe the conditions under which actions are
executable using a distinguished predicate $Poss$;

  * •

successor state axioms that describe the conditions under which changes happen
to fluents after actions (incorporating Reiter’s monotonic solution to the
frame problem); and

  * •

sensing axioms that inform the agent about the world using a distinguished
predicate $SF.$

Note that foundational axioms as usually considered in Reiter’s variant of the
situation calculus (Reiter 2001b) are not needed as the tree-like nature of
the situations is baked into the semantics.

Let us consider a simple example of a loan agency set up for the employees of
a company. For simplicity, assume actions are always executable: $\Box
Poss(a)=\mbox{true}.$ Let us also permit a sensing axiom that allows one to
look up if an individual is male: $\Box{\mathit{S}F}(a)\equiv(a=isMale(x)\land
Male(x))\lor a\neq isMale(x).$ For simplicity, we assume binary genders, but
it is a simple matter of using a predicate such as $Gender(x,y)$ instead to
allow individuals $x$ to take on gender $y$ from an arbitrary set.

To now consider successor state axioms, let us suppose having a loan is simply
a matter of the manager approving, and unless the manager denies it at some
point, the individual continues to hold the loan. For illustration purposes,
we will consider a company policy that approves loans for those with high
salaries. High salaries are enabled for an “eligible” individual if they are
promoted by the manager, and salaries remain high unless they get demoted.
Finally, we model eligibility and maleness as a rigid, but this is not
necessary, and we can permit actions that updates the gender of individuals in
the database. These are formalized as the axioms below, where the left hand
side of the equivalence captures the idea that for every sequence of actions,
the effect of doing $a$ on a predicate is given by the right hand side of the
equivalence.

$\displaystyle\Box[a]$ $\displaystyle hasLoan(x)\equiv
a=approve(x)\lor(hasLoan(x)\land a\neq deny(x)).$ $\displaystyle\Box[a]$
$\displaystyle highSalary(x)\equiv(a=promote(x)\land
Eligible(x))\lor(highSalary(x)\land a\neq demote(x)).$ $\displaystyle\Box[a]$
$\displaystyle Eligible(x)\equiv Eligible(x).$ $\displaystyle\Box[a]$
$\displaystyle Male(x)\equiv Male(x).$

We will lump the successor state, precondition and sensing axioms as
$\Sigma_{\mathit{d}yn}$. The sentences that are true initially will be
referred to by $\Sigma_{0}$; however, the agent cannot be expected to know
everything that is true, and so let $\Sigma_{0}^{\prime}$ be what is believed
initially. It may seem natural to let
$\Sigma_{0}^{\prime}\subseteq\Sigma_{0}$, but that it not necessary. The agent
might be uncertain about what is true (e.g., $\Sigma_{0}$ might have $p$ but
$\Sigma_{0}^{\prime}$ has $p\lor q$ instead).333If the agent believes facts
that are conflicted by observations about the real world, beliefs may need to
be revised (Delgrande and Levesque 2012), a matter we ignore for now. Our
theory of knowledge is based on _knowledge expansion_ where sensing ensures
that the agent is more certain about the world (Scherl and Levesque 2003;
Reiter 2001b). However, for simplicity, we will require that agents at least
believe the dynamics works as would the real world. Therefore, we consider
entailments wrt the following _background theory_ :

$\Sigma=\Sigma_{0}\land\Sigma_{\mathit{d}yn}\land\mathitbf{O}(\Sigma_{0}^{\prime}\land\Sigma_{\mathit{d}yn}).$

In our example, let us suppose: $\Sigma_{0}=\left\\{Male(n_{i}),\neg
Male(n^{\prime}_{i}),Eligible(n_{i}),\neg Eligible(n^{\prime}_{i})\mid i\in
N\right\\}$ whereas, what is believed by the agent initially is:
$\Sigma_{0}^{\prime}=\left\\{Eligible(n_{i}),\neg Eligible(n^{\prime}_{i})\mid
i\in N\right\\}$ So there are two groups of individuals, $n_{i}$ and
$n^{\prime}_{i},$ the first male and the second female, the first considered
eligible and the second not considered eligible. All that the agent knows is
the eligibility of the individuals. Note that $N$ here is any set, possibly an
infinite one, that is, the language allows $N={\rm Nature}.$ For ease of
readability, however, we let $N=\left\\{1\right\\}$ in our examples below, and
we write $n_{1}$ as $n$ and $n^{\prime}_{1}$ as $n^{\prime}.$444Note that
although the language has infinitely many constants, a finite domain can be
enforced using domain relativization. For example, let: $\forall
x(Individual(x)\equiv x=john\lor\ldots\lor x=jane).$ This declares finitely
many individuals. Then instead of saying $\exists x.\leavevmode\nobreak\
Eligible(x)$, which in general means that any one of the infinitely many
constants is eligible, we would write: $\exists x(Individual(x)\land
Eligible),$ which declares that only one from
$\left\\{john,\ldots,jane\right\\}$ is eligible.

It is worth quickly remarking that many features of the language are omitted
here for simplicity. For example, ${\mathcal{}E}{\mathcal{}S}$ can be extended
with second-order variables (Classen and Lakemeyer 2008), which allows one to
consider the equivalent of GOLOG programs (Levesque et al. 1997). Likewise,
notions of probabilistic actions (Bacchus et al. 1999), epistemic
achievability (Lespérance et al. 2000), and causality (Batusov and Soutchanski
2018) in addition to studying program properties (Classen 2018) are
interesting dimensions to explore in the fairness context.

Forgetting. In some of the definitions of fairness, we will need to force the
setting where information about protected attributes is forgotten. While
standard ML approaches propose to do this via column deletion (e.g., remove
all entries for the gender attribute), a richer notion is arguably needed for
a first-order knowledge base. We appeal to the notion of forgetting (Lin and
Reiter 1994).

Lin and Reiter defined the notion of forgetting, which is adapted to
${\mathcal{}E}{\mathcal{}S}$ below. They show that while forgetting ground
atoms is first-order definable, forgetting relations needs second-order logic.
We only focus on the case of atoms, but it would interesting to study how
fairness notions are affected when protected attributes are completely absent
from a theory.

Suppose $S$ denotes a finite set of ground atoms. We write ${\mathcal{}M}(S)$
to mean the set of all truth assignments to $S$. Slightly abusing notation,
given a ground atom $p$, we write $w^{\prime}\sim_{p}w$ to mean that
$w^{\prime}$ and $w$ agree on everything initially, except maybe $p.$ That is,
for every atom $q\neq p,$ $w[q,\langle\rangle]=w^{\prime}[q,\langle\rangle]$.
Next, for every action sequence $z\neq\langle\rangle$ and every atom
$q^{\prime},$ $w[q^{\prime},z]=w^{\prime}[q^{\prime},z].$

_Definition._ Given a formula $\phi$ not mentioning modalities, we say
$\phi^{\prime}$ is the result of forgetting atom $p$, denoted
${\mathit{F}orget}(\phi,p)$, if for any world $w$, $w\models\phi^{\prime}$ iff
there is a $w^{\prime}$ such that $w^{\prime}\models\phi$ and
$w\sim_{p}w^{\prime}$. Inductively, given a set of atoms
$\left\\{p_{1},\ldots,p_{k}\right\\}$, define
${\mathit{F}orget}(\phi,\left\\{p_{1},\ldots,p_{k}\right\\})$ as
${\mathit{F}orget}({\mathit{F}orget}(\phi,p_{1}),\ldots,p_{k})$.

It is not hard to show that forgetting amounts to setting an atom to true
everywhere or setting it false everywhere. In other words: _Proposition._
${\mathit{F}orget}(\phi,S)\equiv\bigvee_{M\in{\mathcal{}M}(s)}\phi[M],$ where
$\phi[M]$ is equivalent to $\phi\land\bigwedge_{i}(p_{i}=b_{i})$ understood to
mean that the proposition $p_{i}$ is accorded the truth value
$b_{i}\in\left\\{0,1\right\\}$ by $M.$

Abusing notation, we extend the notion of forgetting of an atom $p$ for basic
action theories and the background theory as follows in applying it solely to
what is true/known initially:

  * •

${\mathit{F}orget}(\Sigma_{0}\land\Sigma_{\mathit{d}yn},p)={\mathit{F}orget}(\Sigma_{0},p)$;
and

  * •

${\mathit{F}orget}(\Sigma,p)={\mathit{F}orget}(\Sigma_{0},p)\land\Sigma_{\mathit{d}yn}\land\mathitbf{O}({\mathit{F}orget}(\Sigma_{0}^{\prime},p)\land\Sigma_{\mathit{d}yn}).$

One of the benefits of lumping the knowledge of the agent as an objective
formula in the context of the only-knowing operator is the relatively simple
definition of forgetting.

_Proposition._ Suppose $\phi$ is non-modal. Suppose $p$ is an atom. For every
objective $\psi$ such that ${\mathit{F}orget}(\phi,p)\models\psi$ it is also
the case that
$\mathitbf{O}({\mathit{F}orget}(\phi,p))\models\mathitbf{K}\psi.$

Because $\mathitbf{O}\phi\models\mathitbf{K}\psi$ for every
$\left\\{\phi,\psi\right\\}$ provided $\phi\models\psi$, the above statement
holds immediately. In so much as we are concerned with a non-modal initial
theory and the effects of forgetting, our definition of
${\mathit{F}orget}(\Sigma,p)$ above (notational abuse notwithstanding)
suffices. In contrast, forgetting with arbitrary epistemic logical formulas is
far more involved (Zhang and Zhou 2009).

sec:context_and_existing_notions

##  4 Existing notions

As discussed, we will not seek to simply retrofit existing ML notions in a
logical language; rather we aim to identify the principles and emphasize the
provenance of unfair actions in complex events. Nonetheless, it is useful to
revisit a few popular definitions to guide our intuition.

Fairness through unawareness. Fairness through unawareness (FTU) is the
simplest definition of fairness; as its name suggests, an algorithm is “fair”
if it is unaware of the protected attribute $a_{p}$ of a particular individual
when making a prediction (Kusner et al. 2017).

_Definition._ For some set of attributes $X$ any mapping
$f:X\xrightarrow{}\hat{y}$, where $a_{p}\not\in X$ satisfies fairness through
unawareness (Kusner et al. 2017). (Assume $y$ denotes the true label.)

This prevents the algorithm learning direct bias on the basis of the protected
attribute, but does not prevent indirect bias, which the algorithm can learn
by exploiting the relationship between other training variables and the
protected attribute (Pedreschi et al. 2008; Hardt et al. 2016). Moreover, if
any of the training attributes are allocated by humans there is the potential
for bias to be introduced.

Statistical measures of fairness. Rather than defining fairness in terms of
the scope of the training data, much of the existing literature instead
assesses whether an algorithm is fair on the basis of a number of statistical
criteria that depend on the predictions made by the algorithm (Hardt et al.
2016; Kusner et al. 2017; Zemel et al. 2013). One widely used and simple
criterion is demographic parity (DP). In the case that both the predicted
outcome and protected attribute $a_{p}$ are both binary variables, a
classifier is said to satisfy predictive parity (Hardt et al. 2016) if:
$P(\hat{y}=1|a_{p}=1)=P(\hat{y}=1|a_{p}=0).$ By this definition, a classifier
is considered fair if it is equally likely to make a positive prediction
regardless of the value of the protected attribute $a_{p}$.

Fairness and the individual. Another problem with statistical measures is
that, provided that the criterion is satisfied, an algorithm will be judged to
be fair regardless of the impact on individuals. In view of that, various
works have introduced fairness metrics which aim to ensure that individuals
are treated fairly, rather than simply considering the statistical impact on
the population as a whole (Dwork et al. 2011; Kusner et al. 2017).
Counterfactual fairness (CF), for example, was proposed as a fairness
criterion in (Kusner et al. 2017). The fundamental principle behind this
definition of fairness is that the outcome of the algorithm’s prediction
should not be altered if different individuals within the sample training set
were allocated different values for their protected attributes (Kusner et al.
2017). This criterion is written in the following form:
$P(\hat{y}_{A_{p}\leftarrow a_{p}}|A=a,X=x)=P(\hat{y}_{A_{p}\leftarrow
a_{p}^{\prime}}|A=a,X=x)\hskip 2.84526pt\forall y,a^{\prime}.$ The notation
$\hat{y}\leftarrow_{A_{p}\leftarrow a_{p}}$ is understood as “the value of
$\hat{y}$ if $A_{p}$ had taken the value $a_{p}$” (Kusner et al. 2017).

sec:fairness

##  5 Formalizing Fairness

At the outset, let us note a few salient points about our formalizations of
FTU, DP and CF:

  1. 1.

Because we are not modeling a prediction problem, our definitions below should
be seen as being loosely inspired by existing notions rather that faithful
reconstructions. In particular, we will look at “fair outcomes” after a
sequence of actions. Indeed, debates about problems with the mathematical
notions of fairness in single-shot predictions problems are widespread (Dwork
et al. 2011; Kusner et al. 2017; Zafar et al. 2017a), leading to recent work
on looking at the long-term effects of fairness (Creager et al. 2020).
However, we are ignoring probabilities in the formalization in current work
only to better study the principles behind the above notions – we suspect with
a probabilistic epistemic dynamic language (Bacchus et al. 1999), the
definitions might resemble mainstream notions almost exactly and yet
organically use them over actions and programs, which is attractive.

  2. 2.

The first-order nature of the language, such as quantification, will allow us
to easily differentiate fairness for an individual versus groups. In the
mainstream literature, this has to be argued informally, and the intuition
grasped meta-linguistically.

  3. 3.

Because we model the real-world in addition the agent’s knowledge, we will be
able to articulate what needs to be true vs just believed by the agent. In
particular, our notion of equity will refer to the real-world.

  4. 4.

De-re vs de-dicto knowledge will mean having versus not having information
about protected attributes respectively. Sensing actions can be set up to
enable de-re knowledge if need be, but it is easy to see in what follows that
de-dicto is preferable.

  5. 5.

Action sequences can make predicates true, and this will help us think about
equity in terms of balancing opportunities across instances of protected
attributes (e.g., making some property true so that we achieve gender
balance).

Fairness through unawareness. Let us begin with FTU: recall that it requires
that the agent does not know the protected attributes of the individuals. To
simplify the discussion, let us assume we are concerned with one such
attribute $\theta(x)$, say, $Male(x)$, in our examples for concreteness. We
might be interested in achieving $hasLoan(x)$ or $highSalary(x)$, for example,
either for all $x$ or some individual.

_Definition._ A sequence $\delta=a_{1}\cdots a_{k}$ implements FTU for $\phi$
wrt protected attribute $\theta(x)$ iff
$\Sigma\models[\delta]\mathitbf{K}\phi$; and for every
$\delta^{\prime}\leq\delta$: $\Sigma\models[\delta^{\prime}]\neg\exists
x(\mathitbf{K}\theta(x)).$

The attractiveness of a first-order formalism is that in these and other
definitions below where we quantify over all individuals, it is immediate to
limit the applicability of the conditions wrt specific individuals. Suppose
$n$ is such an individual. Then:

_Definition._ A sequence $\delta=a_{1}\cdots a_{k}$ implements FTU for $\phi$
wrt attribute $\theta(x)$ for individual $n$ iff (a)
$\Sigma\models[\delta]\mathitbf{K}\phi$; and (b) for every
$\delta^{\prime}\leq\delta$:
$\Sigma\models[\delta^{\prime}]\neg\mathitbf{K}\theta(n).$

_Example._ Consider $\Sigma$ from eq:example[eq:example], $Male(x)$ as the
protected attribute, and suppose $\delta=approve(n)\cdot approve(n^{\prime})$.
It is clear that $\delta$ implements FTU for both the universal $\phi=\forall
xhasLoan(x)$ as well as an individual $\phi=hasLoan(n).$ Throughout the
history, the agent does not know the gender of the individual.

Before turning to other notions, let us quickly reflect on proxy variables.
Recall that in the ML literature, these are variables that indirectly provide
informations about protected attributes. We might formalize this using
entailment:

_Definition._ Given a protected attribute $\theta(x)$ and theory $\Sigma$, let
the proxy set $Proxy(\theta(x))$ be the set of predicates
$\left\\{\eta_{1}(x),\ldots\eta_{k}(x)\right\\}$ such that:
$\Sigma\models\forall x(\eta_{i}(x)\supset\theta(x)),$ for
$i\in\left\\{1,\ldots,k\right\\}$. That is, given the axioms in the background
theory, $\eta_{i}(x)$ tells us about $\theta(x)$.

_Example._ Suppose the agent knows the following sentence: $\forall
x(EtonForBoys(x)\supset Male(x)).$ Let us assume $EtonForBoys(x)$ is a rigid,
like $Male(x)$. Let us also assume that $\mathitbf{K}(EtonForBoys(n))$. It is
clear that having information about this predicate for $n$ would mean the
agent can infer that $n$ is male.

The advantage of looking at entailment in our definitions is that we do not
need to isolate the proxy set at all, because whatever information we might
have the proxy set and its instances, all we really need to check is that
$\Sigma\not\models\exists x\mathitbf{K}\theta(x)$.555With this discussion, we
do not mean to insist that analyzing “relevant” predicates for $\theta(x)$ is
a pointless endeavor. Rather we only want to point out that regardless of the
information available to the agent, as long as we check that it is actually
ignorant about the gender, other relevant predicates may not matter. Of
course, a biased agent can enable actions that favors individuals based on
such proxy predicates instead, but in that case, such proxy predicates would
also need to be included in the protected attribute list.

Demographic parity. Let us now turn to DP. In the probabilistic context, DP is
a reference to the proportion of individuals in the domain: say, the
proportion of males promoted is the same as the proportion of females
promoted. In logical terms, although FTU permitted its definition to apply to
both groups and individuals, DP, by definition, is necessarily a quantified
constraint. In contrast, CF will stipulate conditions solely on individuals.

_Definition._ A sequence $\delta=a_{1}\cdots a_{k}$ implements DP for
$\phi(x)$ wrt attribute $\theta(x)$ iff:
$\Sigma\models[\delta]\mathitbf{K}((\forall
x\theta(x)\supset\phi(x))\land(\forall x\neg\theta(x)\supset\phi(x))).$

To reiterate, in probabilistic terms, the proportion of men who are promoted
equals the proportion of women who are promoted. In the categorial setting,
the agent knows that all men are promoted as well as that all women are
promoted.

_Example._ Consider $\delta=approve(n)\cdot approve(n^{\prime})$. It
implements DP for $hasLoan(x)$ wrt attribute $isMale(x).$

Note that even though the agent does not know the gender of the individuals,
in every possible world, regardless of the gender assigned to an individual
$n$ in that world, $n$ has the loan. In other words, all men and all women
hold the loan. This is de-dicto knowledge of the genders, and it is sufficient
to capture the thrust of DP.

We might be tempted to propose a stronger requirement, stipulating de-re
knowledge:

_Definition._ A sequence $\delta=a_{1}\cdots a_{k}$ implements strong DP for
$\phi(x)$ wrt attribute $\theta(x)$ iff:
(a)$\Sigma\models[\delta]\mathitbf{K}((\forall
x\theta(x)\supset\phi(x))\land(\forall x\neg\theta(x)\supset\phi(x)));$ and
(b) $\Sigma\models[\delta]\forall
x(\mathitbf{K}\theta(x)\lor\mathitbf{K}\neg\theta(x)).$

That is, the agent knows whether $x$ is a male or not, for every $x.$

_Example._ Consider $\delta=isMale(n)\cdot isMale(n^{\prime})\cdot
approve(n)\cdot approve(n^{\prime})$. It implements strong DP for $hasLoan(x)$
wrt attribute $isMale(x).$ Of course, by definition, $\delta$ also implements
DP for $hasLoan(x).$

FTU-DP. In general, since we do not wish the agent to know the values of
protected attributes, vanilla DP is more attractive. Formally, we may impose a
FTU-style constraint of not knowing on any fairness definition. For example,
_Definition._ A sequence $\delta=a_{1}\cdots a_{k}$ implements FTU-DP for
$\phi(x)$ wrt attribute $\theta(x)$ iff: (a)
$\Sigma\models[\delta]\mathitbf{K}((\forall
x\theta(x)\supset\phi(x))\land(\forall x\neg\theta(x)\supset\phi(x)))$; and
(b) for every $\delta^{\prime}\leq\delta$:
$\Sigma\models[\delta^{\prime}]\neg\exists x\mathitbf{K}\theta(x).$

Again, it is worth remarking that mixing and matching constraints is
straightforward in a logic, and the semantical apparatus provides us with the
tools to study the resulting properties.

_Example._ The example for de-dicto DP is applicable here too. Consider
$\delta=approve(n)\cdot approve(n^{\prime})$. It implements FTU-DP for
$hasLoan(x)$ wrt attribute $isMale(x).$ That is, (a) $\Sigma\not\models\exists
x\mathitbf{K}\theta(x);$ (b) $\Sigma\not\models[approve(n)]\exists
x\mathitbf{K}\theta(x);$ and (c) $\Sigma\not\models[approve(n)\cdot
approve(n^{\prime})]\exists x\mathitbf{K}\theta(x).$ Reversing the actions,
not surprisingly, $\delta^{\prime}=approve(n^{\prime})\cdot approve(n)$ does
not affect the matter: $\delta^{\prime}$ also implements FTU-DP. Had the
sequence including sensing, a reversal could matter.

One can also consider situations where some knowledge of protected attributes
is useful to ensure there is parity but to also account for special
circumstances. In this, the protected attribute itself could be “hidden” in a
more general class, which is easy enough to do in a relational language.

_Example._ Suppose we introduce a new predicate for underrepresented groups.
We might have, for example: $\forall x(\neg Male(x)\lor\ldots\lor
RaceMinority(x)\supset Underrepresented(x)).$ This could be coupled with a
sensing axiom of the sort: $\Box{\mathit{S}F}(checkU(x))\equiv
Underrepresented(x).$ Add the predicate definition and the sensing axioms to
the initial theories and dynamic axioms in $\Sigma$ respectively. Consider
$\delta=checkU(n)\cdot checkU(n^{\prime})\cdot approve(n)\cdot
approve(n^{\prime}).$ Then $\delta$ implements strong DP for $hasLoan(x)$ wrt
attribute $Underrepresented(x).$ That is, both represented and
underrepresented groups have loans.

Equality of opportunity. One problem with DP is that (unless the instance rate
of $y=1$ happens to be the same in both the $a_{p}=0$ group and $a_{p}=1$
group), the classifier cannot achieve $100\%$ classification accuracy and
satisfy the fairness criterion simultaneously (Hardt et al. 2016). Also, there
are scenarios where this definition is completely inappropriate because the
instance rate of $y=1$ differs so starkly between different demographic
groups. Finally, there are also concerns that statistical parity measures fail
to account for fair treatment of individuals (Dwork et al. 2011). Nonetheless
it is often regarded as the most appropriate statistical definition when an
algorithm is trained on historical data (Zafar et al. 2017b; Zemel et al.
2013).

A modification of demographic parity is “equality of opportunity” (EO). By
this definition, a classifier is considered fair if, among those individuals
who meet the positive criterion, the instance rate of correct prediction is
identical, regardless of the value of the protected attribute (Hardt et al.
2016). This condition can be expressed as (Hardt et al. 2016):
$P(y=1|a_{p}=a,\hat{y}=1)=P(y=1|a_{p}=a^{\prime},\hat{y}=1)\hskip
5.69054pt\forall\hskip 2.84526pta,a^{\prime}$. In (Hardt et al. 2016), it is
pointed out that a classifier can simultaneously satisfy equality of
opportunity and achieve perfect prediction whereby $\hat{y}=y$
(prediction=true label) in all cases.

In the logical setting, this can be seen as a matter of only looking at
individuals that satisfy a criterion, such as being eligible for promotion or
not being too old to run for office.

_Definition._ A sequence $\delta$ implements EO for $\phi(x)$ wrt attribute
$\theta(x)$ and criterion $\eta(x)$ iff:

$\Sigma\models[\delta]\mathitbf{K}((\forall
x(\eta(x)\land\theta(x))\supset\phi(x))\land(\forall
x\neg(\eta(x)\land\theta(x))\supset\phi(x))).$

_Example._ Consider $\delta=promote(n)\cdot promote(n^{\prime})$, let
$\phi(x)=highSalary(x)$ and the criterion $\eta(x)=Eligible(x).$ Although the
promote action for $n^{\prime}$ does not lead her to obtain a high salary,
because we condition the definition only for eligible individuals, $\delta$
does indeed implement EO. Note again that the agent does not know the gender
for $n^{\prime}$, but in every possible world, regardless of the gender
$n^{\prime}$ is assigned, $n^{\prime}$ is known to be ineligible. In contrast,
$n$ is eligible and $\delta$ leads to $n$ having a high salary. That is, every
eligible male now has high salary, and every eligible female also has high
salary. (It just so happens there are no eligible females, but we will come to
that.)

In general, the equality of opportunity criterion might well be better applied
in instances where there is a known underlying discrepancy in positive
outcomes between two different groups, and this discrepancy is regarded as
permissible. However, as we might observe in our background theory, there is
systematic bias in that no women is considered eligible.

Counterfactual fairness. Let us now turn to CF. The existing definition forces
us to consider a “counterfactual world” where the protected attribute values
are reversed, and ensure that the action sequence still achieves the goal.

_Definition._ A sequence $\delta=a_{1}\cdots a_{k}$ implements CF for $\phi$
wrt attribute $\theta(x)$ for individual $n$ iff:

  * •

$\Sigma\models(\theta(n)=b)$ for $b\in\left\\{0,1\right\\}$ and
$\Sigma\models[\delta]\mathitbf{K}\phi$; and

  * •

${\mathit{F}orget}(\Sigma,\theta(n))\land(\theta(n)\neq
b)\models[\delta]\mathitbf{K}\phi$.

_Example._ Let us consider the case of loan approvals. Consider the individual
$n$ and the action $\delta=approve(n)$. Let $\phi=hasLoan(n)$, and the
protected attribute $Male(x)$. Clearly $\Sigma\models Male(n)$, and indeed
$\Sigma\models[\delta]hasLoan(n)$. If we consider $\Sigma^{\prime}$ where the
gender for $n$ is swapped, it is still the case that
$\Sigma^{\prime}\models[\delta]hasLoan(n)$. Thus $\delta$ implements CF for
$hasLoan(n)$ wrt $Male(n)$.

The definition of CF is well-intentioned, but does not quite capture
properties that might enable equity. Indeed, there is a gender imbalance in
the theory, in the sense that only the male employee is eligible for
promotions and the female employee can never become eligible. Yet CF does not
quite capture this. Let us revisit the example with getting high salaries:

_Example._ Consider $\delta=promote(n)$ for property $highSalary(n)$ wrt
attribute $Male(n)$. It is clear that $\delta$ implements CF because the
gender is irrelevant given that $n$ is eligible. However, given
$\delta^{\prime}=promote(n^{\prime})$, we see that $\delta^{\prime}$ does not
implement CF for $highSalary(n^{\prime})$ wrt $Male(n^{\prime})$. Because
$n^{\prime}$ is not eligible, $highSalary(n^{\prime})$ does not become true
after the promotion.

Equity. Among the many growing criticisms about formal definitions of fairness
is that notions such as CF fail to capture systemic injustices and imbalances.
We do not suggest that formal languages would address such criticisms, but
they provide an opportunity to study desirable augmentations to the initial
knowledge or action theory.

Rather than propose a new definition, let us take inspiration from DP, which
seems fairly reasonable except that it is the context of what the agent knows.
Keeping in mind a desirable “positive” property such as $Eligible(x)$, let us
consider DP but at the world-level:

_Definition._ Given a theory $\Sigma$, protected attribute $\theta(x)$,
positive property $\eta(x)$, where $x$ is the individual, define _strong
equity_ : $\Sigma\models\forall x(\theta(x)\supset\eta(x))\land\forall
x(\neg\theta(x)\supset\eta(x)).$

In general, it may not be feasible to ensure that properties hold for all
instances of both genders. For example, there may be only a handful of C-level
executives, and we may wish that there are executives of both genders.

_Definition._ Given a theory $\Sigma$, protected attribute $\theta(x)$,
positive property $\eta(x)$, where $x$ is the individual, define _weak equity_
: $\Sigma\models\exists x(\theta(x)\land\eta(x))\land\exists
x(\neg\theta(x)\land\eta(x)).$ It is implicitly assumed that the set of
positive and negative instances for $\theta(x)$ is non-empty: that is, assume
the integrity constraint: $\Sigma\models\exists
x,y(\theta(x)\land\neg\theta(y)).$

We assume weak equity and focus on FTU below. The definitions could be
extended to strong equity or other fairness notions depending on the modelling
requirements.

_Definition._ A sequence $\delta=a_{1}\cdots a_{k}$ implements equitable FTU
for $\phi$ wrt protected attribute $\theta(x)$ and property $\eta(x)$ iff (a)
either weak equity holds in $\Sigma$ and $\delta$ implements FTU; or (b)
$\delta$ implements equitable FTU for $\phi$ wrt $\theta(x)$ and $\eta(x)$ for
the updated theory ${\mathit{F}orget}(\Sigma,S)$, where
$S=\left\\{\eta(n_{i})\mid i\in N\right\\}.$

Note that we are assuming that $N$ is finite here because we have only defined
forgetting wrt finitely many atoms. Otherwise, we would need a second-order
definition.

_Example._ Consider $\delta=promote(n)\cdot promote(n^{\prime})$ for goal
$\phi=\forall x(highSalary(x))$ wrt protected attribute $Male(x)$ and property
$Eligible(x)$. It is clear that weak equity does not hold for $\Sigma$ because
there is a female who is not eligible. In this case, consider
$\Sigma^{\prime}={\mathit{F}orget}(\Sigma,S)$ where
$S=\left\\{Eligible(n),Eligible(n^{\prime})\right\\}.$ And with that,
$\Sigma^{\prime}$ also does not mention that $n$ is eligible, so the promotion
actions does not lead to anyone having high salaries. So $\delta$ does not
enable knowledge of $\phi.$

_Example._ Let us consider $\Sigma^{\prime}$ that is like $\Sigma$ except that
$Eligible(x)$ is not rigid, and can be affected using the action $make(x)$:
$\Box[a]Eligible(x)\equiv Eligible(x)\lor(a=make(x)).$ That is, either an
individual is eligible already or the manager makes them. Of course,
$\delta=promote(n)\cdot promote(n^{\prime})$ from above still does not
implement equitable FTU, because we have not considered any actions yet to
make individuals eligible. However, consider $\delta^{\prime}=make(n)\cdot
make(n^{\prime})\cdot promote(n)\cdot promote(n^{\prime})$. Because $\Sigma$
does not satisfy weak equity, we turn to the second condition of the
definition. On forgetting, no one is eligible in the updated theory, but the
first two actions in $\delta^{\prime}$ makes both $n$ and $n^{\prime}$
eligible, after which, they are both promoted. So $\delta^{\prime}$ enables
knowledge of $\forall x(highSalary(x))$. Thus, the actions have made clear
that eligibility is the first step in achieving gender balance, after which
promotions guarantee that there are individuals of both genders with high
salaries.

sec:conclusions

##  6 Conclusions

In this paper, we looked into notions of fairness from the machine learning
literature, and inspired by these, we attempted a formalization in an
epistemic logic. Although we limited ourselves to categorical knowledge and
noise-free observations, we enrich the literature by considering actions.
Consequently we looked into three notions: fairness through unawareness,
demographic parity and counterfactual fairness, but then expanded these
notions to also tackle equality of opportunity as well as equity. We were also
able to mix and match constraints, showing the advantage of a logical
approach, where one can formally study the properties of (combinations of)
definitions. Using a simple basic action theory we were nonetheless able to
explore these notions using action sequences.

As mentioned earlier, this is only a first step and as argued in works such as
(Pagnucco et al. 2021; Dehghani et al. 2008; Halpern and Kleiman-Weiner 2018)
there is much promise in looking at ethical AI using rich logics. In fact, we
did not aim to necessarily faithfully reconstruct existing ML notions in this
paper but rather study underlying principles. This is primarily because we are
not focusing on single-shot prediction problems but how actions, plans and
programs might implement fairness and de-biasing. The fact that fairness was
defined in terms of actions making knowledge of the goal true, exactly as one
would in planning (Levesque 1996), is no accident.

State-of-the-art analysis in fairness is now primarily based on false
positives and false negatives (Verma and Rubin 2018). So we think as the next
step, a probabilistic language such as (Bacchus et al. 1999) could bring our
notions closer to mainstream definitions, but now in the presence of actions.
In the long term, the goal is to logically capture bias in the presence of
actions as well as repeated harms caused by systemic biases (Creager et al.
2020). Moreover, the use of logics not only serve notions such as verification
and correctness, but as we argue, could also provide a richer landscape for
exploring ethical systems, in the presence of background knowledge and
context. This would enable the use of formal tools (model theory, proof
strategies and reasoning algorithms) to study the long-term impact of bias
while ensuring fair outcomes throughout the operational life of autonomous
agents embedded in complex socio-technical applications.

Of course, a logical study such as ours perhaps has the downside that the
language of the paper is best appreciated by researchers in knowledge
representation, and not immediately accessible to a mainstream machine
learning audience. But on the other hand, there is considerable criticism
geared at single-shot prediction models for not building in sufficient context
and commonsense. In that regard, operationalising a system that permits a
declaration of the assumptions and knowledge of the agents and their actions
might be exactly “what the doctor ordered.” See also efforts in causal
modelling (Chockler and Halpern 2004) that are close in spirit.

## References

  * Alexander and Moore (2016) Larry Alexander and Michael Moore.  Deontological ethics.  In _The Stanford Encyclopedia of Philosophy_. 2016.
  * Anderson and Anderson (2014) Michael Anderson and Susan Leigh Anderson.  Geneth: A general ethical dilemma analyzer.  In _Proceedings of the 28th AAAI Conference on Artificial Intelligence_ , pages 253–261, 2014.
  * Angwin et al. (2016) J. Angwin, J. Larson, S. Mattu, and L. Kirchner.  “machine bias: There’s software used across the country to predict future criminals. and it’s biased against blacks.”.  2016\.
  * Aziz et al. (2018) Haris Aziz, Sylvain Bouveret, Ioannis Caragiannis, Ira Giagkousi, and Jérôme Lang.  Knowledge, fairness, and social constraints.  In _Proceedings of the AAAI Conference on Artificial Intelligence_ , volume 32, 2018.
  * Bacchus et al. (1999) F. Bacchus, J. Y. Halpern, and H. J. Levesque.  Reasoning about noisy sensors and effectors in the situation calculus.  _Artificial Intelligence_ , 111(1–2):171 – 208, 1999.
  * Bacchus et al. (1996) Fahiem Bacchus, Adam J Grove, Joseph Y Halpern, and Daphne Koller.  From statistical knowledge bases to degrees of belief.  _Artificial intelligence_ , 87(1-2):75–143, 1996\.
  * Baier et al. (2007) Jorge A. Baier, Christian Fritz, and Sheila A. McIlraith.  Exploiting procedural domain control knowledge in state-of-the-art planners.  In _Proc. ICAPS_ , pages 26–33, 2007.  URL http://www.aaai.org/Library/ICAPS/2007/icaps07-004.php.
  * Baral et al. (2017) Chitta Baral, Thomas Bolander, Hans van Ditmarsch, and Sheila McIlrath.  Epistemic Planning (Dagstuhl Seminar 17231).  _Dagstuhl Reports_ , 7(6):1–47, 2017.  ISSN 2192-5283.  10.4230/DagRep.7.6.1.  URL http://drops.dagstuhl.de/opus/volltexte/2017/8285.
  * Batusov and Soutchanski (2018) Vitaliy Batusov and Mikhail Soutchanski.  Situation calculus semantics for actual causality.  In _Proceedings of the AAAI Conference on Artificial Intelligence_ , volume 32, 2018.
  * Belle and Lakemeyer (2017) V. Belle and G. Lakemeyer.  Reasoning about probabilities in unbounded first-order dynamical domains.  In _IJCAI_ , 2017.
  * Belle (2022) Vaishak Belle.  Analyzing generalized planning under nondeterminism.  _Artificial Intelligence_ , page 103696, 2022.
  * Broersen et al. (2001) Jan Broersen, Mehdi Dastani, Joris Hulstijn, Zisheng Huang, and Leendert van der Torre.  The boid architecture: conflicts between beliefs, obligations, intentions and desires.  In _Proceedings of the fifth international conference on Autonomous agents_ , pages 9–16, 2001.
  * Chockler and Halpern (2004) Hana Chockler and Joseph Y Halpern.  Responsibility and blame: A structural-model approach.  _Journal of Artificial Intelligence Research_ , 22:93–115, 2004.
  * Chouldechova (2017) A. Chouldechova.  Fair prediction with disparate impact: A study of bias in recidivism prediction instruments.  In _Big Data, Volume 5, No. 2: 153–163_ , 2017.
  * Classen (2018) Jens Classen.  Symbolic verification of Golog programs with first-order BDDs.  In Michael Thielscher, Francesca Toni, and Frank Wolter, editors, _Proceedings of the Sixteenth International Conference on Principles of Knowledge Representation and Reasoning (KR 2018)_ , pages 524–528. AAAI Press, 2018.  URL http://jens-classen.net/pub/Classen2018.pdf.
  * Classen and Delgrande (2020) Jens Classen and James Delgrande.  Dyadic obligations over complex actions as deontic constraints in the situation calculus.  In _Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning_ , volume 17, pages 253–263, 2020.
  * Classen and Lakemeyer (2008) Jens Classen and Gerhard Lakemeyer.  A logic for non-terminating golog programs.  In _KR_ , pages 589–599, 2008.
  * Classen et al. (2008) Jens Classen, Viktor Engelmann, Gerhard Lakemeyer, and Gabriele Röger.  Integrating Golog and planning: An empirical evaluation.  In _NMR Workshop_ , pages 10–18, 2008.
  * Conway and Gawronski (2013) Paul Conway and Bertram Gawronski.  Deontological and utilitarian inclinations in moral decision making: a process dissociation approach.  _Journal of Personality and Social Psychology_ , 104(2):216, 2013.
  * Creager et al. (2020) Elliot Creager, David Madras, Toniann Pitassi, and Richard Zemel.  Causal modeling for fairness in dynamical systems.  In _International Conference on Machine Learning_ , pages 2185–2195. PMLR, 2020.
  * Czelakowski (1997) Janusz Czelakowski.  Action and deontology.  In _Logic, action and cognition_ , pages 47–87. Springer, 1997.
  * Dehghani et al. (2008) Morteza Dehghani, Emmett Tomai, Kenneth D Forbus, and Matthew Klenk.  An integrated reasoning approach to moral decision-making.  In _Proceedings of the 23rd AAAI Conference on Artificial Intelligence_ , pages 1280–1286, 2008.
  * Delgrande and Levesque (2012) James P. Delgrande and Hector J. Levesque.  Belief revision with sensing and fallible actions.  In _Proc. KR_ , 2012.
  * Dwork et al. (2011) C. Dwork, M. Hardt, T. Pitassi, O. Reingold, and R. Zemel.  Fairness through awareness.  In _Innovations in Theoretical Computer Science Conference_ , 2011\.
  * Farnadi et al. (2018) Golnoosh Farnadi, Behrouz Babaki, and Lise Getoor.  Fairness in relational domains.  In _Proceedings of the 2018 AAAI/ACM Conference on AI, Ethics, and Society_ , pages 108–114, 2018.
  * Fu et al. (2020) Zuohui Fu, Yikun Xian, Ruoyuan Gao, Jieyu Zhao, Qiaoying Huang, Yingqiang Ge, Shuyuan Xu, Shijie Geng, Chirag Shah, Yongfeng Zhang, et al.  Fairness-aware explainable recommendation over knowledge graphs.  In _Proceedings of the 43rd International ACM SIGIR Conference on Research and Development in Information Retrieval_ , pages 69–78, 2020.
  * Georgeff et al. (1998) Michael Georgeff, Barney Pell, Martha Pollack, Milind Tambe, and Michael Wooldridge.  The belief-desire-intention model of agency.  In _International workshop on agent theories, architectures, and languages_ , pages 1–10. Springer, 1998.
  * Halpern and Moses (2014) J. Y. Halpern and Y. Moses.  A procedural characterization of solution concepts in games.  _JAIR_ , 49:143–170, 2014.
  * Halpern et al. (2009) J. Y. Halpern, R. Pass, and V. Raman.  An epistemic characterization of zero knowledge.  In _TARK_ , pages 156–165, 2009.
  * Halpern and Kleiman-Weiner (2018) Joseph Y Halpern and Max Kleiman-Weiner.  Towards formal definitions of blameworthiness, intention, and moral responsibility.  In _Proceedings of the 32nd AAAI Conference on Artificial Intelligence_ , pages 1853–1860, 2018.
  * Hardt et al. (2016) M. Hardt, E. Price, and N. Srebro.  Equality of opportunity in supervised learning.  In _International Conference on Neural Information Processing Systems_ , 2016.
  * Hooker and Kim (2018) John N Hooker and Tae Wan N Kim.  Toward non-intuition-based machine and artificial intelligence ethics: A deontological approach based on modal logic.  In _Proceedings of the 2018 AAAI/ACM Conference on AI, Ethics, and Society_ , pages 130–136, 2018.
  * Ignatiev et al. (2020) Alexey Ignatiev, Martin C Cooper, Mohamed Siala, Emmanuel Hebrard, and Joao Marques-Silva.  Towards formal fairness in machine learning.  In _Principles and Practice of Constraint Programming: 26th International Conference, CP 2020, Louvain-la-Neuve, Belgium, September 7–11, 2020, Proceedings 26_ , pages 846–867. Springer, 2020.
  * Kawamoto (2019) Yusuke Kawamoto.  Towards logical specification of statistical machine learning.  In _Software Engineering and Formal Methods: 17th International Conference, SEFM 2019, Oslo, Norway, September 18–20, 2019, Proceedings_ , pages 293–311. Springer, 2019.
  * Khandani et al. (2010) A.E. Khandani, J. Kim, and A.W. Lo.  Consumer credit-risk models via machine-learning algorithms.  In _Journal of Banking and Finance 34_ , 2010.
  * Kusner et al. (2017) M. Kusner, J. Loftus, C. Russel, and R. Silva.  Counterfactual fairness.  _Neural Information Processing Systems_ , 2017.
  * Lakemeyer and Levesque (2007) G. Lakemeyer and H. J. Levesque.  Cognitive robotics.  In _Handbook of Knowledge Representation_ , pages 869–886. Elsevier, 2007.
  * Lakemeyer and Levesque (2011) G. Lakemeyer and H. J. Levesque.  A semantic characterization of a useful fragment of the situation calculus with knowledge.  _Artificial Intelligence_ , 175:142–164, 2011.  ISSN 0004-3702.
  * Lakemeyer and Levesque (2004) G. Lakemeyer and Hector J. Levesque.  Situations, Si! situation terms, No!  In _Proc. KR_ , pages 516–526, 2004.
  * Lee and Palla (2012) Joohyung Lee and Ravi Palla.  Reformulating the situation calculus and the event calculus in the general theory of stable models and in answer set programming.  _Journal of Artificial Intelligence Research_ , 43:571–620, 2012.
  * Lespérance et al. (2000) Y. Lespérance, H. J. Levesque, F. Lin, and R. B. Scherl.  Ability and knowing how in the situation calculus.  _Studia Logica_ , 66(1):165–186, 2000.
  * Levesque et al. (1997) H. Levesque, R. Reiter, Y. Lespérance, F. Lin, and R. Scherl.  Golog: A logic programming language for dynamic domains.  _Journal of Logic Programming_ , 31:59–84, 1997.  URL GOLOGlang.pdf.
  * Levesque (1990) H. J. Levesque.  All I know: a study in autoepistemic logic.  _Artificial Intelligence_ , 42(2-3):263–309, 1990\.  ISSN 0004-3702.
  * Levesque (1996) H. J. Levesque.  What is planning in the presence of sensing?  In _Proc. AAAI / IAAI_ , pages 1139–1146, 1996.
  * Lin and Reiter (1994) F. Lin and R. Reiter.  Forget it.  In _Working Notes of AAAI Fall Symposium on Relevance_ , pages 154–159, 1994.
  * Lindner et al. (2017) Felix Lindner, Martin Mose Bentzen, and Bernhard Nebel.  The hera approach to morally competent robots.  In _Proceedings of the IEEE/RSJ Intelligent Robots and Systems_ , pages 6991–6997, 2017.
  * Liu and Lorini (2022) Xinghan Liu and Emiliano Lorini.  A logic of “black box” classifier systems.  In _Logic, Language, Information, and Computation: 28th International Workshop, WoLLIC 2022, Iași, Romania, September 20–23, 2022, Proceedings_ , pages 158–174. Springer, 2022.
  * McIlraith and Son (2002) Sheila A. McIlraith and Tran Cao Son.  Adapting golog for composition of semantic web services.  In _KR_ , pages 482–496, 2002.
  * Muggleton et al. (2012) Stephen Muggleton, Luc De Raedt, David Poole, Ivan Bratko, Peter Flach, Katsumi Inoue, and Ashwin Srinivasan.  Ilp turns 20.  _Machine learning_ , 86(1):3–23, 2012.
  * Muise et al. (2015) C. Muise, V. Belle, P. Felli, S. McIlraith, T. Miller, A. Pearce, and L. Sonenberg.  Planning over multi-agent epistemic states: A classical planning approach.  In _Proc. AAAI_ , 2015.
  * Pagnucco et al. (2021) Maurice Pagnucco, David Rajaratnam, Raynaldio Limarga, Abhaya Nayak, and Yang Song.  Epistemic reasoning for machine ethics with situation calculus.  In _Proceedings of the 2021 AAAI/ACM Conference on AI, Ethics, and Society_ , pages 814–821, 2021.
  * Pedreschi et al. (2008) D. Pedreschi, S. Ruggieri, and F. Turini.  Discrimination aware data mining.  In _14th ACM SIGKDD international conference on Knowledge Discovery and Data Mining_ , 2008.
  * Raedt et al. (2016) Luc De Raedt, Kristian Kersting, Sriraam Natarajan, and David Poole.  Statistical relational artificial intelligence: Logic, probability, and computation.  _Synthesis lectures on artificial intelligence and machine learning_ , 10(2):1–189, 2016.
  * Reiter (2001a) R. Reiter.  On knowledge-based programming with sensing in the situation calculus.  _ACM Trans. Comput. Log._ , 2(4):433–457, 2001a.
  * Reiter (2001b) R. Reiter.  _Knowledge in action: logical foundations for specifying and implementing dynamical systems_.  MIT Press, 2001b.
  * Sardina et al. (2004) S. Sardina, G. De Giacomo, Y. Lespérance, and H. J. Levesque.  On the semantics of deliberation in indigolog—from theory to implementation.  _Annals of Mathematics and Artificial Intelligence_ , 41(2-4):259–299, 2004.
  * Sardina and Lespérance (2010) Sebastian Sardina and Yves Lespérance.  Golog speaks the bdi language.  In _Programming Multi-Agent Systems_ , volume 5919 of _LNCS_ , pages 82–99. Springer Berlin Heidelberg, 2010.  ISBN 978-3-642-14842-2.
  * Scherl and Levesque (2003) R. B. Scherl and H. J. Levesque.  Knowledge, action, and the frame problem.  _Artificial Intelligence_ , 144(1-2):1–39, 2003\.  ISSN 0004-3702.
  * Verma and Rubin (2018) Sahil Verma and Julia Rubin.  Fairness definitions explained.  In _2018 ieee/acm international workshop on software fairness (fairware)_ , pages 1–7. IEEE, 2018.
  * Wang and Zhang (2005) Kewen Wang and Yan Zhang.  Nested epistemic logic programs.  In _International Conference on Logic Programming and Nonmonotonic Reasoning_ , pages 279–290. Springer, 2005.
  * Zafar et al. (2017a) M. B. Zafar, I. Valera, M. G. Rodriguez, and K. P. Gummadi.  Fairness beyond disparate treatment & disparate impact: Learning classification without disparate mistreatment.  In _International Conference on World Wide Web_ , 2017a.
  * Zafar et al. (2017b) M. B. Zafar, I. Valera, M. G. Rodriguez, and K. P. Gummadi.  International conference on artificial intelligence and statistics.  In _Fairness Constraints: Mechanisms for Fair Classification_ , 2017b.
  * Zemel et al. (2013) R. Zemel, Y. Wu, K. Swersky, and T. Pitassi.  Learning fair representations.  In _International Conference on Machine Learning_ , 2013.
  * Zhang and Zhou (2009) Yan Zhang and Yi Zhou.  Knowledge forgetting: Properties and applications.  _Artificial Intelligence_ , 173(16-17):1525–1537, 2009.