# Cantor-Bernstein implies Excluded Middle

Pierre Pradic ENS de Lyon, Université de Lyon, LIP and University of Warsaw,
MIMUW Chad E. Brown Czech Technical University in Prague

###### Abstract

We prove in constructive logic that the statement of the Cantor-Bernstein
theorem implies excluded middle. This establishes that the Cantor-Bernstein
theorem can only be proven assuming the full power of classical logic. The key
ingredient is a theorem of Martín Escardó stating that quantification over a
particular subset of the Cantor space $2^{\mathbb{N}}$, the so-called one-
point compactification of $\mathbb{N}$, preserves decidable predicates.

The _Cantor-Bernstein theorem_ is an elementary statement ${\mathbb{CB}}$ of
set theory: for any two sets $A$ and $B$, if there are injections
$f:A\hookrightarrow B$ and $g:B\hookrightarrow A$, then there exists a
bijection $h:A\xrightarrow{\sim}B$. An interesting feature of this theorem is
that it may be proven in ZF without assuming the axiom of choice. However,
this proof is non-constructive in the sense that it goes through classical
logic; while the construction of the bijection $h$ is rather explicit, one
needs to appeal to excluded middle to show that it is indeed a bijective
function.

Models of constructive set theory invalidating ${\mathbb{CB}}$ are known, such
as for instance, models based on Kleene realizability111For instance, consider
the subset $H\subseteq\mathbb{N}$ corresponding to the halting problem. If
${\mathbb{CB}}$ held in the effective topos, we would have a recursive
bijection $\mathbb{N}\xrightarrow{\sim}\\{2n\mathrel{|}n\notin
H\\}\cup\\{2n+1\mathrel{|}n\in\mathbb{N}\\}$; since it is in particular
surjective, we would be able to build a recursive enumeration of the
complement of $H$, which is absurd.. However, it left open the question of
whether the full power of _excluded middle_ $({\mathbb{EM}})$ is really
necessary to prove the theorem or if a weaker classical principle would be
enough. The purpose of this note is to show that, indeed, full excluded middle
is required because of the following theorem.

######  Theorem 1.

$({\mathbb{CB}}\Rightarrow{\mathbb{EM}})$ Over intuitionistic set theory, the
Cantor-Bernstein theorem implies the principle of excluded middle.

The argument is a straightforward application of a key theorem of Martín
Escardó [3] concerning the one-point compactification ${\mathbb{N}_{\infty}}$
of $\mathbb{N}$ and decidable predicates: there exists a function

$\varepsilon\quad:\quad({\mathbb{N}_{\infty}}\to
2)\quad\longrightarrow\quad{\mathbb{N}_{\infty}}$

selecting a counter-witness for its input when possible. Formally speaking, it
means that for any decidable predicate $P:{\mathbb{N}_{\infty}}\to 2$, we have
the following equivalence222This should not be confused with Hilbert’s
$\varepsilon$ which dually selects _witnesses_ of existential statements..

$\big{(}\forall
p\in{\mathbb{N}_{\infty}}.\;P(p)=1\big{)}\qquad\Longleftrightarrow\qquad
P(\varepsilon(P))=1$

This result is rather striking as it means that there exists an infinite
set333By which we systematically mean Dedekind-infinite here. for which
decidable predicates are stable under quantification, _provably in
constructive logic_. This is to be contrasted against the case of
$\mathbb{N}$, which admits no recursive selection function.

Assuming the existence of _any_ infinite set equipped with a selection
function, ${\mathbb{CB}}\Rightarrow{\mathbb{EM}}$ may be proven by very
elementary means. The reader familiar with [3] may content themselves with the
proofs of Lemma 7 and Theorem 1. Section 3 as a whole gives a self-contained
proof of ${\mathbb{CB}}\Rightarrow{\mathbb{EM}}$, integrating the necessary
technical content from [3] about ${\mathbb{N}_{\infty}}$. For the more casual
reader, we first give a preliminary example of an elementary set-theoretic
statement implying excluded middle in Section 1 to show how the main theorem
and many similar statements are proven by considering subsingleton sets. We
then give an already-known proof [1] of a weaker variant of Theorem 1 in
Section 2 for didactic purposes, before moving on to the proof of the main
theorem.

### Foundational and notational preliminaries

We work in a constructive set theory such as IZF or CZF where we do not assume
excluded middle upfront. For our purpose, the distinction between these two
systems will not be relevant. We shall reason informally and trust that the
reader knowledgeable of other foundations be able to adapt the argument to
other settings. We assume that the axioms of Zermelo’s set theory hold. Among
other things, this means that our universe of sets is closed under pairing,
union, powerset (which we write $\mathcal{P}(-)$) and set comprehension. For
sets $A$ and $B$, function spaces $B^{A}$ and disjoint unions $A+B$ are built
as usual. We write ${\sf inl}:A\to A+B$ and ${\sf inr}:B\to A+B$ for the usual
injections into disjoint unions. In particular, for every $x\in A+B$ there is
either an $a\in A$ such that $x={\sf inl}(a)$ or $b\in B$ such that $x={\sf
inr}(b)$. Let $0=\emptyset$, $1=\\{0\\}$ and $2=\\{0,1\\}\cong 1+1$.

In set theory, propositions or truth values can be arranged as a set
$\Omega=\mathcal{P}(1)$, which is closed under all logical connective. For a
formal proposition $p\in\Omega$, we sometimes abbreviate “$p=1$” by “$p$” when
writing formulas. _Excluded middle_ ${\mathbb{EM}}$ may then be formally
written as $\forall p\in\Omega.\;p\vee\neg p$444Note that the scheme $\forall
x.\;\varphi(x)\vee\neg\varphi(x)$ for arbitrary $\varphi$ is no more general
since it can be recovered by set comprehension.. Note that an equivalent
formulation of ${\mathbb{EM}}$ in this setting is $\Omega\cong 2$, which is
_not_ the case in constructive settings. In the sequel, although they are
definitionally the same in set theory, we often make a notational distinction
between propositions $p\in\Omega$ and subsets $A\subseteq 1$ in order to keep
the arguments more readable.

Finally, and crucially555Interestingly, one may easily construct models of
finitary models satisfying ${\mathbb{CB}}$ but not ${\mathbb{EM}}$: take the
internal logic of the topos ${\sf Finset}^{\mathcal{C}^{\text{op}}}$. If
$\mathcal{C}$ is not a groupoid, ${\mathbb{EM}}$ is not satisfied, while
${\mathbb{CB}}$ always hold in the internal logic. This indicates that
assuming the axiom of infinity is essential here., we assume the axiom of
infinity: there exists a Dedekind-infinite set $\mathbb{N}$ minimal for
inclusion. We leave to the reader to disambiguate e.g. addition of numbers and
disjoint union from context.

### Related works

We do not reprove ${\mathbb{EM}}\Rightarrow{\mathbb{CB}}$ here; while it is
not necessary to read this note, they motivate a strengthening of
${\mathbb{CB}}$ metionned in Definition 4. Any introduction to set theory
should have a satisfactory proof; for reference, one may look at Theorem 3.2
in [5]. For a historical perspective, the reader may be interested in [4]. The
question of the nonconstructivity of ${\mathbb{CB}}$ from the categorical
point of view was studied by Banaschewski and Brümmer in [1] and mentioned in
Johnstone’s Elephant [6] (Lemma D4.1.12, p. 950).

##  1 An elementary set-theoretic statement implying ${\mathbb{EM}}$

Let us start with an example of a lemma involving functions which may proved
in an introduction to elementary set theory.

######  Proposition 2.

Let $A$ and $B$ be sets and $f:A\to B$ an injective function. Suppose that $A$
is non-empty. If excluded middle holds, then there exists a surjection $g:B\to
A$.

###### Proof.

Since $A$ is non-empty, one can pick a default element $d\in A$. By excluded
middle, we know for every $y\in B$ either there exists an $x\in A$ such that
$f(x)=y$ or no such $x$ exists. Hence we can define $g$ by cases as follows:

$g(y):=\left\\{\begin{array}[]{lr}x&{\mbox{ if }}f(x)=y\\\ d&{\mbox{ if no
such }}x{\mbox{ exists}}\end{array}\right.$

Note $g$ is well defined since $f$ is injective, and $g$ is clearly
surjective. ∎

Notice that in this little proof, one needs to make a case analysis using
excluded middle. As in the case of Cantor-Bernstein, one can ask if this is
necessary. In fact, it is necessary as we now prove.

######  Proposition 3.

Suppose for all sets $A$ and $B$ there is a surjective function $g:B\to A$
whenever $A$ is nonempty and there is an injective function $f:A\to B$. Then
excluded middle holds.

###### Proof.

Let $p\in\Omega$ be given and consider $A\mathrel{:=}\\{0\mathrel{|}p\\}$.
There is clearly an injection $f:A+1\to 2$ given by $f({\sf inl}(x))=0$ for
$x\in A$ and $f({\sf inr}(0))=1$. Note that $A+1$ is non-empty, as ${\sf
inr}(0)\in A+1$. Applying our assumption, we obtain a surjection $g:2\to A+1$.
Note that $\forall i\in 2.\;g(i)={\sf inl}(0)\lor g(i)={\sf inr}(0)$ holds
because of the universal property of disjoint unions. Hence we have two cases.

  * •

Suppose $g(i)={\sf inl}(0)$ for some $i\in 2$. In this case $0\in A$ and so
$p$ holds.

  * •

Suppose $g(0)={\sf inr}(0)$ and $g(1)={\sf inr}(0)$. We prove $\neg p$ holds.
To this end, assume $p$ holds. Hence $0\in A$. Since $g$ is surjective there
must be some $i\in 2$ such that $g(i)={\sf inl}(0)$, contradicting our
assumption.

∎

Here, the strategy was fairly simple: take the $A\subseteq 1$ associated to
the proposition, and try to make it fit in the hypothesis of the lemma using
disjoint unions and singletons. The situation in the proof can be visualized
as follows:

$\vbox{\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
6.75pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{1\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces{\hbox{\kern-2.72223pt\raise-9.81943pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{+}$}}}}}\ignorespaces{}{\hbox{\kern-6.75pt\raise-19.63887pt\hbox{\hbox{\kern
0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{A}$}}}}}}}\ignorespaces}}}}\ignorespaces}\left\\{\quad\vbox{
\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
6.8889pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\bullet\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
30.8889pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
30.8889pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\bullet}$}}}}}}}{\hbox{\kern-6.8889pt\raise-16.53886pt\hbox{\hbox{\kern
0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\divideontimes\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\kern
30.8889pt\raise-16.53886pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}{\hbox{\kern
30.8889pt\raise-16.53886pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\bullet}$}}}}}}}\ignorespaces}}}}\ignorespaces}\quad\right\\}2\hskip
20.0pt\longmapsto\hskip 20.0pt\vbox{\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
6.8889pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\bullet}$}}}}}}}{\hbox{\kern 30.8889pt\raise
0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\bullet}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
5.50002pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\divideontimes}$}}}}}}}{\hbox{\kern
30.8889pt\raise-16.53886pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\bullet}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
6.8889pt\raise-16.53886pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces}}}}\ignorespaces}\text{\quad
or \quad}\vbox{\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
6.8889pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\bullet}$}}}}}}}{\hbox{\kern 30.8889pt\raise
0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\bullet}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\kern
6.8889pt\raise-13.41061pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\divideontimes}$}}}}}}}{\hbox{\kern
30.8889pt\raise-16.53886pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\bullet}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\kern
5.50002pt\raise-2.49219pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces}}}}\ignorespaces}\text{\quad
or \quad}\vbox{\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
6.8889pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\bullet}$}}}}}}}{\hbox{\kern 30.8889pt\raise
0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\bullet}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
5.50002pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\divideontimes}$}}}}}}}{\hbox{\kern
30.8889pt\raise-16.53886pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\bullet}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\kern
5.50002pt\raise-2.49219pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces}}}}\ignorespaces}$

##  2 Reversing Cantor-Bernstein-Banaschewski-Brümmer

One can try to adopt a similar strategy for proving that Cantor-Bernstein
implies excluded middle.

Provided some $A\subseteq 1$, one can start building an injection $f:A\to 1$.

$\textstyle{\divideontimes\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\bullet}$

However, we need to have an injection going back and we are unsure of the
existence of an element in $A$. So let us consider the obvious injection $1\to
A+1$.

$\textstyle{\divideontimes\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\bullet}$$\textstyle{\bullet}$

Again we need a new value to be the image under $f$ of this latest element,
which leads us to consider $2$. Since we still do not have two injections, one
might be tempted to iterate this process.

$\textstyle{\divideontimes\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\bullet}$$\textstyle{\bullet\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\bullet}$
$\textstyle{\divideontimes\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\bullet}$$\textstyle{\bullet\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\bullet}$$\textstyle{\bullet}$
$\textstyle{\divideontimes\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\bullet}$$\textstyle{\bullet\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\bullet}$$\textstyle{\bullet\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\bullet}$$\scriptstyle{\vdots}$

This informal discussion suggests using $\mathbb{N}$ and the following
injections.

$\vbox{\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
6.75pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces{\hbox{\kern-2.72223pt\raise-21.41666pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{+}$}}}}}\ignorespaces{}{\hbox{\kern-6.75pt\raise-42.83331pt\hbox{\hbox{\kern
0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\mathbb{N}}$}}}}}}}\ignorespaces}}}}\ignorespaces}\left\\{\quad\vbox{\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
6.8889pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\divideontimes\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\kern
30.8889pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}{\hbox{\kern
30.8889pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\bullet}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\kern
5.50002pt\raise-14.0413pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\bullet\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
30.8889pt\raise-16.53886pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
30.8889pt\raise-16.53886pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\bullet}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\kern
5.50002pt\raise-29.64687pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\bullet\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
30.8889pt\raise-31.98329pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
30.8889pt\raise-31.98329pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\bullet}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\kern
3.0pt\raise-44.11566pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces{\hbox{\kern
15.56944pt\raise-45.2055pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\vdots}$}}}}}\ignorespaces{}{\hbox{\kern
33.3889pt\raise-45.2055pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern-3.0pt\raise-56.2055pt\hbox{\hbox{\kern
0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces{\hbox{\kern
15.56944pt\raise-56.2055pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\vdots}$}}}}}\ignorespaces{}{\hbox{\kern
33.3889pt\raise-56.2055pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces}\quad\right\\}\mathbb{N}\hskip
40.0pt\begin{array}[]{lrclcllcl}f:&\mathbb{N}&\longrightarrow&A+\mathbb{N}\\\
&n&\mapsto&{\sf inr}(n)\\\ &&&\\\
g:&A+\mathbb{N}&\longrightarrow&\mathbb{N}\\\ &{\sf inl}(0)&\mapsto&0\\\ &{\sf
inr}(n)&\mapsto&n+1\par\end{array}$

${\mathbb{CB}}$ then provides a bijection $h:\mathbb{N}\to A+\mathbb{N}$. In
fact, in elementary proofs of the theorem this bijection can be seen as a
perfect matching of the above graph. Note however that the usual statement
${\mathbb{CB}}$ conceals this relationship between $f,g$ and $h$. Banaschewski
and Brümmer [1] studied the corresponding strengthened version of
${\mathbb{CB}}$, which we dub ${\mathbb{CBBB}}$, in a categorical setting and
proved that it implied excluded middle.

######  Definition 4.

We say _${{\mathbb{CBBB}}}$ holds_ if the following statement holds: given
sets $A$ and $B$ and injections $f:A\to B$ and $g:B\to A$, there is a
bijection $h:A\to B$ such that for all $x\in A$ and $y\in B$, $f(x)=y$ or
$x=g(y)$ whenever $h(x)=y$.

Let us remark that it is obvious that
${\mathbb{CBBB}}\Rightarrow{\mathbb{CB}}$. Let us also stress that
${\mathbb{EM}}\Rightarrow{\mathbb{CBBB}}$ can be easily obtained by adapting
elementary proofs of ${\mathbb{EM}}\Rightarrow{\mathbb{CB}}$.

######  Theorem 5 (Proposition 4.1 in [1]).

If ${{\mathbb{CBBB}}}$ holds, then excluded middle holds.

###### Proof.

Assume ${{\mathbb{CBBB}}}$ holds. Let a proposition $p\in\Omega$ be given,
seen as a subset $A=\\{0\mathrel{|}p\\}\subseteq 1$. Take $f:\mathbb{N}\to
A+\mathbb{N}$ and $g:A+\mathbb{N}\to\mathbb{N}$ to be the injections described
above.

By ${{\mathbb{CBBB}}}$ there is a bijection $h:\mathbb{N}\to A+\mathbb{N}$
such that $f(x)=y$ or $g(y)=x$ whenever $h(x)=y$ for $x\in\mathbb{N}$ and
$y\in A+\mathbb{N}$. We know either $h(0)={\sf inl}(0)$ or $h(0)={\sf inr}(n)$
for some $n\in\mathbb{N}$.

  * •

If $h(0)={\sf inl}(0)$, then $0\in A$ and so $p$ holds.

  * •

Suppose $h(0)={\sf inr}(n)$ for some $n\in\mathbb{N}$. We will prove $\neg p$
holds. To this end, assume $p$ holds, so that $0\in A$. Since $h$ is
surjective, there is some $m\in\mathbb{N}$ such that $h(m)={\sf inl}(0)$.
Either $f(m)={\sf inl}(0)$ or $g({\sf inl}(0))=m$. The first case is
impossible since $f(m)={\sf inr}(m)$ by the definition of $f$ and ${\sf
inl}(0)\not={\sf inr}(m)$. Therefore, $g({\sf inl}(0))=m$ and, by definition
of $g$, we must have $m=0$. This is also impossible since it implies ${\sf
inl}(0)=h(m)=h(0)={\sf inr}(n)$.

∎

##  3 Reversing Cantor-Bernstein

Let us pause a moment and consider why we failed to prove the analogue of
Proposition 3. In that proof of that proposition lemma, we did not use any
information about the surjection $g$. Instead, we resorted to exhasutively
enumerating the set $2$ to check whether we had some $x\in 2$ such that
$g(x)={\sf inr}(0)$, which is a decidable property. This feature of $2$ of
being searchable may be formalized using the notion of _omniscience_.

######  Definition 6 (Omniscient sets).

We say a set $O$ is _omniscient_ if for every $p\in 2^{O}$ if either there
exists $x\in O$ such that $p(x)$ is equal to $0$, or $p$ is constantly equal
to $1$. That is,

