$\mathcal{M},w_{2}\nVdash B{}^{\oplus}$, so we are left to show that
$\mathcal{M},w_{2}\nVdash A{}^{\oplus}$. Indeed, suppose that
$\mathcal{M},w_{2}\Vdash A{}^{\oplus}$ holds. By IH there exists
$w_{3}\mathrel{\geq}w_{2}$ such that either $\mathcal{M},w_{3}\Vdash
A{}^{\oplus}$ or $\mathcal{M},w_{3}\Vdash A{}^{\ominus}$ holds but not both.
However, by monotonicity (Lem. 42) —given that both $\mathcal{M},w_{2}\Vdash
A{}^{\oplus}$ and $\mathcal{M},w_{2}\Vdash A{}^{\ominus}$ hold— we know that
both $\mathcal{M},w_{3}\Vdash A{}^{\oplus}$ and $\mathcal{M},w_{3}\Vdash
A{}^{\ominus}$ hold, a contradiction.

  4. 4.

Negation, $P=(\neg A){}^{+}$ and $P{}^{\sim}=(\neg A){}^{-}$. By IH there is a
world $w^{\prime}\mathrel{\geq}w$ such that either
$\mathcal{M},w^{\prime}\Vdash A{}^{\oplus}$ or $\mathcal{M},w^{\prime}\Vdash
A{}^{\ominus}$ hold but not both, so we consider two cases:

    1. 4.1

If $\mathcal{M},w^{\prime}\Vdash A{}^{\oplus}$ and
$\mathcal{M},w^{\prime}\nVdash A{}^{\ominus}$, then
$\mathcal{M},w^{\prime}\Vdash(\neg A){}^{-}$ and
$\mathcal{M},w^{\prime}\nVdash(\neg A){}^{+}$.

    2. 4.2

If $\mathcal{M},w^{\prime}\Vdash A{}^{\ominus}$ and
$\mathcal{M},w^{\prime}\nVdash A{}^{\oplus}$, then
$\mathcal{M},w^{\prime}\Vdash(\neg A){}^{+}$ and
$\mathcal{M},w^{\prime}\nVdash(\neg A){}^{-}$.

  5. 5.

Classical proposition, $P=A{}^{\oplus}$ and $P{}^{\sim}=A{}^{\ominus}$. By IH
there is a world $w^{\prime}\mathrel{\geq}w$ such that either
$\mathcal{M},w^{\prime}\Vdash A{}^{+}$ or $\mathcal{M},w^{\prime}\Vdash
A{}^{-}$ but not both. We consider two subcases:

    1. 5.1

If $\mathcal{M},w^{\prime}\Vdash A{}^{+}$ and $\mathcal{M},w^{\prime}\nVdash
A{}^{-}$, then we claim that $\mathcal{M},w^{\prime}\Vdash A{}^{\oplus}$ and
$\mathcal{M},w^{\prime}\nVdash A{}^{\ominus}$. Indeed, let us prove each
condition:

      1. 5.1.1

In order to show that $\mathcal{M},w^{\prime}\Vdash A{}^{\oplus}$, it suffices
to check that given $w^{\prime\prime}\mathrel{\geq}w^{\prime}$ we have that
$\mathcal{M},w^{\prime\prime}\nVdash A{}^{-}$. Indeed, suppose that
$\mathcal{M},w^{\prime\prime}\Vdash A{}^{-}$. Then by IH there exists
$w^{\prime\prime\prime}\mathrel{\geq}w^{\prime\prime}$ such that either
$\mathcal{M},w^{\prime\prime\prime}\Vdash A{}^{+}$ or
$\mathcal{M},w^{\prime\prime\prime}\Vdash A{}^{-}$ but not both. However, by
monotonicity (Lem. 42) —given that both $\mathcal{M},w^{\prime}\Vdash A{}^{+}$
and $\mathcal{M},w^{\prime\prime}\Vdash A{}^{-}$ hold, and
$w^{\prime}\mathrel{\leq}w^{\prime\prime}\mathrel{\leq}w^{\prime\prime\prime}$—
we know that both $\mathcal{M},w^{\prime\prime\prime}\Vdash A{}^{+}$ and
$\mathcal{M},w^{\prime\prime\prime}\Vdash A{}^{-}$ hold, a contradiction.

      2. 5.1.2

In order to show that $\mathcal{M},w^{\prime}\nVdash A{}^{\ominus}$, it
suffices to note that $\mathcal{M},w^{\prime}\Vdash A{}^{+}$, which
contradicts the definition of $\mathcal{M},w^{\prime}\Vdash A{}^{\ominus}$,
given that accessibility is reflexive, i.e.
$w^{\prime}\mathrel{\leq}w^{\prime}$.

    2. 5.2

If $\mathcal{M},w^{\prime}\Vdash A{}^{-}$ and $\mathcal{M},w^{\prime}\nVdash
A{}^{+}$, then we claim that $\mathcal{M},w^{\prime}\Vdash A{}^{\ominus}$ and
$\mathcal{M},w^{\prime}\nVdash A{}^{\oplus}$. Indeed, let us prove each
condition:

      1. 5.2.1

In order to show that $\mathcal{M},w^{\prime}\Vdash A{}^{\ominus}$, it
suffices to check that given $w^{\prime\prime}\mathrel{\geq}w^{\prime}$ we
have that $\mathcal{M},w^{\prime\prime}\nVdash A{}^{+}$. Indeed, suppose that
$\mathcal{M},w^{\prime\prime}\Vdash A{}^{+}$. Then by IH there exists
$w^{\prime\prime\prime}\mathrel{\geq}w^{\prime\prime}$ such that either
$\mathcal{M},w^{\prime\prime\prime}\Vdash A{}^{+}$ and
$\mathcal{M},w^{\prime\prime\prime}\Vdash A{}^{-}$ but not both. However, by
monotonicity (Lem. 42) —given that both $\mathcal{M},w^{\prime\prime}\Vdash
A{}^{+}$ and $\mathcal{M},w^{\prime}\Vdash A{}^{-}$ hold, and
$w^{\prime}\mathrel{\leq}w^{\prime\prime}\mathrel{\leq}w^{\prime\prime\prime}$—
we know that both $\mathcal{M},w^{\prime\prime\prime}\Vdash A{}^{+}$ and
$\mathcal{M},w^{\prime\prime\prime}\Vdash A{}^{-}$ hold, a contradiction.

      2. 5.2.2

In order to show that $\mathcal{M},w^{\prime}\nVdash A{}^{\oplus}$ it suffices
to note that $\mathcal{M},w^{\prime}\Vdash A{}^{-}$, which contradicts the
definition of $\mathcal{M},w^{\prime}\Vdash A{}^{\oplus}$, given that
accessibility is reflexive, i.e. $w^{\prime}\mathrel{\leq}w^{\prime}$.

∎

######  Lemma 44 (Non-contradiction of forcing).

If $\mathcal{M},w\Vdash P$ then $\mathcal{M},w\nVdash P{}^{\sim}$.

###### Proof.

Suppose that both $\mathcal{M},w\Vdash P$ and $\mathcal{M},w\Vdash P{}^{\sim}$
hold. By stabilization (Lem. 43) there is a world $w^{\prime}\mathrel{\geq}w$
such that either $\mathcal{M},w^{\prime}\Vdash P$ or
$\mathcal{M},w^{\prime}\Vdash P{}^{\sim}$ but not both. However, by
monotonicity (Lem. 42) we know that both $\mathcal{M},w^{\prime}\Vdash P$ and
$\mathcal{M},w^{\prime}\Vdash P{}^{\sim}$ must hold, a contradiction. ∎

###  .3 Proof of Soundness of prk with respect to the Kripke semantics

######  Lemma 45 (Rule of classical forcing).

  1. 1.

$(\mathcal{M},w\Vdash A{}^{\oplus})$ if and only if, for all
$w^{\prime}\mathrel{\geq}w$, $(\mathcal{M},w^{\prime}\Vdash A{}^{\ominus})$
implies $(\mathcal{M},w^{\prime}\Vdash A{}^{+})$.

  2. 2.

$(\mathcal{M},w\Vdash A{}^{\ominus})$ if and only if, for all
$w^{\prime}\mathrel{\geq}w$, $(\mathcal{M},w^{\prime}\Vdash A{}^{\oplus})$
implies $(\mathcal{M},w^{\prime}\Vdash A{}^{-})$.

###### Proof.

We only prove the first item. The second one is symmetric, flipping all the
signs.

  * $(\Rightarrow)$

Suppose that $\mathcal{M},w\Vdash A{}^{\oplus}$, let
$w^{\prime}\mathrel{\geq}w$, and let us show that the implication
$(\mathcal{M},w^{\prime}\Vdash
A{}^{\ominus})\implies(\mathcal{M},w^{\prime}\Vdash A{}^{+})$ holds. In fact,
the implication holds vacuously, given that $\mathcal{M},w^{\prime}\Vdash
A{}^{\oplus}$ by monotonicity (Lem. 9), and therefore
$\mathcal{M},w^{\prime}\nVdash A{}^{\ominus}$ by non-contradiction (Lem. 9).

  * $(\Leftarrow)$

Suppose that for every $w^{\prime}\mathrel{\geq}w$ the implication
$(\mathcal{M},w^{\prime}\Vdash
A{}^{\ominus})\implies(\mathcal{M},w^{\prime}\Vdash A{}^{+})$ holds. Let us
show that $\mathcal{M},w\Vdash A{}^{\oplus}$ holds, i.e. that for every
$w^{\prime}\mathrel{\geq}w$ we have that $\mathcal{M},w^{\prime}\nVdash
A{}^{-}$. Let $w^{\prime}$ be a world such that $w^{\prime}\mathrel{\geq}w$
and, by contradiction, suppose that $\mathcal{M},w^{\prime}\Vdash A{}^{-}$.
Then by non-contradiction (Lem. 9) we have that $\mathcal{M},w^{\prime}\nVdash
A{}^{+}$. Hence, to obtain a contradiction, using the implication of the
hypothesis, it suffices to show that $\mathcal{M},w^{\prime}\Vdash
A{}^{\ominus}$, that is, that for every
$w^{\prime\prime}\mathrel{\geq}w^{\prime}$ we have that
$\mathcal{M},w^{\prime\prime}\nVdash A{}^{+}$. Indeed, let
$w^{\prime\prime}\mathrel{\geq}w^{\prime}$. By monotonicity (Lem. 9)
$\mathcal{M},w^{\prime\prime}\Vdash A{}^{-}$, so by non-contradiction (Lem. 9)
$\mathcal{M},w^{\prime\prime}\nVdash A{}^{+}$, as required.

∎

######  Proposition 46 (Soundness).

If $\Gamma\vdash P$ is provable in prk, then $\Gamma\Vvdash P$.

###### Proof.

By induction on the derivation of $\Gamma\vdash P$. The axiom rule, and the
introduction and elimination rules for conjunction, disjunction, and negation
are straightforward using the definition of Kripke model. The interesting
cases are the following rules:

  1. 1.

Abs: let $\Gamma\vdash Q$ be derived from $\Gamma\vdash P$ and $\Gamma\vdash
P{}^{\sim}$ for some strong proposition $P$. Suppose that
$\mathcal{M},w\Vvdash\Gamma$ holds in an arbitrary world $w$ under an
arbitrary Kripke model $\mathcal{M}$, and let us show that
$\mathcal{M},w\Vdash Q$. Note that by IH we have that $\mathcal{M},w\Vdash P$
and $\mathcal{M},w\Vdash P{}^{\sim}$. But this is impossible by non-
contradiction (Lem. 9). Hence $\mathcal{M},w\Vdash Q$.

  2. 2.

IC+: let $\Gamma\vdash A{}^{\oplus}$ be derived from
$\Gamma,A{}^{\ominus}\vdash A{}^{+}$. Suppose that
$\mathcal{M},w\Vvdash\Gamma$ holds in an arbitrary world $w$ under an
arbitrary Kripke model $\mathcal{M}$, and let us show that
$\mathcal{M},w\Vdash A{}^{\oplus}$. We claim that for every
$w^{\prime}\mathrel{\geq}w$ the implication $(\mathcal{M},w^{\prime}\Vdash
A{}^{\ominus})\implies(\mathcal{M},w^{\prime}\Vdash A{}^{+})$ holds. Indeed,
suppose that $\mathcal{M},w^{\prime}\Vdash A{}^{\ominus}$. Moreover, by
monotonicity (Lem. 9), we have that $\mathcal{M},w^{\prime}\Vvdash\Gamma$. So
$\mathcal{M},w^{\prime}\Vvdash\Gamma,A{}^{\ominus}$ holds. Hence by IH we have
that $\mathcal{M},w^{\prime}\Vdash A{}^{+}$. Given that the implication
$(\mathcal{M},w^{\prime}\Vdash
A{}^{\ominus})\implies(\mathcal{M},w^{\prime}\Vdash A{}^{+})$ holds for all
$w^{\prime}\mathrel{\geq}w$, using the rule of classical forcing (Lem. 10) we
conclude that $\mathcal{M},w\Vdash A{}^{\oplus}$, as required.

  3. 3.

IC-: similar to the IC+ case.

  4. 4.

EC+, EC-: similar to the Abs case.

∎

###  .4 Auxiliary lemmas to prove Completeness of prk with respect to the
Kripke semantics

In the following proof we use an encoding of falsity with the pure proposition
$\bot\,\mathrel{\overset{\mathrm{def}}{=}}\,(\alpha_{0}\land\neg\alpha_{0})$
for some fixed propositional variable $\alpha_{0}$. Remark that
$\Gamma\vdash\bot{}^{\ominus}$ is provable, being an instance of the law of
non-contradiction (Ex. 3).

######  Lemma 47 (Consistent extension).

Let $\Gamma$ be a consistent set, and let $P$ be a proposition. Then
$\Gamma\cup\\{P\\}$ and $\Gamma\cup\\{P{}^{\sim}\\}$ are not both
inconsistent.

###### Proof.

Suppose that $\Gamma\cup\\{P\\}$ and $\Gamma\cup\\{P{}^{\sim}\\}$ are both
inconsistent. In particular we have that $\Gamma,P\vdash\bot{}^{\oplus}$ and
$\Gamma,P{}^{\sim}\vdash\bot{}^{\oplus}$. By the projection lemma (Lem. 4) we
have that $\Gamma,\ocircle{P}\vdash\bot{}^{\oplus}$ and
$\Gamma,\ocircle{P{}^{\sim}}\vdash\bot{}^{\oplus}$. Moreover, by
contraposition (Lem. 2) we have that
$\Gamma,\bot{}^{\ominus}\vdash\ocircle{P{}^{\sim}}$ and
$\Gamma,\bot{}^{\ominus}\vdash\ocircle{P}$. Since $\bot{}^{\ominus}$ is
provable (Ex. 3), applying the cut rule (Lem. 2) we have that
$\Gamma\vdash\ocircle{P{}^{\sim}}$ and $\Gamma\vdash\ocircle{P}$. The
generalized absurdity rule allows us to derive $\Gamma\vdash Q$ for any $Q$
from these two sequents, so $\Gamma$ is inconsistent. This contradicts the
hypothesis that $\Gamma$ is consistent. ∎

######  Lemma 48 (Saturation).

Let $\Gamma$ be a consistent set of propositions, and let $Q$ be a proposition
such that $\Gamma\nvdash Q$. Then there exists a prime theory
$\Gamma^{\prime}\supseteq\Gamma$ such that $\Gamma^{\prime}\nvdash Q$.

###### Proof.

Consider an enumeration of all propositions $(P_{1},P_{2},\ldots)$. We build a
sequence of sets
$\Gamma=\Gamma_{0}\subseteq\Gamma_{1}\subseteq\Gamma_{2}\subseteq\ldots$, with
the invariant that $\Gamma_{n}\nvdash Q$ for all $n\geq 0$, according to the
following construction.

In the $n$-th step, suppose that $\Gamma_{1},\ldots,\Gamma_{n}$ have already
been constructed, and consider the first proposition $P$ in the enumeration
such that $\Gamma_{n}\vdash P$ but the disjunctive property fails for $P$,
that is, either $P$ is of the form $(A\lor B){}^{+}$ with
$A{}^{\oplus},B{}^{\oplus}\notin\Gamma_{n}$ or $P$ is of the form $(A\land
B){}^{-}$ with $A{}^{\ominus},B{}^{\ominus}\notin\Gamma_{n}$. There are two
subcases:

  1. 1.

If $P=(A\lor B){}^{+}$ with $A{}^{\oplus},B{}^{\oplus}\notin\Gamma_{n}$, note
that $\Gamma_{n},A{}^{\oplus}\vdash Q$ and $\Gamma_{n},B{}^{\oplus}\vdash Q$
cannot both hold simultaneously. Indeed, if both
$\Gamma_{n},A{}^{\oplus}\vdash Q$ and $\Gamma_{n},B{}^{\oplus}\vdash Q$ hold,
given that also $\Gamma_{n}\vdash(A\lor B){}^{+}$, applying E$\lor{}^{+}$ we
would have $\Gamma_{n}\vdash Q$, contradicting the hypothesis. Hence we may
define $\Gamma_{n+1}$ as follows:

