# A search for new dwarf galaxies outside the nearby groups

I.D. Karachentsev<EMAIL_ADDRESS>Special Astrophysical Observatory, Russian
Academy of Sciences, Nizhnii Arkhyz, 369167 Russia  V.E. Karachentseva  Main
Astronomical Observatory, National Academy of Sciences of Ukraine, Kiev 03143,
Ukraine  S.S. Kaisin  Special Astrophysical Observatory, Russian Academy of
Sciences, Nizhnii Arkhyz, 369167 Russia  E.I. Kaisina  Special Astrophysical
Observatory, Russian Academy of Sciences, Nizhnii Arkhyz, 369167 Russia

###### Abstract

We undertook a search for new nearby dwarf galaxies outside the known groups
in the Local Volume using the data on DESI Legacy Imaging Surveys. In a wide
sky area of $\sim$5000 square degrees directed toward the Local Void, we found
only 12 candidates to nearby low mass galaxies. Almost all of them are
classified as irregular or transition type dwarfs. Additionally, we examined
areas of the sky exposed with the Hyper Suprime Camera of the Subaru telescope
($\sim$700 square degrees) and found nine more candidates to nearby dwarfs.
Finally, nine candidates to the Local Volume were selected by us from the
Zaritsky’s SMUDG catalog that contains 7070 ultra-diffuse objects
automatically detected in the whole area of the DESI surveys. We estimated a
fraction of quiescent dSph galaxies in the general cosmic field to be less
than 10 percent.

galaxies: dwarf—galaxies: groups: general—surveys

##  1 Introduction

According to modern ideas, the spatial distribution of galaxies is similar to
a cosmic ”web”, where particles (galaxies) are concentrated in filaments and
walls that encompass large cosmic voids. Groups and clusters form at the
intersection of filaments and walls [1, 2]. Catalogs of groups and clusters in
the nearby universe show that about half of all galaxies are part of
virialized systems of varying populations, and about 15% more galaxies are
located in larger collapsing regions around groups, not participating in the
global cosmological expansion [3–5]. Thus, about one-third of galaxies are
located in the general metagalactic field and do not noticeably interact with
each other.

General field galaxies are of particular interest because the star formation
history in them follows a different scenario than the evolution of members of
virialized systems. The most suitable object to study these differences is the
Local Volume (LV) with a radius of $\sim$10 Mpc around the Milky Way, where
observational data on galaxies are the most complete. By now, the number of
known galaxies in this volume has approached a thousand [6] and continues to
increase due to new surveys of the sky in optical and radio bands.

Most searches for new close dwarf galaxies have been undertaken in the region
of known close groups [7–10]. This approach led to increase the statistics of
the ”test particles” used to determine the virial mass of the groups, thus
making a more complete picture of the dark matter distribution in the LV.

Searches for dwarf galaxies not bound to nearby groups have been repeatedly
undertaken [11–18]. A summary of observational data on the LV galaxies is
presented in the Updated Nearby Galaxy Catalog (=UNGC, [6]) and the Local
Volume Galaxy Database [19], the latest updated version of which is available
at http://www.sao.ru/lv/lvgdb.

An obvious advantage of searching for dwarf galaxies in groups and clusters is
the ability to assign to new objects a likely distance estimate that coincides
with the group mean distance. In the general field dwarfs, their distance and
total luminosity remain uncertain until the radial velocity is measured or
structural features (e.g. globular clusters) suitable as distance indicators
are found. In the LV, the best method is to measure the distance by the
luminosity of the tip of red giant branch (TRGB). This method, used in the
Hubble Space Telescope (HST) observations, can measure the distance for any
type of galaxy in the LV with an accuracy of $\sim$5% or $\sim$(0.3–0.5) Mpc,
allowing us to confidently separate field galaxies against group members.

##  2 Searches for new dwarf galaxies in the Local Volume

###  2.1 The Local Void region

Table 1: LV candidates outside the neighboring groups Name | RA (2000.0) DEC | $a^{\prime}$ | $b/a$ | Type | $m_{\rm FUV}$ | $m_{\rm NUV}$ | $B$ | $g$ | $r$ | Notes
---|---|---|---|---|---|---|---|---|---|---
| h m s deg ′ ′′ | arcmin |  |  | mag | mag | mag | mag | mag |
(1) | (2) | (3) | (4) | (5) | (6) | (7) | (8) | (9) | (10) | (11)
SMDG0956+82 | 09 56 13.0 +82 53 24 | 0.70 | 0.60 | Irr | 19.64 | 19.33 | 18.08 | 17.75 | 17.42 | (1)
Dw1155+78 | 11 55 54.2 +78 04 44 | 0.58 | 0.73 | Tr |  $>$23.5 | — | 19.61 | 19.18 | 18.54 | —
Dw1234+76 | 12 34 23.3 +76 43 34 | 0.96 | 0.58 | Irr | 21.76 | 21.55 | 17.9 | 17.58 | - | (1)
Dw1339+39 | 13 39 45.1 +39 08 09 | 0.60 | 0.66 | Irr | 18.65 | 18.38 | 17.68 | 17.45 | 17.51 | (2)
SMDG1349+04 | 13 49 16.8 +04 49 05 | 0.72 | 0.73 | Tr |  $>$23.5 2 | 1.88 | 18.88 | 18.53 | 18.16 | —
Dw1459+44 | 14 59 38.4 +44 40 23 | 1.43 | 0.95 | BCD | 17.02 | 16.91 | 17.07 | 16.8 | 16.78 | (3)
UGC9893sat | 15 32 51.4 +46 25 55 | 0.71 | 0.79 | Irr |  $>$23.5 | 22.05 | 20.63 | 20.22 | 19.62 | (4)
Dw1533+67 | 15 33 28.1 +67 45 29 | 0.83 | 0.46 | Irr | 19.36 | 19.06 | 17.89 | 17.59 | 17.35 | —
Dw1559+46 | 15 59 02.6 +46 23 40 | 0.60 | 0.88 | Irr | — | — | 17.19 | 16.90 | 16.70 | (1)
Dw1645+46 | 16 45 48.5 +46 47 24 | 0.74 | 0.67 | Irr | 19.71 | 19.48 | 17.93 | 17.63 | 17.40 | (1)
Dw1709+74 | 17 09 45.6 +74 10 44 | 1.39 | 0.81 | Tr | 21.35 | 20.79 | 17.46 | 17.04 | 16.43 | (5)
Dw1735+57 | 17 35 34.6 +57 48 47 | 0.69 | 0.66 | Irr | 18.35 | 18.15 | 17.07 | 16.74 | 16.40 | —
Notes: (1) — granulated; (2) — near a bright star; the object is located at
16′ to West from UGC 9660
that has $V_{h}=608$ km/s and $D$ = 10.76 Mpc via TRGB; (3) — a compact dwarf
with an extended halo,
$V_{h}=683$ km/s; (4) — the object has a very low surface brightness; it is
only 2′ SW from UGC9893;
(5) — probably a distant dwarf.
Figure 1: Images of 12 new dwarf galaxies from DESI Legacy Imaging Surveys
found in the Local Void region. Each image size is
$2\hbox{${}^{\prime}$}\times 2\hbox{${}^{\prime}$}$. North is to the top and
East is to the left.

The publication of DESI Legacy Imaging Surveys [20] has provided an
opportunity to discover new LV dwarf candidates over an area of $\sim$14000
square degrees, covering about one third of the entire sky. We have already
used this survey to search for dwarf satellites around 46 relatively massive
LV galaxies [10]. This resulted in the discovery of 67 satellite candidates
for these galaxies, half of which turned out to be low surface brightness
spheroidal dwarfs (dSph) with no evidence of star formation. To search for new
dwarf galaxies in the local total field, we chose a wide region in the
direction of the Local Void, whose center according to [21] has approximate
equatorial coordinates RA $\simeq 18^{h}$, Dec. $\simeq 0^{\circ}$. Our survey
area covered the sky region RA $>13.5^{h}$, Dec. $>-5^{\circ}$, the eastern
side of which was bounded by the Milky Way band. Additionally, we inspected
the polar cap with Dec. $>+60^{\circ}$, avoiding the virial area of the known
nearby group around M81. In the inspected direction, there is another void
Draco-Cepheus [22] with its center at a distance of 14 Mpc. A panorama of the
large-scale matter distribution in this direction is shown by [2]. In total,
the area we inspected outside the nearby groups amounts to about 5000 square
degrees or 1/3 of the DESI Legacy Imaging Surveys. In this huge area, we
detected only 12 candidates for new LV dwarf galaxies. Their images are shown
as a mosaic in Fig. 1, where the size of each image corresponds to 2′.

The list of detected objects is given in Table 1, whose columns contain: (1) —
galaxy name; (2) — equatorial coordinates in h, m, s and deg,
$\hbox{${}^{\prime}$},\leavevmode\nobreak\ \hbox{${}^{\prime\prime}$}$; (3) —
a maximum apparent galaxy diameter in arc minutes; (4) — an apparent axial
ratio; (5) — morphological type: irregular (Irr), spheroidal (dSph), or
intermediate (transition) (Tr); (6,7) — apparent galaxy magnitudes in the
$FUV$ and $NUV$ bands of the GALEX Ultraviolet Sky Survey [23]; (8) — apparent
magnitude of the galaxy in the $B$-band; (9,10) — apparent magnitudes in the
$g$\- and $r$-bands; (11) — notes on the presence of the galaxy’s structure
features and close surroundings.

The total apparent $g$\- and $r$-magnitudes of galaxies were taken from the
SMUDG Ultra-Diffuse Galaxy Catalog [17] or from the Legacy Survey DR9
photometric data [20]. For some low surface brightness galaxies with patchy
structure, we have made $g$\- and $r$-magnitude measurements for galaxy images
from the DESI Legacy Imaging Surveys using the standard methods of processing
in the MIDAS software package from the European Southern Observatory. A
typical measurement error was about 0.10 mag. The total $B$-magnitude of
galaxies was determined using the ratio $B=g+0.313(g-r)+0.227$ recommended by
Lupton111https://www.sdss3.org/dr10/algorithms
/sdssUBVRITransform.php#Lupton2005. The median apparent magnitude of the
detected dwarf galaxies is $B\simeq 18^{m}$, which at the far edge of the LV
($D$ = 10 Mpc) corresponds to an absolute magnitude of $M_{B}\simeq-12^{m}$.
All of these dwarf galaxies appear to be rather isolated objects located far
away from other known members of the Local Volume. The only exception is a
very low surface brightness dwarf, UGC9893sat, which is almost in contact with
another peculiar dIrr galaxy UGC9893 = IZw115 = VV720 = KIG 686, which has a
distance estimate of 10.2 Mpc based on the Tully-Fisher relation between a
galaxy luminosity and its HI-line width. It is likely that these dwarf
galaxies form a physical pair at a stage close to their merger.

###  2.2 HSC survey areas

