\cline{2-2}\cr\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small$\times_{\beta}$}&\Theta\vdash\forall
x\in b\,.\,\varphi[t_{1}/z],\Delta\\\ \cline{2-2}\cr&\Theta\vdash\forall x\in
b\,.\,\varphi[\pi_{1}(\langle t_{1},t_{2}\rangle)/z],\Delta\end{array}$ (20)

Assuming $x\neq z$ it holds that

$\displaystyle\varphi[t_{1}/z,y/x]=\varphi[y/x,t_{1}[y/x]/z]$ (21)
$\displaystyle\varphi[y/x,\pi_{1}(\langle
t_{1},t_{2}\rangle)[y/x]/z]=\varphi[\pi_{1}(\langle
t_{1},t_{2}\rangle)/z,y/x]$ (22)

and thus (20) becomes

$\begin{array}[]{rc}\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small$\times_{\beta}$}&\Theta,y\in
b\vdash\varphi[y/x,t_{1}[y/x]/z],\Delta\\\
\cline{2-2}\cr\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small$\forall$}&\Theta,y\in
b\vdash\varphi[\pi_{1}(\langle t_{1},t_{2}\rangle)/z,y/x],\Delta\\\
\cline{2-2}\cr&\Theta\vdash\forall x\in b\,.\,\varphi[\pi_{1}(\langle
t_{1},t_{2}\rangle)/z],\Delta\end{array}$ (23)

In (23) the $\times_{\beta}$ inference viewed top-down replaces occurrences of
$t_{1}[y/x]$, which, in case $t_{1}=x$ is $y$, with $\pi_{1}(\langle
t_{1},t_{2}\rangle)[y/x]$. Justified by (22), the middle sequent is in (23)
shown in the form suitable as premise for the application of $\forall$.

In the cases considered so far for permuting $\forall$ down over
$\times_{\beta}$ we assumed $x\neq z$. It remains to consider the case $x=z$.
By Remark 35, since $x$ is bound in $\varphi$, the $\times_{\beta}$ inference
can not have any effect on $\varphi$. The given deduction (19) then
specializes to

$\begin{array}[]{rc}\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small$\forall$}&\Theta[t_{1}/x],y\in
b[t_{1}/x]\vdash\varphi[y/x],\Delta[t_{1}/x]\\\
\cline{2-2}\cr\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small$\times_{\beta}$}&\Theta[t_{1}/x]\vdash\forall
x\in b[t_{1}/x]\,.\,\varphi,\Delta[t_{1}/x]\\\
\cline{2-2}\cr&\Theta[\pi_{1}(\langle t_{1},t_{2}\rangle)/x]\vdash\forall x\in
b[\pi_{1}(\langle t_{1},t_{2}\rangle)/x]\,.\,\varphi,\Delta[\pi_{1}(\langle
t_{1},t_{2}\rangle)/x]\end{array}$ (24)

Given that $y\neq x$, it holds that

$\displaystyle\varphi[y/x]=\varphi[y/x,t/x]$

and thus (24) becomes

$\begin{array}[]{rc}\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small$\times_{\beta}$}&\Theta[t_{1}/x],y\in
b[t_{1}/x]\vdash\varphi[y/x,t_{1}/x],\Delta[t_{1}/x]\\\
\cline{2-2}\cr\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small$\forall$}&\Theta[\pi_{1}(\langle
t_{1},t_{2}\rangle)/x],y\in b[\pi_{1}(\langle
t_{1},t_{2}\rangle)/x]\vdash\varphi[y/x],\Delta[\pi_{1}(\langle
t_{1},t_{2}\rangle)/x]\\\ \cline{2-2}\cr&\Theta[\pi_{1}(\langle
t_{1},t_{2}\rangle)/x]\vdash\forall x\in b[\pi_{1}(\langle
t_{1},t_{2}\rangle)/x]\,.\,\varphi,\Delta[\pi_{1}(\langle
t_{1},t_{2}\rangle)/x]\end{array}$ (25)

This concludes the specification of permuting $\forall$ down over
$\times_{\beta}$ and thus the specification of all permutation schemas
required for step 2 of the ${\mathsf{EL}}$-normalization procedure (Fig. 4).

###  G.3. Conversion to tuple-terms

That term $t$ in instances of the $\exists$ rule is always a tuple-term, i.e.,
does not involve the projection functions $\pi_{1}$ and $\pi_{2}$, is ensured
by a proof transformation where instances of $\times_{\eta}$ and
$\times_{\beta}$ are inserted below instances of $\exists$. The effects of
these interspersed rules are then propagated upwards. The following lemma
states the desired overall property of this transformation.

######  Lemma 36.

A $\Delta_{0}$ formula provable in the base calculus with a proof where the
${\mathsf{EL}}$ requirements of the ${\mathsf{EL}}$-normalized calculus of
Fig. 3 are met (but not necessarily its tuple-term condition of the $\exists$
rule) is also provable in the ${\mathsf{EL}}$-normalized calculus.

Lemma 36 presupposes a proof whose contexts and sequents meet the
${\mathsf{EL}}$ requirements of the ${\mathsf{EL}}$-normalized calculus. The
claimed tuple-term condition can be achieved by exhaustively applying the
proof transformations $\mathit{Elim}\text{-}\pi\text{-}\mathit{var}$ and
$\mathit{Elim}\text{-}\pi\text{-}\mathit{pair}$, specified below, which are
applicable whenever there is an occurrence of $\pi_{1}$ or $\pi_{2}$ in the
term $t$ of an instance of the $\exists$ rule. These transformations lead from
a legal proof in the base calculus to another one with the same bottom
formula. They require and preserve the ${\mathsf{EL}}$ requirements from the
${\mathsf{EL}}$-normalized calculus.

#### Proof transformation $\mathit{Elim}\text{-}\pi\text{-}\mathit{var}$

This transformation applies to an instance of the $\exists$ rule whose term
$t$ has an occurrence of $\pi_{1}(z)$ or $\pi_{2}(z)$, where $z$ is a
variable. The instance of the $\exists$ rule is replaced with an instance of
$\exists$ followed by an instance of $\times_{\eta}$ and the subproof above is
adjusted, according to the following schema.

$\small\begin{array}[]{rc}&P\\\\[-3.87498pt]
&{\footnotesize\begin{array}[]{rcl}.&.&\;\;\;\;.\\\\[-6.2pt]
.&.&\;\;\;.\\\\[-6.2pt] .&.&\;\;.\\\\[-6.2pt] .&.&\;.\\\\[-6.2pt]
.&.&.\\\\[-6.2pt] &.&\end{array}}\\\
\raisebox{-7.74997pt}[0.0pt][0.0pt]{\small$\exists$}&\Theta,t\in
b\vdash\varphi[t/x],\exists x\in b\;\varphi,\Delta_{\mathsf{EL}}\\\
\cline{2-2}\cr&\Theta,t\in b\vdash\exists x\in
b\,.\,\varphi,\Delta_{\mathsf{EL}}\end{array}\;\textrm{ is replaced by
}\;\begin{array}[]{rc}&P^{*}\\\\[-3.87498pt]
&{\footnotesize\begin{array}[]{rcl}.&.&\;\;\;\;.\\\\[-6.2pt]
.&.&\;\;\;.\\\\[-6.2pt] .&.&\;\;.\\\\[-6.2pt] .&.&\;.\\\\[-6.2pt]
.&.&.\\\\[-6.2pt] &.&\end{array}}\\\
\raisebox{-7.74997pt}[0.0pt][0.0pt]{\small$\exists$}&\Theta^{*},t^{*}\in
b^{*}\vdash\varphi^{*}[t^{*}/x],\exists x\in
b^{*}\;\varphi,\Delta^{*}_{\mathsf{EL}}\\\
\cline{2-2}\cr\raisebox{-7.74997pt}[0.0pt][0.0pt]{\small$\times_{\eta}$}&\Theta^{*},t^{*}\in
b^{*}\vdash\exists x\in b^{*}\,.\,\varphi^{*},\Delta^{*}_{\mathsf{EL}}\\\
\cline{2-2}\cr&\Theta,t\in b\vdash\exists x\in
b\,.\,\varphi,\Delta_{\mathsf{EL}}\end{array}$

The starred components are specified there as follows: For a term, formula or
multiset of formulas $\Gamma$, $\Gamma^{*}$ stands for $\Gamma[\langle
z_{1},z_{2}\rangle/z]$, where $z_{1},z_{2}$ are fresh variables. Subproof
$P^{*}$ is obtained from $P$ by removing each instance of $\times_{\eta}$ upon
the variable $z$ and some pair $\langle z_{1}^{\prime},z_{2}^{\prime}\rangle$,
while replacing and $z_{1}^{\prime}$ with $z_{1}$ and of $z_{2}^{\prime}$ with
$z_{2}$, and then replacing all occurrences of $z$ with $\langle
z_{1},z_{2}\rangle$.

#### Proof transformation $\mathit{Elim}\text{-}\pi\text{-}\mathit{pair}$.

This transformation applies to an instance of the $\exists$ rule whose term
$t$ has an occurrence of $\pi_{1}(\langle t_{1},t_{2}\rangle)$ (the case for
$\pi_{2}(\langle t_{1},t_{2}\rangle)$ is analogous). The instance of the
$\exists$ rule is replaced with an instance of $\exists$ followed by an
instance of $\times_{\beta}$ and the subproof above is adjusted, according to
the following schema.

$\small\begin{array}[]{rc}&P\\\\[-3.87498pt]
&{\footnotesize\begin{array}[]{rcl}.&.&\;\;\;\;.\\\\[-6.2pt]
.&.&\;\;\;.\\\\[-6.2pt] .&.&\;\;.\\\\[-6.2pt] .&.&\;.\\\\[-6.2pt]
.&.&.\\\\[-6.2pt] &.&\end{array}}\\\
\raisebox{-7.74997pt}[0.0pt][0.0pt]{\small$\exists$}&\Theta,t\in
b\vdash\varphi[t/x],\exists x\in b\;\varphi,\Delta_{\mathsf{EL}}\\\
\cline{2-2}\cr&\Theta,t\in b\vdash\exists x\in
b\,.\,\varphi,\Delta_{\mathsf{EL}}\end{array}\;\textrm{ is replaced by
}\;\begin{array}[]{rc}&P^{\prime}\\\\[-3.87498pt]
&{\footnotesize\begin{array}[]{rcl}.&.&\;\;\;\;.\\\\[-6.2pt]
.&.&\;\;\;.\\\\[-6.2pt] .&.&\;\;.\\\\[-6.2pt] .&.&\;.\\\\[-6.2pt]
.&.&.\\\\[-6.2pt] &.&\end{array}}\\\
\raisebox{-7.74997pt}[0.0pt][0.0pt]{\small$\exists$}&\Theta,t^{\prime}\in
b\vdash\varphi[t^{\prime}/x],\exists x\in b\;\varphi,\Delta_{\mathsf{EL}}\\\
\cline{2-2}\cr\raisebox{-7.74997pt}[0.0pt][0.0pt]{\small$\times_{\beta}$}&\Theta,t^{\prime}\in
b\vdash\exists x\in b\,.\,\varphi,\Delta_{\mathsf{EL}}\\\
\cline{2-2}\cr&\Theta,t\in b\vdash\exists x\in
b\,.\,\varphi,\Delta_{\mathsf{EL}}\end{array}$

The primed components are specified there as follows: Term $t^{\prime}$ is $t$
with the occurrence of $\pi_{1}(\langle t_{1},t_{2}\rangle)$ replaced by
$t_{1}$. Subproof $P^{\prime}$ is $P$ with that replacement propagated upward.
It may be obtained by performing the inference steps of $P$ in upward
direction, but now starting from $\Theta,t^{\prime}\in
b\vdash\varphi[t^{\prime}/x],\exists x\in b\;\varphi,\Delta_{\mathsf{EL}}$
instead of $\Theta,t\in b\vdash\varphi[t/x],\exists x\in
b\;\varphi,\Delta_{\mathsf{EL}}$. Instances of $\times_{\beta}$ and
$\times_{\eta}$ may get void there (identical premise and conclusion) and can
then be removed.

###  G.4. Complexity considerations

In step 1 of the ${\mathsf{EL}}$-normalization procedure (Fig. 4), through the
two-premise rule $\land$ a leaf can get extended upwards by a number of nodes
that is exponential in the number of occurrences of $\land$ in its conclusion.
Hence the time required for step 1 is exponential in the number of occurrences
of $\land$ in a leaf conclusion.

Step 2 where the proof is permuted, may, through permuting $\land$ down over
one-premise rules, increase the number of nodes. However, none of the
permutations does increase the height $h$ and the number of leaves $l$ of the
proof tree. Both $h$ and $l$ are less than or equal to the number $n$ of nodes
of the input proof, the output of step 1. Since a tree with height $h$ and
number of leaves $l$ can in general not have more that $h*l$ nodes, our proof
tree during performing the permutations can never have more than $n^{2}$
nodes. Since for each node we can apply at most $h$ downward permutation
steps, and $h\leq n$, we can conclude that step 2 involves not more that
$n^{3}$ permutation steps.

Step 3, where instances of $\times_{\eta}$ and $\times_{\beta}$ are inserted
below instances of $\exists$ and the above subproof is adjusted to these
insertions is polynomial. This step does not increase the number of branches
but may increase the length of a branch by twice the number of occurrences of
$\pi_{i}$ in terms $t$ of instances of $\exists$ on the branch.

Thus, for ${\mathsf{EL}}$-normalization we have exponential time complexity,
where, however the source of the exponential characteristics can be associated
with the first stage of the procedure, extending the proof tree at its leaves,
which may be seen in essence as a blow up of _irrelevant_ parts of the proof
that accompany the axioms. The gist of the method, the rule permutation stage,
is only a polynomial-time operation.

##  Appendix H $\Delta_{0}$ interpolation: proof sketch of Theorem 18

We recall the statement:

Let $\Theta$ be an $\in$-context and $\Gamma,\Delta$ finite multisets of
$\Delta_{0}$ formulas. Then from any proof of $\Theta;\;\Gamma\vdash\Delta$ we
can compute in linear time a $\Delta_{0}$ formula $\theta$ with
$FV(\theta)\subseteq FV(\Theta,\Gamma)\cap FV(\Delta)$, such that
$\Theta;\;\Gamma\vdash\theta$ and $\emptyset;\;\theta\vdash\Delta$

Recall also that we claim this for both the higher-level $2$-sided system and
the $1$-sided system, where the $2$-sided syntax is a “macro”:
$\Theta;\;\Gamma\vdash\Delta$ is a shorthand for
$\Theta\vdash\neg\Gamma,\Delta$, where $\neg\Gamma$ is itself a macro for
dualizing connectives. Thus in the $1$-sided version, we are arbitrarily
classifying some of the $\Delta_{0}$ formulas as Left and the others as Right,
and our interpolant must be common according to that partition.