$\Gamma_{n+1}\,\mathrel{\overset{\mathrm{def}}{=}}\,\begin{cases}\Gamma_{n}\cup\\{A{}^{\oplus}\\}&\text{if
$\Gamma_{n},A{}^{\oplus}\nvdash Q$}\\\
\Gamma_{n}\cup\\{B{}^{\oplus}\\}&\text{otherwise}\\\ \end{cases}$

Note that, in the second case, $\Gamma_{n},B{}^{\oplus}\nvdash Q$ holds.

  2. 2.

If $P=(A\land B){}^{-}$ with $A{}^{\ominus},B{}^{\ominus}\notin\Gamma_{n}$,
the construction is similar, defining $\Gamma_{n+1}$ as either
$\Gamma_{n}\cup\\{A{}^{\ominus}\\}$ or $\Gamma_{n}\cup\\{B{}^{\ominus}\\}$.

Now we define $\Gamma_{\omega}$ and $\Gamma^{\prime}$ as follows:

$\begin{array}[]{rcl}\Gamma_{\omega}&\,\mathrel{\overset{\mathrm{def}}{=}}&\bigcup_{n\in\mathbb{N}}\Gamma_{n}\\\
\Gamma^{\prime}&\,\mathrel{\overset{\mathrm{def}}{=}}&\Gamma_{\omega}\cup\\{A^{\pm}\
|\ \Gamma_{\omega}\vdash A^{\pm}\\}\end{array}$

Note that $\Gamma\subseteq\Gamma_{\omega}\subseteq\Gamma^{\prime}$. Moreover,
we claim that $\Gamma^{\prime}$ is a prime theory:

Closure by deduction. Let $\Gamma^{\prime}\vdash P$, and let us show that
$P\in\Gamma^{\prime}$. Since all assumptions in $\Gamma^{\prime}$ of the form
$A^{\pm}$ are provable from $\Gamma_{\omega}$, this means that
$\Gamma_{\omega}\vdash P$ by the cut rule (Lem. 20). We consider four
subcases, depending on whether $P$ is a strong/classical proof/refutation. We
only study the positive cases; the negative cases are symmetric:

  1. 1.

Strong proof, i.e. $P=A{}^{+}$. Then $\Gamma_{\omega}\vdash A{}^{+}$ so
$A{}^{+}\in\Gamma^{\prime}$ by definition of $\Gamma^{\prime}$.

  2. 2.

Classical proof, i.e. $P=A{}^{\oplus}$. Then $\Gamma_{\omega}\vdash
A{}^{\oplus}$ so in particular $\Gamma_{\omega}\vdash(A\lor A){}^{+}$ applying
the I$\lor{}^{+}_{1}$ rule. Then there is an $n_{0}$ such that
$\Gamma_{n}\vdash(A\lor A){}^{+}$ for all $n\geq n_{0}$. Then it cannot be the
case that $A{}^{\oplus}\notin\Gamma_{n}$ for all $n\geq n_{0}$, because the
proposition $(A\lor A){}^{+}$ must be eventually treated by the construction
of $(\Gamma_{n})_{n\in\mathbb{N}}$ above. This means that there is an $n\geq
n_{0}$ such that $A{}^{\oplus}\in\Gamma_{n}$, and therefore
$A{}^{\oplus}\in\Gamma_{\omega}\subseteq\Gamma^{\prime}$, as required.

Consistency. It suffices to note that $\Gamma^{\prime}\nvdash Q$. Indeed,
suppose that $\Gamma^{\prime}\vdash Q$. Then $\Gamma_{\omega}\vdash Q$ by the
cut rule (Lem. 20), so there exists an $n_{0}$ such that $\Gamma_{n}\vdash Q$
for all $n\geq n_{0}$. This contradicts the invariant of the construction of
$(\Gamma_{n})_{n\in\mathbb{N}}$ above.

Disjunctive property. We consider only the positive case. The negative case is
symmetric. Suppose that $\Gamma^{\prime}\vdash(A\lor B){}^{+}$. Then
$\Gamma_{\omega}\vdash(A\lor B){}^{+}$ by the cut rule (Lem. 20), so there
exists an $n_{0}$ such that $\Gamma_{n}\vdash(A\lor B){}^{+}$ for all $n\geq
n_{0}$. Then it cannot be the case that
$A{}^{\oplus},B{}^{\oplus}\notin\Gamma_{n}$ for all $n\geq n_{0}$, because the
proposition $(A\lor B){}^{+}$ must be eventually treated by the construction
of $(\Gamma_{n})_{n\in\mathbb{N}}$ above. This means that there is an $n\geq
n_{0}$ such that either $A{}^{\oplus}\in\Gamma_{n}$ or
$B{}^{\oplus}\in\Gamma_{n}$, and therefore we have that either
$A{}^{\oplus}\in\Gamma_{\omega}\subseteq\Gamma^{\prime}$, or
$B{}^{\oplus}\in\Gamma_{\omega}\subseteq\Gamma^{\prime}$, as required.

Finally, note that $\Gamma^{\prime}\nvdash Q$, as has already been shown in
the proof of consistency above. ∎

######  Definition 49 (Canonical model).

The canonical model is the structure
$\mathcal{M}_{0}=(\mathcal{W}_{0},\subseteq,\mathcal{V}^{+},\mathcal{V}^{-})$:

  1. 1.

$\mathcal{W}_{0}$ is the set of all prime theories, i.e.
$\mathcal{W}_{0}\,\mathrel{\overset{\mathrm{def}}{=}}\,\\{\Gamma\ |\
\text{$\Gamma$ is prime}\\}$.

  2. 2.

$\subseteq$ is the set-theoretic inclusion between prime theories.

  3. 3.

$\mathcal{V}^{+}_{\Gamma}=\\{\alpha\ |\ \alpha{}^{+}\in\Gamma\\}$ and
$\mathcal{V}^{-}_{\Gamma}=\\{\alpha\ |\ \alpha{}^{-}\in\Gamma\\}$.

######  Lemma 50.

The canonical model is a Kripke model.

###### Proof.

Let us check the two required properties. Monotonicity is immediate, since if
$\Gamma\subseteq\Gamma^{\prime}$ then $\alpha^{\pm}\in\Gamma$ implies
$\alpha^{\pm}\in\Gamma^{\prime}$. For stabilization, let $\Gamma$ be a prime
theory and let $\alpha$ be a propositional variable. First note that
$\Gamma\cup\\{\alpha{}^{+}\\}$ and $\Gamma\cup\\{\alpha{}^{-}\\}$ cannot both
be inconsistent, by the consistent extension lemma (Lem. 47). We consider two
subcases, depending on whether $\Gamma\cup\\{\alpha{}^{+}\\}$ is consistent:

  1. 1.

If $\Gamma\cup\\{\alpha{}^{+}\\}$ is consistent. Then
$\Gamma,\alpha{}^{+}\nvdash\alpha{}^{-}$ because
$\Gamma,\alpha{}^{+}\vdash\alpha{}^{-}$ would make the set
$\Gamma\cup\\{\alpha{}^{+}\\}$ inconsistent. Then by saturation (Lem. 48)
there is a prime theory $\Gamma^{\prime}\supseteq\Gamma\cup\\{\alpha{}^{+}\\}$
such that $\Gamma^{\prime}\nvdash\alpha{}^{-}$. Hence we have that
$\Gamma^{\prime}\supseteq\Gamma$ with
$\alpha\in\mathcal{V}^{+}_{\Gamma^{\prime}}\setminus\mathcal{V}^{-}_{\Gamma^{\prime}}$.

  2. 2.

Otherwise, so $\Gamma\cup\\{\alpha{}^{-}\\}$ is consistent. Similarly as in
the previous case, we have that $\Gamma,\alpha{}^{-}\nvdash\alpha{}^{+}$, so
by saturation (Lem. 48) there is a prime theory
$\Gamma^{\prime}\supseteq\Gamma\cup\\{\alpha{}^{-}\\}$ such that
$\Gamma^{\prime}\nvdash\alpha{}^{+}$, and this implies that
$\alpha\in\mathcal{V}^{-}_{\Gamma^{\prime}}\setminus\mathcal{V}^{+}_{\Gamma^{\prime}}$.

∎

######  Lemma 51 (Main Semantic Lemma).

Let $\Gamma$ be a prime theory. Then $\mathcal{M}_{0},\Gamma\Vdash P$ holds in
the canonical model if and only if $P\in\Gamma$.

###### Proof.

We proceed by induction on the measure $\\#(P)$. We only study the positive
cases, the negative cases are symmetric.

Propositional variable, $P=\alpha{}^{+}$.

$\mathcal{M}_{0},\Gamma\Vdash\alpha{}^{+}\iff\alpha\in\mathcal{V}^{+}_{\Gamma}\iff\alpha{}^{+}\in\Gamma$

Strong conjunction, $P=(A\land B){}^{+}$.

$\begin{array}[]{rcll}&&\mathcal{M}_{0},\Gamma\Vdash(A\land B){}^{+}\\\
&\iff&\mathcal{M}_{0},\Gamma\Vdash A{}^{\oplus}\text{ and
}\mathcal{M}_{0},\Gamma\Vdash B{}^{\oplus}\\\
&\iff&A{}^{\oplus}\in\Gamma\text{ and }B{}^{\oplus}\in\Gamma&\text{by IH}\\\
&\iff&(A\land B){}^{+}\in\Gamma\end{array}$

The last equivalence uses the fact that $\Gamma$ is closed by deduction, using
rule I$\land{}^{+}$ for the “only if” direction and rules
$\textsc{\text{E$\land{}^{+}_{1}$}},\textsc{\text{E$\land{}^{+}_{2}$}}$ for
the “if” direction.

Strong disjunction, $P=(A\lor B){}^{+}$.

$\begin{array}[]{rcll}&&\mathcal{M}_{0},\Gamma\Vdash(A\lor B){}^{+}\\\
&\iff&\mathcal{M}_{0},\Gamma\Vdash A{}^{\oplus}\text{ or
}\mathcal{M}_{0},\Gamma\Vdash B{}^{\oplus}\\\
&\iff&A{}^{\oplus}\in\Gamma\text{ or }B{}^{\oplus}\in\Gamma&\text{by IH}\\\
&\iff&(A\lor B){}^{+}\in\Gamma\end{array}$

The last equivalence uses the fact that $\Gamma$ is a prime theory, using
rules I$\lor{}^{+}_{1}$ and I$\lor{}^{+}_{2}$ for the “only if” direction, and
the fact that $\Gamma$ is disjunctive for the “if” direction.

Strong negation, $P=(\neg A){}^{+}$.

$\begin{array}[]{rcll}\mathcal{M}_{0},\Gamma\Vdash(\neg
A){}^{+}&\iff&\mathcal{M}_{0},\Gamma\Vdash A{}^{\ominus}\\\
&\iff&A{}^{\ominus}\in\Gamma&\text{by IH}\\\ &\iff&(\neg
A){}^{+}\in\Gamma\end{array}$

The last equivalence uses the fact that $\Gamma$ is closed by deduction, using
rule I$\lnot{}^{+}$ for the “only if” direction and rule E$\lnot{}^{+}$ for
the “if” direction.

Classical proposition, $P=A{}^{\oplus}$.

$\begin{array}[]{rcll}\mathcal{M}_{0},\Gamma\Vdash
A{}^{\oplus}&\iff&\forall\Gamma^{\prime}\supseteq\Gamma,\
\mathcal{M}_{0},\Gamma^{\prime}\nVdash A{}^{-}\\\
&\iff&\forall\Gamma^{\prime}\supseteq\Gamma,\
A{}^{-}\notin\Gamma^{\prime}&\text{by IH}\\\
&\iff&A{}^{\oplus}\in\Gamma\end{array}$

Note that $\Gamma^{\prime}$ does not vary over arbitrary sets of propositions,
but only over prime theories. To justify the last equivalence, we prove each
implication separately:

  * $(\Rightarrow)$

We show the contrapositive. Let $A{}^{\oplus}\notin\Gamma$ and let us show
that there is a prime theory $\Gamma^{\prime}\supseteq\Gamma$ such that
$A{}^{-}\in\Gamma^{\prime}$. First we claim that $\Gamma\cup\\{A{}^{-}\\}$ is
consistent.

    * Proof of the claim. Suppose by contradiction that $\Gamma\cup\\{A{}^{-}\\}$ is inconsistent. Then in particular $\Gamma,A{}^{-}\vdash\bot{}^{\oplus}$. (Recall that we encode falsity as $\bot\,\mathrel{\overset{\mathrm{def}}{=}}\,(\alpha_{0}\land\neg\alpha_{0})$). By the projection lemma (Lem. 4) we have that $\Gamma,A{}^{\ominus}\vdash\bot{}^{\oplus}$. By contraposition (Lem. 2) $\Gamma,\bot{}^{\ominus}\vdash A{}^{\oplus}$. Since $\bot{}^{\ominus}$ is provable (Ex. 3), by the cut rule (Lem. 2) we have that $\Gamma\vdash A{}^{\oplus}$. But $\Gamma$ is closed by deduction, so $A{}^{\oplus}\in\Gamma$. This contradicts the fact that $A{}^{\oplus}\notin\Gamma$ and concludes the proof of the claim.

Now since $\Gamma\cup\\{A{}^{-}\\}$ is consistent, by saturation (Lem. 48), we
may extend it to a prime theory
$\Gamma^{\prime}\supseteq\Gamma\cup\\{A{}^{-}\\}$. This concludes this case.

  * $(\Leftarrow)$

Suppose that $A{}^{\oplus}\in\Gamma$, and let $\Gamma^{\prime}\supseteq\Gamma$
such that $A{}^{-}\in\Gamma^{\prime}$. Then since $\Gamma^{\prime}$ is closed
by deduction, using the IC+ rule we have that
$A{}^{\ominus}\in\Gamma^{\prime}$. Since $\Gamma^{\prime}$ contains both
$A{}^{\oplus}$ and $A{}^{\ominus}$, using the generalized absurdity rule we
may derive an arbitrary proposition from $\Gamma^{\prime}$, which means that
$\Gamma^{\prime}$ is inconsistent, contradicting the fact that
$\Gamma^{\prime}$ is a prime theory.

∎

###  .5 Proof of Subject Reduction of $\lambda^{\textsc{prk}}$ (Prop. 24)

######  Proposition 52 (Subject reduction).

If $\Gamma\vdash t:P$ and $t\xrightarrow{}s$, then $\Gamma\vdash s:P$.

###### Proof.

Since reduction is closed under arbitrary contexts, the term on the left hand
side is of the form $\mathtt{C}\langle t_{0}\rangle$ and it reduces to
$\mathtt{C}\langle t_{1}\rangle$ contracting the redex $t_{0}$. We proceed by
induction on the context $\mathtt{C}$ under which the rewriting step takes
place. The interesting case is when the context is empty. All other cases are
easy by resorting to the IH. We proceed by case analysis on each of the
reduction rules. Note that each rule actually stands for two rules, depending
on the instantiations of the signs. We write only one of these cases; if the
signs are flipped the proof is symmetric. We use the admissible typing rules
Cut and $\textsc{\text{Abs}}^{\prime}$ (Lem. 20).

$\bullet$ $\mathsf{proj}$: let $i\in\\{1,2\\}$. We have:

${\small\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\hskip 4.5pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\hskip 4.5pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
16.2174pt\hbox{$\displaystyle\penalty 1\pi_{1}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=40.08505pt\hbox{\kern
2.70003pt$\textsc{}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\Gamma\vdash
t_{1}:A_{1}{}^{\oplus}$}}}}\hskip 4.5pt plus 1.0fil\penalty 2\end{array}\hskip
14.22636pt\begin{array}[]{c}\hskip 4.5pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
16.2174pt\hbox{$\displaystyle\penalty 1\pi_{2}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=40.08505pt\hbox{\kern
2.70003pt$\textsc{}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\Gamma\vdash
t_{2}:A_{2}{}^{\oplus}$}}}}\hskip 4.5pt plus 1.0fil\penalty
2\end{array}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=175.99034pt\hbox{\kern
2.70003pt$\textsc{{\text{I$\land{}^{+}$}}}$}}}\hbox{\kern
46.33371pt\hbox{$\displaystyle\Gamma\vdash\langle
t_{1},t_{2}\rangle{}^{+}:(A_{1}\land A_{2}){}^{+}$}}}}\hskip 4.5pt plus
1.0fil\penalty 2\end{array}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.225pt,depth=0.225pt,width=229.9573pt\hbox{\kern
2.70003pt$\textsc{{\text{E$\land{}^{+}_{i}$}}}$}}}\hbox{\kern
95.71979pt\hbox{$\displaystyle\Gamma\vdash
t_{i}:A_{i}{}^{\oplus}$}}}}\end{array}}$

Then:

${\small{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
14.9574pt\hbox{$\displaystyle\penalty 1\pi_{i}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=36.78137pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash t_{i}:A{}^{\oplus}$}}}}}$

