# Small-Gain Theorem for Safety Verification of Interconnected Systems

Ziliang Lyu, Xiangru Xu, and Yiguang Hong Z. Lyu (e-mail:
<EMAIL_ADDRESS>and Y. Hong (e-mail<EMAIL_ADDRESS>are with the
Department of Control Science and Engineering, Tongji University, Shanghai,
ChinaX. Xu (e-mail<EMAIL_ADDRESS>is with the Department of Mechanical
Engineering, University of Wisconsin-Madison, Madison, WI, USA.

###### Abstract

A small-gain theorem in the formulation of barrier function is developed in
this work for safety verification of interconnected systems. This result is
helpful to verify input-to-state safety (ISSf) of the overall system from the
safety information encoded in the subsystem’s ISSf-barrier function. Also, it
can be used to obtain a safety set in a higher dimensional space from the
safety sets in two lower dimensional spaces.

###### Index Terms:

Input-to-state safety (ISSf), set invariance, barrier function, interconnected
systems, small-gain theorem.

##  I Introduction

Safety is crucial in the design of control systems, which requires any
trajectories of the control systems initialized in a prescribed safety set to
be kept out of the unsafe region. Applications concerned with safety are
ubiquitous in our daily life, ranging from the cars on the ground to the
aeroplanes in the air. For example, autonomous vehicles are equipped with lane
keeping modules [1], a robot team is designed to avoid the collision between
robots [2], and aircrafts must satisfy the safety requirement during takeoff
and landing [3].

For safety-critical systems, a rigorous verification of safety is the first
step towards other control objectives (e.g., stabilization and regulation). In
general, the techniques for safety verification can be classified into two
sorts: model checking [4] and deductive verification [5]. Compared with the
former one, deductive verification provides a safety certificate by
mathematical inferences rather than exhaustively checking all of the possible
system behaviors. The barrier function gives a promising deductive
verification approach, with a set of Lyapunov-like criterions for safety
verification; e.g., see [6, 7, 8, 9, 10, 11, 12, 13] for more details. In [6],
barrier functions were used to formulate the verification tasks as convex
programming problems. A framework by combining control Lyapunov functions and
barrier functions was proposed in [7] to balance the objective of
stabilization and safety verification. In [8], a novel barrier function,
called the zeroing barrier function, was proposed for establishing safety and
analyzing the robustness of safe sets. Later, [10] redefined a new notion of
input-to-state safety (ISSf) and provided a sufficient condition in the sense
of barrier function to check ISSf, which could be regarded as the counterpart
of Sontag’s input-to-state stability (ISS) [14] for safety verification.
However, it should be mentioned that most of these results were not given for
interconnected systems.

The small gain technique is effective for interconnected systems to keep good
properties, which completes the verification tasks of a large-scale system to
be completed by analyzing its less complicated subsystems. In the stability
analysis, this technique has been investigated [15, 16, 17, 18, 19]. For
example, the Lyapunov-based small-gain theorem developed in [16] has been
found useful to establish ISS for interconnected systems. This result has been
extended to switched systems [17] and hybrid systems [19] in recent years.

Considering that the barrier function provides a Lyapunov-like verification
approach, it is natural to ask a question: whether there exists a small-gain
condition such that one can establish ISSf for the overall system from the
safety information encoded in the subsystem’s ISSf-barrier function. This
question is not trivial. First, the existing small-gain theorems for stability
rely on some nonnegative assumptions, which cannot be met in safety
verification. Therefore, we cannot directly employ the tools developed in [15,
16, 17, 18, 19] to analyze the small-gain condition for safety verification.
Second, the ISS plays important roles on the small-gain conditions, but there
are no small-gain results of ISSf.

The objective of this paper is to develop a small-gain theorem based on
barrier functions for safety verification of interconnected system, in order
to establish a higher dimensional safety set from two lower dimensional safety
sets. Based on the proposed ISSf-barrier function, we prove that, if the
absolute value of the composition of ISSf gains is smaller than that of the
identity function, then the overall system is ISSf. This condition is
different from traditional small-gain conditions for stability.

Notations and Terminologies. Throughout this paper, ‘$\circ$’ denotes the
composition operator, i.e., $f\circ{g}(s)=f(g(s))$; ‘T’ denotes the transpose
operator; $|\cdot|$ denotes the Euclidean norm; $\mathbb{R}$ and
$\mathbb{R}_{\geq 0}$ denote the set of real numbers and nonnegative real
numbers, respectively. For any measurable function $u:\mathbb{R}_{\geq
0}\rightarrow\mathbb{R}^{m}$, $\|u\|=\sup\\{|u(t)|,t\geq 0\\}$. In the
following, we review the comparison functions, whose details can be founded in
[8] and [20]. A continuous function $\gamma$: $\mathbb{R}_{\geq
0}\rightarrow\mathbb{R}_{\geq 0}$ with $\gamma(0)=0$ is of class
$\mathcal{K}$, if it is strictly increasing. Moreover, a class $\mathcal{K}$
function $\gamma$ is of class $\mathcal{K}_{\infty}$ if it is unbounded. A
continuous function $\gamma:\mathbb{R}\rightarrow\mathbb{R}$ with
$\gamma(0)=0$ is of extended class $\mathcal{K}$ if it is strictly increasing.
In particular, an extended class $K$ function $\gamma$ is of extended class
$\mathcal{K}_{\infty}$ if it is unbounded.

##  II Preliminaries

Consider the system

$\displaystyle\dot{x}=f(x,u),\;\;x(t_{0})=x_{0}$ (1)

where $x\in\mathbb{R}^{n}$ is the state, $u\in\mathbb{R}^{m}$ is the external
input, and the vector field
$f:\mathbb{R}^{n}\times\mathbb{R}^{m}\rightarrow\mathbb{R}^{n}$ is locally
Lipschitz continuous with $f(0,0)=0$.

We first review two definitions related to safety.

######  Definition 1 (Forward Robust Invariance [21]).

A set $\mathcal{S}$ is forward robustly invariant if for every
$x_{0}\in\mathcal{S}$, there exists an external input $u$ such that the
solution $x(t)$ to (1) satisfies $x(t)\in\mathcal{S}$ for all $t\geq{t}_{0}$.

######  Definition 2 (Input-to-State Safety [10]).

The system (1) is input-to-state safe (ISSf) on the set

$\displaystyle\mathcal{S}_{\gamma(\|u\|)}=\\{x\in\mathbb{R}^{n}:h(x)+\gamma(\|u\|)\geq
0\\}$ (2)

with respect to the external input $u$, if $\mathcal{S}_{\gamma(\|u\|)}$ is
forward robustly invariant. Herein, $h:\mathbb{R}^{n}\rightarrow\mathbb{R}$ is
a continuously differentiable function, and $\gamma$ is a function of class
$\mathcal{K}_{\infty}$. In particular, we say that system (1) is safe if there
is no external input (i.e., $u=0$), in which case
$S_{\gamma(\|u\|)}=\\{x\in\mathbb{R}^{n}:h(x)\geq 0\\}$.

Because in the proof of our small-gain theorem we need to handle nonsmooth
functions, here we introduce the Dini derivative and corresponding results.

######  Definition 3 (Dini Derivative [22]).

Consider a function $h:\mathbb{R}\rightarrow\mathbb{R}$. The upper and the
lower Dini derivatives of $h$ at $r\in\mathbb{R}$ are, respectively, defined
by

$\displaystyle D^{+}h(r)=\limsup_{s\rightarrow 0^{+}}\frac{h(r+s)-h(r)}{s},$
$\displaystyle D_{+}h(r)=\liminf_{s\rightarrow 0^{+}}\frac{h(r+s)-h(r)}{s}.$

Given a continuous function $h:\mathbb{R}\rightarrow\mathbb{R}$, it is known
that $h$ is not increasing at $r\in\mathbb{R}$ if and only if the Dini
derivative of $h$ at $r$ is nonpositive, and is not decreasing if and only if
the Dini derivative of $h$ at $r$ is nonnegative.

######  Lemma 1.

For $i=1,2$, suppose that $h_{i}:\mathbb{R}^{n_{i}}\rightarrow\mathbb{R}$ is
locally Lipschitz and let $h(x)=\min\\{h_{1}(x_{1}),h_{2}(x_{2})\\}$. Then
$h(x)$ is locally Lipschitz as well, and

$\displaystyle
D_{+}{h}(x)=\dot{h}_{1}(x_{1}),\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\,\text{if
}h_{1}(x_{1})<h_{2}(x_{2});$ $\displaystyle
D_{+}h(x)=\dot{h}_{2}(x_{2}),\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\,\text{if
}h_{1}(x_{1})>h_{2}(x_{2});$ $\displaystyle
D_{+}h(x)=\min\\{\dot{h}_{1}(x_{1}),\dot{h}_{2}(x_{2})\\},\;\;\text{if
}h_{1}(x_{1})=h_{2}(x_{2}).$

Let $f_{i}(x)=-h_{i}(x)$ and $f(x)=-h(x)$. Then Lemma 1 follows directly from
[23, Theorem 2.1] due to $D^{+}f(x)=-D_{+}h(x)$ and
$\max\\{\dot{f}_{1}(x_{1}),\dot{f}_{2}(x_{2})\\}=-\min\\{\dot{h}_{1}(x_{1}),\dot{h}_{2}(x_{2})\\}$.

######  Lemma 2 (Comparison Principle [24]).

Consider

$\displaystyle\dot{x}=f(x),\;\;x(t_{0})=x_{0}$

where $f:\mathbb{R}\rightarrow\mathbb{R}$ is locally Lipschitz. Let
$[t_{0},T)$ be the maximal interval of existence of the solution $x(t)$.
Suppose that $y(t)$ is a continuous function with

$\displaystyle D_{+}y(t)\geq{f}(y(t)),\;\;y(t_{0})\geq{x}_{0}.$ (3)

Then $y(t)\geq{x}(t)$ for all $t\in[t_{0},T)$.

##  III ISSf-Barrier Function

In this section, we present a new notion of ISSf-barrier function, which is
suitable to characterize the ISSf gains of our small-gain condition.

######  Definition 4 (ISSf-Barrier Function).

A continuously differentiable function $h:\mathbb{R}^{n}\rightarrow\mathbb{R}$
is called an ISSf-barrier function for system (1), if there exist functions
$\gamma$ of class $\mathcal{K}$ and $\alpha$ of extended class $\mathcal{K}$
such that for each $u\in\mathbb{R}^{m}$,

$\displaystyle
h(x)\leq-\gamma(|u|)\Rightarrow\nabla{h}(x)f(x,u)\geq-\alpha(h(x)).$ (4)

Herein, $\gamma$ is referred to as the ISSf gain.

Note that [10] has presented another definition of ISSf-barrier functions;
referring to (5) below. The relation between the ISSf-barrier function defined
in (4) and the one of [10] is shown by the following result.

######  Proposition 1.

A continuously differentiable function $h:\mathbb{R}^{n}\rightarrow\mathbb{R}$
is an ISSf-barrier function for system (1) with $\alpha$ of extended class
$\mathcal{K}_{\infty}$ if and only if there exist functions $\chi$ of extended
class $\mathcal{K}_{\infty}$ and $\phi$ of class $\mathcal{K}_{\infty}$ such
that

$\displaystyle\nabla{h}(x)f(x,u)\geq-\chi(h(x))-\phi(|u|).$ (5)

Proof. Select a constant $c\in(0,1)$. Then it follows from (5) that

$\displaystyle
h(x)\leq-\hat{\phi}(|u|)\Rightarrow\nabla{h}(x)f(x,u)\geq-(1-c)\chi(h(x))$

where $\hat{\phi}(r)=-\chi^{-1}(-\phi(r)/c)$. The remainder is to verify that
$\hat{\phi}$ is of class $\mathcal{K}$. To see this, note that
$\hat{\chi}(r)=-\chi^{-1}(-r/c)$ is continuous and strictly increasing on the
interval $[0,\infty)$, which in turn, implies that
$\hat{\phi}(r)=\hat{\chi}\circ\phi(r)$ is of class $\mathcal{K}$.

Then we show that the converse is also true. Assume that (4) holds with some
$\alpha$ of extended class $\mathcal{K}_{\infty}$ and $\gamma$ of class
$\mathcal{K}$. According to (4), we have the following two cases.

Case 1. $h(x)\leq-\gamma(|u|)$. In this case, there exists a function $\phi$
of class $\mathcal{K}_{\infty}$ such that,

$\displaystyle\nabla{h}(x)f(x,u)\geq-\alpha(h(x))\geq-\alpha(h(x))-\phi(|u|).$
(6)

Case 2. $h(x)>-\gamma(|u|)$. Since $\alpha$ is of extended class
$\mathcal{K}_{\infty}$,

$\displaystyle\nabla{h}(x)f(x,u)+\alpha(h(x))$
$\displaystyle\geq\nabla{h}(x)f(x,u)+\alpha(-\gamma(|u|))$
$\displaystyle\geq\inf_{h(x)\geq-\gamma(|u|)}\nabla{h}(x)f(x,u)+\alpha(-\gamma(|u|))$
(7)

Let $\tilde{\phi}(r)=\max\\{0,\hat{\phi}(r)\\}$ with

$\displaystyle\hat{\phi}(r)=-\inf_{h(x)\geq-\gamma(|r|)}\nabla{h}(x)f(x,r)+\alpha(-\gamma(|r|)).$

This implies that $\tilde{\phi}$ is continuous and $\tilde{\phi}(0)=0$
(recalling $f(0,0)=0$). Note that $\tilde{\phi}(r)\geq 0$ for each $r\geq 0$.
By combining this with (7), we can select a class $\mathcal{K}_{\infty}$
function $\phi$ with $\phi(r)\geq\tilde{\phi}(r)$ for all ${r}\geq 0$ such
that

$\displaystyle\nabla{h}(x)f(x,u)+\alpha(h(x))\geq-\phi(|u|).$

By combining the two cases above, we conclude that the converse is true as
well. $\Box$

Then we are ready to present the main result of this section, which can be
used as a tool to establish ISSf.

######  Theorem 1.

Consider the system (1) and the set $\mathcal{S}_{\gamma(\|u\|)}$ defined in
(2). Suppose that $h:\mathbb{R}^{n}\rightarrow\mathbb{R}$ is an ISSf-barrier
function satisfying (4). Then,

(i) $\mathcal{S}_{\gamma(\|u\|)}$ is forward robustly invariant, and system
(1) is ISSf on $\mathcal{S}_{\gamma(\|u\|)}$;

(ii) the safety set $\mathcal{S}_{\gamma(\|u\|)}$ is ISS.

Proof. We show the conclusion of (i) by contradiction. If this is not true,
then there exist some $t\geq{t_{0}}$ and some $\epsilon>0$ such that
$h(x(t))<-\gamma(\|u\|)-\epsilon$. Let
$\tau=\inf\\{t\geq{t_{0}}:h(x(t))\leq-\gamma(\|u\|)-\epsilon\\}$. Therefore,
$h(x(\tau))\leq-\gamma(\|u\|)\leq-\gamma(|u(\tau)|)$, which in turn, implies
that

$\displaystyle\dfrac{\text{d}}{\text{d}t}\bigg{|}_{t=\tau}h(x(t))$
$\displaystyle=\nabla{h}(x(\tau))f(x(\tau),u(\tau))$
$\displaystyle\geq-\alpha(h(x(\tau)))>0.$ (8)

Thus, $h(x(t))\leq{h}(x(\tau))$ for some $t$ in $(t_{0},\tau)$. This
contradicts the minimality of $\tau$ and consequently,
$x(t)\in\mathcal{S}_{\gamma(\|u\|)}$ for all $t\geq{t_{0}}$.

Then we consider (ii). Construct a Lyapunov-like function as in [8]:

$\displaystyle V(x)=\left\\{\begin{array}[]{ll}0,&\text{if
}x\in\mathcal{S}_{\gamma(\|u\|)}\\\ -h(x),&\text{if
}x\in\mathbb{R}^{n}\setminus\mathcal{S}_{\gamma(\|u\|)}\end{array}\right.$
(11)

With (4), we have

$\displaystyle
V(x)\geq\gamma(|u|)\Rightarrow\nabla{V}(x)f(x,u)\leq\alpha(-V(x)),\;\;\forall{x}\in\mathbb{R}^{n}\setminus\mathcal{S}_{\gamma(\|u\|)}.$

Moreover, with [14, Lemma 2.14] and [8, Proposition 4], we conclude that the
set $\mathcal{S}_{\gamma(\|u\|)}$ is ISS. $\Box$

##  IV Small-Gain Theorem for Safety Verification

Consider the interconnected system

$\displaystyle\dot{x}_{1}=f_{1}(x_{1},x_{2},u_{1})$ (12a)
$\displaystyle\dot{x}_{2}=f_{2}(x_{1},x_{2},u_{2})$ (12b)

where, for $i=1,2$, $x_{i}\in\mathbb{R}^{n_{i}}$, $u_{i}\in\mathbb{R}^{m_{i}}$
and
$f_{i}:\mathbb{R}^{n_{1}}\times\mathbb{R}^{n_{2}}\times\mathbb{R}^{m_{i}}\rightarrow\mathbb{R}^{n_{i}}$
is locally Lipschitz. Let $x=(x_{1}^{\text{T}},x_{2}^{\text{T}})^{\text{T}}$,
$u=(u_{1}^{\text{T}},u_{2}^{\text{T}})^{\text{T}}$ and
$f(x,u)=(f_{1}(x_{1},x_{2},u_{1})^{\text{T}},f_{2}(x_{1},x_{2},u_{2})^{\text{T}})^{\text{T}}$

The small-gain theorem for safety verification of the interconnected system
(12) is summarized as follows.

######  Theorem 2.

Consider the interconnected system given in (12). Assume that there exist
functions $\alpha_{i}$ of extended class $\mathcal{K}$, $\phi_{i}$ of extended
class $\mathcal{K}_{\infty}$ and $\gamma_{i}$ of class $\mathcal{K}$ such that

$\displaystyle
h_{1}(x_{1})\leq-\max\\{\phi_{1}(|h_{2}(x_{2})|),\gamma_{1}(|u_{1}|)\\}$
$\displaystyle\;\;\;\;\;\;\;\;\;\Rightarrow\nabla{h}_{1}(x_{1})f_{1}(x_{1},x_{2},u_{1})\geq-\alpha_{1}(h_{1}(x_{1})),$
(13) $\displaystyle
h_{2}(x_{2})\leq-\max\\{\phi_{2}(|h_{1}(x_{1})|),\gamma_{2}(|u_{2}|)\\}$
$\displaystyle\;\;\;\;\;\;\;\;\;\Rightarrow\nabla{h}_{2}({x}_{2})f_{2}(x_{1},x_{2},u_{2})\geq-\alpha_{2}(h_{2}(x_{2})).$
(14)

Then there exist an ISS-barrier function
$h:\mathbb{R}^{n_{1}}\times\mathbb{R}^{n_{2}}\rightarrow\mathbb{R}$, which is
dependent on $h_{1}$ and $h_{2}$, and a class $\mathcal{K}_{\infty}$ function
$\gamma:\mathbb{R}_{\geq 0}\rightarrow\mathbb{R}_{\geq 0}$, which is dependent
on $\gamma_{1}$ and $\gamma_{2}$, such that the interconnected system (12) is
ISSf on the set

$\displaystyle\mathcal{S}_{\gamma(\|u\|)}=\\{x\in\mathbb{R}^{n}:h(x)+\gamma(\|u\|)\geq
0\\}$ (15)

with respect to the external input $u$, if

$\displaystyle\left\\{\begin{array}[]{ll}\phi_{1}\circ\phi_{2}(r)>r,&\forall{r}<0;\\\
\phi_{1}\circ\phi_{2}(r)<r,&\forall{r}>0.\end{array}\right.$ (18)

######  Remark 1.

Clearly, $h_{i}(x_{i})$ is an ISSf-barrier function for $x_{i}$-subsystem.
According to Theorem 1, the barrier-type conditions given in (13) and (14)
imply that the sets

$\displaystyle\mathcal{S}_{1}=\big{\\{}x_{1}:h_{1}(x_{1})+\max\\{\phi_{1}(\|h_{2}(x_{2})\|),\gamma_{1}(\|u_{1}\|)\\}\geq
0\big{\\}},$
$\displaystyle\mathcal{S}_{2}=\big{\\{}x_{2}:h_{2}(x_{2})+\max\\{\phi_{2}(\|h_{1}(x_{1})\|),\gamma_{2}(\|u_{2}\|)\\}\geq
0\big{\\}}$

are forward robustly invariant. Intuitively, Theorem 2 can be regarded as a
tool to establish a robustly invariant set $\mathcal{S}_{\gamma(\|u\|)}$ in a
higher dimensional space from the robustly invariant sets $\mathcal{S}_{1}$
and $\mathcal{S}_{2}$ in lower dimensional spaces. This tool is particularly
useful for safety verification of large scale systems, since it allows the
safety verification to be completed by analyzing its less complicated
subsystems rather than analyzing the overall complex system.

The small-gain condition (18) is different from the traditional small-gain
condition of [15], whose analysis tools cannot be directly employed in our
result. To prove Theorem 2, we first introduce two lemmas, which are extended
from those given in [15, Appendix].

######  Lemma 3.

Let $\rho_{0}:\mathbb{R}\rightarrow\mathbb{R}$ be a continuous function with
$\rho_{0}(r)<0$ for all $r<0$ and $\rho_{0}(r)>0$ for all $r>0$. Then there
exists a continuous function $\rho:\mathbb{R}\rightarrow\mathbb{R}$ such that

  * •

$\rho_{0}(r)<\rho(r)<0$ for all $r<0$, and $0<\rho(r)<\rho_{0}(r)$ for all
$r>0$;

  * •

$\rho$ is continuously differentiable on $\mathbb{R}$, and
$\rho^{\prime}(r)<\frac{1}{2}$ for all $r\in\mathbb{R}$.

Proof. See Appendix. $\Box$

######  Lemma 4.

Let $\phi_{i}$ be of extended class $\mathcal{K}_{\infty}$ and satisfy (18).
Then there exists an extended class $\mathcal{K}_{\infty}$ function $\phi$
such that

  * •

$\phi_{1}^{-1}(r)<\phi(r)<\phi_{2}(r)$ for all $r<0$, and
$\phi_{2}(r)<\phi(r)<\phi_{1}^{-1}(r)$ for all $r>0$;

  * •

$\phi(r)$ is continuously differentiable on $\mathbb{R}\backslash 0$, and
$\phi^{\prime}(r)>0$ for all $r\in\mathbb{R}\backslash 0$.

Proof. See Appendix. $\Box$

Then it is time to prove Theorem 2.

Proof of Theorem 2. By applying Lemma 4 to $\phi_{1}$ and $\phi_{2}$, one can
select an extended class $\mathcal{K}_{\infty}$ function $\phi$, which is
continuously differentiable on $\mathbb{R}\backslash 0$, such that

$\displaystyle\phi_{1}^{-1}(r)<\phi(r)<\phi_{2}(r),\;\;\forall r<0;$ (19a)
$\displaystyle\phi_{2}(r)<\phi(r)<\phi_{1}^{-1}(r),\;\;\forall r>0.$ (19b)

Define a function

$\displaystyle h(x)=\min\\{\phi(h_{1}(x_{1})),h_{2}(x_{2})\\}.$ (20)

Let

$\displaystyle\mathcal{S}_{\phi_{1}(\|h_{2}\|)}=\\{x_{1}:h_{1}(x_{1})+\phi_{1}(\|h_{2}\|)\geq
0\\},$
$\displaystyle\mathcal{S}_{\gamma_{1}(\|u_{1}\|)}=\\{x_{1}:h_{1}(x_{1})+\gamma_{1}(\|u_{1}\|)\geq
0\\},$
$\displaystyle\mathcal{S}_{\phi_{2}(\|h_{1}\|)}=\\{x_{2}:h_{2}(x_{2})+\phi_{2}(\|h_{1}\|)\geq
0\\},$
$\displaystyle\mathcal{S}_{\gamma_{2}(\|u_{2}\|)}=\\{x_{2}:h_{2}(x_{2})+\gamma_{2}(\|u_{2}\|)\geq
0\\}.$

Clearly,
$\mathcal{S}_{1}=\mathcal{S}_{\phi_{1}(\|h_{2}\|)}\cup\mathcal{S}_{\gamma_{1}(\|u_{1}\|)}$
and
$\mathcal{S}_{2}=\mathcal{S}_{\phi_{2}(\|h_{1}\|)}\cup\mathcal{S}_{\gamma_{2}(\|u_{2}\|)}$.

For every
$(x_{1},x_{2})\in\partial\mathcal{S}_{\phi_{1}(\|h_{2}\|)}\times\partial\mathcal{S}_{\phi_{2}(\|h_{1}\|)}$,
we have the following three cases.

Case 1. $\phi(h_{1}(x_{1}))<h_{2}(x_{2})$. Note that $h_{i}(x_{i})\leq 0$ when
$(x_{1},x_{2})\in\partial\mathcal{S}_{\phi_{1}(\|h_{2}\|)}\times\partial\mathcal{S}_{\phi_{2}(\|h_{1}\|)}$.
According to (19),

$\displaystyle\phi_{1}^{-1}(h_{1}(x_{1}))<\phi(h_{1}(x_{1}))<h_{2}(x_{2})$

and hence, it follows immediately from (13) that

$\displaystyle D_{+}{h}(x)$
$\displaystyle=\phi^{\prime}(h_{1}(x_{1}))\nabla{h}_{1}(x_{1})f_{1}(x_{1},x_{2},u_{1})$
$\displaystyle\geq-\phi^{\prime}(h_{1}(x_{1}))\alpha_{1}(h_{1}(x_{1}))$ (21)

when $h(x)\leq-\hat{\gamma}_{1}(|u|)$ with
$\hat{\gamma}_{1}(r)=-\phi(-\gamma_{1}(r))$. The derivation of (21) has
employed the fact that $\phi^{\prime}(h_{1}(x_{1}))>0$.

Case 2. $\phi(h_{1}(x_{1}))>h_{2}(x_{2})$. According to (19),

$\displaystyle h_{2}(x_{2})<\phi(h_{1}(x_{1}))<\phi_{1}(h_{1}(x_{1}))$

which implies

$\displaystyle
D_{+}{h}(x)=\nabla{h}_{2}(x_{2})f_{2}(x_{1},x_{2},u_{2})\geq-\alpha_{2}(h_{2}(x_{2}))$
(22)

when $h(x)\leq-\gamma_{2}(|u_{2}|)$.

Case 3. $\phi(h_{1}(x_{1}))=h_{2}(x_{2})$. With Lemma 1, it follows from (21)
and (22) that

$\displaystyle
D_{+}{h}(x)\geq-\max\\{\phi^{\prime}(h_{1}(x_{1}))\alpha_{1}(h_{1}(x_{1})),\alpha_{2}(h_{2}(x_{2}))\\}$
(23)

when $h(x)\leq-\gamma(|u|)$ with
$\gamma(r)=\hat{\gamma}_{1}(r)+\gamma_{2}(r)$.

Let $\alpha(r):=\max\\{\phi^{\prime}(r)\alpha_{1}(r),\alpha_{2}(r)\\}$. Since
$\phi^{\prime}(r)>0$ for each $r\in\mathbb{R}$, $\alpha$ is an extended class
$\mathcal{K}_{\infty}$ function. By summarizing the three cases above, we have

$\displaystyle h(x)\leq-\gamma(|u|){\Rightarrow}D_{+}{h}(x)\geq-\alpha(h(x)).$
(24)

Without loss of generality, we can assume that $\alpha$ is smooth. In the
following, we use the smoothing technique given in [25, Remark 4.1] to show
that such an assumption is always possible.

Pick an extended class $\mathcal{K}_{\infty}$ function $\tilde{\alpha}$, which
is smooth on $\mathbb{R}$, such that

$\displaystyle\tilde{\alpha}(s)\geq-{s}\alpha(s),\;\;\forall{s}\in[-1,0);$
$\displaystyle\tilde{\alpha}(s)\leq{s}\alpha(s),\;\;\;\;\,\forall{s}\in(0,1].$

This is possible since $\alpha(r)$ is positive definite when $r>0$ and
negative definite when $r<0$. Then let $\eta:\mathbb{R}\rightarrow\mathbb{R}$
be an extended class $\mathcal{K}_{\infty}$ function, which is smooth in
$\mathbb{R}$, such that

  * •

$\eta(r)\leq{r}$ for all $r\in[-1,0)$;

  * •

$\eta(r)<-\tilde{\alpha}(r)/\alpha(r)$ for all $r<-1$.

Define

$\displaystyle\beta(r)=\left\\{\begin{array}[]{ll}\int_{0}^{s}\eta(s),&\forall{r}\geq
0;\\\ \int_{s}^{0}\eta(s),&\forall{r}<0.\end{array}\right.$ (27)

Note that $\beta$ is of extended class $\mathcal{K}_{\infty}$. Let
$W(h(x))=\beta(h(x))$ and then,

$\displaystyle
D_{+}W(h(x))=\beta^{\prime}(h(x))D_{+}h(x)\geq\eta(h(x))\alpha(h(x))$ (28)

when $h(x)\leq-\gamma(|u|)$. In the following, we show that $D_{+}W(h(x))$ is
lower bounded by $-\tilde{\alpha}(h(x))$. Since $h(x)\leq-\gamma(|u|)\leq 0$,
we have the following two cases.

$\bullet$ If $h(x)\in[-1,0]$,

$\displaystyle\eta(h(x))\leq{h}(x)\leq-\frac{\tilde{\alpha}(h(x))}{\alpha(h(x))}.$
(29)

$\bullet$ If $h(x)\in(-\infty,-1)$, with the definition of $\eta$ on this
interval, we have

$\displaystyle\eta(h(x))\leq-\frac{\tilde{\alpha}(h(x))}{\alpha(h(x))}.$ (30)

Therefore,

$\displaystyle
h(x)\leq-\gamma(|u|)\Rightarrow{D}_{+}W(h(x))\geq-\tilde{\alpha}(h(x)).$ (31)

By combining the proof of Theorem 1 and Lemma 2, we can conclude from (31)
that the set
$\mathcal{S}_{\gamma(\|u\|)}=\\{x\in\mathbb{R}^{n}:h(x)+\gamma(\|u\|)\geq
0\\}$ is forward robustly invariant. In other words, the interconnected system
(12) is ISSf on the set $\mathcal{S}_{\gamma(\|u\|)}$. $\Box$

Before the end of this section, we provide a simple example for illustration.

Example 1. Consider the interconnected system

$\displaystyle\dot{x}_{1}=-x_{1}-0.24x_{2}\sin(x_{1}-x_{2})-0.5u_{1}^{3},$
$\displaystyle\dot{x}_{2}=-x_{2}-0.16x_{1}\sin(x_{2}-x_{1})-0.5u_{2}.$

Suppose that $x_{1}$-subsystem and $x_{2}$-subsystem are ISSf on the safety
sets $\mathcal{S}_{1}$ and $\mathcal{S}_{2}$, respectively, where

$\displaystyle\mathcal{S}_{1}=\big{\\{}x_{1}:x_{1}+\max\\{0.96\|x_{2}\|,2\|u_{1}\|^{3}\\}\geq
0\big{\\}},$
$\displaystyle\mathcal{S}_{2}=\big{\\{}x_{2}:x_{2}+\max\\{0.64\|x_{1}\|,2\|u_{2}\|\\}\geq
0\big{\\}}.$

The objective of this example is to verify that the overall system is ISSf.

To achieve the control objective of Example 1, we choose $h_{1}(x_{1})=x_{1}$
and $h_{2}(x_{2})=x_{2}$, and then it follows that

$\displaystyle
h_{1}(x_{1})\leq-\max\\{0.96|h_{2}|,2|u_{1}|^{3}\\}\Rightarrow\dot{h}_{1}(x_{1})\geq-0.5h_{1}(x_{1}),$
$\displaystyle
h_{2}(x_{2})\leq-\max\\{0.64|h_{1}|,2|u_{2}|\\}\Rightarrow\dot{h}_{2}(x_{2})\geq-0.5h_{2}(x_{2}).$

Thus, the barrier-type conditions given in (13) and (14) are satisfied.
Moreover, we can specify that $\phi_{1}(r)=0.96r$, $\phi_{2}(r)=0.64r$,
$\gamma_{1}(r)=2r^{3}$ and $\gamma_{2}(r)=2r$. Then we obtain
$\phi_{1}\circ\phi_{2}(r)=0.6144r$, which implies that the small-gain
condition (18) is satisfied. By combining this with Lemma 4, we can take
$\phi(r)=r$. With taking $h(x)=\min\\{x_{1},x_{2}\\}$ and recalling (24), we
have

$\displaystyle h(x)\leq-2|u|^{3}-2|u|{\Rightarrow}D_{+}{h}(x)\geq-0.5h(x),$

which implies the set

$\displaystyle\mathcal{S}=\\{x:h(x)+2\|u\|^{3}+2\|u\|\geq 0\\}$

is forward robustly invariant. Clearly, we can see that $\mathcal{S}$ is a
safety set obtained from the safety sets $\mathcal{S}_{1}$ and
$\mathcal{S}_{2}$ in the lower dimensional spaces.

##  V Conclusion

We have developed a small-gain theorem based on ISSf-barrier functions for
safety verification. It is shown that an interconnected system, which consists
of two ISSf subsystems, is ISSf if the absolute value of the composition of
ISSf gains of two subsystems is smaller than that of the identity function.

## Appendix

###  V-A Proof of Lemma 3

Suppose $-\frac{1}{2}\leq\rho_{0}(r)<0$ for all $r<0$ and
$0<\rho_{0}(r)\leq\frac{1}{2}$ for all $r>0$. Otherwise, we use

$\displaystyle\left\\{\begin{array}[]{ll}\max\\{-\frac{1}{2},\rho_{0}(r)\\},&\text{if
}r<0\\\ 0,&\text{if }r=0\\\ \min\\{\frac{1}{2},\rho_{0}(r)\\},&\text{if
}r>0\end{array}\right.$ (35)

to replace $\rho_{0}(r)$. Let $\rho_{1}(0)=0$ and

$\displaystyle\rho_{1}(r)=\left\\{\begin{array}[]{ll}\rho_{1}^{-}(r),&\text{if
}r<0\\\ \rho_{1}^{+}(r),&\text{if }r>0\end{array}\right.$ (38)

with

$\displaystyle\rho_{1}^{-}(r)=\left\\{\begin{array}[]{ll}\max_{s\in[-2,r]}\rho_{0}(s)&\text{if
}-1\leq{r}<0;\\\ \max_{s\in[r-1,-1]}\rho_{0}(s)&\text{if
}r<-1;\end{array}\right.$ (41)
$\displaystyle\rho_{1}^{+}(r)=\left\\{\begin{array}[]{ll}\min_{s\in[r,2]}\rho_{0}(s)&\text{if
}0<r\leq 1\\\ \min_{s\in[1,r+1]}\rho_{0}(s)&\text{if }r>1.\end{array}\right.$
(44)

Since $\rho_{0}(r)<0$ for $r\in[-2,0)$,

$\displaystyle\lim_{r\rightarrow
0^{-}}\rho_{1}(r)=\max_{s\in[-2,0]}\rho_{0}(s)=0;$

and analogously,

$\displaystyle\lim_{r\rightarrow
0^{+}}\rho_{1}(r)=\min_{s\in[r,2]}\rho_{0}(s)=0.$

Thus, $\rho_{1}$ is continuous at zero. Clearly, $\rho_{1}$ is continuous at
$r=-1$ and at $r=1$. Thus, $\rho_{1}$ is continuous on $\mathbb{R}$.

To get a desired function $\rho$ satisfying the properties given in Lemma 3,
we take

$\displaystyle\rho(r)=\left\\{\begin{array}[]{ll}\int_{r}^{r+1}\rho_{1}(s)\text{d}s,&\text{if
}r<-1;\\\ \int_{r}^{0}\rho_{1}(s)\text{d}s,&\text{if }-1\leq{r}<0;\\\
\int_{0}^{r}\rho_{1}(s)\text{d}s,&\text{if }0\leq{r}\leq 1;\\\
\int_{r-1}^{r}\rho_{1}(s)\text{d}s&\text{if }r>1.\end{array}\right.$ (49)

Since $\rho_{1}$ is a continuous function, we can verify that $\rho$ is
continuously differentiable on $\mathbb{R}$. Note that
$\rho_{0}(r)\leq\rho_{1}(r)<0$ for $r<0$, and $0<\rho_{1}(r)\leq\rho_{0}(r)$
for $r>0$. As a result, it is easy to see that
$\rho^{\prime}(r)\leq|\rho_{1}(r)|\leq\frac{1}{2}$ for all $r\in\mathbb{R}$.
The second requirement given in Lemma 3 is met.

Next, we show that $\rho$ also meets the first requirement of Lemma 3. Note
that $\rho_{1}$ is not increasing on $(-\infty,-1)\cup(1,\infty)$, and not
decreasing on $(-1,1)$. Also note that $\rho_{1}(r+1)\geq\rho_{0}(r)$ for
$r\leq-1$, and $\rho_{1}(-1)\leq\rho_{0}(r)$ for all $r\geq 1$. Then, with
(49), it can be observed that

$\displaystyle\begin{array}[]{ll}\rho(r)\geq-{r}\rho_{1}(r)\geq\rho_{0}(r),&\forall{r}\in[-1,0);\\\
\rho(r)\geq\rho_{1}(-1)\geq\rho_{0}(r),&\forall{r}\in(-2,-1);\\\
\rho(r)\geq\rho_{1}(r+1)\geq\rho_{0}(r),&\forall{r}\in(-\infty,-2].\\\
\end{array}$ (53)

The first and the third inequalities are easy to verify by noting that
$\rho_{1}$ is not decreasing on $(-1,0)$ and not increasing on $(-\infty,-2]$.
For the second inequality, note that $\rho_{1}(-1)\leq\rho_{1}(r)<0$ for all
$r\in(-2,-1)$. Similarly,

$\displaystyle\begin{array}[]{ll}\rho(r)\leq{r}\rho_{1}(r)\leq\rho_{0}(r),&\forall
r\in(0,1];\\\ \rho(r)\leq\rho_{1}(1)\leq\rho_{0}(r),&\forall r\in(1,2);\\\
\rho(r)\leq\rho_{1}(r-1)\leq\rho_{0}(r),&\forall r\in[2,\infty).\end{array}$
(57)

Thus, the conclusion follows.

###  V-B Proof of Lemma 4

Let

$\displaystyle\rho_{0}(r)=\frac{1}{2}[r-\phi_{1}\circ\phi_{2}(r)].$ (58)

According to (18),

$\displaystyle\phi_{1}\circ\phi_{2}(r)>r-\rho_{0}(r),\;\;\text{if }r<0;$
$\displaystyle\phi_{1}\circ\phi_{2}(r)<r-\rho_{0}(r),\;\;\text{if }r>0;$

and hence,

$\displaystyle\phi_{2}(r)>\phi_{1}^{-1}(r-\rho_{0}(r)),\;\;\forall r<0;$
$\displaystyle\phi_{2}(r)<\phi_{1}^{-1}(r-\rho_{0}(r)),\;\;\forall r>0.$

By Lemma 3, there exists a continuously differentiable function
$\rho:\mathbb{R}\rightarrow\mathbb{R}$ with $\rho^{\prime}(r)\leq\frac{1}{2}$
such that $\rho_{0}(r)<\rho(r)<0$ for each $r<0$, and $0<\rho(r)<\rho_{0}(r)$
for each $r>0$. Without loss of generality, we assume that $|\rho(r)|<|r|$.
Now we let $\phi(0)=0$ and

$\displaystyle\phi(r)=\frac{1}{\rho(r)}\int_{r-\rho(r)}^{r}\phi_{1}^{-1}(s)\text{d}s,\;\;\forall{r}\neq
0.$ (59)

With such a function, it yields immediately that
$\phi_{1}^{-1}(r)<\phi(r)<\phi_{1}^{-1}(r-\rho(r))<\phi_{2}(r)$ for all $r<0$,
and $\phi_{2}(r)<\phi_{1}^{-1}(r-\rho(r))<\phi(r)<\phi_{1}^{-1}(r)$ for all
$r>0$. Recall that $\phi_{1}^{-1}(0)=0$ and $\phi_{1}^{-1}$ is continuous on
$\mathbb{R}$. It means that $\lim_{r\rightarrow
0^{+}}\phi(r)=\lim_{r\rightarrow 0^{-}}\phi(r)=0$, which further implies that
$\phi(r)$ is continuous at zero, and consequently, $\phi(r)$ is continuous on
$\mathbb{R}$ as well.

Since $\rho$ is continuously differentiable on $\mathbb{R}$, $\phi$ is
continuously differentiable on $\mathbb{R}\backslash 0$, and

$\displaystyle\phi^{\prime}(r)$
$\displaystyle=-\frac{\rho^{\prime}(r)}{\rho^{2}(r)}\int_{r-\rho(r)}^{r}\phi_{1}^{-1}(s)\text{d}s$
$\displaystyle\;\;\;\;+\frac{1}{\rho(r)}[\phi_{1}^{-1}(r)-\phi_{1}^{-1}(r-\rho(r))(1-\rho^{\prime}(r))]$
$\displaystyle=\frac{1}{\rho(r)}\bigg{[}\phi_{1}^{-1}(r)-\phi_{1}^{-1}(r-\rho(r))-\frac{\rho^{\prime}(r)}{\rho(r)}$
$\displaystyle\;\;\;\;\;\;\;\;\;\;\;\;\times\int_{r-\rho(r)}^{r}\phi_{1}^{-1}(s)\text{d}s+\rho^{\prime}(r)\phi_{1}^{-1}(r-\rho(r))\bigg{]}.$
(60)

Then we show that $\phi^{\prime}(r)>0$ for all $r<0$. According to
$\rho^{\prime}(r)$, we have the following two cases.

$\bullet$ If $\rho^{\prime}(r)\leq 0$, then

$\displaystyle-\frac{\rho^{\prime}(r)}{\rho(r)}\int_{r-\rho(r)}^{r}\phi_{1}^{-1}(s)\text{d}s+\rho^{\prime}(r)\phi_{1}^{-1}(r-\rho(r))$
$\displaystyle\;\;\;\;\leq-\rho^{\prime}(r)\phi_{1}^{-1}(r-\rho(r))+\rho^{\prime}(r)\phi_{1}^{-1}(r-\rho(r))$
$\displaystyle\;\;\;\;\leq 0$ (61)

and hence, by substituting this into (V-B), one obtains $\phi^{\prime}(r)>0$.

$\bullet$ If $\rho^{\prime}(r)>0$, then

$\displaystyle-\frac{\rho^{\prime}(r)}{\rho(r)}\int_{r-\rho(r)}^{r}\phi_{1}^{-1}(s)\text{d}s+\rho^{\prime}(r)\phi_{1}^{-1}(r-\rho(r))$
$\displaystyle\;\;\;\;\leq-\rho^{\prime}(r)\phi_{1}^{-1}(r)+\rho^{\prime}(r)\phi_{1}^{-1}(r-\rho(r))$
(62)

and hence,

$\displaystyle\phi^{\prime}(r)$
$\displaystyle\geq\frac{1}{\rho(r)}[1-\rho^{\prime}(r)][\phi_{1}^{-1}(r)-\phi_{1}^{-1}(r-\rho(r))]$
$\displaystyle\geq\frac{1}{2\rho(r)}[\phi_{1}^{-1}(r)-\phi_{1}^{-1}(r-\rho(r))]$
$\displaystyle>0.$ (63)

By combining the two cases above, one can conclude that $\phi^{\prime}(r)>0$
for all $r<0$. Moreover, we can obtain from [15, Lemma A.1] that
$\phi^{\prime}(r)>0$ for all $r>0$.

## References

  * [1] X. Xu, J. W. Grizzle, P. Tabuada, and A. D. Ames, “Correctness guarantees for the composition of lane keeping and adaptive cruise control,” IEEE Transactions on Automation Science and Engineering, vol. 15, no. 3, pp. 1216–1229, 2017.
  * [2] L. Wang, A. D. Ames, and M. Egerstedt, “Safety barrier certificates for collisions-free multirobot systems,” IEEE Transactions on Robotics, vol. 33, no. 3, pp. 661–674, 2017.
  * [3] S. Balachandran, N. Ozay, and E. M. Atkins, “Verification guided refinement of flight safety assessment and management system for takeoff,” Journal of Aerospace Information Systems, vol. 13, no. 9, pp. 357–369, 2016.
  * [4] E. M. Clarke Jr, O. Grumberg, D. Kroening, D. Peled, and H. Veith, Model checking.  MIT press, 2018.
  * [5] Z. Manna and A. Pnueli, Temporal verification of reactive systems: safety.  Springer Science & Business Media, 2012.
  * [6] S. Prajna, A. Jadbabaie, and G. J. Pappas, “A framework for worst-case and stochastic safety verification using barrier certificates,” IEEE Transactions on Automatic Control, vol. 52, no. 8, pp. 1415–1428, 2007.
  * [7] A. D. Ames, J. W. Grizzle, and P. Tabuada, “Control barrier function based quadratic programs with application to adaptive cruise control,” in 53rd IEEE Conference on Decision and Control, pp. 6271–6278, IEEE, 2014.
  * [8] X. Xu, P. Tabuada, J. W. Grizzle, and A. D. Ames, “Robustness of control barrier functions for safety critical control,” IFAC-PapersOnLine, vol. 48, no. 27, pp. 54–61, 2015.
  * [9] A. D. Ames, X. Xu, J. W. Grizzle, and P. Tabuada, “Control barrier function based quadratic programs for safety critical systems,” IEEE Transactions on Automatic Control, vol. 62, no. 8, pp. 3861–3876, 2016.
  * [10] S. Kolathaya and A. D. Ames, “Input-to-state safety with control barrier functions,” IEEE control systems letters, vol. 3, no. 1, pp. 108–113, 2018\.
  * [11] P. Wieland and F. Allgöwer, “Constructive safety using control barrier functions,” IFAC Proceedings Volumes, vol. 40, no. 12, pp. 462–467, 2007\.
  * [12] S. Coogan and M. Arcak, “A dissipativity approach to safety verification for interconnected systems,” IEEE Transactions on Automatic Control, vol. 60, no. 6, pp. 1722–1727, 2014.
  * [13] M. Z. Romdlony and B. Jayawardhana, “On the new notion of input-to-state safety,” in 2016 IEEE 55th Conference on Decision and Control (CDC), pp. 6403–6409, IEEE, 2016.
  * [14] E. D. Sontag and Y. Wang, “On characterizations of the input-to-state stability property,” Systems and Control letters, vol. 24, no. 5, pp. 351–360, 1995.
  * [15] Z.-P. Jiang, I. M. Mareels, and Y. Wang, “A Lyapunov formulation of the nonlinear small-gain theorem for interconnected ISS systems,” Automatica, vol. 32, no. 8, pp. 1211–1215, 1996.
  * [16] Z.-P. Jiang, A. R. Teel, and L. Praly, “Small-gain theorem for iss systems and applications,” Mathematics of Control, Signals and Systems, vol. 7, no. 2, pp. 95–120, 1994.
  * [17] G. Yang and D. Liberzon, “A lyapunov-based small-gain theorem for interconnected switched systems,” Systems & Control Letters, vol. 78, pp. 47–54, 2015.
  * [18] L. Long and J. Zhao, “A small-gain theorem for switched interconnected nonlinear systems and its applications,” IEEE Transactions on Automatic Control, vol. 59, no. 4, pp. 1082–1088, 2013.
  * [19] D. Nesic and A. R. Teel, “A lyapunov-based small-gain theorem for hybrid iss systems,” 47th IEEE Conference on Decision and Control, pp. 3380–3385, 2008.
  * [20] H. K. Khalil and J. W. Grizzle, Nonlinear systems, vol. 3.  Prentice hall Upper Saddle River, NJ, 2002.
  * [21] F. Blanchini and S. Miani, Set-theoretic methods in control.  Springer, 2008.
  * [22] K. O. Friedrichs, Advanced ordinary differential equations.  CRC Press, 1985.
  * [23] F. H. Clarke, “Generalized gradients and applications,” Transactions of the American Mathematical Society, vol. 205, pp. 247–262, 1975.
  * [24] N. Rouche, P. Habets, and M. Laloy, Stability theory by Liapunov’s direct method, vol. 4.  Springer, 1977.
  * [25] Y. Lin, E. D. Sontag, and Y. Wang, “A smooth converse lyapunov theorem for robust stability,” SIAM Journal on Control and Optimization, vol. 34, no. 1, pp. 124–160, 1996.


# Uniquely orderable interval graphs

Marta Fiori-Carones  Instytut Matematyki, Uniwersytet Warszawski, Banacha 2,
02-097 Warszawa — Poland<EMAIL_ADDRESS>and  Alberto Marcone
Dipartimento di scienze matematiche, informatiche e fisiche, Università di
Udine, Via delle Scienze 208, 33100 Udine — Italy<EMAIL_ADDRESS>
###### Abstract.

Interval graphs and interval orders are deeply linked. In fact, edges of an
interval graphs represent the incomparability relation of an interval order,
and in general, of different interval orders. The question about the
conditions under which a given interval graph is associated to a unique
interval order (up to duality) arises naturally. Fishburn provided a
characterisation for uniquely orderable finite connected interval graphs. We
show, by an entirely new proof, that the same characterisation holds also for
infinite connected interval graphs. Using tools from reverse mathematics, we
explain why the characterisation cannot be lifted from the finite to the
infinite by compactness, as it often happens.

###### Key words and phrases:

Interval graphs, infinite graphs, unique orderability, reverse mathematics

###### 2020 Mathematics Subject Classification:

Primary 05C63; Secondary 05C75, 03B30, 05C62

Both authors were partially supported by the Italian PRIN 2017 Grant
“Mathematical Logic: models, sets, computability”.

##  1\. Introduction

An _interval graph_ is a graph whose vertices can be mapped (by an _interval
representation_) to nonempty intervals of a linear order in such a way that
two vertices are adjacent if and only if the intervals associated to them
intersect (it is thus convenient to assume that the adjacency relation is
reflexive). Consequently, if two vertices are incomparable in the graph, the
corresponding intervals are placed one before the other in the linear order.
The definition of interval graphs leads to an analogous concept for partial
orders. In fact, a partial order $<_{P}$ is an _interval order_ if its points
can be mapped to nonempty intervals of a linear order in such a way that
$x<_{P}y$ if and only if the interval associated to $x$ completely precedes
the interval associated to $y$. Thus interval graphs are the incomparability
graphs of interval orders, i.e. two vertices are adjacent in the graph if and
only if they are incomparable in the partial order.

Norbert Wiener was probably the first to pay attention to interval orders,
disguised under the less familiar name ‘relations of complete sequence’, in
[Wie14]. Interval graphs and interval orders were rediscovered and given the
current name in [Fis70]. There is now an extensive literature on the topic:
[Tro97] provides a survey for many result in this area, focusing primarily on
finite structures.

Interval graphs and interval orders are extensively employed in diverse fields
like psychology, archaeology and physics, just to mention a few. Wiener
himself noticed that interval orders are useful for the analysis of temporal
events and in the representation of measures subject to a margin of error.
Interval orders actually occur in many digital calendars, where hours and days
form a linear order and a rectangle covers the time assigned to an
appointment: if two rectangles intersect, we better choose which event we will
miss. Intervals are also suitable for representations of measurements of
physical properties which are subject to error, since they can take into
account the accuracy of the measuring device much better than a representation
with points. In psychology and economics the overlap between two intervals
often indicates that the corresponding stimuli or preferences are
indistinguishable.

In the first paragraph we described how to build an interval order from an
interval representation of an interval graph. In general, an interval graph
leads to many different interval orders on its vertices: an extreme example is
a totally disconnected graph which is associated to any total order on its
vertices. This paper deals with the situation were the interval graph is
_uniquely orderable_ , i.e. there is essentially only one interval order
associated to the given interval graph. (The “essentially” in the previous
sentence is due to the obvious observation that if an interval order is
associated to a graph, then the same is true for the reverse partial order.)
Here the extreme example is a complete graph, which is associated to a unique
partial order, the antichain of its vertices.

The question of which interval graphs are uniquely orderable is easily settled
for non connected graphs. It is in fact immediate that a non connected
interval graph is uniquely orderable if and only if it has at most two
components each of which is complete.

We can thus restrict our attention to connected interval graphs. In this
context, Fishburn [Fis85, §3.6], building on results proved in [Han82],
provides two characterizations of unique orderability for finite graphs.
Indeed, some steps of the proof heavily rely on the finiteness of the graph.
This is in contrast with the rest of Fishburn’s monograph, where results are
systematically proved for arbitrary interval graphs and orders; we thus
believe that Fishburn did not know whether his result held for infinite
interval graphs as well. The main result of this paper solves this issue by
extending Fishburn’s characterizations to arbitrary interval graphs by an
entirely different proof (for undefined notions see §2 below):

######  Theorem 1.

Let $(V,E)$ be a (possibly infinite) connected interval graph. Let
$W=\\{(a,b)\in V\times V\mid\neg a\,E\,b\\}$ and $(a,b)\,Q\,(c,d)\iff
a\,E\,c\land b\,E\,d$. The following are equivalent:

  1. (1)

$(V,E)$ is uniquely orderable;

  2. (2)

$(V,E)$ does not contain a buried subgraph;

  3. (3)

the graph $(W,Q)$ has two components.

Fishburn’s statement is slightly different from ours, since it is formulated
for connected interval graphs without universal vertices. Since universal
vertices (i.e. those adjacent to all vertices of the graph) are incomparable
to all other vertices in any partial order associated to an interval graph,
removing all universal vertices does not change the unique orderability of the
graph. We prefer our formulation of the result since it highlights the
connectedness of the graph, which is the central property characterising the
class of interval graphs for which 1 holds.

A typical method to lift a result from finite structures to arbitrary ones is
compactness. Hence, once 1 is proved for finite interval graphs, the first
attempt to generalise it to the infinite is to argue by compactness. This is
not obvious and, using tools from mathematical logic, we are able to show that
it is in fact impossible. To this end we work in the framework of reverse
mathematics, a research program whose goal is to establish the minimal axioms
needed to prove a theorem. In this framework compactness is embodied by the
formal system $\mathsf{WKL}_{0}$. We first indicate, with results which
parallel those obtained in [Mar07] about interval orders, that all the basic
aspects of the theory of interval orders can be developed in
$\mathsf{WKL}_{0}$. On the other hand we prove the following:

######  Theorem 2.

Over the base system $\mathsf{RCA}_{0}$, the following are equivalent:

  1. (1)

$\mathsf{ACA}_{0}$,

  2. (2)

a countable connected interval graph $(V,E)$ is uniquely orderable if and only
if does not contain a buried subgraph.

Since $\mathsf{ACA}_{0}$ is properly stronger than $\mathsf{WKL}_{0}$ this
shows that compactness does not suffice to prove 1.

Section 2 establishes notation and terminology, while Section 3 is devoted to
the proof of 1. Section 4 gives an overview of the reverse mathematics of
interval graphs: the first author’s PhD thesis [FC19] includes full proofs.
The last section is devoted to the proof of 2.

##  2\. Preliminaries

In this section we establish the terminology used in the paper and underline
some properties of interval graphs that turn out to be useful in the next
section.

All the graphs $(V,E)$ in this paper are such that $E\subseteq V\times V$ is a
symmetric relation (we do not ask $E$ to be irreflexive, as in some cases it
is convenient to have reflexivity). As usual, we write $v\,E\,u$ to mean
$(v,u)\in E$ and, if $V^{\prime}\subseteq V$, we write $(V^{\prime},E)$ in
place of $(V^{\prime},E\cap(V^{\prime}\times V^{\prime}))$. We denote by
$(V,\overline{E})$ the _complementary graph_ of $(V,E)$: for $u,v\in V$ we
have $u\,\overline{E}\,v$ if and only if $u\,E\,v$ does not hold.

Paths and cycles are defined as usual, and their length is the number of their
edges. A _simple cycle_ $v_{0}\,E\,\dots\,E\,v_{n}$ is a cycle such that the
vertices in $v_{0},\dots,v_{n-1}$ are distinct. A _chord_ of a cycle
$v_{0}\,E\,v_{1}\,E\,\dots\,E\,v_{n}$ is an edge $(v_{i},v_{j})$ with $2\leq
j-i\leq n-2$. The chord is _triangular_ if either $j-i=2$ or $j-i=n-2$.

######  Definition 2.1.

If $(V,\prec)$ is a strict partial order, the _comparability graph of
$(V,\prec)$_ is the graph $(V,E)$ such that for $v,u\in V$ it holds that
$v\,E\,u$ if and only if either $v\prec u$ or $u\prec v$. The _incomparability
graph of $(V,\prec)$_ is the complementary graph of the comparability graph,
so that two vertices are adjacent if and only if they coincide or are
$\prec$-incomparable.

While the comparability graph of a strict partial order is irreflexive, its
incomparability graph is reflexive.

Notice that a graph $(V,E)$ can be the incomparability graph of more than one
partial order: we say that each such partial order is _associated to $(V,E)$_.
In particular, $\prec$ and the dual of $\prec$ (i.e. $\prec^{\prime}$ such
that $u\prec^{\prime}v$ iff $v\prec u$) are associated to the same
incomparability graph.

######  Definition 2.2.

A graph $(V,E)$ is _uniquely orderable_ if it is the incomparability graph of
a partial order $\prec$ and the only other partial order associated to $(V,E)$
is the dual order of $\prec$; in other words, there exists a unique (up to
duality) partial order $\prec$ such that for each $v,u\in V$ it holds that
$\neg u\,E\,v$ if and only if $u\prec v$ or $v\prec u$.

The following definition formalises the intuitive idea of interval graph given
in the previous pages.

######  Definition 2.3.

A graph $(V,E)$ is an _interval graph_ if it is reflexive and there exist a
linear order $(L,<_{L})$ and a map $F\colon V\to\wp(L)$ such that for all
$v,u\in V$, $F(v)$ is an interval in $(L,<_{L})$ (i.e. if
$\ell<_{L}\ell^{\prime}<_{L}\ell^{\prime\prime}$ and
$\ell,\ell^{\prime\prime}\in F(v)$, then also $\ell^{\prime}\in F(v)$) and

$v\,E\,u\Leftrightarrow F(v)\cap F(u)\neq\emptyset.$

It is well-known that we may in fact assume that there exist functions
$f_{L},f_{R}\colon V\to L$ such that $F(v)=\\{\ell\in L\mid
f_{L}(v)\leq_{L}\ell\leq_{L}f_{R}(v)\\}$ for all $v\in V$ (this is the
definition given in [Fis85]).

We say that $(L,<_{L},f_{L},f_{R})$ (but often only $(f_{L},f_{R})$ or just
$F$) is a _representation_ of $(V,E)$.

To decide whether two vertices $u$ and $v$ are adjacent in an interval graph
with representation $(f_{L},f_{R})$ we can assume without loss of generality
that $f_{L}(v)\leq_{L}f_{L}(u)$ and then simply check whether
$f_{L}(u)\leq_{L}f_{R}(v)$.

In the context of a representation $(f_{L},f_{R})$ of an interval graph, we
write $F(v)<_{L}F(u)$ in place of $f_{R}(v)<_{L}f_{L}(u)$. Then $\neg v\,E\,u$
means that either $F(v)<_{L}F(u)$ or $F(u)<_{L}F(v)$.

Figure 1 provides an example of interval graph, while the graph in Figure 2
does not have an interval representation (in the figures self loops are not
shown for clarity).

abcd Figure 1. An example of interval graph with its representation acbxyz?
Figure 2. A graph which is not an interval graph, with a partial
representation

A classical characterization of interval graphs is the following ([LB62], see
[Fis85, Theorem 3.6]).

######  Definition 2.4.

A graph $(V,E)$ is _triangulated_ if every simple cycle of length four or more
has a chord. An _asteroidal triple_ in $(V,E)$ is an independent set of three
vertices (i.e. a set of pairwise non adjacent vertices) of $V$ such that any
two of them are connected by a path that avoids the vertices adjacent to the
third.

######  Theorem 2.5.

A reflexive graph $(V,E)$ is an interval graph if and only it is triangulated
and has no asteroidal triples.

######  Proposition 2.6.

Let $v_{0}\,E\,\dots\,E\,v_{n}$ be a path in the interval graph $(V,E)$ with
representation $F$, and suppose $w\in V$ is such that $F(w)\nless_{L}F(v_{0})$
and $F(v_{n})\nless_{L}F(w)$. Then $v_{i}\,E\,w$ for some $i\leq n$, and hence
$v_{0}\,E\,\dots\,E\,v_{i}\,E\,w$ and $w\,E\,v_{i}\,E\,\dots\,E\,v_{n}$ are
paths.

###### Proof.

Let $i\leq n$ be maximum such that $F(w)\nless_{L}F(v_{i})$. If $i=n$, then
$F(w)\nless_{L}F(v_{n})$ and $F(v_{n})\nless_{L}F(w)$ imply $v_{n}\,E\,w$. If
$i<n$, then $F(w)<_{L}F(v_{i+1})$ and $F(v_{i})\nless_{L}F(v_{i+1})$ (because
$v_{i}\,E\,v_{i+1}$) imply $F(v_{i})\nless_{L}F(w)$. This, together with
$F(w)\nless_{L}F(v_{i})$, yields $v_{i}\,E\,w$. ∎

######  Definition 2.7.

Let $(V,E)$ be a graph. A path $v_{0}\,E\,\dots\,E\,v_{n}$ is a _minimal path_
if $\neg v_{i}\,E\,v_{j}$ for every $i,j$ such that $i+1<j\leq n$.

Notice that if $v_{0}\,E\,\dots\,E\,v_{n}$ is a path of minimal length among
the paths connecting $v_{0}$ and $v_{n}$, then it is a minimal path, but the
reverse implication does not hold.

######  Property 2.8.

Let $(V,E)$ be a graph. Then each path can be refined to a minimal path.

###### Proof.

The statement follows immediately from the following observation: if
$v_{0}\,E\,\dots\,E\,v_{n}$ is a path and $v_{i}\,E\,v_{j}$ with $i+1<j\leq
n$, then $v_{0}\,E\,\dots\,E\,v_{i}\,E\,v_{j}\,E\,\dots\,E\,v_{n}$ is still a
path. ∎

######  Property 2.9.

Let $(V,E)$ be an interval graph with representation $(L,<_{L},f_{L},f_{R})$
and suppose that $v_{0}\,E\,\dots\,E\,v_{n}$ is a minimal path with
$F(v_{0})<_{L}F(v_{n})$.

  1. (i)

Then $f_{R}(v_{i})<_{L}f_{R}(v_{i+1})$ for each $i<n-1$ and
$f_{L}(v_{j})<_{L}f_{L}(v_{j+1})$ for each $j>0$;

  2. (ii)

if $F(v)<_{L}F(v_{0})$, then $\neg v_{i}\,E\,v$ for every $i\neq 1$;
symmetrically, if $F(v_{n})<_{L}F(v)$, then $\neg v_{i}\,E\,v$ for every
$i\neq n-1$.

###### Proof.

To check the first conjunct of (i), suppose $i<n-1$ is least such that
$f_{R}(v_{i+1})\leq_{L}f_{R}(v_{i})$. Since $i<n-1$ it holds that $\neg
v_{j}\,E\,v_{n}$ for each $j\leq i$ by definition of minimal path. An easy
induction, starting with our assumption $F(v_{0})<_{L}F(v_{n})$, shows that
$F(v_{k})<_{L}F(v_{n})$ for each $k\leq i$. Thus, in particular it holds that
$f_{R}(v_{i})<_{L}f_{R}(v_{n})$. Let $m\leq n$ be least such that
$f_{R}(v_{i})<_{L}f_{R}(v_{m})$ and notice that $m>i+1$ by choice of $i$. By
choice of $m$ it holds that
$f_{R}(v_{m-1})\leq_{L}f_{R}(v_{i})<_{L}f_{R}(v_{m})$, and so that
$f_{L}(v_{m})\leq_{L}f_{R}(v_{m-1})$ because $v_{m-1}\,E\,v_{m}$. To summarise
we get that $f_{L}(v_{m})\leq_{L}f_{R}(v_{i})<_{L}f_{R}(v_{m})$, namely that
$v_{i}\,E\,v_{m}$ contrary to the definition of minimal path.

The second conjunct of (i) follows from the first considering the interval
representation given by the linear order $(L,>_{L})$ and by the maps $f_{L}$
and $f_{R}$.

For (ii), let $v_{0}\,E\,\dots\,E\,v_{n}$ be a minimal path and
$F(v)<_{L}F(v_{0})<_{L}F(v_{n})$. Assume $v\,E\,v_{i}$, for some $i>1$ (notice
that $\neg v\,E\,v_{0}$ by assumption). Since $f_{R}(v)<_{L}f_{L}(v_{0})$ by
assumption, $f_{R}(v_{0})<_{L}f_{R}(v_{i})$ by (i), and
$f_{L}(v_{i})<_{L}f_{R}(v)$ by $v\,E\,v_{i}$, it holds that $v_{0}\,E\,v_{i}$,
contrary to the definition of minimal path. ∎

##  3\. Uniquely orderable connected interval graphs

In this section we prove 1. Suppose $(V,E)$ is a connected incomparability
graph. Saying that $(V,E)$ is not uniquely orderable amounts to check that
there are two partial orders $\prec$ and $\prec^{\prime}$ associated to
$(V,E)$ and three vertices $a,b,c\in V$ such that $a\prec b\prec c$ and
$b\prec^{\prime}a\prec^{\prime}c$. The vertices $a$ and $b$ can be reordered
regardless, so to speak, the order of $c$. The connected graph pictured (by
one of its interval representations) in Figure 3 is an example of a non
uniquely orderable connected interval graph (in fact the intervals for $a$ and
$b$ can be swapped without changing their relationship with the intervals $c$
and $k$).

$\scriptstyle{a}$$\scriptstyle{b}$$\scriptstyle{c}$$\scriptstyle{k}$ Figure 3.
An interval representation of a non uniquely orderable connected interval
graph

The first characterization of uniquely orderable interval graphs exploits the
above observation to identify subgraphs which are forbidden in uniquely
orderable interval graphs.

######  Definition 3.1.

Let $(V,E)$ be a graph. For $B\subseteq V$ let $K(B)=\\{v\in V\mid\forall b\in
B\,(v\,E\,b)\\}$ and $R(B)=V\setminus(B\cup K(B))$. We say that $B$ is a
_buried subgraph_ of $(V,E)$ if the following hold:

  1. (i)

there exist $a,b\in B$ such that $\neg a\,E\,b$,

  2. (ii)

$K(B)\cap B=\emptyset$ and $R(B)\neq\emptyset$,

  3. (iii)

if $b\in B$ and $r\in R(B)$, then $\neg b\,E\,r$.

The last point in the previous definition implies that any path between a
vertex in $B$ and a vertex outside $B$ must go through a vertex in $K(B)$. The
main consequence of (iii), which we use many times without mention, is that if
$v\in V$ is such that there exist $a,b\in B$ such that $v\,E\,a$ and $\neg
v\,E\,b$, then $v\in B$ (because $\neg v\,E\,b$ implies $v\notin K(B)$, while
$v\,E\,a$ and (iii) imply $v\notin R(B)$).

Our definition of buried subgraph is slightly different from the one in
[Fis85], but it is equivalent for the class of graphs studied by Fishburn,
i.e. connected interval graphs without universal vertices. Since we allow
universal vertices, in condition (ii) we substituted $K(B)\neq\emptyset$ with
$R(B)\neq\emptyset$ (the former condition implies the latter if there are no
universal vertices, the reverse implication holds if the graph is connected by
(iii)). Moreover we restated condition (iii) in simpler, yet equivalent,
terms.

The other main character of 1 is the graph $(W,Q)$.

######  Definition 3.2.

If $(V,E)$ is a graph we let $W=\\{(a,b)\in V\times V\mid\neg a\,E\,b\\}$ and
(writing $ab$ in place of $(a,b)$ for concision) $ab\,Q\,cd$ if and only if
$a\,E\,c$ and $b\,E\,d$.

If $ab$ and $cd$ are elements of $W$ which are connected by a path in $(W,Q)$
we write $ab\,\bar{Q}\,cd$.

######  Proposition 3.3.

Let $(V,E)$ be an interval graph and $\prec$ a partial order associated to
$(V,E)$. If $ab,cd\in W$ are such that $ab\,\bar{Q}\,cd$ and $a\prec b$, then
$c\prec d$. In particular we have $\neg ab\,\bar{Q}\,ba$.

###### Proof.

Suppose first that $ab\,Q\,cd$, so that $a\,E\,c$ and $b\,E\,d$. Notice that
$b\,E\,c$ and $a\,E\,d$ cannot both hold. In fact, if $a,b,c,d$ are not all
distinct, then this would contradict $ab\in W$ or $cd\in W$. Otherwise,
$a\,E\,c\,E\,b\,E\,d\,E\,a$ would be a simple cycle of length four without
chords, against Theorem 2.5. If $\neg b\,E\,c$, then $c\prec b$ because
$a\prec b$ and $a\,E\,c$. From this we obtain $c\prec d$, since $d\,E\,b$. If
instead $\neg a\,E\,d$ we obtain first $a\prec d$ and then again $c\prec d$.

To derive $c\prec d$ from $ab\,\bar{Q}\,cd$ it suffices to apply the
transitivity of $\prec$ to a $Q$-path connecting $ab$ with $cd$. ∎

The last part of the previous proposition implies that if $W\neq\emptyset$
(which is equivalent to $(V,E)$ being not complete), then $(W,Q)$ has at least
two components. Moreover, if $(W,Q)$ has more than two (and so at least four)
components, then for every partial order $\prec$ associated to $(V,E)$ there
exist $ab,cd\in W$ such that $a\prec b$ and $c\prec d$, yet $ab\,\bar{Q}\,cd$
fails.

We split, as originally done by Fishburn, the proof of 1 in three steps
corresponding to (1) implies (2) (Lemma 3.4), (3) implies (1) (Lemma 3.5), and
(2) implies (3) (Theorem 3.12). The proof of the first implication in [Fis85]
is not completely accurate, and we apply Fishburn’s idea after a preliminary
step which is necessary even when the graph is finite. The second implication
is straightforward and applies to interval graphs of any cardinality. The
proof of the last implication is completely new and requires more work.

The connectedness of the graph is not needed in the first two implications.
Moreover, the hypotheses of Lemma 3.4 could be further relaxed, as the proof
applies to arbitrary incomparability graphs.

######  Lemma 3.4.

Every uniquely orderable interval graph does not contain a buried subgraph.

###### Proof.

Let $(V,E)$ be an interval graph with a buried subgraph $B$. Fix a partial
order $\prec_{0}$ associated to $(V,E)$ and some $b_{0}\in B$. We define a new
binary relation $\prec$ on $V$ as follows: when either $u,v\in B$ or
$u,v\notin B$ set $u\prec v$ if and only if $u\prec_{0}v$; when $b\in B$ and
$v\notin B$ set $b\prec v$ if and only if $b_{0}\prec_{0}v$, and $v\prec b$ if
and only if $v\prec_{0}b_{0}$. Thus the whole $B$ is $\prec$-above the
elements not in $B$ which are $\prec_{0}$-below $b_{0}$ and $\prec$-below the
elements not in $B$ which are $\prec_{0}$-above $b_{0}$.

Using the fact that the vertices not in $B$ are either
$\prec_{0}$-incomparable to every vertex of $B$ or $\prec_{0}$-comparable to
every vertex of $B$, it is straightforward to check that $\prec$ is
transitive, and hence a partial order. For the same reason $\prec$ is
associated to $(V,E)$. The key feature of $\prec$ (not necessarily shared by
$\prec_{0}$) is that $B$ is $\prec$-convex, i.e. if $b\prec v\prec b^{\prime}$
with $b,b^{\prime}\in B$, then $v\in B$ as well. Indeed, if $v\notin B$, then
$b\prec v$ implies $b_{0}\prec_{0}v$ and $v\prec b^{\prime}$ implies
$v\prec_{0}b_{0}$.

Following now [Fis85], let $\prec^{\prime}$ be such that the restrictions of
$\prec$ and $\prec^{\prime}$ to $B$ are dual, while $\prec^{\prime}$ and
$\prec$ coincide on $V\setminus B$ and between elements of $B$ and $V\setminus
B$. Formally, $u\prec^{\prime}v$ if and only if either $u,v\in B$ and $v\prec
u$, or if at least one of $u$ and $v$ does not belong to $B$ and $u\prec v$.
The transitivity of $\prec^{\prime}$ is a consequence of the $\prec$-convexity
of $B$ (an observation lacking in the proof given in [Fis85]) and hence
$\prec^{\prime}$ is a partial order associated to $(V,E)$.

If $x,y\in B$ are such that $x\prec y$ and $v\in R(B)$ (these elements exist
by Definition 3.1) we have either $x\prec y\prec v$ or $v\prec x\prec y$. In
the first case $y\prec^{\prime}x\prec^{\prime}v$, in the second case
$v\prec^{\prime}y\prec^{\prime}x$, witnessing that $\prec^{\prime}$ is neither
$\prec$ nor the dual order of $\prec$. ∎

######  Lemma 3.5.

Let $(V,E)$ be an interval graph. If ($W,Q$) has two components, then $(V,E)$
is uniquely orderable.

###### Proof.

This follows easily from Proposition 3.3. ∎

For the proof of Theorem 3.12 we describe a construction that, starting from a
pair of non-adjacent vertices, attempts to build the minimal buried subgraph
containing those two vertices. We then show that if this attempt always fails,
then for any $ab,cd\in W$ either $ab\,\bar{Q}\,cd$ or $ab\,\bar{Q}\,dc$.

######  Construction 3.6.

Let $(V,E)$ be a connected interval graph and $v,u\in V$ be such that $\neg
v\,E\,u$. We define recursively $B_{n}(v,u)\subseteq V$:

$\displaystyle B_{0}(v,u)$ $\displaystyle=\\{v,u\\}$ $\displaystyle
B_{n+1}(v,u)$ $\displaystyle=\\{w\in V\mid\exists z,z^{\prime}\in
B_{n}(v,u)\,(z\,E\,w\land\neg z^{\prime}\,E\,w)\\}$

We then set $B(v,u)=\bigcup B_{n}(v,u)$. If $w\in B(v,u)$ let $e_{w}$ be the
least $n$ such that $w\in B_{n}(v,u)$ (formally we should write $e_{w}^{v,u}$
but we omit the superscript as $v$ and $u$ will always be understood).

A straightforward induction shows that $B_{n}(v,u)\subseteq B_{n+1}(v,u)$, for
each $n\in\mathbb{N}$ (for the base step recall that interval graphs are
reflexive, so that $v$ and $u$ themselves witness that $v,u\in B_{1}(v,u)$).

We now show that $B(v,u)$ is close to being a buried subgraph.

######  Property 3.7.

In the situation of 3.6, $B(v,u)$ is a buried subgraph if and only if
$R(B(v,u))\neq\emptyset$.

###### Proof.

Notice that Condition (i) of Definition 3.1 is witnessed by $v$ and $u$.
Condition (3) is obvious, because if $r\notin K(B(u,v))$ but $b\,E\,r$ for
some $b\in B(u,v)$, then $r\in B(u,v)$. Moreover, if $k\in K(B(v,u))$, then
$k\in K(B_{n}(u,v))$ for every $n$ and hence $k\notin B(u,v)$; hence
$B(v,u)\cap K(B(v,u))=\emptyset$. Therefore, to verify that $B(v,u)$ is a
buried subgraph it suffices that $R(B(v,u))\neq\emptyset$. ∎

In the next propositions, we will always consider a connected interval graph
$(V,E)$ with representation $(L,<_{L},f_{L},f_{R})$, fix $v,u\in V$ with $\neg
v\,E\,u$ and $F(v)<_{L}F(u)$ and define $B(v,u)$ as in 3.6. For brevity, we
call this set of hypotheses $(\maltese)$ and indicate it next to the
proposition number.

######  Proposition 3.8 (✠).

Let $x,y\in B(v,u)$. If $F(u)<_{L}F(x)$ and $f_{L}(x)\leq_{L}f_{L}(y)$, then
$e_{x}\leq e_{y}$. Analogously, if $F(x)<_{L}F(v)$ and
$f_{R}(y)\leq_{L}f_{R}(x)$, then $e_{x}\leq e_{y}$ as well.

###### Proof.

We prove the first half of the statement by induction on $e_{y}$. The base
case is trivially satisfied since there is no $y\in B_{0}(v,u)$ satisfying the
hypotheses. Assume $e_{y}>0$ and let $z\in B_{e_{y}-1}(v,u)$ be such that
$z\,E\,y$. If $f_{L}(x)\leq_{L}f_{L}(z)$, then $e_{x}\leq e_{z}<e_{y}$ by
induction hypothesis. Otherwise, $f_{L}(z)<_{L}f_{L}(x)\leq
f_{L}(y)\leq_{L}f_{R}(z)$ given that $z\,E\,y$. This means that $z\,E\,x$,
which implies that $x\in B_{e_{z}+1}(v,u)$ since $u\in B_{e_{z}}(v,u)$ is such
that $\neg u\,E\,x$. Hence $e_{x}\leq e_{z}+1\leq e_{y}$

The second half of the statement follows considering the representation
$(L,>_{L},f_{L},f_{R})$. ∎

######  Proposition 3.9 (✠).

Let $w\in B(v,u)$. If $F(w)\nless_{L}F(u)$, then there exists a path
$u\,E\,b_{1}\,E\,\dots b_{k}\,E\,w$ such that $e_{b_{i}}<e_{w}$ for all $i\leq
k$.

Analogously, if $F(v)\nless_{L}F(w)$, then there exists a path
$v\,E\,b_{1}\,E\,\dots b_{k}\,E\,w$ such that $e_{b_{i}}<e_{w}$ for all $i\leq
k$.

###### Proof.

By definition of $B_{e_{w}}(v,u)$ there exists a path
$b_{0}\,E\,b_{1}\,E\,\dots\,E\,b_{k}\,E\,w$ where $b_{i}\in B(v,u)$ and
$0=e_{b_{0}}<e_{b_{1}}<\dots<e_{b_{k}}<e_{w}$. Hence $b_{0}\in\\{u,v\\}$ and,
since $F(w)\nless_{L}F(u)$ and $F(u)\nless_{L}F(v)$, by Proposition 2.6 we can
assume that $b_{0}=u$.

The second half of the statement follows from the first one as usual. ∎

######  Proposition 3.10 (✠).

Let $x,z\in B(v,u)$ and $m=\max\\{e_{x},e_{z}\\}$. Assume $F(z)<_{L}F(x)$ and
$F(v)\nless_{L}F(x)$ (this implies $m>0$). Then there exists a minimal path
$z\,E\,v_{1}\,E\,\dots\,E\,v_{n}\,E\,x$ and $s\in B(v,u)$ with $e_{s}<m$ such
that $e_{v_{i}}<m$ and $F(v_{i})<_{L}F(s)$ for each $i\leq n$.

Analogously, if $F(x)<_{L}F(z)$ and $F(x)\nless_{L}F(u)$ there exists a
minimal path $x\,E\,v_{1}\,E\,\dots\,E\,v_{n}\,E\,z$ and $s\in B(v,u)$ with
$e_{s}<m$ such that $e_{v_{i}}<m$ and $F(s)<_{L}F(v_{i})$ for each $i\leq n$.

###### Proof.

Notice that once we find the minimal path
$z\,E\,v_{1}\,E\,\dots\,E\,v_{n}\,E\,x$ and $s\in B(v,u)$ with $e_{s}<m$ such
that $e_{v_{i}}<m$ for all $i\leq n$ it suffices to prove that
$F(v_{n})<_{L}F(s)$, since then $F(v_{i})<_{L}F(s)$ for $i<n$ follows from
2.9.i.

We can apply Proposition 3.9 to both $x$ and $z$ obtaining paths connecting
$v$ to $x$ and $v$ to $z$ and with $e_{b}<m$ for all vertices $b$, distinct
from $x$ and $z$, occurring in the paths. Joining these paths and then using
2.8 we obtain a minimal path $z\,E\,v_{1}\,E\,\dots\,E\,v_{n}\,E\,x$ with
$e_{v_{i}}<m$. Notice that $n>0$ as $\neg z\,E\,x$. Let $j<m$ be such that
$e_{v_{n}}=j$: we may assume $j$ is least for which such a minimal path
exists.

If $j=0$, then we claim that we can assume $v_{n}=v$ and hence we can choose
$s=u$. In fact, if $v_{n}=u$, then $F(x)<_{L}F(v)$ is impossible and we have
$v\,E\,x$. The hypotheses imply $F(v)\nless_{L}F(z)$ and, since
$F(u)\nless_{L}F(v)$, by Proposition 2.6 we can find $i<n$ such that
$v\,E\,v_{i}$ and consider the path
$z\,E\,v_{1}\,E\,\dots\,E\,v_{i}\,E\,v\,E\,x$.

We now assume $j>0$: there exists $s\in B(v,u)$ such that $e_{s}<j$ and $\neg
s\,E\,v_{n}$. We claim that $F(v_{n})<_{L}F(s)$, completing the proof. Suppose
on the contrary that $F(s)<_{L}F(v_{n})$ ($F(v_{n})\cap F(s)\neq\emptyset$
cannot hold because $\neg s\,E\,v_{n}$).

In this case we have $F(s)<_{L}F(x)$ because $f_{L}(v_{n})<_{L}f_{L}(x)$ by
2.9.i. Hence $F(v)\nless_{L}F(s)$ and we can use Proposition 3.9 and 2.8 to
obtain a minimal path $s\,E\,u_{1}\,E\,\dots\,E\,u_{\ell}$, with $u_{\ell}=v$
and $e_{u_{i}}<e_{s}$. Since $F(x)\nless_{L}F(s)$ and $F(v)\nless_{L}F(x)$ by
Proposition 2.6 there exists $k\leq\ell$ such that $u_{k}\,E\,x$. We
distinguish two cases: $F(z)\nless_{L}F(s)$ and $F(z)<_{L}F(s)$.

In the first case we apply Proposition 2.6 to the path
$s\,E\,u_{1}\,E\,\dots\,E\,u_{k}\,E\,x$: there exists $h\leq k$ such that
$z\,E\,u_{h}$. Since $z\,E\,u_{h}\,E\,\dots\,E\,u_{k}\,E\,x$ can be refined to
a minimal path and $e_{u_{i}}<j$, the minimality of $j$ is contradicted.

In the second case we apply Proposition 2.6 to the path
$z\,E\,v_{1}\,E\,\dots\,E\,v_{n}\,E\,x$: there exists $h<n$ (recall that $\neg
v_{n}\,E\,s$) such that $v_{h}\,E\,s$. Then
$z\,E\,v_{1}\,E\,\dots\,E\,v_{h}\,E\,s\,E\,u_{1}\,E\,\dots\,E\,u_{k}\,E\,x$
can be refined to a path, which can then be refined to a minimal path
$z\,E\,w_{1}\,E\,\dots\,E\,w_{r}\,E\,x$. Notice that $w_{r}=u_{p}$, for some
$p\leq k$ because $\neg v_{i}\,E\,x$ for every $i\leq h<n$, by minimality of
the path $z\,E\,v_{1}\,E\,\dots\,E\,v_{n}\,E\,x$, and $F(s)<_{L}F(x)$. Since
$e_{w_{r}}<j$ we contradict again the minimality of $j$.

The second half of the statement follows from the first one as usual. ∎

######  Lemma 3.11 (✠).

If $x,y\in B(v,u)$, $f_{R}(x)\leq_{L}f_{R}(v)$ and $f_{L}(u)\leq_{L}f_{L}(y)$,
then $vu\,\bar{Q}\,xy$.

###### Proof.

The proof is by induction on $e_{x}+e_{y}$. If $e_{x}+e_{y}=0$, then $x=v$ and
$y=u$, so that the conclusion is immediate (recall that $Q$ is reflexive). Now
assume that $e_{x}+e_{y}>0$ and suppose $e_{x}\leq e_{y}$ (if $e_{y}<e_{x}$ we
can employ the usual trick of reversing the representation) and hence
$e_{y}>0$.

If $u\,E\,y$, then $xu\,Q\,xy$ and, since the induction hypothesis implies
$vu\,\bar{Q}\,xu$ (because $e_{u}=0$), we obtain $vu\,\bar{Q}\,xy$. Thus we
assume $\neg u\,E\,y$ and hence $F(u)<_{L}F(y)$. Let $z\in B_{e_{y}-1}(v,u)$
be such that $y\,E\,z$. If $f_{L}(u)\leq_{L}f_{L}(z)$, then we can apply the
induction hypothesis to $xz$ obtaining $vu\,\bar{Q}\,xz$. Since $xz\,Q\,xy$,
we are done.

We thus assume $f_{L}(z)<_{L}f_{L}(u)$ which, together with $F(u)<_{L}F(y)$
and $z\,E\,y$, implies $f_{R}(u)<_{L}f_{R}(z)$ and hence $z\,E\,u$. Notice
moreover that $z\neq u$ and hence (since $z\neq v$ is obvious) $e_{y}>1$. If
$\neg x\,E\,z$, then $xu\,Q\,xz\,Q\,xy$ and, since by induction hypothesis
$vu\,\bar{Q}\,xu$, we have $vu\,\bar{Q}\,xy$. If instead $x\,E\,z$ we must
have $f_{L}(z)\leq_{L}f_{R}(x)\leq_{L}f_{R}(v)$. Let $t\in B_{e_{y}-2}(v,u)$
be such that $\neg t\,E\,z$. If $F(z)<_{L}F(t)$, then $F(u)<_{L}F(t)$ and
$f_{L}(y)<_{L}f_{L}(t)$, so that Proposition 3.8 implies $y\in
B_{e_{y}-2}(v,u)$, which is impossible. Hence $F(t)<_{L}F(z)$. This implies
$f_{R}(t)<_{L}f_{R}(x)$. It follows that $x\in B_{e_{y}-1}(v,u)$, either by
Proposition 3.8, if $F(x)<_{L}F(v)$, or because $x\in B_{1}(v,u)$ if
$x\,E\,v$, given that $\neg x\,E\,u$. Since $vu\,\bar{Q}\,tu$ holds by
induction hypothesis and we have also $tu\,Q\,tz\,Q\,ty$ it suffices to show
that $ty\,\bar{Q}\,xy$.

If $t\,E\,x$ the conclusion is immediate, otherwise $F(t)<_{L}F(x)$. Since
$F(v)\nless_{L}F(x)$ we can apply Proposition 3.10 finding a minimal path
$t\,E\,u_{1}\,E\,\dots\,E\,u_{n}\,E\,x$ and $s\in B_{e_{y}-2}(v,u)$ such that
$u_{i}\in B_{e_{y}-2}(v,u)$ and $F(u_{i})<_{L}F(s)$ for all $i\leq n$. We
claim that $\neg u_{i}\,E\,y$, for each $i\leq n$, so that
$ty\,Q\,u_{1}y\,Q\,\dots\,Q\,u_{n}y\,Q\,xy$ witnesses $ty\,\bar{Q}\,xy$.
Indeed, if $u_{i}\,E\,y$, for some $i\leq n$, we would have
$f_{L}(y)<_{L}f_{R}(u_{i})<_{L}f_{L}(s)$ and we could apply Proposition 3.8 to
obtain $y\in B_{e_{y}-2}(v,u)$, which is impossible. ∎

######  Theorem 3.12.

Let $(V,E)$ be a connected interval graph. If $(V,E)$ does not contain a
buried subgraph, then $(W,Q)$ has two components.

###### Proof.

Fix a representation $(L,<_{L},f_{L},f_{R})$ of $(V,E)$ and assume that
$(V,E)$ does not contain a buried subgraph. We show that if $ab,cd\in W$ are
such that $F(a)<_{L}F(b)$ and $F(c)<_{L}F(d)$, then $ab\,\bar{Q}\,cd$. We can
assume without loss of generality that $f_{R}(c)\leq_{L}f_{R}(a)$. We consider
three cases:

  1. Case 1:

$f_{L}(b)<_{L}f_{L}(d)$: $B(a,b)$ (which satisfies the hypotheses of
$(\maltese)$) is not a buried subgraph and hence by 3.7 we must have
$B(a,b)=V$. In particular $c,d\in B(a,b)$ and we are in the hypotheses of
Lemma 3.11: we conclude that $ab\,\bar{Q}\,cd$.

  2. Case 2:

$f_{R}(a)<_{L}f_{L}(d)\leq_{L}f_{L}(b)$: $B(a,d)$ (which satisfies the
hypotheses of $(\maltese)$) is not a buried subgraph and hence by 3.7 $b,c\in
B(a,d)$. Lemma 3.11 implies both $ad\,\bar{Q}\,ab$ and $ad\,\bar{Q}\,cd$. It
follows that $ab\,\bar{Q}\,cd$.

  3. Case 3:

$f_{L}(d)\leq_{L}f_{R}(a)$: neither $B(a,b)$ nor $B(c,d)$ (which both satisfy
the hypotheses of $(\maltese)$) is a buried subgraph. By 3.7 we have $c\in
B(a,b)$, which implies $ab\,\bar{Q}\,cb$, and $b\in B(c,d)$, which together
with $f_{L}(d)<_{L}f_{L}(b)$ yields $cd\,\bar{Q}\,cb$ (we use Lemma 3.11 in
both cases). Thus $ab\,\bar{Q}\,cd$ also in this case.∎

##  4\. Reverse mathematics and interval graphs

Reverse mathematics is a research program, which dates back to the Seventies,
whose goal is to find the exact axiomatic strength of theorems from different
areas of mathematics. It deals with statements about countable, or countably
representable, structures, using the framework of the formal system of second
order arithmetic $\mathsf{Z}_{2}$. We do not introduce reverse mathematics
here, but refer the reader to monographs such as [Sim09] and [Hir15].

The subsystems of second order arithmetic are obtained by limiting the
comprehension and induction axioms of $\mathsf{Z}_{2}$ to specific classes of
formulas. We mention only the subsystems we are going to use in this paper:
$\mathsf{RCA}_{0}$ is the weak base theory corresponding to computable
mathematics, $\mathsf{WKL}_{0}$ extends $\mathsf{RCA}_{0}$ by adding Weak
König’s Lemma (each infinite binary tree has an infinite path), and
$\mathsf{ACA}_{0}$ is even stronger allowing for definitions of sets by
arithmetical comprehension. It is well-known that $\mathsf{WKL}_{0}$ is
equivalent to many compactness principles and thus we can claim that a theorem
not provable in $\mathsf{WKL}_{0}$ does not admit a proof by compactness. In
particular this applies to 1, as 2 shows that it is not provable in
$\mathsf{WKL}_{0}$.

The second author studied the equivalence of different characterizations of
interval orders from the reverse mathematics perspective in [Mar07]. A similar
study can be carried out for interval graphs, and we summarize here the main
results: full details and proofs are included in the first author’s PhD thesis
[FC19], which includes also results about the subclass of indifference graphs
(corresponding to proper interval orders studied in [Mar07]).

As customary in reverse mathematics, the system in parenthesis indicates where
the definition is given or the statement proved. Notice also that in this and
in the next section we deal with countable graphs and orders, the only ones
second order arithmetic and its subsystems can speak of.

In the literature it is possible to find slightly different definitions of
interval graphs and orders, which depend on the notion of interval employed.
For example intervals may be required to be closed or not. We thus have five
conceptually distinct definitions of interval graphs:

######  Definition 4.1 ($\mathsf{RCA}_{0}$).

Let $(V,E)$ be a graph.

  * •

$(V,E)$ is an _interval graph_ if there exist a linear order $(L,<_{L})$ and a
relation $F\subseteq V\times L$ such that, abbreviating $\\{x\in L\mid(p,x)\in
F\\}$ by $F(p)$, for all $p,q\in V$ the following hold:

    * (i1)

$F(p)\neq\emptyset$ and $\forall x,y\in F(p)\,\forall z\in
L\,(x<_{L}z<_{L}y\rightarrow z\in F(p))$,

    * (i2)

$p\,E\,q\Leftrightarrow F(p)\cap F(q)\neq\emptyset$.

  * •

$(V,E)$ is a _1-1 interval graph_ if it also satisfies

    * (i3)

$F(p)\neq F(q)$ whenever $p\neq q$.

  * •

$(V,E)$ is a _closed interval graph_ if there exist a linear order $(L,<_{L})$
and two functions $f_{L},f_{R}\colon V\to L$ such that for all $p,q\in V$

    * (c1)

$f_{L}(p)<_{L}f_{R}(p)$,

    * (c2)

$p\,E\,q\Leftrightarrow f_{L}(p)\leq_{L}f_{R}(q)\leq_{L}f_{R}(p)\lor
f_{L}(q)\leq_{L}f_{R}(p)\leq_{L}f_{R}(q)$

  * •

A closed interval graph $(V,E)$ is a _1-1 closed interval graph_ if we also
have

    * (c3)

$f_{R}(p)\neq f_{R}(q)\lor f_{L}(p)\neq f_{L}(q)$ whenever $p\neq q$.

  * •

$(V,E)$ is a _distinguishing interval graph_ if (c1) and (c2) hold together
with

    * (c4)

$f_{i}(p)\neq f_{j}(q)$ whenever $p\neq q\lor i\neq j$.

###  4.1. Definitions and characterizations of interval graph

In Definition 2.3 we mentioned that every interval graph is a closed interval
graph: in fact all the notions introduced in Definition 4.1 are equivalent in
a sufficiently strong theory. Our first results concern the systems where the
implications between the notions introduced in Definition 4.1 can be proved.
The same investigation for interval orders was carried out in [Mar07] and in
this respect interval graphs and interval orders behave similarly. Indeed the
proofs of the results we are going to state either mimic the corresponding
proofs for interval orders or are easily derived from those results.

Definition 4.1 enumerates increasingly strong conditions, so that the
implications from a later to an earlier notion are easily proved in
$\mathsf{RCA}_{0}$. Regarding the other implications we obtain that, as is the
case for interval orders, there are three distinct notions of interval graphs
in $\mathsf{RCA}_{0}$, namely that of interval, 1-1 interval and closed
interval graph.

######  Theorem 4.2 ($\mathsf{RCA}_{0}$).

Every closed interval graph is a distinguishing interval graph.

######  Theorem 4.3 ($\mathsf{RCA}_{0}$).

The following are equivalent:

  1. (1)

$\mathsf{WKL}_{0}$;

  2. (2)

every interval graph is a 1-1 interval graph;

  3. (3)

every 1-1 interval graph is a closed interval graph;

  4. (4)

every interval graph is a closed interval graph.

###  4.2. Structural characterizations of interval graphs

Since interval graphs are incomparability graphs (and Definition 2.1 can be
given in $\mathsf{RCA}_{0}$) we first look at the most important structural
characterization of comparability graphs. The first result is due to Jeff
Hirst ([Hir87, Theorem 3.20]).

######  Lemma 4.4 ($\mathsf{RCA}_{0}$).

The following are equivalent:

  1. (1)

$\mathsf{WKL}_{0}$;

  2. (2)

every irreflexive graph such that every cycle of odd length has a triangular
chord is a comparability graph.

We then consider two structural characterizations of interval graphs (notice
that Definition 2.4 can be given in $\mathsf{RCA}_{0}$). The necessity of both
conditions is provable in $\mathsf{RCA}_{0}$, but the sufficiency of one of
them requires $\mathsf{WKL}_{0}$.

######  Theorem 4.5 ($\mathsf{RCA}_{0}$).

Every interval graph is an incomparability graph such that every simple cycle
of length four has a chord. Moreover, every interval graph is triangulated and
has no asteroidal triples.

Every incomparability graph such that every simple cycle of length four has a
chord is an interval graph.

######  Theorem 4.6 ($\mathsf{RCA}_{0}$).

The following are equivalent:

  1. (1)

$\mathsf{WKL}_{0}$;

  2. (2)

if a reflexive graph is triangulated and has no asteroidal triples, then it is
an interval graph.

Figure 4 summarizes the results about the different definitions and
characterizations of interval graphs. The arrows correspond to provability in
$\mathsf{RCA}_{0}$, while every implication from a notion below another is
equivalent to $\mathsf{WKL}_{0}$.

distinguishing interval1-1 closed intervalclosed interval1-1 intervalfour
cycle + incomparabilityinterval graphtriangulated + no asteroidal triples
Figure 4. Implications in $\mathsf{RCA}_{0}$

Schmerl [Sch05] claimed that the statement “A graph is an interval graph if
and only if each finite subgraph is representable by intervals” is equivalent
to $\mathsf{WKL}_{0}$. Theorem 4.6 confirms his claim and shows that
compactness is necessary to prove the statement. On the other hand, the
corresponding statement for interval orders, i.e. an order is an interval
order if and only if each suborders is an interval order, is provable in
$\mathsf{RCA}_{0}$ because the structural characterization of interval orders
(as the partial orders not containing $2\oplus 2$) is provable in
$\mathsf{RCA}_{0}$ [Mar07, Theorem 2.1]. The different strengths of the
structural characterizations of interval graphs and orders can be traced to
the fact that an interval order carries full information about the relative
position of the intervals in its representations, while an interval graph does
not.

Lekkerkerker and Boland [LB62] provide another characterization of interval
graphs listing all the forbidden subgraphs. It is routine to check in
$\mathsf{RCA}_{0}$ that those graphs are a complete list of graphs whose
cycles of length greater than four do not have chords or which contain an
asteroidal triple.

###  4.3. Interval graphs and interval orders

Different definitions for interval orders, mirroring those of Definition 4.1,
were given and studied in [Mar07]. We give here only the most basic one, as
the others can be easily guessed from this.

######  Definition 4.7 ($\mathsf{RCA}_{0}$).

A partial order $(V,\preceq)$ is an _interval order_ if there exist a linear
order $(L,<_{L})$ and a relation $F\subseteq V\times L$ such that,
abbreviating $\\{x\in L\mid(p,x)\in F\\}$ by $F(p)$, for all $p,q\in V$ the
following hold:

  * (i1)

$F(p)\neq\emptyset$ and $\forall x,y\in F(p)\,\forall z\in
L\,(x<_{L}z<_{L}y\rightarrow z\in F(p))$,

  * (i2)

$p\preceq q\Leftrightarrow\forall x\in F(p)\,\forall y\in F(q)\,(x<_{L}y)$.

We explore the strength of the statements that allow moving from interval
graphs to interval orders and back. By the previous results (and the
corresponding ones in [Mar07]) it suffices to consider three different notions
on each side, and we concentrate on the relationship between corresponding
notions. In one direction everything goes through in $\mathsf{RCA}_{0}$.

######  Theorem 4.8 ($\mathsf{RCA}_{0}$).

Let $(V,E)$ be a graph and let $\mathcal{P}$ be any of “interval”, “1-1
interval”, “closed interval”. $(V,E)$ is a $\mathcal{P}$ graph if and only if
there exists a $\mathcal{P}$ order $(V,\prec)$ such that
$p\,E\,q\Leftrightarrow p\nprec q\land q\nprec p$ for all $p,q\in V$.

The other direction is more interesting, as only in one case
$\mathsf{RCA}_{0}$ suffices. The proofs of the reversals to $\mathsf{WKL}_{0}$
are modifications of the proof of [Mar07, Theorem 6.4].

######  Theorem 4.9 ($\mathsf{RCA}_{0}$).

Let $(V,\preceq)$ be a partial order. $(V,\preceq)$ is an interval order if
and only if $(V,E)$, where $p\,E\,q\Leftrightarrow p\nprec q\land q\nprec p$
for all $p,q\in V$, is an interval graph.

######  Theorem 4.10 ($\mathsf{RCA}_{0}$).

The following are equivalent:

  1. (1)

$\mathsf{WKL}_{0}$

  2. (2)

Let $(V,\preceq)$ be a partial order. $(V,\preceq)$ is a 1-1 interval order if
and only if $(V,E)$, where $p\,E\,q\Leftrightarrow p\nprec q\land q\nprec p$
for all $p,q\in V$, is a 1-1 interval graph.

  3. (3)

Let $(V,\preceq)$ be a partial order. $(V,\preceq)$ is a closed interval order
if and only if $(V,E)$, where $p\,E\,q\Leftrightarrow p\nprec q\land q\nprec
p$ for all $p,q\in V$, is a closed interval graph.

##  5\. Why compactness does not suffice

It is immediate (using Theorem 4.5) that Lemmas 3.4 and 3.5 are provable in
$\mathsf{RCA}_{0}$. On the other hand, we now show that Theorem 3.12 is much
stronger, and indeed equivalent to $\mathsf{ACA}_{0}$. As mentioned in the
introduction of the paper, this result explains why the attempts to prove it
by compactness cannot succeed.

######  Lemma 5.1 ($\mathsf{ACA}_{0}$).

Let $(V,E)$ be a connected reflexive graph which is triangulated and with no
asteroidal triples. Suppose furthermore that $a,b,c,d\in V$ are such that
$\neg ab\,\bar{Q}\,cd$ and $\neg ab\,\bar{Q}\,dc$. Then there exists a buried
subgraph $B\subseteq V$ such that either $a,b\in B$ or $c,d\in B$, and no
subgraph $A\subseteq B$, which contains either $a,b$ or $c,d$ respectively, is
a buried subgraph.

###### Proof.

By Theorems 4.3 and 4.6 $\mathsf{WKL}_{0}$, and a fortiori $\mathsf{ACA}_{0}$,
suffices to prove that any connected graph which is triangulated and with no
asteroidal triples has a closed interval representation. We then need to check
that the proof of Theorem 3.12, which indeed provides a buried subgraph with
the desired properties, goes through in $\mathsf{ACA}_{0}$.

The first step is checking that, given $v,u\in V$ with $\neg v\,E\,u$, we can
carry out 3.6 and define $B(v,u)$ and the various $B_{n}(v,u)$’s in
$\mathsf{ACA}_{0}$. In fact the definition of each $B_{n}(v,u)$ in 3.6 uses an
instance of arithmetical comprehension and thus the whole construction, as
presented there, appears to require the system known as
$\mathsf{ACA}_{0}^{+}$, which is properly stronger than $\mathsf{ACA}_{0}$.

This problem can however be overcome in the following way. Given $v,u\in V$ as
before, we can characterize $B(v,u)$ as the set of $w\in V$ such that there
exists a finite tree $T\subseteq 2^{<\mathbb{N}}$ and a label function
$\ell\colon T\to V$ with the following properties:

  * •

$\ell(\emptyset)=w$ (here $\emptyset$ is the root of $T$);

  * •

if $\sigma\in T$ is not a leaf of $T$, then
$\sigma{}^{\smallfrown}0,\sigma{}^{\smallfrown}1\in T$,
$\ell(\sigma)\,E\,\ell(\sigma{}^{\smallfrown}0)$ and
$\neg\ell(\sigma)\,E\,\ell(\sigma{}^{\smallfrown}1)$;

  * •

if $\sigma\in T$ is a leaf of $T$, then $\ell(\sigma)\in\\{v,u\\}$.

In fact, the tree and its label function describe the ‘steps’ allowing $w$ to
enter $B(v,u)$. Moreover $B_{n}(v,u)$ is the set of $w\in V$ such that there
exists $T\subseteq 2^{<n}$ and $\ell$ witnessing $w\in B(v,u)$. These
characterizations of $B(v,u)$ and $B_{n}(v,u)$ use $\Sigma^{0}_{1}$-formulas,
and show that $\mathsf{ACA}_{0}$ suffices to prove the existence of the sets.

Once $B(v,u)$ and each $B_{n}(v,u)$ are defined, it is straightforward to
check that all subsequent steps in the proof of Theorem 3.12 can be carried
out in $\mathsf{RCA}_{0}$. ∎

To prove that Theorem 3.12 implies $\mathsf{ACA}_{0}$ we use the following
notions. Given an injective function $f\colon\mathbb{N}\to\mathbb{N}$ we say
that $i$ is true for $f$ when $f(k)>f(i)$ for all $k>i$. It is easy to see
that there exist infinitely many $i$ which are true for $f$. If $i$ is not
true for $f$, i.e. if $f(k)<f(i)$ for some $k>i$, we say that $i$ is false for
$f$. Moreover, we say that $i$ is true for $f$ at stage $s$ if $f(k)>f(i)$
whenever $i<k<s$, and that $i$ is false for $f$ at stage $s$ if $f(k)<f(i)$
for some $k$ with $i<k<s$. If the injective function $f$ is fixed, we omit
“for $f$” from this terminology.

The following Proposition is well-known (see e.g. the discussion after
Definition 4.1 in [FHM+16]).

######  Proposition 5.2 ($\mathsf{RCA}_{0}$).

The following are equivalent:

  1. (1)

$\mathsf{ACA}_{0}$;

  2. (2)

if $f\colon\mathbb{N}\to\mathbb{N}$ is an injective function there exists an
infinite set $T$ such that every $i\in T$ is true for $f$.

######  Theorem 5.3 ($\mathsf{RCA}_{0}$).

The following are equivalent:

  1. (1)

$\mathsf{ACA}_{0}$;

  2. (2)

let $(V,E)$ be a connected graph, triangulated and with no asteroidal triples;
if $a,b,c,d\in V$ are such that $\neg ab\,\bar{Q}\,cd$ and $\neg
ab\,\bar{Q}\,dc$, then there exists a buried subgraph $B\subseteq V$ such that
either $a,b\in B$ or $c,d\in B$, and no subgraph $A\subseteq B$, which
contains either $a,b$ or $c,d$ respectively, is a buried subgraph;

  3. (3)

let $(V,E)$ be a connected closed interval graph; if $(W,Q)$ has more than two
components, then there exists a buried subgraph $B\subseteq V$;

  4. (4)

let $(V,E)$ be a connected closed interval graph; if $(V,E)$ is not uniquely
orderable, then there exists a buried subgraph $B\subseteq V$.

###### Proof.

$(1\Rightarrow 2)$ is Lemma 5.1. The implication $(2\Rightarrow 3)$ is
trivial, while $(3\Rightarrow 4)$ follows directly from Lemma 3.5, which goes
through in $\mathsf{RCA}_{0}$.

To prove $(4\Rightarrow 1)$ we fix an injective function
$f\colon\mathbb{N}\to\mathbb{N}$ and we define (within $\mathsf{RCA}_{0}$) a
connected closed interval graph $(V,E)$ such that $(W,Q)$ has more than two
components. We then prove, arguing in $\mathsf{RCA}_{0}$, that the unique
buried subgraph $B\subseteq V$ codes the (necessarily infinite) set of numbers
which are true for $f$.

We let $V=\\{a,b,k,r\\}\cup\\{x_{i},y_{i}\mid i\in\mathbb{N}\\}$. Beside
making sure that $(V,E)$ is reflexive, the definition of the edge relation is
by stages: at stage $s$ we define $E$ on
$V_{s}=\\{a,b,k,r\\}\cup\\{x_{i},y_{i}\mid i<s\\}\subseteq V$. At stage $0$
let $k$ be adjacent to $a$, $b$ and $r$ (and add no other edges). At stage
$s+1$ we define the vertices adjacent to $x_{s}$ and $y_{s}$ by the following
clauses:

  1. (a)

$a\,E\,x_{s}\,E\,b\,E\,y_{s}$ and $x_{s}\,E\,k\,E\,y_{s}$,

  2. (b)

$x_{s}\,E\,x_{i}$ and $y_{s}\,E\,y_{i}$ for each $i<s$,

  3. (c)

$x_{s}\,E\,y_{i}$ for each $i\leq s$,

  4. (d)

for $i\leq s$, $y_{s}\,E\,x_{i}$ if and only if $i$ is true for $f$ at stage
$s+1$.

It is immediate that $(V,E)$ is connected. To check that it is a closed
interval graph we define a closed interval representation $f_{L},f_{R}:V\to L$
where $(L,<_{L})$ is a dense linear order. The definition of $f_{L}$ and
$f_{R}$ reflects the construction of the graph by stages. At stage $0$ assign
to the members of $V_{0}$ elements of $L$ satisfying

$f_{L}(r)<_{L}f_{L}(k)<_{L}f_{R}(r)<_{L}f_{L}(a)<_{L}f_{R}(a)<_{L}f_{L}(b)<_{L}f_{R}(b)<_{L}f_{R}(k).$

This ensures that we are representing the restriction of the graph to $V_{0}$.

At stage $s+1$, first let $f_{L}(x_{s})=f_{L}(a)$ and $f_{R}(y_{s})=f_{R}(b)$
(since this is done at every stage, we are respecting conditions (a) and (b)).
We thus still need to define $f_{R}(x_{s})$ and $f_{L}(y_{s})$; first of all
we make sure that
$f_{L}(b)<_{L}f_{L}(y_{i})<_{L}f_{L}(y_{s})<_{L}f_{R}(x_{s})<_{L}f_{R}(b)$ for
every $i<s$, so that (c) is also respected. To respect condition (d) as well
we satisfy the following requirements:

  * •

if $i<s$ is true at stage $s+1$, then $f_{R}(x_{s})<_{L}f_{R}(x_{i})$ (which
implies $f_{L}(y_{s})<_{L}f_{R}(x_{i})$);

  * •

if $j<s$ is false at stage $s+1$, then $f_{R}(x_{j})<_{L}f_{L}(y_{s})$.

The existence of $f_{L}(y_{s})<_{L}f_{R}(x_{s})$ with these properties follows
from the density of $L$ and from the fact that if $i<s$ is true at stage $s+1$
and $j<s$ is false at stage $s+1$, then $f_{R}(x_{j})<_{L}f_{R}(x_{i})$. To
see this notice that:

  * •

if $i<j$, then $i$ was also true at stage $j+1$ and we set
$f_{R}(x_{j})<_{L}f_{R}(x_{i})$ then;

  * •

if $j<i$, then $j$ was already false at stage $i+1$ (if $j$ was true at stage
$i+1$, then $f(j)<f(i)$, and $i$ would be false at stage $s+1$ because $j$ is
false at that stage), and hence we set
$f_{R}(x_{j})<_{L}f_{L}(y_{i})<_{L}f_{R}(x_{i})$ at that stage.

Figure 5 depicts a sample interval representation following this construction.

$k$$a$$b$$r$$y_{0}$$x_{0}$$y_{1}$$x_{1}$$y_{2}$$x_{2}$$y_{3}$$x_{3}$ Figure 5.
Interval representation of $V_{4}$ in case $1$ (and so $2$) becomes false at
stage $3$.

To check that $(V,E)$ is not uniquely orderable let $\prec_{1}$ be the partial
order induced by the interval representation we just described: $v\prec_{1}u$
if and only if $f_{R}(v)<_{L}f_{L}(u)$. Define $\prec_{2}$ so that $\prec_{1}$
and $\prec_{2}$ coincide on $V\setminus\\{s\\}$ and $u\prec_{2}s$ for all
$u\in V\setminus\\{r,k\\}$. It is immediate that both $\prec_{1}$ and
$\prec_{2}$ are associated to $(V,E)$, and that $\prec_{2}$ is not dual of
$\prec_{1}$.

By (4) there exists a buried subgraph $B\subseteq V$. First of all notice that
$k\in K(B)$ and hence $k\notin B$. Now observe that $r\in B$ implies, using
Conditions (i) and (iii) of Definition 3.1, that either some $x_{n}$ or some
$y_{n}$ belongs to $B$. From there, using Condition (iii) again, it is easy to
see that $B=V\setminus\\{k\\}$ and hence $R(B)=\emptyset$, contradicting
Condition (ii). Thus $r\notin B$. Then, in order to satisfy Condition (i), we
must have either $a,b\in B$ or $a,y_{n}\in B$ or $x_{m},y_{n}\in B$, for some
$n$ and some $m$ which is false at stage $n+1$. In any case we have $a\in B$:
in the first two cases this is obvious, and in the latter case this follows
from Condition (iii) because $a\,E\,x_{m}$ and $\neg a\,E\,y_{n}$ for every
$n$ and $m$. But then, using $b\,E\,y_{n}$ and $\neg b\,E\,a$ we obtain $b\in
B$ even in the second and third case. Thus we can conclude that $a,b\in B$.
For each $n$ we have $y_{n}\,E\,b$ and $\neg y_{n}\,E\,a$ and therefore
$y_{n}\in B$. Since $b\,E\,x_{n}\,E\,a$ for each $n\in\mathbb{N}$, then either
$x_{n}\in K(B)$ or $x_{n}\in B$ depending whether $x_{n}$ is adjacent to every
$y_{m}$ or not, namely whether $n$ is true or false for $f$. Therefore we
showed

$B=\\{a,b\\}\cup\\{y_{n}\mid n\in\mathbb{N}\\}\cup\\{x_{n}\mid n\text{ is
false}\\},$

so that $K(B)=\\{k\\}\cup\\{x_{n}\mid n\text{ is true}\\}$ and $R(B)=\\{r\\}$.
Then $T=\\{n\mid x_{n}\notin B\\}$ is the (necessarily infinite) set of all
$n$ which are true for $f$. ∎

## References

  * [FC19] Marta Fiori-Carones.  Filling cages. Reverse mathematics and combinatorial principles.  PhD thesis, Università di Udine, Italy, 2019.
  * [FHM+16] Emanuele Frittaion, Matthew Hendtlass, Alberto Marcone, Paul Shafer, and Jeroen Van der Meeren.  Reverse mathematics, well-quasi-orders, and Noetherian spaces.  Archive for Mathematical Logic, 55(3-4):431–459, 2016.
  * [Fis70] Peter C Fishburn.  Intransitive indifference with unequal indifference intervals.  Journal of Mathematical Psychology, 7(1):144–149, 1970.
  * [Fis85] Peter C. Fishburn.  Interval Orders and Interval Graphs.  Wiley, 1985.
  * [Han82] Philip Hanlon.  Counting interval graphs.  Transactions of the American Mathematical Society, 272(2):383–426, 1982.
  * [Hir87] Jeffry L. Hirst.  Combinatorics in Subsystems of Second Order Arithmetic.  PhD thesis, The Pennsylvania State University, 1987.
  * [Hir15] Denis R. Hirschfeldt.  Slicing the Truth.  World Scientific, 2015.
  * [LB62] Cornelis J. Lekkerkerker and Johan C. Boland.  Representation of a finite graph by a set of intervals on the real line.  Fundamenta Mathematicae, 51:45–64, 1962.
  * [Mar07] Alberto Marcone.  Interval orders and reverse mathematics.  Notre Dame Journal of Formal Logic, 48:425–448, 2007.
  * [Sch05] James H. Schmerl.  Reverse mathematics and graph coloring: eliminating diagonalization.  In S. Simpson, editor, Reverse Mathematics 2001, volume 21 of Lecture Notes in Logic, pages 331–348. Association of Symbolic Logic, La Jolla, CA, 2005.
  * [Sim09] Stephen G. Simpson.  Subsystems of Second Order Arithmetic.  Cambridge University Press, second edition, 2009.
  * [Tro97] William T. Trotter.  New perspectives on interval orders and interval graphs.  In Surveys in combinatorics, 1997 (London), volume 241 of London Math. Soc. Lecture Note Ser., pages 237–286. Cambridge Univ. Press, Cambridge, 1997.
  * [Wie14] Norbert Wiener.  A contribution to the theory of relative position.  Proc. Camb. Philos. Soc., 17:441–449, 1914.