We stress that there are no new ideas needed in proving Theorem 18 — unlike
for our main tool, the Parameter Collection Theorem, or our final result. The
construction for Theorem 18 proceeds exactly as in prior interpolation
theorems for similar calculi [Tak87, TS00, Smu68b]. Similar constructions are
utilized in works for query reformulation in databases, so for a presentation
geared towards a database audience one can check [TW11] or the later [BCLT16].

We explain the argument for the higher-level $2$-sided system. We prove a more
general statement, where we partition the context and the formulas on both
sides of $\vdash$ into Left and Right. So we have

$\Theta_{L}\Theta_{R};\Gamma_{L},\Gamma_{R}\vdash\Delta_{L},\Delta_{R}$

And our inductive invariant is that we will compute in linear time a $\theta$
such that:

$\displaystyle\Theta_{L};\Gamma_{L}\vdash\theta,\Delta_{L}$
$\displaystyle\Theta_{R};\Gamma_{R},\theta\vdash\Delta_{R}$

And we require that $FV(\theta)\subseteq
FV(\Theta_{L},\Gamma_{L},\Delta_{L})\cap
FV(\Theta_{R},\Gamma_{R},\Delta_{R})$. This generalization is used to handle
the negation rules, as we explain below.

We proceed by induction on the depth of the proof tree.

One of the base cases is where we have a trivial proof tree, which uses rule
(Ax) to derive:

$\Theta;\Gamma,\varphi\vdash\varphi,\Delta$

We do a case distinction on where the occurrences of $\varphi$ sit in our
partition. Assume the occurrence on the left is in $\Gamma_{L}$ and the
occurrence on the right is in $\Delta_{R}$. Then we can take our interpolant
$\theta$ to be $\varphi$. Suppose the occurrence on the left is $\Gamma_{L}$
and the occurrence on the right is in $\Delta_{L}$. Then we can take $\theta$
to be $\bot$. The other base cases are similar.

The inductive cases for forming the interpolant will work “in reverse” for
each proof rule. That is, if we used an inference rule to derive sequent $S$
from sequents $S_{1}$ and $S_{2}$, we will partition the sequents $S_{1}$ and
$S_{2}$ based on the partition of $S$. We will then apply induction to our
partitioned sequent for $S_{1}$ to get an interpolant $\theta_{1}$, and also
apply induction to our partitioned version of $S_{2}$ to get an interpolant
$\theta_{2}$. We then put them together to get the interpolant for the
partitioned sequent $S$. This “putting together” will usually reflect the
semantics of the connective mentioned in the proof rule.

Consider the case where the last rule applied is the $\neg$-L rule: this is
the case that motivates the more general invariant involving partitions. We
have a partition of the final sequent $\Theta;\Gamma,\varphi\vdash\Delta$. We
form a partition of the sequent $\Theta;\Gamma\vdash\neg\varphi,\Delta$ by
placing $\neg\varphi$ on the same side (Left, Right) as $\varphi$ was in the
original partition. We then get an interpolant $\theta$ by induction. We just
use $\theta$ for the final interpolant.

We consider the inductive case for $\wedge$-R. We have two top sequents, one
for each conjunct. We partition them in the obvious way: each $\varphi_{i}$ in
the top is in the same partition that $\varphi_{1}\wedge\varphi_{2}$ was in
the bottom. Inductively we take the interpolants $\theta_{1}$ and $\theta_{2}$
for each sequent. We again do a case analysis based on whether
$\varphi_{1}\wedge\varphi_{2}$ was in $\Delta_{L}$ or in $\Delta_{R}$.

Suppose $\varphi_{1}\wedge\varphi_{2}$ was in $\Delta_{R}$, so
$\Delta_{R}=\varphi_{1}\wedge\varphi_{2},\Delta^{\prime}_{R}$. Then we
arranged that each $\varphi_{i}$ was in $\Delta_{R}$ in the corresponding top
sequent. So we know that $\Theta_{L};\Gamma_{L}\vdash\theta_{i},\Delta_{L}$
and $\Theta_{R};\Gamma_{R},\theta_{i}\vdash\varphi_{i},\Delta^{\prime}_{R}$
for $i=1,2$. Now we can set the interpolant $\theta$ to be
$\theta_{1}\wedge\theta_{2}$.

In the other case, $\varphi_{1}\wedge\varphi_{2}$ was in $\Delta_{L}$, say
$\Delta_{L}=\varphi_{1}\wedge\varphi_{2},\Delta^{\prime}_{L}$. Then we would
arrange each $\varphi_{i}$ to be “Left” in the corresponding top sequent, so
we know that
$\Theta_{L};\Gamma_{L}\vdash\theta_{i},\varphi_{i},\Delta^{\prime}_{L}$ and
$\Theta_{R};\Gamma_{R},\theta_{i}\vdash\Delta_{R}$ for $i=1,2$. We set
$\theta=\theta_{1}\vee\theta_{2}$ in this case.

With the $\exists$ rule, a term in the inductively-assumed $\theta^{\prime}$
for the top sequent may become illegal for the $\theta$ for the bottom
sequent, since it has a free variable that is not common. In this case, the
term in $\theta$ is replaced by a quantified variable, where the quantifier is
existential or universal, depending on the partitioning, and bounded according
to the requirements for $\Delta_{0}$ formulas. The non-common variables are
then replaced and variable constraints are added as described with the
notation $\exists x_{1}\ldots x_{n}|t\in b\,.\,\varphi$ and $\forall
x_{1}\ldots x_{n}|t\in b\,.\,\varphi$ on p. 5.2.3.

##  Appendix I Proofs of polytime admissibility

The goal of this section is to prove most claims of polytime admissibility
made in the body of the paper, crucially those of Subsection 5.3. Recall that
a rule

$\dfrac{\Theta\vdash\Delta}{\Theta^{\prime}\vdash\Delta^{\prime}}$

is _polytime admissible_ if we can compute in polynomial time a proof of the
conclusion $\Theta^{\prime}\vdash\Delta^{\prime}$ from a proof of the
antecedent $\Theta\vdash\Delta$.

Throughout this section we deal with the ${\mathsf{EL}}$-normalized proof
system of Figure 3.

###  I.1. Standard rules

Here we collect some useful standard sequent calculi rules, which are all
polytime admissible in our system. The arguments for these rules are
straightforward.

######  Lemma 37.

The following weakening rule is polytime admissible:

$\dfrac{\Theta\vdash\Delta}{\Theta^{\prime}\vdash\Delta,\Delta^{\prime}}$

######  Lemma 38.

The following inference, witnessing the invertibility of the $\wedge$ rule, is
polytime admissible for both $i\in\\{1,2\\}$:

$\dfrac{\Theta\vdash\varphi_{1}\wedge\varphi_{2},\Delta}{\Theta\vdash\varphi_{i},\Delta}$

######  Lemma 39.

The following, witnessing the invertibility of the $\forall$ rule, is polytime
admissible:

$\dfrac{\Theta\vdash\forall x\in t.\varphi,\Delta}{\Theta,x\in
t\vdash\varphi,\Delta}$

######  Lemma 40.

The following generalization of the $\exists$ rule is polytime admissible:

$\dfrac{\Theta,\Theta_{2}\vdash\varphi^{\prime},\varphi,\Delta^{\mathsf{EL}}\quad\text{$\varphi^{\prime}$
is a spec~{}of $\varphi$ wrt an ordering of
$\Theta_{2}$}}{\Theta,\Theta_{2}\vdash\varphi,\Delta^{\mathsf{EL}}}$

######  Lemma 41.

The following substitution rule is polytime admissible:

$\dfrac{\Theta\vdash\Delta}{\Theta[t/x]\vdash\Delta[t/x]}$

###  I.2. Admissibility of generalized congruence

Recall the admissibility claim concerning the rule related to congruence:

######  Lemma 42.

The following generalized congruence rule is polytime admissible:

$\dfrac{\Theta[t/x,t/y]\vdash\Delta[t/x,t/y]}{\Theta[t/x,u/y]\vdash\neg(t\equiv
u),\Delta[t/x,u/y]}$

Recall that in a two-sided reading of this, the hypothesis is $t\equiv
u;\Theta[t/x,u/y]\vdash\Delta[t/x,u/y]$. So the rule says that if we $\Theta$
entails $\Delta$ where both contain $t$, then if we assume $t\equiv u$ and
substitute some occurrences of $t$ with $u$ in $\Theta$, we can conclude the
corresponding substitution of $\Delta$.

To prove Lemma 42 in the case where the terms $t$ and $u$ are of type ${\sf
Set}(T)$, we will need a more general statement. We are going to generalize
the statement to treat tuples of terms and use ${\mathsf{EL}}$ formulas
instead of $\neg(t\equiv u)$ to simplify the inductive invariant.

Given two terms $t$ and $u$ of type $t$, define by induction the set of
formulas $\mathcal{E}_{t,u}$:

  * •

If $T=\mathfrak{U}$, then $\mathcal{E}_{t,u}$ is $t\neq_{\mathfrak{U}}u$

  * •

If $T=T_{1}\times T_{2}$, then $\mathcal{E}_{t,u}$ is
$\mathcal{E}_{\pi_{1}(t),\pi_{1}(u)},\mathcal{E}_{\pi_{2}(t),\pi_{2}(u)}$

  * •

If $T={\sf Set}(T^{\prime})$, $\mathcal{E}_{t,u}$ is
$\neg(t\subseteq_{T}u),\neg(u\subseteq_{T}t)$

The reader can check that $\mathcal{E}_{t,u}$ is essentially $\neg(t\equiv
u)$.

######  Lemma 43.

The following rule is polytime admissible:

$\dfrac{\Theta\vdash\Delta,\mathcal{E}_{t,u}}{\Theta\vdash\Delta,\neg(t\equiv
u)}$

######  Proof I.1.

Straightforward induction over $T$.

Since we will deal with multiple equivalences, we will adopt vector notation
$\vec{t}=t_{1},\ldots,t_{n}$ and $\vec{x}=x_{1},\ldots,x_{n}$ for lists of
terms and variables. Call $\mathcal{E}_{\vec{t},\vec{u}}$ the union of the
$\mathcal{E}_{t_{i},u_{i}}$. We can now state our more general lemma:

######  Lemma 44.

The following generalized $n$-ary congruence rule for set variables is
polytime admissible:

$\dfrac{\Theta[\vec{t}/\vec{x},\vec{t}/\vec{y}]\vdash\Delta[\vec{t}/\vec{x},\vec{t}/\vec{y}]}{\Theta[\vec{t}/\vec{x},\vec{u}/\vec{y}]\vdash\Delta[\vec{t}/\vec{x},\vec{u}/\vec{y}],\mathcal{E}_{\vec{t},\vec{u}}}$

######  Proof I.2 (Proof of Lemma 44).

We proceed by induction over the proof of
$\Theta[\vec{t}/\vec{x},\vec{t}/\vec{y}]\vdash\Delta[\vec{t}/\vec{x},\vec{u}/\vec{y}]$,

  * •

If the last rule applied is the $=$ rule, i.e. we have

$\dfrac{}{\Theta[\vec{t}/\vec{x},\vec{t}/\vec{y}]\vdash
a[\vec{t}/\vec{x},\vec{t}/\vec{y}]=_{\mathfrak{U}}b[\vec{t}/\vec{x},\vec{t}/\vec{y}],\Delta[\vec{t}/\vec{x},\vec{t}/\vec{y}]}$

and $a[\vec{t}/\vec{x},\vec{t}/\vec{y}]=b[\vec{t}/\vec{x},\vec{t}/\vec{y}]$,
with $a,b$ variables. Now if $a$ and $b$ are equal, or if they belong both to
either $\vec{x}$ or $\vec{y}$, it is easy to derive the desired conclusion
with a single application of the $=$ rule. Otherwise, assume $a=x_{i}$ and
$b=y_{j}$ (the symmetric case is handled similarly). In such a case, we have
that $\mathcal{E}_{\vec{t},\vec{u}}$ contains $t_{i}\neq_{\mathfrak{U}}t_{j}$.
So the desired proof

$\dfrac{}{\Theta[\vec{t}/\vec{x},\vec{t}/\vec{y}]\vdash
t_{i}=_{\mathfrak{U}}u_{j},\Delta[\vec{t}/\vec{x},\vec{t}/\vec{y}],\mathcal{E}_{\vec{t},\vec{u}},t_{i}\neq_{\mathfrak{U}}t_{j}}$

follows from the polytime admissibility of the axiom rule.

  * •

Suppose the last rule applied is the $\top$ rule:

$\dfrac{}{\Theta[\vec{t}/\vec{x},\vec{t}/\vec{y}]\vdash\top,\Delta[\vec{t}/\vec{x},\vec{t}/\vec{y}]}$

Then we do not need to apply the induction hypothesis. Instead we can
immediately apply the $\top$ rule to obtain

$\dfrac{}{\Theta[\vec{t}/\vec{x},\vec{u}/\vec{y}]\vdash\top,\Delta[\vec{t}/\vec{x},\vec{u}/\vec{y}],\mathcal{E}_{\vec{t},\vec{u}}}$

  * •

If the last rule applied is the $\wedge$ rule

$\dfrac{\Theta[\vec{t}/\vec{x},\vec{t}/\vec{y}]\vdash\varphi_{1}[\vec{t}/\vec{x},\vec{t}/\vec{y}],\Delta[\vec{t}/\vec{x},\vec{t}/\vec{y}]\qquad\Theta[\vec{t}/\vec{x},\vec{t}/\vec{y}]\vdash\varphi_{2}[\vec{t}/\vec{x},\vec{t}/\vec{y}],\Delta[\vec{t}/\vec{x},\vec{t}/\vec{y}]}{\Theta[\vec{t}/\vec{x},\vec{t}/\vec{y}]\vdash(\varphi_{1}\wedge\varphi_{2})[\vec{t}/\vec{x},\vec{t}/\vec{y}],\Delta[\vec{t}/\vec{x},\vec{t}/\vec{y}]}$

then the induction hypothesis gives us proofs of

$\Theta[\vec{t}/\vec{x},\vec{u}/\vec{y}]\vdash\varphi_{i}[\vec{t}/\vec{x},\vec{u}/\vec{y}],\Delta[\vec{t}/\vec{x},\vec{u}/\vec{y}],\mathcal{E}_{\vec{t},\vec{u}}$

for both $i\in\\{1,2\\}$. So we can apply the $\wedge$ rule to conclude that
we have

$\Theta[\vec{t}/\vec{x},\vec{u}/\vec{y}]\vdash(\varphi_{1}\wedge\varphi_{2})[\vec{t}/\vec{x},\vec{u}/\vec{y}],\Delta[\vec{t}/\vec{x},\vec{u}/\vec{y}],\mathcal{E}_{\vec{t},\vec{u}}$

as desired.

  * •

The cases of the rules $\vee$,$\forall$ and $\times_{\eta}$ are equally
straightforward and left to the reader.

  * •

Now, let us handle the case of the $\exists$ rule. To simplify notation, we
just treat the case where there is only one leading existential in the
formula.