$\bullet$ $\mathsf{case}$: let $i\in\\{1,2\\}$. We have:

${\small\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\hskip 4.5pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\hskip 4.5pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
17.07558pt\hbox{$\displaystyle\penalty 1\pi$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=39.28139pt\hbox{\kern
2.70003pt$\textsc{}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\Gamma\vdash
t:A_{i}{}^{\oplus}$}}}}\hskip 4.5pt plus 1.0fil\penalty 2\end{array}$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=80.07832pt\hbox{\kern
2.70003pt$\textsc{{\text{I$\lor{}^{+}_{i}$}}}$}}}\hbox{\kern
0.54343pt\hbox{$\displaystyle\Gamma\vdash\mathsf{in}_{i}\\!\\!{}^{+}(t):(A_{1}\lor
A_{2}){}^{+}$}}}}\hskip 4.5pt plus 1.0fil\penalty 2\end{array}\hskip
14.22636pt\pi_{1}\hskip 14.22636pt\pi_{2}$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=177.7985pt\hbox{\kern
2.70003pt$\textsc{{\text{E$\lor{}^{+}$}}}$}}}\hbox{\kern
36.54024pt\hbox{$\displaystyle\Gamma\vdash\delta{}^{+}(\mathsf{in}_{i}\\!\\!{}^{+}(t))\,[_{x}.s_{1}][_{x}.s_{2}]:P$}}}}\end{array}}$

where for each $j\in\\{1,2\\}$, the derivation $\pi_{j}$ is:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 30.22066pt\hbox{$\displaystyle\penalty
1\pi^{\prime}_{j}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=67.68158pt\hbox{\kern
3.00003pt$\textsc{}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma,x:A_{j}{}^{\oplus}\vdash
s_{j}:P$}}}}\end{array}$

Then:

${\small{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.5pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
26.57108pt\hbox{$\displaystyle\penalty 1\pi^{\prime}_{i}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=59.65837pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma,x:A_{i}{}^{\oplus}\vdash s_{i}:P$}}}}\hskip
4.5pt plus 1.0fil\penalty 2\hskip 4.5pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
17.07558pt\hbox{$\displaystyle\penalty 1\pi$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=39.28139pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash t:A_{i}{}^{\oplus}$}}}}\hskip 4.5pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=160.53363pt\hbox{\kern
2.70003pt${\textsc{{\text{Cut}}}}$}}}\hbox{\kern
49.51582pt\hbox{$\displaystyle\Gamma\vdash s_{i}[x\\!:=\\!t]:P$}}}}}$

$\bullet$ $\mathsf{neg}$: We have:

${\small{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.5pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.5pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
16.20741pt\hbox{$\displaystyle\penalty 1\pi$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=37.54506pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash t:A{}^{\ominus}$}}}}\hskip 4.5pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=68.342pt\hbox{\kern
2.70003pt${\textsc{\text{I$\lnot{}^{+}$}}}$}}}\hbox{\kern
3.96553pt\hbox{$\displaystyle\Gamma\vdash\nu{}^{+}t:(\lnot A){}^{+}$}}}}\hskip
4.5pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.225pt,depth=0.225pt,width=112.30896pt\hbox{\kern
2.70003pt${\textsc{{\text{E$\lnot{}^{+}$}}}}$}}}\hbox{\kern
25.02756pt\hbox{$\displaystyle\Gamma\vdash\mu{}^{+}(\nu{}^{+}t):A{}^{\ominus}$}}}}}$

Then:

${\small{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
16.20741pt\hbox{$\displaystyle\penalty 1\pi$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=37.54506pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash t:A{}^{\ominus}$}}}}}$

$\bullet$ $\mathsf{beta}$: we have:

${\small{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.5pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.5pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
28.1143pt\hbox{$\displaystyle\penalty 1\pi$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=61.35884pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma,x:A{}^{\ominus}\vdash t:A{}^{+}$}}}}\hskip
4.5pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.225pt,depth=0.225pt,width=92.15578pt\hbox{\kern
2.70003pt${\textsc{\text{IC${}^{+}$}}}$}}}\hbox{\kern
18.97035pt\hbox{$\displaystyle\Gamma\vdash\mathsf{IC}{}^{+}_{x}.\,t:A{}^{\oplus}$}}}}\hskip
4.5pt plus 1.0fil\penalty 2\hskip 4.5pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
15.9988pt\hbox{$\displaystyle\penalty 1\pi^{\prime}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=38.51381pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash s:A{}^{\ominus}$}}}}\hskip 4.5pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=205.93349pt\hbox{\kern
2.70003pt${\textsc{{\text{EC${}^{+}$}}}}$}}}\hbox{\kern
63.53981pt\hbox{$\displaystyle\Gamma\vdash(\mathsf{IC}{}^{+}_{x}.\,t)\bullet\\!\\!{}^{+}\,s:A{}^{+}$}}}}}$

Then:

${\small{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.5pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
28.1143pt\hbox{$\displaystyle\penalty 1\pi$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=61.35884pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma,x:A{}^{\ominus}\vdash t:A{}^{+}$}}}}\hskip
4.5pt plus 1.0fil\penalty 2\hskip 4.5pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
15.9988pt\hbox{$\displaystyle\penalty 1\pi^{\prime}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=38.51381pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash s:A{}^{\ominus}$}}}}\hskip 4.5pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=161.46652pt\hbox{\kern
2.70003pt${\textsc{{\text{Cut}}}}$}}}\hbox{\kern
49.02948pt\hbox{$\displaystyle\Gamma\vdash t[x\\!:=\\!s]:A{}^{+}$}}}}}$

$\bullet$ $\mathsf{absPairInj}$: we have:

${\footnotesize{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
14.41548pt\hbox{$\displaystyle\penalty 1\pi_{1}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=35.63118pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash t_{1}:A_{1}{}^{\oplus}$}}}}\hskip 4.0pt
plus 1.0fil\penalty 2\hskip 4.0pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
14.41548pt\hbox{$\displaystyle\penalty 1\pi_{2}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=35.63118pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash t_{2}:A_{2}{}^{\oplus}$}}}}\hskip 4.0pt
plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.20001pt,depth=0.20001pt,width=126.01251pt\hbox{\kern
2.40002pt${\textsc{\text{I$\land{}^{+}$}}}$}}}\hbox{\kern
25.54175pt\hbox{$\displaystyle\Gamma\vdash\langle
t_{1},t_{2}\rangle{}^{+}:(A_{1}\land A_{2}){}^{+}$}}}}\hskip 4.0pt plus
1.0fil\penalty 2\hskip 4.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{\kern 1.97028pt\hbox{$\displaystyle\penalty 1\hskip
4.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 14.99283pt\hbox{$\displaystyle\penalty
1\pi^{\prime}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=35.77786pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash s:A_{i}{}^{\ominus}$}}}}\hskip 4.0pt
plus 1.0fil\penalty 2$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=67.0935pt\hbox{\kern
2.40002pt${\textsc{{\text{I$\land{}^{-}_{i}$}}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash\mathsf{in}_{i}\\!\\!{}^{-}(s):(A_{1}\land
A_{2}){}^{-}$}}}}\hskip 4.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.20001pt,depth=0.20001pt,width=269.27841pt\hbox{\kern
2.40002pt${\textsc{{\text{Abs}}}}$}}}\hbox{\kern
95.11292pt\hbox{$\displaystyle\Gamma\vdash\langle
t_{1},t_{2}\rangle{}^{+}\mathrel{{\RHD\\!\\!\\!\LHD_{P}}}\mathsf{in}_{i}\\!\\!{}^{-}(s):P$}}}}}$

Then:

${\small{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.5pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
15.82558pt\hbox{$\displaystyle\penalty 1\pi_{i}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=38.51773pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash t_{i}:A_{i}{}^{\oplus}$}}}}\hskip 4.5pt
plus 1.0fil\penalty 2\hskip 4.5pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
16.86696pt\hbox{$\displaystyle\penalty 1\pi^{\prime}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=40.25014pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash s:A_{i}{}^{\ominus}$}}}}\hskip 4.5pt
plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.225pt,depth=0.225pt,width=140.36174pt\hbox{\kern
2.70003pt${\textsc{{\text{Abs}}'}}$}}}\hbox{\kern
44.90887pt\hbox{$\displaystyle\Gamma\vdash
t_{i}\mathrel{\bowtie_{P}}s:P$}}}}}$

$\bullet$ $\mathsf{absInjPair}$: similar to the previous case.

$\bullet$ $\mathsf{absNeg}$:

${\small{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.5pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.5pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
16.20741pt\hbox{$\displaystyle\penalty 1\pi$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=37.54506pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash t:A{}^{\ominus}$}}}}\hskip 4.5pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=68.342pt\hbox{\kern
2.70003pt${\textsc{{\text{I$\lnot{}^{+}$}}}}$}}}\hbox{\kern
3.96553pt\hbox{$\displaystyle\Gamma\vdash\nu{}^{+}t:(\lnot A){}^{+}$}}}}\hskip
4.5pt plus 1.0fil\penalty 2\hskip 4.5pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\hskip
4.5pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 15.9988pt\hbox{$\displaystyle\penalty
1\pi^{\prime}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=38.51381pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash s:A{}^{\oplus}$}}}}\hskip 4.5pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=69.31075pt\hbox{\kern
2.70003pt${\textsc{{\text{I$\lnot{}^{-}$}}}}$}}}\hbox{\kern
6.20555pt\hbox{$\displaystyle\Gamma\vdash\nu{}^{-}s:(\lnot A){}^{-}$}}}}\hskip
4.5pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.225pt,depth=0.225pt,width=223.34665pt\hbox{\kern
2.70003pt${\textsc{{\text{Abs}}}}$}}}\hbox{\kern
71.64865pt\hbox{$\displaystyle\Gamma\vdash(\nu{}^{+}t)\mathrel{{\RHD\\!\\!\\!\LHD_{P}}}(\nu{}^{-}s):P$}}}}}$

Then:

${\small{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.5pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
16.20741pt\hbox{$\displaystyle\penalty 1\pi$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=37.54506pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash t:A{}^{\ominus}$}}}}\hskip 4.5pt plus
1.0fil\penalty 2\hskip 4.5pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{\kern 15.9988pt\hbox{$\displaystyle\penalty
1\pi^{\prime}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=38.51381pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash s:A{}^{\oplus}$}}}}\hskip 4.5pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=137.65274pt\hbox{\kern
2.70003pt${\textsc{{\text{Abs}}'}}$}}}\hbox{\kern
44.42256pt\hbox{$\displaystyle\Gamma\vdash t\mathrel{\bowtie_{P}}s:P$}}}}}$

∎

###  .6 Proof of the Positivity Condition for Coro. 27

######  Definition 53.

Recall that the set of type constraints $\mathcal{C}_{\mathbf{pn}}$ is given
by all equations of the following form, for all types $A,B$ of System F:

$\mathbf{p}_{A,B}\equiv(\mathbf{n}_{A,B}\to A)\hskip
14.22636pt\mathbf{n}_{A,B}\equiv(\mathbf{p}_{A,B}\to B)$

######  Proposition 54.

The set of type constraints $\mathcal{C}_{\mathbf{pn}}$ verifies Mendler’s
positivity condition (stated in the body of the paper, and also in the
appendix in Def. 77).

###### Proof.

Define the complexity of a type as follows:

$\begin{array}[]{rcl@{\hspace{1cm}}rcl}||\alpha||&\,\mathrel{\overset{\mathrm{def}}{=}}&1\text{\hskip
14.22636ptif $\alpha\in\mathbf{V}$}\hfil\hskip 28.45274pt\\\
||\mathbf{p}_{A,B}||=||\mathbf{n}_{A,B}||=||A\to
B||&\,\mathrel{\overset{\mathrm{def}}{=}}&1+||A||+||B||\hfil\hskip
28.45274pt\\\
||\forall\alpha.A||&\,\mathrel{\overset{\mathrm{def}}{=}}&1+||A||\hfil\hskip
28.45274pt\end{array}$

Recall that $\textsf{p}(A)$ (resp. $\textsf{n}(A)$) stand for the set of type
variables occurring positively (resp. negatively) in a given type $A$.
Moreover, the set of type variables occurring weakly positively (resp. weakly
negatively) in $A$ are written $\textsf{p}^{\mathtt{w}}(A)$ (resp.
$\textsf{n}^{\mathtt{w}}(A)$) and defined as follows:

$\begin{array}[]{rcl}\textsf{p}^{\mathtt{w}}(\alpha)&\,\mathrel{\overset{\mathrm{def}}{=}}&\\{\alpha\\}\text{\hskip
14.22636ptif $\alpha\in\mathbf{V}$}\\\
\textsf{p}^{\mathtt{w}}(\mathbf{p}_{A,B})&\,\mathrel{\overset{\mathrm{def}}{=}}&\\{\mathbf{p}_{A,B}\\}\cup\textsf{p}^{\mathtt{w}}(A)\cup\textsf{n}^{\mathtt{w}}(B)\\\
\textsf{p}^{\mathtt{w}}(\mathbf{n}_{A,B})&\,\mathrel{\overset{\mathrm{def}}{=}}&\\{\mathbf{n}_{A,B}\\}\cup\textsf{n}^{\mathtt{w}}(A)\cup\textsf{p}^{\mathtt{w}}(B)\\\
\textsf{p}^{\mathtt{w}}(A\to
B)&\,\mathrel{\overset{\mathrm{def}}{=}}&\textsf{n}^{\mathtt{w}}(A)\cup\textsf{p}^{\mathtt{w}}(B)\\\
\textsf{p}^{\mathtt{w}}(\forall\alpha.A)&\,\mathrel{\overset{\mathrm{def}}{=}}&\textsf{p}^{\mathtt{w}}(A)\setminus\\{\alpha\\}\end{array}$
$\begin{array}[]{rcl}\\\
\textsf{n}^{\mathtt{w}}(\alpha)&\,\mathrel{\overset{\mathrm{def}}{=}}&\varnothing\text{\hskip
14.22636ptif $\alpha\in\mathbf{V}$}\\\
\textsf{n}^{\mathtt{w}}(\mathbf{p}_{A,B})&\,\mathrel{\overset{\mathrm{def}}{=}}&\textsf{n}^{\mathtt{w}}(A)\cup\textsf{p}^{\mathtt{w}}(B)\\\
\textsf{n}^{\mathtt{w}}(\mathbf{n}_{A,B})&\,\mathrel{\overset{\mathrm{def}}{=}}&\textsf{p}^{\mathtt{w}}(A)\cup\textsf{n}^{\mathtt{w}}(B)\\\
\textsf{n}^{\mathtt{w}}(A\to
B)&\,\mathrel{\overset{\mathrm{def}}{=}}&\textsf{p}^{\mathtt{w}}(A)\cup\textsf{n}^{\mathtt{w}}(B)\\\
\textsf{n}^{\mathtt{w}}(\forall\alpha.A)&\,\mathrel{\overset{\mathrm{def}}{=}}&\textsf{n}^{\mathtt{w}}(A)\setminus\\{\alpha\\}\end{array}$

It is easy to check that $\textsf{p}(A)\subseteq\textsf{p}^{\mathtt{w}}(A)$
and $\textsf{n}(A)\subseteq\textsf{n}^{\mathtt{w}}(A)$ by simultaneous
induction on $A$. It is also easy to check that if
$\alpha\in\textsf{p}^{\mathtt{w}}(A)\cup\textsf{n}^{\mathtt{w}}(A)$ then
$||\alpha||\leq||A||$, by induction on $A$. Moreover, let $X,Y$ be types. A
type $A$ is said to be $(X,Y)$-positive if
$\mathbf{p}_{X,Y}\in\textsf{p}^{\mathtt{w}}(A)$ or
$\mathbf{n}_{X,Y}\in\textsf{n}^{\mathtt{w}}(A)$. Symmetrically, a type $A$ is
said to be $(X,Y)$-negative if $\mathbf{p}_{X,Y}\in\textsf{n}^{\mathtt{w}}(A)$
or $\mathbf{n}_{X,Y}\in\textsf{p}^{\mathtt{w}}(A)$. It is straightforward to
prove the following invariant for the equivalence $A\equiv B$ between types
induced by the recursive type constraints, by induction on the derivation of
$A\equiv B$.

  1. 1.

If $A\equiv B$, then $A$ is $(X,Y)$-positive if and only if $B$ is
$(X,Y)$-positive.

  2. 2.

If $A\equiv B$, then $A$ is $(X,Y)$-negative if and only if $B$ is
$(X,Y)$-negative.

To prove Mendler’s positivity condition, we must check that given any type
variable $\alpha$ of the form $\mathbf{p}_{A,B}$ or of the form
$\mathbf{n}_{A,B}$, then whenever $\alpha\equiv C$ we have that $\alpha$ does
not occur negatively in $C$. We consider two cases, depending on whether
$\alpha=\mathbf{p}_{A,B}$ or $\alpha=\mathbf{n}_{A,B}$:

  1. 1.