Among the DESI Legacy Imaging Surveys (http://www.legacysurvey.org/), there is
a series of sky areas exposed on the 8.5-meter Subaru telescope Hyper Suprime
Camera (HSC) with a deeper limit and higher angular resolution in comparison
with the Legacy surveys. The combined area of them is about 700 square
degrees. We inspected these regions of the sky and found 9 other LV dwarf
galaxy candidates. Their images are shown in Fig. 2, where each element of the
mosaic is $2\hbox{${}^{\prime}$}$ in size. The data on these objects are
compiled in Table 2, in which the column designations are the same as in Table
1. Some individual features of the galaxies are presented in notes to the
table. Among these objects there are only two dwarf galaxies of spheroidal
type. Of them, Dw0852-0210 may be a companion of the Sc galaxy UGC4640 having
a heliocentric velocity $V_{h}=3308$ km/s, and Dw1229+0144 may be a companion
of the Sbc galaxy NGC4536 with $V_{h}=1807$ km/s or be belong to peripheral
members of the Virgo cluster.

Table 2: LV candidates from survey of HSC-fields in DESI Legacy Imaging Surveys Name | RA (2000.0) DEC | $a^{\prime}$ | $b/a$ | Type | $m_{\rm FUV}$ | $m_{\rm NUV}$ | $B$ | $g$ | $r$ | Notes
---|---|---|---|---|---|---|---|---|---|---
| h m s deg ′ ′′ | arcmin |  |  | mag | mag | mag | mag | mag |
(1) | (2) | (3) | (4) | (5) | (6) | (7) | (8) | (9) | (10) | (11)
Dw0010-0112 | 00 10 26.4 $-$01 12 18 | 0.58 | 0.61 | Tr |  $>$23.5 | — | 20.58 | 20.2 | 19.7 | (1)
SMDG0220-00 | 02 20 48.2 $-$00 27 54 | 0.97 | 0.83 | Tr | 22.79 | 20.9 | 18.04 | 17.65 | 17.13 | (2)
SMDG0223-02 | 02 23 18.7 $-$02 03 25 | 0.66 | 0.67 | BCD | 23.5: | — | 18.68 | 18.32 | 17.93 | (3)
Dw0852-0210 | 08 52 35.5 $-$02 10 41 | 0.73 | 0.97 | Sph |  $>$23.5 | — | 20.01 | 19.55 | 18.8 | (4)
Dw1229+0144 | 12 29 22.1 $+$01 44 17 | 1.11 | 0.68 | Sph | 23.49 | 21.53 | 18.66 | 18.22 | 17.53 | (5)
Dw1235-0215 | 12 35 53.0 $-$02 15 54 | 0.64 | 0.82 | Irr | 20.13 | 20.04 | 19.02 | 18.7 1 | 8.39 | (6)
SMDG1245+01 | 12 45 52.3 $+$01 54 22 | 0.85 | 0.56 | Sph |  $>$23.5 | — | 18.01 | 17.61 | 17.05 | (7)
SMDG1256-00 | 12 56 35.8 $-$00 31 44 | 0.74 | 0.67 | Irr | 20.28 | 19.65 | 18.14 | 17.8 1 | 7.44 | (8)
Dw1416-0212 | 14 16 38.9 $-$02 12 04 | 0.81 | 0.89 | Im | 20.47 | 19.62 | 18.17 | 17.83 | 17.46 | (9)
Notes: (1) — there are some cirrus in its vicinity; (2) — $V_{h}=4400\pm 6000$
km/s from [24];
(3) — it is located at 20′ to NW from UGC 1862 that has $V_{h}=1383$ km/s; (4)
— very low
surface brightness; above the bright star; at 12′ to W there is a galaxy UGC
4640 with
$V_{h}=3309$ km/s; (5) — in contact with a bright star, may be a member of
Virgo cluster;
(6) — granulated, a probable satellite of the Sombrero galaxy; (7) —
granulated; at 40′ to W
there is a bright peculiar SB galaxy NGC 4643 with 3 tight dSphs and
$V_{h}=1333$ km/s
(the Virgo cluster members?); (8) — probably a peripheric member of the Virgo
cluster;
(9) — with a faint asymmetric envelope; not detected in HIPASS.

###  2.3 Candidate dwarf galaxies of the LV from the SMUDG catalog

The regions of the sky, where our search for new Local Volume candidates was
conducted, cover a significant part, but not the entire DESI Legacy Imaging
Surveys area. Therefore, we used data from the SMUDG catalog (Systematically
Measuring Ultra-Diffuse Galaxies, [24]) to continue our search. The latest
full version of this catalog [17] contains 7070 low surface brightness objects
automatically extracted from DR9 Legacy Survey images, with the results of
surface photometry of these objects presented in the $g$\- and $r$-bands. As
shown by our analysis, along with dwarf galaxies, the catalog includes a
number of fragments of interstellar cirrus. Visual inspection of the SMUDG
objects allowed us to identify 9 dwarf galaxies that can be located at a
distance $D\leq 12$ Mpc. The list of them is summarized in Table 3. The
content of its columns is analogous to the corresponding data in Tables 1 and
2. The images of these galaxies are reproduced in Fig. 3 in the same manner as
in the previous figures.

Among the 9 galaxies, one, KK220=AGC232003 has a radial velocity measurement,
$V_{\rm hel}=776\pm 6$ km/s, which allows us to estimate the galaxy distance
$D$=11.1 Mpc based on the Numerical Action Method model (NAM, [25]). According
to the table annotations, two dSph galaxies are well-isolated objects, while
the other two dSphs may be members of more distant systems outside the LV.

Figure 2: Images of 9 new dwarf galaxies found in areas of the Subaru telescope Hyper SuprimeCamera survey. Each image size is $2\hbox{${}^{\prime}$}\times 2\hbox{${}^{\prime}$}$. North is to the top and East is to the left. Table 3: LV candidates from Zaritsky+2023 catalog of ultra-diffuse galaxies. Name | RA (2000.0) DEC | $a^{\prime}$ | $b/a$ | Type | $m_{\rm FUV}$ | $m_{\rm NUV}$ | $B$ | $g$ | $r$ | Notes
---|---|---|---|---|---|---|---|---|---|---
| h m s deg ′ ′′ | arcmin |  |  | mag | mag | mag | mag | mag |
(1) | (2) | (3) | (4) | (5) | (6) | (7) | (8) | (9) | (10) | (11)
SMDG0740+40 | 07 40 23.0 $+$40 32 56 | 0.48 | 0.63 | Irr | 21.46 | — | 19.27 | 18.87 | 18.30 | (1)
SMDG1017-05 | 10 17 16.3 $-$05 29 53 | 0.69 | 0.72 | Sph |  $>$23.5 | — | 19.17 | 18.75 | 18.13 | (2)
SMDG1103+60 | 11 03 56.4 $+$60 29 53 | 0.43 | 0.64 | Irr | — | — | 19.48 | 19.16 | 18.88 | —
SMDG1110+18 | 11 10 55.0 $+$18 58 52 | 0.63 | 0.83 | Sph |  $>$23.5 | — | 18.53 | 18.14 | 17.61 | (2)
SMDG1221+28 | 12 21 49.7 $+$28 31 12 | 0.47 | 0.74 | Sph |  $>$23.5 | — | 19.35 | 18.95 | 18.39 | (3)
SMDG1241+35 | 12 41 11.0 $+$35 11 46 | 0.73 | 0.92 | Irr | 21.8 | 21.08 | 18.90 | 18.53 | 18.09 | —
SMDG1250+07 | 12 50 26.9 $+$07 44 35 | 1.33 | 0.54 | Sph |  $>$23.5 | — | 17.99 | 17.53 | 16.78 | (4)
SMDG1345+33 | 13 45 11.0 $+$33 11 31 | 0.43 | 0.86 | Irr |  $>$23.5 | 22.47 | 19.10 | 18.71 | 18.2 | (5)
KK220=A232003 | 13 47 36.5 $+$33 12 22 | 1.11 | 0.93 | Im | 18.92 | 18.07 | 16.3 | 8 16.02 | 15.59 | (6)
Notes: (1) — at 30′ to S there is DDO 46 with D = 10.38 Mpc via TRGB;(2) — an
isolated dSph;
(3) — may be a satellite of NGC 4251 with $V_{h}$ = 1066 km/s or NGC 4278 with
$V_{h}$ = 649 km/s and
$D$ = 16.07 Mpc via sbf; (4) — granulated; in the Virgo cluster?; (5) — a
probable pair with the KK 220;
(6) — It has $V_{h}$ = 776 km/s, $W_{50}$ = 19 km/s and $m_{21}$ = 17.1 mag,
$D$ = 11.1 Mpc via NAM method.

##  3 The problem of distance estimation for dSph galaxies

Dwarf dIrr- and BCD-galaxies rich in gas and with active star formation are
easy targets for measuring their radial velocity both in the optical and radio
ranges. The situation with determination of the radial velocity in dwarfs of
spheroidal and transitional (Tr) types is much more complicated. The absence
of star formation sites as well as appreciable amount of neutral hydrogen
makes it almost impossible to measure the velocity of a galaxy. In nearby dSph
objects, it is sometimes possible to determine the optical velocity in the
presence of a globular cluster or planetary nebula in the galaxy.

$SB=(1/3)\times M_{B}+const,$

Figure 3: Images of 9 the Local Volume galaxy candidates from Zaritsky’s SMUDG
catalog. Each image size is $2\hbox{${}^{\prime}$}\times
2\hbox{${}^{\prime}$}$. North is to the top and East is to the left.

There is a dependence between the absolute magnitude of dSph-galaxy and its
average surface brightness which reflects the approximate constancy of the
mean spatial stellar density in galaxies [26]. This relation can be used to
estimate roughly the distance to a Sph or Tr type galaxy. However, a scatter
in the diagram M vs. SB is quite large, which produces significant errors in
the distance estimates. For example, about a dozen dSph galaxies were found in
the nearby ($D$=6.9 Mpc) group around the luminous Sc galaxy M101, which were
thought to be members of this group [27]. However, the HST observations of
these galaxies have disproved this naive assumption. These low surface
brightness galaxies turned out to be members of more distant groups at
distances of $D\sim$ 28 Mpc. A similar situation happened with dSph galaxies:
KKR08, KDG218, KDG229, where the HST observations did not confirm their
belonging to the LV.

Looking through large portions of the sky in Legacy Imaging Surveys, we have
found many cases where very low surface brightness tidal structures are seen
around a bright host galaxy. They are usually similar in size and brightness
contrast to isolated ultra-diffuse dwarf galaxies. The tidal nature of such
semi-detached dwarfs is quite obvious. In Table 4, we present a few examples
where it is difficult to make the distinction between clumps in tidal
structures and detached dSph galaxies. The table contains the name of the
bright galaxy, its equatorial coordinates in degrees, the galaxy redshift, and
the characteristic angular size of the field in which neighboring dwarfs and
tidal structures are visible.

Two fields around the galaxies NGC4643 and NGC5557 are presented in Fig. 4.
The low- contrast structures on them are marked with dashed ellipses. In the
case of NGC4643, the dSph galaxy SMUDG1245+01 shown in Table 2 is located
$\sim 40\hbox{${}^{\prime}$}$. East of NGC4643, i.e. outside the image frame.
The three noted clumps (or detached spheroidal dwarfs?) bear a strong
resemblance to SMUDG1245+01. The tidal structures around NGC5557 are barely
distinguishable from usual ultra-diffuse dwarf galaxies. These faint objects
near NGC5557 are also well seen in the deep image obtained by [28]. Other
examples of similar structures found in Legacy Imaging Surveys have been
demonstrated recently by [29].

Figure 4: Images of the nearby bright galaxies: NGC 4643 (upper panel) and NGC 5557 (bottom panel) with low surface brightness objects around them indicated by dashed ellipses. The size of the images are $12\hbox{${}^{\prime}$}\times 10\hbox{${}^{\prime}$}$ for NGC 4643 and $28\hbox{${}^{\prime}$}\times 15\hbox{${}^{\prime}$}$ for NGC 5557.  Table 4: Borderline cases of semi-separated tidal dwarf galaxies. Name | RA (2000.0) DEC | Z | Field size
---|---|---|---
| degr degr |  | arcmin
NGC 4643 | 190.834 +01.978 | 0.0044 | 12
PGC 049168 | 207.751 +36.954 | 0.0174 | 6
NGC 5363 | 209.030 +05.255 | 0.0038 | 20
NGC 5557 | 214.607 +36.494 | 0.0107 | 28
UGC 9386 | 218.720 +40.748 | 0.0190 | 6
NGC 5754 | 221.332 +38.731 | 0.0147 | 8
IC 1069 | 222.694 +54.411 | 0.0376 | 6
PGC 055442 | 233.454 +21.136 | 0.0234 | 6
NGC 5971 | 233.904 +56.462 | 0.0112 | 6
NGC 6020 | 239.284 +22.405 | 0.0144 | 8
PGC 2308494 | 248.470 +47.998 | 0.0354 | 6

##  4 Discussion and conclusion

Our experience with the search for new nearby dwarf galaxies in regions of the
sky outside of close groups has led us to conclude that the efficiency of this
hunt is low. For instance, our search for new members in 46 LV groups
undertaken with DESI Legacy Imaging Surveys found 67 probable members of these
groups over a total area of 280 square degrees [10]. Performing a survey of
the broad vicinity of the Local Void on the same material and in the same
manner, we found only 12 Local Volume candidates over an area of about 5000
square degrees. The effectiveness of searches in the general field, outside
the groups, turns out to be two orders of magnitude lower than that in the
groups themselves. This is consistent with the well-known fact that the slope
of the galaxy luminosity function at its faint end is much smaller for field
galaxies than for members of groups and clusters [30].

The population of the general field and cosmic voids is dominated by dwarf
galaxies richer in gas and with a more active star formation rate [31].
According to our data presented in Tables 1–3, quiescent dSph galaxies account
for a quarter of the total. Some of them may turn out to be members of the
nearby Virgo cluster. However, the examples of dSph galaxies SMUDG1017-05 and
SMUDG1110+18 suggest that a small percentage of dwarf spheroidal galaxies may
be well-isolated objects. In the vicinity of the Local Group, the dSph
galaxies KKR25 and KKs3 locate at a distance of $\sim$2 Mpc from the Milky
Way, i.e. well beyond the virial radius of the Local Group [32, 33].
Investigating the distribution of dwarf satellites around massive Milky Way-
type LV galaxies, [34] found that the fraction of dSph dwarfs among satellites
with $K$-band luminosity $L/L_{\odot}>10^{7}$ decreases with the projected
distance from the host galaxy Rp according to the exponential law

$q(R_{p})=0.75\times exp(-R_{p}/350\,\,{\rm kpc}).$

Then outside the radius of the zero-velocity sphere of a typical nearby group
($R_{0}\simeq 1.0$ Mpc), i.e., in the general expanding field, the relative
number of quiescent dSph dwarfs is about 5%. The presence of two definitely
isolated dSph galaxies among the 28 ones found in our survey agrees well with
the above estimate.

It is interesting to note, that Park et al, [35] performed measurements of
satellite radial velocities around isolated massive early-type galaxies and
found a lack of faint satellites with absolute magnitudes $M_{r}$ fainter than
–14.0 mag. This effect, if confirmed on large statistics, can be caused by a
peculiarity of the dynamical evolution of isolated elliptical galaxies.

Finally, we note a planned photometric survey of the sky with small-aperture
telescopes of The Dragonfly Telephoto Array [36]. The authors expect to find a
lot of new dwarf galaxies in the general field. They estimate that the number
of new dwarfs in the LV up to the surface brightness limit of $\sim$30 mag
$\times$ arcsec2 could reach $\sim$0.1 per square degree or N $\sim 10^{3}$
across the entire sky.

Acknowledgements. In the work we use the DESI Legacy Imaging Surveys and the
Galaxy Evolution Explorer Survey. This work is supported by the grant
075-15-2022-262 (13.MNPMU.21.0003) of the Ministry of Science and Higher
Education of the Russian Federation.

REFERENCES

1\. Wilding G., Nevenzeel K., van de Weygaert R., et al., MNRAS, 507, 2968,
2021.

2\. Courtois H.M., van de Weygaert R., Aubert M., et al., A & A, 673A, 38,
2023.

3\. Vennik J., Tartu Astrofuusika Observatorium Treated, 73, 1, 1984.

4\. Makarov D.I., Karachentsev I.D., MNRAS, 412, 2498 , 2011.

5\. Kourkchi E., Tully R.B., ApJ, 843, 16, 2017.

6\. Karachentsev I.D., Makarov D.I., Kaisina E.I., AJ, 145, 101, 2013.

7\. Chiboucas K., Karachentsev I.D., Tully R.B., AJ, 137, 3009, 2009.

8\. Muller O., Rejkuba M., Pawlowski M.S., et al., A & A, 629, A18, 2019.

9\. Carlsten, S.G., Greene, J.E., Beaton, R.L., ApJ, 933, 47, 2022.

10\. Karachentsev I.D., Kaisina E.I., Astr.Bull., 77, 411, 2022.
11\. van den Bergh S., A Catalog of Dwarf Galaxies, Publ. David Dunlap obs.,
2, 147, 1959.

12\. Karachentseva V.E., Soobsch. Byurakan astrophys. Obs., 39, 61, 1968.

13\. Karachentseva V.E., Astron. Tsirk., 723, 1, 1972.

14\. Karachentseva V.E., Izvestia SAO, 5, 10, 1973.

15\. Karachentsev I.D., Karachentseva V.E., Suchkov A.A., Grebel E.K., A&AS,
145, 415, 2000.

16\. Karachentseva V.E., Karachentsev I.D., A&AS, 127, 409, 1998.

17\. Zaritsky D., Donnerstein R., Dey A., et al., ApJS, 267, 27, 2023.

18\. Paudel S., Yoon S.J., Yoo J., et al., ApJS, 265, 57, 2023.

19\. Kaisina E.I., Makarov D.I., Karachentsev I.D., et al., AstBul, 67, 115,
2012.

20\. Dey A., Schlegel D.J., Lang D., et al., AJ, 157, 168, 2019.

21\. Tully R.B., Nearby Galaxies Catalog, Cambridge University Press, 1988.

22\. Pustilnik S.A., Tepliakova A.L., Makarov D.I., MNRAS, 482, 4329, 2019.

23\. Martin D.C., Fanson J., Schiminovich D., et al., ApJ, 619, L1, 2005.

24\. Zaritsky D., Donnerstein R., Karunakaran A., et al., ApJS, 261, 11, 2022.

25\. Shaya E. L., Tully R. B., Hoffman Y., Pomarede D., ApJ, 850, 207, 2017.

26\. Karachentsev I.D., Karachentseva V.E., Huchtmeier W.K., Makarov D.I., AJ,
127, 2031, 2004.

27\. Merritt A., van Dokkum P., Abraham R., ApJ, 787, L37, 2014.

28\. Duc P.A., Paudel S., McDermid R.M., et al., MNRAS, 440, 1458, 2014.

29\. Martinez-Delgado D., Cooper A.P., Roman J., et al., A & A, 671A, 141,
2023.

30\. Driver S. , De Propris R., ASpSci, 285, 175, 2003.

31\. Rodriguez-Medrano A.M., Paz D.J., Stasyszyn F.A., et al., MNRAS, 521,
916, 2023.

32\. Makarov D.I., Makarova L.N., Sharina M.E., et al., MNRAS, 425, 709, 2012.

33\. Karachentsev I.D., Kniazev A.Y., Sharina M.E., AN, 336, 707, 2015.

34\. Karachentsev I., Kashibadze O., Astr. Nachr., 342, 99, 2021.

35\. Park C., Hwang H.S., Park H., Lee J.C., NatAs, 2, 162, 2018.

36\. Danieli S., van Dokkum P., Conroy C., ApJ, 856, 69, 2018.


# Causal Kripke Models111This project has received funding from the European
Union’s Horizon 2020 research and innovation programme under the Marie
Skłodowska-Curie grant agreement No 101007627.

Yiwen Ding2 222Yiwen Ding, Ruoding Wang and Xiaolong Wang are supported by the
China Scholarship Council Shandong University1 Vrije Universiteit, Amsterdam2
Xiamen University3 Krishna Manoorkar2 Krishna Manoorkar is supported by the
NWO grant KIVI.2019.001 awarded to Alessandra Palmigiano. Shandong University1
Vrije Universiteit, Amsterdam2 Xiamen University3 Apostolos Tzimoulis2
Shandong University1 Vrije Universiteit, Amsterdam2 Xiamen University3 Ruoding
Wang${}^{2,3\,\small{\dagger}}$ Shandong University1 Vrije Universiteit,
Amsterdam2 Xiamen University3 Xiaolong Wang${}^{1,2\,\small{\dagger}}$
Shandong University1 Vrije Universiteit, Amsterdam2 Xiamen University3

###### Abstract

This work extends Halpern and Pearl’s causal models for actual causality to a
possible world semantics environment. Using this framework we introduce a
logic of actual causality with modal operators, which allows for reasoning
about causality in scenarios involving multiple possibilities, temporality,
knowledge and uncertainty. We illustrate this with a number of examples, and
conclude by discussing some future directions for research.

##  1 Introduction

Causality is crucial in human reasoning and knowledge. Defining and
formalizing causality has been a significant area of research in philosophy
and formal methods [13, 22, 25, 12]. In recent years, with the rise of machine
learning and AI, there has been growing interest in formalizing causal
reasoning. One of the key areas of AI research is designing algorithms capable
of comprehending causal information and performing causal reasoning [6, 30,
31]. Causal reasoning can be instrumental in formally modeling notions such as
responsibility, blame, harm, and explanation, which are important aspects in
designing ethical and responsible AI systems [4].

In this article we focus on the kind of causality known as ”actual causality”
(a.k.a. token causality) [11, 21, 20, 32]. Actual causality refers to the
causality of a specific event which has actually happened (e.g. ”John died
because Alice shot him”) rather than general causes (e.g. ”smoking causes
cancer”). Several formal approaches have been used for modelling actual
causality [25, 26, 14, 15]. One of the most prominent formalizations of actual
causation was developed by Halpern and Pearl [29, 18, 19]. This model
describes dependencies between endogenous variables and exogenous variables
using structural equations. Based on causal models Halpern and Pearl have
given three different definitions of actual causality known as original,
updated and modified definitions [18, 19, 16] of actual causality using
counterfactual reasoning. The formal language developed to describe actual
causality in this model is used to define several notions like normality,
blame, accountability and responsibility. This model has been used in several
applications in law [28], database theory [27], model checking [9, 10, 5], and
AI [23, 12, 4].

Notions like knowledge, temporality, possibility, normality (or typicality)
and uncertainty play important role in causal reasoning and related
applications. In the past, attempts have been made to incorporate some of
these notions into the causal models of Halpern and Pearl. In [5], Beer et.al.
define causality in linear temporal logic to explain counterexamples. This
line of research has been carried forward in model checking and program
verification [2, 24]. The Halpern and Pearl formalism has also been extended
to define causality in frameworks such as transition systems and Hennessy-
Milner logic [7, 8, 2]. In [3], Barbero et.al. define causality with epistemic
operators. However, to the best of our knowledge a general Kripke model for
actual causality based on Halpern and Pearl framework has not been studied
yet.

In this work, we develop the notion of causal Kripke models and introduce a
modal language for causal reasoning with uncertainty, temporality,
possibility, and epistemic knowledge. We show that our model can formalize
notions like sufficient causality, blame, responsibility, normality, and
explanations. Our framework provides a more natural definition of sufficient
causality [17, Section 2.6] by considering nearby contexts, which Halpern’s
causal model does not support (c.f. 5.1). The developed causal Kripke models
offer a straightforward way to describe nearby contexts and define sufficient
causality as intended by Halpern. In order to stay as close as possible to
Halpern’s original framework, where formally only atomic events can be causes,
we utilize a hybrid language not only contains modalities but also names for
the possible worlds.

The structure of the paper is as follows. In Section 2, we provide
preliminaries on causal models and logic of causality. In Section 3, we give
several examples to motivate the development of causal Kripke semantics. In
Section 4, we define causal Kripke models, and develop a modal logic of actual
causality to reason about them. We generalize the Halpern-Pearl definitions of
actual causality to this framework and provide a sound and complete
axiomatization of the modal logic of actual causality. In Section 5, we model
the examples discussed in Section 3 using our framework and also show how this
model can be used to provide an intuitive definition of sufficient causality.
Finally, in Section 6 we conclude and provide some directions for future
research.

##  2 Preliminaries

###  2.1 Causal models

In this section we briefly recall key concepts and ideas of the standard logic
of causal reasoning as presented in [17]. A causal model describes the world
in terms of variables which take values over certain sets. The variables and
their ranges are given by a signature
$\mathcal{S}=(\mathcal{U},\mathcal{V},\mathcal{R})$ where $\mathcal{U}$ is a
finite set of exogenous variables (i.e., variables whose value is independent
of other variables in the model), $\mathcal{V}$, which is disjoint with
$\mathcal{U}$, is a finite set of endogenous variables (i.e., variables whose
value is determined by other variables in the model), and $\mathcal{R}(X)$ for
any $X\in\mathcal{U}\cup\mathcal{V}$, is the (finite) range of $X$. These
variables may have dependencies between them described by structural equations
defined as follows.

######  Definition 2.1.

A causal model is a pair $(\mathcal{S},\mathcal{F})$, where
$\mathcal{S}=(\mathcal{U},\mathcal{V},\mathcal{R})$ is the model’s signature
and $\mathcal{F}=(f_{V_{i}}\mid V_{i}\in\mathcal{V})$ assigns to each
endogenous variable $V_{i}$ a map such that

$f_{V_{i}}:\mathcal{R}(\mathcal{U}\cup\mathcal{V}-\\{V_{i}\\})\to\mathcal{R}(V_{i}).$

######  Definition 2.2.

For any variables $V\in\mathcal{V}$ and $X\in\mathcal{U}\cup\mathcal{V}$, we
say ”$X$ is a direct cause, or a parent, of $V$” if there exist
$x,x^{\prime}\in\mathcal{R}(X)$ and
$\overline{z}\in\mathcal{R}(\mathcal{U}\cup\mathcal{V}-\\{X,V\\})$ such that
$f_{V}(\overline{z},x)\neq f_{V}(\overline{z},x^{\prime})$. A causal model is
said to be recursive if it contains no cyclic dependencies.

######  Definition 2.3.

For a causal model $M=(\mathcal{S},\mathcal{F})$, a  context $\overline{t}$
assigns every variable $U\in\mathcal{U}$ a value in $\mathcal{R}(U)$. A
causal setting is a pair $(M,\overline{t})$, where $M$ is a causal model and
$\overline{t}$ is a context for it.

In recursive models, as there are no cyclic dependencies the values of all
endogenous variables are determined by the context. Throughout this paper we
only consider recursive causal models.

######  Definition 2.4.

Let $M=(\mathcal{S},\mathcal{F})$ be some causal model and
$\mathcal{Y}\subseteq\mathcal{V}$ be a set of endogenous variables. Let
$\overline{Y}$ be the injective listing of the variables of $\mathcal{Y}$. Let
$\overline{Y}=\overline{y}$ be an assignment such that
$y_{i}\in\mathcal{R}(Y_{i})$ for every $Y_{i}\in\mathcal{Y}$. The causal model
obtained from  intervention setting values of variables of $\overline{Y}$ to
$\overline{y}$ is given by
$M_{\overline{Y}\leftarrow\overline{y}}=(\mathcal{S},\mathcal{F}_{\overline{Y}\leftarrow\overline{y}})$
, where $\mathcal{F}_{\overline{Y}\leftarrow\overline{y}}$ is obtained by
replacing for every variable $Y_{i}\in\mathcal{Y}$, the structural equation
$f_{Y_{i}}$ with $Y_{i}=y_{i}$.

Here, we consider the exogenous variables as given. Thus, we do not allow
interventions on them.

###  2.2 Basic language for describing causality

The basic language, $\mathrm{L}_{C}$, for describing causality is an extension
of propositional logic where primitive events are of the form $X=x$, where
$X\in\mathcal{V}$ is an endogenous variable and $x\in\mathcal{R}(X)$. Given
the signature $\mathcal{S}=(\mathcal{U},\mathcal{V},\mathcal{R})$, the
formulas $\phi\in\mathrm{L}_{C}$ are defined by the following recursion:

$\alpha::=X=x\mid\neg\alpha\mid\alpha\wedge\alpha\quad\text{where},\,X\in\mathcal{V},\,x\in\mathcal{R}(X)$
$\phi::=X=x\mid\neg\phi\mid\phi\wedge\phi\mid[\overline{Y}\leftarrow\overline{y}]\alpha\quad\text{where},\,\overline{Y}\leftarrow\overline{y}\,\text{is
an intervention}$

For any causal setting $(M,\overline{t})$ and formula $\phi\in\mathrm{L}_{C}$,
the satisfaction relation $(M,\overline{t})\Vdash\phi$ is defined as follows.
For any formula $X=x$, $(M,\overline{t})\Vdash X=x$ if the value of endogenous
variable $X$ is set to $x$ in context $\overline{t}$. Satisfaction for the
Boolean connectives is defined in a standard manner. Satisfaction of
intervention formulas is defined as follows: for any event $\alpha$,
$(M,\overline{t})\Vdash[\overline{Y}\leftarrow\overline{y}]\alpha$ iff
$(M_{\overline{Y}\leftarrow\overline{y}},\overline{t})\Vdash\alpha$. This
language is used by Halpern and Pearl to provide three different definitions
of causality referred as original , updated and modified definitions of
causality [17, Section 2.2] (for details see Appendix A.1).

##  3 Motivation for possible world semantics of causal models

The basic language for causal reasoning described above uses propositional
logic as the language of events and for reasoning with causal formulas.
However, we are interested in describing causal reasoning in scenarios that
involve notions like possibility, knowledge or belief, temporality,
uncertainty and accessibility. Here we provide several such examples.

######  Example 3.1 (Umbrella).

Alice is going on a trip to London. She thinks that it may rain when she is
there. Thus, she decides to take her umbrella with her for the trip. In this
example, the possibility of raining in London in the future seems to be the
cause for Alice taking her umbrella with her.

######  Example 3.2 (Chess).

In a chess game, if knight and the king are only pieces that can move but
every king move leads to king getting in check, then the player is forced to
move the knight. Suppose that the king can not move to a certain square
because it is covered by a bishop. Then it seems reasonable that the fact that
bishop covers this square to be a cause for player being forced to move the
knight. This example shows that reasoning with causality naturally involves
considering possibilities.

######  Example 3.3 (Police).

Suppose John is a criminal who is currently absconding. Inspectors Alice and
Bob are trying to catch John. John is currently in Amsterdam. He has a train
ticket to Brussels. Thus, his (only) options are to stay in Amsterdam or to
take the train to Brussels. Bob decides to go to Brussels to catch John in
case he takes the train. John learns this information and decides to stay in
Amsterdam where Alice catches him. In this case, John’s belief of Bob’s
presence in Brussels leads to him staying in Amsterdam. It seems reasonable
that this should be part of the cause of John getting caught, even though he
was caught by Alice in Amsterdam. This shows that the knowledge of the agents
is crucially involved in causal reasoning.

######  Example 3.4 (Robot).

Consider a scenario in which a robot is being commanded by a scientific team.
Upon receiving command c, the robot completes task t or malfunctions. In this
case the possibility of causing malfunction may become the cause of not
sending command c. i.e. , causal reasoning involves scenarios in which the
dependencies between different events may be ”indeterministic” or
”underdetermined”. Halpern considers such scenarios in [17, Section 2.5],
using the notion of probabilities over causal models. However, in certain
cases qualitative reasoning in terms of possibilities may be more appropriate.

######  Example 3.5 (Navigation).

Suppose Alice is trying to reach village A. She reaches a marker which
indicates that she is at location B, C or D. She does not know in which of
these locations she is at. However, she knows that A is to the east of all of
these locations. Thus, she decides to go east. Suppose Alice was actually at
point B. The fact that A is to the east of locations C and D is still part of
Alice’s considerations and seems to be part of the cause for her going east.

These examples highlight that notions such as possibility, knowledge and
uncertainty play an important role in causal reasoning. Possible world
semantics, formally described by Kripke models, are the natural logical
framework for modeling such notions. In the next section we develop a
framework for causal reasoning, based on Kripke frames, which allows for
modeling such scenarios in a clear, intuitive and efficient way.

##  4 Possible world semantics for causal reasoning

In this section, we define the causal Kripke model, introduce the modal
language for causality and give the corresponding three HP definitions of
causality in causal Kripke models. In our framework, we allow the same
variable to possibly take different values in different worlds. Moreover, the
structural equations treat the same endogenous variable separately for each
different possible world.

######  Definition 4.1.

A causal Kripke model is a tuple $\mathcal{K}=(\mathcal{S},W,R,\mathcal{F}$),
where $W$ is a finite set of possible worlds, $R\subseteq W\times W$ is an
accessibility relation, and
$\mathcal{S}=(\mathcal{U},\mathcal{V},\mathcal{R})$ is the signature such that
$\mathcal{U}$ and $\mathcal{V}$ are the disjoint sets of exogenous and
endogenous variables, and $\mathcal{R}$ is a function assigning each
$\Gamma\in\mathcal{U}\cup\mathcal{V}$ and a world $w\in W$ a set of possible
values that $\Gamma$ can take at $w$, and $\mathcal{F}=(f_{(X_{i},w_{j})}\mid
X_{i}\in\mathcal{V},w_{j}\in W)$ assigns to each endogenous variable $X_{i}$
and each world $w_{j}$ a map such that

$f_{(X_{i},w_{j})}:\ \mathcal{R}((\mathcal{U}\cup\mathcal{V})\times
W)-\\{(X_{i},w_{j})\\})\to\mathcal{R}(X_{i},w_{j}).$