$\dfrac{\Theta,t\in u\vdash\varphi[t/x],\Delta^{\mathsf{EL}}}{\Theta,t\in
u\vdash\exists x\in u.\;\varphi,\Delta^{\mathsf{EL}}}$

The generalization to multiple existentials can be obtained by translating the
general $\exists$ rule into a sequence of applications of the rule above and
applying the same argument to each instance.

So assume that $z$ is fresh wrt $\vec{x},\vec{y},\vec{t},\vec{u},a,b$ and that
the last step of the proof is

$\dfrac{\Theta[\vec{t}/\vec{x},\vec{t}/\vec{y}],a[\vec{t}/\vec{x},\vec{t}/\vec{y}]\in
b[\vec{t}/\vec{x},\vec{t}/\vec{y}]\vdash\varphi[a/z][\vec{t}/\vec{x},\vec{t}/\vec{y}],\exists
z\in
c[\vec{t}/\vec{x},\vec{t}/\vec{y}].\;\varphi[\vec{t}/\vec{x},\vec{t}/\vec{y}],\Delta[\vec{t}/\vec{x},\vec{t}/\vec{y}]}{\Theta[\vec{t}/\vec{x},\vec{t}/\vec{y}],a[\vec{t}/\vec{x},\vec{t}/\vec{y}]\in
b[\vec{t}/\vec{x},\vec{t}/\vec{y}]\vdash\exists z\in
c[\vec{t}/\vec{x},\vec{t}/\vec{y}].\;\varphi[\vec{t}/\vec{x},\vec{t}/\vec{y}],\Delta[\vec{t}/\vec{x},\vec{t}/\vec{y}]}$

with $b[\vec{t}/\vec{x},\vec{t}/\vec{y}]=c[\vec{t}/\vec{x},\vec{t}/\vec{y}]$.
Set $a^{\prime}=a[\vec{t}/\vec{x},\vec{u}/\vec{y}]$,
$b^{\prime}=b[\vec{t}/\vec{x},\vec{u}/\vec{y}]$,
$c^{\prime}=c[\vec{t}/\vec{x},\vec{u}/\vec{y}]$. We have three subcases:

    * –

If we have that $b^{\prime}=c^{\prime}$, using the induction hypothesis, we
have a proof of

$\Theta[\vec{t}/\vec{x},\vec{u}/\vec{y}],a^{\prime}\in
b^{\prime}\vdash\varphi[a/z][\vec{t}/\vec{x},\vec{u}/\vec{y}],\exists z\in
c^{\prime}.\;\varphi[\vec{u}/\vec{x},\vec{u}/\vec{y}],\Delta[\vec{t}/\vec{x},\vec{u}/\vec{y}],\mathcal{E}_{\vec{t},\vec{u}}$

we can simply apply an $\exists$ rule to that proof and we are done.

    * –

Otherwise, if we have that $b^{\prime}=t_{i}$ and $c^{\prime}=u_{j}$ for some
$i,j\leq n$. In that case, extending the tuples $\vec{t}$ and $\vec{u}$ with
$a^{\prime}$ and a fresh variable $z^{\prime}$ (the substitutions under
consideration would be, we can apply the induction hypothesis to obtain a
proof of

$\displaystyle\Theta[\vec{t}/\vec{x},\vec{u}/\vec{y},a^{\prime}/z],a^{\prime}\in
t_{i},z^{\prime}\in u_{j}\vdash$
$\displaystyle\varphi[\vec{t}/\vec{x},\vec{u}/\vec{y},z^{\prime}/z],\exists
z\in
u_{j}.\;\varphi[\vec{u}/\vec{x},\vec{u}/\vec{y}],\Delta[\vec{t}/\vec{x},\vec{u}/\vec{y}],\mathcal{E}_{\vec{t},\vec{u}},\mathcal{E}_{a^{\prime},z^{\prime}}$

Note that $\mathcal{E}_{\vec{t},\vec{u}}$ contains an occurrence of
$\neg(t_{i}\subseteq u_{j})$, which expands to $\exists z\in t_{i}.\forall
z^{\prime}\in u_{j}.\neg(z\equiv z^{\prime})$, so we can construct the partial
derivation

$\Theta[\vec{t}/\vec{x},\vec{u}/\vec{y},a^{\prime}/z],a^{\prime}\in
t_{i},z^{\prime}\in
u_{j}\vdash\varphi[\vec{t}/\vec{x},\vec{u}/\vec{y},z^{\prime}/z^{\prime}],\exists
z\in
u_{j}.\;\varphi[\vec{u}/\vec{x},\vec{u}/\vec{y}],\Delta[\vec{t}/\vec{x},\vec{u}/\vec{y}],\mathcal{E}_{\vec{t},\vec{u}},\mathcal{E}_{a^{\prime},z^{\prime}}$
$\exists$ $\Theta[\vec{t}/\vec{x},\vec{u}/\vec{y}],a^{\prime}\in
t_{i},z^{\prime}\in u_{j}\vdash\exists z\in
u_{j}.\varphi[\vec{t}/\vec{x},\vec{u}/\vec{y}],\Delta[\vec{t}/\vec{x},\vec{u}/\vec{y}],\mathcal{E}_{\vec{t},\vec{u}},\mathcal{E}_{a^{\prime},z^{\prime}}$
Lemma 43 $\Theta[\vec{t}/\vec{x},\vec{u}/\vec{y},a^{\prime}/z],a^{\prime}\in
t_{i},z^{\prime}\in u_{j}\vdash\exists z\in
u_{j}.\;\varphi[\vec{u}/\vec{x},\vec{u}/\vec{y}],\Delta[\vec{t}/\vec{x},\vec{u}/\vec{y}],\mathcal{E}_{\vec{t},\vec{u}},a^{\prime}\equiv
z^{\prime}$ $\forall$
$\Theta[\vec{t}/\vec{x},\vec{u}/\vec{y},a^{\prime}/z],a^{\prime}\in
t_{i}\vdash\exists z\in
c^{\prime}.\;\varphi[\vec{u}/\vec{x},\vec{u}/\vec{y}],\Delta[\vec{t}/\vec{x},\vec{u}/\vec{y}],\mathcal{E}_{\vec{t},\vec{u}},\forall
z^{\prime}\in u_{j}.a^{\prime}\equiv z^{\prime}$ $\exists$
$\Theta[\vec{t}/\vec{x},\vec{u}/\vec{y},a^{\prime}/z],a^{\prime}\in
t_{i}\vdash\exists z\in
c^{\prime}.\;\varphi[\vec{t}/\vec{x},\vec{u}/\vec{y}],\Delta[\vec{t}/\vec{x},\vec{u}/\vec{y}],\mathcal{E}_{\vec{t},\vec{u}}$

whose conclusion matches what we want.

    * –

Otherwise, we are in a similar case where $b^{\prime}=u_{j}$ and
$c^{\prime}=t_{i}$. We proceed similarly, except that we use the formula
$\neg(u_{j}\subseteq t_{i})$ of $\mathcal{E}_{t_{i},u_{j}}$ instead of
$\neg(t_{i}\subseteq u_{j})$.

    * –

For the rule $\times_{\beta}$, which has general shape

$\dfrac{\Theta[z_{i}/z]\vdash\Delta[z_{i}/z]}{\Theta[\pi_{i}(\langle
z_{1},z_{2}\rangle)/z]\vdash\Delta[\pi_{i}(\langle z_{1},z_{2}\rangle)/z]}$

we can assume, without loss of generality, that $z$ occurs only once in
$\Theta,\Delta$. Let us only sketch the case where $z$ occurs in a formula
$\varphi$ and the rule has shape

$\dfrac{\Theta\vdash\varphi[z_{i}/z],\Delta}{\Theta\vdash\varphi[\pi_{i}(\langle
z_{1},z_{2}\rangle)/z],\Delta}$

We have that $\varphi[\pi_{i}(\langle z_{1},z_{2}\rangle)/z)]$ is also of the
shape $\psi[\vec{t}/\vec{x},\vec{u}/\vec{y}]$ in our situation. We can also
assume without loss of generality that each variable in $\vec{x}$ and
$\vec{y}$ occur each a single time in $\Theta,\Delta$. Now if we have a couple
of situations:

      * *

If the occurrence of $z$ do not interfere with the substitution
$[\vec{t}/\vec{x},\vec{u}/\vec{y}]$, i.e., there is a formula $\theta$ such
that

$\varphi[\pi_{i}(\langle
z_{1},z_{2}\rangle)/z]=\psi[\vec{t}/\vec{x},\vec{u}]=\theta[\vec{t}/\vec{x},\vec{u}/\vec{y},\langle
z_{1},z_{2}\rangle/z]$

we can simply apply the induction hypothesis on the subproof and conclude with
one application of $\times_{\eta}$.

      * *

If we have that $z$ clashes with a variable of $\vec{x},\vec{y}$, say $x_{j}$,
but that $t_{j}=v[\pi_{i}(\langle z_{1},z_{2}\rangle/x_{j})]$ for some term
$v$. Then we can apply the induction hypothesis with the matching tuples of
terms $\vec{t},x_{i}$ and $\vec{u},t_{i}$ and conclude by applying the $\beta$
rule.

      * *

Otherwise, the occurrence of $z$ does interfere with the substitution in such
a way that we have, say $t_{j}=\langle z_{1},z_{2}\rangle$. Then we can apply
the induction hypothesis on the subproof with the matching tuples of terms
$\vec{x},z_{i}$ and $\vec{y},\pi_{i}(u_{j})$ and conclude by applying the
$\beta$ rule.

One easy consequence of the above is Lemma 42:

######  Proof I.3 (Proof of Lemma 42).

Combine Lemma 44 and Lemma 43.

Another consequence is the following corollary, which will be used later in
this section:

######  Corollary 45.

The following rule is polytime admissible:

$\dfrac{\Theta,t\in u\vdash\Delta}{\Theta\vdash\neg
t\mathrel{\hat{\in}}u,\Delta}$

######  Proof I.4.

Recall that $t\mathrel{\hat{\in}}u$ expands to $\exists x\in u.\;x\equiv t$,
so that $\neg t\mathrel{\hat{\in}}u$ is $\forall x\in u.\;\neg(x\equiv t)$. So
we have

$\Theta,t\in u\vdash\Delta$ Lemma 42 $\Theta,x\in u\vdash\neg(x\equiv
t),\Delta$ $\forall$ $\Theta\vdash\neg t\mathrel{\hat{\in}}u,\Delta$

###  I.3. Proof of Lemma 19

We now recall the claim of admissibility concerning rules for “moving down in
an equivalence”. Recall that these use the notation for quantifying on a path
below an object, defined in the body.

See 19

######  Proof I.5.

We proceed by induction over the input proof of $\Theta\vdash\Delta,\exists
r^{\prime}\in_{p}o^{\prime}.\;r\equiv_{{\sf Set}(T^{\prime})}r^{\prime}$ and
make a case distinction according to which rule was applied last. All cases
are straightforward, save for one: when a $\exists$ rule is applied on the
formula $\exists r^{\prime}\in_{p}o^{\prime}.\;r\equiv_{{\sf
Set}(T^{\prime})}r^{\prime}$. Let us only detail that one.

In that case, the last step has shape

$\dfrac{\Theta\vdash\Delta^{\mathsf{EL}},r\equiv_{{\sf
Set}(T^{\prime})}w,\exists r^{\prime}\in_{p}o^{\prime}.\;r\equiv_{{\sf
Set}(T^{\prime})}r^{\prime}}{\Theta\vdash\Delta^{\mathsf{EL}},\exists
r^{\prime}\in_{p}o^{\prime}.\;r\equiv_{{\sf Set}(T^{\prime})}r^{\prime}}$

and because $r\equiv_{{\sf Set}(T^{\prime})}w$ is not ${\mathsf{EL}}$, we can
further infer that the corresponding proof tree starts as follows

$\Theta,z\in r\vdash\Delta^{\mathsf{EL}},z\mathrel{\hat{\in}}w,\exists
r^{\prime}\in_{p}o^{\prime}.\;r\equiv_{{\sf Set}(T^{\prime})}r^{\prime}$
$\Theta\vdash\Delta^{\mathsf{EL}},r\subseteq w,\exists
r^{\prime}\in_{p}o^{\prime}.\;r\equiv_{{\sf Set}(T^{\prime})}r^{\prime}$
$\vdots$ $\Theta\vdash\Delta^{\mathsf{EL}},w\subseteq r,\exists
r^{\prime}\in_{p}o^{\prime}.\;r\equiv_{{\sf Set}(T^{\prime})}r^{\prime}$
$\Theta\vdash\Delta^{\mathsf{EL}},r\equiv_{{\sf Set}(T^{\prime})}w,\exists
r^{\prime}\in_{p}o^{\prime}.\;r\equiv_{{\sf Set}(T^{\prime})}r^{\prime}$
$\exists$ $\Theta\vdash\Delta^{\mathsf{EL}},\exists
r^{\prime}\in_{p}o^{\prime}.\;r\equiv_{{\sf Set}(T^{\prime})}r^{\prime}$

In particular, we have a strictly smaller subproof of

$\Theta,z\in r\vdash\Delta^{\mathsf{EL}},z\mathrel{\hat{\in}}w,\exists
r^{\prime}\in_{p}o^{\prime}.\;r\equiv_{{\sf Set}(T^{\prime})}r^{\prime}$

Applying the induction hypothesis, we get a proof of

$\Theta,z\in r\vdash\Delta^{\mathsf{EL}},z\mathrel{\hat{\in}}w,\exists
z^{\prime}\in_{mp}o^{\prime}.\;z\equiv_{{\sf Set}(T^{\prime})}z^{\prime}$

Recall that there is a max specialization of $\exists
r^{\prime}\in_{p}o^{\prime}.\;r\equiv_{{\sf Set}(T^{\prime})r^{\prime}}$.
Using that same specialization and the admissibility of the $\exists$ rule
that allows to perform a non-maximal specialization (Lemma 40), we can then
obtain a proof with conclusion

$\Theta,z\in r\vdash\Delta^{\mathsf{EL}},\exists
r\in_{p}o^{\prime}.\;z\mathrel{\hat{\in}}r,\exists
z^{\prime}\in_{mp}o^{\prime}.\;z\equiv_{{\sf Set}(T^{\prime})}z^{\prime}$

which concludes our argument, since $\exists
r\in_{p}o^{\prime}.\;z\mathrel{\hat{\in}}r$ and $\exists
z^{\prime}\in_{mp}o^{\prime}.\;z\equiv_{{\sf Set}(T^{\prime})}z^{\prime}$ are
syntactically the same.

###  I.4. Proof of Lemma 20

See 20

######  Proof I.6.

By induction over the shape of the input derivation, making a case distinction
according to the last rule applied. All cases are trivial, except of the case
of the rule $\exists$ where $\exists r^{\prime}\in_{p}o^{\prime}.r\equiv_{{\sf
Set}(T^{\prime})}r^{\prime}$ is the principal formula. So let us focus on that
one.

In that case, the proof necessarily has shape