Let $\mathbf{p}_{A,B}\equiv C$ and suppose that
$\mathbf{p}_{A,B}\in\textsf{n}(C)$. Then we have that
$\mathbf{p}_{A,B}\in\textsf{n}^{\mathtt{w}}(C)$, so $C$ is $(A,B)$-negative.
By the invariant, $\mathbf{p}_{A,B}$ is also $(A,B)$-negative, so either
$\mathbf{p}_{A,B}\in\textsf{n}^{\mathtt{w}}(\mathbf{p}_{A,B})$ or
$\mathbf{n}_{A,B}\in\textsf{p}^{\mathtt{w}}(\mathbf{p}_{A,B})$. Both
conditions are impossible, indeed:

    1. 1.1

Suppose that $\mathbf{p}_{A,B}\in\textsf{n}^{\mathtt{w}}(\mathbf{p}_{A,B})$.
Then, given that $\mathbf{p}_{A,B}$ does not occur weakly negatively at the
root of $\mathbf{p}_{A,B}$, so it must occur either inside $A$ or inside $B$,
so $||\mathbf{p}_{A,B}||<||\mathbf{p}_{A,B}||$, which is a contradiction.

    2. 1.2

Suppose that $\mathbf{n}_{A,B}\in\textsf{n}^{\mathtt{w}}(\mathbf{p}_{A,B})$.
Then, again, $\mathbf{n}_{A,B}$ must occur either inside $A$ or inside $B$, so
$||\mathbf{n}_{A,B}||<||\mathbf{p}_{A,B}||$, which is a contradiction.

  2. 2.

If $\mathbf{n}_{A,B}\equiv C$ then, symmetrically as above, we have that
$\mathbf{n}_{A,B}\notin\textsf{n}(C)$.

∎

###  .7 Proof of the Simulation Lemma for the Translation from prk to the
Extended System F

######  Lemma 55.

If $t\xrightarrow{}s$ in $\lambda^{\textsc{prk}}$ then
$[\\![t]\\!]\xrightarrow{}^{+}[\\![s]\\!]$ in System F extended with
$\mathcal{C}_{\mathbf{pn}}$.

###### Proof.

By case analysis on the rewriting rule used to derive the step
$t\xrightarrow{}s$. Note that showing contextual closure is immediate, so we
only study the cases in which the rewriting rule is applied at the root:

$\bullet$ $\mathsf{proj}$: $[\\![\pi_{i}^{\pm}(\langle
t_{1},t_{2}\rangle^{\pm})]\\!]=\pi_{i}(\langle[\\![t_{1}]\\!],[\\![t_{2}]\\!]\rangle)\xrightarrow{}[\\![t_{i}]\\!]$.

$\bullet$ $\mathsf{case}$:

$\begin{array}[]{rcll}&&[\\![\delta^{\pm}\mathsf{in}_{i}^{\pm}(t)\,[_{(x:P)}.s_{1}][_{(x:Q)}.s_{2}]]\\!]\\\
&=&\delta\mathsf{in}_{i}([\\![t]\\!])\,[_{(x:[\\![P]\\!])}.[\\![s_{1}]\\!]][_{(x:[\\![Q]\\!])}.[\\![s_{2}]\\!]]\\\
&\to&[\\![s_{i}]\\!][x\\!:=\\![\\![t]\\!]]\\\
&=&[\\![s_{i}[x\\!:=\\![\\![t]\\!]]]\\!]\\\ &&\hskip 14.22636pt\text{by
Lem.~{}\ref{lemma:semF_properties}}\end{array}$

$\bullet$ $\mathsf{neg}$: $[\\![\mu^{\pm}\nu^{\pm}t]\\!]=(\lambda
x^{\mathbf{1}}.\,[\\![t]\\!])\,\star\xrightarrow{}[\\![t]\\!][x\\!:=\\!\star]=[\\![t]\\!]$
by Lem. 30, since $x\not\in\mathsf{fv}(t)$ by definition of
$[\\![\nu^{\pm}t]\\!]$.

$\bullet$ $\mathsf{beta}$:
$[\\![(\mathsf{IC}^{\pm}_{(x:P)}.\,t)\bullet\\!\\!^{\pm}\,s]\\!]=(\lambda
x^{[\\![P]\\!]}.\,[\\![t]\\!])\,[\\![s]\\!]\to[\\![t]\\!][x\\!:=\\![\\![s]\\!]]=[\\![t[x\\!:=\\!s]]\\!]$
by Lem. 30.

$\bullet$ $\mathsf{absPairInj}$: we consider two subcases, depending on the
signs:

  1. 1.

Let $\vdash t_{1}:A_{1}{}^{\oplus}$, $\vdash t_{2}:A_{2}{}^{\oplus}$, and
$\vdash s:A_{i}{}^{\ominus}$ for some $i\in\\{1,2\\}$. Then:

$\begin{array}[]{ll}&[\\![\langle
t_{1},t_{2}\rangle{}^{+}\mathrel{{\RHD\\!\\!\\!\LHD_{P}}}\mathsf{in}_{i}\\!\\!{}^{-}(s)]\\!]\\\
=&\mathsf{abs}^{(A_{1}\land
A_{2}){}^{+}}_{P}\,\langle[\\![t_{1}]\\!],[\\![t_{2}]\\!]\rangle\,\mathsf{in}_{i}([\\![s]\\!])\\\
\xrightarrow{}^{+}&\begin{array}[t]{l}\delta\mathsf{in}_{i}([\\![s]\\!])\\\
\hskip
14.22636pt[_{(z:[\\![A_{1}{}^{\ominus}]\\!])}.\mathsf{abs}^{A_{1}{}^{\oplus}}_{P}\,\pi_{1}(\langle[\\![t_{1}]\\!],[\\![t_{2}]\\!]\rangle)\,z]\\\
\hskip
14.22636pt[_{(z:[\\![A_{2}{}^{\ominus}]\\!])}.\mathsf{abs}^{A_{2}{}^{\oplus}}_{P}\,\pi_{2}(\langle[\\![t_{1}]\\!],[\\![t_{2}]\\!]\rangle)\,z]\\\
\end{array}\\\ &\hskip 14.22636pt\text{by definition of
$\mathsf{abs}^{(A_{1}\land A_{2}){}^{+}}_{P}$}\\\
\xrightarrow{}&\mathsf{abs}^{A_{i}{}^{\oplus}}_{P}\,\pi_{i}(\langle[\\![t_{1}]\\!],[\\![t_{2}]\\!]\rangle)\,[\\![s]\\!]\\\
\xrightarrow{}&\mathsf{abs}^{A_{i}{}^{\oplus}}_{P}\,[\\![t_{i}]\\!]\,[\\![s]\\!]\\\
\xrightarrow{}^{+}&\mathsf{abs}^{A_{i}{}^{+}}_{P}\,([\\![t_{i}]\\!]\,[\\![s]\\!])([\\![s]\\!]\,[\\![t_{i}]\\!])\\\
&\hskip 14.22636pt\text{by definition of
$\mathsf{abs}^{A_{i}{}^{\oplus}}_{P}$}\\\
=&[\\![(t_{i}\bullet\\!\\!{}^{+}\,s)\mathrel{{\RHD\\!\\!\\!\LHD_{P}}}(t_{i}\bullet\\!\\!{}^{-}\,s)]\\!]\\\
=&[\\![t_{i}\mathrel{\bowtie_{P}}s]\\!]\end{array}$

  2. 2.

Let $\Gamma\vdash t_{1}:A_{1}{}^{\ominus}$, $\Gamma\vdash
t_{2}:A_{2}{}^{\ominus}$, and $\Gamma\vdash s:A_{i}{}^{\oplus}$ for some
$i\in\\{1,2\\}$. Then, symmetrically as for the previous case, $[\\![\langle
t_{1},t_{2}\rangle{}^{-}\mathrel{{\RHD\\!\\!\\!\LHD_{P}}}\mathsf{in}_{i}\\!\\!{}^{+}(s)]\\!]\xrightarrow{}^{+}[\\![t_{i}\mathrel{\bowtie_{P}}s]\\!]$.

$\bullet$ $\mathsf{absInjPair}$: symmetric to the previous case.

$\bullet$ $\mathsf{absNeg}$: we consider two subcases, depending on the signs:

  1. 1.

Let $\Gamma\vdash t:A{}^{\ominus}$ and $\Gamma\vdash s:A{}^{\oplus}$. Then:

$\begin{array}[]{rcll}&&[\\![(\nu{}^{+}t)\mathrel{{\RHD\\!\\!\\!\LHD_{P}}}(\nu{}^{-}s)]\\!]\\\
&=&\mathsf{abs}^{(\neg A){}^{+}}_{P}(\lambda
x^{\mathbf{1}}.\,[\\![t]\\!])(\lambda y^{\mathbf{1}}.\,[\\![s]\\!])\\\
&&\hskip 14.22636pt\text{where $x\not\in\mathsf{fv}(t)$,
$y\not\in\mathsf{fv}(s)$}\\\
&\xrightarrow{}^{+}&\mathsf{abs}^{A{}^{\ominus}}_{P}((\lambda
x^{\mathbf{1}}.\,[\\![t]\\!])\,\star)((\lambda
y^{\mathbf{1}}.\,[\\![s]\\!])\,\star)\\\ &&\hskip 14.22636pt\text{by
definition of $\mathsf{abs}^{(\neg A){}^{+}}_{P}$}\\\
&\xrightarrow{}^{+}&\mathsf{abs}^{A{}^{\ominus}}_{P}\,[\\![t]\\!]\,[\\![s]\\!]\\\
&\xrightarrow{}^{+}&\mathsf{abs}^{A{}^{-}}_{P}\,([\\![t]\\!]\,[\\![s]\\!])\,([\\![s]\\!]\,[\\![t]\\!])\\\
&&\hskip 14.22636pt\text{by definition of
$\mathsf{abs}^{A{}^{\ominus}}_{P}$}\\\
&=&[\\![(t\bullet\\!\\!{}^{-}\,s)\mathrel{{\RHD\\!\\!\\!\LHD_{P}}}(s\bullet\\!\\!{}^{+}\,t)]\\!]\\\
&=&[\\![t\mathrel{\bowtie_{P}}s]\\!]\end{array}$

  2. 2.

Let $\Gamma\vdash t:A{}^{\oplus}$ and $\Gamma\vdash s:A{}^{\ominus}$. Then,
symmetrically as for the previous case:
$[\\![(\nu{}^{-}t)\mathrel{{\RHD\\!\\!\\!\LHD_{P}}}(\nu{}^{+}s)]\\!]\xrightarrow{}^{+}[\\![t\mathrel{\bowtie_{P}}s]\\!]$.

∎

###  .8 Proof of Characterization of Normal Forms (Prop. 34)

######  Proposition 56.

A term is normal if and only if it does not reduce in
$\lambda^{\textsc{prk}}$.

###### Proof.

$(\Rightarrow)$ Let $t$ be a normal term, and let us check that it is a
$\xrightarrow{}$-normal form. We proceed by induction on the derivation that
$t$ is a normal term.

The cases corresponding to introduction rules are straightforward by IH. For
example, if $t=\langle N_{1},N_{2}\rangle^{\pm}$, then by IH $N_{1}$ and
$N_{2}$ have no $\xrightarrow{}$-redexes. Moreover, there are no rules
involving a pair $\langle-,-\rangle^{\pm}$ at the root, so $\langle
N_{1},N_{2}\rangle^{\pm}$ is in $\xrightarrow{}$-normal form.

The cases corresponding to elimination rules and the absurdity rule are also
straightforward by IH, observing that there cannot be a redex at the root. For
example, if $t=\pi_{i}^{\pm}(S)$, then by IH $S$ has no
$\xrightarrow{}$-redexes. Moreover, the only rule involving a projection
$\pi_{i}^{\pm}(-)$ at the root is $\mathsf{proj}$, which would require that
$S=\langle t_{1},t_{2}\rangle^{\pm}$. But this is impossible —as can be
checked by exhaustive case analysis on $S$—, so $t$ is in
$\xrightarrow{}$-normal form.

$(\Leftarrow)$ Let $t$ be a $\xrightarrow{}$-normal form, let us check that it
is a normal term. We proceed by induction on the structure of the term $t$:

  1. 1.

Variable, $x$: it is a neutral term.

  2. 2.

Absurdity, $t\mathrel{{\RHD\\!\\!\\!\LHD_{P}}}s$: by IH, $t$ and $s$ are
normal terms. If either $t$ or $s$ is a neutral term, we are done. We are left
to analyze the case in which they are not neutral terms, i.e. both $t$ and $s$
are built using introduction rules. Note that the types of $t$ and $s$ are $Q$
and $Q{}^{\sim}$ respectively, for some strong type $Q$. We proceed by case
analysis on the form of the proposition $Q$. There are four cases:

    1. 2.1

Proof/refutation of a propositional variable, $Q=\alpha^{\pm}$. This case is
impossible, since $t$ only may be of one of the following forms: $\langle
N,N\rangle^{\pm}$, $\mathsf{in}_{i}^{\pm}(N)$, $\mathsf{IC}^{\pm}_{x:P}.\,N$,
or $\nu^{\pm}N$, none of which are of type $\alpha^{\pm}$.

    2. 2.2

Proof of a conjunction, $Q=(A\land B){}^{+}$ or refutation of a disjunction
$Q=(A\lor B){}^{-}$. Then $t$ is of the form $\langle
t_{1},t_{2}\rangle^{\pm}$ and $s$ is of the form
$\mathsf{in}_{i}^{\mp}(s^{\prime})$ for some $i\in\\{1,2\\}$, so the rule
$\mathsf{absPairInj}$ may be applied at the root, contradicting the hypothesis
that the term is $\to{}$-normal.

    3. 2.3

Disjunction, $Q=(A\land B)^{\pm}$. Then $t$ is of the form
$\mathsf{in}_{i}^{\pm}(s^{\prime})$ for some $i\in\\{1,2\\}$ and $s$ is of the
form $\langle t_{1},t_{2}\rangle^{\mp}$, so the rule $\mathsf{absInjPair}$ may
be applied at the root, contradicting the hypothesis that the term is
$\to{}$-normal.

    4. 2.4

Negation, $Q=(\neg A)^{\pm}$. Then $t$ is of the form $\nu^{\pm}t^{\prime}$
and $s$ is of the form $\nu^{\mp}s^{\prime}$, so the rule $\mathsf{absNeg}$
may be applied at the root, contradicting the hypothesis that the term is
$\to{}$-normal.

  3. 3.

Pair, $\langle t,s\rangle^{\pm}$: by IH, $t$ and $s$ are normal terms, so
$\langle t,s\rangle^{\pm}$ is also a normal term.

  4. 4.

Projection, $\pi_{i}^{\pm}(t)$: by IH, $t$ is a normal term. It suffices to
show that $t$ is neutral. Indeed, if $t$ is a normal but not neutral term,
then since the type of $t$ may be either of the form $(A\land B){}^{+}$ or of
the form $(A\lor B){}^{-}$, we have that $t$ is of the form $\langle
s,u\rangle^{\pm}$. Then the rule $\mathsf{proj}$ may be applied at the root,
contradicting the hypothesis that the term is $\to{}$-normal.

  5. 5.

Injection, $\mathsf{in}_{i}^{\pm}(t)$: by IH, $t$ is a normal term, so
$\mathsf{in}_{i}^{\pm}(t)$ is also normal.

  6. 6.

Case, $\delta^{\pm}t\,[_{x}.s][_{x}.u]$: by IH $t$, $s$ and $u$ are normal
terms. It suffices to show that $t$ is neutral. Indeed, if $t$ is a normal but
not neutral term, then since the type of $t$ may be either of the form $(A\lor
B){}^{+}$ or of the form $(A\land B){}^{-}$, we have that $t$ is of the form
$\mathsf{in}_{i}^{\pm}(t^{\prime})$ for some $i\in\\{1,2\\}$. Then the rule
$\mathsf{case}$ may be applied at the root, contradicting the hypothesis that
the term is $\to{}$-normal.

  7. 7.

Negation introduction, $\nu^{\pm}t$: by IH, $t$ is a normal term. Then
$\nu^{\pm}t$ is also normal.

  8. 8.

Negation elimination, $\mu^{\pm}t$: by IH, $t$ is a normal term. It suffices
to show that $t$ is neutral. Indeed, if $t$ is a normal but not neutral term,
then since the type of $t$ is of the form $(\neg A)^{\pm}$, then $t$ is of the
form $\nu^{\pm}t^{\prime}$. Then the rule $\mathsf{neg}$ may be applied at the
root, contradicting the hypothesis that the term is $\to{}$-normal.

  9. 9.

Classical introduction, $\mathsf{IC}^{\pm}_{x:P}.\,t$: by IH, $t$ is a normal
term, so $\mathsf{IC}^{\pm}_{x:P}.\,t$ is also normal.

  10. 10.