$\forall p\in{2^{O}}.(\exists x\in O.p(x)=0)\vee(\forall x\in O.p(x)=1)$

In classical logic, all sets are clearly omniscient, but this is not
necessarily true in constructive logics. However, all finite sets, and in
particular $2$, are omniscient. This concept allows us to isolate the actual
core of the proof of Proposition 3.

######  Lemma 7.

Suppose that we have an omniscient set $O$ and some sets $A$ and $B$. If there
exists a surjection $f:O\to A+B$, then either $A$ is inhabited or it is empty.

###### Proof.

Let $f:O\to A+B$ be given and define $p\in 2^{O}$ by

$p(x)=\left\\{\begin{array}[]{lr}0&{\mbox{ if }}\exists a\in A.\;f(x)={\sf
inl}(a)\\\ 1&{\mbox{ if }}\exists b\in B.\;f(x)={\sf
inr}(b)\end{array}\right.$

Since $O$ is omniscient either $\exists x.\;P(x)=0$ or $\forall x\in
O.\;P(x)=1$. If $\exists x\in O.\;P(x)=0$, then $A$ is clearly inhabited.
Suppose $P(x)=1$ for every $x\in O$. We will prove $A$ is empty. Suppose $a\in
A$. Since $f$ is surjective there must be some $x\in O$ such that $f(x)={\sf
inl}(a)$, contradicting $P(x)=1$. ∎

From ${{\mathbb{CB}}}$ (instead of the stronger ${{\mathbb{CBBB}}}$) we could
use the injections from the proof of Theorem 5 to obtain a surjection
$\mathbb{N}\to A+\mathbb{N}$. If $\mathbb{N}$ were omniscient, then we could
use this surjection with Lemma 7 to ${\mathbb{EM}}$. However, omniscience of
$\mathbb{N}$ correspond to the axiom of _limited principle of omniscience_
(${\mathbb{LPO}}$) a well-known constructive taboo [2], which can be thought
of as a (strictly weaker) version of ${\mathbb{EM}}$666 Remark that, at this
point, we have ${\mathbb{LPO}}\wedge{\mathbb{CB}}\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ {\mathbb{EM}}$ over constructive set theory.
This observation is however not necessary to carry out the subsequent
argument.. This means that deriving ${\mathbb{EM}}$ from the existence of
bijections $\mathbb{N}\cong 1+\mathbb{N}$ by way of Lemma 7 is unreasonable.
Luckily, Escardó proved that there exists an infinite subset of the Cantor
space, ${\mathbb{N}_{\infty}}$, which is omniscient [3] and can be used to
prove ${\mathbb{CB}}\Rightarrow{\mathbb{EM}}$.

In order to keep the argument self-contained, we reproduce his argument below
before deriving the main result.

######  Definition 8.

We define ${\mathbb{N}_{\infty}}$ to be the set of non-increasing sequences in
$2^{\mathbb{N}}$, i.e.777For more categorically-inclined people,
${\mathbb{N}_{\infty}}$ is the final coalgebra for the functor $X\mapsto 1+X$.
This justifies calling ${\mathbb{N}_{\infty}}$ the set of conatural numbers.
The induced topology from $2^{\mathbb{N}}$ in Definition 8 also justifies
calling ${\mathbb{N}_{\infty}}$ the _one-point compactification of
$\mathbb{N}$_.,

${\mathbb{N}_{\infty}}=\big{\\{}p\in 2^{\mathbb{N}}\mathrel{\big{|}}\forall
n\in\mathbb{N}.\leavevmode\nobreak\ \big{(}p(n)=1\;\Rightarrow\;\forall
m\in\mathbb{N}.\leavevmode\nobreak\
(m<n\;\Rightarrow\;p(m)=1)\big{)}\big{\\}}.$

Let $\omega\in{\mathbb{N}_{\infty}}$ denote the constant $1$ function. We
define an injection taking $n\in\mathbb{N}$ to
$\underline{n}\in{\mathbb{N}_{\infty}}$ by taking

$\underline{n}(m)=\left\\{\begin{array}[]{lr}1&{\mbox{ if }}m<n\\\ 0&{\mbox{
otherwise.}}\end{array}\right.$

Finally we define $\underline{{\sf
S}}:{\mathbb{N}_{\infty}}\to{\mathbb{N}_{\infty}}$ by cases taking
$\underline{{\sf S}}(p)(0)=1$ and $\underline{{\sf S}}(p)(n+1)=p(n)$.

The set ${\mathbb{N}_{\infty}}$ is infinite as witnessed by $\underline{0}$
and $\underline{{\sf S}}$.

######  Lemma 9.

The function $\underline{{\sf
S}}:{\mathbb{N}_{\infty}}\to{\mathbb{N}_{\infty}}$ is injective and
$\underline{{\sf S}}(p)\not=\underline{0}$ for all
$p\in{\mathbb{N}_{\infty}}$.

###### Proof.

Suppose $\underline{{\sf S}}(p)=\underline{{\sf S}}(q)$. Since
$p(n)=\underline{{\sf S}}(p)(n+1)=\underline{{\sf S}}(q)(n+1)=q(n)$ for every
$n\in\mathbb{N}$ we know $p=q$, as desired. The fact that $\underline{{\sf
S}}(p)\not=\underline{0}$ for all $x\in{\mathbb{N}_{\infty}}$ follows from
$\underline{{\sf S}}(p)(0)=1\not=0=\underline{0}(0)$. ∎

Classically every element of ${\mathbb{N}_{\infty}}$ is either $\omega$ or of
the form $\underline{n}$. The corresponding disjunction is equivalent to
${\mathbb{LPO}}$, and so is unprovable constructively. However, for decidable
predicates, it is sufficient to show that they hold over all elements
$\underline{n}$ and $\omega$ to show they hold everywhere888This constitutes a
particular case of Lemma 3.4 in [3]..

######  Lemma 10.

Let $Q\in 2^{\mathbb{N}_{\infty}}$ be given. If $Q(\omega)=1$ and $\forall
n\in\mathbb{N}.\leavevmode\nobreak\ Q(\underline{n})=1$, then $\forall p\in
2^{\mathbb{N}_{\infty}}.\leavevmode\nobreak\ Q(p)=1$.

###### Proof.

Let $Q\in 2^{\mathbb{N}_{\infty}}$ such that $Q(\omega)=1$ and $\forall
n\in\mathbb{N}.\leavevmode\nobreak\ Q(\underline{n})=1$. Let
$p\in{\mathbb{N}_{\infty}}$ be given. To prove $Q(p)=1$, it is enough to prove
$Q(p)\not=0$. Assume $Q(p)=0$. Under this assumption we can prove $\forall
n\in\mathbb{N}.\leavevmode\nobreak\ p(n)=1$ by strong induction. Assume
$\forall k\in\mathbb{N}.\leavevmode\nobreak\ (k<n\Rightarrow p(k)=1)$ and
$p(n)=0$. This is enough information to infer $p=\underline{n}$, contradicting
$Q(p)=0$ and $Q(\underline{n})=1$. To end the proof we note that $p$ must be
$\omega$ (since $\forall n\in\mathbb{N}.\leavevmode\nobreak\ p(n)=1$),
contradicting $Q(p)=0$ and $Q(\omega)=1$. ∎

While the desired function
$\varepsilon:2^{{\mathbb{N}_{\infty}}}\to{\mathbb{N}_{\infty}}$ is rather
straightforward to define, Lemma 10 is critical in allowing to prove
constructively that it is indeed a selection function.

######  Theorem 11 (Theorem 3.15 in [3]).

There is a function
$\varepsilon:2^{{\mathbb{N}_{\infty}}}\to{\mathbb{N}_{\infty}}$ such that for
every $Q\in 2^{{\mathbb{N}_{\infty}}}$, if $Q(\varepsilon(Q))=1$, then
$\forall p\in 2^{\mathbb{N}_{\infty}}.\leavevmode\nobreak\ Q(p)=1$.

###### Proof.

For $Q\in 2^{{\mathbb{N}_{\infty}}}$, take $\varepsilon(Q)\in 2^{\mathbb{N}}$
to be

$\varepsilon(Q)(n)=\left\\{\begin{array}[]{lr}1&{\mbox{ if
}}Q(\underline{k}){\mbox{ for each }}k\leq n\\\ 0&{\mbox{
otherwise.}}\end{array}\right.$

This may be well-defined recursion over $n$. It is easy to check that
$\varepsilon(Q)\in{\mathbb{N}_{\infty}}$ as well.

Assume $Q(\varepsilon(Q))=1$ and let $p\in{\mathbb{N}_{\infty}}$ be given. If
$\forall k<n.\;Q(\underline{k})=1$ and $Q(\underline{n})=0$, then
$\varepsilon(Q)=\underline{n}$ and so $Q(\underline{n})=Q(\varepsilon(Q))=1$,
contradicting $Q(\underline{n})=0$. Consequently, $Q(\underline{n})=1$ for
every $n$ by induction. Thus $\varepsilon(Q)=\omega$ and so
$Q(\omega)=Q(\varepsilon(Q))=1$ holds as well. Hence $Q(p)=1$ for every $p\in
2^{\mathbb{N}}$ by Lemma 10. ∎

######  Corollary 12 (Corollary 3.6 in [3]).

The set ${\mathbb{N}_{\infty}}$ is omniscient.

###### Proof.

Let $Q\in 2^{{\mathbb{N}_{\infty}}}$ be given. If $Q(\varepsilon(Q))=0$, then
$\exists x\in{\mathbb{N}_{\infty}}.Q(x)=0$. If $Q(\varepsilon(Q))=1$, then
$\forall x\in{\mathbb{N}_{\infty}}.\;Q(x)=1$ by Theorem 11. ∎

This completes the part of the construction we obtained following Escardó [3].
We can now easily put it together with Lemma 7 to conclude.

###### Proof of Theorem 1.

Assume ${{\mathbb{CB}}}$ holds. We know ${\mathbb{N}_{\infty}}$ is omniscient
by Lemma 12. We know $\underline{{\sf S}}$ is injective and $\underline{{\sf
S}}(x)\not=\underline{0}$ for every $x\in{\mathbb{N}_{\infty}}$ by Lemma 9.
Let $p\in\Omega$ be a proposition and take $A=\\{0\mathrel{|}p\\}\subseteq 1$.
Analogously to Section 2, we consider the following functions:

$\begin{array}[]{lcclcccl}f:&{\mathbb{N}_{\infty}}&\longrightarrow&A+{\mathbb{N}_{\infty}}&\phantom{aaaaaaa}g:&A+{\mathbb{N}_{\infty}}&\longrightarrow&{\mathbb{N}_{\infty}}\\\
&x&\mapsto&{\sf inr}(x)&&{\sf inl}(0)&\mapsto&\underline{0}\\\ &&&&&{\sf
inr}(x)&\mapsto&\underline{{\sf S}}(x)\end{array}$

Both $f$ and $g$ are clearly injective, so we can apply ${{\mathbb{CB}}}$ to
obtain a bijection $h:{\mathbb{N}_{\infty}}\to A+{\mathbb{N}_{\infty}}$. Lemma
7 now implies that either $A$ is inhabited (so $p$ holds) or $A$ is empty (so
$\neg p$ holds). ∎

## References

  * [1] G. C.L. Banaschewski, B.; Brümmer.  Thoughts on the Cantor-Bernstein Theorem.  Quaestiones Mathematicae, 9, 01 1986.
  * [2] E. Bishop.  Foundations of constructive analysis.  McGraw-Hill, 1967.
  * [3] M. Escardó.  Infinite sets that satisfy the principle of omniscience in any variety of constructive mathematics.  J. Symb. Log., 78(3):764–784, 2013.
  * [4] A. Hinkis.  Proofs of the Cantor-Bernstein Theorem: A Mathematical Excursion.  Science Networks. Historical Studies, Vol. 45. Birkhäuser (Springer Basel), 2013.
  * [5] T. Jech.  Set theory.  Springer Science & Business Media, 2013.
  * [6] P. T. Johnstone.  Sketches of an Elephant: A Topos Theory Compendium: 2 Volume Set.  Oxford University Press UK, 2002.


Algorithm 1 therefore decides query entailment in $(\kappa-1)\text{-\text{{\sc
NExpSpace}}}$, and we get membership in $(\kappa-1)\text{-\text{{\sc
ExpSpace}}}$ by Savitch’s Theorem.

We show hardness via reduction from the word problem for alternating Turing
Machines (ATMs) with a $(\kappa-1)$-exponential time bound, which is
$(\kappa-1)\text{-\text{{\sc ExpSpace}}}$-complete (Chandra et al., 1981).

Let $\mathcal{M}=\langle{Q,\Gamma,\Delta,q_{0},t}\rangle$ be an ATM with a
finite set of states $Q$, a finite tape alphabet $\Gamma$ consisting of an
input alphabet and a special symbol ␣ (blank), a transition relation
$\Delta\subseteq(Q\times\Gamma)\times(Q\times\Gamma\times\\{l,r\\})$, an
initial state $q_{0}\in Q$, and a function
$t:Q\to\\{\exists,\forall,\text{\sf{acc}}\\}$ that marks states as
existential, universal, or accepting. As usual, we write configurations as
$w_{l}qw_{r}$ where $w_{l}$ denotes the tape symbols left of the read-write
head, $q\in Q$ is the current state, and $w_{r}$ is a sequence of symbols to
the right of the read-write head (the first symbol of which is underneath the
head). Tape symbols right of $w_{r}$ are assumed to be ␣. For a configuration
$C=w_{l}q\sigma w_{r}$ and a transition
$\langle{\langle{q,\sigma}\rangle,\langle{q^{+},\sigma^{+},d}\rangle}\rangle\in\Delta$,
there is a successor configuration

$\displaystyle
C^{+}:=\begin{cases}w_{l}\sigma^{+}q^{+}w_{r}\texttt{\textvisiblespace}&\text{if
$d=r$,}\\\ \hat{w}_{l}q^{+}\sigma_{l}\sigma^{+}w_{r}&\text{if $d=l$ and
$w_{l}=\hat{w}_{l}\sigma_{l}$ for some $\sigma_{l}\in\Gamma$.}\end{cases}$

A configuration $w_{l}qw_{r}$ is accepting if  (1) $t(q)=\text{\sf{acc}}$,
(2) $t(q)=\exists$and there is an accepting successor configuration, or  (3)
$t(q)=\forall$and all successor configurations are accepting.  $\mathcal{M}$
accepts a word $w$ if the initial configuration $q_{0}w$ is accepting.

For a word $w=\sigma_{1}\ldots\sigma_{n}$ with $n>0$ (the case of the empty
word is irrelevant for hardness), let $\mathcal{D}_{w}$ denote the database
with the facts $\mathit{first}_{0}(1)$, $\mathit{next}_{0}(i,i+1)$ for
$i\in\\{1,\ldots,n-1\\}$, $\mathit{last}_{0}(n)$, and
$\mathit{symbol}(i,\sigma_{i})$ for $i\in\\{1,\ldots,n\\}$. Let
$\Sigma_{\leq}$ denote a set of tgds constructed as in the proof of Theorem 25
to entail a $(\kappa-1)$-exponentially long chain over the initial chain
encoded in predicates $\mathit{first}_{0}$, $\mathit{next}_{0}$, and
$\mathit{last}_{0}$. We assume that the constructed $(\kappa-1)$-exponential
chain is encoded predicates $\mathit{first}$, $\mathit{next}$, and
$\mathit{last}$. Moreover, we extend $\Sigma_{\leq}$ with the following rules
to encode the transitive (non-reflexive) closure of $\mathit{next}$:

(35) $\displaystyle\mathit{next}(x,y)$
$\displaystyle\to\mathit{next}^{+}(x,y)$ (36)
$\displaystyle\mathit{next}(x,y)\wedge\mathit{next}^{+}(y,z)$
$\displaystyle\to\mathit{next}^{+}(x,z)$

We use facts $\mathit{step}(c,i)$ to encode that $c$ is an $i$th configuration
in a run, i.e., there is a sequence $c_{0},\ldots,c_{i}=c$ with $c_{0}$ being
the initial configuration, facts $\mathit{q}(c,q)$ to encode the state $q$ of
configuration $c$, facts $\mathit{hpos}(c,i)$ to encode that the head of
$\mathcal{M}$ is at the $i$th position of the tape in configuration $w$, and
facts $\mathit{tape}(c,i,s)$ to encode that the $i$th position of the tape of
configuration $c$ is symbol $s$. The following tgds
$\Sigma_{\text{\sf{init}}}$ then establish the initial configuration $c_{0}$
(with constants $c_{0}$, $q_{0}$, and ␣):

(37) $\displaystyle\mathit{first}(i)$
$\displaystyle\to\mathit{step}(c_{0},i)\land\mathit{q}(c_{0},q_{0})\land\mathit{hpos}(c_{0},i)$
(38) $\displaystyle\mathit{first}(i)\land\mathit{first}_{0}(j)$
$\displaystyle\to\mathit{samepos}(i,j)$ (39)
$\displaystyle\mathit{samepos}(i,j)\land\mathit{next}(i,i^{+})\land\mathit{next}_{0}(j,j^{+})$
$\displaystyle\to\mathit{samepos}(i^{+},j^{+})$ (40)
$\displaystyle\mathit{samepos}(i,j)\land\mathit{symbol}(j,s)$
$\displaystyle\to\mathit{tape}(c_{0},i,s)$ (41)
$\displaystyle\mathit{samepos}(i,j)\land\mathit{last}_{0}(j)\land\mathit{next}^{+}(i,i^{+})$
$\displaystyle\to\mathit{tape}(c_{0},i,\texttt{\textvisiblespace})$

The tgd (37) initialises step, state, and head position of the initial
configuration $c_{0}$. The tgds (38) and (39) match elements of the initial
chain to the first elements of the $(\kappa-1)$-exponential chain. This is
then used to transcribe the input word to the initial tape (40), with the
remaining tape filled with blanks (41).

Next, we encode how to construct a null for the successor of a configuration.
For this purpose, we introduce predicates $\mathit{to}_{\delta}$ for every
$\delta\in\Delta$, each encoding successor configurations for this transition
in a certain step. Concretely, for all $\delta,\delta^{\prime}\in\Delta$ with
$\delta=\langle{\langle{q,\sigma}\rangle,\langle{q^{+},\sigma^{+},d}\rangle}\rangle$,
the tgds $\Sigma_{+}$ contain the following tgds (with constants $q$ and
$\sigma$):

(42)
$\displaystyle\mathit{step}(C,i)\land\mathit{next}(i,i^{+})\land\mathit{hpos}(C,p)\land\mathit{tape}(C,p,\sigma)\land\mathit{q}(C,q)$
$\displaystyle\to\exists
v_{\delta}\ldotp\mathit{to}_{\delta}(i^{+},C,v_{\delta})$ (43)
$\displaystyle\mathit{to}_{\delta}(i,C^{-},C)$
$\displaystyle\to\mathit{to}_{\delta^{\prime}}(i,C,C)$ (44)
$\displaystyle\mathit{to}_{\delta}(i,C^{-},C)\land\mathit{to}_{\delta^{\prime}}(j,C^{-},C^{-})$
$\displaystyle\to\mathit{to}_{\delta^{\prime}}(j,C,C)$

The tgd (42) creates a new null for each valid transition $\delta$ from a
configuration $C$ with state $q$ and $s$ at the head position. Facts of the
form $\mathit{to}_{\delta}(i^{+},C,C^{+})$ encode that $C^{+}$ is a
$\delta$-successor of $C$ at depth $i^{+}$. The idea is that each $i$ of the
linear order encoded by $\mathit{next}$ can be used at most once per
configuration path $c_{1},\ldots,c_{n}$ to create a successor.

$\Sigma_{+}$ will induces a saturating strongly connected component in the
overall labeled dependency graph. Indeed, Definition 13 is satisfied for the
set $E=\\{v_{\delta}\stackrel{{\scriptstyle
C(\delta^{\prime})}}{{\to}}v_{\delta}^{\prime}\mid\delta,\delta^{\prime}\in\Delta\\}$,
where we use $C(\delta^{\prime})$ to disambiguate the universal variables $C$
in tgds of the form (42). Note that the empty path is the only $\bar{E}$-path
in this case. Now, for tgd $\rho_{\delta^{\prime}}$ with existential variable
$v_{\delta^{\prime}}$, tgds (43) ensure base-propagation for
$e=v_{\delta}^{\prime}\stackrel{{\scriptstyle
C(\delta^{\prime})}}{{\to}}v_{\delta^{\prime}}\in E$ and tgds (44) ensure
step-propagation for $e_{1},e_{2}=v_{\delta}^{\prime}\stackrel{{\scriptstyle
C(\delta^{\prime})}}{{\to}}v_{\delta^{\prime}}\in E$.

Next, the tgds $\Sigma_{\to}$ encode the $\delta$-successor $C^{+}$ of a
configuration $C$ based on the encoding of $C$. For
$\delta=\langle{\langle{q,\sigma}\rangle,\langle{q^{+},\sigma^{+},d}\rangle}\rangle$,
$\Sigma_{\to}$ contains the following tgds:

(45)
$\displaystyle\begin{split}\mathit{step}(C,i)\land{}\mathit{next}(i,i^{+})\land\mathit{to}_{\delta}(i^{+},C,C^{+})&\to\mathit{step}(C^{+},i^{+})\land\mathit{succ}_{\delta}(C,C^{+})\land\mathit{q}(C^{+},q^{+})\end{split}$
(46)
$\displaystyle\begin{split}\mathit{hpos}(C,p)\land\mathit{next}^{+}(p,p^{\prime})\land{}&\mathit{tape}(C,p^{\prime},s^{\prime})\land\mathit{succ}_{\delta}(C,C^{+})\\\
&\to\mathit{tape}(C^{+},p^{\prime},s^{\prime})\end{split}$ (47)
$\displaystyle\begin{split}\mathit{hpos}(C,p)\land\mathit{next}^{+}(p^{\prime},p)\land{}&\mathit{tape}(C,p^{\prime},s^{\prime})\land\mathit{succ}_{\delta}(C,C^{+})\\\
&\to\mathit{tape}(C^{+},p^{\prime},s^{\prime})\end{split}$ (48)
$\displaystyle\mathit{hpos}(C,p)\land{}\mathit{succ}_{\delta}(C,C^{+})$
$\displaystyle\to\mathit{tape}(C^{+},p,\sigma^{+})$

Here, the tgd (45) writes the step and state of $C^{+}$ and introduces a
notion $\mathit{succ}_{\delta}(C,C^{+})$, which states that $C^{+}$ is the
‘real’ $\delta$-successor of $C$ (tgds (43) and (44) makes $C^{+}$ a pseudo-
successors of itself for all $i\leq i^{+}$). The tgds (46)–(48) write the tape
of configuration $C^{+}$. Moreover, $\Sigma_{\to}$ requires tgds to update the
head position, and we make a case distinction based on the direction $d$ to
which the head moves. If $d=l$, $\Sigma_{\to}$ contains the tgd:

(49)
$\displaystyle\mathit{hpos}(C,p)\land\mathit{next}(p^{\prime},p)\land\mathit{succ}_{\delta}(C,C^{+})$
$\displaystyle\to\mathit{hpos}(C^{+},p^{\prime})$

and, otherwise, if $d=r$, $\Sigma_{\to}$ contains the tgd:

(50) $\displaystyle\mathit{hpos}(C,p)\land{}$
$\displaystyle\mathit{next}(p,p^{\prime})\land\mathit{to}_{\delta}(C,C^{+})\to\mathit{hpos}(C^{+},p^{\prime})$

Finally, we define tgds to evaluate which configurations are accepting. The
set of tgds $\Sigma_{\text{\sf{eval}}}$ contains the following tgds, where we
introduce further predicates $\mathit{acc}$ and $\mathit{acc}_{\delta}$ for
each $\delta\in\Delta$.

1\. For every state $q_{a}\in Q$ with $t(q_{a})=\text{\sf{acc}}$: (52)
$\displaystyle\mathit{q}(C,q_{a})$ $\displaystyle\to\mathit{acc}(C)$ 2\. For
every state $q_{\exists}\in Q$ with $t(q_{\exists})=\exists$, and every
transition
$\delta=\langle{\langle{q_{\exists},\sigma}\rangle,\langle{q^{+},\sigma^{+},d}\rangle}\rangle\in\Delta$:
(53) $\displaystyle\mathit{succ}_{\delta}(C,C^{+})\land\mathit{acc}(C^{+})$
$\displaystyle\to\mathit{acc}(C)$ 3\. For every state $q_{\forall}\in Q$ with
$t(q_{\forall})=\forall$, and every symbol $\sigma\in\Gamma$ with
$\delta_{1},\ldots,\delta_{n}$ a list of all transitions of form
$\langle{\langle{q_{\forall},\sigma}\rangle,\langle{q^{+},\sigma^{+},d}\rangle}\rangle\in\Delta$:
(54)
$\displaystyle\mathit{succ}_{\delta_{1}}(C,C^{+})\land\mathit{acc}(C^{+})$
$\displaystyle\to\mathit{acc}_{\delta_{1}}(C)$ (55)
$\displaystyle\mathit{acc}_{\delta_{i}}(C)\land\mathit{succ}_{\delta_{i+1}}(C,C^{+})\land\mathit{acc}(C^{+})$
$\displaystyle\to\mathit{acc}_{\delta_{i+1}}(C)$ (56)
$\displaystyle\mathit{acc}_{\delta_{i}}(C)$ $\displaystyle\to\mathit{acc}(C)$

The tgds recursively mark configurations as accepting. Concretely, (52)
directly marks all configuration with an accepting state, and (53) marks
configurations with an existential state if they have an accepting successor.
The tgds (54)–(56) mark a configuration with a universal state if all of its
successors are accepting. To achieve this, the successors are traversed in an
arbitrary but fixed order $\delta_{1},\ldots,\delta_{n}$. Semantically, one
could just combine these rules into one, but the above splitting ensures path-
guardedness. Indeed, the relation $\preceq$ of Definition 31 for the above
sets of tgds contains
$\langle{\mathit{to}_{\delta},2}\rangle\preceq\langle{\mathit{to}_{\delta},3}\rangle$
and
$\langle{\mathit{succ}_{\delta},1}\rangle\preceq\langle{\mathit{succ}_{\delta},2}\rangle$.
Therefore, all tgds are path-guarded.

To conclude, let
$\Sigma=\Sigma_{\leq}\cup\Sigma_{\text{\sf{init}}}\cup\Sigma_{+}\cup\Sigma_{\to}\cup\Sigma_{\text{\sf{eval}}}$.
As $\Sigma$ constructs and evaluates the configuration tree of $\mathcal{M}$,
we obtain that $\mathcal{M}$ accepts $w$ if and only if
$\text{\sf{chase}}(\Sigma,\mathcal{D}_{w})\models\mathit{acc}(c_{0})$. Since
$\Sigma$ is saturating with $\text{\sf{rank}}(\Sigma)=\kappa$, arboreous, and
path-guarded, this shows the claim. ∎


# RHRSegNet: Relighting High-Resolution Night-Time Semantic Segmentation

Sarah Elmahdy, Rodaina Hebishy, Ali Hamdi  MSA University
Giza, Egypt
{sarah.kamaleldeen<EMAIL_ADDRESS>
###### Abstract

Night-time semantic segmentation is a crucial task in computer vision,
focusing on accurately classifying and segmenting objects in low-light
conditions. Unlike daytime techniques, which often perform worse in nighttime
scenes, it is essential for autonomous driving due to insufficient lighting,
low illumination, dynamic lighting, shadow effects, and reduced contrast. We
propose RHRSegNet, implementing a relighting model over a High-Resolution
Network for semantic segmentation. RHRSegNet implements residual convolutional
feature learning to handle complex lighting conditions. Our model then feeds
the lightened scene feature maps into a high-resolution network for scene
segmentation. The network consists of a convolutional producing feature maps
with varying resolutions, achieving different levels of resolution through
down-sampling and up-sampling. Large nighttime datasets are used for training
and evaluation, such as NightCity, City-Scape, and Dark-Zurich datasets. Our
proposed model increases the HRnet segmentation performance by $5\%$ in low-
light or nighttime images. The code is available at the following URL:
https://github.com/SarahELMAHDY03/RHRSegNet.git.

##  I Introduction

Semantic segmentation, a fundamental task in computer vision, involves the
challenging process of assigning semantic labels to each pixel in an image.
This significant effort enhances scene understanding and aids in recognizing
objects within the visual context. Despite notable advances in semantic
segmentation for daytime conditions, addressing the complexities of low-light
conditions presents an additional set of challenges. With the growth of deep
learning and machine learning, many techniques for semantic segmentation have
recently been proposed. These methods perform very well; however, their
application to nighttime imaging has not been extensively studied. Reduced
visibility and increased noise in low-light conditions often cause existing
approaches to fail in maintaining accuracy. This work aims to close this gap
by introducing a novel strategy for semantic segmentation during nighttime.
Utilizing deep learning techniques and algorithms adapted for low-light
conditions, our goal is to enhance the precision and reliability of
segmentation. An increasing number of researchers have started to segment more
complex images under various types of degradation, such as those captured at
night or in hazy conditions. Semantic segmentation of nighttime images is the
main focus of this research, as it has numerous significant applications in
autonomous driving. In this paper, we propose RHRSegNet, a model for nighttime
semantic segmentation, using the Night-city, Cityscape, and Dark Zurich
datasets. Previous work employed an intermediate twilight domain for gradually
adapting semantic models trained in daylight scenarios to evening conditions
[5]. [14, 15] later expanded this into a guided curriculum adaptation
framework, leveraging the cross-time-of-day relationship of scene photographs
using both stylized synthetic images and unlabeled real images. However, these
progressive adaptation methods typically require training multiple semantic
segmentation models, such as the three models in [14] for three distinct
domains, which is highly inefficient. Moreover, their performance fails in
some specific circumstances. Most existing semantic segmentation approaches
are not designed for nighttime. While considerable progress has been made in
semantic segmentation for daytime scenes, tackling low-light conditions
presents unique challenges. This is particularly relevant in applications such
as autonomous driving, where accurate scene interpretation at night is crucial
for safe navigation. The primary contributions of our work are as follows: we
propose RHRSegNet, which incorporates a relighting model followed by a
segmentation model. The main contributions of our work are summarized as
follows:

  * •

We present RHRSegNet, a novel semantic segmentation method designed to address
lighting challenges in nighttime environments, offering precise semantic
information distinction in low-light conditions with minimal additional
parameters.

  * •

We improve nighttime semantic segmentation by transferring knowledge between
the Cityscape dataset and Dark Zurich dataset, enhancing object segmentation
in low-light situations by effectively transferring knowledge between domains.

  * •

We experimented with RHRSegNet without domain adaptation on NightCity,
achieving high performance.

The rest of the paper is structured as follows. Section $2$ introduces the
related work. Section $3$ presents the proposed research methodology. The
datasets used and experimental results are explained in Sections $4$ and $5$,
respectively.

##  II Related Work

###  II-A Nighttime Semantic Segmentation

Semantic segmentation at night has seen advancements through various methods.
[5] introduced the concept of using an intermediate twilight domain to
gradually transform semantic models trained in daylight scenarios to evening
situations. This approach was expanded upon by [14, 15], who developed a
guided curriculum adaptation framework leveraging the cross-time-of-day
relationship in scene photographs, employing both stylized synthetic images
and unlabeled actual images. However, such progressive adaptation methods
often necessitate training multiple semantic segmentation models for different
domains, as seen in [14]. This approach can be resource-intensive and
wasteful. Subsequent research [13, 16, 12] has explored the use of additional
image transfer models, such as CycleGAN [25], for day-to-night or night-to-day
image translation prior to training semantic segmentation models. The
effectiveness of these techniques heavily relies on the performance of the
pre-trained image transfer model. Recognizing the resilience of thermal
radiation to changes in light, Vertens et al. [19] proposed the incorporation
of thermal infrared images alongside RGB images for nighttime semantic
segmentation. Additionally, domain adaptation techniques, as demonstrated in
[7], have been employed for semantic segmentation of night scenes. NightLab
[6] categorizes items as simple or complex. A Hardness Detection Module
identifies difficult categories and sends them to a segmentation module. [22]
suggest employing image frequency distributions for nighttime scene analysis.
However, these methods do not estimate the impact of lighting on semantics.

###  II-B Semantic Segmentation

Semantic segmentation aims to categorize each pixel individually. Recently,
methods based on Fully Convolutional Networks (FCN) [11] paired with encoder-
decoder architectures have dominated this field. Various techniques [1, 2, 23]
utilize dilated convolutions to expand the receptive field, while PSPNet [24]
employs a pyramid pooling module (PPM) to capture multi-scale contexts.
Integrating these advancements, the DeepLab series [1, 2, 3, 4] introduces
atrous spatial pyramid pooling (ASPP) to incorporate contextual information.
More recently, self-attention mechanisms have been extensively used to capture
long-range dependencies in semantic segmentation. Additionally, several
transformer-based networks, including Vision Transformer and Swin Transformer,
have been used to provide stronger backbones. Moreover, ConvNeXt [10] has
emerged as a competitive alternative to transformers. However, the majority of
these methods are primarily focused on daytime scenes.

##  III Research Methodology

###  III-A Relighting Model

Figure 1: Relighting Model

The relighting model simulates lighting changes using a shared-weight
architecture, allowing for a robust and unified approach. The relighting model
takes an input image, passes it through four convolutional layers, three
residual blocks, and two transposed convolutional layers. Each layer is
followed by a batch normalization layer. The relighted image is created by
combining the output of the last layer with the input image. The resulting
relighted image is then passed to the HRNet.

$I_{\text{e}}=\text{BN1}(\text{TransConv2D}(\text{BN2}(\text{Conv2D}(I)))+I)$
(1)

In this simplified equation: $I_{\text{e}}$ represents the enhanced image.
Conv1 and Conv2 are convolutional layers.
BN1 and BN2 are batch normalization layers.
$+$ denotes the skip connection, where $I$ is added to the output of the first
convolutional layer before being processed by the second convolutional layer
and batch normalization, as shown in Figure 1.

###  III-B Learning Parameter Sharing

This research utilizes shared weights in the relighting network to optimize
learning parameter utilization, improve computational and memory efficiency,
generate transferable insights, and ensure consistent feature extraction. Let
$W$ represent the shared weights within the relighting network. Let $f(x)$
represent the function of the relighting network, where $x$ is the input
image. Then, the output of the relighting network can be represented as:

$\text{Output}=f(x;W)$ (2)

Here, $f(x;W)$ denotes the function $f$ parameterized by the shared weights
$W$, which generates the relighted output given the input image $x$. The
equation explains how shared weights are used in a relighting network to adapt
to different lighting conditions and input domains, enhancing computation,
memory utilization, and generalization capabilities. This approach improves
knowledge transfer across datasets and generalization capabilities,
outperforming traditional methods in computational efficiency and result
quality. It also optimizes model training and inference processes, allowing
the network to quickly adjust to new lighting conditions.

###  III-C Semantic Segmentation Network

Figure 2: Our HRNet Architecture

High-resolution representations are crucial for high-resolution problems like
semantic segmentation, human pose estimation, and object detection. The High-
Resolution Network (HRNet) maintains these representations by connecting high-
to-low resolution convolution streams in parallel and repeatedly exchanging
information across resolutions. The HRNet architecture is divided into many
phases, each of which aims to incrementally improve and aggregate multi-scale
characteristics for accurate semantic segmentation. Our model consists of a
series of fundamental blocks, starting with an input layer, followed by
convolutional layers, Batch Normalization, ReLU activation functions, residual
connections, and an output layer. The model uses a hierarchical processing
pipeline, which includes downsampling, convolutional operations, Batch
Normalization, ReLU activation functions, and an output layer for model
predictions. This model takes the relighted image and processes the input
features at the original resolution, setting the model at the first stage
(STAGE1). Then, by adding more branches and blocks, the subsequent stages
(STAGE2, STAGE3, STAGE4) increase the network’s capacity and allow it to
capture features at various resolutions. The transition layer is used to
bridge feature maps of different resolutions between the adjacent stages of
the network. Each phase consists of high-resolution modules that combine
feature maps from many branches using techniques such as interpolation and
summation to provide a comprehensive representation.

$\text{Output}=\text{Concatenation}(F1,F2,F3,F4)$ (3)

where:

  * •

$F1$ represents the feature map extracted from stage 1

  * •

$F2$ represents the feature map extracted from stage 2

  * •

$F3$ represents the feature map extracted from stage 3

  * •

$F4$ represents the feature map extracted from stage 4

The output from each stage from the 4 stages are processed through two
$1\times 1$ convolutions, followed by batch normalization and ReLU activation,
and finally producing the output with 19 channels, as shown in Figure 2.

###  III-D Data Augmentation

Image transformations are crucial for data preparation in deep learning. Input
images are converted into tensors and normalized to ensure consistent values,
stability, and effective model training. Our data augmentation process
includes cropping, resizing, and flipping to enhance dataset diversity and
improve model generalization. The dataset’s segmentation masks are transformed
into tensor representations.The transformations are applied to the incoming
data without issue, preparing it for further analysis and model training. This
process ensures the model’s success across various contexts.

##  IV Datasets

###  IV-A Night-city

Night City [17, 6] is the largest available nighttime semantic segmentation
dataset. It comprises $2,998$ images at a resolution of $1024\times 512$ for
training and $1,299$ images for validation. Each image comes with pixel-level
annotations. However, there are noticeable annotation errors, such as missing
labels and incorrectly labeled areas, which reduce the dataset’s
effectiveness. Additionally, [21] introduced NightCity-fine, an improved
dataset derived from Night City for nighttime semantic segmentation. In this
dataset, unreasonable annotations have been systematically corrected in both
the training and validation sets.

###  IV-B Dark-Zurich

The Dark-Zurich dataset, a popular benchmark in computer vision and robotics
research, is a collection of high-resolution images, primarily used for object
detection and semantic segmentation tasks. The dataset features high-quality
images with high spatial resolution, enabling detailed examination of urban
environments. It includes a diverse range of urban scenes such as roads,
crosswalks, buildings, green spaces, and other infrastructure. Additionally,
many images are manually annotated with pixel-level labels, providing crucial
ground truth annotations for semantic segmentation tasks. The dataset is well-
suited for testing, comprising $8,377$ images for training and $100$ images
for validation, evenly divided into $50$ night and $50$ day images. The test
set includes 302 images, split into subsets for nighttime and daytime scenes,
respectively.

###  IV-C Cityscape

The Cityscapes dataset is a comprehensive resource for urban scene
understanding, featuring $5,000$ high-resolution frames captured across
diverse street scenes. It includes pixel-level annotations across 19 semantic
categories, such as cars, pedestrians, roads, traffic signs, and buildings.
The dataset’s landscape orientation ensures consistency and smooth integration
into computer vision pipelines. With a resolution of $2,048\times 1,024$
pixels, the images provide sufficient detail for accurate semantic
segmentation and scene understanding tasks. Divided into three subsets, the
dataset offers sample data for model training, validation, and testing, with
$2,975$ images allocated for training, $500$ images for validation, and
$1,525$ images for testing.

###  IV-D Experimental Design

We initiated our training by utilizing domain adaptation techniques on the
Cityscapes and Dark Zurich datasets. Domain adaptation methods were employed
to enhance the model’s performance on Dark Zurich images. Specifically, we
utilized techniques such as adversarial training to align the feature
distributions between the two domains, using the SGD optimizer. By adapting
the model trained on Cityscapes to better generalize to Dark Zurich, our goal
was to minimize the domain shift and improve the model’s robustness in low-
light conditions. The results are shown in Table I. Additionally, we
experimented with RHRSegnet on the NightCity-Fine dataset for training and
obtained extremely good performance metrics without using domain adaptation
approaches. Despite the lack of domain adaptation, the model showed
proficiency in correctly classifying objects in night settings. This
achievement demonstrates the adaptability and flexibility of RHRSegnet to
changing environmental factors, especially low light levels, without requiring
further domain-specific changes. The remarkable outcomes suggest that
RHRSegnet has the ability to generalize effectively over a wide range of
datasets, highlighting its potential for practical use in tasks involving the
analysis and segmentation of night scenes. Results evaluated on the Cityscapes
dataset are shown in Table II.

###  IV-E Results

The benchmark results presented in Table I offer a comparison of different
segmentation models based on their mean intersection over union (mIOU)
performance in the context of Cityscapes $\rightarrow$ Dark Zurich adaptation,
evaluated on the Dark Zurich validation set. The first model, AdaptSegNet,
employs the Deeplab architecture and achieves a modest mIOU of $20.2$. The
next two models, GCMA and MGCDA, utilize the RefineNet architecture, yielding
mIOUs of $26.7$ and $26.1$, respectively, showcasing a notable improvement
over AdaptSegNet. Notably, our model, RHRSegNet, stands out with the highest
mIOU of $27.19$, leveraging the HRNet architecture. This performance
underscores the effectiveness of our model in handling domain adaptation
challenges, particularly in challenging low-light conditions as represented in
the Dark Zurich dataset. The results clearly highlight the superior
performance of RHRSegNet, suggesting that our chosen architecture and model
optimizations effectively enhance segmentation accuracy, outperforming the
other competitive models in this challenging task.

Method | Architecture | mIOU
---|---|---
AdaptSegNet [18] | Deeplab | 20.2
GCMA [14] | RefineNet | 26.7
MGCDA [15] | RefineNet | 26.1
RHRSegNet (Ours) | HRNet | 27.19
TABLE I: Comparison by mIOU metric using Cityscapes $\rightarrow$ Dark Zurich
adaptation evaluated on Dark Zurich validation between our model RHRSegNet and
other models

The benchmark results in Table II showcase a comparison of various
segmentation models based on their mean intersection over union (mIoU)
performance using the Cityscapes dataset for evaluation. RefineNet, an
advanced segmentation network, achieves a respectable mIoU of $28.5$.
DeepLab-v2 and PSPNet, both well-known models in the domain, slightly
outperform RefineNet, each with an mIoU of $28.8$. However, our model,
RHRSegNet, demonstrates a substantial improvement, achieving an impressive
mIoU of $37.53$. This result highlights the effectiveness of RHRSegNet in
segmenting complex urban scenes, significantly outperforming other models. The
remarkable performance of RHRSegNet underscores its robust architecture and
superior feature extraction capabilities, making it highly effective for
semantic segmentation tasks, especially within urban environments as
represented in the Cityscapes dataset.

Method | mIoU
---|---
RefineNet [9] | 28.5
DeepLab-v2 [2] | 28.8
PSPNet [24] | 28.8
RHRSegNet | 37.53
TABLE II: Comparison by mIoU metric using Cityscapes for evaluation

Method |  Road |  Sidewalk |  Building |  Wall |  Fence |  Pole |  Traffic Light |  Traffic Sign |  Vegetation |  Terrain |  Sky |  Person |  Rider |  Car |  Truck |  Bus |  Train |  Motorcycle |  Bicycle | mIoU
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---
RefineNet [9] | 68.8 | 23.2 | 46.8 | 20.8 | 12.6 | 29.8 | 30.4 | 26.9 | 43.1 | 14.3 | 0.3 | 36.9 | 49.7 | 63.6 | 6.8 | 0.2 | 24.0 | 33.6 | 9.3 | 28.5
DeepLab-v2 [2] | 79.0 | 21.8 | 53.0 | 13.3 | 11.2 | 22.5 | 20.2 | 22.1 | 43.5 | 10.4 | 18.0 | 37.4 | 33.8 | 64.1 | 6.4 | 0.0 | 52.3 | 30.4 | 7.4 | 28.8
PSPNet [24] | 78.2 | 19.0 | 51.2 | 15.5 | 10.6 | 30.3 | 28.9 | 22.0 | 56.7 | 13.3 | 20.8 | 38.2 | 21.8 | 52.1 | 1.6 | 0.0 | 53.2 | 23.2 | 10.7 | 28.8
AdaptSegNet [18] | 86.1 | 44.2 | 55.1 | 22.2 | 4.8 | 21.1 | 5.6 | 16.7 | 37.2 | 8.4 | 1.2 | 35.9 | 26.7 | 68.2 | 45.1 | 0.0 | 50.1 | 33.9 | 15.6 | 30.4
ADVENT [20] | 85.8 | 37.9 | 55.5 | 27.7 | 14.5 | 23.1 | 14.0 | 21.1 | 32.1 | 8.7 | 2.0 | 39.9 | 16.6 | 64.0 | 13.8 | 0.0 | 58.8 | 28.5 | 20.7 | 29.7
BDL [9] | 85.3 | 41.1 | 61.9 | 32.7 | 17.4 | 20.6 | 11.4 | 21.3 | 29.4 | 8.9 | 1.1 | 37.4 | 22.1 | 63.2 | 28.2 | 0.0 | 47.7 | 39.4 | 15.7 | 30.8
DMAda [8] | 75.5 | 29.1 | 48.6 | 21.3 | 14.3 | 34.3 | 36.8 | 29.9 | 49.4 | 13.8 | 0.4 | 43.3 | 50.2 | 69.4 | 18.4 | 0.0 | 27.6 | 34.9 | 11.9 | 32.1
RHRSegNet-Cityscapes (Ours) | 92.59 | 58.56 | 78.65 | 5.83 | 10.11 | 30.48 | 16.33 | 32.45 | 78.97 | 30.35 | 80.25 | 52.98 | 14.57 | 80.77 | 0.46 | 0.02 | 0.02 | 0.11 | 49.52 | 37.53
RHRSegNet-NightCity-Fine (Ours) | 87.25 | 37.63 | 77.84 | 23.79 | 32.72 | 23.58 | 9.87 | 28.06 | 49.62 | 14.63 | 82.82 | 29.76 | 0.01 | 70.84 | 20.65 | 24.55 | 0.0 | 0.0 | 20.01 | 33.35

TABLE III: Comparison by 19 Classes and mIoU

The benchmark results presented in Table III provide a comprehensive
comparison of segmentation models across various categories based on their
mean Intersection over Union (mIoU) performance using the Cityscapes and Dark
Zurich datasets. Notably, the models evaluated include RefineNet, DeepLab-v2,
PSPNet, AdaptSegNet, ADVENT, BDL, DMAda, and our proposed RHRSegNet with two
variations: RHRSegNet-Cityscapes and RHRSegNet-NightCity-Fine. In terms of
overall performance, RHRSegNet-Cityscapes clearly outperforms the other models
with a remarkable mIoU of $37.53$, showcasing exceptional segmentation
accuracy, particularly in key categories like Road, Building, Sky, Car, and
Bus. This reflects the robust architecture and superior feature extraction
capabilities of RHRSegNet. The second variation, RHRSegNet-NightCity-Fine,
also performs competitively with an mIoU of $33.35$, highlighting its
effectiveness in challenging low-light conditions. Among the competing models,
DMAda demonstrates strong performance with an mIoU of $32.1$, particularly
excelling in categories like Rider and Car. Meanwhile, BDL achieves an mIoU of
$30.8$, showing solid results across several categories. The other models,
including RefineNet, DeepLab-v2, PSPNet, AdaptSegNet, and ADVENT, achieve
mIoUs below $30$, indicating that they struggle more with the segmentation
tasks, particularly in challenging urban and nighttime environments. Overall,
the results highlight the superior performance of RHRSegNet, particularly in
complex and challenging conditions, reaffirming its robust design and superior
segmentation capabilities across a wide range of urban scene categories.

Figure 3: Original Image

Figure 4: Ground Truth

Figure 5: Our RHRSegNet

##  V Conclusion

The paper presents a novel model, RHRSegNet, for nighttime semantic
segmentation using deep learning techniques and low-light-adapted algorithms.
The model evenly distributes light, simulates changes in lighting conditions
to improve brightness and contrast, and separates different factors in an
image, such as lighting conditions and object colors. It also distinguishes
between different features in an image, thereby improving image quality and
processing images with multiple variables. The model is tested using the
Night-City, Cityscape, and Dark-Zurich datasets, demonstrating its potential
in handling complex lighting conditions and recognizing semantics even in
challenging scenarios. This approach sets a stronger standard for evaluating
segmentation throughout the night, enhancing the quality of computer vision
applications like autonomous driving.

## References

  * [1] Liang-Chieh Chen, George Papandreou, Iasonas Kokkinos, Kevin Murphy, and Alan L Yuille.  Semantic image segmentation with deep convolutional nets and fully connected crfs.  arXiv preprint arXiv:1412.7062, 2014.
  * [2] Liang-Chieh Chen, George Papandreou, Iasonas Kokkinos, Kevin Murphy, and Alan L Yuille.  Deeplab: Semantic image segmentation with deep convolutional nets, atrous convolution, and fully connected crfs.  IEEE transactions on pattern analysis and machine intelligence, 40(4):834–848, 2017.
  * [3] Liang-Chieh Chen, George Papandreou, Florian Schroff, and Hartwig Adam.  Rethinking atrous convolution for semantic image segmentation.  arXiv preprint arXiv:1706.05587, 2017.
  * [4] Liang-Chieh Chen, Yukun Zhu, George Papandreou, Florian Schroff, and Hartwig Adam.  Encoder-decoder with atrous separable convolution for semantic image segmentation.  In Proceedings of the European conference on computer vision (ECCV), pages 801–818, 2018.
  * [5] Dengxin Dai and Luc Van Gool.  Dark model adaptation: Semantic image segmentation from daytime to nighttime.  In 2018 21st International Conference on Intelligent Transportation Systems (ITSC), pages 3819–3824. IEEE, 2018.
  * [6] Xueqing Deng, Peng Wang, Xiaochen Lian, and Shawn Newsam.  Nightlab: A dual-level architecture with hardness detection for segmentation at night.  In Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition, pages 16938–16948, 2022.
  * [7] Shuai Di, Qi Feng, Chun-Guang Li, Mei Zhang, Honggang Zhang, Semir Elezovikj, Chiu C Tan, and Haibin Ling.  Rainy night scene understanding with near scene semantic adaptation.  IEEE Transactions on Intelligent Transportation Systems, 22(3):1594–1602, 2020.
  * [8] Hsin-Ying Lee, Hung-Yu Tseng, Jia-Bin Huang, Maneesh Singh, and Ming-Hsuan Yang.  Diverse image-to-image translation via disentangled representations.  In Proceedings of the European conference on computer vision (ECCV), pages 35–51, 2018.
  * [9] Yunsheng Li, Lu Yuan, and Nuno Vasconcelos.  Bidirectional learning for domain adaptation of semantic segmentation.  In Proceedings of the IEEE/CVF conference on computer vision and pattern recognition, pages 6936–6945, 2019.
  * [10] Zhuang Liu, Hanzi Mao, Chao-Yuan Wu, Christoph Feichtenhofer, Trevor Darrell, and Saining Xie.  A convnet for the 2020s.  In Proceedings of the IEEE/CVF conference on computer vision and pattern recognition, pages 11976–11986, 2022.
  * [11] Jonathan Long, Evan Shelhamer, and Trevor Darrell.  Fully convolutional networks for semantic segmentation.  In Proceedings of the IEEE conference on computer vision and pattern recognition, pages 3431–3440, 2015.
  * [12] Sauradip Nag, Saptakatha Adak, and Sukhendu Das.  What’s there in the dark.  In 2019 IEEE International Conference on Image Processing (ICIP), pages 2996–3000. IEEE, 2019.
  * [13] Eduardo Romera, Luis M Bergasa, Kailun Yang, Jose M Alvarez, and Rafael Barea.  Bridging the day and night domain gap for semantic segmentation.  In 2019 IEEE Intelligent Vehicles Symposium (IV), pages 1312–1318. IEEE, 2019.
  * [14] Christos Sakaridis, Dengxin Dai, and Luc Van Gool.  Guided curriculum model adaptation and uncertainty-aware evaluation for semantic nighttime image segmentation.  In Proceedings of the IEEE/CVF International Conference on Computer Vision, pages 7374–7383, 2019.
  * [15] Christos Sakaridis, Dengxin Dai, and Luc Van Gool.  Map-guided curriculum domain adaptation and uncertainty-aware evaluation for semantic nighttime image segmentation.  IEEE Transactions on Pattern Analysis and Machine Intelligence, 44(6):3139–3153, 2020.
  * [16] Lei Sun, Kaiwei Wang, Kailun Yang, and Kaite Xiang.  See clearer at night: towards robust nighttime semantic segmentation through day-night image conversion.  In Artificial Intelligence and Machine Learning in Defense Applications, volume 11169, pages 77–89. SPIE, 2019.
  * [17] Xin Tan, Ke Xu, Ying Cao, Yiheng Zhang, Lizhuang Ma, and Rynson WH Lau.  Night-time scene parsing with a large real dataset.  IEEE Transactions on Image Processing, 30:9085–9098, 2021.
  * [18] Yi-Hsuan Tsai, Wei-Chih Hung, Samuel Schulter, Kihyuk Sohn, Ming-Hsuan Yang, and Manmohan Chandraker.  Learning to adapt structured output space for semantic segmentation.  In Proceedings of the IEEE conference on computer vision and pattern recognition, pages 7472–7481, 2018.
  * [19] Johan Vertens, Jannik Zürn, and Wolfram Burgard.  Heatnet: Bridging the day-night domain gap in semantic segmentation with thermal images.  In 2020 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pages 8461–8468. IEEE, 2020.
  * [20] Tuan-Hung Vu, Himalaya Jain, Maxime Bucher, Matthieu Cord, and Patrick Pérez.  Advent: Adversarial entropy minimization for domain adaptation in semantic segmentation.  In Proceedings of the IEEE/CVF conference on computer vision and pattern recognition, pages 2517–2526, 2019.
  * [21] Zhixiang Wei, Lin Chen, Tao Tu, Pengyang Ling, Huaian Chen, and Yi Jin.  Disentangle then parse: Night-time semantic segmentation with illumination disentanglement.  In Proceedings of the IEEE/CVF International Conference on Computer Vision, pages 21593–21603, 2023.
  * [22] Zhifeng Xie, Sen Wang, Ke Xu, Zhizhong Zhang, Xin Tan, Yuan Xie, and Lizhuang Ma.  Boosting night-time scene parsing with learnable frequency.  IEEE Transactions on Image Processing, 2023.
  * [23] Fisher Yu and Vladlen Koltun.  Multi-scale context aggregation by dilated convolutions.  arXiv preprint arXiv:1511.07122, 2015.
  * [24] Hengshuang Zhao, Jianping Shi, Xiaojuan Qi, Xiaogang Wang, and Jiaya Jia.  Pyramid scene parsing network.  In Proceedings of the IEEE conference on computer vision and pattern recognition, pages 2881–2890, 2017.
  * [25] Jun-Yan Zhu, Taesung Park, Phillip Isola, and Alexei A Efros.  Unpaired image-to-image translation using cycle-consistent adversarial networks.  In Proceedings of the IEEE international conference on computer vision, pages 2223–2232, 2017.