$\Theta,y\in w\vdash\Delta^{\mathsf{EL}},y\mathrel{\hat{\in}}r,\exists
r^{\prime}\in_{p}o^{\prime}.\;r\equiv_{{\sf Set}(T^{\prime})}r^{\prime}$
$\forall$ $\Theta\vdash\Delta^{\mathsf{EL}},w\subseteq_{T^{\prime}}r,\exists
r^{\prime}\in_{p}o^{\prime}.\;r\equiv_{{\sf Set}(T^{\prime})}r^{\prime}$
$\Theta,x\in r\vdash\Delta^{\mathsf{EL}},x\mathrel{\hat{\in}}w,\exists
r^{\prime}\in_{p}o^{\prime}.\;r\equiv_{{\sf Set}(T^{\prime})}r^{\prime}$
$\forall$ $\Theta\vdash\Delta^{\mathsf{EL}},r\subseteq_{T^{\prime}}w,\exists
r^{\prime}\in_{p}o^{\prime}.\;r\equiv_{{\sf Set}(T^{\prime})}r^{\prime}$
$\wedge$ $\Theta\vdash\Delta^{\mathsf{EL}},r\equiv_{{\sf
Set}(T^{\prime})}w,\exists r^{\prime}\in_{p}o^{\prime}.\;r\equiv_{{\sf
Set}(T^{\prime})}r^{\prime}$ $\exists$
$\Theta\vdash\Delta^{\mathsf{EL}},\exists
r^{\prime}\in_{p}o^{\prime}.\;r\equiv_{{\sf Set}(T^{\prime})}r^{\prime}$

Applying the induction hypothesis to the leaves of that proof, we obtain two
proofs of

$\displaystyle\Theta,y\in
w\vdash\Delta^{\mathsf{EL}},y\mathrel{\hat{\in}}r,\exists
r^{\prime}\in_{p}o^{\prime}.\forall z\in
a,\;z\mathrel{\hat{\in}}r\leftrightarrow z\mathrel{\hat{\in}}r^{\prime}$

and

$\displaystyle\Theta,x\in
r\vdash\Delta^{\mathsf{EL}},x\mathrel{\hat{\in}}w,\exists
r^{\prime}\in_{p}o^{\prime}.\forall z\in
a,\;z\mathrel{\hat{\in}}r\leftrightarrow z\mathrel{\hat{\in}}r^{\prime}$

and we can conclude using the admissibility of weakening and Corollary 45
twice and replaying the $\wedge/\forall/\exists$ steps in the appropriate
order (a branch of the proof derivation is elided below for lack of horizontal
space):

$\Theta,y\in w\vdash\Delta^{\mathsf{EL}},y\mathrel{\hat{\in}}r,\exists
r^{\prime}\in_{p}o^{\prime}.\forall z\in
a,\;z\mathrel{\hat{\in}}r\leftrightarrow z\mathrel{\hat{\in}}r^{\prime}$
Corollary 45
$\Theta\vdash\Delta^{\mathsf{EL}},\neg(y\mathrel{\hat{\in}}w),y\mathrel{\hat{\in}}r,\exists
r^{\prime}\in_{p}o^{\prime}.\forall z\in
a,\;z\mathrel{\hat{\in}}r\leftrightarrow z\mathrel{\hat{\in}}r^{\prime}$
$\vee$
$\Theta\vdash\Delta^{\mathsf{EL}},{y\mathrel{\hat{\in}}w}\rightarrow{y\mathrel{\hat{\in}}r},\exists
r^{\prime}\in_{p}o^{\prime}.\forall z\in
a,\;z\mathrel{\hat{\in}}r\leftrightarrow z\mathrel{\hat{\in}}r^{\prime}$
$\vdots$
$\Theta\vdash\Delta^{\mathsf{EL}},{y\mathrel{\hat{\in}}r}\leftrightarrow{y\mathrel{\hat{\in}}w},\exists
r^{\prime}\in_{p}o^{\prime}.\forall z\in
a,\;z\mathrel{\hat{\in}}r\leftrightarrow z\mathrel{\hat{\in}}r^{\prime}$ Lemma
37 $\Theta,y\in
a\vdash\Delta^{\mathsf{EL}},{y\mathrel{\hat{\in}}r}\leftrightarrow{y\mathrel{\hat{\in}}w},\exists
r^{\prime}\in_{p}o^{\prime}.\forall z\in
a,\;z\mathrel{\hat{\in}}r\leftrightarrow z\mathrel{\hat{\in}}r^{\prime}$
$\forall$ $\Theta\vdash\Delta^{\mathsf{EL}},\forall z\in
a.\;{z\mathrel{\hat{\in}}r}\leftrightarrow{z\mathrel{\hat{\in}}w},\exists
r^{\prime}\in_{p}o^{\prime}.\forall z\in
a,\;z\mathrel{\hat{\in}}r\leftrightarrow z\mathrel{\hat{\in}}r^{\prime}$
$\exists$ $\Theta\vdash\Delta^{\mathsf{EL}},\exists
r^{\prime}\in_{p}o^{\prime}.\forall z\in
a,\;z\mathrel{\hat{\in}}r\leftrightarrow z\mathrel{\hat{\in}}r^{\prime}$

##  Appendix J Proof of the main theorem for non-set types

Recall again our main result:

See 16

In the body of the paper, we gave a proof for the case where the type of the
defined object is ${\sf Set}(T)$ for any $T$. We now discuss the remaining
cases: the base case and the inductive case for product types.

So assume we are given an implicit definition $\varphi(\vec{i},\vec{a},o)$ and
a ${\mathsf{EL}}$-normalized witness, and proceed by induction over the type
$o$:

  * •

If $o$ has type ${\mathsf{Unit}}$, then, since there is only one inhabitant in
type ${\mathsf{Unit}}$, then we can take our explicit definition to be the
corresponding ${\mathsf{NRC}}$ expression $\langle\rangle$.

  * •

If $o$ has type $\mathfrak{U}$, then using interpolation on the entailment
$\varphi(\vec{i},\vec{a},o)\rightarrow(\varphi(\vec{i},\vec{a}^{\prime},o^{\prime})\rightarrow
o=_{\mathfrak{U}}o^{\prime})$, we obtain $\theta(\vec{i},o)$ with
$\varphi(\vec{i},\vec{a},o)\rightarrow\theta(\vec{i},\vec{a},o)$ and
$\theta(\vec{i},o)\wedge\varphi(\vec{i},\vec{a},o^{\prime})\rightarrow
o=_{\mathfrak{U}}o^{\prime}$. But then we know that $\varphi$ implies $o$ is a
subobject of $\vec{i}$: otherwise we could find a model that contradicts the
entailment. There is an ${\mathsf{NRC}}$ definition $A(\vec{i})$ that collects
all of the $\mathfrak{U}$-elements lying beneath $\vec{i}$. We can then take
$E(\vec{i})=\textsc{get}_{T}(\\{x\in A(\vec{i})\mid\theta(\vec{i},x)\\})$ as
our ${\mathsf{NRC}}$ definition of $o$. The correctness of $E$ follows from
the properties of $\theta$ above.

  * •

If $o$ has type $T_{1}\times T_{2}$, recalling the definition of
$\equiv_{T_{1}\times T_{2}}$, we have a derivation of

$\varphi(\vec{i},\vec{a},o)\wedge\varphi(\vec{i},\vec{a},o^{\prime})\vdash\pi_{1}(o)\equiv_{T_{1}}\pi_{1}(o^{\prime})\wedge\pi_{2}(o)\equiv_{T_{2}}\pi_{2}(o^{\prime})$

By Lemma 38, we have proofs of

$\varphi(\vec{i},\vec{a},o)\wedge\varphi(\vec{i},\vec{a},o^{\prime})\vdash\pi_{i}(o)\equiv_{T_{i}}\pi_{i}(o^{\prime})$

for $i\in\\{1,2\\}$. Take $o_{1}$ and $o_{2}$ to be fresh variables of types
$T_{1}$ and $T_{2}$. Take $\tilde{\varphi}(\vec{i},\vec{a},o_{1},o_{2})$ to be
$\varphi(\vec{i},\vec{a},\langle o_{1},o_{2}\rangle)$. By substitutivity (the
admissible rule given by Lemma 41) and applying the $\times_{\beta}$ rule, we
have ${\mathsf{EL}}$-normalized proofs of

$\varphi(\vec{i},\vec{a},\langle
o_{1},o_{2}\rangle)\wedge\varphi(\vec{i},\vec{a},\langle
o_{1}^{\prime},o_{2}^{\prime}\rangle)\vdash o_{i}\equiv_{T_{i}}o^{\prime}_{i}$

We can apply our inductive hypothesis to obtain a definition
$E^{\mathsf{IH}}_{i}(\vec{i})$ for both $i\in\\{1,2\\}$. We can then take our
explicit definition to be $\langle
E^{\mathsf{IH}}_{1}(\vec{i}),E^{\mathsf{IH}}_{2}(\vec{i})\rangle$.

##  Appendix K Variant of Parameter Collection Theorem, Theorem 21, for
parameterized definability in first-order logic

Our paper has focused on the setting of nested relations, phrasing our results
in terms of the language ${\mathsf{NRC}}$. We indicated in the conclusion of
the paper that there is a variant of the ${\mathsf{NRC}}$ parameter collection
theorem, Theorem 21, for the broader context of first-order logic. In fact,
this first-order version of the result provided the intuition for the theorem.
In this section we present this variant.

We consider first-order logic with equality and without function symbols,
which also excludes nullary function symbols, that is, individual constants,
whose role is just taken by free individual variables. Specifically, we
consider first-order formulas with the following syntax

$\varphi,\psi~{}~{}\mathrel{::=}~{}~{}P(\vec{x})\;|\;\neg
P(\vec{x})\;|\;x=y\;|\;x\neq
y\;|\;\top\;|\;\bot\;|\;\varphi\wedge\psi\;|\;\varphi\vee\psi\;|\;\forall
x\,\varphi\;|\;\exists x\,\varphi.$

Amongst the formulas given in the grammar above, those of the shape
$P(\vec{x}),\neg P(\vec{x}),x=y$ and $x\neq y$ are called _literals_. Literals
come with a polarity: those of the shape $P(\vec{x})$ and $x=y$ are positive
while the other, of the shape $\neg P(\vec{x})$ or $x\neq y$ are negative.

On top of this, we give some “syntactic sugar”. We define $\neg\varphi$ by
induction over $\varphi$, dualizing every connective, including the
quantifiers, and removing doubled negation over literals. We define
implication $\varphi\rightarrow\psi$ as an abbreviation of
$\neg\varphi\vee\psi$ and bi-implication $\varphi\leftrightarrow\psi$ as an
abbreviation of $(\varphi\rightarrow\psi)\wedge(\psi\rightarrow\varphi)$. The
set of free variables occurring in a formula $\varphi$ is denoted by
$FV(\varphi)$ and the set of predicates occurring in $\varphi$ by
$\mathit{PR}(\varphi)$.

Figure 5 shows our proof system for first-order logic. It is identical to a
system from the prior literature.444 G3c+Ref+Repl [NvP01, TS00], in the one-
sided form of GS3, discussed in Chapter 3 of [TS00], which reduces the number
of rules. Like the ${\mathsf{EL}}$-normalized proof system we used in the body
of the paper for $\Delta_{0}$ formulas, it is a $1$-sided calculus. The
formulas other than $\Gamma$ in the premise are the _active formulas_ of the
rule, while the _principal formulas_ are the other formulas in its conclusion.
The complementary principal formulas in Ax have to be literals. The
replacement of symbols induced by equality with Repl is only performed on
negative literals.

* [left=Ax, right= $\varphi$ a positive literal] ⊢Γ, φ, ¬φ * [left=$\top$] ⊢Γ, ⊤ * [left=$\wedge$] ⊢Γ, φ_1 ⊢Γ, φ_2 ⊢Γ, φ_1 ∧φ_2 * [left=$\vee$] ⊢Γ, φ_1, φ_2 ⊢Γ, φ_1 ∨φ_2
* [left=$\forall$, right= $y\notin FV(\Gamma,\forall x\;\varphi)$] ⊢Γ, φ[y/x]⊢Γ, ∀x φ * [left=$\exists$] ⊢Γ, φ[t/x], ∃x φ⊢Γ, ∃x φ
* [left=Ref] ⊢t ≠t, Γ ⊢Γ * [left=Repl, right= $\varphi$ a negative literal] ⊢t≠u, φ[u/x], φ[t/x], Γ ⊢t≠u, φ[t/x], Γ

Figure 5. One-sided sequent calculus for first-order logic with equality.

As in the body of the paper, a proof tree or derivation is a tree whose nodes
are labelled with sequents, such that the labels of the children of a given
node and that of the node itself are the premises and conclusion, resp., of an
instance of a rule from Figure 5. The _conclusion_ of a proof tree is the
sequent that labels its root. The proof system is closed under cut, weakening
and contraction. Closure under contraction in particular makes it suited as
basis for “root-first” proof search. Read in this “bottom-up” way, the
$\exists$ rule states that a disjunction with an existentially quantified
formula can be proven if the extension of the disjunction by a copy of the
formula where the formerly quantified variable $x$ is instantiated with an
arbitrary variable $t$ can be proven. The existentially quantified formula is
retained in the premise and may be used to add further instances by applying
$\exists$ again in the course of the proof.

Soundness of the rules is straightforward. For example the $\exists$ rule
could be read as stating that if we deduce a disjunction in which one disjunct
is a formula $\varphi$ with $t$ in it, then we can deduce the same disjunction
but with some occurrences of $t$ replaced in that disjunct with an
existentially quantified variable. Completeness of the proof system can also
be proven by a standard Henkin-style construction: indeed, since this is
really ordinary first-order logic, there are proofs in the literature for
systems that are very similar to this one: [TS00, NvP98].

Like our higher-level system in the body of the paper (Fig. 2) the first-order
system in Fig. 5 does not impose any special constraints on the shape of the
proof. We adapt the extra conditions on contexts of the
${\mathsf{EL}}$-normalized system for $\Delta_{0}$ formulas (Fig. 3) to our
first-order system. We characterize a proof in the system of Fig. 5 as _FO-
normalised_ if no application of Ax, $\top$, $\exists$, Ref, Repl contains in
its conclusion a formula whose top-level connective is $\lor$, $\land$ or
$\forall$.

The FO-normalised property may be either incorporated directly into a “root-
first” proof procedure by constraining rule applications or it may be ensured
by converting an arbitrary given proof tree to a FO-normalised proof tree with
the same ultimate consequence. This conversion is achieved by a
straightforward adaption of the method for the $\Delta_{0}$ calculus from
Appendix G, Fig. 4. Only steps (1) and (2) of the method are relevant here,
since step (3) is specifically for the pair terms of $\Delta_{0}$ formulas. In
step (2), instances of $\lor$, $\land$ or $\forall$ are permuted down over
$\exists$, Ref and Repl according to the generic permutation schemas of Lemma
33. The left sides of $\vdash$ in these schemas can be ignored since they
represent the $\in$-contexts for $\Delta_{0}$ formulas. Finally, derivations
of sequents containing $\top$ are replaced by applications of rule $\top$ and
derivations of sequents containing complementary literals
$\varphi,\lnot\varphi$ by applications of rule Ax. The conversion, however,
may increase the proof size exponentially as discussed in Sect. G.4.