Classical elimination, $t\bullet\\!\\!^{\pm}\,s$: by IH, $t$ and $s$ are
normal terms. It suffices to show that $t$ is neutral. Indeed, if $t$ is a
normal but not neutral term, then since the type of $t$ may be either of the
form $A{}^{\oplus}$ or of the form $A{}^{\ominus}$, we have that $t$ is of the
form $\mathsf{IC}^{\pm}_{x}.\,t^{\prime}$. Then the rule $\mathsf{beta}$ may
be applied at the root, contradicting the hypothesis that the term is
$\to{}$-normal.

∎

###  .9 Proof of Canonicity (Thm. 35)

We give a slightly different statement of Canonicity, adding the additional
hypothesis that $t$ is already a normal form. This addition comes at no loss
of generality, given that $\lambda^{\textsc{prk}}$ enjoys subject reduction
(Prop. 24) and strong normalization (Thm. 32).

######  Theorem 57 (Canonicity).

  1. 1.

Let $\vdash t:P$ where $t$ is a normal form. Then $t$ is canonical.

  2. 2.

Let $\Gamma\vdash t:A^{\pm}$ where $\Gamma$ is classical and $t$ is a normal
form. Then either $t$ is canonical or $t$ is of the form $\mathtt{K}\langle
t^{\prime}\rangle$ where $\mathtt{K}$ is a case-context and $t^{\prime}$ is an
open explosion.

  3. 3.

Let $\Gamma\vdash t:A{}^{\oplus}$ or $\Gamma\vdash t:A{}^{\ominus}$, where
$\Gamma$ is classical and $t$ is a normal form. Then either
$t=\mathsf{IC}^{\pm}_{x}.\,t^{\prime}$ or $t=\mathtt{E}\langle
t^{\prime}\rangle$, where $\mathtt{E}$ is an eliminative context and
$t^{\prime}$ is a variable or an open explosion.

###### Proof.

  1. 1.

Let $\vdash t:P$ where $t$ is a normal form. Note, by induction on the
formation rules for neutral terms (Def. 33) that a neutral term must have at
least one free variable. But $t$ is typed in the empty typing context, so it
must be closed. Hence $t$ is not a neutral term, so by Prop. 34, it must be
canonical.

  2. 2.

Let $\Gamma\vdash t:P$ where $\Gamma$ is classical and $t$ is a normal form.
By Prop. 34 either $t$ is canonical or it is a neutral term. If $t$ is
canonical we are done. If $t$ is a neutral term it suffices to show the
following claim, namely that if $\Gamma\vdash t:B^{\pm}$ is a derivable
judgment such that $\Gamma$ is classical and $t$ is a neutral term, then $t$
is of the form $t=\mathtt{K}\langle t^{\prime}\rangle$, where $\mathtt{K}$ is
a case-context and $t^{\prime}$ is an open explosion. We proceed by induction
on the formation rules for neutral terms (Def. 33):

    1. 2.1

Variable, $t=x$. this case is impossible, given that $\Gamma$ is assumed to be
classical, so $\Gamma\vdash x:P$ where $P$ must be of the form $C{}^{\oplus}$
or $C{}^{\ominus}$, hence $P$ cannot be of the form $B^{\pm}$.

    2. 2.2

Projection, $\pi_{i}^{\pm}(S)$: this case is impossible, as
$\Gamma\vdash\pi_{i}^{\pm}(S):P$ where $P$ must be of the form $C{}^{\oplus}$
or $C{}^{\ominus}$, hence $P$ cannot be of the form $B^{\pm}$.

    3. 2.3

Case, $\delta^{\pm}S\,[_{x}.N_{1}][_{x}.N_{2}]$: by inversion of the typing
rules we have that either $\Gamma\vdash S:(A\lor B){}^{+}$ or $\Gamma\vdash
S:(A\land B){}^{-}$. In both cases we may apply the IH to conclude that $S$ is
of the form $S=\mathtt{K}\langle t^{\prime}\rangle$ where $\mathtt{K}$ is a
case-context and $t^{\prime}$ is an open explosion. Therefore
$t=\delta^{\pm}(\mathtt{K}\langle
t^{\prime}\rangle)\,[_{x}.N_{1}][_{x}.N_{2}]$ where now
$\delta^{\pm}(\mathtt{K})\,[_{x}.N_{1}][_{x}.N_{2}]$ is a case-context.

    4. 2.4

Classical elimination, $S\bullet\\!\\!^{\pm}\,N$: then $t$ is an explosion
under the empty case-context. Moreover, $S$ must have at least one free
variable so $t$ is indeed an open explosion.

    5. 2.5

Negation elimination, $\mu^{\pm}S$: this case is impossible, as
$\Gamma\vdash\mu^{\pm}S:P$ where $P$ must be of the form $C{}^{\oplus}$ or
$C{}^{\ominus}$, hence $P$ cannot be of the form $B^{\pm}$.

    6. 2.6

Absurdity, $S\mathrel{{\RHD\\!\\!\\!\LHD}}N$ or
$N\mathrel{{\RHD\\!\\!\\!\LHD}}S$: then $t$ is an explosion under the empty
case-context. Moreover, $S$ must have at least one free variable so $t$ is
indeed an open explosion.

  3. 3.

Let $\Gamma\vdash t:A{}^{\oplus}$ or $\Gamma\vdash t:A{}^{\ominus}$, where
$\Gamma$ is classical and $t$ is a normal form. By Prop. 34 either $t$ is
canonical or it is a neutral term. If $t$ is canonical, then by the
constraints on its type it must be of the form
$t=\mathsf{IC}^{\pm}_{x}.\,t^{\prime}$, so we are done. If $t$ is neutral, it
suffices to show the following claim namely that if $\Gamma\vdash t:P$ is a
derivable judgment, with $P\in\\{B{}^{\oplus},B{}^{\ominus}\\}$, such that
$\Gamma$ is classical and $t$ is a neutral term, then $t$ is of the form
$t=\mathtt{E}\langle t^{\prime}\rangle$, where $\mathtt{E}$ is an eliminative
context and $t^{\prime}$ is a variable or an open explosion. We proceed by
induction on the formation rules for neutral terms (Def. 33):

    1. 3.1

Variable, $t=x$. immediate, as $t$ is a variable under the empty eliminative
context.

    2. 3.2

Projection, $\pi_{i}^{\pm}(S)$: by inversion of the typing rules, we have that
either $\Gamma\vdash S:(A\land B){}^{+}$ or $\Gamma\vdash S:(A\lor B){}^{-}$.
In both cases we may apply the second item of this lemma to conclude that $S$
is of the form $S=\mathtt{K}\langle t^{\prime}\rangle$ where $\mathtt{K}$ is a
case-context and $t^{\prime}$ is an open explosion. Therefore
$t=\pi_{i}^{\pm}(\mathtt{K}\langle t^{\prime}\rangle)$, where now
$\pi_{i}^{\pm}(\mathtt{K})$ is an eliminative context.

    3. 3.3

Case, $\delta^{\pm}S\,[_{x}.N_{1}][_{x}.N_{2}]$: by inversion of the typing
rules, we have that either $\Gamma\vdash S:(A\lor B){}^{+}$ or $\Gamma\vdash
S:(A\land B){}^{-}$. In both cases we may apply the second item of this lemma
to conclude that $S$ is of the form $S=\mathtt{K}\langle t^{\prime}\rangle$
where $\mathtt{K}$ is an eliminative context and $t^{\prime}$ is an open
explosion. Therefore $t=\delta^{\pm}(\mathtt{K}\langle
t^{\prime}\rangle)\,[_{x}.N_{1}][_{x}.N_{2}]$, where now
$\delta^{\pm}(\mathtt{K})\,[_{x}.N_{1}][_{x}.N_{2}]$ is an eliminative
context.

    4. 3.4

Classical elimination, $S\bullet\\!\\!^{\pm}\,N$: then $t$ is an explosion
under the empty eliminative context. Moreover, $S$ must have at least one free
variable so $t$ is indeed an open explosion.

    5. 3.5

Negation elimination, $\mu^{\pm}S$: by inversion of the typing rules, we have
that $\Gamma\vdash S:(\neg A)^{\pm}$. By the second item of this lemma, $S$ is
of the form $S=\mathtt{K}\langle t^{\prime}\rangle$ where $\mathtt{K}$ is a
case-context and $t^{\prime}$ is an open explosion. Therefore
$t=\mu^{\pm}\mathtt{K}\langle t^{\prime}\rangle$, where now
$\mu^{\pm}\mathtt{K}$ is an eliminative context.

    6. 3.6

Absurdity, $S\mathrel{{\RHD\\!\\!\\!\LHD}}N$ or
$N\mathrel{{\RHD\\!\\!\\!\LHD}}S$: then $t$ is an explosion under the empty
eliminative context. Moreover, $S$ must have at least one free variable so $t$
is indeed an open explosion.

∎

###  .10 Proof that $\lambda^{\textsc{prk}}_{\eta}$ is Strongly Normalizing
and Confluent (Thm. 37)

######  Lemma 58 (Local confluence).

The $\lambda^{\textsc{prk}}_{\eta}$-calculus has the weak Church–Rosser
property.

###### Proof.

Let $t_{0}\xrightarrow{}t_{1}$ and $t_{0}\xrightarrow{}t_{2}$, and let us show
that the diagram can be closed, i.e. that there is a term $t_{3}$ such that
$t_{1}\mathrel{\rightarrow^{*}}t_{3}$ and
$t_{2}\mathrel{\rightarrow^{*}}t_{3}$. The proof is by induction on $t_{0}$
and by case analysis on the relative positions of the steps
$t_{0}\xrightarrow{}t_{1}$ and $t_{0}\xrightarrow{}t_{2}$. Most cases are
straightforward by resorting to the IH. We study only the interesting cases,
when the patterns of the redexes overlap. There are two such cases:

  1. 1.

$\mathsf{beta}$/$\mathsf{eta}$: Let $x\notin\mathsf{fv}(t)$. The overlap
involves a step
$(\mathsf{IC}^{\pm}_{x}.\,t\bullet\\!\\!^{\pm}\,x)\bullet\\!\\!^{\pm}\,s\xrightarrow{\mathsf{beta}}t\bullet\\!\\!^{\pm}\,s$
and a step
$(\mathsf{IC}^{\pm}_{x}.\,t\bullet\\!\\!^{\pm}\,x)\bullet\\!\\!^{\pm}\,s\xrightarrow{\mathsf{eta}}t\bullet\\!\\!^{\pm}\,s$,
so the diagram is trivially closed in zero rewriting steps.

  2. 2.

$\mathsf{eta}$/$\mathsf{beta}$: Let $x\notin\mathsf{fv}(t)$. The overlap
involves a step
$\mathsf{IC}^{\pm}_{x}.\,(\mathsf{IC}^{\pm}_{y}.\,t)\bullet\\!\\!^{\pm}\,x\xrightarrow{\mathsf{eta}}\mathsf{IC}^{\pm}_{y}.\,t$
and a step
$\mathsf{IC}^{\pm}_{x}.\,(\mathsf{IC}^{\pm}_{y}.\,t)\bullet\\!\\!^{\pm}\,x\xrightarrow{\mathsf{beta}}\mathsf{IC}^{\pm}_{x}.\,t[y\\!:=\\!x]$.
Note that the targets of the steps are $\alpha$-equivalent, so the diagram is
trivially closed in zero rewriting steps.

∎

######  Lemma 59 (Properties of reduction in $\lambda^{\textsc{prk}}_{\eta}$).

  1. 1.

Reduction does not create free variables. If $t\to t^{\prime}$ then
$\mathsf{fv}(t)\supseteq\mathsf{fv}(t^{\prime})$.

  2. 2.

Substitution (I). Let $\Gamma,x:A\vdash t:B$ and $\Gamma\vdash s:A$. If $t\to
t^{\prime}$ then $t[x\\!:=\\!s]\to t^{\prime}[x\\!:=\\!s]$.

  3. 3.

Substitution (II). Let $\Gamma,x:A\vdash t:B$ and $\Gamma\vdash s:A$. If $s\to
s^{\prime}$ then
$t[x\\!:=\\!s]\mathrel{\rightarrow^{*}}t[x\\!:=\\!s^{\prime}]$.

  4. 4.

Substitution (III). Let $\Gamma,x:A\vdash t:B$ and $\Gamma\vdash s:A$. If
$t\mathrel{\rightarrow^{*}}t^{\prime}$ and
$s\mathrel{\rightarrow^{*}}s^{\prime}$ then
$t[x\\!:=\\!s]\mathrel{\rightarrow^{*}}t^{\prime}[x\\!:=\\!s^{\prime}]$.

###### Proof.

Items 1., 2., and 3. are by induction on $t$. Item 4. is by induction on the
sum of the lengths of the sequences $t\mathrel{\rightarrow^{*}}t^{\prime}$ and
$s\mathrel{\rightarrow^{*}}s^{\prime}$, resorting to the two previous items. ∎

######  Lemma 60 (Postponement of $\mathsf{eta}$ steps).

Let $t\xrightarrow{\mathsf{eta}}s\xrightarrow{\mathsf{r}}u$ where $\mathsf{r}$
is a rewriting rule other than $\mathsf{eta}$. Then there exists a term
$s^{\prime}$ such that
$t\mathrel{\xrightarrow{\mathsf{r}}\\!\\!{}^{+}\,\,}s^{\prime}\mathrel{\xrightarrow{\mathsf{eta}}\\!\\!{}^{*}\,\,}u$.

###### Proof.

By induction on $t$. If the $\mathsf{eta}$ step and the $\mathsf{r}$ step are
not reduction steps at the root, it is immediate to conclude, resorting to the
IH when appropriate.

If the $\mathsf{eta}$ step is at the root, then the first step is of the form
$t=\mathsf{IC}^{\pm}_{x}.\,(s\bullet\\!\\!^{\pm}\,x)\xrightarrow{\mathsf{eta}}s$,
where $x\notin\mathsf{fv}(s)$. Taking
$s^{\prime}:=\mathsf{IC}^{\pm}_{x}.\,(u\bullet\\!\\!^{\pm}\,x)$ we have that
$t=\mathsf{IC}^{\pm}_{x}.\,(s\bullet\\!\\!^{\pm}\,x)\xrightarrow{\mathsf{r}}\mathsf{IC}^{\pm}_{x}.\,(u\bullet\\!\\!^{\pm}\,x)\xrightarrow{\mathsf{eta}}u$,
so we are done. For the last reduction step, we use the fact that reduction
does not create free variables (Lem. 59).

Otherwise, we have that the $\mathsf{eta}$ step is not at the root and the
$\mathsf{r}$ step is at the root. Then we proceed by case analysis, depending
on the kind of rule applied. We only study the positive cases (the negative
cases are symmetric):

  1. 1.

$\mathsf{proj}$: then we have that
$t\xrightarrow{\mathsf{eta}}s=\pi_{i}^{+}(\langle
s_{1},s_{2}\rangle{}^{+})\xrightarrow{\mathsf{proj}}s_{i}$. Recall that the
$\mathsf{eta}$ step is not at the root of $t$. Moreover, it cannot be the case
that $t=\pi_{i}^{+}(t^{\prime})$ and the $\mathsf{eta}$ step is at the root of
$t^{\prime}$, because the type of $t^{\prime}$ must be of the form $(A\land
B){}^{+}$ but the $\mathsf{eta}$ rule can only be applied on a term
constructed with a $\mathsf{IC}^{\pm}_{-}.\,-$, whose type is classical. This
means that $t$ must be of the form $\pi_{i}^{+}(\langle
t_{1},t_{2}\rangle{}^{+})$ and that the $\mathsf{eta}$ step is either internal
to $t_{1}$ or internal to $t_{2}$, which implies that
$t_{1}\mathrel{\xrightarrow{\mathsf{eta}}\\!\\!{}^{*}\,\,}s_{1}$ and
$t_{2}\mathrel{\xrightarrow{\mathsf{eta}}\\!\\!{}^{*}\,\,}s_{2}$. Taking
$s^{\prime}:=t_{i}$ we have that $t=\pi_{i}^{+}(\langle
t_{1},t_{2}\rangle{}^{+})\xrightarrow{\mathsf{proj}}t_{i}\mathrel{\xrightarrow{\mathsf{eta}}\\!\\!{}^{*}\,\,}s_{i}$,
as required.

  2. 2.