For any causal Kripke model $\mathcal{K}=(\mathcal{S},W,R,\mathcal{F})$ we
refer to $\mathcal{S}$ as its signature. For any variable $\Gamma$ and world
$w$ we use $(\Gamma,w)$ to denote the restriction of variable $\Gamma$ to the
world $w$. That is, $(\Gamma,w)$ is a variable which takes a value $c$ iff the
propositional variable $\Gamma$ takes the value $c$ at the world $w$. For any
$\Gamma\in\mathcal{U}$ (resp. $\Gamma\in\mathcal{V}$) and any world $w\in W$,
we say $(\Gamma,w)$ is an exogenous (resp. endogenous) variable. Note that we
allow the same endogenous variable to have different structural equations
associated with it in different worlds.

######  Definition 4.2.

A  context over a causal Kripke model
$\mathcal{K}=(\mathcal{S},W,R,\mathcal{F})$ is a function $\overline{t}$ such
that for any $w\in W$, and $U\in\mathcal{U}$, assigns a value in
$\mathcal{R}(U,w)$. A causal Kripke setting is a pair
$(\mathcal{K},\overline{t})$, where $\mathcal{K}$ is a causal Kripke model and
$\overline{t}$ is a context for it.

######  Definition 4.3.

For any variables $X\in\mathcal{V}$, and
$\Gamma\in\mathcal{U}\cup\mathcal{V}$, and any $w,w^{\prime}\in W$, we say
”$(X,w)$ is a direct cause, or a parent, of $(\Gamma,w^{\prime})$” if there
exist $\gamma,\gamma^{\prime}\in\mathcal{R}(\Gamma,w^{\prime}),$ and
$\overline{z}\in\mathcal{R}((\mathcal{U}\cup\mathcal{V})\times
W-\\{(\Gamma,w^{\prime})\\})$ such that $f_{(X,w)}(\overline{z},\gamma)\neq
f_{(X,w)}(\overline{z},\gamma^{\prime})$. A causal Kripke model is said to be
recursive if it contains no cyclic dependencies.