We now discuss our generalization of the ${\mathsf{NRC}}$ Parameter Collection
Theorem from the body of the paper to this first-order setting. The concept of
explicit definition can be generalized to _definition up to parameters and
disjunction_ : A family of formulas $\chi_{i}(\vec{z},\vec{y},\vec{r})$,
$1\leq i\leq n$, provides an _explicit definition up to parameters and
disjunction_ of a formula $\lambda(\vec{z},\vec{l})$ relative to a formula
$\varphi$ if

$\varphi\models\bigvee_{i=n}^{n}\exists\vec{y}\forall\vec{z}\,(\lambda(\vec{z},\vec{l})\leftrightarrow\chi_{i}(\vec{z},\vec{y},\vec{r})).$
($\star$)

The entailment ($\star$ ‣ K) is considered with restrictions on the predicates
and variables permitted to occur in the $\chi_{i}$. In the simplest case,
$\lambda(\vec{z},\vec{l})$ is a positive literal $p(\vec{z})$ with a predicate
that is permitted in $\varphi$ but not in the $\chi_{i}$. The predicate $p$ is
then said to be _explicitly definable up to parameters and disjunction_ with
respect to $\varphi$ [CK92].

The disjunction over a finite family of formulas $\chi_{i}$ can be
consolidated into a single quantified biconditional as long as the domain has
size at least $2$ in every model of $\varphi$. Notice that if $\varphi$ has
only finite models, then by the compactness theorem of first-order logic, the
size of models must be bounded. In such cases every formula $\lambda$ is
definable with sufficiently many parameters.

We can now state our analog of the Parameter Collection Theorem, Theorem 21.

######  Theorem 46.

Let $\varphi$, $\psi$, $\lambda(\vec{z},\vec{l})$, and
$\rho(\vec{z},\vec{y},\vec{r})$ be first-order formulas such that

$\varphi\land\psi\models\exists\vec{y}\forall\vec{z}\,(\lambda(\vec{z},\vec{l})\leftrightarrow\rho(\vec{z},\vec{y},\vec{r})).$

Then there exist first-order formulas
$\chi_{i}(\vec{z},{\vec{v}}_{i},{\vec{c}}_{i})$, $1\leq i\leq n$, such that

  1. (1)

$\varphi\land\psi\models\bigvee_{i=1}^{n}\exists{\vec{v}}_{i}\forall
z(\lambda(\vec{z},\vec{l})\leftrightarrow\chi_{i}(\vec{z},{\vec{v}}_{i},{\vec{c}}_{i}))$,

  2. (2)

${\vec{c}}_{i}\subseteq(FV(\varphi)\cup\vec{l})\cap(FV(\psi)\cup\vec{r})$,

  3. (3)

$\mathit{PR}(\chi_{i})\subseteq(\mathit{PR}(\varphi)\cup\mathit{PR}(\lambda))\cap(\mathit{PR}(\psi)\cup\mathit{PR}(\rho))$.

Moreover, given a FO-normalised proof of the precondition with the system of
Fig. 5, a family of formulas $\chi_{i}$, $1\leq i\leq n$, with the claimed
properties can be computed in polynomial time in the size of the proof tree.

In the theorem statement, the free variables of $\lambda$ are $\vec{z}$ and
$\vec{l}$, and the free variables of $\rho$ are $\vec{z}$, $\vec{y}$, and
$\vec{r}$. The precondition supposes an explicit definition $\rho$ of
$\lambda$ up to parameters with respect to a conjunction $\varphi\land\psi$.
The conclusion then claims that one can effectively compute another definition
of $\lambda$ with respect to $\varphi\land\psi$ that is up to parameters and
disjunction and has a constrained signature: free variables and predicates
must occur in at least one of the “left side” formulas $\varphi$ and $\lambda$
and also in at least one of the “right side” formulas $\psi$ and $\rho$. In
other words, the theorem states that if ${\mathcal{S}IG}_{L}$ and
${\mathcal{S}IG}_{R}$ are “left” and “right” signatures such that $\varphi$
and $\lambda$ are over ${\mathcal{S}IG}_{L}$, $\psi$ and $\rho$ are over
${\mathcal{S}IG}_{R}$, and $\rho$ provides an explicit definition of $\lambda$
up to parameters with respect to $\varphi\land\psi$, then one can effectively
compute another definition of $\lambda$ with respect to $\varphi\land\psi$
that is up to parameters and disjunction and is just over the intersection of
the signatures ${\mathcal{S}IG}_{L}$ and ${\mathcal{S}IG}_{R}$.

We now prove Theorem 46 by induction on the depth of the proof tree,
generalizing the constructive proof method for Craig interpolation often
called Maehara’s method [Tak87, TS00, Smu68b]. To simplify the presentation we
assume that the tuples $\vec{z}$ and $\vec{y}$ in the theorem statement each
consist of a single variable $z$ and $y$, respectively. The generalization of
our argument to tuples of variables is straightforward.

To specify conveniently the construction steps of the family of formulas
$\chi_{i}$ we introduce the following concept: A _pre-defining equivalence up
to parameters and disjunction_ (briefly ${\mathsf{PDEPD}}$) for a formula
$\lambda(z,\vec{l})$ is a formula $\delta$ built up from formulas of the form
$\forall z\,(\lambda(z,\vec{l})\leftrightarrow\chi(z,\vec{p}))$ (where the
left side is always the same formula $\lambda(z,\vec{l})$ but the right sides
$\chi(z,\vec{p})$ may differ) and a finite number of applications of
disjunction and existential quantification upon variables from the vectors
$\vec{p}$ of the right sides. The empty disjunction $\bot$ is allowed as a
special case of a ${\mathsf{PDEPD}}$. By rewriting with the equivalence
$\exists v\,(\delta_{1}\lor\delta_{2})\equiv\exists v\,\delta_{1}\lor\exists
v\,\delta_{2}$, any ${\mathsf{PDEPD}}$ for $\lambda$ can be efficiently
transformed into the form $\bigvee_{i=1}^{n}\exists\vec{v}_{i}\forall
z\,(\lambda(z,\vec{l})\leftrightarrow\chi_{i}(z,\vec{v}_{i},\vec{r}_{i}))$ for
some natural number $n\geq 0$. That is, although a ${\mathsf{PDEPD}}$ has in
general not the syntactic form of the disjunction of quantified biconditionals
in the theorem statement (thus “pre-”), it corresponds to such a disjunction.
The more generous syntax will be convenient in the induction. The sets of
additional variables $\vec{l}$ and $\vec{p}$ in the biconditionals
$\lambda(z,\vec{l})\leftrightarrow\chi(z,\vec{p})$ can overlap, but the
overlap will be top-level variables that never get quantified. Although we
have defined the notion of ${\mathsf{PDEPD}}$ for a general $\lambda$, in the
proof we just consider ${\mathsf{PDEPD}}$s for the formula $\lambda$ from the
theorem statement.

For ${\mathsf{PDEPD}}$s $\delta$ we provide analogs to $FV$ and $\mathit{PR}$
that only yield free variables and predicates of $\delta$ that occur in a
right side of its biconditionals, which helps to express the restrictions by
definability properties that constrains the signature of exactly those right
sides. Recall that we refer of these right sides as subformulas
$\chi(z,\vec{p})$. For ${\mathsf{PDEPD}}$ $\delta$, define
$\mathit{PR}^{\mathsf{RHS}}(\delta)$ as the set of the predicate symbols that
occur in a subformula $\chi(z,\vec{p})$ of $\delta$ and define
$FV^{\mathsf{RHS}}(\delta)$ as the set of all variables that occur in a
subformula $\chi(z,\vec{p})$ of $\delta$ and are free in $\delta$. In other
words, $FV^{\mathsf{RHS}}(\delta)$ is the set of all variables $p$ in the
vectors $\vec{p}$ of the subformulas $\chi(z,\vec{p})$ that have an occurrence
in $\delta$ which is not in the scope of a quantifier $\exists p$. If, for
example $\delta=\bigvee_{i=1}^{n}\exists\vec{v}_{i}\forall
z\,(\lambda(z,\vec{l})\leftrightarrow\chi_{i}(z,\vec{v}_{i},\vec{r}_{i}))$,
then $FV^{\mathsf{RHS}}(\delta)$ is the set of all variables in the vectors
$r_{i}$, for $1\leq i\leq n$.

To build up ${\mathsf{PDEPD}}$s we provide an operation that only affects the
right sides of the biconditionals, a restricted form of existential
quantification. It is for use in interpolant construction to convert a free
variable in right sides that became illegal into an existentially quantified
parameter. For variables $p,y$ define $\delta[y/p]^{\mathsf{RHS}}$ as $\delta$
after substituting all occurrences of $p$ that are within a right side
$\chi(z,\vec{p})$ and are free in $\delta$ with $y$. Define
$\exists^{\mathsf{RHS}}p\,\delta$ as shorthand for $\exists
y\,\delta[y/p]^{\mathsf{RHS}}$, where $y$ is a fresh variable. Clearly
$\delta\models\exists^{\mathsf{RHS}}p\,\delta$ and $p$ has no free occurrences
in $\exists^{\mathsf{RHS}}p\,\delta$ that are in any of the right side
formulas $\chi(z,\vec{p})$, i.e., $p\notin
FV^{\mathsf{RHS}}(\exists^{\mathsf{RHS}}p\,\delta)$. Occurrences of $p$ in the
left sides $\lambda(z,\vec{l})$, if $p$ is a member of $\vec{l}$, are
untouched in $\exists^{\mathsf{RHS}}p\,\delta$. If $p$ is not in $\vec{l}$,
then $\exists^{\mathsf{RHS}}p\,\delta$ reduces to ordinary existential
quantification $\exists y\,\delta[y/p]$.

We introduce the following symbolic shorthand for the parametric definition on
the right side in the theorem’s precondition.

$\begin{array}[]{lcl@{\hspace{1em}}lcl}\mathcal{G}&\mathrel{:=}&\exists
y\forall z\,(\lambda(z,\vec{l})\leftrightarrow\rho(z,y,\vec{r})).\hfil\hskip
10.00002pt\\\ \end{array}$

Note that our proof rules are such that if we have a proof (FO-normalised or
not) that our original top-level “global” parametric definition is implied by
some formula, then every one-sided sequent in the proof must include that
parametric definition in it. This is because the rules that eliminate a
formula when read “bottom-up” cannot apply to that parametric definition,
whose outermost logic operator is the existential quantifier. Thus, in our
inductive argument, we can assume that $\mathcal{G}$ is always present.

We write

$\vdash\Gamma_{L};\;\;\Gamma_{R};\;\;\mathcal{G}\;:\;\langle\theta,\mathcal{D}\rangle,$

where $\vdash\Gamma_{L},\Gamma_{R},\mathcal{G}$ is a sequent, partitioned into
three components, multisets $\Gamma_{L}$ and $\Gamma_{R}$ of formulas and the
formula $\mathcal{G}$ from the theorem’s hypothesis, $\theta$ is a formula and
$\mathcal{D}$ is a ${\mathsf{PDEPD}}$, to express that the following
properties hold:

  1. (1)

$\models\Gamma_{R}\lor\theta$.

  2. (2)

$\models\lnot\theta\lor\Gamma_{L}\lor\mathcal{D}$.

  3. (3)

$\mathit{PR}(\theta)\subseteq(\mathit{PR}(\Gamma_{L})\cup\mathit{PR}(\lambda))\cap(\mathit{PR}(\Gamma_{R})\cup\mathit{PR}(\rho))$.

  4. (4)

$FV(\theta)\subseteq(FV(\Gamma_{L})\cup\vec{l})\cap(FV(\Gamma_{R})\cup\vec{r})$.

  5. (5)

$\mathcal{D}$ is a ${\mathsf{PDEPD}}$ for $\lambda(z,\vec{l})$.

  6. (6)

$\mathit{PR}^{\mathsf{RHS}}(\mathcal{D})\subseteq(\mathit{PR}(\Gamma_{L})\cup\mathit{PR}(\lambda))\cap(\mathit{PR}(\Gamma_{R})\cup\mathit{PR}(\rho))$.

  7. (7)

$FV^{\mathsf{RHS}}(\mathcal{D})\subseteq(FV(\Gamma_{L})\cup\vec{l})\cap(FV(\Gamma_{R})\cup\vec{r})$.

For a given proof with conclusion $\vdash\lnot\varphi,\lnot\psi,\mathcal{G}$,
corresponding to the hypothesis $\varphi\land\psi\models\mathcal{G}$ of the
theorem, we show the construction of a formula $\theta$ and ${\mathsf{PDEPD}}$
$\mathcal{D}$ such that

$\vdash\lnot\varphi;\;\;\lnot\psi;\;\;\mathcal{G}\;:\;\langle\theta,\mathcal{D}\rangle.$

From properties 1–2 and 5– 7 it is then straightforward to read off that the
formula
$\bigvee_{i=1}^{n}\exists\vec{v_{i}}\forall\vec{z}(\lambda(\vec{z},\vec{l})\leftrightarrow\chi_{i}(\vec{z},{\vec{v}}_{i},{\vec{r}}_{i}))$
obtained from $\mathcal{D}$ by propagating existential quantifiers inwards is
as claimed in the theorem’s conclusion.

Formula $\theta$ plays an auxiliary role in the induction. For the overall
conclusion of the proof it a side result that is like a Craig interpolant of
$\psi$ and $\varphi\rightarrow D$, but slightly weaker syntactically
constrained by taking $\lambda$ and $\rho$ into account:
$FV(\theta)\subseteq((FV(\varphi)\cup\vec{l})\cap(FV(\psi)\cup\vec{r}))$ and
$\mathit{PR}(\theta)\subseteq(\mathit{PR}(\varphi)\cup\mathit{PR}(\lambda))\cup\mathit{PR}(\psi)\cup\mathit{PR}(\rho)$.

As basis of the induction, we have to show constructions of $\theta$ and
$\mathcal{D}$ such that
$\vdash\Gamma_{L};\;\;\Gamma_{R};\;\;\mathcal{G}\;:\;\langle\theta,\mathcal{D}\rangle$
holds for Ax and $\top$, considering each possibility in which the principal
formula(s) can be in $\Gamma_{L}$ or $\Gamma_{R}$. For the induction step,
there are a number of subcases, according to which rule is last applied and
which of the partitions $\Gamma_{L}$, $\Gamma_{R}$ or $\mathcal{G}$ contain
the principal formula(s). We first discuss the most interesting case, the
induction step where $\mathcal{G}$ is the principal formula. This case is
similar to the most interesting case in the ${\mathsf{NRC}}$ Parameter
Collection Theorem, covered in the body of the paper.

##### Case where the principal formula is $\mathcal{G}$.