$\mathsf{case}$: then we have that
$t\xrightarrow{\mathsf{eta}}s=\delta{}^{+}\mathsf{in}_{i}\\!\\!{}^{+}(s_{0})\,[_{y}.s_{1}][_{y}.s_{2}]\xrightarrow{\mathsf{case}}s_{i}[y\\!:=\\!s_{0}]$.
Recall that the $\mathsf{eta}$ step is not at the root of $t$. Moreover, it
cannot be the case that $t=\delta{}^{+}t^{\prime}\,[_{y}.s_{1}][_{y}.s_{2}]$
and the $\mathsf{eta}$ step is at the root of $t^{\prime}$, because the type
of $t^{\prime}$ must be of the form $(A\lor B){}^{+}$, but the $\mathsf{eta}$
rule can only be applied on a term constructed with a
$\mathsf{IC}^{\pm}_{-}.\,-$, whose type is classical. This means that $t$ must
be of the form
$\delta{}^{+}\mathsf{in}_{i}\\!\\!{}^{+}(t_{0})\,[_{y}.t_{1}][_{y}.t_{2}]$ and
that the $\mathsf{eta}$-step is either internal to $t_{0}$, or internal to
$t_{1}$, or internal to $t_{2}$, which implies that
$t_{0}\mathrel{\xrightarrow{\mathsf{eta}}\\!\\!{}^{*}\,\,}s_{0}$ and
$t_{1}\mathrel{\xrightarrow{\mathsf{eta}}\\!\\!{}^{*}\,\,}s_{1}$ and
$t_{2}\mathrel{\xrightarrow{\mathsf{eta}}\\!\\!{}^{*}\,\,}s_{2}$. Taking
$s^{\prime}:=t_{i}[y\\!:=\\!t_{0}]$ we have that
$t=\delta{}^{+}\mathsf{in}_{i}\\!\\!{}^{+}(t_{0})\,[_{y}.t_{1}][_{y}.t_{2}]\xrightarrow{\mathsf{case}}t_{i}[y\\!:=\\!t_{0}]\mathrel{\xrightarrow{\mathsf{eta}}\\!\\!{}^{*}\,\,}s_{i}[y\\!:=\\!s_{0}]$
resorting to Lem. 59 for the last step.

  3. 3.

$\mathsf{neg}$: then we have that
$t\xrightarrow{\mathsf{eta}}\mu{}^{+}(\nu{}^{+}s_{1})\xrightarrow{\mathsf{neg}}s_{1}$.
Recall that the $\mathsf{eta}$-reduction step is not at the root of $t$.
Moreover, it cannot be the case that $t=\mu{}^{+}t^{\prime}$ and the
$\mathsf{eta}$-reduction step is at the root of $t^{\prime}$, because the type
of $t^{\prime}$ must be of the form $(\neg A){}^{+}$ but the $\mathsf{eta}$
rule can only be applied on a term constructed with a
$\mathsf{IC}^{\pm}_{-}.\,-$, whose type is classical. This means that $t$ must
be of the form $\mu{}^{+}(\nu{}^{+}t_{1})$ and that the $\mathsf{eta}$ step is
internal to $t_{1}$, i.e. $t_{1}\xrightarrow{\mathsf{eta}}s_{1}$. Then taking
$s^{\prime}:=t_{1}$ we have that
$t=\mu{}^{+}(\nu{}^{+}t_{1})\xrightarrow{\mathsf{neg}}t_{1}\xrightarrow{\mathsf{eta}}s_{1}$
as required.

  4. 4.

$\mathsf{beta}$: then we have that
$t\xrightarrow{\mathsf{eta}}(\mathsf{IC}{}^{+}_{y}.\,s_{1})\bullet\\!\\!{}^{+}\,s_{2}\xrightarrow{\mathsf{beta}}s_{1}[y\\!:=\\!s_{2}]$.
Recall that the $\mathsf{eta}$ step is not at the root of $t$. There are three
cases, depending on the position of the $\mathsf{eta}$-step:

    1. 4.1

Immediately to the left of the application. That is,
$t=t^{\prime}\bullet\\!\\!{}^{+}\,s_{2}$ and the $\mathsf{eta}$ step is at the
root of $t^{\prime}$, i.e.
$t^{\prime}\xrightarrow{\mathsf{eta}}\mathsf{IC}{}^{+}_{y}.\,s_{1}$ is a
reduction step at the root. Then
$t^{\prime}=\mathsf{IC}{}^{+}_{x}.\,((\mathsf{IC}{}^{+}_{y}.\,s_{1})\bullet\\!\\!{}^{+}\,x)$.
Hence taking $s^{\prime}:=s_{1}[y\\!:=\\!s_{2}]$ we have that

$\begin{array}[]{cl}&t=(\mathsf{IC}{}^{+}_{x}.\,((\mathsf{IC}{}^{+}_{y}.\,s_{1})\bullet\\!\\!{}^{+}\,x))\bullet\\!\\!{}^{+}\,s_{2}\\\
\xrightarrow{\mathsf{beta}}&(\mathsf{IC}{}^{+}_{y}.\,s_{1})\bullet\\!\\!{}^{+}\,s_{2}\\\
\xrightarrow{\mathsf{beta}}&s_{1}[y\\!:=\\!s_{2}]\end{array}$

using two $\mathsf{beta}$ steps and no $\mathsf{eta}$ steps.

    2. 4.2

Inside the abstraction. That is,
$t=(\mathsf{IC}{}^{+}_{y}.\,t_{1})\bullet\\!\\!{}^{+}\,s_{2}$ with
$t_{1}\xrightarrow{\mathsf{eta}}s_{1}$. Then taking
$s^{\prime}:=t_{1}[y\\!:=\\!s_{2}]$ we have that
$t=(\mathsf{IC}{}^{+}_{y}.\,t_{1})\bullet\\!\\!{}^{+}\,s_{2}\xrightarrow{\mathsf{beta}}t_{1}[y\\!:=\\!s_{2}]\xrightarrow{\mathsf{eta}}s_{1}[y\\!:=\\!s_{2}]$
resorting to Lem. 59 for the last step.

    3. 4.3

To the right of the application. That is,
$t=(\mathsf{IC}{}^{+}_{y}.\,s_{1})\bullet\\!\\!{}^{+}\,t_{2}$ with
$t_{2}\xrightarrow{\mathsf{eta}}s_{2}$. Then taking
$s^{\prime}:=s_{1}[y\\!:=\\!t_{2}]$ we have that
$t=(\mathsf{IC}{}^{+}_{y}.\,s_{1})\bullet\\!\\!{}^{+}\,t_{2}\xrightarrow{\mathsf{beta}}s_{1}[y\\!:=\\!t_{2}]\mathrel{\xrightarrow{\mathsf{eta}}\\!\\!{}^{*}\,\,}s_{1}[y\\!:=\\!s_{2}]$
resorting to Lem. 59 for the last step.

  5. 5.

$\mathsf{absPairInj}$: then we have that $t\xrightarrow{\mathsf{eta}}\langle
s_{1},s_{2}\rangle{}^{+}\mathrel{{\RHD\\!\\!\\!\LHD}}\mathsf{in}_{i}\\!\\!{}^{-}(s_{3})\xrightarrow{\mathsf{absPairInj}}s_{i}\mathrel{\bowtie}s_{3}$.
Recall that the $\mathsf{eta}$ step is not at the root of $t$. Moreover, it
cannot be the case that
$t=t^{\prime}\mathrel{{\RHD\\!\\!\\!\LHD}}\mathsf{in}_{i}\\!\\!{}^{-}(s_{3})$
and the $\mathsf{eta}$ step is at the root of $t^{\prime}$, because the type
of $t^{\prime}$ must be of the form $(A\land B){}^{+}$, but the $\mathsf{eta}$
rule can only be applied on a term constructed with a
$\mathsf{IC}^{\pm}_{-}.\,-$, whose type is classical. For similar reasons, it
cannot be the case that $t=\langle
s_{1},s_{2}\rangle{}^{+}\mathrel{{\RHD\\!\\!\\!\LHD}}t^{\prime}$ with the
$\mathsf{eta}$ step is at the root of $t^{\prime}$, because then the type of
$t^{\prime}$ must be of the form $(A\land B){}^{-}$. This means that $t$ must
be of the form $\langle
t_{1},t_{2}\rangle{}^{+}\mathrel{{\RHD\\!\\!\\!\LHD}}\mathsf{in}_{i}\\!\\!{}^{-}(t_{3})$
and that the $\mathsf{eta}$ step is either internal to $t_{1}$, or internal to
$t_{2}$, or internal to $t_{3}$. This implies that
$t_{1}\mathrel{\xrightarrow{\mathsf{eta}}\\!\\!{}^{*}\,\,}s_{1}$ and
$t_{2}\mathrel{\xrightarrow{\mathsf{eta}}\\!\\!{}^{*}\,\,}s_{2}$ and
$t_{3}\mathrel{\xrightarrow{\mathsf{eta}}\\!\\!{}^{*}\,\,}s_{3}$. Taking
$s^{\prime}:=t_{i}\mathrel{\bowtie}t_{3}$ we have that $t=\langle
t_{1},t_{2}\rangle{}^{+}\mathrel{{\RHD\\!\\!\\!\LHD}}\mathsf{in}_{i}\\!\\!{}^{-}(t_{3})\xrightarrow{\mathsf{absPairInj}}t_{i}\mathrel{\bowtie}t_{3}=(t_{i}\bullet\\!\\!{}^{+}\,t_{3})\mathrel{{\RHD\\!\\!\\!\LHD}}(t_{3}\bullet\\!\\!{}^{-}\,t_{i})\mathrel{\xrightarrow{\mathsf{eta}}\\!\\!{}^{*}\,\,}(s_{i}\bullet\\!\\!{}^{+}\,s_{3})\mathrel{{\RHD\\!\\!\\!\LHD}}(s_{3}\bullet\\!\\!{}^{-}\,s_{i})=s_{i}\mathrel{\bowtie}s_{3}$.

  6. 6.

$\mathsf{absInjPair}$: Symmetric to the previous case.

  7. 7.

$\mathsf{absNeg}$: then we have that
$t\xrightarrow{\mathsf{eta}}(\nu{}^{+}s_{1})\mathrel{{\RHD\\!\\!\\!\LHD}}(\nu{}^{-}s_{2})\xrightarrow{\mathsf{absNeg}}s_{1}\mathrel{\bowtie}s_{2}$.
Recall that the $\mathsf{eta}$ step is not at the root of $t$. Moreover, it
cannot be the case that
$t=t^{\prime}\mathrel{{\RHD\\!\\!\\!\LHD}}(\nu{}^{-}s_{2})$ and the
$\mathsf{eta}$ step is at the root of $t^{\prime}$, because the type of
$t^{\prime}$ must be of the form $(\neg A){}^{+}$, but the $\mathsf{eta}$ rule
can only be applied on a term constructed with a $\mathsf{IC}^{\pm}_{-}.\,-$,
whose type is classical. For similar reasons, it cannot be the case that
$t=\nu{}^{+}s_{1}\mathrel{{\RHD\\!\\!\\!\LHD}}t^{\prime}$ with the
$\mathsf{eta}$ step is at the root of $t^{\prime}$, because then the type of
$t^{\prime}$ must be of the form $(\neg A){}^{-}$. This means that $t$ must be
of the form $(\nu{}^{+}t_{1})\mathrel{{\RHD\\!\\!\\!\LHD}}(\nu{}^{-}t_{2})$
and that the $\mathsf{eta}$ step is either internal to $t_{1}$ or internal to
$t_{2}$. This implies that
$t_{1}\mathrel{\xrightarrow{\mathsf{eta}}\\!\\!{}^{*}\,\,}s_{1}$ and
$t_{2}\mathrel{\xrightarrow{\mathsf{eta}}\\!\\!{}^{*}\,\,}s_{2}$. Taking
$s^{\prime}:=t_{1}\mathrel{\bowtie}t_{2}$ we have that
$t=(\nu{}^{+}t_{1})\mathrel{{\RHD\\!\\!\\!\LHD}}(\nu{}^{-}t_{2})\xrightarrow{\mathsf{absNeg}}t_{1}\mathrel{\bowtie}t_{2}=(t_{1}\bullet\\!\\!{}^{+}\,t_{2})\mathrel{{\RHD\\!\\!\\!\LHD}}(t_{2}\bullet\\!\\!{}^{+}\,t_{1})\mathrel{\xrightarrow{\mathsf{eta}}\\!\\!{}^{*}\,\,}(s_{1}\bullet\\!\\!{}^{+}\,s_{2})\mathrel{{\RHD\\!\\!\\!\LHD}}(s_{2}\bullet\\!\\!{}^{+}\,s_{1})=s_{1}\mathrel{\bowtie}s_{2}$.

∎

######  Theorem 61.

The $\lambda^{\textsc{prk}}_{\eta}$-calculus is strongly normalizing and
confluent.

###### Proof.

Strong normalization follows from postponement of the $\mathsf{eta}$ rule
(Lem. 60) and strong normalization of the calculus without $\mathsf{eta}$
(Thm. 32) by the usual rewriting techniques.

More precisely, let us write $\xrightarrow{\neg\mathsf{eta}}$ for reduction
not using $\mathsf{eta}$, that is,
$\xrightarrow{\neg\mathsf{eta}}\,\mathrel{\overset{\mathrm{def}}{=}}\,(\xrightarrow{\,}\setminus\xrightarrow{\mathsf{eta}})$.
Suppose there is an infinite reduction sequence $t_{1}\to t_{2}\to
t_{3}\ldots$ in $\lambda^{\textsc{prk}}_{\eta}$. Let
$t_{1}\mathrel{\xrightarrow{\neg\mathsf{eta}}\\!\\!{}^{*}\,\,}t_{i}$ be the
longest prefix of the sequence whose steps are not $\mathsf{eta}$ steps. This
prefix cannot be infinite given that $\lambda^{\textsc{prk}}$ is strongly
normalizing. Let
$t_{i}\mathrel{\xrightarrow{\mathsf{eta}}\\!\\!{}^{*}\,\,}t_{i+n}$ be the
longest sequence of $\mathsf{eta}$ steps starting on $t_{i}$. This sequence
cannot be infinite given that an $\mathsf{eta}$ step decreases the size of the
term. Now there must be a step
$t_{i+n}\xrightarrow{\neg\mathsf{eta}}t_{i+n+1}$. Applying the postponement
lemma (Lem. 60) $n$ times, we obtain an infinite sequence of the form
$t_{1}\mathrel{\xrightarrow{\neg\mathsf{eta}}\\!\\!{}^{*}\,\,}t_{i}\xrightarrow{\neg\mathsf{eta}}t^{\prime}_{i+1}\ldots$.
By repeatedly applying this argument, we may build an infinite sequence of
$\xrightarrow{\neg\mathsf{eta}}$ steps, contradicting the fact that
$\lambda^{\textsc{prk}}$ is strongly normalizing.

Confluence of $\lambda^{\textsc{prk}}_{\eta}$ follows from the fact that it is
strongly normalizing and locally confluent (Lem. 58), resorting to Newman’s
Lemma [36, Theorem 1.2.1]. ∎

###  .11 Computation Rules for the Embedding of Classical Logic into prk

The statements of all of the following lemmas are in
$\lambda^{\textsc{prk}}_{\eta}$ (with $\mathsf{eta}$ reduction).

####  .11.1 Simulation of conjunction

######  Definition 62 (Conjunction introduction).

Let $\Gamma\vdash t:A{}^{\oplus}$ and $\Gamma\vdash s:B{}^{\oplus}$. Then
$\Gamma\vdash\langle t,s\rangle^{\mathcal{C}}:(A\land B){}^{\oplus}$ where:

$\langle
t,s\rangle^{\mathcal{C}}\,\mathrel{\overset{\mathrm{def}}{=}}\,\mathsf{IC}{}^{+}_{(\underline{\,\,\,}:(A\land
B){}^{\ominus})}.\,\langle t,s\rangle{}^{+}$

######  Definition 63 (Conjunction elimination).

Let $\Gamma\vdash t:(A_{1}\land A_{2}){}^{\oplus}$. Then
$\Gamma\vdash\pi_{i}^{\mathcal{C}}(t):A_{i}{}^{\oplus}$ where:

$\pi_{i}^{\mathcal{C}}(t)\,\mathrel{\overset{\mathrm{def}}{=}}\,\mathsf{IC}{}^{+}_{(x:A_{i}{}^{\ominus})}.\,\pi_{i}^{+}(t\bullet\\!\\!{}^{+}\,\mathsf{IC}{}^{-}_{(\underline{\,\,\,}:(A_{1}\land
A_{2}){}^{\oplus})}.\,\mathsf{in}_{i}\\!\\!{}^{-}(x))\bullet\\!\\!{}^{+}\,x$

######  Lemma 64.

$\pi_{i}^{\mathcal{C}}(\langle
t_{1},t_{2}\rangle^{\mathcal{C}})\mathrel{\rightarrow^{*}}t_{i}$

###### Proof.

${\small\begin{array}[]{rcll}&&\pi_{i}^{\mathcal{C}}(\langle
t_{1},t_{2}\rangle^{\mathcal{C}})\\\
&=&\mathsf{IC}{}^{+}_{x:A_{i}{}^{\ominus}}.\,\pi_{i}^{+}((\mathsf{IC}{}^{+}_{\underline{\,\,\,}}.\,\langle
t_{1},t_{2}\rangle{}^{+})\bullet\\!\\!{}^{+}\,\mathsf{IC}{}^{-}_{\underline{\,\,\,}}.\,\mathsf{in}_{i}\\!\\!{}^{-}(x))\bullet\\!\\!{}^{+}\,x\\\
&\xrightarrow{\mathsf{beta}}&\mathsf{IC}{}^{+}_{x:A_{i}{}^{\ominus}}.\,\pi_{i}^{+}(\langle
t_{1},t_{2}\rangle{}^{+})\bullet\\!\\!{}^{+}\,x\\\
&\xrightarrow{\mathsf{proj}}&\mathsf{IC}{}^{+}_{x:A_{i}{}^{\ominus}}.\,t_{i}\bullet\\!\\!{}^{+}\,x\\\
&\xrightarrow{\mathsf{eta}}&t_{i}\end{array}}$