In recursive models, as there are no cyclic dependencies the values of all
endogenous variables at all the worlds are completely determined by the
context. If $\mathcal{V}$ only contains binary variables (i.e. the variable
which take values either $0$ or $1$), then for any context $\overline{t}$, and
any world $w$, we use $\overline{t}(w)$ to denote the set of endogenous
variables set to value $1$ at $w$ by $\overline{t}$. In this paper, we only
consider recursive causal Kripke models.

######  Definition 4.4.

Given a causal Kripke model $\mathcal{K}=(\mathcal{S},W,R,\mathcal{F})$, as
assignment over $\mathcal{K}$ is a function on some subset
$\mathcal{Y}\subseteq\mathcal{V}\times W$ such that, for every
$Y=(X,w)\in\mathcal{Y}$, it assigns some value in $\mathcal{R}(X,w)$.

######  Definition 4.5.

Let $\mathcal{K}=(\mathcal{S},W,R,\mathcal{F})$ be some causal Kripke model
and $\mathcal{Y}$ be a finite subset of $\mathcal{V}\times W$. Let
$\overline{Y}$ be an injective (possibly empty) listing of all the variables
in $\mathcal{Y}$. Let $\overline{Y}=\overline{y}$ be an assignment such that
for any $Y_{i}\in\mathcal{Y}$, $y_{i}\in\mathcal{R}(Y_{i})$. The causal Kripke
model obtained from intervention setting values of variables of $\overline{Y}$
to $\overline{y}$ is given by
$\mathcal{K}_{\overline{Y}\leftarrow\overline{y}}=(\mathcal{S},W,R,\mathcal{F}_{\overline{Y}\leftarrow\overline{y}})$
, where $\mathcal{F}_{\overline{Y}\leftarrow\overline{y}}$ is obtained by
replacing for every variable $Y_{i}\in\mathcal{Y}$, the structural equation
$f_{Y_{i}}$ with $Y_{i}=y_{i}$.

###  4.1 Modal logic language for describing causality

In this section we define the formal logical framework we introduce for
describing causality. Since we want to talk about variables whose values
depend on the possible world of a Kripke model, our language will be hybrid in
character, augmenting the standard language (as presented e.g. in Section 2.2)
not only with modal operators but also with a countable set of names, denoted
with $W$. In principle each model $M$ comes with an assignment from $W$ to
points of $M$, however in practice we will often conflate names with elements
of Kripke models. The reason we require a countable number of names, even
though the models are always finite, is because there is no bound on the size
of the models. We will denote the language with $\mathrm{L}_{M}(W)$. We often
omit $W$ and write $\mathrm{L}_{M}$ when $W$ is clear from the context.
$\mathcal{S}$ is a given signature, and all $X,Y,x,y$ come from $\mathcal{S}$.
In what follows we will consistently use $Y$ to denote a variable parametrized
with a name for a world (i.e. $Y=(X,w)$). It is important to notice that in
our language interventions involve only such variables. Any event $\alpha$ and
formula $\phi$ of the language $\mathrm{L}_{M}$ is defined by the following
recursion.

$\alpha::=X=x\mid(X,w)=x\mid\neg\alpha\mid\alpha\wedge\alpha\mid\Box\alpha\quad\text{where},\,X\in\mathcal{V},w\in
W$

$\phi::=X=x\mid(X,w)=x\mid\neg\phi\mid\phi\wedge\phi\mid\Box\phi\mid[\overline{Y}\leftarrow\overline{y}]\alpha\quad\text{where},\,\overline{Y}\leftarrow\overline{y}\,\text{is
an intervention}$

In particular, the language $\mathrm{L}_{M}$ has two types of atomic
propositions, using variables of the form $X$ and of the form $(X,w)$. The
second, the hybrid aspect of our language, provides global information
regarding the Kripke model. For any causal Kripke setting
$(\mathcal{K},\overline{t})$ with $\mathcal{K}=(\mathcal{S},W,R,\mathcal{F})$,
any causal formula $\phi$, and any world $w\in W$, we define satisfaction
relation $\Vdash$ in the following way. For any primitive event $X=x$ (resp.
$(X,w^{\prime})=x$), $(\mathcal{K},\overline{t},w)\Vdash X=x$ (resp.
$(\mathcal{K},\overline{t},w)\Vdash(X,w^{\prime})=x$) iff the value of $X$ is
set to be $x$ at $w$ (resp. at $w^{\prime}$) by the context $\overline{t}$.
Note that the satisfaction of $(X,w^{\prime})=x$ is independent of the world
it is evaluated at. The satisfaction relation for Boolean connectives is
defined by standard recursion. For the $\Box$ operator,

$(\mathcal{K},\overline{t},w)\Vdash\Box\alpha\quad\text{iff}\quad\text{for
all}\,w^{\prime},\,wRw^{\prime}\,\text{implies}\,(\mathcal{K},\overline{t},w^{\prime})\Vdash\alpha.$

Let $\mathcal{Y}\subseteq\mathcal{V}\times W$ be a set of endogenous
variables. Satisfaction of intervention formulas is defined as for any event
$\alpha$,
$(\mathcal{K},\overline{t},w)\Vdash[\overline{Y}\leftarrow\overline{y}]\alpha$
iff
$(\mathcal{K}_{[\overline{Y}\leftarrow\overline{y}]},\overline{t},w)\Vdash\alpha$.
Satisfaction for Boolean combinations of causal formulas is defined in a
standard manner. For the $\Box$ operator,

$(\mathcal{K},\overline{t},w)\Vdash\Box\phi\quad\text{iff}\quad\text{for
all}\,w^{\prime},\,wRw^{\prime}\,\text{implies}\,(\mathcal{K},\overline{t},w^{\prime})\Vdash\phi.$

We now extend the HP definition(s) of causality to the setting of causal
Kripke models.

######  Definition 4.6.

Let $\alpha$ be any event. For $\overline{Y}\subseteq\mathcal{V}\times
W,\overline{Y}=\overline{y}$ is an actual cause of $\alpha$ in a causal Kripke
setting $(\mathcal{K},\overline{t})$ at a world $w$ if the following
conditions hold.

  * AC1.

$(\mathcal{K},\overline{t},w)\Vdash\alpha$ and for every $w_{j}\in W$,
$(\mathcal{K},\overline{t},w_{j})\Vdash(X_{i},w_{j})=y_{ij}$, for every
$(X_{i},w_{j})=y_{ij}\in\overline{Y}=\overline{y}$.

  * AC2a.

There exists a partition of $\mathcal{V}\times W$ into two disjoint subsets
$\overline{Z}$ and $\overline{N}$ with $\overline{Y}\subseteq\overline{Z}$ and
settings $\overline{y^{\prime}}$ and $\overline{n}$ of variables in
$\overline{Y}$ and $\overline{N}$, such that

$(\mathcal{K},\overline{t},w)\Vdash[\overline{Y}\leftarrow\overline{y^{\prime}},\overline{N}\leftarrow\overline{n}]\neg\alpha.$

  * AC2$b^{o}$.

Let $\overline{z}^{\ast}$ be the unique setting of the variables in
$\overline{Z}$ such that
$(\mathcal{K},\overline{t},w)\Vdash\overline{Z}=\overline{z}^{\ast}$. If
$(\mathcal{K},\overline{t},w^{\prime})\Vdash X=z^{\ast}$, for every
$(X,w^{\prime})=z^{\ast}\in\overline{Z}=\overline{z}^{\ast}$, then for all
subsets $\overline{Z}^{\prime}$ of $\overline{Z}\setminus\overline{Y}$ we have

$(\mathcal{K},\overline{t},w)\Vdash[\overline{Y}\leftarrow\overline{y},\overline{N}\leftarrow\overline{n},\overline{Z}^{\prime}\leftarrow\overline{z}^{\prime\ast}]\alpha.$
333Here we use the abuse of notation that if
$\overline{Z}^{\prime}\subseteq\overline{Z}$ and
$\overline{Z}=\overline{z}^{\ast}$, then $\overline{z}^{\prime\ast}$ in
$\overline{Z}^{\prime}\leftarrow\overline{z}^{\prime\ast}$ refers to the
restriction of $\overline{z}^{\ast}$ to $\overline{Z}^{\prime}$.

  * AC3.

$\overline{Y}$ is a minimal set of variables that satisfy AC1 and AC2.

We say that $\overline{Y}=\overline{y}$ is an actual cause of $\alpha$ in a
causal Kripke setting $(\mathcal{K},\overline{t})$ at a world $w$ by updated
definition iff AC1, AC2a, AC3 hold and AC2$b^{o}$ is replaced by the following
condition.

Let $\overline{z}^{\ast}$ be the unique setting of the variables in
$\overline{Z}$ such that
$(\mathcal{K},\overline{t},w)\Vdash\overline{Z}=\overline{z}^{\ast}$. If
$(\mathcal{K},\overline{t},w^{\prime})\Vdash X=z^{\ast}$, for every
$(X,w^{\prime})=z^{\ast}\in\overline{Z}=\overline{z}^{\ast}$, then for all
subsets $\overline{Z}^{\prime}$ of $\overline{Z}\setminus\overline{Y}$ and
$\overline{N}^{\prime}$ of $\overline{N}$ we have