We now give more detail on the most complex case. If the principal formula of
a conclusion $\vdash\Gamma_{L};\;\;\Gamma_{R};\;\;\mathcal{G}$ is
$\mathcal{G}$, then the rule that is applied rule must be $\exists$. From the
FO-normalised property of the proof it follows that the derivation tree ending
in $\vdash\Gamma_{L};\;\;\Gamma_{R};\;\;\mathcal{G}$ must have the following
shape, for some $u\notin FV(\Gamma_{L},\Gamma_{R},\mathcal{G})$ and $w\neq u$.
Note that $u$ could be either a top-level variable from $\lambda$, i.e., a
member of $\vec{l}$, or one introduced during the proof.

$\begin{array}[]{rccrc}\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small$\lor$}&\vdash\Gamma_{L},\lnot\lambda(u,\vec{l}),\Gamma_{R},\rho(u,w,\vec{r}),\mathcal{G}&&\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small$\lor$}&\vdash\Gamma_{L},\lambda(u,\vec{l}),\Gamma_{R},\lnot\rho(u,w,\vec{r}),\mathcal{G}\\\
\cline{2-2}\cr\cline{5-5}\cr\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small$\land$}&\vdash\Gamma_{L},\Gamma_{R},\lambda(u,\vec{l})\rightarrow\rho(u,w,\vec{r}),\mathcal{G}&&&\vdash\Gamma_{L},\lambda(u,\vec{l}),\Gamma_{R},\rho(u,w,\vec{r})\rightarrow\lambda(u,\vec{l}),\mathcal{G}\\\
\cline{2-5}\cr\lx@intercol\hfil\begin{array}[]{rc}\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small$\forall$}&\vdash\Gamma_{L},\Gamma_{R},\lambda(u,\vec{l})\leftrightarrow\rho(u,w,\vec{r}),\mathcal{G}\\\
\cline{2-2}\cr\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small$\exists$}&\vdash\Gamma_{L},\Gamma_{R},\forall
z\,(\lambda(z,\vec{l})\leftrightarrow\rho(z,w,\vec{r})),\mathcal{G}\\\
\cline{2-2}\cr&\vdash\Gamma_{L},\Gamma_{R},\mathcal{G}\end{array}\hfil\lx@intercol\end{array}$

The important point is that the two “leaves” of the above tree are both
sequents where we can apply our induction hypothesis. Taking into account the
partitioning of the sequents at the bottom conclusion and the top premises in
this figure, we can express the induction step in the form of a “macro” rule
that specifies the how we constructed the required $\theta$ and $\mathcal{D}$
for the conclusion, making use of the $\theta_{1},\mathcal{D}_{1}$ and
$\theta_{2},\mathcal{D}_{2}$ that we get by applying the induction hypothesis
to each of the two premises.

$\begin{array}[]{c@{\hspace{1em}}cl}\vdash\Gamma_{L},\lnot\lambda(u,\vec{l});\,\Gamma_{R},\rho(u,w,\vec{r});\,\mathcal{G}:\langle\theta_{1},\mathcal{D}_{1}\rangle\hfil\hskip
10.00002pt&\vdash\Gamma_{L},\lambda(u,\vec{l});\,\Gamma_{R},\lnot\rho(u,w,\vec{r});\,\mathcal{G}:\langle\theta_{2},\mathcal{D}_{2}\rangle\\\
\cline{1-2}\cr\lx@intercol\hfil\vdash\Gamma_{L};\;\;\Gamma_{R};\;\;\mathcal{G}\;:\;\langle\theta,\mathcal{D}\rangle,\hfil\lx@intercol\end{array}$

where $u$ is as above. The values of $\theta$ and $\mathcal{D}$ – the new
formula and definition that we are building – will depend on occurrences of
$w$, and we give their construction in cases below:

  1. (1)

If $w\notin FV(\Gamma_{L})\cup\vec{l}$ or $w\in FV(\Gamma_{R})\cup\vec{r}$,
then

$\begin{array}[]{lcl}\theta&\mathrel{:=}&\forall
u\,(\theta_{1}\lor\theta_{2}).\\\
\mathcal{D}&\mathrel{:=}&\exists^{\mathsf{RHS}}u\,\mathcal{D}_{1}\lor\exists^{\mathsf{RHS}}u\,\mathcal{D}_{2}\lor\forall
z\,(\lambda(z,\vec{l})\leftrightarrow\theta_{2}[z/u]).\end{array}$

  2. (2)

Else it holds that $w\in FV(\Gamma_{L})\cup\vec{l}$ and $w\notin
FV(\Gamma_{R})\cup\vec{r}$. Then

$\begin{array}[]{lcl}\theta&\mathrel{:=}&\forall w\forall
u\,(\theta_{1}\lor\theta_{2}).\\\
\mathcal{D}&\mathrel{:=}&\exists^{\mathsf{RHS}}w\,(\exists^{\mathsf{RHS}}u\,\mathcal{D}_{1}\lor\exists^{\mathsf{RHS}}u\,\mathcal{D}_{2}\lor\forall
z\,(\lambda(z,\vec{l})\leftrightarrow\theta_{2}[z/u])).\end{array}$

We now verify that
$\vdash\Gamma_{L};\;\;\Gamma_{R};\;\;\mathcal{G}\;:\;\langle\theta^{\prime},\mathcal{D}^{\prime}\rangle$,
that is, properties 1–7, hold. The proofs for the individual properties are
presented in tabular form, with explanations annotated in the side column,
where _IH_ stands for _induction hypothesis_. We concentrate on the case 1 and
indicate the modifications of the proofs for case 2 in remarks, where we refer
to the values of $\theta$ and $\mathcal{D}$ for that case in terms of the
values for the case 1 as $\forall w\,\theta$ and
$\exists^{\mathsf{RHS}}w\,\mathcal{D}$. In the proofs of the semantic
properties 1 and 2 we let sequents stand for the disjunction of their members.

Property 1:

${{{{{{{{{{\begin{array}[]{Z{1.8em}<EMAIL_ADDRESS>Phys.~{}Rev.~{}Lett.}{r-theta-1}$\@add@raggedleft}}\hskip
10.00002pt&\models\Gamma_{R}\lor\rho(u,w,\vec{r})\lor\theta_{1}.\hfil\hskip
5.0pt&\textrm{IH}\\\ {\rm
Phys.~{}Rev.~{}Lett.}{r-theta-2}$\@add@raggedleft}}\hskip
10.00002pt&\models\Gamma_{R}\lor\lnot\rho(u,w,\vec{r})\lor\theta_{2}.\hfil\hskip
5.0pt&\textrm{IH}\\\ {\rm
Phys.~{}Rev.~{}Lett.}{r-theta-3}$\@add@raggedleft}}\hskip
10.00002pt&\models\Gamma_{R}\lor\theta_{1}\lor\theta_{2}.\hfil\hskip
5.0pt&\textrm{by~{}(??)\immediate, (??)\immediate}\\\ {\rm
Phys.~{}Rev.~{}Lett.}{r-theta-4}$\@add@raggedleft}}\hskip
10.00002pt&\models\Gamma_{R}\lor\forall
u\,(\theta_{1}\lor\theta_{1})\hfil\hskip 5.0pt&\textrm{by~{}(??)\immediate
since }u\notin FV(\Gamma_{R})\\\ {\rm
Phys.~{}Rev.~{}Lett.}{r-theta-5}$\@add@raggedleft}}\hskip
10.00002pt&\models\Gamma_{R}\lor\theta.\hfil\hskip
5.0pt&\textrm{by~{}(??)\immediate and def. of }\theta\\\ \end{array}$

For case 2, it follows from the precondition $w\notin FV(\Gamma_{R})$ and step
(??) that $\models\Gamma_{R}\lor\forall w\,\theta$.

Property 2:

${{{{{{{{{{{{{{{{{{{{{{{{{{\begin{array}[]{Z{1.8em}<EMAIL_ADDRESS>Phys.~{}Rev.~{}Lett.}{l-theta-i1}$\@add@raggedleft}}\hskip
10.00002pt&\models\lnot\theta_{1}\lor\Gamma_{L}\lor\lnot\lambda(u,\vec{l})\lor\mathcal{D}_{1}.\hfil\hskip
5.0pt&\textrm{IH}\\\ {\rm
Phys.~{}Rev.~{}Lett.}{l-theta-i2}$\@add@raggedleft}}\hskip
10.00002pt&\models\lnot\theta_{2}\lor\Gamma_{L}\lor\lambda(u,\vec{l})\lor\mathcal{D}_{2}.\hfil\hskip
5.0pt&\textrm{IH}\\\ {\rm
Phys.~{}Rev.~{}Lett.}{l-theta-3}$\@add@raggedleft}}\hskip
10.00002pt&\models\lnot(\theta_{1}\lor\theta_{2})\lor\Gamma_{L}\lor\lnot\lambda(u,\vec{l})\lor\mathcal{D}_{1}\lor\theta_{2}.\hfil\hskip
5.0pt&\textrm{by (??)\immediate}\\\ {\rm
Phys.~{}Rev.~{}Lett.}{l-theta-4}$\@add@raggedleft}}\hskip
10.00002pt&\models\lnot(\theta_{1}\lor\theta_{2})\lor\Gamma_{L}\lor\lnot\lambda(u,\vec{l})\lor\mathcal{D}_{1}\lor\mathcal{D}_{2}\lor\theta_{2}.\hfil\hskip
5.0pt&\textrm{by (??)\immediate}\\\ {\rm
Phys.~{}Rev.~{}Lett.}{l-theta-5}$\@add@raggedleft}}\hskip
10.00002pt&\models\lnot\forall
u\,(\theta_{1}\lor\theta_{2})\lor\Gamma_{L}\lor\lnot\lambda(u,\vec{l})\lor\mathcal{D}_{1}\lor\mathcal{D}_{2}\lor\theta_{2}.\hfil\hskip
5.0pt&\textrm{by (??)\immediate}\\\ {\rm
Phys.~{}Rev.~{}Lett.}{l-theta-6}$\@add@raggedleft}}\hskip
10.00002pt&\models\lnot\forall
u\,(\theta_{1}\lor\theta_{2})\lor\lnot\theta_{2}\lor\Gamma_{L}\lor\lambda(u,\vec{l})\lor\mathcal{D}_{1}\lor\mathcal{D}_{2}.\hfil\hskip
5.0pt&\textrm{by (??)\immediate}\\\ {\rm
Phys.~{}Rev.~{}Lett.}{l-theta-7}$\@add@raggedleft}}\hskip
10.00002pt&\models\lnot\forall
u\,(\theta_{1}\lor\theta_{2})\lor\Gamma_{L}\lor\mathcal{D}_{1}\lor\mathcal{D}_{2}\;\lor\hfil\hskip
5.0pt\\\ $\@add@raggedleft}}\hskip 10.00002pt&\hskip
20.00003pt(\lambda(u,\vec{l})\leftrightarrow\theta_{2}).\hfil\hskip
5.0pt&\textrm{by (??)\immediate, (??)\immediate}\\\ {\rm
Phys.~{}Rev.~{}Lett.}{l-theta-8}$\@add@raggedleft}}\hskip
10.00002pt&\models\lnot\forall
u\,(\theta_{1}\lor\theta_{2})\lor\Gamma_{L}\lor\exists^{\mathsf{RHS}}u\,\mathcal{D}_{1}\lor\exists^{\mathsf{RHS}}u\,\mathcal{D}_{2}\;\lor\hfil\hskip
5.0pt\\\ $\@add@raggedleft}}\hskip 10.00002pt&\hskip
20.00003pt(\lambda(u,\vec{l})\leftrightarrow\theta_{2}).\hfil\hskip
5.0pt&\textrm{by (??)\immediate}\\\ {\rm
Phys.~{}Rev.~{}Lett.}{l-theta-9}$\@add@raggedleft}}\hskip
10.00002pt&\models\lnot\forall
u\,(\theta_{1}\lor\theta_{2})\lor\Gamma_{L}\lor\exists^{\mathsf{RHS}}u\,\mathcal{D}_{1}\lor\exists^{\mathsf{RHS}}u\,\mathcal{D}_{2}\;\lor\hfil\hskip
5.0pt\\\ $\@add@raggedleft}}\hskip 10.00002pt&\hskip 20.00003pt\forall
z\,(\lambda(z,\vec{l})\leftrightarrow\theta_{2}[z/u]).\hfil\hskip
5.0pt&\textrm{by (??)\immediate}\textrm{ since }u\notin
FV(\Gamma_{L},\lambda(z,\vec{l}))\\\ {\rm
Phys.~{}Rev.~{}Lett.}{l-theta-10}$\@add@raggedleft}}\hskip
10.00002pt&\models\lnot\theta\lor\Gamma_{L}\lor\mathcal{D}.\hfil\hskip
5.0pt&\textrm{by (??)\immediate, defs. }\theta,\mathcal{D}\\\ \end{array}$

That $u\notin FV(\lambda(z,\vec{l}))$ follows from the precondition $u\notin
FV(\mathcal{G})$. It is used in step (??) to justify that the substitution
$[z/u]$ has only to be applied to $\theta_{2}$ and not to $\lambda(z,\vec{l})$
and, in addition, to justify that $u\notin
FV(\exists^{\mathsf{RHS}}u\,\mathcal{D}_{1})$ and $u\notin
FV(\exists^{\mathsf{RHS}}u\,\mathcal{D}_{2})$, which follow from $u\notin
FV(\lambda(z,\vec{l}))$ and the induction hypotheses that property 5 applies
to $\mathcal{D}_{1}$ and $\mathcal{D}_{2}$.

For case 2, it follows from step (??) that $\models\lnot\forall
w\,\theta\lor\Gamma_{L}\lor\exists^{\mathsf{RHS}}w\,\mathcal{D}$.

Property 3:

${{{{{{{{\begin{array}[]{Z{1.8em}<EMAIL_ADDRESS>Phys.~{}Rev.~{}Lett.}{sig-theta-1}$\@add@raggedleft}}\hskip
10.00002pt&\mathit{PR}(\theta_{1})\subseteq(\mathit{PR}(\Gamma_{L},\lnot\lambda(u,\vec{l}))\cup\mathit{PR}(\lambda))\cap(\mathit{PR}(\Gamma_{R},\rho(u,w,\vec{r}))\cup\mathit{PR}(\rho)).\hfil\hskip
5.0pt&\textrm{IH}\\\ {\rm Phys.~{}Rev.~{}Lett.}{sig-
theta-2}$\@add@raggedleft}}\hskip
10.00002pt&\mathit{PR}(\theta_{2})\subseteq(\mathit{PR}(\Gamma_{L},\lambda(u,\vec{l}))\cup\mathit{PR}(\lambda))\cap(\mathit{PR}(\Gamma_{R},\lnot\rho(u,w,\vec{r}))\cup\mathit{PR}(\rho)).\hfil\hskip
5.0pt&\textrm{IH}\\\ {\rm Phys.~{}Rev.~{}Lett.}{sig-
theta-3}$\@add@raggedleft}}\hskip 10.00002pt&\mathit{PR}(\forall
u\,(\theta_{1}\lor\theta_{1}))\hfil\hskip 5.0pt&\textrm{by (??)\immediate,
(??)\immediate}\\\ {\rm Phys.~{}Rev.~{}Lett.}{sig-
theta-4}$\@add@raggedleft}}\hskip
10.00002pt&\mathit{PR}(\theta)\subseteq(\mathit{PR}(\Gamma_{L})\cup\mathit{PR}(\lambda))\cap(\mathit{PR}(\Gamma_{R})\cup\mathit{PR}(\rho))\hfil\hskip
5.0pt&\textrm{by (??)\immediate, def. }\\!\theta\end{array}$