∎

####  .11.2 Simulation of disjunction

######  Definition 65 (Disjunction introduction).

Let $\Gamma\vdash t:A_{i}{}^{\oplus}$. Then
$\Gamma\vdash\mathsf{in}_{i}^{\mathcal{C}}(t):(A_{1}\lor A_{2}){}^{\oplus}$
where:

$\mathsf{in}_{i}^{\mathcal{C}}(t)\,\mathrel{\overset{\mathrm{def}}{=}}\,\mathsf{IC}{}^{+}_{(\underline{\,\,\,}:(A_{1}\lor
A_{2}){}^{\ominus})}.\,\mathsf{in}_{i}\\!\\!{}^{+}(t)$

######  Definition 66 (Disjunction elimination).

Let $\Gamma\vdash t:(A\lor B){}^{\oplus}$ and $\Gamma,x:A{}^{\oplus}\vdash
s:C{}^{\oplus}$ and $\Gamma,x:B{}^{\oplus}\vdash u:C{}^{\oplus}$. Then
$\Gamma\vdash\delta^{\mathcal{C}}t\,[_{(x:A{}^{\oplus})}.s][_{(x:B{}^{\oplus})}.u]:C{}^{\oplus}$,
where:

$\mathsf{IC}{}^{+}_{(y:C{}^{\ominus})}.\,\begin{array}[t]{l@{\
}l}\delta{}^{+}&(t\bullet\\!\\!{}^{+}\,\mathsf{IC}{}^{-}_{(\underline{\,\,\,}:(A\lor
B){}^{\oplus})}.\,\langle{\updownarrow_{x}^{y}(s)},{\updownarrow_{x}^{y}(u)}\rangle{}^{-})\\\
&[_{(x:A{}^{\oplus})}.s\bullet\\!\\!{}^{+}\,y]\\\
&[_{(x:B{}^{\oplus})}.u\bullet\\!\\!{}^{+}\,y]\\\ \end{array}$

######  Lemma 67.

$\delta^{\mathcal{C}}\mathsf{in}_{i}^{\mathcal{C}}(t_{i})\,[_{x}.s_{1}][_{x}.s_{2}]\mathrel{\rightarrow^{*}}s_{i}[x\\!:=\\!t]$

###### Proof.

${\small\begin{array}[]{rcll}&&\delta^{\mathcal{C}}\mathsf{in}_{i}^{\mathcal{C}}(t_{i})\,[_{x}.s_{1}][_{x}.s_{2}]\\\
&=&\begin{array}[t]{l}\mathsf{IC}{}^{+}_{(y:C{}^{\ominus})}.\\\ \
\begin{array}[t]{l@{\
}l}\delta{}^{+}&\left(\begin{array}[]{l@{}l}&\mathsf{IC}{}^{+}_{(\underline{\,\,\,}:(A_{1}\lor
A_{2}){}^{\ominus})}.\,\mathsf{in}_{i}\\!\\!{}^{+}(t)\\\
\bullet\\!\\!{}^{+}&\mathsf{IC}{}^{-}_{(\underline{\,\,\,}:(A\lor
B){}^{\oplus})}.\,\langle{\updownarrow_{x}^{y}(s_{1})},{\updownarrow_{x}^{y}(s_{2})}\rangle{}^{-}\end{array}\right)\\\
&[_{(x:A{}^{\oplus})}.s_{1}\bullet\\!\\!{}^{+}\,y]\\\
&[_{(x:B{}^{\oplus})}.s_{2}\bullet\\!\\!{}^{+}\,y]\\\
\end{array}\end{array}\\\
&\xrightarrow{\mathsf{beta}}&\mathsf{IC}{}^{+}_{(y:C{}^{\ominus})}.\,\delta{}^{+}\mathsf{in}_{i}\\!\\!{}^{+}(t)\,[_{(x:A{}^{\oplus})}.s_{1}\bullet\\!\\!{}^{+}\,y][_{(x:B{}^{\oplus})}.s_{2}\bullet\\!\\!{}^{+}\,y]\\\
&\xrightarrow{\mathsf{case}}&\mathsf{IC}{}^{+}_{(y:C{}^{\ominus})}.\,s_{i}[x\\!:=\\!t]\bullet\\!\\!{}^{+}\,y\\\
&\xrightarrow{\mathsf{eta}}&s_{i}[x\\!:=\\!t]\end{array}}$

∎

####  .11.3 Simulation of negation

######  Definition 68 (Negation introduction).

By Lem. 20 we have that
$\Gamma\vdash\pitchfork^{-}_{\alpha_{0}}:(\alpha_{0}\land\neg\alpha_{0}){}^{\ominus}$,
that is $\Gamma\vdash\pitchfork^{-}_{\alpha_{0}}:\bot{}^{\ominus}$. Moreover,
suppose that $\Gamma,x:A{}^{\oplus}\vdash t:\bot{}^{\oplus}$. Then
$\Gamma\vdash\Lambda^{\mathcal{C}}_{(x:A{}^{\oplus})}.\,t:(\neg
A){}^{\oplus}$, where:

$\Lambda^{\mathcal{C}}_{(x:A{}^{\oplus})}.\,t\,\mathrel{\overset{\mathrm{def}}{=}}\,\mathsf{IC}{}^{+}_{(\underline{\,\,\,}:(\neg
A){}^{\ominus})}.\,\nu{}^{+}\mathsf{IC}{}^{-}_{(x:A{}^{\oplus})}.\,(t\mathrel{\bowtie_{A{}^{-}}}\pitchfork^{-}_{\alpha_{0}})$

######  Definition 69 (Negation elimination).