$(\mathcal{K},\overline{t},w)\Vdash[\overline{Y}\leftarrow\overline{y},\overline{N}^{\prime}\leftarrow\overline{n},\overline{Z}^{\prime}\leftarrow\overline{z}^{\prime\ast}]\alpha.$

We say that $\overline{Y}=\overline{y}$ is an actual cause of $\alpha$ in a
causal Kripke setting $(\mathcal{K},\overline{t})$ at a world $w$ by modified
definition iff AC1, AC3 hold and AC2 is replaced by the following condition.

If there exists a set of variables $\overline{N}\subseteq\mathcal{V}\times W$,
and a setting $\overline{y}^{\prime}$ of the variables in $\overline{Y}$ such
that if $\overline{n}^{\ast}$ is such that
$(\mathcal{K},\overline{t},w^{\prime})\Vdash X=n^{\ast}$, for every
$(X,w^{\prime})=n^{\ast}\in\overline{N}=\overline{n}^{\ast}$, then

$(\mathcal{K},\overline{t},w)\Vdash[\overline{Y}\leftarrow\overline{y}^{\prime},\overline{N}\leftarrow\overline{n}^{\ast}]\neg\alpha.$

We will refer to these definitions as original, updated, and modified
definitions henceforth. Example B.1 shows that these definitions do not in
general coincide. Theorem B.3 which relates these definitions in causal models
can be generalized to causal Kripke models in a straightforward manner (see
Theorem, B.5).

For any set of variables $\mathcal{Y}\subseteq\mathcal{V}\times W$, we use
$cause^{o}(\overline{Y}=\overline{y},\alpha)$ (resp.
$cause^{u}(\overline{Y}=\overline{y},\alpha)$,
$cause^{m}(\overline{Y}=\overline{y},\alpha)$) as an abbreviation for stating
$\overline{Y}=\overline{y}$ is a cause of $\alpha$ by the original (resp.
updated, modified) definition. We write $(\mathcal{K},\overline{t},w)\Vdash
cause^{o}(\overline{Y}=\overline{y},\alpha)$ (resp.
$(\mathcal{K},\overline{t},w)\Vdash
cause^{u}(\overline{Y}=\overline{y},\alpha)$,
$(\mathcal{K},\overline{t},w)\Vdash
cause^{m}(\overline{Y}=\overline{y},\alpha)$ ) as an abbreviation for stating
$\overline{Y}=\overline{y}$ is a cause of $\alpha$ in causal Kripke setting
$(\mathcal{K},\overline{t})$ at a world $w$ by the original (resp. updated,
modified) definition. Moreover, For $x=o,u,m$, we write
$(\mathcal{K},\overline{t},w)\Vdash\Box
cause^{x}(\overline{Y}=\overline{y},\alpha)$ if for all $w^{\prime}$ such that
$wRw^{\prime}$, $(\mathcal{K},\overline{t},w^{\prime})\Vdash
cause^{x}(\overline{Y}=\overline{y},\alpha)$ and
$(\mathcal{K},\overline{t},w)\Vdash\Diamond
cause^{x}(\overline{Y}=\overline{y},\alpha)$ if there exists $w^{\prime}$ such
that $wRw^{\prime}$ and $(\mathcal{K},\overline{t},w^{\prime})\Vdash
cause^{x}(\overline{Y}=\overline{y},\alpha)$.

###  4.2 Axiomatization

In [17], Halpern provides a sound and complete axiomatization for the logic of
causality. This axiomatization can be extended to the modal logic of causality
by adding the following axioms to the axiomatization in [17, Section 5.4]:

  * •

All substitution instances of axioms of basic modal logic $\mathrm{K}$.

  * •

Necessitation rule: from $\phi$ infer $\Box\phi$

  * •

$\Diamond$-axiom :
$[\overline{Y}\leftarrow\overline{y}]\Diamond\phi\Leftrightarrow\Diamond[\overline{Y}\leftarrow\overline{y}]\phi$
and $\Box$-axiom :
$[\overline{Y}\leftarrow\overline{y}]\Box\phi\Leftrightarrow\Box[\overline{Y}\leftarrow\overline{y}]\phi$

  * •

G-axiom:
$([\overline{Y}\leftarrow\overline{y}](X,w)=x)\Rightarrow\Box([\overline{Y}\leftarrow\overline{y}](X,w)=x)$

Notice that, similar to the axiomatization in [17, Section 5.4], the schemes
$\Diamond$-axiom, $\Box$-axiom, and G-axiom include empty interventions. When
importing the axioms from [17, Section 5.4] axiom scheme C5 involves only
variables of the form $(X,w)$. For the axiom schemes C1-4 and C6, the axioms
involve atoms both of the form $X=x$ and of the form $(X,w)=x$. Notice also
that G-axiom is similar to axioms in Hybrid modal logic.

Since the language in [17] is finite (modulo classical tautologies), weak and
strong completeness coincide. However our language is countable (given that
$W$ is countable). Since there is no upper bound on the size of the models, we
cannot hope to have strong completeness w.r.t. finite models. However the
axioms presented in this section are sound and weakly complete. In Appendix C
we provide the proofs of soundness and weak completeness w.r.t. the modal
logic of causality.

##  5 Examples and applications

In this section, we analyze the examples discussed in Section 3 using causal
Kripke models. For any endogenous variable $X$, and any world $w$, we use
$Eq(X,w)$ to denote the structural equation for $X$ at $w$. Throughout this
section, we use $U$ to denote exogenous variables only.

######  Example 5.1 (Umbrella).

Let $\mathcal{S}$ be the signature with endogenous variables $p$, $q$, and $r$
standing for ‘it rains in London’ and ‘Alice adds umbrella to the luggage’ and
‘Alice is in London’. Let $w_{0}$ be the current world and $w_{1},w_{2},w_{3}$
be the future possible worlds considered by Alice. Let
$W=\\{w_{0},w_{1},w_{2},w_{3}\\}$ and
$R=\\{(w_{0},w_{1}),(w_{0},w_{2}),(w_{0},w_{3})\\}$. Let
$U=(U_{1},U_{2})\in\\{0,1\\}^{2}$ be such that $(p,w)=(U_{1},w)$ and
$(r,w)=(U_{2},w)$ for any $w\in W$. Let $Eq(q,w)=\Diamond(p\wedge r)$ for all
$w$, i.e., Alice puts her umbrella in her luggage if she thinks it is possible
that in the future she will be in London and it rains there.

Let $\overline{t}$ be a context such that $U$ is set to be $(0,0)$,$(0,1)$,
$(1,0)$ and $(1,1)$ at the worlds $w_{0},w_{1},w_{2}$ and $w_{3}$
respectively. We have $\overline{t}(w_{0})=\\{q\\}$,
$\overline{t}(w_{1})=\\{r\\}$, $\overline{t}(w_{2})=\\{p\\}$,
$\overline{t}(w_{3})=\\{p,r\\}$. Here, $(p,w_{3})=1$ and $(r,w_{3})=1$ are
both causes of $q=1$ at $w_{0}$ by all three definitions.

We show that $(p,w_{3})=1$ is a cause by the original and updated definitions.
The proof for $(r,w_{3})=1$ is analogous. Indeed, as
$(\mathcal{K},\overline{t},w_{3})\Vdash(p,w_{3})=1$,
$(\mathcal{K},\overline{t},w_{3})\Vdash(r,w_{3})=1$ and
$(\mathcal{K},\overline{t},w_{0})\Vdash q$, AC1 is satisfied. Let
$\overline{Z}=\\{(r,w_{3}),(p,w_{3})\\}$ and $\overline{N}=\varnothing$,
$\overline{Y}=\\{(p,w_{3})\\}$, and $\overline{y^{\prime}}=0$. Then from the
structural equation as no world related to $w_{0}$ satisfies $p\wedge r$ under
this intervention, we have

$(\mathcal{K},\overline{t},w_{0})\Vdash[\overline{Y}\leftarrow
0]\neg(q=1)\quad\text{and}\quad(\mathcal{K},\overline{t},w_{0})\Vdash[\overline{Y}\leftarrow
1,\overline{Z^{\prime}}\leftarrow\overline{z}^{\ast}]q=1.$

where $\overline{Z^{\prime}}=(r,w_{3})$, $\overline{z}^{\ast}=(1,1)$ as
described by the context. Thus, AC2 is satisfied and AC3 is trivial as we are
considering a single variable. The updated definition in this case is
equivalent to the original definition as $\overline{N}=\emptyset$. The
modified definition is satisfied for the same setting
$\overline{y^{\prime}}=0$ and $\overline{N}=\\{(r,w_{3})\\}$. Thus, the fact
that it rains in the world $w_{3}$ is a cause of Alice carrying her umbrella
by all three definitions.

Now consider a slight variation of the above example in which we are sure
Alice will be in the London and do not include $r$ as a variable in our
analysis. In this case, the structural equation for $q$ is given by
$q=\Diamond p$. Note that, in this new model, we can argue in the way similar
to the above example that any world $w^{\prime}$ accessible from $w_{0}$,
$(p,w^{\prime})=1$ would be a part of the cause of Alice carrying her umbrella
at $w_{0}$ by all three definitions. This can be interpreted as the fact that
’Alice considers the possibility of a future world in which it rains in London
and she will be in London’ is a part of cause of her adding umbrella to
luggage.

In general, for any event $\alpha$ and endogenous variable $X$ we say that
”the possibility of ${X}={x}$” is a cause of $\alpha$ at $w$ iff
$\bigwedge\\{(X,w^{\prime})=x\mid
wRw^{\prime}\&(\mathcal{K},\overline{t},w^{\prime})\Vdash{X}={x}\\}$ is a
cause of $\alpha$ at $w$ by the modified definition. Here, we use the modified
definition because as mentioned by Halpern [17, Example 2.3.1], the
conjunction being a cause by modified definition can in fact be interpreted as
a cause being disjunctive, i.e. , the disjunction of the conjuncts can be
interpreted as the cause of the event. Hence under this interpretation the
existence of some $w^{\prime}$ which is accessible from $w_{0}$ and where
${X}={x}$ is a cause of $\alpha$ here. This can be interpreted as ”the
possibility of ${X}={x}$” being a cause of $\alpha$. Thus, in the variation of
the example discussed in the above paragraph, we can say that the possibility
of the world where it rains in London is a cause of Alice adding umbrella to
her luggage.

######  Example 5.2 (stalemate).

Let $\mathcal{S}$ be the signature with endogenous variables $p$, $q$ and $r$
standing for ‘The king is in check’, ‘The king and the knight are the only
pieces that can move in the current position’ and ‘The player is forced to
move the knight’. Let $w_{0}$ be the current position. Let $w_{1}$ and $w_{2}$
be the positions obtained from the (only) available moves by the king. Let
$W=\\{w_{0},w_{1},w_{2}\\}$ and $R=\\{(w_{0},w_{1}),(w_{0},w_{2})\\}$. Let
$U=(U_{1},U_{2})\in\\{0,1\\}^{2}$ be such that $(p,w)=(U_{1},w)$ and
$(q,w)=(U_{2},w)$ for any $w\in W$. Let $Eq(r,w)=\neg p\wedge q\wedge\Box p$
at any $w$, i.e., the player is forced to move the knight if the king and the
knight are the only pieces that can move, the king is not in check, and the
king’s every available move leads to the king being in check.

Let $\overline{t}$ be a context such that $U$ is set to be $(0,1)$,$(1,1)$,
and $(1,0)$ at the worlds $w_{0}$, $w_{1}$, and $w_{2}$ respectively. We have
$\overline{t}(w_{0})=\\{q,r\\}$, $\overline{t}(w_{1})=\\{p,q\\}$,
$\overline{t}(w_{2})=\\{p\\}$. In the same way as in the last example, we can
show that $(p,w_{0})=0$, $(q,w_{0})=1$, $(p,w_{1})=1$ and $(p,w_{2})=1$ are
all the causes of $r=1$ at $w_{0}$ by all three definitions. This can
intuitively be seen as the certainty of the king ending up in a check
regardless of the king move (while not currently being in check) is a part of
cause of being forced to move the knight.

In general, for any variable $X$, and any event $\alpha$ we say that the
certainty of ${X}={x}$ is a cause of $\alpha$ at $w$ iff
$({X},w^{\prime})={x}$ is a cause of $\alpha$ at $w$ for all $wRw^{\prime}$ by
the modified definition.

######  Example 5.3 (Police).

Let $\mathcal{S}$ be the signature with endogenous variables $p$, $q$, $r$,
and $s$ standing for ‘Inspector Bob is in Brussels’, ‘Inspector Alice is in
Amsterdam’, ‘John takes the train’, and ‘John is caught in Amsterdam’. Let
$w_{0}$ be the current world and $w_{1},w_{2}$ be the possible future worlds
considered by John. Let $W=\\{w_{0},w_{1},w_{2}\\}$ and
$R=\\{(w_{0},w_{1}),(w_{0},w_{2})\\}$.

Let $U\in\\{0,1\\}^{2}$ be such that $(p,w)=(U_{1},w)$ and $(q,w)=(U_{2},w)$
for any $w\in W$. Let $Eq(r,w_{0})=\neg\Box p$ and
$Eq(r,w_{1})=Eq(r,w_{2})=1$. i.e. , John takes the train if there is a
possible future scenario in which inspector Bob is not in Brussels (John
considers future scenarios when he takes the train). Let
$Eq(s,w_{0})=q\wedge\neg r$ (John gets caught in Amsterdam if Alice is there
and he does not take the train) and $Eq(s,w_{1})=Eq(s,w_{2})=0$ (John
considers future scenarios in which he is not caught).