For case 2 the property follows since $\mathit{PR}(\theta)=\mathit{PR}(\forall
w\,\theta)$.

Property 4:

${{{{{{{{{{{{{{\begin{array}[]{Z{1.8em}<EMAIL_ADDRESS>Phys.~{}Rev.~{}Lett.}{fv-theta-1}$\@add@raggedleft}}\hskip
10.00002pt&FV(\theta_{1})\subseteq(FV(\Gamma_{L},\lnot\lambda(u,\vec{l}))\cup\vec{l})\cap(FV(\Gamma_{R},\rho(u,w,\vec{r}))\cup\vec{r}).\hfil\hskip
5.0pt&\textrm{IH}\\\ {\rm Phys.~{}Rev.~{}Lett.}{fv-
theta-2}$\@add@raggedleft}}\hskip
10.00002pt&FV(\theta_{2})\subseteq(FV(\Gamma_{L},\lambda(u,\vec{l}))\cup\vec{l})\cap(FV(\Gamma_{R},\lnot\rho(u,w,\vec{r}))\cup\vec{r}).\hfil\hskip
5.0pt&\textrm{IH}\\\ {\rm Phys.~{}Rev.~{}Lett.}{fv-
theta-x1}$\@add@raggedleft}}\hskip
10.00002pt&FV(\theta_{1})\subseteq(FV(\Gamma_{L})\cup\vec{l}\cup\\{u\\})\cap(FV(\Gamma_{R})\cup\vec{r}\cup\\{u,w\\}).\hfil\hskip
5.0pt&\textrm{by (??)\immediate}\\\ {\rm Phys.~{}Rev.~{}Lett.}{fv-
theta-x2}$\@add@raggedleft}}\hskip
10.00002pt&FV(\theta_{1})\subseteq(FV(\Gamma_{L})\cup\vec{l}\cup\\{u\\})\cap(FV(\Gamma_{R})\cup\vec{r}\cup\\{u,w\\}).\hfil\hskip
5.0pt&\textrm{by (??)\immediate}\\\ {\rm Phys.~{}Rev.~{}Lett.}{fv-
theta-3}$\@add@raggedleft}}\hskip 10.00002pt&FV(\forall
u\,(\theta_{1}\lor\theta_{2}))\subseteq(FV(\Gamma_{L})\cup\vec{l})\cap(FV(\Gamma_{R})\cup\vec{r}).\hfil\hskip
5.0pt&\textrm{by (??)\immediate, (??)\immediate},\\\ $\@add@raggedleft}}\hskip
10.00002pt&\lx@intercol\hfil\textrm{and $w\notin FV(\Gamma_{L})\cup\vec{l}$ or
$w\in FV(\Gamma_{R})\cup\vec{r}$}\lx@intercol\\\ {\rm
Phys.~{}Rev.~{}Lett.}{fv-theta-4}$\@add@raggedleft}}\hskip
10.00002pt&FV(\theta)\subseteq(FV(\Gamma_{L})\cup\vec{l})\cap(FV(\Gamma_{R})\cup\vec{r}).\hfil\hskip
5.0pt&\textrm{by (??)\immediate, def. }\theta\\\ \end{array}$

For case 2 step (??) has to be replaced by

$FV(\forall w\forall
u\,(\theta_{1}\lor\theta_{2}))\subseteq(FV(\Gamma_{L})\cup\vec{l})\cap(FV(\Gamma_{R})\cup\vec{r}),$

which follows just from (??) and (??). Instead of step (??) we then have
$FV(\forall
w\,\theta)\subseteq(FV(\Gamma_{L})\cup\vec{l})\cap(FV(\Gamma_{R})\cup\vec{r})$.

Property 5: Immediate from the induction hypothesis and the definition of
$\mathcal{D}$.

Property 6:

${{{{{{{{{{{{\begin{array}[]{Z{1.8em}<EMAIL_ADDRESS>Phys.~{}Rev.~{}Lett.}{sig-d-1}$\@add@raggedleft}}\hskip
10.00002pt&\mathit{PR}^{\mathsf{RHS}}(\mathcal{D}_{1})\subseteq(\mathit{PR}(\Gamma_{L},\lnot\lambda(u,\vec{l}))\cup\mathit{PR}(\lambda))\cap(\mathit{PR}(\Gamma_{R},\rho(u,w,\vec{r}))\cup\mathit{PR}(\rho)).\hfil\hskip
5.0pt&\textrm{IH}\\\ {\rm
Phys.~{}Rev.~{}Lett.}{sig-d-2}$\@add@raggedleft}}\hskip
10.00002pt&\mathit{PR}^{\mathsf{RHS}}(\mathcal{D}_{2})\subseteq(\mathit{PR}(\Gamma_{L},\lambda(u,\vec{l}))\cup\mathit{PR}(\lambda))\cap(\mathit{PR}(\Gamma_{R},\lnot\rho(u,w,\vec{r}))\cup\mathit{PR}(\rho)).\hfil\hskip
5.0pt&\textrm{IH}\\\ {\rm
Phys.~{}Rev.~{}Lett.}{sig-d-3}$\@add@raggedleft}}\hskip
10.00002pt&\mathit{PR}(\theta_{2})\subseteq(\mathit{PR}(\Gamma_{L},\lambda(u,\vec{l}))\cup\mathit{PR}(\lambda))\cap(\mathit{PR}(\Gamma_{R},\lnot\rho(u,w,\vec{r}))\cup\mathit{PR}(\rho)).\hfil\hskip
5.0pt&\textrm{IH}\\\ {\rm
Phys.~{}Rev.~{}Lett.}{sig-d-4}$\@add@raggedleft}}\hskip
10.00002pt&\mathit{PR}^{\mathsf{RHS}}(\exists^{\mathsf{RHS}}u\,\mathcal{D}_{1}\lor\exists^{\mathsf{RHS}}u\,\mathcal{D}_{2}\lor\forall
z\,(\lambda(z,\vec{l})\leftrightarrow\theta_{2}[z/u]))\;\subseteq\hfil\hskip
5.0pt\\\ $\@add@raggedleft}}\hskip
10.00002pt&(\mathit{PR}(\Gamma_{L})\cup\mathit{PR}(\lambda))\cap(\mathit{PR}(\Gamma_{R})\cup\mathit{PR}(\rho))\hfil\hskip
5.0pt&\textrm{by (??)\immediate--(??)\immediate}\\\ {\rm
Phys.~{}Rev.~{}Lett.}{sig-d-5}$\@add@raggedleft}}\hskip
10.00002pt&\mathit{PR}^{\mathsf{RHS}}(\mathcal{D})\subseteq(\mathit{PR}(\Gamma_{L})\cup\mathit{PR}(\lambda))\cap(\mathit{PR}(\Gamma_{R})\cup\mathit{PR}(\rho))\hfil\hskip
5.0pt&\textrm{by (??)\immediate, def. }\mathcal{D}\end{array}$

For case 2 the property follows since
$\mathit{PR}^{\mathsf{RHS}}(\mathcal{D})=\mathit{PR}^{\mathsf{RHS}}(\exists^{\mathsf{RHS}}w\,\mathcal{D})$.

Property 7:

${{{{{{{{{{{{{{{{{{{{\begin{array}[]{Z{1.8em}<EMAIL_ADDRESS>Phys.~{}Rev.~{}Lett.}{fv-d-1}$\@add@raggedleft}}\hskip
10.00002pt&FV^{\mathsf{RHS}}(\mathcal{D}_{1})\subseteq(FV(\Gamma_{L},\lnot\lambda(u,\vec{l}))\cup\vec{l})\cap(FV(\Gamma_{R},\rho(u,w,\vec{r}))\cup\vec{r}).\hfil\hskip
5.0pt&\textrm{IH}\\\ {\rm
Phys.~{}Rev.~{}Lett.}{fv-d-2}$\@add@raggedleft}}\hskip
10.00002pt&FV^{\mathsf{RHS}}(\mathcal{D}_{2})\subseteq(FV(\Gamma_{L},\lambda(u,\vec{l}))\cup\vec{l})\cap(FV(\Gamma_{R},\lnot\rho(u,w,\vec{r}))\cup\vec{r}).\hfil\hskip
5.0pt&\textrm{IH}\\\ {\rm
Phys.~{}Rev.~{}Lett.}{fv-d-3}$\@add@raggedleft}}\hskip
10.00002pt&FV(\theta_{2})\subseteq(FV(\Gamma_{L},\lambda(u,\vec{l}))\cup\vec{l})\cap(FV(\Gamma_{R},\lnot\rho(u,w,\vec{r}))\cup\vec{r}).\hfil\hskip
5.0pt&\textrm{IH}\\\ {\rm
Phys.~{}Rev.~{}Lett.}{fv-d-1x}$\@add@raggedleft}}\hskip
10.00002pt&FV^{\mathsf{RHS}}(\mathcal{D}_{1})\subseteq(FV(\Gamma_{L})\cup\vec{l}\cup\\{u\\})\cap(FV(\Gamma_{R})\cup\vec{r}\cup\\{u,w\\}).\hfil\hskip
5.0pt&\textrm{by (??)\immediate}\\\ {\rm
Phys.~{}Rev.~{}Lett.}{fv-d-2x}$\@add@raggedleft}}\hskip
10.00002pt&FV^{\mathsf{RHS}}(\mathcal{D}_{2})\subseteq(FV(\Gamma_{L})\cup\vec{l}\cup\\{u\\})\cap(FV(\Gamma_{R})\cup\vec{r}\cup\\{u,w\\}).\hfil\hskip
5.0pt&\textrm{by (??)\immediate}\\\ {\rm
Phys.~{}Rev.~{}Lett.}{fv-d-3x}$\@add@raggedleft}}\hskip
10.00002pt&FV(\theta_{2})\subseteq(FV(\Gamma_{L})\cup\vec{l}\cup\\{u\\})\cap(FV(\Gamma_{R})\cup\vec{r}\cup\\{u,w\\}).\hfil\hskip
5.0pt&\textrm{by (??)\immediate}\\\ {\rm
Phys.~{}Rev.~{}Lett.}{fv-d-4}$\@add@raggedleft}}\hskip
10.00002pt&FV^{\mathsf{RHS}}(\exists^{\mathsf{RHS}}u\,\mathcal{D}_{1}\lor\exists^{\mathsf{RHS}}u\,\mathcal{D}_{2}\lor\forall
z\,(\lambda(z,\vec{l})\leftrightarrow\theta_{2}[z/u]))\;\subseteq\hfil\hskip
5.0pt\\\ $\@add@raggedleft}}\hskip
10.00002pt&(FV(\Gamma_{L})\cup\vec{l})\cap(FV(\Gamma_{R})\cup\vec{r}).\hfil\hskip
5.0pt&\textrm{by (??)\immediate, (??)\immediate, (??)\immediate,}\\\
$\@add@raggedleft}}\hskip 10.00002pt&\lx@intercol\hfil\textrm{and $w\notin
FV(\Gamma_{L})\cup\vec{l}$ or $w\in FV(\Gamma_{R})\cup\vec{r}$}\lx@intercol\\\
{\rm Phys.~{}Rev.~{}Lett.}{fv-d-5}$\@add@raggedleft}}\hskip
10.00002pt&FV^{\mathsf{RHS}}(\mathcal{D})\subseteq(FV(\Gamma_{L})\cup\vec{l})\cap(FV(\Gamma_{R})\cup\vec{r}).\hfil\hskip
5.0pt&\textrm{by (??)\immediate, def. }\mathcal{D}\end{array}$

For case 2 step (??) has to be replaced by

$\begin{array}[]{l}FV^{\mathsf{RHS}}(\exists^{\mathsf{RHS}}w(\exists^{\mathsf{RHS}}u\,\mathcal{D}_{1}\lor\exists^{\mathsf{RHS}}u\,\mathcal{D}_{2}\lor\forall
z\,(\lambda(z,\vec{l})\leftrightarrow\theta_{2}[z/u])))\;\subseteq\\\
(FV(\Gamma_{L})\cup\vec{l})\cap(FV(\Gamma_{R})\cup\vec{r}),\end{array}$

which follows just from (??), (??), (??). Instead of step (??) we then have
$FV^{\mathsf{RHS}}(\exists^{\mathsf{RHS}}w\,\mathcal{D})\subseteq(FV(\Gamma_{L})\cup\vec{l})\cap(FV(\Gamma_{R})\cup\vec{r})$.

This completes the verification of correctness, and thus ends our discussion
of this case.

We now turn to the base of the induction along with the other inductive cases.

##### Cases where the principal formulas are in the $\Gamma_{L}$ or
$\Gamma_{R}$ partition.

The inductive cases where the principal formulas are in the $\Gamma_{L}$ or
$\Gamma_{R}$ partition can be conveniently specified in the form of rules that
lead from induction hypotheses of the form
$\vdash\Gamma_{L};\;\;\Gamma_{R};\;\;\mathcal{G}\;:\;\langle\theta,\mathcal{D}\rangle$
as premises to an induction conclusion of the same form. Base cases can there
be taken just as such rules without premises. The axioms and rules shown below
correspond to the those of the calculus, but replicated for each possible way
in which the partitions $\Gamma_{L}$, $\Gamma_{R}$ or $\mathcal{G}$ of the
conclusion may contain the principal formula(s). To verify that properties 1–7
are preserved by each of the shown constructions is in general
straightforward, such that we only have annotated a few subtleties that may
not be evident.

  1. (1)

$\begin{array}[]{rcl}\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small{Ax}}&&\hskip
20.00003pt\raisebox{-8.61108pt}[0.0pt][0.0pt]{$\varphi\textit{ a positive
literal}$}\\\
\cline{2-2}\cr&\vdash\Gamma_{L},\varphi,\lnot\varphi;\;\;\Gamma_{R};\;\;\mathcal{G}\;:\;\langle\top,\bot\rangle\\\
\end{array}$

  2. (2)

$\begin{array}[]{rcl}\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small{Ax}}&&\hskip
20.00003pt\raisebox{-8.61108pt}[0.0pt][0.0pt]{$\varphi\textit{ a positive
literal}$}\\\
\cline{2-2}\cr&\vdash\Gamma_{L};\;\;\Gamma_{R},\varphi,\lnot\varphi;\;\;\mathcal{G}\;:\;\langle\bot,\bot\rangle\end{array}$

  3. (3)