Let $\Gamma\vdash t:(\neg A){}^{\oplus}$ and $\Gamma\vdash s:A{}^{\oplus}$.
Then $\Gamma\vdash t\texttt{{\\#}}^{\mathcal{C}}s:\bot{}^{\oplus}$, where:

$t\texttt{{\\#}}^{\mathcal{C}}s\,\mathrel{\overset{\mathrm{def}}{=}}\,t\mathrel{\bowtie_{\bot{}^{\oplus}}}\mathsf{IC}{}^{-}_{(\underline{\,\,\,}:(\neg
A){}^{\oplus})}.\,\nu{}^{-}s$

######  Lemma 70.

$(\Lambda^{\mathcal{C}}_{x}.\,t)\texttt{{\\#}}^{\mathcal{C}}s\mathrel{\rightarrow^{*}}(t[x\\!:=\\!s]\mathrel{\bowtie}\pitchfork^{-}_{\alpha_{0}})\mathrel{{\RHD\\!\\!\\!\LHD}}(s\bullet\\!\\!{}^{-}\,(\mathsf{IC}{}^{-}_{x}.\,(t\mathrel{\bowtie}\pitchfork^{-}_{\alpha_{0}})))$

###### Proof.

${\small\begin{array}[]{rl}&(\Lambda^{\mathcal{C}}_{x}.\,t)\texttt{{\\#}}^{\mathcal{C}}s\\\
\\\
=&(\mathsf{IC}{}^{+}_{\underline{\,\,\,}}.\,\nu{}^{+}\mathsf{IC}{}^{-}_{x}.\,(t\mathrel{\bowtie}\pitchfork^{-}_{\alpha_{0}}))\mathrel{\bowtie_{\bot{}^{\oplus}}}\mathsf{IC}{}^{-}_{\underline{\,\,\,}}.\,\nu{}^{-}s\\\
\\\
=&\begin{array}[t]{l@{}l}&((\mathsf{IC}{}^{+}_{\underline{\,\,\,}}.\,\nu{}^{+}\mathsf{IC}{}^{-}_{x}.\,(t\mathrel{\bowtie}\pitchfork^{-}_{\alpha_{0}}))\bullet\\!\\!{}^{+}\,\mathsf{IC}{}^{-}_{\underline{\,\,\,}}.\,\nu{}^{-}s)\\\
{\RHD\\!\\!\\!\LHD}&(\mathsf{IC}{}^{-}_{\underline{\,\,\,}}.\,\nu{}^{-}s\bullet\\!\\!{}^{-}\,(\mathsf{IC}{}^{+}_{\underline{\,\,\,}}.\,\nu{}^{+}\mathsf{IC}{}^{-}_{x}.\,(t\mathrel{\bowtie}\pitchfork^{-}_{\alpha_{0}})))\end{array}\\\
\\\
\xrightarrow{\mathsf{beta}}(2)&(\nu{}^{+}\mathsf{IC}{}^{-}_{x}.\,(t\mathrel{\bowtie}\pitchfork^{-}_{\alpha_{0}}))\mathrel{{\RHD\\!\\!\\!\LHD}}(\nu{}^{-}s)\\\
\\\
\xrightarrow{\mathsf{absNeg}}&((\mathsf{IC}{}^{-}_{x}.\,(t\mathrel{\bowtie}\pitchfork^{-}_{\alpha_{0}}))\bullet\\!\\!{}^{+}\,s)\mathrel{{\RHD\\!\\!\\!\LHD}}(s\bullet\\!\\!{}^{-}\,(\mathsf{IC}{}^{-}_{x}.\,(t\mathrel{\bowtie}\pitchfork^{-}_{\alpha_{0}})))\\\
\\\
\xrightarrow{\mathsf{beta}}&(t[x\\!:=\\!s]\mathrel{\bowtie}\pitchfork^{-}_{\alpha_{0}})\mathrel{{\RHD\\!\\!\\!\LHD}}(s\bullet\\!\\!{}^{-}\,(\mathsf{IC}{}^{-}_{x}.\,(t\mathrel{\bowtie}\pitchfork^{-}_{\alpha_{0}})))\end{array}}$

∎

####  .11.4 Simulation of implication

Define implication $A\Rightarrow B$ as an abbreviation of $\neg A\lor B$.

######  Definition 71 (Implication introduction).

If $\Gamma,x:A{}^{\oplus}\vdash t:B{}^{\oplus}$ then
$\Gamma\vdash\lambda^{\mathcal{C}}_{(x:A)}.\,t:(A\Rightarrow B){}^{\oplus}$
where:

${\small\begin{array}[]{rcl}\lambda^{\mathcal{C}}_{x}.\,t&\,\mathrel{\overset{\mathrm{def}}{=}}&\mathsf{IC}{}^{+}_{(y:(A\Rightarrow
B){}^{\ominus})}.\,\mathsf{in}_{2}\\!\\!{}^{+}(t[x\\!:=\\!\mathbf{X}_{y}])\\\
\mathbf{X}_{y}&\,\mathrel{\overset{\mathrm{def}}{=}}&\mathsf{IC}{}^{+}_{(z:A{}^{\ominus})}.\,(\mu{}^{-}(\mathbf{X^{\prime}}_{y,z}\bullet\\!\\!{}^{-}\,\mathsf{IC}{}^{+}_{(\underline{\,\,\,}:(\neg
A){}^{\ominus})}.\,\nu{}^{+}z))\bullet\\!\\!{}^{+}\,z\\\
\mathbf{X^{\prime}}_{y,z}&\,\mathrel{\overset{\mathrm{def}}{=}}&\pi_{1}^{+}(y\bullet\\!\\!{}^{-}\,\mathsf{IC}{}^{+}_{(\underline{\,\,\,}:(A\Rightarrow
B){}^{\ominus})}.\,\mathsf{in}_{1}\\!\\!{}^{+}(\mathsf{IC}{}^{+}_{(\underline{\,\,\,}:(\neg
A){}^{\ominus})}.\,\nu{}^{+}z))\end{array}}$

######  Definition 72 (Implication elimination).

If $\Gamma\vdash t:(A\Rightarrow B){}^{\oplus}$ and $\Gamma\vdash
s:A{}^{\oplus}$, then $\Gamma\vdash
t\,\texttt{{@}}^{\mathcal{C}}\,s:B{}^{\oplus}$, where:

${\small\begin{array}[]{r@{}c@{}l}t\,\texttt{{@}}^{\mathcal{C}}\,s&\,\mathrel{\overset{\mathrm{def}}{=}}&\begin{array}[t]{l}\mathsf{IC}{}^{+}_{(x:B{}^{\ominus})}.\\\
\ \begin{array}[t]{l@{\
}l}\delta{}^{+}&(t\bullet\\!\\!{}^{+}\,\mathsf{IC}{}^{-}_{(\underline{\,\,\,}:(A\Rightarrow
B){}^{\oplus})}.\,\langle(\mathsf{IC}{}^{-}_{(\underline{\,\,\,}:(\neg
A){}^{\oplus})}.\,\nu{}^{-}s),x\rangle{}^{-})\\\ &[_{(y:(\neg
A){}^{\oplus})}.s\mathrel{\bowtie_{B{}^{+}}}\mu{}^{-}(y\bullet\\!\\!{}^{+}\,\mathsf{IC}{}^{-}_{(\underline{\,\,\,}:(\neg
A){}^{\oplus})}.\,\nu{}^{-}x)]\\\
&[_{(z:B{}^{\oplus})}.z\bullet\\!\\!{}^{+}\,x]\\\
\end{array}\end{array}\end{array}}$

The following lemma is the computational rule for implication:

######  Lemma 73.

$(\lambda^{\mathcal{C}}_{x}.\,t)\,\texttt{{@}}^{\mathcal{C}}\,s\mathrel{\rightarrow^{*}}t[x\\!:=\\!s]$

###### Proof.

First let
$u=\mathsf{IC}{}^{-}_{\underline{\,\,\,}}.\,\langle(\mathsf{IC}{}^{-}_{\underline{\,\,\,}}.\,\nu{}^{-}s),x^{\prime}\rangle{}^{-}$
and note that:

${\small\begin{array}[]{r@{\ }c@{\ }l}&&\mathbf{X^{\prime}}_{u,z}\\\
&=&\pi_{1}^{+}(u\bullet\\!\\!{}^{-}\,\mathsf{IC}{}^{+}_{(\underline{\,\,\,}:(A\Rightarrow
B){}^{\ominus})}.\,\mathsf{in}_{1}\\!\\!{}^{+}(\mathsf{IC}{}^{+}_{(\underline{\,\,\,}:(\neg
A){}^{\ominus})}.\,\nu{}^{+}z))\\\
&\xrightarrow{\mathsf{beta}}&\pi_{1}^{+}(\langle(\mathsf{IC}{}^{-}_{\underline{\,\,\,}}.\,\nu{}^{-}s),x^{\prime}\rangle{}^{-})\\\
&\xrightarrow{\mathsf{proj}}&\mathsf{IC}{}^{-}_{\underline{\,\,\,}}.\,\nu{}^{-}s\end{array}}$

Hence:

${\small\begin{array}[]{r@{\ }c@{\ }l}&&\mathbf{X}_{u}\\\
&=&\mathsf{IC}{}^{+}_{(z:A{}^{\ominus})}.\,(\mu{}^{-}(\mathbf{X^{\prime}}_{u,z}\bullet\\!\\!{}^{-}\,\mathsf{IC}{}^{+}_{(\underline{\,\,\,}:(\neg
A){}^{\ominus})}.\,\nu{}^{+}z))\bullet\\!\\!{}^{+}\,z\\\
&\mathrel{\rightarrow^{*}}&\mathsf{IC}{}^{+}_{(z:A{}^{\ominus})}.\,(\mu{}^{-}((\mathsf{IC}{}^{-}_{\underline{\,\,\,}}.\,\nu{}^{-}s)\bullet\\!\\!{}^{-}\,\mathsf{IC}{}^{+}_{(\underline{\,\,\,}:(\neg
A){}^{\ominus})}.\,\nu{}^{+}z))\bullet\\!\\!{}^{+}\,z\\\
&\xrightarrow{\mathsf{beta}}&\mathsf{IC}{}^{+}_{(z:A{}^{\ominus})}.\,(\mu{}^{-}(\nu{}^{-}s))\bullet\\!\\!{}^{+}\,z\\\
&\xrightarrow{\mathsf{neg}}&\mathsf{IC}{}^{+}_{(z:A{}^{\ominus})}.\,s\bullet\\!\\!{}^{+}\,z\\\
&\xrightarrow{\mathsf{eta}}&s\end{array}}$

Hence:

${\small\begin{array}[]{r@{\ }c@{\
}l}&&(\lambda^{\mathcal{C}}_{x}.\,t)\,\texttt{{@}}^{\mathcal{C}}\,s\\\
&=&\begin{array}[t]{l}\mathsf{IC}{}^{+}_{x^{\prime}}.\\\ \
\begin{array}[t]{l@{\
}l}\delta{}^{+}&\left(\begin{array}[]{l@{}l}&(\mathsf{IC}{}^{+}_{y}.\,\mathsf{in}_{2}\\!\\!{}^{+}(t[x\\!:=\\!\mathbf{X}_{y}]))\\\
\bullet\\!\\!{}^{+}&\mathsf{IC}{}^{-}_{\underline{\,\,\,}}.\,\langle(\mathsf{IC}{}^{-}_{\underline{\,\,\,}}.\,\nu{}^{-}s),x^{\prime}\rangle{}^{-}\end{array}\right)\\\
&[_{y^{\prime}}.s\mathrel{\bowtie_{B{}^{+}}}\mu{}^{-}(y^{\prime}\bullet\\!\\!{}^{+}\,\mathsf{IC}{}^{-}_{\underline{\,\,\,}}.\,\nu{}^{-}x^{\prime})]\\\
&[_{z^{\prime}}.z^{\prime}\bullet\\!\\!{}^{+}\,x^{\prime}]\\\
\end{array}\end{array}\\\
&\xrightarrow{\mathsf{beta}}&\begin{array}[t]{l}\mathsf{IC}{}^{+}_{x^{\prime}}.\\\
\ \begin{array}[t]{l@{\
}l}\delta{}^{+}&\mathsf{in}_{2}\\!\\!{}^{+}(t[x\\!:=\\!\mathbf{X}_{u}])\\\
&[_{y^{\prime}}.s\mathrel{\bowtie_{B{}^{+}}}\mu{}^{-}(y^{\prime}\bullet\\!\\!{}^{+}\,\mathsf{IC}{}^{-}_{\underline{\,\,\,}}.\,\nu{}^{-}x^{\prime})]\\\
&[_{z^{\prime}}.z^{\prime}\bullet\\!\\!{}^{+}\,x^{\prime}]\\\
\end{array}\end{array}\\\
&\xrightarrow{\mathsf{case}}&\mathsf{IC}{}^{+}_{x^{\prime}}.\,t[x\\!:=\\!\mathbf{X}_{u}]\bullet\\!\\!{}^{+}\,x^{\prime}\\\
&\mathrel{\rightarrow^{*}}&\mathsf{IC}{}^{+}_{x^{\prime}}.\,t[x\\!:=\\!s]\bullet\\!\\!{}^{+}\,x^{\prime}\\\
&\xrightarrow{\mathsf{eta}}&t[x\\!:=\\!s]\end{array}}$

∎

####  .11.5 Computational content of the law of excluded middle

######  Lemma 74.

${\small\begin{array}[]{ll}&\delta^{\mathcal{C}}\pitchfork^{\mathcal{C}}_{A}\,[_{x}.s_{1}][_{x}.s_{2}]\\\
\mathrel{\rightarrow^{*}}&\mathsf{IC}{}^{+}_{y}.\,s_{2}[x\\!:=\\!\mathsf{IC}{}^{+}_{\underline{\,\,\,}}.\,\nu{}^{+}(\mathsf{IC}{}^{-}_{x}.\,s_{1}\mathrel{\bowtie}y)]\bullet\\!\\!{}^{+}\,y\end{array}}$

###### Proof.

Recall that $\pitchfork^{\mathcal{C}}_{A}=\pitchfork^{+}_{A}$, where:

${\footnotesize\begin{array}[]{r@{\,}c@{\,}l}\pitchfork^{+}_{A}&\,\mathrel{\overset{\mathrm{def}}{=}}&\mathsf{IC}{}^{+}_{(x:(A\lor\neg
A){}^{\ominus})}.\,\mathsf{in}_{2}\\!\\!{}^{+}(\mathsf{IC}{}^{+}_{(y:\neg
A{}^{\ominus})}.\,\nu{}^{+}\pi_{1}^{-}(x\bullet\\!\\!{}^{-}\,\Delta^{+}_{y,A}))\\\
\Delta^{+}_{y,A}&\,\mathrel{\overset{\mathrm{def}}{=}}&\mathsf{IC}{}^{+}_{(\underline{\,\,\,}:(A\lor\neg
A){}^{\ominus})}.\,\mathsf{in}_{1}\\!\\!{}^{+}(\mathsf{IC}{}^{+}_{(z:A{}^{\ominus})}.\,(y\mathrel{\bowtie_{A{}^{+}}}\mathsf{IC}{}^{+}_{(\underline{\,\,\,}:\neg
A{}^{\ominus})}.\,\nu{}^{+}z))\end{array}}$

Let
$u=\mathsf{IC}{}^{-}_{\underline{\,\,\,}}.\,\langle{\updownarrow_{x^{\prime}}^{y^{\prime}}(s_{1})},{\updownarrow_{x^{\prime}}^{y^{\prime}}(s_{2})}\rangle{}^{-}$.
Then:

${\small\begin{array}[]{r@{\ }c@{\
}l}&&\delta^{\mathcal{C}}\pitchfork^{\mathcal{C}}_{A}\,[_{x^{\prime}}.s_{1}][_{x^{\prime}}.s_{2}]\\\
&=&\begin{array}[t]{l}\mathsf{IC}{}^{+}_{y^{\prime}}.\\\ \
\begin{array}[t]{l@{\
}l}\delta{}^{+}&\left(\begin{array}[]{l@{}l}&\mathsf{IC}{}^{+}_{x}.\,\mathsf{in}_{2}\\!\\!{}^{+}(\mathsf{IC}{}^{+}_{y}.\,\nu{}^{+}\pi_{1}^{-}(x\bullet\\!\\!{}^{-}\,\Delta^{+}_{y,A}))\\\
\bullet\\!\\!{}^{+}&u\end{array}\right)\\\
&[_{x^{\prime}}.s_{1}\bullet\\!\\!{}^{+}\,y^{\prime}]\\\
&[_{x^{\prime}}.s_{2}\bullet\\!\\!{}^{+}\,y^{\prime}]\\\
\end{array}\end{array}\\\
&\xrightarrow{\mathsf{beta}}&\begin{array}[t]{l}\mathsf{IC}{}^{+}_{y^{\prime}}.\\\
\ \begin{array}[t]{l@{\
}l}\delta{}^{+}&\mathsf{in}_{2}\\!\\!{}^{+}(\mathsf{IC}{}^{+}_{y}.\,\nu{}^{+}\pi_{1}^{-}(u\bullet\\!\\!{}^{-}\,\Delta^{+}_{y,A}))\\\
&[_{x^{\prime}}.s_{1}\bullet\\!\\!{}^{+}\,y^{\prime}]\\\
&[_{x^{\prime}}.s_{2}\bullet\\!\\!{}^{+}\,y^{\prime}]\\\
\end{array}\end{array}\\\
&\xrightarrow{\mathsf{case}}&\mathsf{IC}{}^{+}_{y^{\prime}}.\,s_{2}[x^{\prime}\\!:=\\!\mathsf{IC}{}^{+}_{y}.\,\nu{}^{+}\pi_{1}^{-}(u\bullet\\!\\!{}^{-}\,\Delta^{+}_{y,A})]\bullet\\!\\!{}^{+}\,y^{\prime}\\\
&\xrightarrow{\mathsf{beta}}&\mathsf{IC}{}^{+}_{y^{\prime}}.\,s_{2}[x^{\prime}\\!:=\\!\mathsf{IC}{}^{+}_{\underline{\,\,\,}}.\,\nu{}^{+}\pi_{1}^{-}(\langle{\updownarrow_{x^{\prime}}^{y^{\prime}}(s_{1})},{\updownarrow_{x^{\prime}}^{y^{\prime}}(s_{2})}\rangle{}^{-})]\bullet\\!\\!{}^{+}\,y^{\prime}\\\
&\xrightarrow{\mathsf{proj}}&\mathsf{IC}{}^{+}_{y^{\prime}}.\,s_{2}[x^{\prime}\\!:=\\!\mathsf{IC}{}^{+}_{\underline{\,\,\,}}.\,\nu{}^{+}{\updownarrow_{x^{\prime}}^{y^{\prime}}(s_{1})}]\bullet\\!\\!{}^{+}\,y^{\prime}\\\
&=&\mathsf{IC}{}^{+}_{y^{\prime}}.\,s_{2}[x^{\prime}\\!:=\\!\mathsf{IC}{}^{+}_{\underline{\,\,\,}}.\,\nu{}^{+}(\mathsf{IC}{}^{-}_{x^{\prime}}.\,s_{1}\mathrel{\bowtie}y^{\prime})]\bullet\\!\\!{}^{+}\,y^{\prime}\\\
\end{array}}$

∎

## Formal Systems

###  .1 System F Extended with Recursive Type Constraints

######  Definition 75 (System F$\langle\mathcal{C}\rangle$).

The set of types is given by:

$A,B,\ldots::=\alpha\mid A\to B\mid\forall\alpha.A$

The set of terms is given by:

$t,s,\ldots::=x\mid\lambda x^{A}.\,t\mid t\,s\mid\lambda\alpha.\,t\mid t\,A$

we omit type annotations over variables when clear from the context. A type
constraint is an equation of the form $\alpha\equiv A$. Each set $\mathcal{C}$
of type constraints induces a notion of equivalence between types, written
$A\equiv B$ and defined as the congruence generated by $\mathcal{C}$. More
precisely:

${\small\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1(A\equiv B)\in\mathcal{C}$}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=48.0282pt\hbox{\kern
2.70003pt$\textsc{constr}$}}}\hbox{\kern 11.00002pt\hbox{$\displaystyle
A\equiv B$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
12.75002pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=25.50003pt\hbox{\kern
2.70003pt$\textsc{refl}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle A\equiv
A$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt
plus 0.0001fil\hbox{$\displaystyle\penalty 1A\equiv B$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=26.02817pt\hbox{\kern
2.70003pt$\textsc{sym}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle B\equiv
A$}}}}\end{array}}$ ${\small\begin{array}[]{c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1A\equiv
B\hskip 14.22636ptB\equiv C$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.225pt,depth=0.225pt,width=66.60892pt\hbox{\kern
2.70003pt$\textsc{trans}$}}}\hbox{\kern 20.39133pt\hbox{$\displaystyle A\equiv
C$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt
plus 0.0001fil\hbox{\kern 29.33356pt\hbox{$\displaystyle\penalty 1A\equiv
B$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=84.69528pt\hbox{\kern
2.70003pt$\textsc{cong}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle
C[\alpha\\!:=\\!A]\equiv C[\alpha\\!:=\\!B]$}}}}\end{array}}$

We suppose that $\mathcal{C}$ is fixed. Typing judgments are of the form
$\Gamma\vdash t:A$.

${\small\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 28.95627pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=57.91254pt\hbox{\kern
2.70003pt$\textsc{{\text{Ax}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma,x:A\vdash
x:A$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash t:A\hskip
14.22636ptA\equiv B$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=73.87956pt\hbox{\kern
2.70003pt$\textsc{Conv}$}}}\hbox{\kern
19.8632pt\hbox{$\displaystyle\Gamma\vdash t:B$}}}}\end{array}}$
${\small\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 6.76501pt\hbox{$\displaystyle\penalty 1\Gamma,x:A\vdash
t:B$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=70.07695pt\hbox{\kern
2.70003pt$\textsc{{\text{I$\rightarrow$}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash\lambda x^{A}.\,t:A\to
B$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt
plus 0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash t:A\to B\hskip
14.22636pt\Gamma\vdash s:A$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.225pt,depth=0.225pt,width=99.22333pt\hbox{\kern
2.70003pt$\textsc{E$\rightarrow$}$}}}\hbox{\kern
29.67572pt\hbox{$\displaystyle\Gamma\vdash t\,s:B$}}}}\end{array}}$
${\small\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash t:A\hskip
14.22636pt\alpha\notin\mathsf{fv}(\Gamma)$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=82.98375pt\hbox{\kern
2.70003pt$\textsc{I$\forall$}$}}}\hbox{\kern
8.29703pt\hbox{$\displaystyle\Gamma\vdash\lambda\alpha.\,t:\forall\alpha.A$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
11.02814pt\hbox{$\displaystyle\penalty 1\Gamma\vdash
t:\forall\alpha.A$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=71.93863pt\hbox{\kern
2.70003pt$\textsc{E$\forall$}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash
t\,B:A[\alpha\\!:=\\!B]$}}}}\end{array}}$

Reduction is defined as the closure by arbitrary contexts of the following
rewriting rules:

$\begin{array}[]{rcl}(\lambda x.\,t)\,s&\to&t[x\\!:=\\!s]\\\
(\lambda\alpha.\,t)\,A&\to&t[\alpha\\!:=\\!A]\\\ \end{array}$

######  Definition 76 (Positive/negative occurrences).

The set of type variables occurring positively (resp. negatively) in a type
$A$ are written $\textsf{p}(A)$ (resp. $\textsf{n}(A)$) and defined by:

${\small\begin{array}[]{r@{\ }c@{\ }l@{\hspace{.5cm}}r@{\ }c@{\
}l}\textsf{p}(\alpha)&\,\mathrel{\overset{\mathrm{def}}{=}}&\\{\alpha\\}\hfil\hskip
14.22636pt&\textsf{n}(\alpha)&\,\mathrel{\overset{\mathrm{def}}{=}}&\varnothing\\\
\textsf{p}(A\to
B)&\,\mathrel{\overset{\mathrm{def}}{=}}&\textsf{n}(A)\cup\textsf{p}(B)\hfil\hskip
14.22636pt&\textsf{n}(A\to
B)&\,\mathrel{\overset{\mathrm{def}}{=}}&\textsf{p}(A)\cup\textsf{n}(B)\\\
\textsf{p}(\forall\alpha.A)&\,\mathrel{\overset{\mathrm{def}}{=}}&\textsf{p}(A)\setminus\\{\alpha\\}\hfil\hskip
14.22636pt&\textsf{n}(\forall\alpha.A)&\,\mathrel{\overset{\mathrm{def}}{=}}&\textsf{n}(A)\setminus\\{\alpha\\}\end{array}}$

######  Definition 77 (Positivity condition).

A set of type constraints $\mathcal{C}$ verifies the positivity condition if
for every type constraint $(\alpha\equiv A)\in\mathcal{C}$ and every type $B$
such that $\alpha\equiv B$ one has that $\alpha\not\in\textsf{n}(B)$.

######  Theorem 78 (Mendler).

If $\mathcal{C}$ verifies the positivity condition, then System
F$\langle\mathcal{C}\rangle$ is strongly normalizing.

###### Proof.

See [16, Theorem 13]. ∎

Abbreviations. We define the following standard abbreviations for types:

$\begin{array}[]{rcl}\mathbf{1}&\,\mathrel{\overset{\mathrm{def}}{=}}&\forall\alpha.(\alpha\to\alpha)\\\
\mathbf{0}&\,\mathrel{\overset{\mathrm{def}}{=}}&\forall\alpha.\alpha\\\ \neg
A&\,\mathrel{\overset{\mathrm{def}}{=}}&A\to\mathbf{0}\\\ A\times
B&\,\mathrel{\overset{\mathrm{def}}{=}}&\forall\alpha.((A\to
B\to\alpha)\to\alpha)\\\
A+B&\,\mathrel{\overset{\mathrm{def}}{=}}&\forall\alpha.((A\to\alpha)\to(B\to\alpha)\to\alpha)\\\
\end{array}$

And the following terms. We omit the typing contexts for succintness:

${\small\begin{array}[]{rcllll}\star&\,\mathrel{\overset{\mathrm{def}}{=}}&\lambda\alpha.\,\lambda
x^{\alpha}.\,x\\\ &:&\mathbf{1}\\\ \\\
\mathcal{E}_{A}(t)&\,\mathrel{\overset{\mathrm{def}}{=}}&t\,A\\\ &:&A\\\
&&\text{if $t:\mathbf{0}$}\\\ \\\ \langle
t,s\rangle&\,\mathrel{\overset{\mathrm{def}}{=}}&\lambda\alpha.\,\lambda
f^{A\to B\to\alpha}.\,f\,t\,s\\\ &:&A\times B\\\ &&\text{if $t:A$ and
$s:B$}\\\ \\\
\pi_{i}(t)&\,\mathrel{\overset{\mathrm{def}}{=}}&t\,A_{i}\,(\lambda
x_{1}^{A_{1}}.\,\lambda x_{2}^{A_{2}}.\,x_{i})\\\ &:&A_{i}\\\ &&\text{if
$t:A_{1}\times A_{2}$}\\\ \\\
\mathsf{in}_{i}(t)&\,\mathrel{\overset{\mathrm{def}}{=}}&\lambda\alpha.\,\lambda
f_{1}^{A_{1}\to\alpha}.\,\lambda f_{2}^{A_{2}\to\alpha}.\,f_{i}\,t\\\
&:&A_{1}+A_{2}\\\ &&\text{if $t:A_{i}$ and $i\in\\{1,2\\}$}\\\ \\\ \delta
t\,[_{x:A_{1}}.s_{1}][_{x:A_{2}}.s_{2}]&\,\mathrel{\overset{\mathrm{def}}{=}}&t\,B\,(\lambda
x^{A_{1}}.\,s_{1})\,(\lambda x^{A_{2}}.\,s_{2})\\\ &:&B\\\ &&\text{if
$t:A_{1}+A_{2}$ and $s_{i}:B$}\\\ &&\text{for each
$i\in\\{1,2\\}$}\end{array}}$