Let $\overline{t}$ be a context such that $U$ is set to be $(1,1)$ at all the
worlds. We have $\overline{t}(w_{0})=\\{p,q,s\\}$ and
$\overline{t}(w_{1})=\overline{t}(w_{2})=\\{p,q,r\\}$. It is easy to check
that $(p,w_{1})=1$ and $(p,w_{2})=1$ are both causes of $s=1$ at $w_{0}$ by
all three definitions. Thus, the fact that Bob is present in Brussels in all
possible worlds considered by John is a cause of John getting caught in
Amsterdam. If we assume that John knows Bob is in Brussels iff he is actually
in Brussels, then we can say that Bob’s presence in Brussels is a cause of
John getting caught in Amsterdam.

Here we have assumed that John’s knowledge of Bob’s presence in Brussels is
the same as Bob being actually present in Brussels. However, this need not be
the case always. Now consider a slightly more complicated version of the same
story in which we have another endogenous variable $o$ standing for ‘John lost
his ticket’. Suppose John does not take the train if he loses the ticket or he
knows inspector Bob is in Brussels. i.e. ,$Eq(r,w_{0})=\neg(\Box p\vee o)$.
Other structural equations remain the same. Let $\overline{t}^{\prime}$ be a
context that sets variables $p$, $q$ to the same values as $\overline{t}$ at
all the worlds and sets $o$ to be $1$ at $w_{0}$. In this case $(p,w_{1})=1$,
$(p,w_{2})=1$ and $(o,w_{0})=1$ are all the causes of $s=1$ at $w_{0}$ by all
three definitions. Now consider slightly different context
$\overline{t}^{\prime\prime}$ such that $p$ is set to be true at worlds
$w_{0}$ and $w_{1}$, $q$ at worlds $w_{0}$, $w_{1}$, and $w_{2}$ and $o$ at
world $w_{0}$. In this case, we again have $r=0$ and $s=1$ at $w_{0}$.
However, only $(o,w_{0})=1$ is a cause for $s=1$ at $w_{0}$ by all three
definitions. Now suppose that Bob actually did go to Brussels, however John
does not know this information and thinks that there is a possibility that Bob
may not be in Brussels. The only reason he does not take the train is that he
lost the ticket. Thus, Bob being present in Brussels is not a cause of John
getting caught in Amsterdam in this case. This shows that the knowledge John
has about the presence of Bob in Brussels (and not just presence itself) is an
important part of causal reasoning.

######  Example 5.4 (Robot).

Let $\mathcal{S}$ be the signature with endogenous variables $p$, $q$ and $r$
standing for ‘The command $c$ is sent by the scientific team’, ‘The task $t$
is completed by the robot’ and ‘The robot malfunctions’. Let $w_{0}$ be the
current world, the world in which the scientific team is reasoning. Let
$w_{1}$ and $w_{2}$ be the possible worlds considered by the team. Let
$W=\\{w_{0},w_{1},w_{2}\\}$ and $R=\\{(w_{0},w_{1}),(w_{0},w_{2})\\}$.

Suppose $Eq(q,w_{1})=\blacklozenge p$, $Eq(r,w_{1})=0$,
$Eq(r,w_{2})=\blacklozenge p$, $Eq(q,w_{2})=0$, and
$Eq(q,w_{0})=Eq(r,w_{0})=0$, where $\blacklozenge$ is the diamond operator
corresponding to the relation $R^{-1}$, i.e., there are two possible
scenarios. In one scenario sending command $c$ leads to the completion of task
$t$ and no malfunctioning, while in the other it leads to the malfunctioning
of the robot and task $t$ is not completed.

Let $U\in\\{0,1\\}$ be such that $(p,w_{i})=(U,w_{i})$. Let $\overline{t}$ be
a context such that $U$ is set to be $1$ in all the worlds. We have
$\overline{t}(w_{0})=\\{p\\}$, $\overline{t}(w_{1})=\\{p,q\\}$,
$\overline{t}(w_{2})=\\{p,r\\}$. It is easy to see that $(p,w_{0})=1$ is the
cause of $r=1$ at $w_{2}$ but not at $w_{1}$ (it is not even true at $w_{1}$)
by all three definitions. Suppose the scientific team believes that if sending
command can possibly cause malfunctioning then command shouldn’t be sent. Then
as $(\mathcal{K},\overline{t},w_{0})\Vdash\Diamond cause((p,w_{0})=1,r=1)$ (
for all three definitions), the team will decide not to send the command. On
the other hand, if the team believes that the command should be sent if it can
possibly cause the completion of the task, then it must be sent as
$(\mathcal{K},\overline{t},w_{0})\Vdash\Diamond cause((p,w_{0})=1,q=1)$, i.e.
sending signal can cause completion of task $t$.

######  Example 5.5 (Navigation).

Let $\mathcal{S}$ be the signature with endogenous variables $p_{x}$, $q$ and
$r$ standing for ‘The current location of Alice is x’ for $x=B,C,D$, ‘Point
$A$ is to the east of Alice’s current location’ and ‘Alice moves to the east’.
Alice does not know if she is at point $B$, $C$ or $D$. Let $w_{1}$, $w_{2}$
and $w_{3}$ be possible worlds and $U\in\\{0,1\\}^{4}$ be such that
$(p_{B},w)=(U_{1},w)$, $(p_{C},w)=(U_{2},w)$, $(p_{D},w)=(U_{3},w)$ and
$(q,w)=(U_{4},w)$ for any $w\in W$.

Let $\overline{t}$ be a context such that $U$ is set to be $(1,0,0,1)$,
$(0,1,0,1)$, and $(0,0,1,1)$ at worlds $w_{1}$, $w_{2}$ and $w_{3}$. We have
$\overline{t}(w_{1})=\\{p_{B},q,r\\}$, $\overline{t}(w_{2})=\\{p_{C},q,r\\}$,
and $\overline{t}(w_{3})=\\{p_{D},q,r\\}$. Worlds $w_{1}$, $w_{2}$ and $w_{3}$
here represent the possible scenarios considered by Alice. With the current
available knowledge these worlds are indistinguishable from each other for
Alice. This can be represented by $R=W\times W$. At any world $w$
$Eq(r,w)=\Box q$, i.e. Alice moves to the East iff she knows point $A$ is to
the East of her current location. Here, in the world $w_{1}$ in which Alice is
at $B$ (the real situation), $(q,w_{1})=1$, $(q,w_{2})=1$ and $(q,w_{3})=1$
are all causes of $(r,w_{1})=1$ by all three definitions. Thus, the fact that
$A$ is to the East of point $C$ or point $D$ is also a cause of Alice moving
to East even if she is not present there.

These examples show that causal Kripke models can be used to model several
different scenarios involving causality interacting with notions like
possibility, knowledge and uncertainty.

###  5.1 Sufficient causality

Halpern discusses the notion of sufficient causality in [17] to model the fact
that people’s reasoning about causality depends on how sensitive the causality
ascription is to changes in various other factors. “The key intuition behind
the definition of sufficient causality is that not only does
$\overline{X}=\overline{x}$ suffice to bring about $\phi$ in the actual
context, but it also brings it about in other “nearby” contexts. Since the
framework does not provide a metric on contexts, there is no obvious way to
define nearby context. Thus, in the formal definition below, I start by
considering all contexts.”[17, Section 2.6] Sufficient causality is thus
defined in [17] using Definition A.2.

We can use the framework of causal Kripke models to define sufficient
causality for a causal setting $(M,u)$ in terms of nearby contexts instead of
all the contexts (as suggested by Halpern) in the following way. We consider
the causal Kripke model $\mathcal{K}=(\mathcal{S},W,R,\mathcal{F})$, where
$\mathcal{S}$ is the signature of $M$, $W$ is the set of all the possible
contexts on $M$, and $\mathcal{F}$ is the set of structural equations such
that for any structural equation for the endogenous variable $X$, $Eq(X,w)$ is
the same as the structural equation for $X$ in $M$ and the relation
$R\subseteq W\times W$ is such that $uRu^{\prime}$ iff context $u^{\prime}$ is
nearby $u$. Let $\overline{t}$ be the setting of exogenous variables so that
for any possible world the endogenous variables are set by the context
identifying that world. Let $\overline{X}=\overline{x}$ be as in Definition
A.2 and let $\overline{Y}=\overline{X}\times W$. For any $Y=(X,u)$, $Y=y$ iff
$X$ is set to be $x$ by the context ${u}$. Let
$\overline{Y}\leftarrow\overline{y}$ is intervention setting $X$ to $x$ in all
the possible contexts. In this structure we can describe sufficient causality
in terms of nearby contexts by replacing the clause $SC3$ in the Definition
A.2 by the condition

$uRu^{\prime}\quad\implies(\mathcal{K},\overline{t},u^{\prime})\models[\overline{Y}\leftarrow\overline{y}]\alpha\quad\text{or
equivalently}\quad(\mathcal{K},\overline{t},u)\models\Box[\overline{Y}\leftarrow\overline{y}]\alpha.$

We call this property $SC3$-local as we only require that the intervention
$[\overline{Y}\leftarrow\overline{y}]$ makes $\alpha$ true in nearby (not all)
contexts.

In this Section, we have mainly only considered the causal Kripke model with
only one relation which is the ”nearby” relation. However, we can also
consider causal Kripke models with multiple relations in which we have a
nearby relation $N$ on the worlds in addition to the other accessibility
relations denoting relationships between world like time, indistingushibility,
etc. The definition of sufficient causality discussed above can naturally be
extended to this setting allowing us to describe the sufficient causality in
the setting of causal Kripke models. Here, we do not go into details of this
generalization but we believe this would be an interesting direction for
future research.

##  6 Conclusions and future directions

In this paper, we have developed a possible world semantics for reasoning
about actual causality. We develop a modal language and logic to formally
reason in this framework. This language is used to generalize the HP
definitions of actual causality for this framework. We provide a sound and
complete axiomatization of the modal logic of causality developed, and give a
number of examples to illustrate how our model can be used to reason about
causality. Finally, we show that our framework allows us to define the
intended notion of sufficient causality in a straightforward and more
intuitive manner.

This work can be extended in several directions. First, results regarding the
relationship of the HP definitions with but-for causality [17, Proposition
2.2.2], and transitivity of cause [17, Section 2.4], can be generalized to our
modal setting. Secondly, we can allow for interventions on the relation $R$ in
causal Kripke models. Indeed, in many scenarios intuitively the cause for some
event is accessibility to some possible world. Allowing interventions on $R$
would allow us to model such scenarios. Finally, similar to sufficient
causality, other notions related to actual causality like normality (or
typicality) and graded causation can be described in more nuanced and possibly
multiple ways using the causal modal language.