$\begin{array}[]{rcl}\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small{Ax}}&&\hskip
20.00003pt\raisebox{-8.61108pt}[0.0pt][0.0pt]{$\varphi\textit{ a literal}$}\\\
\cline{2-2}\cr&\vdash\Gamma_{L},\varphi;\;\;\Gamma_{R},\lnot\varphi;\;\;\mathcal{G}\;:\;\langle\varphi,\bot\rangle\end{array}$

  4. (4)

$\begin{array}[]{rc}\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small$\top$}\\\
\cline{2-2}\cr&\vdash\Gamma_{L},\top;\;\;\Gamma_{R};\;\;\mathcal{G}\;:\;\langle\top,\bot\rangle\end{array}$

  5. (5)

$\begin{array}[]{rc}\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small$\top$}\\\
\cline{2-2}\cr&\vdash\Gamma_{L};\;\;\Gamma_{R},\top;\;\;\mathcal{G}\;:\;\langle\bot,\bot\rangle\end{array}$

  6. (6)

$\begin{array}[t]{rc}\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small$\lor$}&\vdash\Gamma_{L},\varphi_{1},\varphi_{2};\;\;\Gamma_{R};\;\;\mathcal{G}\;:\;\langle\theta,\mathcal{D}\rangle\\\
\cline{2-2}\cr&\vdash\Gamma_{L},\varphi_{1}\lor\varphi_{2};\;\;\Gamma_{R};\;\;\mathcal{G}\;:\;\langle\theta,\mathcal{D}\rangle\end{array}$

  7. (7)

$\begin{array}[t]{rc}\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small$\lor$}&\vdash\Gamma_{L};\;\;\Gamma_{R},\varphi_{1},\varphi_{2};\;\;\mathcal{G}\;:\;\langle\theta,\mathcal{D}\rangle\\\
\cline{2-2}\cr&\vdash\Gamma_{L};\;\;\Gamma_{R},\varphi_{1}\lor\varphi_{2};\;\;\mathcal{G}\;:\;\langle\theta,\mathcal{D}\rangle\end{array}$

  8. (8)

$\begin{array}[t]{rc@{\hspace{2em}}c}\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small$\land$}&\vdash\Gamma_{L},\varphi_{1};\;\;\Gamma_{R};\;\;\mathcal{G}\;:\;\langle\theta_{1},\mathcal{D}_{1}\rangle\hfil\hskip
20.00003pt&\vdash\Gamma_{L},\varphi_{2};\;\;\Gamma_{R};\;\;\mathcal{G}\;:\;\langle\theta_{2},\mathcal{D}_{2}\rangle\\\
\cline{2-3}\cr&\lx@intercol\hfil\vdash\Gamma_{L},\varphi_{1}\land\varphi_{2};\;\;\Gamma_{R};\;\;\mathcal{G}\;:\;\langle\theta_{1}\land\theta_{2},\mathcal{D}_{1}\lor\mathcal{D}_{2}\rangle\hfil\lx@intercol\end{array}$

  9. (9)

$\begin{array}[t]{rc@{\hspace{2em}}c}\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small$\land$}&\vdash\Gamma_{L};\;\;\Gamma_{R},\varphi_{1};\;\;\mathcal{G}\;:\;\langle\theta_{1},\mathcal{D}_{1}\rangle\hfil\hskip
20.00003pt&\vdash\Gamma_{L};\;\;\Gamma_{R},\varphi_{2};\;\;\mathcal{G}\;:\;\langle\theta_{2},\mathcal{D}_{2}\rangle\\\
\cline{2-3}\cr&\lx@intercol\hfil\vdash\Gamma_{L};\;\;\Gamma_{R},\varphi_{1}\land\varphi_{2};\;\;\mathcal{G}\;:\;\langle\theta_{1}\lor\theta_{2},\mathcal{D}_{1}\lor\mathcal{D}_{2}\rangle\hfil\lx@intercol\end{array}$

  10. (10)

$\begin{array}[t]{rc}\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small$\exists$}&\vdash\Gamma_{L},\varphi[t/x],\exists
x\,\varphi;\;\;\Gamma_{R};\;\;\mathcal{G}\;:\;\langle\theta,\mathcal{D}\rangle\\\
\cline{2-2}\cr&\vdash\Gamma_{L},\exists
x\,\varphi;\;\;\Gamma_{R};\;\;\mathcal{G}\;:\;\langle\theta^{\prime},\mathcal{D}^{\prime}\rangle,\end{array}$

where the values of $\theta^{\prime}$ and $\mathcal{D}^{\prime}$ depend on
occurrences of $t$:

     * •

If $t\in FV(\Gamma_{L},\exists x\,\varphi)\cup\vec{l}$, then
$\theta^{\prime}\mathrel{:=}\theta$ and
$\mathcal{D}^{\prime}\mathrel{:=}\mathcal{D}$.

     * •

Else it holds that $t\notin FV(\Gamma_{L},\exists x\,\varphi)\cup\vec{l}$.
Then $\theta^{\prime}\mathrel{:=}\exists t\,\theta$ and
$\mathcal{D}^{\prime}\mathrel{:=}\exists^{\mathsf{RHS}}t\,\mathcal{D}$.

  11. (11)

$\begin{array}[t]{rc}\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small$\exists$}&\vdash\Gamma_{L};\;\;\Gamma_{R},\varphi[t/x],\exists
x\,\varphi;\;\;\mathcal{G}\;:\;\langle\theta,\mathcal{D}\rangle\\\
\cline{2-2}\cr&\vdash\Gamma_{L};\;\;\Gamma_{R},\exists
x\,\varphi;\;\;\mathcal{G}\;:\;\langle\theta^{\prime},\mathcal{D}^{\prime}\rangle,\end{array}$

where the values of $\theta^{\prime}$ and $\mathcal{D}^{\prime}$ depend on
occurrences of $t$:

     * •

If $t\in FV(\Gamma_{R},\exists x\,\varphi)\cup\vec{r}$, then
$\theta^{\prime}\mathrel{:=}\theta$ and
$\mathcal{D}^{\prime}\mathrel{:=}\mathcal{D}$.

     * •

Else it holds that $t\notin FV(\Gamma_{R},\exists x\,\varphi)\cup\vec{r}$.
Then $\theta^{\prime}\mathrel{:=}\forall t\,\theta$ and
$\mathcal{D}^{\prime}\mathrel{:=}\exists^{\mathsf{RHS}}t\,\mathcal{D}$.

  12. (12)

$\begin{array}[t]{rcl}\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small$\forall$}&\vdash\Gamma_{L},\varphi[y/x];\;\;\Gamma_{R};\;\;\mathcal{G}\;:\;\langle\theta,\mathcal{D}\rangle&\hskip
20.00003pt\raisebox{-8.61108pt}[0.0pt][0.0pt]{$y\notin FV(\Gamma_{L},\forall
x\,\varphi,\Gamma_{R},\mathcal{G})$}\\\
\cline{2-2}\cr&\vdash\Gamma_{L},\forall
x\,\varphi;\;\;\Gamma_{R};\;\;\mathcal{G}\;:\;\langle\theta,\mathcal{D}\rangle\end{array}$

  13. (13)

$\begin{array}[t]{rcl}\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small$\forall$}&\vdash\Gamma_{L};\;\;\Gamma_{R},\varphi[y/x];\;\;\mathcal{G}\;:\;\langle\theta,\mathcal{D}\rangle&\hskip
20.00003pt\raisebox{-8.61108pt}[0.0pt][0.0pt]{$y\notin
FV(\Gamma_{L},\Gamma_{R},\forall x\,\varphi,\mathcal{G})$}\\\
\cline{2-2}\cr&\vdash\Gamma_{L};\;\;\Gamma_{R},\forall
x\,\varphi;\;\;\mathcal{G}\;:\;\langle\theta,\mathcal{D}\rangle\end{array}$

  14. (14)

$\begin{array}[t]{rcl}\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small{Ref}}&\vdash
t\neq
t,\Gamma_{L};\;\;\Gamma_{R};\;\;\mathcal{G}\;:\;\langle\theta,\mathcal{D}\rangle&\hskip
20.00003pt\raisebox{-8.61108pt}[0.0pt][0.0pt]{$t\in
FV(\Gamma_{L})\cup\vec{l}$}\\\
\cline{2-2}\cr&\vdash\Gamma_{L};\;\;\Gamma_{R};\;\;\mathcal{G}\;:\;\langle\theta,\mathcal{D}\rangle\end{array}$

  15. (15)

$\begin{array}[t]{rcl}\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small{Ref}}&\vdash\Gamma_{L};\;\;t\neq
t,\Gamma_{R};\;\;\mathcal{G}\;:\;\langle\theta,\mathcal{D}\rangle&\hskip
20.00003pt\raisebox{-8.61108pt}[0.0pt][0.0pt]{$t\notin
FV(\Gamma_{L})\cup\vec{l}$}\\\
\cline{2-2}\cr&\vdash\Gamma_{L};\;\;\Gamma_{R};\;\;\mathcal{G}\;:\;\langle\theta,\mathcal{D}\rangle\end{array}$

  16. (16)

$\begin{array}[t]{rcl}\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small{Repl}}&\vdash
t\neq
u,\varphi[u/x],\varphi[t/x],\Gamma_{L};\;\;\Gamma_{R};\;\;\mathcal{G}\;:\;\langle\theta,\mathcal{D}\rangle&\hskip
20.00003pt\raisebox{-8.61108pt}[0.0pt][0.0pt]{$\varphi\textit{ a negative
literal}$}\\\ \cline{2-2}\cr&\vdash t\neq
u,\varphi[t/x],\Gamma_{L};\;\;\Gamma_{R};\;\;\mathcal{G}\;:\;\langle\theta,\mathcal{D}\rangle\end{array}$

  17. (17)

$\begin{array}[t]{rcl}\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small{Repl}}&\vdash
t\neq
u,\Gamma_{L};\;\;\varphi[u/x],\varphi[t/x],\Gamma_{R};\;\;\mathcal{G}\;:\;\langle\theta,\mathcal{D}\rangle&\hskip
20.00003pt\raisebox{-8.61108pt}[0.0pt][0.0pt]{$\varphi\textit{ a negative
literal}$}\\\ \cline{2-2}\cr&\vdash t\neq
u,\Gamma_{L};\;\;\varphi[t/x],\Gamma_{R};\;\;\mathcal{G}\;:\;\langle\theta^{\prime},\mathcal{D}^{\prime}\rangle,\end{array}$

where the values of $\theta^{\prime}$ and $\mathcal{D}^{\prime}$ depend on
occurrences of $t$ and $u$:

     * •

If $t\notin FV(\varphi[t/x],\Gamma_{R})\cup\vec{r}$, then
$\theta^{\prime}\mathrel{:=}\theta$ and
$\mathcal{D}^{\prime}\mathrel{:=}\mathcal{D}$. In this subcase the
precondition $t\notin FV(\varphi[t/x])$ implies that $x\notin FV(\varphi)$ and
thus $\varphi[u/x]=\varphi[t/x]$.

     * •

If $t,u\in FV(\varphi[t/x],\Gamma_{R})\cup\vec{r}$, then
$\theta^{\prime}\mathrel{:=}\theta\lor t\neq u$ and
$\mathcal{D}^{\prime}\mathrel{:=}\mathcal{D}$.

     * •

Else it holds that $t\in FV(\varphi[t/x],\Gamma_{R})\cup\vec{r}$ and $u\notin
FV(\varphi[t/x],\Gamma_{R})\cup\vec{r}$. Then
$\theta^{\prime}\mathrel{:=}\theta[t/u]$ and
$\mathcal{D}^{\prime}\mathrel{:=}\mathcal{D}[t/u]^{\mathsf{RHS}}$. For this
subcase, to derive property 1 it is used that the precondition
$u\notin\varphi[t/x]$ implies that $\varphi[u/x][t/u]=\varphi[t/x]$.

  18. (18)

$\begin{array}[t]{rcl}\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small{Repl}}&\vdash\Gamma_{L};\;\;t\neq
u,\varphi[u/x],\varphi[t/x],\Gamma_{R};\;\;\mathcal{G}\;:\;\langle\theta,\mathcal{D}\rangle&\hskip
20.00003pt\raisebox{-8.61108pt}[0.0pt][0.0pt]{$\varphi\textit{ a negative
literal}$}\\\ \cline{2-2}\cr&\vdash\Gamma_{L};\;\;t\neq
u,\varphi[t/x],\Gamma_{R};\;\;\mathcal{G}\;:\;\langle\theta,\mathcal{D}\rangle\end{array}$

  19. (19)

$\begin{array}[t]{rcl}\raisebox{-8.61108pt}[0.0pt][0.0pt]{\small{Repl}}&\vdash\varphi[u/x],\varphi[t/x],\Gamma_{L};\;\;t\neq
u;\Gamma_{R};\;\;\mathcal{G}\;:\;\langle\theta,\mathcal{D}\rangle&\hskip
20.00003pt\raisebox{-8.61108pt}[0.0pt][0.0pt]{$\varphi\textit{ a negative
literal}$}\\\ \cline{2-2}\cr&\vdash\varphi[t/x],\Gamma_{L};\;\;t\neq
u,\Gamma_{R};\;\;\mathcal{G}\;:\;\langle\theta^{\prime},\mathcal{D}^{\prime}\rangle,\end{array}$

where the values of $\theta^{\prime}$ and $\mathcal{D}^{\prime}$ depend on
occurrences of $t$ and $u$:

     * •

If $t\notin FV(\varphi[t/x],\Gamma_{L})\cup\vec{l}$, then
$\theta^{\prime}\mathrel{:=}\theta$ and
$\mathcal{D}^{\prime}\mathrel{:=}\mathcal{D}$. In this subcase the
precondition $t\notin FV(\varphi[t/x])$ implies that $x\notin FV(\varphi)$ and
thus $\varphi[u/x]=\varphi[t/x]$.

     * •

If $t,u\in FV(\varphi[t/x],\Gamma_{L})\cup\vec{l}$, then
$\theta^{\prime}\mathrel{:=}\theta\land t=u$ and
$\mathcal{D}^{\prime}\mathrel{:=}\mathcal{D}$.

     * •

Else it holds that $t\in FV(\varphi[t/x],\Gamma_{L})\cup\vec{l}$ and $u\notin
FV(\varphi[t/x],\Gamma_{L})\cup\vec{l}$. Then
$\theta^{\prime}\mathrel{:=}\theta[t/u]$ and
$\mathcal{D}^{\prime}\mathrel{:=}\mathcal{D}[t/u]^{\mathsf{RHS}}$. To derive
property 2 for this subcase, that is,
$\models\lnot\theta[t/u]\lor\varphi[t/x],\Gamma_{L}\lor\mathcal{D}[t/u]^{\mathsf{RHS}}$,
it is required that $u\notin FV(\mathcal{D}[t/u]^{\mathsf{RHS}})$, which
follows from the precondition $u\notin\vec{l}$ of the subcase.

This completes the proof of Theorem 46.