## References

  * [1]
  * [2] Christel Baier, Clemens Dubslaff, Florian Funke, Simon Jantsch, Rupak Majumdar, Jakob Piribauer & Robin Ziemek (2021): _From Verification to Causality-Based Explications_.  In: 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021), 198, Schloss Dagstuhl–Leibniz-Zentrum f $\\{$$\backslash$” u$\\}$ r Informatik, p. 1, 10.4230/LIPIcs.ICALP.2021.1.
  * [3] Fausto Barbero, Katrin Schulz, Fernando R Velázquez-Quesada & Kaibo Xie: _Observing interventions: a logic for thinking about experiments_.  Journal of Logic and Computation, 10.1093/logcom/exac011.
  * [4] Sander Beckers (2022): _Causal explanations and XAI_.  In: Conference on Causal Learning and Reasoning, PMLR, pp. 90–109, 10.48550/arXiv.2201.13169.
  * [5] Ilan Beer, Shoham Ben-David, Hana Chockler, Avigail Orni & Richard Trefler (2012): _Explaining counterexamples using causality_.  Formal Methods in System Design 40, pp. 20–40, 10.1007/s10703-011-0132-2.
  * [6] Brian Bergstein (2020): _What AI still can’t do_.  MIT Technol Rev 123(2), pp. 1–7.  Available at https://www.technologyreview.com/2020/02/19/868178/what-ai-still-cant-do/.
  * [7] Georgiana Caltais, Stefan Leue & Mohammad Reza Mousavi (2016): _(De-) Composing Causality in Labeled Transition Systems_.  In: The 1st Workshop on Causal Reasoning for Embedded and safety-critical Systems Technologies, Eindhoven, The Netherlands, April 8, 2016, 224, Open Publishing Association, pp. 10–24, 10.4204/EPTCS.224.3.
  * [8] Georgiana Caltais, Mohammad Reza Mousavi & Hargurbir Singh (2020): _Causal reasoning for safety in Hennessy Milner logic_.  Fundamenta Informaticae 173(2-3), pp. 217–251, 10.1007/s10849-022-09357-y.
  * [9] Hana Chockler, Joseph Y Halpern & Orna Kupferman (2008): _What causes a system to satisfy a specification?_ ACM Transactions on Computational Logic (TOCL) 9(3), pp. 1–26, 10.1145/1352582.1352588.
  * [10] Anupam Datta, Deepak Garg, Dilsun Kaynar, Divya Sharma & Arunesh Sinha (2015): _Program actions as actual causes: A building block for accountability_.  In: 2015 IEEE 28th Computer Security Foundations Symposium, IEEE, pp. 261–275, 10.1109/CSF.2015.25.
  * [11] A Philip Dawid et al. (2007): _Fundamentals of statistical causality_.  RSS/EPSRC Grad Train Progr 279, pp. 1–94.  Available at https://www.semanticscholar.org/paper/FUNDAMENTALS-OF-STATISTICAL-CAUSALITY-Dawid/c4bcad0bb58091ecf9204ddb5db7dce749b0d461.
  * [12] Didier Dubois & Henri Prade (2020): _A glance at causality theories for artificial intelligence_.  A Guided Tour of Artificial Intelligence Research: Volume I: Knowledge Representation, Reasoning and Learning, pp. 275–305, 10.1007/978-3-030-06164-7_9.
  * [13] Andrea Falcon (2006): _Aristotle on causality_.  Available at https://plato.stanford.edu/entries/aristotle-causality/.
  * [14] Clark Glymour & Frank Wimberly (2007): _Actual causes and thought experiments_.  Causation and explanation 4, p. 43.  Available at https://www.semanticscholar.org/paper/Actual-Causes-and-Thought-Experiments-Glymour-Wimberly/d17f5a2896cf38b06e13713042e655e33753a69b.
  * [15] Ned Hall (2007): _Structural equations and causation_.  Philosophical Studies 132, pp. 109–136, 10.1007/s11098-006-9057-9.
  * [16] Joseph Y Halpern (2015): _A modification of the Halpern-Pearl definition of causality_.  arXiv preprint arXiv:1505.00162, 10.48550/arXiv.1505.00162.
  * [17] Joseph Y Halpern (2016): _Actual causality_.  MiT Press, 10.7551/mitpress/10809.001.0001.
  * [18] Joseph Y Halpern & Judea Pearl (2005): _Causes and explanations: A structural-model approach. Part I: Causes_.  The British journal for the philosophy of science, 10.1093/bjps/axi147.
  * [19] Joseph Y Halpern & Judea Pearl (2005): _Causes and explanations: A structural-model approach. Part II: Explanations_.  The British journal for the philosophy of science, 10.1093/bjps/axi148.
  * [20] Christopher Hitchcock (2001): _A tale of two effects_.  The Philosophical Review 110(3), pp. 361–396, 10.1215/00318108-110-3-361.
  * [21] Christopher Hitchcock (2013): _What is the ‘cause’in causal decision theory?_ Erkenntnis 78, pp. 129–146, 10.1007/s10670-013-9440-9.
  * [22] David Hume (1748): _An enquiry concerning human understanding and other writings_.
  * [23] Amjad Ibrahim, Tobias Klesel, Ehsan Zibaei, Severin Kacianka & Alexander Pretschner (2020): _Actual causality canvas: a general framework for explanation-based socio-technical constructs_.  In: ECAI 2020, IOS Press, pp. 2978–2985, 10.3233/FAIA200472.
  * [24] Florian Leitner-Fischer & Stefan Leue (2013): _Causality Checking for Complex System Models_.  In Roberto Giacobazzi, Josh Berdine & Isabella Mastroeni, editors: Verification, Model Checking, and Abstract Interpretation, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 248–267, 10.1007/978-3-642-35873-9_16.
  * [25] David Lewis (1973): _Causation_.  The journal of philosophy 70(17), pp. 556–567, 10.2307/2025310.
  * [26] David Lewis (2004): _Causation as influence_.  The Journal of Philosophy 97(4), pp. 182–197, 10.7551/mitpress/1752.003.0004.
  * [27] Alexandra Meliou, Wolfgang Gatterbauer, Joseph Y Halpern, Christoph Koch, Katherine F Moore & Dan Suciu (2010): _Causality in databases_.  IEEE Data Engineering Bulletin 33(ARTICLE), pp. 59–67.  Available at https://www.cs.cornell.edu/home/halpern/papers/DE_Bulletin2010.pdf.
  * [28] Michael S Moore (2009): _Causation and responsibility: An essay in law, morals, and metaphysics_.  Oxford University Press on Demand, 10.1093/acprof:oso/9780199256860.001.0001.
  * [29] Judea Pearl (2009): _Causality_.  Cambridge university press, 10.1017/CBO9780511803161.
  * [30] Judea Pearl & Dana Mackenzie (2018): _The book of why: the new science of cause and effect_.  Basic books, 10.1080/01621459.2020.1721245.
  * [31] Bernhard Schölkopf (2022): _Causality for machine learning_.  In: Probabilistic and Causal Inference: The Works of Judea Pearl, pp. 765–804, 10.1145/3501714.3501755.
  * [32] James Woodward (2005): _Making things happen: A theory of causal explanation_.  Oxford university press, 10.1111/j.1933-1592.2007.00012.x.

##  Appendix A HP definitions of causality and sufficient causality

######  Definition A.1 ([17], Definition 2.2.1).

Let $\alpha$ be an event obtained by Boolean combination of primitive events.
Let $\mathcal{X}\subseteq\mathcal{V}$ be a set of endogenous variables.
$\overline{X}=\overline{x}$ is an actual cause of $\alpha$ in a causal setting
$(M,\overline{t})$ if the following conditions hold.

  * AC1.

$(M,\overline{t})\Vdash\overline{X}=\overline{x}$ and
$(M,\overline{t})\Vdash\alpha$.

  * AC2a.

There is a partition of $\mathcal{V}$ into two disjoint subsets $\overline{Z}$
and $\mathcal{W}$ with $\overline{X}\subseteq\overline{Z}$ and a setting
$\overline{x}^{\prime}$ and $\overline{w}$ of variables in $\mathcal{X}$ and
$\mathcal{W}$, respectively, such that

$(M,\overline{t})\Vdash_{p}[\overline{X}\leftarrow\overline{x}^{\prime},\overline{W}\leftarrow\overline{w}]\neg\alpha.$

  * AC2$b^{o}$.

If $\overline{z}^{\ast}$ is such that
$(M,\overline{t})\Vdash\overline{Z}=\overline{z}^{\ast}$, then for all subsets
$\overline{Z}^{\prime}$ of $\overline{Z}\setminus\mathcal{X}$ we have

$(M,\overline{t})\Vdash_{p}[\overline{X}\leftarrow\overline{x},\overline{W}\leftarrow\overline{w},\overline{Z}^{\prime}\leftarrow\overline{z}^{\ast}]\alpha.$

  * AC3.

$\mathcal{X}$ is minimal set of variable that satisfy AC1 and AC2.

We say that $\overline{X}=\overline{x}$ is an actual cause of $\alpha$ in a
causal setting $(M,\overline{t})$ by updated definition iff AC1, AC2a, AC3
hold and AC2$b^{o}$ is replaced by the following condition.

If $\overline{z}^{\ast}$ is such that
$(M,\overline{t})\Vdash\overline{Z}=\overline{z}^{\ast}$, then for all subsets
$\overline{Z}^{\prime}$ of $\overline{Z}\setminus\mathcal{X}$ and
$\mathcal{W}^{\prime}$ of $\mathcal{W}$ we have

$(M,\overline{t})\Vdash_{p}[\overline{X}\leftarrow\overline{x},\overline{W}^{\prime}\leftarrow\overline{w},\overline{Z}^{\prime}\leftarrow\overline{z}^{\ast}]\alpha.$

We say that $\overline{X}=\overline{x}$ is an actual cause of $\alpha$ in a
causal setting $(M,\overline{t})$ by modified definition iff AC1, AC3 hold and
AC2 is replaced by the following condition.

If there exists a set of variables $\mathcal{W}\subseteq\mathcal{V}$, and a
setting $\overline{x}^{\prime}$ of variable in $\overline{X}$ such that if
$(M,\overline{t})\Vdash\overline{W}=\overline{w}^{\ast}$, then

$(M,\overline{t})\Vdash_{p}[\overline{X}\leftarrow\overline{x}^{\prime},\overline{W}\leftarrow\overline{w}^{\ast}]\neg\alpha.$

The following theorem describes relationship between these three definitions
of causality.

######  Definition A.2 ([17], Definition 2.6.1).

$\overline{X}=\overline{x}$ is a sufficient cause of $\alpha$ in the causal
setting $(M,\overline{u})$ if the following conditions hold:

  * SC1.

$(M,\overline{u})\models\overline{X}=\overline{x}$ and
$(M,\overline{u})\models\alpha$.

  * SC2.

Some conjunct of $\overline{X}=\overline{x}$ is part of a cause of $\alpha$ in
$(M,\overline{u})$. More precisely, there exists a conjunct $X=x$ of
$\overline{X}=\overline{x}$ and another (possibly empty) conjunction
$\overline{Y}=\overline{y}$ such that $X=x\wedge\overline{Y}=\overline{y}$ is
a cause of $\alpha$ in $(M,\overline{u})$; i.e. , AC1, AC2, and AC3 hold for
(possibly empty) conjunction $\overline{Y}=\overline{y}$ such that
$X=x\wedge\overline{Y}=\overline{y}$

  * SC3.

$(M,\overline{u}^{\prime})\models[\overline{X}\leftarrow\overline{x}]\alpha$
for all contexts $\overline{u}^{\prime}$.

  * •

$\overline{X}$ is the minimal set satisfying above properties.

##  Appendix B Relationship between three HP definitions of causality

In [17] Halpern gives examples to show that the three HP definitions do not
coincide with each other. Here we give one example to show that the modified
definition may not coincide with the original and updated definition in the
causal Kripke model. Similar example can be given to show that original and
updated definition do not coincide.

######  Example B.1 (stalemate detailed).

We consider the following variation of the example 5.2. Let $\mathcal{S}$ be
signature with endogenous variables $p_{1}$ and $p_{2}$ instead of $p$
(keeping the other endogenous variables unchanged) standing for ’The king is
in check by the opponent’s queen’ and ’The king is in check by the opponent’s
king’. Let $U=(U_{1},U_{2},U_{3})\in\\{0,1\\}^{3}$ be such that
$(p_{1},w)=(U_{1},w)$, $(p_{2},w)=(U_{2},w)$, and $(q,w)=(U_{3},w)$ for any
$w\in W$. Let the structural equation for $r$ at $w_{0}$ be given by
$r=\neg(p_{1}\vee p_{2})\wedge q\wedge\Box(p_{1}\vee p_{2})$. i.e. , the
player is forced to move the knoight if if the only pieces that can move are
the king and the knight, ther king is not in check and every possible king
move leads to king being in the check by the king or the queen (We assume
there are no other pieces on the board) of the opponenet . Let $\overline{t}$
be a context such that $U$ is set to be $(0,0,1)$,$(1,1,1)$, and $(0,1,0)$ at
the worlds $w_{0}$, $w_{1}$, and $w_{2}$ respectively. We have
$\overline{t}(w_{0})=\\{r\\}$, $\overline{t}(w_{1})=\\{p_{1},p_{2},q\\}$,
$\overline{t}(w_{2})=\\{p_{2}\\}$. In the same way as the last example we can
show that $(p_{1},w_{0})=0$, $(p_{2},w_{0})=0$,$(q,w_{0})=1$,
$(p_{1},w_{1})=1$, $(p_{2},w_{1})=1$ and $(p_{2},w_{2})=1$ are all the causes
of $r=1$ at $w_{0}$ by the original and updated definition. However, in the
case of modified definition, neither $(p_{1},w_{1})=1$ nor $(p_{2},w_{1})=1$
is the causes but $(p_{1},w_{1})=1\wedge(p_{2},w_{1})=1$ is a cause of $r=1$
at $w_{0}$. To see this notice that for any choice of $\overline{N}$ we will
always have

$(\mathcal{K},\overline{t},w_{0})\Vdash[(p_{1},w_{1})\leftarrow{x}^{\prime},\overline{N}\leftarrow\overline{n}^{\ast}]r=1.$

for any choice of ${x}^{\prime}$. Thus, $(p_{1},w_{1})=1$ is not cause of
$r=1$ at $w_{0}$ by modified definition. Similar argument holds for
$(p_{2},w_{1})=1$. However, $(p_{1},w_{1})=1\wedge(p_{2},w_{1})=1$ is a cause
is showed by setting $\overline{N}=\emptyset$ and
$\overline{x}^{\prime}=(0,0)$. Thus, three definitions of causality need not
always match in causal Kripke models.

The following theorem describes relationship between the three HP definitions
in the causal models.

######  Definition B.2 ([17], Section 2.2).

For any event $\alpha$, any variable $X$, and any world $w$, $X=x$ is a part
of cause of $\alpha$ by original (resp. updated, modified) definition of
causality if it is a conjunct in the cause of $\alpha$ by original (resp.
updated, modified) definition.

######  Theorem B.3 ([17], Theorem 2.2.3).

If $X=x$ is a part of cause of $\alpha$ in $(M,\overline{u})$ according to

  1. 1.

the modified HP definition then $X=x$ is a part of cause of $\alpha$ in
$(M,\overline{u})$ according to the original HP definition .

  2. 2.

the modified HP definition then $X=x$ is a part of cause of $\alpha$ in
$(M,\overline{u})$ according to the updated HP definition.

  3. 3.

the updated HP definition then $X=x$ is a part of cause of $\alpha$ in
$(M,\overline{u})$ according to the original HP definition.

Now, we generalize this result to our framework of causal Kripke models.

######  Definition B.4.

For any event $\alpha$, any variable $X$, and any world $w^{\prime}$,
$(X,w)=x$ is a part of cause of $\alpha$ by original (resp. updated, modified)
definition of causality if it is a conjunct in the cause of $\alpha$ at
$w^{\prime}$ by original (resp. updated, modified) definition.

######  Theorem B.5.

If $(X,w)=x$ is a part of cause of $\phi$ in $(\mathcal{K},\overline{t})$ at
$w^{\prime}$ according to

  1. 1.

the modified HP definition then $(X,w)=x$ is a part of cause of $\alpha$ in
$(\mathcal{K},\overline{t})$ at $w^{\prime}$ according to the original HP
definition.

  2. 2.

the modified HP definition then $(X,w)=x$ is a part of cause of $\alpha$ in
$(\mathcal{K},\overline{t})$ at $w^{\prime}$ according to the updated HP
definition.

  3. 3.

the updated HP definition then $(X,w)=x$ is a part of cause of $\alpha$ in
$(\mathcal{K},\overline{t})$ at $w^{\prime}$ according to the original HP
definition.

###### Proof.

For item 1, let $(X,w)=x$ be a part of cause of $\alpha$ in
$(\mathcal{K},\overline{t})$ at a world $w^{\prime}$ according to the modified
HP definition, so that there is a cause $\overline{Y}=\overline{y}$ such that
$(X,w)=x$ is one of its conjuncts. Then there must exist a value
$\overline{x}^{\prime}\in\mathcal{R}(\overline{Y})$ and a set
$\overline{N}\subseteq\mathcal{V}\times W\setminus\overline{Y}$, such that if
$(\mathcal{K},\overline{t},w)\vdash X=n^{\ast}$ for every
$(X,w)=n^{\ast}\in\overline{N}=\overline{n}^{\ast}$, then
$(\mathcal{K},\overline{t},w^{\prime})\vdash[\overline{Y}\leftarrow\overline{y},\overline{N}\leftarrow\overline{n}^{\ast}]\neg\alpha$.
Moreover $\overline{Y}$ is minimal.

We will show that $(X,w)=x$ is a cause of $\alpha$. If
$\overline{Y}=\\{(X,w)\\}$, then the original HP definition is satisfied by
$(\overline{N},\overline{n}^{\ast},x^{\prime})$ given by the condition
$AC2a^{m}$. If $|\overline{Y}|>1$, then without loss of generality let
$\overline{Y}=((X_{1},w_{1}),(X_{2},w_{2}),\cdots,(X_{n},w_{n}))$ and
$(X,w)=(X_{1},w_{1})$. For any vector $\overline{Y}$, we use
$\overline{Y}_{-1}$ to denote all components of $Y$ except the first.

We will show that $(X_{1},w_{1})$ is a cause of $\alpha$ in
$(\mathcal{K},\overline{t})$ at $w^{\prime}$ according to the original
definition. Since $\overline{Y}=\overline{y}$ is a cause of $\alpha$ in
$(\mathcal{K},\overline{t})$ at $w^{\prime}$ according to the modified
definition, by AC1 $(\mathcal{K},\overline{t},w_{1})\vdash X_{1}=x_{1}$ and
$(\mathcal{K},\overline{t},w^{\prime})\vdash\alpha$. Let
$\overline{N}^{\prime}=(\overline{Y}_{-1},\overline{N})$,
$\overline{n^{\ast}}^{\prime}=(\overline{y^{\prime}}_{-1},\overline{n^{\ast}})$,
$y^{\prime}=y_{1}^{\prime}$, where $\overline{y}^{\prime}$ is as given by the
modified definition. It is easy to see that
$(\mathcal{K},\overline{t},w^{\prime})\vdash[(X_{1},w_{1})\leftarrow
x_{1}^{\prime},\overline{Y}_{-1}\leftarrow\overline{y}_{-1},\overline{N}\leftarrow\overline{n^{\ast}}]\neg\alpha$
satisfying condition $AC2a$. Since $(X_{1},w_{1})$ is single variable, $AC3$
holds trivially. Thus, to complete the proof of $(a)$ we need to show that
$AC2b^{o}$ holds. Suppose $AC2b^{o}$ does not hold. Then there exists a subset
$\overline{Z^{\prime}}\subseteq\mathcal{V}\times
W\setminus(\overline{Y}_{-1}\cup\overline{N})$ of variables and value
$z^{\ast}$ such that (i) for each $Z\in\overline{Z^{\prime}}$,
$(\mathcal{K},\overline{t},w)\vdash Z=z^{\ast}$ and (ii)
$(\mathcal{K},\overline{t},w^{\prime})\vdash[(X_{1},w_{1})\leftarrow
x_{1},\overline{Y}_{-1}\leftarrow\overline{y}_{-1},\overline{N}\leftarrow\overline{n^{\ast}},\overline{Z^{\prime}}\leftarrow\overline{z^{\ast}}]\neg\alpha$.
But then $\overline{Y}=\overline{y}$ is not a cause of $\alpha$ according to
the modified definition. Indeed, $AC2a^{m}$ is satisfied for
$\overline{T}^{\prime}=\overline{Y}_{-1}$ by setting
$\overline{N}=((X_{1},w_{1}),\overline{N},\overline{Z^{\prime}})$ and
$\overline{n^{\ast}}=(x_{1},\overline{n^{\ast}},\overline{z^{\ast}})$ and
$\overline{t^{\prime}}=\overline{y^{\prime}}_{-1}$ violating $AC3$ for
$\overline{Y}=\overline{y}$. i.e. , $\overline{Y}=\overline{y}$ is not a
minimal cause by the modified definition as the conjunct obtained by removing
$(X_{1},w_{1})=x_{1}$ from it is still a cause by the modified definition.
This is a contradiction. Therefore, $AC2b^{o}$ is valid.

For item 2, the proof is similar in spirit. In addition to 1, we need to show
that if $\overline{Y^{\prime}}\subseteq\overline{Y}_{-1}$,
$\overline{N^{\prime}}\subseteq\overline{N}$, and
$\overline{Z^{\prime}}\subseteq\overline{Z}$, then

$(\mathcal{K},\overline{t},w)\vdash[(X,w_{1})\leftarrow
x_{1},\overline{Y}_{-1}\leftarrow\overline{y}_{-1},\overline{N^{\prime}}\leftarrow\overline{{n^{\ast}}^{\prime}},\overline{Z^{\prime}}\leftarrow\overline{{z^{\ast}}^{\prime}}\phi]$

If $X^{\prime}=\emptyset$, then the condition holds since $(X,w)=x$ is a cause
of $\phi$ according to the original definition by item 1. In case this
condition does not hold for some non-empty
$\overline{Y^{\prime}}\subseteq\overline{Y}_{-1}$, then
$\overline{Y}=\overline{y}$ does not satisfy the minimimality condition AC3 of
the modified HP definition (in causal Kripke models).

For item 3, the proof is same as item 1, upto the point where we have to prove
$AC2^{o}$. Suppose there exists $\overline{Z^{\prime}}\subseteq\overline{Z}$
such that

$(\mathcal{K},\overline{t},w)\vdash[(X,w_{1})\leftarrow
x_{1},\overline{Y}_{-1}\leftarrow\overline{y}_{-1},\overline{N^{\prime}}\leftarrow\overline{{n^{\ast}}^{\prime}},\overline{Z^{\prime}}\leftarrow\overline{{z^{\ast}}^{\prime}}\neg\phi]$

then $\overline{Y}_{-1}\leftarrow\overline{y}_{-1}$ satisfies AC2a and
$AC2b^{u}$. Thus, $\overline{Y}=\overline{y}$ does not satisfy the
minimimality condition AC3 for the updated definition. Hence proved. ∎

##  Appendix C Soundness and completeness

In this section we provide the proof of soundness and (weak) completeness of
the axiomatization given in Section 4.2. The proof is a modification of the
proof provided in [17] to include the modal operators.

###### Proof.

Showing that the axiomatization is sound is routine. It is straightforward to
verify that all the axioms except $G$-axiom are valid and that modus ponens
and necessitation preserve validity. For the G-axiom, note that the truth of
the formula $(X,w)=x$ is independent of the world $w^{\prime}$ at which it is
evaluated. Thus, if it is true at some world, then it is true at all the
worlds, in particular true at all the world related to $w$.

To prove that the axiomatization is weakly complete, we show contrapositively
that if $\nvdash\psi$ then there exists a model satisfying $\lnot\psi$. As
usual, starting with a consistent formula $\varphi$ we obtain a maximal
consistent set $\Sigma$ containing all axioms such that $\varphi\in\Sigma$, is
closed under $\land$ and consequence, and enjoys the disjunction property (see
also the proof of Theorem 5.4.1 in [17, Section 5.5]).

Before moving to the details of the proof, we provide a high-level
presentation of the argument, to help the reader follow: Given a consistent
set of formulas, we can extract the formulas that do not contain modalities.
Treating the variables $(X,w)$ and $(X,w)$ (where $w\neq w^{\prime}$) as
simply distinct variables, this set can be seen as a consistent set of
formulas for the standard logic of causality presented in [17], because the
axioms in Section 4.2 strictly extend the axioms of the logic in [17]. Then,
by the completeness presented in [17], we get a set of structural equations,
which readily provides a set of structural equations over a Kripke model with
the empty relation (where $(X,w)$ and $(X,w^{\prime})$ are now interpreted as
the same variable at different points in the Kripke model). By the soundness
of the axioms in Section 4.2, the set of non-modal formulas at each such state
is consistent. These consistent sets guarantee that the “canonical” model we
construct has enough points to interpret all the names that appear in our
finite set of formulas. The proof then follows a standard filtration argument
to show in the usual way the truth lemma for modal formulas.

Let $\varphi$ be such that $\nvdash\lnot\varphi$. Let us define
$W_{\varphi}:=\\{w\in W\mid w\text{ appears in }\varphi\\}$ and
$S_{\varphi}:=\\{\psi,\Box\psi\mid\psi\text{ is a subformula of }\varphi\\}$.
Now let $\Sigma$ be a maximal consistent set of formulas of
$\mathbf{L}(W_{\varphi})$ that contains $\varphi$. Given axiom C6 in [17,
Section 5.4] and $\Diamond$-axiom and $\Box$-axiom, we can assume without loss
of generality that all formulas are generated from
$[\overline{Y}\leftarrow\overline{y}]X=x$ and
$[\overline{Y}\leftarrow\overline{y}](X,w)=x$ using the connectives
$\Diamond,\Box,\land,\lor$ and $\lnot$. Notice that $\Sigma$ “decides” the
value of variables $(X,w)$ for every $w\in W_{\varphi}$ (that is to say,
$(X,w)=x\in\Sigma$ for some $x\in$ for some $x\in\mathcal{R}(X,w)$). Consider
the set
$B=\\{[\overline{Y}\leftarrow\overline{y}](X,w)=x\in\mathbf{L}(W_{\varphi})\mid[\overline{Y}\leftarrow\overline{y}](X,w)=x\in\Sigma\\}$.
By the completeness in [17, Section 5.5], it follows that there exists a
system of structural equations satisfying the non-modal formulas of $\Sigma$.
Using this system we can define a causal Kripke model with domain
$W_{\varphi}$, and empty Kripke relation. By the soundness of this system it
follows that for every $w\in W_{\varphi}$ the set
$\Sigma_{w}:=\\{[\overline{Y}\leftarrow\overline{y}]X=x\mid[\overline{Y}\leftarrow\overline{y}](X,w)=x\in\Sigma\\}\cup
B$ (the set $\Sigma_{w}$ includes the ) is consistent and hence can be
extended to an maximal consistent set $\Sigma^{\prime}_{w}$.

Let
$S=S_{\varphi}\cup\\{[\overline{Y}\leftarrow\overline{y}](X,w)=x,[\overline{Y}\leftarrow\overline{y}]X=x\in\mathbf{L}(W_{\varphi})\\}$.
Notice that $S$ is finite. Define an equivalence relation on maximal
consistent sets extending $B$ of $\mathbf{L}(W_{\varphi})$, $T_{1}\sim T_{2}$
if and only if $T_{1}\cap S=T_{2}\cap S$. Given that $S$ is finite, there
exist finite many equivalence classes. Let $\mathbb{W}$ be the set of
equivalence classes, and let $\mathfrak{R}\subseteq\mathbb{W}\times\mathbb{W}$
be defined as $C_{1}\mathfrak{R}C_{2}$ if and only if there exists $T_{1}\in
C_{1}$ and $T_{2}\in C_{2}$, such that for all $\psi\in T_{2}$,
$\Diamond\psi\in T_{1}$. Define a name assignment $i$ such that
$i(w)=[\Sigma^{\prime}_{w}]$ for $w\in W_{\varphi}$, and arbitrarily
otherwise. Finally define the structural equations, depending only on
variables of $W_{\varphi}$, exactly as defined in [17, Section 5.4]. In
particular the equations are independent of variables in $W\setminus
W_{\varphi}$, and $f_{(X,w)}(\overline{y})=x$, if and only if
$[\overline{Y}\leftarrow\overline{y}]X=x\in T$ for any $T\in i(w)$ (given that
$[\overline{Y}\leftarrow\overline{y}]X=x\in S$, this is well defined).

We claim that $\overline{t},[T]\Vdash\psi$ if and only if $\psi\in T$, for
every $\psi\in S$, and maximal consistent set $T$.

The proof proceeds via induction on the complexity of the formulas. For
formulas of the form $[\overline{Y}\leftarrow\overline{y}]X=x$,
$[\overline{Y}\leftarrow\overline{y}](X,w)=x$, and for logical connectives the
proof is verbatim the same as that of [17, Section 5.4].

Finally, let’s show this for the case when $\psi$ is $\Diamond\sigma$.

First, let’s assume that $\overline{t},[T]\Vdash\Diamond\sigma$. Then there
exists $C\in\mathbb{W}$ such that $[T]\mathfrak{R}C$ and
$\overline{t},C\Vdash\sigma$. By induction hypothesis $\sigma\in T^{\prime}$,
for every $T^{\prime}\in C$. Since $\sigma\in S$, by the definition of
$\mathfrak{R}$, it follows that $\Diamond\sigma\in T$.

For the converse direction, assume that $\Diamond\sigma\in T$. Notice
preliminarily, that since $\Diamond\top\land\Box p\Rightarrow\Diamond p$ is a
theorem of classical normal modal logic, then
$(\Diamond\top\land\Box([\overline{Y}\leftarrow\overline{y}](X,w)=x))\Rightarrow\Diamond[\overline{Y}\leftarrow\overline{y}](X,w)=x$
is provable in our system. From the G-axiom, this implies that also

$(\Diamond\top\land([\overline{Y}\leftarrow\overline{y}](X,w)=x))\Rightarrow\Diamond[\overline{Y}\leftarrow\overline{y}](X,w)=x$
(1)

is provable. Consider the set
$Z_{T}=\\{\tau\in\mathbf{L}(W_{\varphi})\mid\Diamond\tau\notin T\\}$. Clearly
$Z_{T}$ is an ideal of the free Boolean algebra of the logic. Given that
$B\subseteq T$ and $\Diamond\sigma\in T$, it follows that $\Diamond\top\in T$,
and by (1) it follows that $\Diamond B\subseteq T$ and so $B\cap
Z_{T}=\varnothing$. Hence there exists a maximal consistent set $T^{\prime}$,
extending $B\cap\\{\sigma\\}$ such that $T^{\prime}\cap Z_{T}=\varnothing$. By
definition $[T]\mathfrak{R}[T^{\prime}]$, and hence
$\overline{t},[T]\Vdash\Diamond\sigma$, as required.

The proof, that the model is recursive, follows again the proof of [17,
Section 5.4], using the fact that our Kripke frame is finite. ∎