Universidad de Buenos Aires, Argentina and Univeridad Nacional de Quilmes
(CONICET<EMAIL_ADDRESS>de Buenos Aires,
<EMAIL_ADDRESS>Pablo Barenbaum and Teodoro Freund

###### Acknowledgements.

This work was partially supported by project grant PUNQ 2247/22. <ccs2012>
<concept> <concept_id>10003752.10003790.10003792</concept_id>
<concept_desc>Theory of computation Proof theory</concept_desc>
<concept_significance>500</concept_significance> </concept> <concept>
<concept_id>10003752.10003790.10011740</concept_id> <concept_desc>Theory of
computation Type theory</concept_desc>
<concept_significance>500</concept_significance> </concept> </ccs2012>
[500]Theory of computation Proof theory [500]Theory of computation Type theory

# Proofs and Refutations for Intuitionistic and Second-Order Logic (Extended
Version)

Pablo Barenbaum  Teodoro Freund

###### Abstract

The $\lambda^{\textup{PRK}}$-calculus is a typed $\lambda$-calculus that
exploits the duality between the notions of proof and refutation to provide a
computational interpretation for classical propositional logic. In this work,
we extend $\lambda^{\textup{PRK}}$ to encompass classical second-order logic,
by incorporating parametric polymorphism and existential types. The system is
shown to enjoy good computational properties, such as type preservation,
confluence, and strong normalization, which is established by means of a
reducibility argument. We identify a syntactic restriction on proofs that
characterizes exactly the intuitionistic fragment of second-order
$\lambda^{\textup{PRK}}$, and we study canonicity results.

###### keywords:

lambda-calculus, propositions-as-types, classical logic, proof normalization

###### category:

##  1 Introduction

Constructivism in logic is closely related with the notion of algorithm in
computer science. The reason is that a constructive proof of existence of a
mathematical object fulfilling certain properties should provide an effective
construction of such an object. For example, a constructive proof of $\forall
x\in\mathbb{N}.\,\exists y\in\mathbb{N}.\,P(x,y)$ may be understood as an
algorithm that takes as input a natural number $x$ and produces as output a
natural number $y$ that verifies $P(x,y)$. The close relationship that exists
between proofs and computer programs, and between logical propositions and
program specifications (or types), can be taken to its maximum consequences in
the form of the propositions-as-types correspondence.

This correspondence has given rise to a broad and active area of research,
guided by the principle that each proof-theoretical notion has a computational
counterpart and vice-versa. The interest is that this correspondence allows
logic and computer science to feed back on each other. Indeed, besides minimal
propositional logic, it has been extended to such settings as first-order
logic [14, 29, 7], second-order logic [20, 41], linear logic [21], modal logic
[5, 13] and classical logic [22, 9, 3, 36].

The question of what kind of computational system would constitute a
reasonable counterpart for classical logic, from the point of view of the
propositions-as-types correspondence, is far from being definitely settled.
This work is part of the quest for a satisfactory answer to this problem.

#### The proofs and refutations calculus ($\lambda^{\textup{PRK}}$)

Until the late 1980s, it was widely thought that it was not possible to extend
the propositions-as-types correspondence to encompass classical logic. This
view changed when Griffin [22] remarked that the classical principle of double
negation elimination ($\neg\neg A\to A$) can be understood as the typing rule
for a control operator $\mathcal{C}$, closely related to Felleisen’s
$\mathcal{C}$ operator [18] and to Scheme’s call/cc. Since then, many other
calculi for classical logic have been proposed. Significant examples are
Parigot’s $\lambda\mu$ [36], Barbanera and Berardi’s symmetric
$\lambda$-calculus [3], and Curien and Herbelin’s
$\bar{\lambda}\mu\tilde{\mu}$ calculus [9].

The starting point of this paper is the logical system PRK, introduced
recently by the authors [4] and extending Nelson’s constructive negation [33].
In PRK, propositions become classified along two dimensions: their sign, which
may be positive or negative, and their strength, which may be strong or weak.
This results into four possible modes to state

$\begin{array}[]{l|ll}&\text{Positive}&\text{Negative}\\\
\hline\cr\text{Strong}&A{}^{+}&A{}^{-}\\\
\text{Weak}&A{}^{\oplus}&A{}^{\ominus}\vspace{-0.2cm}\end{array}$

a proposition. Positive ($A{}^{+}/A{}^{\oplus}$) and negative
($A{}^{-}/A{}^{\ominus}$) propositions correspond to affirmations and denials.
Strong ($A{}^{+}/A{}^{-}$) and weak ($A{}^{\oplus}/A{}^{\ominus}$)
propositions impose restrictions on the shape of canonical proofs: a canonical
proof of a strong affirmation ($A{}^{+}$) must always be constructed with an
introduction rule for the corresponding logical connective, whereas a
canonical proof of a weak affirmation ($A{}^{\oplus}$) must always proceed by
reductio ad absurdum, by assuming the weak denial $A{}^{\ominus}$ and proving
the strong affirmation $A{}^{+}$.

We summarize some important characteristics of PRK. First, PRK is a refinement
of classical logic: $A_{1},\ldots,A_{n}\vdash B$ holds in classical
propositional logic if and only if
$A{}^{\oplus}_{1},\ldots,A{}^{\oplus}_{n}\vdash B{}^{\oplus}$ holds in PRK. In
fact PRK is “finer” than classical logic: for example, the law of excluded
middle holds weakly, i.e. $(A\lor\neg A){}^{\oplus}$ is valid in PRK, whereas
it does not hold strongly, i.e. $(A\lor\neg A){}^{+}$ is not valid (in
general) in PRK. Second, the $\lambda^{\textup{PRK}}$-calculus, which results
from assigning proof terms to PRK proofs and endowing it with rewrite rules,
turns out to be confluent and strongly normalizing, besides enjoying subject
reduction. Third, as a result, PRK enjoys canonicity: a proof of a sequent
$\vdash P$ without assumptions can always be normalized to a canonical proof,
headed by an introduction rule.

#### Contributions and structure of this paper

The PRK logical system of [4] only treats three propositional connectives:
conjunction, disjunction, and negation.

  * •

In Section 2, we extend the $\lambda^{\textup{PRK}}$ calculus to propositional
second-order logic. We incorporate second-order universal and existential
quantification, as well as two propositional connectives, implication and co-
implication. The system is shown to refine classical second-order logic, and
to enjoy good computational properties: subject reduction and confluence. This
extension increases the expressivity of the system, allowing to encode
inductive datatypes such as natural numbers, lists, and trees.

  * •

In Section 3, we study Böhm–Berarducci encodings, that is, we study how the
logical connectives of second-order $\lambda^{\textup{PRK}}$ may be encoded in
terms of universal quantification and implication only
($\\{\forall,\rightarrow\\}$). The encoding turns out to be only partially
satisfactory: it simulates proof normalization for an introduction rule
followed by an elimination rule in the positive case but, unfortunately, not
in the negative case.

  * •

In Section 4 we prove strong normalization for the second-order
$\lambda^{\textup{PRK}}$-calculus. This is the most technically challenging
part of the work. In [4], normalization of the propositional fragment of
$\lambda^{\textup{PRK}}$ is attained by means of a translation to System F
with non-strictly positive recursion. This technique does not carry over to
the second-order case. To prove strong normalization, we use a variant of
Girard’s technique of reducibility candidates and, in particular, we resort to
a non-trivial adaptation of Mendler’s proof of strong normalization for System
F with non-strictly positive recursion [30].

  * •

In Section 5, we define a subsystem of second-order $\lambda^{\textup{PRK}}$,
called $\lambda^{\textup{PRJ}}$, by imposing a syntactic restriction on terms.
We show that $\lambda^{\textup{PRJ}}$ refines second-order intuitionistic
logic, in the sense that $\lambda^{\textup{PRJ}}$ is a conservative extension
of second-order intuitionistic logic and, conversely, second-order
intuitionistic logic can be embedded in $\lambda^{\textup{PRJ}}$.

  * •

In Section 6 we formulate canonicity results for $\lambda^{\textup{PRK}}$. In
particular, we strengthen the canonicity results of [4] to show that an
explicit witness can be extracted from a proof of $P$.

  * •

Finally, in Section 7 we conclude and we discuss some related and future work.

##  2 Second-Order Proofs and Refutations

In this section we define a second-order extension of
$\lambda^{\textup{PRK}}$, including its syntax, typing rules, and rewriting
rules. We show that the system enjoys subject reduction, it is confluent, and
it refines classical second-order logic (Thm. 2.3).

#### Syntax of types

We assume given a denumerable set of type variables
$\alpha,\beta,\gamma,\ldots$. The sets of pure types ($A,B,\ldots$) and types
($P,Q,\ldots$) are given by:

$A::=\alpha\mid A\land A\mid A\lor A\mid A\rightarrow A\mid A\ltimes A\mid\neg
A\mid\forall\alpha.\,A\mid\exists\alpha.\,A\hskip 14.22636pt\hskip
14.22636ptP::=A{}^{+}\mid A{}^{-}\mid A{}^{\oplus}\mid A{}^{\ominus}$

where $A\ltimes B$ represents co-implication, the dual connective to
implication, to be understood (roughly) as $\neg A\land B$. The four modes
represent strong affirmation ($A{}^{+}$), strong denial ($A{}^{-}$), weak
affirmation ($A{}^{\oplus}$), and weak denial ($A{}^{\ominus}$). Note that
modes (${}^{+},{}^{-},{}^{\oplus},{}^{\ominus}$) can only decorate the root of
a type, i.e. they cannot be nested.

Sometimes one may be interested in fragments of the system. For instance, the
$\lambda^{\textup{PRK}}$-calculus of [4] corresponds to the
$\\{\land,\lor,\neg\\}$ fragment. In this paper we are usually interested in
the full $\\{\land,\lor,\rightarrow,\ltimes,\neg,\forall,\exists\\}$ fragment.
As long as there is little danger of confusion we still speak of
$\lambda^{\textup{PRK}}$ without further qualifications.

#### Syntax of terms

Terms of $\lambda^{\textup{PRK}}$ are given by the following grammar. The
letter $i$ ranges over $\\{1,2\\}$. Some terms are decorated with either “+”
or “-”. In the grammar we write “±” to stand for either “+” or “-”.

$\begin{array}[]{rllllll}t,s,\ldots::=&x^{P}&\text{variable}&\mid&t\mathrel{{\RHD\\!\\!\\!\LHD_{P}}}s&\text{absurdity}\\\
\mid&\mathsf{\textup{\Circle}}^{\pm}_{(x:P)}.\,t&\text{${}^{\oplus}/{}^{\ominus}$
introduction}&\mid&t\bullet\\!\\!^{\pm}\,s&\text{${}^{\oplus}/{}^{\ominus}$
elimination}\\\ \mid&\langle t,s\rangle^{\pm}&\text{$\land{}^{+}$/$\lor{}^{-}$
introduction}&\mid&\pi_{i}^{\pm}(t)&\text{$\land{}^{+}$/$\lor{}^{-}$
elimination}\\\ \mid&\mathsf{in}_{i}^{\pm}(t)&\text{$\lor{}^{+}$/$\land{}^{-}$
introduction}&\mid&\delta^{\pm}t\,[_{x:P}.s][_{y:Q}.u]&\text{$\lor{}^{+}$/$\land{}^{-}$
elimination}\\\
\mid&\lambda^{\pm}_{(x:P)}.{t}&\text{$\rightarrow{}^{+}$/$\ltimes{}^{-}$
introduction}&\mid&t@^{\pm}s&\text{$\rightarrow{}^{+}$/$\ltimes{}^{-}$
elimination}\\\
\mid&(t\,\bm{;}\\!^{\pm}s)&\text{$\ltimes{}^{+}$/$\rightarrow{}^{-}$
introduction}&\mid&\varrho^{\pm}{t}[_{x:P;y:Q}.{s}]&\text{$\ltimes{}^{+}$/$\rightarrow{}^{-}$
elimination}\\\ \mid&\mathsf{N}^{\pm}t&\text{$\neg{}^{+}$/$\neg{}^{-}$
introduction}&\mid&\mathsf{M}^{\pm}t&\text{$\neg{}^{+}$/$\neg{}^{-}$
elimination}\\\
\mid&\lambda^{\pm}_{\alpha}.\,t&\text{$\forall{}^{+}$/$\exists{}^{-}$
introduction}&\mid&t@^{\pm}A&\text{$\forall{}^{+}$/$\exists{}^{-}$
elimination}\\\ \mid&\langle
A,t\rangle^{\pm}&\text{$\exists{}^{+}$/$\forall{}^{-}$
introduction}&\mid&\nabla^{\pm}\,t[_{(\alpha,x:P)}.s]&\text{$\exists{}^{+}$/$\forall{}^{-}$
elimination}\end{array}$

The notions of free and bound occurrences of variables are defined as
expected, with the typographical convention that subscripted variable
occurrences are binding. Terms are considered up to $\alpha$-renaming of bound
variables. We write $\mathsf{fv}(t)$ for the set of free variables of $t$ and
$\mathsf{ftv}(t)$ for the set of type variables occurring free in $t$. By
$t\\{x:=s\\}$ we mean the capture-avoiding substitution of the free
occurrences of $x$ in $t$ by $s$.

Variables are formally annotated with their type, which we usually omit.
Sometimes we also omit the types of bound variables if they are clear from the
context, as well as the name of unused bound variables, writing
“$\underline{\,\,\,}$” instead. For example, if $x\not\in\mathsf{fv}(t)$ we
may write $\mathsf{\textup{\Circle}}{}^{+}_{\underline{\,\,\,}}.\,t$ rather
than $\mathsf{\textup{\Circle}}{}^{+}_{(x:A{}^{-})}.\,t$. Application-like
operators are assumed to be left-associative; for example,
$t@{}^{+}s\bullet\\!\\!{}^{+}\,u@{}^{+}A$ stands for
$((t@{}^{+}s)\bullet\\!\\!{}^{+}\,u)@{}^{+}A$. In a term of the form
$\mathsf{\textup{\Circle}}^{\pm}_{(x:P)}.\,t$, the variable $x$ is called the
counterfactual, and more specifically a negative counterfactual in a term of
the form $\mathsf{\textup{\Circle}}{}^{+}_{(x:A{}^{\ominus})}.\,t$. In a term
of the form $t\bullet\\!\\!^{\pm}\,s$, we call $t$ the subject and $s$ the
argument. We write $\mathtt{C}$ for arbitrary term contexts, i.e. terms with a
single free occurrence of a distinguished variable $\Box$ called a hole. We
write $\mathtt{C}\langle t\rangle$ for the variable-capturing substitution of
the hole of $\mathtt{C}$ by $t$.

#### The $\lambda^{\textup{PRK}}$ type system

A typing context, ranged over by $\Gamma,\Delta,\ldots$, is a finite
assignment of variables to types, written as $x_{1}:P_{1},\ldots,x_{n}:P_{n}$.
We write $\mathsf{dom}(\Gamma)$ for the domain of $\Gamma$, i.e. the finite
set $\\{x_{1},\ldots,x_{n}\\}$. Typing judgments in $\lambda^{\textup{PRK}}$
are of the form $\Gamma\vdash t:P$, meaning that $t$ has type $P$ under the
context $\Gamma$. Derivable judgments are given inductively by the typing
rules below.

We write $\Gamma\vdash_{\textup{PRK}}t:P$ if the typing judgment $\Gamma\vdash
t:P$ is derivable in $\lambda^{\textup{PRK}}$. When we wish to emphasize the
logical point of view, we may write sequents as $P_{1},\ldots,P_{n}\vdash Q$,
and we may write $P_{1},\ldots,P_{n}\vdash_{\textup{PRK}}Q$ to mean that there
exists a term $t$ such that
$x_{1}:P_{1},\ldots,x_{n}:P_{n}\vdash_{\textup{PRK}}t:Q$.

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 27.27437pt\hbox{$\displaystyle\penalty
1\vphantom{{}^{@}}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=58.46875pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{Ax}}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma,x:P\vdash
x:P$}}}}\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.22636pt\Gamma\vdash s:A{}^{-}$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=88.04518pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{Abs}}}}$}}}\hbox{\kern
18.24376pt\hbox{$\displaystyle\Gamma\vdash
t\mathrel{{\RHD\\!\\!\\!\LHD_{P}}}s:P$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\Gamma,x:A{}^{\ominus}\vdash t:A{}^{+}$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=62.35883pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{I${}_{\circ}^{+}$}}}}$}}}\hbox{\kern
4.44688pt\hbox{$\displaystyle\Gamma\vdash\mathsf{\textup{\Circle}}{}^{+}_{x:A{}^{\ominus}}.\,t:A{}^{\oplus}$}}}}\end{array}$
$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma,x:A{}^{\oplus}\vdash
t:A{}^{-}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=59.1188pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{I${}_{\circ}^{-}$}}}}$}}}\hbox{\kern
2.82687pt\hbox{$\displaystyle\Gamma\vdash\mathsf{\textup{\Circle}}{}^{+}_{x:A{}^{\oplus}}.\,t:A{}^{\ominus}$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\Gamma\vdash t:A{}^{\oplus}\hskip 8.5359pt\Gamma\vdash
s:A{}^{\ominus}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=84.59474pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{E${}_{\circ}^{+}$}}}}$}}}\hbox{\kern
15.95546pt\hbox{$\displaystyle\Gamma\vdash
t\bullet\\!\\!{}^{+}\,s: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{}^{\ominus}\hskip 8.5359pt\Gamma\vdash
s:A{}^{\oplus}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=84.59474pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{E${}_{\circ}^{-}$}}}}$}}}\hbox{\kern
18.19548pt\hbox{$\displaystyle\Gamma\vdash
t\bullet\\!\\!{}^{-}\,s: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{}^{\oplus}\hskip
14.22636pt\Gamma\vdash s:B{}^{\oplus}$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=90.81332pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{I${}_{\land}^{+}$}}}}$}}}\hbox{\kern
7.03679pt\hbox{$\displaystyle\Gamma\vdash\langle t,s\rangle{}^{+}:(A\land
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{}^{\ominus}\hskip 14.22636pt\Gamma\vdash s:B{}^{\ominus}$}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=90.81332pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{I${}_{\lor}^{-}$}}}}$}}}\hbox{\kern
9.27681pt\hbox{$\displaystyle\Gamma\vdash\langle t,s\rangle{}^{-}:(A\lor
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_{1}\land
A_{2}){}^{+}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=64.33508pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{E${}^{+}_{\land{i}}$}}}}$}}}\hbox{\kern
5.59357pt\hbox{$\displaystyle\Gamma\vdash\pi_{i}^{+}(t):A_{i}{}^{\oplus}$}}}}\end{array}$
$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash t:(A_{1}\lor
A_{2}){}^{-}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=62.09506pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{E${}^{-}_{\lor{i}}$}}}}$}}}\hbox{\kern
4.47356pt\hbox{$\displaystyle\Gamma\vdash\pi_{i}^{-}(t):A_{i}{}^{\ominus}$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\Gamma\vdash t:A_{i}{}^{\oplus}\hskip 14.22636pti\in\\{1,2\\}$}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=88.10844pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{I${}^{+}_{\lor{i}}$}}}}$}}}\hbox{\kern
4.55849pt\hbox{$\displaystyle\Gamma\vdash\mathsf{in}_{i}\\!\\!{}^{+}(t):(A_{1}\lor
A_{2}){}^{+}$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\Gamma\vdash t:A_{i}{}^{\ominus}\hskip 14.22636pti\in\\{1,2\\}$}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=88.10844pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{I${}^{-}_{\land{i}}$}}}}$}}}\hbox{\kern
6.79851pt\hbox{$\displaystyle\Gamma\vdash\mathsf{in}_{i}\\!\\!{}^{-}(t):(A_{1}\land
A_{2}){}^{-}$}}}}\end{array}$ $\begin{array}[]{c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\Gamma\vdash t:(A\lor B){}^{+}\hskip 14.22636pt\Gamma,x:A{}^{\oplus}\vdash
s:P\hskip 14.22636pt\Gamma,y:B{}^{\oplus}\vdash u:P$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=208.70042pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{E${}_{\lor}^{+}$}}}}$}}}\hbox{\kern
58.66914pt\hbox{$\displaystyle\Gamma\vdash\delta{}^{+}t\,[_{x:A{}^{\oplus}}.s][_{y:B{}^{\oplus}}.u]:P$}}}}\end{array}$
$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash t:(A\land B){}^{-}\hskip
14.22636pt\Gamma,x:A{}^{\ominus}\vdash s:P\hskip
14.22636pt\Gamma,y:B{}^{\ominus}\vdash u:P$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=206.4604pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{E${}_{\land}^{-}$}}}}$}}}\hbox{\kern
58.66914pt\hbox{$\displaystyle\Gamma\vdash\delta{}^{-}t\,[_{x:A{}^{\ominus}}.s][_{y:B{}^{\ominus}}.u]:P$}}}}\end{array}$

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 3.05315pt\hbox{$\displaystyle\penalty
1\Gamma,x:A{}^{\oplus}\vdash t:B{}^{\oplus}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=67.99324pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{I${}_{\rightarrow}^{+}$}}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash\lambda{}^{+}_{x:A{}^{\oplus}}.{t}:(A\rightarrow
B){}^{+}$}}}}\end{array}\\!\\!\begin{array}[]{c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
2.81313pt\hbox{$\displaystyle\penalty 1\Gamma,x:A{}^{\ominus}\vdash
t:B{}^{\ominus}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=67.5132pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{I${}_{\ltimes}^{-}$}}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash\lambda{}^{-}_{x:A{}^{\ominus}}.{t}:(A\ltimes
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\rightarrow B){}^{+}\hskip 8.5359pt\\!\Gamma\vdash
s:A{}^{\oplus}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=106.8729pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{E${}_{\rightarrow}^{+}$}}}}$}}}\hbox{\kern
26.83047pt\hbox{$\displaystyle\Gamma\vdash
t@{}^{+}s:B{}^{\oplus}$}}}}\end{array}$ $\begin{array}[]{c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\Gamma\vdash t:(A\ltimes B){}^{-}\hskip 8.5359pt\\!\Gamma\vdash
s:A{}^{\ominus}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=106.13287pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{E${}_{\ltimes}^{-}$}}}}$}}}\hbox{\kern
27.58047pt\hbox{$\displaystyle\Gamma\vdash
t@{}^{-}s:B{}^{\ominus}$}}}}\end{array}\\!\\!\begin{array}[]{c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\Gamma\vdash t:A{}^{\ominus}\hskip 14.22636pt\\!\Gamma\vdash
s:B{}^{\oplus}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=89.31332pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{I${}_{\ltimes}^{+}$}}}}$}}}\hbox{\kern
4.42569pt\hbox{$\displaystyle\Gamma\vdash(t\,\bm{;}\\!{}^{+}s):(A\ltimes
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{}^{\oplus}\hskip 8.5359pt\\!\Gamma\vdash
s:B{}^{\ominus}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=83.62286pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{I${}_{\rightarrow}^{-}$}}}}$}}}\hbox{\kern
4.57048pt\hbox{$\displaystyle\Gamma\vdash(t\,\bm{;}\\!{}^{-}s):(A\rightarrow
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\ltimes B){}^{+}\hskip
8.5359pt\\!\\!\Gamma,x:A{}^{\ominus},y:B{}^{\oplus}\vdash s:P$}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=154.47836pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{E${}_{\ltimes}^{+}$}}}}$}}}\hbox{\kern
39.10762pt\hbox{$\displaystyle\Gamma\vdash\varrho^{+}{t}[_{x:A{}^{\ominus};y:B{}^{\oplus}}.{s}]:P$}}}}\end{array}\\!\\!\\!\begin{array}[]{c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\Gamma\vdash t:(A\rightarrow B){}^{-}\hskip
8.5359pt\\!\\!\Gamma,x:A{}^{\oplus},y:B{}^{\ominus}\vdash s:P$}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=150.73834pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{E${}_{\rightarrow}^{-}$}}}}$}}}\hbox{\kern
38.35762pt\hbox{$\displaystyle\Gamma\vdash\varrho^{-}{t}[_{x:A{}^{\oplus};y:B{}^{\ominus}}.{s}]:P$}}}}\end{array}$

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 11.33502pt\hbox{$\displaystyle\penalty 1\Gamma\vdash
t:A{}^{\ominus}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=60.21509pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{I${}_{\lnot}^{+}$}}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash\mathsf{N}{}^{+}t:(\neg
A){}^{+}$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{\kern 9.095pt\hbox{$\displaystyle\penalty
1\Gamma\vdash t:A{}^{\oplus}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.225pt,depth=0.225pt,width=55.73505pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{I${}_{\lnot}^{-}$}}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash\mathsf{N}{}^{-}t:(\neg
A){}^{-}$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash t:(\neg
A){}^{+}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=49.54506pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{E${}_{\lnot}^{+}$}}}}$}}}\hbox{\kern
1.165pt\hbox{$\displaystyle\Gamma\vdash\mathsf{M}{}^{+}t:A{}^{\ominus}$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\Gamma\vdash t:(\neg A){}^{-}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.225pt,depth=0.225pt,width=49.80504pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{E${}_{\lnot}^{-}$}}}}$}}}\hbox{\kern
2.415pt\hbox{$\displaystyle\Gamma\vdash\mathsf{M}{}^{-}t:A{}^{\oplus}$}}}}\end{array}$

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash t:A{}^{\oplus}\hskip
14.22636pt\alpha\notin\mathsf{ftv}(\Gamma)$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=90.40376pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{I${}_{\forall}^{+}$}}}}$}}}\hbox{\kern
6.71568pt\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{$\displaystyle\penalty
1\Gamma\vdash t:A{}^{\ominus}\hskip
14.22636pt\alpha\notin\mathsf{ftv}(\Gamma)$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=87.90376pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{I${}_{\exists}^{-}$}}}}$}}}\hbox{\kern
7.7057pt\hbox{$\displaystyle\Gamma\vdash\lambda{}^{-}_{\alpha}.\,t:(\exists\alpha.\,A){}^{-}$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
14.96005pt\hbox{$\displaystyle\penalty 1\Gamma\vdash
t:(\forall\alpha.\,B){}^{+}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.225pt,depth=0.225pt,width=92.7506pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{E${}_{\forall}^{+}$}}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash
t@{}^{+}A:B{}^{\oplus}\\{\alpha:=A\\}$}}}}\end{array}$
$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 14.96005pt\hbox{$\displaystyle\penalty 1\Gamma\vdash
t:(\exists\alpha.\,B){}^{-}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.225pt,depth=0.225pt,width=90.51057pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{E${}_{\exists}^{-}$}}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash
t@{}^{-}A:B{}^{\ominus}\\{\alpha:=A\\}$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
2.59889pt\hbox{$\displaystyle\penalty 1\Gamma\vdash
t:B{}^{\oplus}\\{\alpha:=A\\}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.225pt,depth=0.225pt,width=80.27832pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{I${}_{\exists}^{+}$}}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash\langle
A,t\rangle{}^{+}:(\exists\alpha.\,B){}^{+}$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
0.35887pt\hbox{$\displaystyle\penalty 1\Gamma\vdash
t:B{}^{\ominus}\\{\alpha:=A\\}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.225pt,depth=0.225pt,width=75.79828pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{I${}_{\forall}^{-}$}}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash\langle
A,t\rangle{}^{-}:(\forall\alpha.\,B){}^{-}$}}}}\end{array}$
$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash
t:(\exists\alpha.\,A){}^{+}\hskip 14.22636pt\Gamma,x:A{}^{\oplus}\vdash
s:P\hskip 14.22636pt\alpha\notin\mathsf{ftv}(\Gamma,P)$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=198.10123pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{E${}_{\exists}^{+}$}}}}$}}}\hbox{\kern
59.60736pt\hbox{$\displaystyle\Gamma\vdash\nabla{}^{+}\,t[_{(\alpha,x:A{}^{\oplus})}.s]:P$}}}}\end{array}$
$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash
t:(\forall\alpha.\,A){}^{-}\hskip 14.22636pt\Gamma,x:A{}^{\ominus}\vdash
s:P\hskip 14.22636pt\alpha\notin\mathsf{ftv}(\Gamma,P)$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=195.8612pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{E${}_{\forall}^{-}$}}}}$}}}\hbox{\kern
59.60736pt\hbox{$\displaystyle\Gamma\vdash\nabla{}^{-}\,t[_{(\alpha,x:A{}^{\ominus})}.s]:P$}}}}\end{array}$

The typing rules may be informally explained as follows. Ax is the standard
axiom. The absurdity rule (Abs) allows to derive any conclusion from a strong
proof and a strong refutation of $A$. Introduction and elimination rules for
weak affirmation and denial (I${}_{\circ}^{\pm}$, E${}_{\circ}^{\pm}$) follow
the principle that a weak affirmation $A{}^{\oplus}$ behaves like an
implication “$A{}^{\ominus}\to A{}^{+}$”. Indeed, I${}_{\circ}^{+}$ and
E${}_{\circ}^{+}$ have the same structure as the introduction and the
elimination rule for an implication “$A{}^{\ominus}\to A{}^{+}$”, where
$\mathsf{\textup{\Circle}}{}^{+}_{x}.\,t$ and $t\bullet\\!\\!{}^{+}\,s$ are
akin to $\lambda$-abstraction and application. The intuition behind this is
that $A{}^{\oplus}$ is the type of weak proofs of a proposition $A$, where a
weak proof proceeds by reductio ad absurdum, assuming a weak refutation
($A{}^{\ominus}$), and providing a strong proof ($A{}^{+}$). Dually, a weak
denial $A{}^{\ominus}$ behaves like “$A{}^{\oplus}\to A{}^{-}$”.

The remaining rules are introduction and elimination rules for positive and
negative strong connectives. These rules come in dual pairs: for each rule for
a connective with positive sign there is a symmetric rule for the dual
connective with negative sign. For example, the introduction rule for positive
conjunction (I${}_{\land}^{+}$) states that to strongly prove $A\land B$ it
suffices to weakly prove $A$ and weakly prove $B$. Dually, the introduction
rule for negative disjunction (I${}_{\lor}^{-}$) states that to strongly
refute $A\lor B$ it suffices to weakly refute $A$ and weakly refute $B$.

The introduction and elimination rules for most logical connectives ($\land$,
$\lor$, $\rightarrow$, $\ltimes$, $\forall$, $\exists$) are mechanically
derived from the standard natural deduction rules following this methodology,
taking in account that the dual pairs of connectives are $(\land,\lor)$,
$(\rightarrow,\ltimes)$, and $(\forall,\exists)$. In general, introduction
rules have weak premises and strong conclusions, whereas elimination rules
have strong premises and weak conclusions.

The typing rules for conjunction
($\textup{{I${}_{\land}^{+}$}},\textup{{E${}^{+}_{\land{i}}$}},\textup{{I${}^{-}_{\land{i}}$}},\textup{{E${}_{\land}^{-}$}}$),
disjunction
($\textup{{I${}^{+}_{\lor{i}}$}},\textup{{E${}_{\lor}^{+}$}},\textup{{I${}_{\lor}^{-}$}},\textup{{E${}^{-}_{\lor{i}}$}}$),
positive implication
($\textup{{I${}_{\rightarrow}^{+}$}},\textup{{E${}_{\rightarrow}^{+}$}}$),
negative co-implication
($\textup{{I${}_{\ltimes}^{-}$}},\textup{{E${}_{\ltimes}^{-}$}}$), universal
($\textup{{I${}_{\forall}^{+}$}},\textup{{E${}_{\forall}^{+}$}},\textup{{I${}_{\forall}^{-}$}},\textup{{E${}_{\forall}^{-}$}}$)
and existential quantification
($\textup{{I${}_{\exists}^{+}$}},\textup{{E${}_{\exists}^{+}$}},\textup{{I${}_{\exists}^{-}$}},\textup{{E${}_{\exists}^{-}$}}$)
are typical, so for instance $\langle t,s\rangle^{\pm}$ forms a pair,
$\pi_{i}^{\pm}(t)$ is the $i$-th projection, $\mathsf{in}_{i}^{\pm}(t)$ is the
$i$-th injection into a disjoint union type, $\delta^{\pm}t\,[_{x}.s][_{y}.u]$
is a pattern matching construct, and so on. The rules differ from usual typed
$\lambda$-calculi only in the signs and strengths that decorate premises and
conclusions.

The typing rules for positive co-implication
($\textup{{I${}_{\ltimes}^{+}$}},\textup{{E${}_{\ltimes}^{+}$}}$), sometimes
called subtraction [8], and negative implication
($\textup{{I${}_{\rightarrow}^{-}$}},\textup{{E${}_{\rightarrow}^{-}$}}$)
follow the rough interpretation of $A\ltimes B$ as $\neg A\land B$, so a
strong proof of a co-implication $A\ltimes B$ is given by a pair
$(t\,\bm{;}\\!{}^{+}s)$ comprising a weak refutation of $A$ and a weak proof
of $B$. Dually, a strong refutation of $A\rightarrow B$ is given by a pair
$(t\,\bm{;}\\!{}^{-}s)$ comprising a weak proof of $A$ and a weak refutation
of $B$. The eliminators $\varrho^{\pm}{t}[_{x;y}.{s}]$ are presented as
generalized elimination rules, in multiplicative style.

The typing rules for negation
($\textup{{I${}_{\lnot}^{+}$}},\textup{{E${}_{\lnot}^{+}$}},\textup{{I${}_{\lnot}^{-}$}},\textup{{E${}_{\lnot}^{-}$}}$)
express that to strongly prove $\neg A$ is the same as to weakly refute $A$,
and dually for strong refutations of $\neg A$.

######  Example 2.1.

Let
$\top\,\mathrel{\overset{\mathrm{def}}{=}}\,\forall\alpha.\,(\alpha\rightarrow\alpha)$
and $\bot\,\mathrel{\overset{\mathrm{def}}{=}}\,\forall\alpha.\,\alpha$.
Recall from [4] that the weak non-contradiction principle
$\Gamma\vdash(A\land\neg A){}^{\ominus}$ holds in $\lambda^{\textup{PRK}}$.
Then $\vdash\top{}^{\oplus}$ and $\bot{}^{\oplus}\vdash A{}^{\oplus}$ hold,
where $A$ stands for any pure type:

$\begin{array}[]{c@{\hspace{2cm}}c}{\small\begin{array}[b]{c@{}r}{\small\begin{array}[b]{c@{}r}{\small\begin{array}[b]{c@{}r}{\small\begin{array}[b]{c<EMAIL_ADDRESS>&\,\textup{{Ax}}\\!\vspace{-.2cm}\\\ \cline{1-1}\cr\vspace{-.3cm}\hfil\\\
\top{}^{\ominus},(\alpha\rightarrow\alpha){}^{\ominus},\alpha{}^{\oplus}\vdash\alpha{}^{\oplus}\end{array}\vspace{-.1cm}}\\\
&\,\textup{{I${}_{\rightarrow}^{+}$}}\\!\vspace{-.2cm}\\\
\cline{1-1}\cr\vspace{-.3cm}\hfil\\\
\top{}^{\ominus},(\alpha\rightarrow\alpha){}^{\ominus}\vdash(\alpha\rightarrow\alpha){}^{+}\end{array}\vspace{-.1cm}}\\\
&\,\textup{{I${}_{\circ}^{+}$}}\\!\vspace{-.2cm}\\\
\cline{1-1}\cr\vspace{-.3cm}\hfil\\\
\top{}^{\ominus}\vdash(\alpha\rightarrow\alpha){}^{\oplus}\end{array}\vspace{-.1cm}}\\\
&\,\textup{{I${}_{\forall}^{+}$}}\\!\vspace{-.2cm}\\\
\cline{1-1}\cr\vspace{-.3cm}\hfil\\\
\top{}^{\ominus}\vdash\top{}^{+}\end{array}\vspace{-.1cm}}\\\
&\,\textup{{I${}_{\circ}^{+}$}}\\!\vspace{-.2cm}\\\
\cline{1-1}\cr\vspace{-.3cm}\hfil\\\
\vdash\top{}^{\oplus}\end{array}}\hfil\hskip
56.9055pt&{\small\begin{array}[b]{c<EMAIL_ADDRESS>&\,\textup{{Ax}}\\!\vspace{-.2cm}\\\ \cline{1-1}\cr\vspace{-.3cm}\hfil\\\
\bot{}^{\oplus}\vdash\bot{}^{\oplus}\end{array}}\hskip
14.22636pt{\small\begin{array}[b]{c@{}r}{\small\begin{array}[b]{c@{}r}{\small\begin{array}[b]{c@{}r}\text{(By
weak non-contradiction.)}\vspace{-.1cm}\\\ &\,\\!\vspace{-.2cm}\\\
\cline{1-1}\cr\vspace{-.3cm}\hfil\\\
\bot{}^{\oplus},\bot{}^{\oplus}\vdash(B\land\neg
B){}^{\ominus}\end{array}\vspace{-.1cm}}\\\
&\,\textup{{I${}_{\forall}^{-}$}}\\!\vspace{-.2cm}\\\
\cline{1-1}\cr\vspace{-.3cm}\hfil\\\
\bot{}^{\oplus},\bot{}^{\oplus}\vdash\bot{}^{-}\end{array}\vspace{-.1cm}}\\\
&\,\textup{{I${}_{\circ}^{-}$}}\\!\vspace{-.2cm}\\\
\cline{1-1}\cr\vspace{-.3cm}\hfil\\\
\bot{}^{\oplus}\vdash\bot{}^{\ominus}\end{array}\vspace{-.1cm}}\\\
&\,\textup{{Abs}}^{\prime}\\!\vspace{-.2cm}\\\
\cline{1-1}\cr\vspace{-.3cm}\hfil\\\ \bot{}^{\oplus}\vdash
A{}^{\oplus}\end{array}}\end{array}$

#### The $\lambda^{\textup{PRK}}$-calculus

The opposite type $P{}^{\sim}$ of a given type $P$ is defined by flipping the
sign, i.e.
$(A{}^{\oplus}){}^{\sim}\,\mathrel{\overset{\mathrm{def}}{=}}\,A{}^{\ominus}$;
$(A{}^{\ominus}){}^{\sim}\,\mathrel{\overset{\mathrm{def}}{=}}\,A{}^{\oplus}$;
$(A{}^{+}){}^{\sim}\,\mathrel{\overset{\mathrm{def}}{=}}\,A{}^{-}$; and
$(A{}^{-}){}^{\sim}\,\mathrel{\overset{\mathrm{def}}{=}}\,A{}^{+}$. If
$\Gamma\vdash_{\textup{PRK}}t:P$ and $\Gamma\vdash_{\textup{PRK}}s:P{}^{\sim}$
then a term $t\mathrel{\bowtie_{Q}}s$ may be constructed such that
$\Gamma\vdash_{\textup{PRK}}t\mathrel{\bowtie_{Q}}s:Q$, as follows:

$\begin{array}[]{rl@{\hspace{.5cm}}rl}t\mathrel{\bowtie_{Q}}s\,\mathrel{\overset{\mathrm{def}}{=}}\,t\mathrel{{\RHD\\!\\!\\!\LHD_{Q}}}s&\text{if
$P=A{}^{+}$}\hfil\hskip
14.22636pt&t\mathrel{\bowtie_{Q}}s\,\mathrel{\overset{\mathrm{def}}{=}}\,s\mathrel{{\RHD\\!\\!\\!\LHD_{Q}}}t&\text{if
$P=A{}^{-}$}\\\
t\mathrel{\bowtie_{Q}}s\,\mathrel{\overset{\mathrm{def}}{=}}\,(t\bullet\\!\\!{}^{+}\,s)\mathrel{{\RHD\\!\\!\\!\LHD_{Q}}}(s\bullet\\!\\!{}^{-}\,t)&\text{if
$P=A{}^{\oplus}$}\hfil\hskip
14.22636pt&t\mathrel{\bowtie_{Q}}s\,\mathrel{\overset{\mathrm{def}}{=}}\,(s\bullet\\!\\!{}^{+}\,t)\mathrel{{\RHD\\!\\!\\!\LHD_{Q}}}(t\bullet\\!\\!{}^{-}\,s)&\text{if
$P=A{}^{\ominus}$}\\\ \end{array}$

We endow typable PRK terms with a notion of reduction, defining the
$\lambda^{\textup{PRK}}$-calculus by a binary rewriting relation
$\xrightarrow{}$ on typable PRK terms, given by the rewriting rules below, and
closed by compatibility under arbitrary contexts. Rules are presented
following the convention that, if many occurrences of “$\pm$” appear in the
same expression, they are all supposed to stand for the same sign:

${\small\begin{array}[]{r@{\,}l@{\,}l@{\,\,\,}@{\,\,\,}r@{\,}l@{\,}l}(\mathsf{\textup{\Circle}}^{\pm}_{x}.\,t)\bullet\\!\\!^{\pm}\,s&\xrightarrow{\mathsf{\beta{}^{+}_{\circ}}\,/\,\mathsf{\beta{}^{-}_{\circ}}}&t\\{x:=s\\}\\\
\pi_{i}^{\pm}(\langle
t_{1},t_{2}\rangle^{\pm})&\xrightarrow{\mathsf{\beta{}^{+}_{\land}}\,/\,\mathsf{\beta{}^{-}_{\lor}}}&t_{i}&\delta^{\pm}(\mathsf{in}_{i}^{\pm}(t))\,[_{x}.s_{1}][_{x}.s_{2}]&\xrightarrow{\mathsf{\beta{}^{+}_{\lor}}\,/\,\mathsf{\beta{}^{-}_{\land}}}&s_{i}\\{x:=t\\}\\\
(\lambda^{\pm}_{x}.{t})@^{\pm}s&\xrightarrow{\mathsf{\beta{}^{+}_{\rightarrow}}\,/\,\mathsf{\beta{}^{-}_{\ltimes}}}&t\\{x:=s\\}&\varrho^{\pm}{(t\,\bm{;}\\!^{\pm}s)}[_{x;y}.{u}]&\xrightarrow{\mathsf{\beta{}^{+}_{\ltimes}}\,/\,\mathsf{\beta{}^{-}_{\rightarrow}}}&u\\{x:=t\\}\\{y:=s\\}\\\
\mathsf{M}^{\pm}(\mathsf{N}^{\pm}t)&\xrightarrow{\mathsf{\beta{}^{+}_{\neg}}\,/\,\mathsf{\beta{}^{-}_{\neg}}}&t\\\
(\lambda^{\pm}_{\alpha}.\,t)@^{\pm}A&\xrightarrow{\mathsf{\beta{}^{+}_{\forall}}\,/\,\mathsf{\beta{}^{-}_{\exists}}}&t\\{\alpha:=A\\}&\nabla^{\pm}\,\langle
A,t\rangle^{\pm}[_{(\alpha,x)}.s]&\xrightarrow{\mathsf{\beta{}^{+}_{\exists}}\,/\,\mathsf{\beta{}^{-}_{\forall}}}&s\\{\alpha:=A\\}\\{x:=t\\}\\\
\langle
t_{1},t_{2}\rangle{}^{+}\mathrel{{\RHD\\!\\!\\!\LHD}}\mathsf{in}_{i}\\!\\!{}^{-}(s)&\xrightarrow{\mathsf{{\RHD\\!\\!\\!\LHD_{\land}}}}&t_{i}\mathrel{\bowtie}s&\mathsf{in}_{i}\\!\\!{}^{+}(t)\mathrel{{\RHD\\!\\!\\!\LHD}}\langle
s_{1},s_{2}\rangle{}^{-}&\xrightarrow{\mathsf{{\RHD\\!\\!\\!\LHD_{\lor}}}}&t\mathrel{\bowtie}s_{i}\\\
\lambda{}^{+}_{x}.{t}\mathrel{{\RHD\\!\\!\\!\LHD}}(s\,\bm{;}\\!{}^{-}u)&\xrightarrow{\mathsf{{\RHD\\!\\!\\!\LHD_{\rightarrow}}}}&t\\{x:=s\\}\mathrel{\bowtie}u&(t\,\bm{;}\\!{}^{+}s)\mathrel{{\RHD\\!\\!\\!\LHD}}\lambda{}^{-}_{x}.{u}&\xrightarrow{\mathsf{{\RHD\\!\\!\\!\LHD_{\ltimes}}}}&s\mathrel{\bowtie}u\\{x:=t\\}\\\
(\mathsf{N}{}^{+}t)\mathrel{{\RHD\\!\\!\\!\LHD}}(\mathsf{N}{}^{-}s)&\xrightarrow{\mathsf{{\RHD\\!\\!\\!\LHD_{\neg}}}}&t\mathrel{\bowtie}s\\\
(\lambda{}^{+}_{\alpha}.\,t)\mathrel{{\RHD\\!\\!\\!\LHD}}\langle
A,s\rangle{}^{-}&\xrightarrow{\mathsf{{\RHD\\!\\!\\!\LHD_{\forall}}}}&t\\{\alpha:=A\\}\mathrel{\bowtie}s&\langle
A,t\rangle{}^{+}\mathrel{{\RHD\\!\\!\\!\LHD}}(\lambda{}^{-}_{\alpha}.\,s)&\xrightarrow{\mathsf{{\RHD\\!\\!\\!\LHD_{\exists}}}}&t\mathrel{\bowtie}s\\{\alpha:=A\\}\end{array}}$

The $\lambda^{\textup{PRK}}$-calculus has two kinds of rules: “$\beta$” rules,
akin to proof normalization rules in natural deduction, and
“$\mathrel{{\RHD\\!\\!\\!\LHD}}$” rules, akin to cut elimination rules in
sequent calculus. The
$\mathsf{\beta{}^{+}_{\circ}}\,/\,\mathsf{\beta{}^{-}_{\circ}}$ rules are
exactly like the standard $\beta$-rule of the $\lambda$-calculus, with the
difference that the abstraction
$\mathsf{\textup{\Circle}}{}^{+}_{x:A{}^{\ominus}}.\,t$ is not an introduction
of an implication “$A{}^{\ominus}\to A{}^{+}$” but rather the introduction of
a weak affirmation $A{}^{\oplus}$. The
$\mathsf{\beta{}^{+}_{\rightarrow}}\,/\,\mathsf{\beta{}^{-}_{\ltimes}}$ rules
also describe a similar behavior, where $\lambda{}^{+}_{x:A{}^{\oplus}}.{t}$
is of type $(A\to B){}^{\oplus}$. The remaining $\beta$ rules are
straightforward, encoding projection
($\mathsf{\beta{}^{+}_{\land}}\,/\,\mathsf{\beta{}^{-}_{\lor}}$), pattern
matching ($\mathsf{\beta{}^{+}_{\lor}}\,/\,\mathsf{\beta{}^{-}_{\land}}$),
etcetera.

The $\mathrel{{\RHD\\!\\!\\!\LHD}}$ rules simplify an absurdity
$(t\mathrel{{\RHD\\!\\!\\!\LHD}}s)$ as much as possible, but they are never
able to get rid of the absurdity. Indeed, note that the right-hand side of all
the $\mathrel{{\RHD\\!\\!\\!\LHD}}$ rules include the generalized absurdity
operator ($\mathrel{\bowtie}$), which is in turn defined in terms of the
absurdity operator ($\mathrel{{\RHD\\!\\!\\!\LHD}}$). Recall, for example,
that if $t:A{}^{\oplus}$ and $s:A{}^{\ominus}$ then
$t\mathrel{\bowtie}s=(t\bullet\\!\\!{}^{+}\,s)\mathrel{{\RHD\\!\\!\\!\LHD}}(s\bullet\\!\\!{}^{-}\,t)$.
This means that an instance of the absurdity is a proof which provides no
relevant information. For example, if $P=(B\land C){}^{+}$ then
$\pi_{1}^{+}(t\mathrel{{\RHD\\!\\!\\!\LHD_{P}}}s)$ is a well-formed term of
type $B{}^{\oplus}$; but the argument of the projection is a term
$t\mathrel{{\RHD\\!\\!\\!\LHD_{P}}}s$ which may never become a pair $\langle
p,q\rangle{}^{+}$. This means that the normal form will be a “stuck” term of
the form $\pi_{1}^{+}(t^{\prime}\mathrel{{\RHD\\!\\!\\!\LHD_{P}}}s^{\prime})$.

######  Example 2.2 (Reduction in $\lambda^{\textup{PRK}}$).

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

$\begin{array}[]{ll}&(\lambda{}^{+}_{\alpha}.\,\mathsf{\textup{\Circle}}{}^{+}_{\underline{\,\,\,}:(\alpha\rightarrow\alpha){}^{\ominus}}.\,\lambda{}^{+}_{x:\alpha{}^{\oplus}}.{x})\mathrel{{\RHD\\!\\!\\!\LHD}}\langle
A,\mathsf{\textup{\Circle}}{}^{-}_{\underline{\,\,\,}:(\alpha\rightarrow\alpha){}^{\oplus}}.\,(t\,\bm{;}\\!{}^{-}s)\rangle{}^{-}\\\
\xrightarrow{\mathsf{{\RHD\\!\\!\\!\LHD_{\forall}}}}&(\mathsf{\textup{\Circle}}{}^{+}_{\underline{\,\,\,}:(A\rightarrow
A){}^{\ominus}}.\,\lambda{}^{+}_{x:A{}^{\oplus}}.{x})\mathrel{\bowtie}(\mathsf{\textup{\Circle}}{}^{-}_{\underline{\,\,\,}:(A\rightarrow
A){}^{\oplus}}.\,(t\,\bm{;}\\!{}^{-}s))\\\
=&((\mathsf{\textup{\Circle}}{}^{+}_{\underline{\,\,\,}:(A\rightarrow
A){}^{\ominus}}.\,\lambda{}^{+}_{x:A{}^{\oplus}}.{x})\bullet\\!\\!{}^{+}\,(\mathsf{\textup{\Circle}}{}^{-}_{\underline{\,\,\,}:(A\rightarrow
A){}^{\oplus}}.\,(t\,\bm{;}\\!{}^{-}s)))\,{\RHD\\!\\!\\!\LHD}\\\
&((\mathsf{\textup{\Circle}}{}^{-}_{\underline{\,\,\,}:(A\rightarrow
A){}^{\oplus}}.\,(t\,\bm{;}\\!{}^{-}s))\bullet\\!\\!{}^{-}\,(\mathsf{\textup{\Circle}}{}^{+}_{\underline{\,\,\,}:(A\rightarrow
A){}^{\ominus}}.\,\lambda{}^{+}_{x:A{}^{\oplus}}.{x}))\\\
\mathrel{\xrightarrow{{\small\mathsf{\beta^{\pm}_{\circ}}}}\\!\\!{}^{*}\,\,}&(\lambda{}^{+}_{x:A{}^{\oplus}}.{x})\mathrel{{\RHD\\!\\!\\!\LHD}}(t\,\bm{;}\\!{}^{-}s)\,\,\xrightarrow{\mathsf{{\RHD\\!\\!\\!\LHD_{\rightarrow}}}}\,\,t\mathrel{\bowtie}s=(t\bullet\\!\\!{}^{+}\,s)\mathrel{{\RHD\\!\\!\\!\LHD}}(s\bullet\\!\\!{}^{-}\,t)\end{array}$

An $\eta$-like rewriting rule can also be incorporated to
$\lambda^{\textup{PRK}}$ as done in [4, Thm. 37], declaring that
$\mathsf{\textup{\Circle}}^{\pm}_{x}.\,(t\bullet\\!\\!^{\pm}\,x)\xrightarrow{\mathsf{\eta_{\circ}}}t$
if $x\notin\mathsf{fv}(t)$. The $\lambda^{\textup{PRK}}$-calculus (with or
without the $\mathsf{\eta_{\circ}}$ rule) enjoys the following properties:

######  Theorem 2.3.

  1. 1.

Subject reduction. If $\Gamma\vdash_{\textup{PRK}}t:P$ and $t\xrightarrow{}s$,
then $\Gamma\vdash_{\textup{PRK}}s:P$.

  2. 2.

Confluence. The $\lambda^{\textup{PRK}}$-calculus has the Church–Rosser
property.

  3. 3.

Classical refinement. $A{}^{\oplus}_{1},\ldots,A{}^{\oplus}_{n}\vdash
B{}^{\oplus}$ holds in $\lambda^{\textup{PRK}}$ if and only if
$A_{1},\ldots,A_{n}\vdash B$ holds in the classical second-order natural
deduction system NK.

######  Proof 2.4.

Subject reduction is a straightforward extension of [4, Prop. 24], with minor
adaptations to account for implication, co-implication, and second-order
quantification. Confluence follows from the fact that $\lambda^{\textup{PRK}}$
can be modeled as an orthogonal higher-order rewriting system in the sense of
Nipkow [34]. Classical refinement is an extension of Prop. 38 and Thm. 39 from
[4]; this theorem has two parts:

  * •

The “only if” direction
($A{}^{\oplus}_{1},\ldots,A{}^{\oplus}_{n}\vdash_{\textup{PRK}}B{}^{\oplus}$
implies $A_{1},\ldots,A_{n}\vdash_{\mathsf{NK}}B$) means that PRK is a
conservative extension of classical second-order logic. To prove this
statement, we generalize the statement as follows: if
$P_{1},\ldots,P_{n}\vdash_{\textup{PRK}}Q$ then
$\iota(P_{1}),\ldots,\iota(P_{n})\vdash_{\mathsf{NK}}\iota(Q)$, where
$\iota(A{}^{\oplus})=\iota(A{}^{+})=A$ and
$\iota(A{}^{\ominus})=\iota(A{}^{-})=\neg A$. This can be shown by a
straightforward induction on the derivation of the first judgment.

  * •

The “if” direction ($A_{1},\ldots,A_{n}\vdash_{\mathsf{NK}}B$ implies
$A{}^{\oplus}_{1},\ldots,A{}^{\oplus}_{n}\vdash_{\textup{PRK}}B{}^{\oplus}$)
means that classical logic can be embedded into PRK. The essence of the proof
is showing that all the inference rules of classical second-order natural
deduction are admissible in $\lambda^{\textup{PRK}}$, taking the weak
affirmation of all propositions (i.e. decorating all formulas with “⊕”). Some
cases are subtle, especially elimination rules. Here we show the introduction
and elimination rules for quantifiers (see Sections B, C in the appendix for
complete proofs):

    1. 1.

Universal introduction. Let
$\Gamma\vdash_{\textup{PRK}}t:(\forall\alpha.\,B){}^{\oplus}$, and define
$t\,\texttt{{@}}^{\mathcal{C}}\,A$ as the following term:
$\mathsf{\textup{\Circle}}{}^{+}_{(x:(B\\{\alpha:=A\\}){}^{\ominus})}.\,((t\bullet\\!\\!{}^{+}\,\mathsf{\textup{\Circle}}{}^{+}_{(\underline{\,\,\,}:(\forall\alpha.\,B){}^{\oplus})}.\,\langle
A,x\rangle{}^{-})@{}^{+}A\bullet\\!\\!{}^{+}\,x)$. Then we have that
$\Gamma\vdash_{\textup{PRK}}t\,\texttt{{@}}^{\mathcal{C}}\,A:B\\{\alpha:=A\\}{}^{\oplus}$.

    2. 2.

Universal elimination. Let
$\Gamma\vdash_{\textup{PRK}}t:(\forall\alpha.\,B){}^{\oplus}$. Define
$t\,\texttt{{@}}^{\mathcal{C}}\,A$ as the following term:
$\mathsf{\textup{\Circle}}{}^{+}_{(x:(B\\{\alpha:=A\\}){}^{\ominus})}.\,((t\bullet\\!\\!{}^{+}\,\mathsf{\textup{\Circle}}{}^{+}_{(\underline{\,\,\,}:(\forall\alpha.\,B){}^{\oplus})}.\,\langle
A,x\rangle{}^{-})@{}^{+}A\bullet\\!\\!{}^{+}\,x)$. Then we have that
$\Gamma\vdash_{\textup{PRK}}t\,\texttt{{@}}^{\mathcal{C}}\,A:B\\{\alpha:=A\\}{}^{\oplus}$.

    3. 3.

Existential introduction. Let
$\Gamma\vdash_{\textup{PRK}}t:(B\\{\alpha:=A\\}){}^{\oplus}$. Define $\langle
A,t\rangle^{\mathcal{C}}$ as the following term:
$\mathsf{\textup{\Circle}}{}^{+}_{(\underline{\,\,\,}:(\exists\alpha.\,B){}^{\ominus})}.\,\langle
A,t\rangle{}^{+}$. Then we have that $\Gamma\vdash_{\textup{PRK}}\langle
A,t\rangle^{\mathcal{C}}:(\exists\alpha.\,B){}^{\oplus}$.

    4. 4.

Existential elimination. Let
$\Gamma\vdash_{\textup{PRK}}t:(\exists\alpha.\,A){}^{\oplus}$ and
$\Gamma,x:A{}^{\oplus}\vdash_{\textup{PRK}}s:B{}^{\oplus}$ with
$\alpha\not\in\mathsf{ftv}(\Gamma,P)$. Define
$\nabla^{\mathcal{C}}\,t[_{(\alpha,x)}.s]$ as the following term:
$\mathsf{\textup{\Circle}}{}^{+}_{(y:B{}^{\ominus})}.\,(\nabla{}^{+}\,t^{\prime}[_{(\alpha,x)}.s]\bullet\\!\\!{}^{+}\,y)$
where
$t^{\prime}\,\mathrel{\overset{\mathrm{def}}{=}}\,t\bullet\\!\\!{}^{+}\,\mathsf{\textup{\Circle}}{}^{-}_{(\underline{\,\,\,}:(\exists\alpha.\,A){}^{\oplus})}.\,\lambda{}^{-}_{\alpha}.\,\mathsf{\textup{\Circle}}{}^{-}_{(x:A{}^{\oplus})}.\,(s\mathrel{\bowtie_{A{}^{-}}}y)$.
Then
$\Gamma\vdash_{\textup{PRK}}\nabla^{\mathcal{C}}\,t[_{(\alpha,x)}.s]:B{}^{\oplus}$.

##  3 Böhm–Berarducci Encodings

It is well-known that, in System F, logical connectives such as $\top$,
$\bot$, $\land$, $\lor$, $\exists$, as well as inductive data types, can be
represented using only $\forall$ and $\rightarrow$ by means of their
Böhm–Berarducci encodings [6], which can be understood as universal properties
or structural induction principles. Böhm–Berarducci encodings can be
reproduced in $\lambda^{\textup{PRK}}$. In the following subsections we study
the encoding of connectives in terms of universal quantification and
implication.

The encoding of conjunction, for instance, can be taken to be $A\land
B\,\mathrel{\overset{\mathrm{def}}{=}}\,\forall\alpha.\,((A\to
B\to\alpha)\to\alpha)$. Then positive typing rules for conjunction, analogous
to I${}_{\land}^{+}$ and E${}^{+}_{\land{i}}$ are derivable, and their
constructions simulate the $\mathsf{\beta{}^{+}_{\land}}$ rule. Indeed, let
$X:=(A_{1}\rightarrow A_{2}\rightarrow A_{i})\rightarrow\alpha$ and
$Y:=A_{1}\rightarrow A_{2}\rightarrow\alpha$. Moreover, let
$X_{i}:=(A_{1}\rightarrow A_{2}\rightarrow A_{i})\rightarrow A_{i}$ and
$Y_{i}:=A_{1}\rightarrow A_{2}\rightarrow A_{i}$. Given $\Gamma\vdash
t_{1}:A_{1}{}^{\oplus}$ and $\Gamma\vdash t_{2}:A_{2}{}^{\oplus}$ and
$\Gamma\vdash s:(A_{1}\land A_{2}){}^{+}$, define:

  * •

$\langle
t_{1},t_{2}\rangle{}^{+}\,\mathrel{\overset{\mathrm{def}}{=}}\,\lambda{}^{+}_{\alpha}.\,\mathsf{\textup{\Circle}}{}^{+}_{(\underline{\,\,\,}:X{}^{\ominus})}.\,\lambda{}^{+}_{(x:Y{}^{\oplus})}.{\mathsf{\textup{\Circle}}{}^{+}_{(y:\alpha{}^{\ominus})}.\,x\bullet\\!\\!{}^{+}\,(\mathsf{\textup{\Circle}}{}^{-}_{(\underline{\,\,\,}:Y{}^{\oplus})}.\,(t_{1}\,\bm{;}\\!{}^{-}u))@{}^{+}t_{1}\bullet\\!\\!{}^{+}\,u@{}^{+}t_{2}\bullet\\!\\!{}^{+}\,y}$,
where
$u\,\mathrel{\overset{\mathrm{def}}{=}}\,\mathsf{\textup{\Circle}}{}^{-}_{(\underline{\,\,\,}:(B\to\alpha){}^{\oplus})}.\,(t_{2}\,\bm{;}\\!{}^{-}y)$.

  * •

$\pi_{i}^{+}(s)\,\mathrel{\overset{\mathrm{def}}{=}}\,\mathsf{\textup{\Circle}}{}^{+}_{(x:A_{i}{}^{\ominus})}.\,(t_{1}@{}^{+}A_{i}\bullet\\!\\!{}^{+}\,(\mathsf{\textup{\Circle}}{}^{+}_{(\underline{\,\,\,}:X_{i}{}^{\oplus})}.\,(r\,\bm{;}\\!{}^{-}x))@{}^{+}r\bullet
x)$,
where
$r\,\mathrel{\overset{\mathrm{def}}{=}}\,\mathsf{\textup{\Circle}}{}^{+}_{(\underline{\,\,\,}:Y_{i}{}^{\ominus})}.\,\lambda{}^{+}_{(y_{1}:A_{1}{}^{\oplus})}.{\mathsf{\textup{\Circle}}{}^{+}_{(\underline{\,\,\,}:(A_{2}\rightarrow
A_{i}){}^{\ominus})}.\,\lambda{}^{+}_{(y_{2}:A_{2}{}^{\oplus})}.{y_{i}}}$.

Then $\Gamma\vdash\langle t_{1},t_{2}\rangle{}^{+}:(A_{1}\land A_{2}){}^{+}$
and $\Gamma\vdash\pi_{i}^{+}(s):A_{i}{}^{\oplus}$ and it can be easily checked
that $\pi_{i}^{+}(\langle
t_{1},t_{2}\rangle{}^{+})\mathrel{\rightarrow^{*}}t_{i}$ (using
$\mathsf{\eta_{\circ}}$).

On the other hand, negative typing rules for conjunction, analogous to
I${}^{-}_{\land{i}}$ and a weak variant of E${}_{\land}^{-}$ can also be
derived. First note that, given terms $\Gamma\vdash p:(A\to B){}^{\oplus}$ and
$\Gamma\vdash q:A{}^{\oplus}$, a term $p\,\texttt{{@}}^{\mathcal{C}}\,q$ may
be defined in such a way that
$\Gamma\vdash_{\textup{PRK}}p\,\texttt{{@}}^{\mathcal{C}}\,q:B{}^{\oplus}$. An
explicit construction is
$p\,\texttt{{@}}^{\mathcal{C}}\,q\,\mathrel{\overset{\mathrm{def}}{=}}\,\mathsf{\textup{\Circle}}{}^{+}_{(x:B{}^{\ominus})}.\,(p\bullet\\!\\!{}^{+}\,(\mathsf{\textup{\Circle}}{}^{-}_{(\underline{\,\,\,}:(A\to
B){}^{\oplus})}.\,(q\,\bm{;}\\!{}^{-}x))@{}^{+}q\bullet\\!\\!{}^{+}\,x)$. Then
we may encode I${}^{-}_{\land{i}}$ and a weak variant of E${}_{\land}^{-}$ as
follows:

  * •

$\mathsf{in}_{i}\\!\\!{}^{-}(t)\,\mathrel{\overset{\mathrm{def}}{=}}\,\langle
A_{i},\mathsf{\textup{\Circle}}{}^{-}_{(\underline{\,\,\,}:X_{i}{}^{\oplus})}.\,(r\,\bm{;}\\!{}^{-}t)\rangle{}^{-}$,
where
$r\,\mathrel{\overset{\mathrm{def}}{=}}\,\mathsf{\textup{\Circle}}{}^{+}_{(\underline{\,\,\,}:Y_{i}{}^{\ominus})}.\,\lambda{}^{+}_{(y_{1}:A_{1}{}^{\oplus})}.{\mathsf{\textup{\Circle}}{}^{+}_{(\underline{\,\,\,}:(A_{2}\rightarrow
A_{i}){}^{\ominus})}.\,\lambda{}^{+}_{(y_{2}:A_{2}{}^{\oplus})}.{y_{i}}}$.

  * •

$\delta{}^{-}t\,[_{a_{1}}.s_{1}][_{a_{2}}.s_{2}]\,\mathrel{\overset{\mathrm{def}}{=}}\,\nabla{}^{-}\,t[_{(\alpha,x:X{}^{\ominus})}.\mathsf{\textup{\Circle}}{}^{-}_{(c:C{}^{\oplus})}.\,s^{\prime}_{1}\bullet\\!\\!{}^{-}\,c]$,
where
$s^{\prime}_{1}\,\mathrel{\overset{\mathrm{def}}{=}}\,s_{1}\\{a_{1}:=\mathsf{\textup{\Circle}}{}^{-}_{(z_{1}:A_{1}{}^{\oplus})}.\,(s^{\prime}_{2}\mathrel{\bowtie_{A{}^{-}}}c)\\}$,
and
$s^{\prime}_{2}\,\mathrel{\overset{\mathrm{def}}{=}}\,s_{2}\\{a_{2}:=\mathsf{\textup{\Circle}}{}^{-}_{(z_{2}:A_{2}{}^{\oplus})}.\,(u\mathrel{\bowtie_{A{}^{-}}}x)\\}$,
and
$u\,\mathrel{\overset{\mathrm{def}}{=}}\,\mathsf{\textup{\Circle}}{}^{+}_{\underline{\,\,\,}:X{}^{\ominus}}.\,\lambda{}^{+}_{y:Y{}^{\oplus}}.{(y\,\texttt{{@}}^{\mathcal{C}}\,z_{1}\,\texttt{{@}}^{\mathcal{C}}\,z_{2})}$.

Note that $\Gamma\vdash\mathsf{in}_{i}\\!\\!{}^{-}(t):(A_{1}\land
A_{2}){}^{-}$ and
$\Gamma\vdash\delta{}^{-}t\,[_{a_{1}}.s_{1}][_{a_{2}}.s_{2}]:C{}^{\ominus}$.
However, unfortunately, it is not the case that
$\delta{}^{-}\mathsf{in}_{i}\\!\\!{}^{-}(t)\,[_{a_{1}}.s_{1}][_{a_{2}}.s_{2}]\mathrel{\rightarrow^{*}}s_{i}\\{a_{i}:=t\\}$;
in fact the computation becomes stuck.

In general, these kinds of encodings are able to simulate reduction for the
positive half of the system but not for the negative half111Naturally, one may
consider dual encodings in terms of $\exists$ and $\ltimes$, for example
$A\lor B=\exists\alpha.\,((A\ltimes B\ltimes\alpha)\ltimes\alpha)$, which
behave well only for the negative half of the system.. This seems to suggest
that $\lambda^{\textup{PRK}}$ cannot be fully simulated by the
$\\{\forall,\rightarrow\\}$ fragment, although we do not know of a proof of
this fact and there might exist other encodings which allow simulating the
full $\lambda^{\textup{PRK}}$ calculus.

In Section D of the appendix, encodings for (positive) disjunction and
existential quantification in terms of $\\{\forall,\rightarrow\\}$ are also
studied.

##  4 Normalization of Second-Order $\lambda^{\textup{PRK}}$

In this section we construct a reducibility model for $\lambda^{\textup{PRK}}$
and we prove adequacy (Thm. 4.2) of the model, from which strong normalization
of second-order $\lambda^{\textup{PRK}}$ follows. We only discuss the proof of
strong normalization for the calculus without the $\mathsf{\eta_{\circ}}$
rule222Strong normalization for the full $\lambda^{\textup{PRK}}$-calculus
with the $\mathsf{\eta_{\circ}}$ rule comes out as a relatively easy corollary
by postponing $\mathsf{\eta_{\circ}}$ steps (see e.g. [4, Theorem 37] for a
similar result)..

In [4], strong normalization for the propositional fragment of
$\lambda^{\textup{PRK}}$ is shown via a translation to System F extended with
recursive type constraints enjoying a (non-strict) positivity condition. This
technique does not seem to extend to the second-order case. The problem is
that the translation given in [4] is not closed under type substitution. More
precisely, if we denote the translation by $\\{\\!\\!\\{-\\}\\!\\!\\}$, an
equality such that
$\\{\\!\\!\\{t\\{\alpha:=A\\}\\}\\!\\!\\}=\\{\\!\\!\\{t\\}\\!\\!\\}\\{\alpha:=\\{\\!\\!\\{A\\}\\!\\!\\}\\}$
does not hold in general, making the proof fail.

Our proof of strong normalization is based on an adaptation of Girard’s
technique of reducibility candidates. Specifically, we adapt Mendler’s proof
of strong normalization for the extended System F given in [30]. We begin by
defining an untyped version of $\lambda^{\textup{PRK}}$:

#### The untyped $\lambda^{\textup{PRK}}$-calculus
($\lambda^{\textup{PRK}}_{\mathbf{U}}$)

By $\mathbf{U}$ we denote the set of untyped terms, given by the following
grammar:

$\begin{array}[]{rrl}a,b,c,\ldots&::=&x\mid
a\mathrel{{\RHD\\!\\!\\!\LHD}}b\mid\langle
a,b\rangle\mid\pi_{i}(a)\mid\mathsf{in}_{i}(a)\mid\delta
a\,[_{x}.b][_{y}.c]\mid\lambda_{x}.\,a\mid
a@b\mid(a\,\bm{;}b)\mid\varrho{a}[_{x;y}.{b}]\\\
&\mid&\mathsf{N}a\mid\mathsf{M}a\mid\lambda_{\Diamond}.\,a\mid
a@\Diamond\mid\langle\Diamond,a\rangle\mid\nabla\,a[_{(\Diamond,x)}.b]\end{array}$

The reduction relation $\to_{\mathbf{U}}\subseteq\mathbf{U}\times\mathbf{U}$
of the $\lambda^{\textup{PRK}}_{\mathbf{U}}$-calculus is defined by the
following reduction rules, closed by compatibility under arbitrary reduction
contexts:

$\begin{array}[]{rcl@{\HS}rcl}\pi_{i}(\langle
a_{1},a_{2}\rangle)&\to_{\mathbf{U}}&a_{i}\hfil\hskip
14.22636pt&\delta(\mathsf{in}_{i}(a))\,[_{x}.b_{1}][_{x}.b_{2}]&\to_{\mathbf{U}}&b_{i}\\{x:=a\\}\\\
(\lambda_{x}.\,a)@b&\to_{\mathbf{U}}&a\\{x:=b\\}\hfil\hskip
14.22636pt&\varrho{(a_{1}\,\bm{;}a_{2})}[_{x;y}.{b}]&\to_{\mathbf{U}}&b\\{x:=a_{1}\\}\\{y:=a_{2}\\}\\\
\mathsf{M}(\mathsf{N}a)&\to_{\mathbf{U}}&a\hfil\hskip 14.22636pt\\\
(\lambda_{\Diamond}.\,a)@\Diamond&\to_{\mathbf{U}}&a\hfil\hskip
14.22636pt&\nabla\,\langle\Diamond,a\rangle[_{(\Diamond,x)}.b]&\to_{\mathbf{U}}&b\\{x:=a\\}\\\
\langle
a_{1},a_{2}\rangle\mathrel{{\RHD\\!\\!\\!\LHD}}\mathsf{in}_{i}(b)&\to_{\mathbf{U}}&a_{i}\mathrel{\bowtie}b\hfil\hskip
14.22636pt&\mathsf{in}_{i}(a)\mathrel{{\RHD\\!\\!\\!\LHD}}\langle
b_{1},b_{2}\rangle&\to_{\mathbf{U}}&a\mathrel{\bowtie}b_{i}\\\
\lambda_{x}.\,a\mathrel{{\RHD\\!\\!\\!\LHD}}(b\,\bm{;}c)&\to_{\mathbf{U}}&a\\{x:=b\\}\mathrel{\bowtie}c\hfil\hskip
14.22636pt&(a\,\bm{;}b)\mathrel{{\RHD\\!\\!\\!\LHD}}\lambda_{x}.\,c&\to_{\mathbf{U}}&b\mathrel{\bowtie}c\\{x:=a\\}\\\
(\mathsf{N}a)\mathrel{{\RHD\\!\\!\\!\LHD}}(\mathsf{N}b)&\to_{\mathbf{U}}&b\mathrel{\bowtie}a\hfil\hskip
14.22636pt\\\
\lambda_{\Diamond}.\,a\mathrel{{\RHD\\!\\!\\!\LHD}}\langle\Diamond,b\rangle&\to_{\mathbf{U}}&a\mathrel{\bowtie}b\hfil\hskip
14.22636pt&\langle\Diamond,a\rangle\mathrel{{\RHD\\!\\!\\!\LHD}}\lambda_{\Diamond}.\,b&\to_{\mathbf{U}}&a\mathrel{\bowtie}b\end{array}$

where
$a\mathrel{\bowtie}b\,\mathrel{\overset{\mathrm{def}}{=}}\,(a@b)\mathrel{{\RHD\\!\\!\\!\LHD}}(b@a)$.
The set $\mathbf{CAN}\subseteq\mathbf{U}$ of canonical terms is the set of
terms built with a constructor, i.e. of any of the forms: $\langle
a,b\rangle$, $\mathsf{in}_{i}(a)$, $\lambda_{x}.\,a$, $(a\,\bm{;}b)$,
$\mathsf{N}a$, $\lambda_{\Diamond}.\,a$, $\langle\Diamond,a\rangle$.

Note that the untyped calculus $\lambda^{\textup{PRK}}_{\mathbf{U}}$ is
obtained from $\lambda^{\textup{PRK}}$ by erasing all signs and type
annotations from terms, replacing types and type variables by a placeholder
“$\Diamond$” in introductors and eliminators for quantifiers, and
identifying333This identification is not essential, but just a matter of
syntactic economy. “weak” abstraction and application
($\mathsf{\textup{\Circle}}_{x}.\,t$ and $t\bullet s$) with regular
abstraction and application ($\lambda_{x}.\,t$ and $t@s$). It is easy to note
that the $\to_{\mathbf{U}}$ reduction is confluent, observing that it can be
modeled as an orthogonal higher-order rewriting system [34].

One difficult aspect of the strong normalization proof is that terms of type
$A{}^{\oplus}$ behave as functions “$A{}^{\ominus}\to A{}^{+}$” and, dually,
terms of $A{}^{\ominus}$ behave as functions “$A{}^{\oplus}\to A{}^{-}$”.
Consequently, sets of reducible terms cannot be defined by straightforward
recursion, as this would lead to a non-well-founded mutual dependency between
reducible terms of types $A{}^{\oplus}$ and $A{}^{\ominus}$. To address this
difficulty, we follow Mendler’s approach of taking fixed points in the
complete lattice of reducibility candidates.

###  4.1 A Reducibility Model for $\lambda^{\textup{PRK}}$

We begin by recalling a few standard notions from order theory. A complete
lattice is a partially ordered set $(A,\leq)$ such that every subset
$B\subseteq A$ has a least upper bound and a greatest lower bound, denoted
respectively by $\bigvee{B}$ and $\bigwedge{B}$. Then (see [11, Thm. 2.35]):

######  Theorem 4.1 (Knaster–Tarski fixed point theorem).

If $(A,\leq)$ is a complete lattice and $f:A\to A$ is an order-preserving map,
i.e. $a\leq a^{\prime}\implies f(a)\leq f(a^{\prime})$, then $f$ has a least
fixed point and a greatest fixed point, given respectively by:
$\bm{\mu}(f)=\bigwedge\\{a\in A\ |\ f(a)\leq a\\}$ and
$\bm{\nu}(f)=\bigvee\\{a\in A\ |\ a\leq f(a)\\}$.

We write $\bm{\mu}(\xi.f(\xi))$ for $\bm{\mu}(f)$ and $\bm{\nu}(\xi.f(\xi))$
for $\bm{\nu}(f)$.

#### Reducibility candidates

Let $\mathbf{SN}\subseteq\mathbf{U}$ denote the set of strongly normalizing
terms, with respect to $\to_{\mathbf{U}}$. A set $\xi\subseteq\mathbf{SN}$ is
closed by reduction if for every $a,b\in\mathbf{U}$ such that $a\in\xi$ and
$a\to_{\mathbf{U}}b$, one has that $b\in\xi$. A set $\xi\subseteq\mathbf{SN}$
is complete if for every $a\in\mathbf{SN}$ the following holds:

($\forall b\in\mathbf{CAN}.\ ((a\to^{*}_{\mathbf{U}}b)\implies b\in\xi$))
implies $a\in\xi$

A set $\xi\subseteq\mathbf{SN}$ is a reducibility candidate (or a r.c. for
short) if it is closed by reduction and complete. We write $\mathbf{RC}$ for
the set of all r.c.’s, that is,
$\mathbf{RC}\,\mathrel{\overset{\mathrm{def}}{=}}\,\\{\xi\subseteq\mathbf{SN}\
|\ \xi\text{ is a r.c.}\\}$.

It is easy to see that reducibility candidates are non-empty. In particular,
for every $\xi\in\mathbf{RC}$ we have that any variable $x\in\xi$ is strongly
normalizing and it vacuously verifies the property $\forall c\in\mathbf{CAN}.\
((x\to^{*}_{\mathbf{U}}c)\implies c\in\xi)$ so, since $\xi$ is complete, we
have that $x\in\xi$. Moreover, the set $\mathbf{RC}$ forms a complete lattice
ordered by inclusion $\subseteq$. Following Mendler [30, Prop. 2], the
greatest lower bound of $\\{\xi_{i}\\}_{i\in{I}}$ is given by the intersection
$\cap_{i\in{I}}{\xi_{i}}$, and the bottom element is the set
$\bm{\bot}=\\{a\in\mathbf{SN}\ |\ \nexists
b\in\mathbf{CAN}.\,a\to^{*}_{\mathbf{U}}b\\}$ of terminating terms that have
no canonical reduct. See Section E in the appendix for details.

#### Operations on reducibility candidates

For each set of canonical terms $X\subseteq\mathbf{CAN}$, we define its
closure $\mathbb{C}{X}$ as the set of all strongly normalizing terms whose
canonical reducts are in $X$. More precisely,
$\mathbb{C}{X}\,\mathrel{\overset{\mathrm{def}}{=}}\,\\{a\in\mathbf{SN}\ |\
\forall b\in\mathbf{CAN}.((a\to^{*}_{\mathbf{U}}b)\implies b\in X)\\}$. If
$\xi_{1},\xi_{2}$ are r.c.’s and if $\\{\xi_{i}\\}_{i\in{I}}$ is a set of
r.c.’s, we define the following operations:

${\small\begin{array}[]{rcl@{\HS}rcl}(\xi_{1}\bm{\times}\xi_{2})&\,\mathrel{\overset{\mathrm{def}}{=}}&\mathbb{C}{\\{\langle
a_{1},a_{2}\rangle\ |\ a_{1}\in\xi_{1},a_{2}\in\xi_{2}\\}}\hfil\hskip
14.22636pt&(\xi_{1}\bm{+}\xi_{2})&\,\mathrel{\overset{\mathrm{def}}{=}}&\mathbb{C}{\\{\mathsf{in}_{i}(a)\
|\ i\in\\{1,2\\},a\in\xi_{i}\\}}\\\
(\xi_{1}\bm{\rightarrow}\xi_{2})&\,\mathrel{\overset{\mathrm{def}}{=}}&\\{a\in\mathbf{SN}\
|\ \forall b\in\xi_{1}.\ a@b\in\xi_{2}\\}\hfil\hskip
14.22636pt&(\xi_{1}\bm{\ltimes}\xi_{2})&\,\mathrel{\overset{\mathrm{def}}{=}}&\mathbb{C}{\\{(a_{1}\,\bm{;}a_{2})\
|\ a_{1}\in\xi_{1},a_{2}\in\xi_{2}\\}}\\\
\bm{\mathord{\sim}}\xi&\,\mathrel{\overset{\mathrm{def}}{=}}&\mathbb{C}{\\{\mathsf{N}a\
|\ a\in\xi\\}}\hfil\hskip 14.22636pt\\\
\bm{\Pi}_{i\in{I}}\,{\xi_{i}}&\,\mathrel{\overset{\mathrm{def}}{=}}&\\{a\in\mathbf{SN}\
|\ \forall i\in{I}.\ a@\Diamond\in\xi_{i}\\}\hfil\hskip
14.22636pt&\bm{\Sigma}_{i\in{I}}\,{\xi_{i}}&\,\mathrel{\overset{\mathrm{def}}{=}}&\mathbb{C}{\\{\langle\Diamond,a\rangle\
|\ \exists i\in I.\ a\in\xi_{i}\\}}\end{array}}$

It can be checked that all these operations map r.c.’s to r.c.’s. See Section
E for details.

A straightforward observation is that the arrow operator is order-reversing on
the left, i.e. that if $\xi_{1}\subseteq\xi^{\prime}_{1}$ then
$(\xi^{\prime}_{1}\bm{\rightarrow}\xi_{2})\subseteq(\xi_{1}\bm{\rightarrow}\xi_{2})$.

#### Orthogonality

The idea of the normalization proof is, as usual, to associate, to each type
$P$, a set of reducible terms $[\\![P]\\!]\in\mathbf{RC}$. The interpretation
of a type variable, such as $[\\![\alpha{}^{+}]\\!]$ or
$[\\![\alpha{}^{-}]\\!]$ shall be given by an environment $\rho$, mapping type
variables to r.c.’s. However, the sets $[\\![\alpha{}^{+}]\\!]$ and
$[\\![\alpha{}^{-}]\\!]$ should not be chosen independently of each other: we
require them to be orthogonal in the following sense.

Two reducibility candidates $\xi_{1},\xi_{2}\in\mathbf{RC}$ are orthogonal, if
for all $a_{1}\in\xi_{1}$ and $a_{2}\in\xi_{2}$ we have that
$(a_{1}\mathrel{{\RHD\\!\\!\\!\LHD}}a_{2})\in\mathbf{SN}$. We write
$\bm{\,\perp\\!\\!\\!\perp}$ for the set of all pairs
$(\xi_{1},\xi_{2})\in\mathbf{RC}^{2}$ such that $\xi_{1}$ and $\xi_{2}$ are
orthogonal.

#### Reducible terms

The set of reducible terms is defined by induction on the following notion of
measure $\\#(-)$ of a type $P$, given by
$\\#(A{}^{+})=\\#(A{}^{-})\,\mathrel{\overset{\mathrm{def}}{=}}\,2|A|$ and
$\\#(A{}^{\oplus})=\\#(A{}^{\ominus})\,\mathrel{\overset{\mathrm{def}}{=}}\,2|A|+1$,
where $|A|$ denotes the size, i.e. the number of symbols, of the pure type
$A$. Note for example that $\\#((A\land B){}^{\oplus})>\\#((A\land
B){}^{+})>\\#(A{}^{\oplus})$.

An environment is a function $\rho$ mapping each type variable $\alpha^{\pm}$,
with either positive or negative sign, to a reducibility candidate
$\rho(\alpha^{\pm})\in\mathbf{RC}$, in such a way that
$(\rho(\alpha{}^{+}),\rho(\alpha{}^{-}))\in\bm{\,\perp\\!\\!\\!\perp}$. If
$(\xi{}^{+},\xi{}^{-})\in\bm{\,\perp\\!\\!\\!\perp}$, we write
$\rho[\alpha:=\xi{}^{+},\xi{}^{-}]$ for the environment $\rho^{\prime}$ that
extends $\rho$ in such a way that $\rho^{\prime}(\alpha{}^{+})=\xi{}^{+}$ and
$\rho^{\prime}(\alpha{}^{-})=\xi{}^{-}$ and
$\rho^{\prime}(\beta^{\pm})=\rho(\beta^{\pm})$ for any other type variable
$\beta\neq\alpha$.

Given an environment $\rho$, we define the set of reducible terms of type $P$
under the environment $\rho$, written $[\\![P]\\!]_{\rho}$, by induction on
the measure $\\#(P)$ as follows:

${\small\begin{array}[]{r@{\,\,}c@{\,\,}l@{\,\,}r@{\,\,}c@{\,\,}l}[\\![\alpha{}^{+}]\\!]_{\rho}&\,\mathrel{\overset{\mathrm{def}}{=}}&\rho(\alpha{}^{+})&[\\![\alpha{}^{-}]\\!]_{\rho}&\,\mathrel{\overset{\mathrm{def}}{=}}&\rho(\alpha{}^{-})\\\
[\\![(A\land
B){}^{+}]\\!]_{\rho}&\,\mathrel{\overset{\mathrm{def}}{=}}&[\\![A{}^{\oplus}]\\!]_{\rho}\bm{\times}[\\![B{}^{\oplus}]\\!]_{\rho}&[\\![(A\land
B){}^{-}]\\!]_{\rho}&\,\mathrel{\overset{\mathrm{def}}{=}}&[\\![A{}^{\ominus}]\\!]_{\rho}\bm{+}[\\![B{}^{\ominus}]\\!]_{\rho}\\\
[\\![(A\lor
B){}^{+}]\\!]_{\rho}&\,\mathrel{\overset{\mathrm{def}}{=}}&[\\![A{}^{\oplus}]\\!]_{\rho}\bm{+}[\\![B{}^{\oplus}]\\!]_{\rho}&[\\![(A\lor
B){}^{-}]\\!]_{\rho}&\,\mathrel{\overset{\mathrm{def}}{=}}&[\\![A{}^{\ominus}]\\!]_{\rho}\bm{\times}[\\![B{}^{\ominus}]\\!]_{\rho}\\\
[\\![(A\rightarrow
B){}^{+}]\\!]_{\rho}&\,\mathrel{\overset{\mathrm{def}}{=}}&[\\![A{}^{\oplus}]\\!]_{\rho}\bm{\rightarrow}[\\![B{}^{\oplus}]\\!]_{\rho}&[\\![(A\rightarrow
B){}^{-}]\\!]_{\rho}&\,\mathrel{\overset{\mathrm{def}}{=}}&[\\![A{}^{\oplus}]\\!]_{\rho}\bm{\ltimes}[\\![B{}^{\ominus}]\\!]_{\rho}\\\
[\\![(A\ltimes
B){}^{+}]\\!]_{\rho}&\,\mathrel{\overset{\mathrm{def}}{=}}&[\\![A{}^{\ominus}]\\!]_{\rho}\bm{\ltimes}[\\![B{}^{\oplus}]\\!]_{\rho}&[\\![(A\ltimes
B){}^{-}]\\!]_{\rho}&\,\mathrel{\overset{\mathrm{def}}{=}}&[\\![A{}^{\ominus}]\\!]_{\rho}\bm{\rightarrow}[\\![B{}^{\ominus}]\\!]_{\rho}\\\
[\\![(\neg
A){}^{+}]\\!]_{\rho}&\,\mathrel{\overset{\mathrm{def}}{=}}&\bm{\mathord{\sim}}[\\![A{}^{\ominus}]\\!]_{\rho}&[\\![(\neg
A){}^{-}]\\!]_{\rho}&\,\mathrel{\overset{\mathrm{def}}{=}}&\bm{\mathord{\sim}}[\\![A{}^{\oplus}]\\!]_{\rho}\\\
[\\![(\forall\alpha.\,A){}^{+}]\\!]_{\rho}&\,\mathrel{\overset{\mathrm{def}}{=}}&\bm{\Pi}_{(\xi{}^{+},\xi{}^{-})\in\bm{\,\perp\\!\\!\\!\perp}}\,{[\\![A{}^{\oplus}]\\!]_{\rho[\alpha:=\xi{}^{+},\xi{}^{-}]}}&[\\![(\forall\alpha.\,A){}^{-}]\\!]_{\rho}&\,\mathrel{\overset{\mathrm{def}}{=}}&\bm{\Sigma}_{(\xi{}^{+},\xi{}^{-})\in\bm{\,\perp\\!\\!\\!\perp}}\,{[\\![A{}^{\ominus}]\\!]_{\rho[\alpha:=\xi{}^{+},\xi{}^{-}]}}\\\
[\\![(\exists\alpha.\,A){}^{+}]\\!]_{\rho}&\,\mathrel{\overset{\mathrm{def}}{=}}&\bm{\Sigma}_{(\xi{}^{+},\xi{}^{-})\in\bm{\,\perp\\!\\!\\!\perp}}\,{[\\![A{}^{\oplus}]\\!]_{\rho[\alpha:=\xi{}^{+},\xi{}^{-}]}}&[\\![(\exists\alpha.\,A){}^{-}]\\!]_{\rho}&\,\mathrel{\overset{\mathrm{def}}{=}}&\bm{\Pi}_{(\xi{}^{+},\xi{}^{-})\in\bm{\,\perp\\!\\!\\!\perp}}\,{[\\![A{}^{\ominus}]\\!]_{\rho[\alpha:=\xi{}^{+},\xi{}^{-}]}}\\\
[\\![A{}^{\oplus}]\\!]_{\rho}&\,\mathrel{\overset{\mathrm{def}}{=}}&\bm{\mu}(\xi.((\xi\bm{\rightarrow}[\\![A{}^{-}]\\!]_{\rho})\bm{\rightarrow}[\\![A{}^{+}]\\!]_{\rho}))&[\\![A{}^{\ominus}]\\!]_{\rho}&\,\mathrel{\overset{\mathrm{def}}{=}}&\bm{\nu}(\xi.((\xi\bm{\rightarrow}[\\![A{}^{+}]\\!]_{\rho})\bm{\rightarrow}[\\![A{}^{-}]\\!]_{\rho}))\end{array}}$

It is straightforward to check for each type $P$ and each environment $\rho$
that $[\\![P]\\!]_{\rho}$ is a reducibility candidate, by induction on the
measure $\\#(P)$. In the case of $[\\![A{}^{\oplus}]\\!]_{\rho}$, by the
Knaster–Tarski theorem (Thm. 4.1), to see that the least fixed point exists,
it suffices to observe that the mapping
$f(\xi)=((\xi\bm{\rightarrow}[\\![A{}^{-}]\\!]_{\rho})\bm{\rightarrow}[\\![A{}^{+}]\\!]_{\rho})$
is order-preserving. The case of $[\\![A{}^{\ominus}]\\!]_{\rho}$ is similar.

#### Adequacy of the reducibility model

For each term $t$ of $\lambda^{\textup{PRK}}$, we define an untyped term $|t|$
of $\lambda^{\textup{PRK}}_{\mathbf{U}}$ via the obvious forgetful map. For
instance
$|\mathsf{\textup{\Circle}}{}^{+}_{(x:(\exists\alpha.\,\alpha){}^{\ominus})}.\,\langle
B,z^{B{}^{\oplus}}\rangle{}^{+}|=\lambda_{x}.\,\langle\Diamond,z\rangle$. Note
that each reduction step $t\xrightarrow{}s$ in $\lambda^{\textup{PRK}}$ is
mapped to a reduction step $|t|\to_{\mathbf{U}}|s|$ in
$\lambda^{\textup{PRK}}_{\mathbf{U}}$. Hence, if $|t|$ is strongly normalizing
with respect to $\to_{\mathbf{U}}$, then $t$ is strongly normalizing with
respect to $\xrightarrow{}$.

A substitution is a function $\sigma$ mapping each variable to a term in
$\mathbf{U}$. We write $a^{\sigma}$ for the term that results from the
capture-avoiding substitution of each free occurrence of each variable $x$ in
$a$ by $\sigma(x)$. We say that the substitution $\sigma$ is adequate for the
typing context $\Gamma$ under the environment $\rho$, and we write
$\sigma\vDash_{\rho}\Gamma$, if for each type assignment $(x:P)\in\Gamma$ we
have that $\sigma(x)\in[\\![P]\\!]_{\rho}$. We are finally able to state the
key result:

######  Theorem 4.2 (Adequacy).

If $\Gamma\vdash t:P$ and $\sigma\vDash_{\rho}\Gamma$ then
$|t|^{\sigma}\in[\\![P]\\!]_{\rho}$.

The proof of the adequacy theorem relies on a number of auxiliary lemmas
stating properties such as
$[\\![A{}^{\oplus}]\\!]_{\rho}=[\\![A{}^{\ominus}]\\!]_{\rho}\bm{\rightarrow}[\\![A{}^{+}]\\!]_{\rho}$
and
$([\\![A{}^{+}]\\!]_{\rho},[\\![A{}^{-}]\\!]_{\rho})\in\bm{\,\perp\\!\\!\\!\perp}$.
See Section E in the appendix for the detailed proof. From this we obtain as
an easy corollary that the $\lambda^{\textup{PRK}}$-calculus is strongly
normalizing, taking $\rho$ as the environment that maps all type variables to
the bottom reducibility candidate, and $\sigma$ as the identity substitution.

##  5 Intuitionistic Proofs and Refutations

In natural deduction, it is well-known that classical logic can be obtained
from the intuitionistic system by adding a single classical axiom, such as
excluded middle or double negation elimination. In sequent calculus, it is
well-known that intuitionistic logic can be obtained by restricting sequents
$A_{1},\ldots,A_{n}\vdash B_{1},\ldots,B_{m}$ to have at most one formula on
the right. As we have seen, $\lambda^{\textup{PRK}}$ refines classical logic.
It is a natural question to ask what subsystem of $\lambda^{\textup{PRK}}$
corresponds to intuitionistic logic.

In this section we characterize a restricted subsystem of
$\lambda^{\textup{PRK}}$ that corresponds to intuitionistic logic, called
$\lambda^{\textup{PRJ}}$, by imposing a syntactic restriction on the shape of
$\lambda^{\textup{PRK}}$ proofs, that forbids certain specific patterns of
reasoning. In particular, a variable $x$ introduced by a positive weak
introduction $\mathsf{\textup{\Circle}}{}^{+}_{x}.\,t$ can only occur free in
$t$ inside the arguments of weak eliminations. The main result in this section
is that $\lambda^{\textup{PRJ}}$ refines intuitionistic second-order logic
(Thm. 5.5).

As mentioned before, proofs of strong propositions in PRK must be
constructive. However, this is only true for the toplevel logical connective
in the formula. In general, a proof of $A{}^{+}$ in PRK does not necessarily
correspond to an intuitionistic proof of $A$. For example, a canonical proof
of $(A\land B){}^{+}$ is given by a proof of $A{}^{\oplus}$ and a proof of
$B{}^{\oplus}$, but these subproofs may resort to classical reasoning
principles.

The key to identify an intuitionistic subset of $\lambda^{\textup{PRK}}$ is to
disallow inference rules which embody classical principles. One example is the
E${}_{\lnot}^{-}$ rule, which derives $A{}^{\oplus}$ from $(\neg A){}^{-}$.
This rule embodies the classical principle of double negation elimination
($\neg\neg A\to A$). Another important example is the I${}_{\circ}^{+}$ rule,
which derives $A{}^{\oplus}$ from $A{}^{\ominus}\vdash A{}^{+}$. This rule
embodies the classical principle of consequentia mirabilis ($(\neg A\to A)\to
A$).

The analysis of the I${}_{\circ}^{+}$ rule suggests that, in the
intuitionistic fragment, $A{}^{\oplus}$ should not be identified with
“$A{}^{\ominus}\to A{}^{+}$”, but directly with $A{}^{+}$. One natural idea
would be to impose an invariant over terms of the form
$\mathsf{\textup{\Circle}}{}^{+}_{(x:A{}^{\ominus})}.\,t$, in such a way that
the body $t$ may have no free occurrences of the negative counterfactual $x$.
With this invariant,

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash t:A{}^{+}\hskip
14.22636ptx\notin\mathsf{fv}(t)$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=91.65808pt\hbox{\kern
3.00003pt$\textsc{\footnotesize{$\textup{{I${}_{\circ}^{+}$}}$
{(variant)}}}$}}}\hbox{\kern
16.12637pt\hbox{$\displaystyle\Gamma\vdash\mathsf{\textup{\Circle}}{}^{+}_{(x:A{}^{\ominus})}.\,t:A{}^{\oplus}$}}}}\end{array}$

all instances of the I${}_{\circ}^{+}$ rule are actually instances of the
variant of I${}_{\circ}^{+}$ shown on the right. This in turn means that, in
an application $t\bullet\\!\\!{}^{+}\,s$, the argument $s$ is useless. Indeed,
if $t$ becomes
$\mathsf{\textup{\Circle}}{}^{+}_{(x:A{}^{\ominus})}.\,t^{\prime}$, the
invariant ensures that $x\notin\mathsf{fv}(t^{\prime})$, so
$(\mathsf{\textup{\Circle}}{}^{+}_{(x:A{}^{\ominus})}.\,t^{\prime})\bullet\\!\\!{}^{+}\,s\to
t^{\prime}$, which does not depend on the specific choice of $s$.

Rather than completely forbidding classical reasoning principles, we relax
this condition so that classical principles are allowed as long as they are
useless, i.e. inside the argument of an application $t\bullet\\!\\!{}^{+}\,s$.
Furthermore, the invariant over terms of the form
$\mathsf{\textup{\Circle}}{}^{+}_{(x:A{}^{\ominus})}.\,t$, requesting that
$x\notin\mathsf{fv}(t)$, can also be relaxed, in such a way that $x$ is
allowed to occur in $t$ as long as all of its free occurrences are useless.
Formally:

######  Definition 5.1 (Intuitionistic terms).

A subterm of a term $t$ is said to be useless if it lies inside the argument
of a positive weak elimination. More precisely, given a term
$t=\mathtt{C}\langle s\rangle$, we say that the subterm $s$ under the context
$\mathtt{C}$ is useless if and only if there exist contexts
$\mathtt{C}_{1},\mathtt{C}_{2}$ and a term $u$ such that $\mathtt{C}$ is of
the form $\mathtt{C}_{1}\langle
u\bullet\\!\\!{}^{+}\,\mathtt{C}_{2}\langle\Box\rangle\rangle$. A subterm of
$t$ is useful if it is not useless. A term is said to be intuitionistic if and
only if the two following conditions hold:

  1. 1.

Useless negative eliminations (E${}_{\land}^{-}$, E${}_{\rightarrow}^{-}$,
E${}_{\lnot}^{-}$, E${}_{\forall}^{-}$). There are no useful subterms of any
of the following forms:
$\delta{}^{-}t\,[_{(x:A{}^{\ominus})}.s][_{(y:B{}^{\ominus})}.u]$,
$\varrho^{-}{t}[_{(x:A{}^{\oplus});(y:B{}^{\ominus})}.{s}]$,
$\mathsf{M}{}^{-}t$, $\nabla{}^{-}\,t[_{(\alpha,x)}.s]$.

  2. 2.

Useless negative counterfactuals. In every useful subterm of the form
$\mathsf{\textup{\Circle}}{}^{+}_{(x:A{}^{\ominus})}.\,t$, there are no useful
occurrences of $x$ in $t$.

#### The $\lambda^{\textup{PRJ}}$ type system

The type system $\lambda^{\textup{PRJ}}$ is defined by imposing the
restriction on $\lambda^{\textup{PRK}}$ that terms be intuitionistic. More
precisely, we say that a judgment $\Gamma\vdash t:P$ holds in PRJ, and in this
case we write $\Gamma\vdash_{\textup{PRJ}}t:P$, if the judgment holds in PRK
and furthermore $t$ is an intuitionistic term. We also write
$P_{1},\ldots,P_{n}\vdash_{\textup{PRJ}}Q$ if there exists a term $t$ such
that $x_{1}:P_{1},\ldots,x_{n}:P_{n}\vdash_{\textup{PRJ}}t:Q$.

######  Example 5.2.

The weak variant of the law of excluded middle, $(A\lor\neg A){}^{\oplus}$,
can be proven in PRK. For example, if we define $\pitchfork^{+}_{A}$:

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

we can note that $\vdash_{\textup{PRK}}\pitchfork^{+}_{A}:(A\lor\neg
A){}^{\oplus}$ holds. However, $\pitchfork^{+}_{A}$ is not intuitionistic, due
to the fact that there is a useful occurrence of the negative counterfactual
$x$.

The intuitionistic fragment is stable by reduction:

######  Proposition 5.3 (Subject reduction for PRJ).

Let $\Gamma\vdash_{\textup{PRJ}}t:P$ and $t\to s$. Then
$\Gamma\vdash_{\textup{PRJ}}s:P$.

######  Proof 5.4.

If $X$ is a set of variables, we say that a term $t$ is $X$-intuitionistic if
it is intuitionistic and, furthermore, it has no useful free occurrences of
variables in $X$. We write $\Gamma\vdash^{X}_{\textup{PRJ}}t:P$, if the
judgment is derivable in PRK and $t$ is $X$-intuitionistic. The statement of
subject reduction is generalized as follows:
$\Gamma\vdash^{X}_{\textup{PRJ}}t:P$ and $t\to s$, then
$\Gamma\vdash^{X}_{\textup{PRJ}}s:P$.

The interesting case is the $\beta$ rule for positive weak proofs,
$(\mathsf{\textup{\Circle}}{}^{+}_{x:A{}^{\ominus}}.\,t)\bullet\\!\\!{}^{+}\,s\xrightarrow{\mathsf{\beta{}^{+}_{\circ}}}t\\{x:=s\\}$.
By hypothesis,
$\Gamma\vdash^{X}_{\textup{PRJ}}(\mathsf{\textup{\Circle}}{}^{+}_{x:A{}^{\ominus}}.\,t)\bullet\\!\\!{}^{+}\,s:A{}^{+}$.
This judgment can only be derived from the I${}_{\circ}^{+}$ rule, so
$\Gamma,x:A{}^{\ominus}\vdash^{X}_{\textup{PRJ}}t:A{}^{+}$. Moreover, $x$ is a
negative counterfactual, so there cannot be useful free occurrences of $x$ in
$t$, which means that
$\Gamma,x:A{}^{\ominus}\vdash^{X\cup\\{x\\}}_{\textup{PRJ}}t:A{}^{+}$. On the
other hand, $s$ lies inside a positive application, so it is not necessarily
$X$-intuitionistic, i.e. we only know
$\Gamma\vdash_{\textup{PRK}}s:A{}^{\ominus}$. The key observation is that all
the copies of $s$ on the right-hand side $t\\{x:=s\\}$ must be useless,
because all the occurrences of $x$ in $t$ are useless. More precisely, from
$\Gamma,x:A{}^{\ominus}\vdash^{X\cup\\{x\\}}_{\textup{PRJ}}t:A{}^{+}$ and
$\Gamma\vdash_{\textup{PRK}}s:A{}^{\ominus}$ one concludes
$\Gamma\vdash^{X}_{\textup{PRJ}}t\\{x:=s\\}:P$ by induction on $t$.

Reasoning principles in PRJ differ from those of PRK. For example, if $P$ is a
weak formula, a sequent $\Gamma,x:P\vdash_{\textup{PRK}}t:Q$ valid in PRK can
always be contraposed to a sequent of the form
$\Gamma,y:Q{}^{\sim}\vdash_{\textup{PRK}}t^{\prime}:P{}^{\sim}$. The analogous
of this contraposition principle in PRJ depends on the sign of $P$. If $P$ is
positive, i.e. $P=A{}^{\oplus}$ the sequent
$\Gamma,x:A{}^{\oplus}\vdash_{\textup{PRJ}}t:Q$ can always be contraposed to
$\Gamma,y:Q{}^{\sim}\vdash_{\textup{PRJ}}t^{\prime}:A{}^{\ominus}$. But if $P$
is negative, i.e. $P=A{}^{\ominus}$ the sequent
$\Gamma,x:A{}^{\ominus}\vdash_{\textup{PRJ}}t:Q$ can only be contraposed to
$\Gamma,y:Q{}^{\sim}\vdash_{\textup{PRJ}}t^{\prime}:A{}^{\oplus}$ if there are
no useful occurrences of $x$ in $t$.

The following theorem is an analog of Thm. 2.3 for $\lambda^{\textup{PRJ}}$.
We omit the proof for lack of space; see Sections F, G, H in the appendix.

######  Theorem 5.5 (Intuitionistic refinement).

$A{}^{\oplus}_{1},\ldots,A{}^{\oplus}_{n}\vdash B{}^{\oplus}$ holds in
$\lambda^{\textup{PRJ}}$ if and only if $A_{1},\ldots,A_{n}\vdash B$ holds in
intuitionistic second-order logic.

##  6 Canonicity

In sequent calculus and natural deduction, an indirect proof (e.g. with cuts),
can always be mechanically converted into a canonical proof (e.g. cut-free),
in which the justification for the conclusion is immediately available, as is
known from the works of Gentzen [19] and Prawitz [40]. Its philosophical
importance is that the validity of an indirect proof can thus be justified by
understanding it as a notation for describing a canonical proof. A practical
consequence is that an explicit witness may be extracted from a proof of
existence.

In this section, we formulate a canonicity result strengthening those of [4].
We start by introducing some nomenclature. Neutral terms ($e,\ldots$) and
normal terms ($f,\ldots$) are given by $e::=x\mid
e\mathrel{{\RHD\\!\\!\\!\LHD_{P}}}f\mid
f\mathrel{{\RHD\\!\\!\\!\LHD_{P}}}e\mid\pi_{i}^{\pm}(e)\mid\delta^{\pm}e\,[_{x}.f][_{x}.f]\mid
e@^{\pm}f\mid\varrho^{\pm}{e}[_{x;y}.{f}]\mid\mathsf{M}^{\pm}e\mid
e@^{\pm}A\mid\nabla^{\pm}\,e[_{(x,\alpha)}.f]\mid e\bullet\\!\\!^{\pm}\,f$ and
$f::=e\mid\langle
f,f\rangle^{\pm}\mid\mathsf{in}_{i}^{\pm}(f)\mid\lambda^{\pm}_{x}.{f}\mid(f\,\bm{;}\\!^{\pm}f)\mid\mathsf{N}^{\pm}f\mid\lambda^{\pm}_{\alpha}.\,f\mid\langle
A,f\rangle^{\pm}\mid\mathsf{\textup{\Circle}}^{\pm}_{x}.\,f$. Terms built with
an introduction rule: $\langle t,s\rangle^{\pm}$, $\mathsf{in}_{i}^{\pm}(t)$,
$\lambda^{\pm}_{x}.{t}$, $(t\,\bm{;}\\!^{\pm}s)$, $\mathsf{N}^{\pm}t$,
$\lambda^{\pm}_{\alpha}.\,t$, $\langle A,t\rangle^{\pm}$,
$\mathsf{\textup{\Circle}}^{\pm}_{x}.\,t$ are called canonical. Then (see Thm.
I.3 in the appendix for details):

######  Theorem 6.1 (Canonicity).

  1. 1.

If $\vdash_{\textup{PRK}}t:P$, then $t$ reduces to a canonical normal form $f$
such that $\vdash_{\textup{PRK}}f:P$.

  2. 2.

If $\vdash_{\textup{PRK}}t:P$, where $P$ is weak, then a canonical normal form
$f$ can be effectively found such that
$\vdash_{\textup{PRK}}\mathsf{\textup{\Circle}}^{\pm}_{(x:P{}^{\sim})}.\,f:P$

Note that this canonicity theorem applies to closed terms only, so there is no
need to include commutative conversions, such as
$\delta{}^{+}x\,[_{y}.t][_{z}.s]\bullet\\!\\!{}^{+}\,u\to\delta{}^{+}x\,[_{y}.t\bullet\\!\\!{}^{+}\,u][_{z}.s\bullet\\!\\!{}^{+}\,u]$,
to unblock redexes. The preceding canonicity result extends and strengthens
Thm. 35 of [4]. The first part of the theorem confirms the intuition,
mentioned in the introduction, that canonical proofs of strong propositions
are always constructed with an introduction rule for the corresponding logical
connective, while canonical proofs of weak propositions proceed by reductio ad
absurdum. For example, if $\vdash t:(A_{1}\land A_{2}){}^{+}$ is the strong
proof of a conjunction, its normal form must be a pair $\langle
t_{1},t_{2}\rangle{}^{+}$ and we know that $\vdash t_{i}:A_{i}{}^{\oplus}$
must hold for $i\in\\{1,2\\}$. On the other hand, if $\vdash s:(A_{1}\land
A_{2}){}^{+}$ is the weak proof of a conjunction, we can only assure that its
normal form is of the form $\mathsf{\textup{\Circle}}{}^{+}_{(x:(A_{1}\land
A_{2}){}^{\ominus})}.\,s^{\prime}$, where $x:(A_{1}\land
A_{2}){}^{\ominus}\vdash s^{\prime}:(A_{1}\land A_{2}){}^{+}$. The second part
of the theorem provides the stronger guarantee that, in such case, one can
compute a canonical $s^{\prime\prime}$ such that $x:(A_{1}\land
A_{2}){}^{\ominus}\vdash s^{\prime\prime}:(A_{1}\land A_{2}){}^{+}$, so in
particular one has that $s^{\prime\prime}=\langle s_{1},s_{2}\rangle{}^{+}$
and that $x:(A_{1}\land A_{2}){}^{\ominus}\vdash s_{i}:A_{i}{}^{\oplus}$ for
all $i\in\\{1,2\\}$.

Canonicity can also be used to obtain a (weak) form of disjunctive property.
In particular, from $\vdash t:(A_{1}\lor A_{2}){}^{\oplus}$ one can always
find an $i\in\\{1,2\\}$ and a term
$\vdash\mathsf{\textup{\Circle}}{}^{+}_{(x:(A_{1}\lor
A_{2}){}^{\ominus})}.\,\mathsf{in}_{i}\\!\\!{}^{+}(t^{\prime}):(A_{1}\lor
A_{2}){}^{\oplus}$ such that $x:(A_{1}\lor A_{2}){}^{\ominus}\vdash
t^{\prime}:A_{i}{}^{\oplus}$. Similarly, a (weak) form of witness extraction
can be obtained: given $\vdash t:(\exists\alpha.\,A){}^{\oplus}$ one can
always find a term
$\vdash\mathsf{\textup{\Circle}}{}^{+}_{(x:(\exists\alpha.\,A){}^{\ominus})}.\,\langle
B,t^{\prime}\rangle{}^{+}:(\exists\alpha.\,A){}^{\oplus}$ where
$x:(\exists\alpha.\,A){}^{\ominus}\vdash
t^{\prime}:A\\{\alpha:=B\\}{}^{\oplus}$.

Furthermore, canonicity provides a purely syntactic proof of the consistency
of PRK444Another way to prove consistency is using Thm. 2.3, noting that
$\vdash_{\textup{PRK}}\alpha{}^{+}$ implies $\vdash_{\mathsf{NK}}\alpha$..
Note, for example, that if $\alpha$ is a base type, there is no canonical term
$t$ such that $\vdash_{\textup{PRK}}t:\alpha{}^{+}$.

##  7 Conclusion

In this paper we have extended the $\lambda^{\textup{PRK}}$-calculus of [4] to
incorporate implication and co-implication, as well as second-order
quantifiers. From the logical point of view, this extension of
$\lambda^{\textup{PRK}}$ refines classical second order logic (Thm. 2.3). From
the computational point of view, it is confluent (Thm. 2.3) and strongly
normalizing (Section 4). These ingredients constitute a computational
interpretation for second-order classical logic. We have identified a well-
behaved subset of the system, called $\lambda^{\textup{PRJ}}$, that refines
intuitionistic second-order logic (Thm. 5.5). We have also formulated a
canonicity (Thm. 6.1) result that strengthens results of previous works. One
noteworthy property of $\lambda^{\textup{PRK}}$ is that both typing and
reduction rules are fully symmetric with respect to the operation that flips
signs and exchanges the roles of dual connectives, while still being
confluent.

#### Related work

The “I${}_{\circ}^{+}$”/“I${}_{\circ}^{-}$” rules in $\lambda^{\textup{PRK}}$
encode a primitive variant of consequentia mirabilis ($(\neg A\to A)\to A$),
while the “$\lambda$” rule in Barbanera and Berardi’s calculus [3], as well as
the “$\mu$” rule in Parigot’s $\lambda\mu$-calculus [36], encode a primitive
variant of double negation elimination ($\neg\neg A\to A$). To prove $A$ using
double negation elimination one may assume $\neg A$ and then provide a proof
of $\bot$. This proof cannot be canonical, as there are no introduction rules
for the empty type. This motivates that we instead rely on consequentia
mirabilis.

Strong normalization proofs are often based on reducibility candidates.
Yamagata proves strong normalization for second-order formulations of
classical calculi [47, 48], via reducibility candidates. Our proof is inspired
by ideas known from the literature of logical relations and biorthogonality:
for instance, the notions of orthogonal r.c.’s and closure of a r.c. can be
traced back to Krivine’s work on classical realizability [27], Pitts’
$\top\top$-closed logical relations [38], and related notions (see e.g. [17]).
The challenging aspect of $\lambda^{\textup{PRK}}$ is the mutually recursive
dependency between $A{}^{\oplus}$ and $A{}^{\ominus}$, for which our key
reference is Mendler’s work [30].

The problem of finding a good calculus for classical logic has not been
unquestionably settled. Current proof assistants based on type theory, such as
Coq, allow classical reasoning by postulating axioms with no computational
content, which breaks canonicity. An established classical calculus is
Parigot’s $\lambda\mu$, whose metatheory has been thoroughly developed; see
for instance [15, 12, 28, 43, 44, 37, 26, 25]. One difference between
$\lambda\mu$ and $\lambda^{\textup{PRK}}$ is that $\lambda^{\textup{PRK}}$
computational rules are based on the standard operation of substitution, while
$\lambda\mu$ is based on an ad hoc substitution operator. Another difference
is that the embedding of the $\lambda$-calculus into $\lambda\mu$ is an
inclusion, whereas the embedding into $\lambda^{\textup{PRK}}$ is much more
convoluted.

Another established classical calculus is Curien and Herbelin’s [9]
$\bar{\lambda}\mu\tilde{\mu}$, whose study is also quite mature; see for
instance [39, 24, 16, 46, 10, 2, 1, 31]. One difference between
$\bar{\lambda}\mu\tilde{\mu}$ and $\lambda^{\textup{PRK}}$ is that
$\bar{\lambda}\mu\tilde{\mu}$ is not confluent unless a reduction strategy is
fixed in the presence of a specific critical pair, whereas
$\lambda^{\textup{PRK}}$ is orthogonal. Another difference is that
$\bar{\lambda}\mu\tilde{\mu}$ is derived from a proof term assignment for
classical sequent calculus, while $\lambda^{\textup{PRK}}$ is defined in
natural deduction style with four forms of judgment (given by the modes
$A{}^{+}$, $A{}^{-}$, $A{}^{\oplus}$, $A{}^{\ominus}$). Munch-Maccagnoni [32]
proposes a classical calculus by polarizing Curien and Herbelin’s calculus, in
such a way that the reduction strategy becomes determined by the polarities.

As mentioned in the introduction, $\lambda^{\textup{PRK}}$ is related to
Nelson’s constructible falsity [33]. Parigot [35] studies free deduction, a
system for classical logic in which natural deduction and sequent calculus can
both be embedded. Rumfitt [42] proposes bilateral logical systems, in which
assertion and denial judgments, with dual rules, are formulated. Zeilberger
[49] studies a polarized logical system with proofs and refutations
distinguishing between verificationist and pragmatist connectives. These
systems, however, do not distinguish between weak and strong propositions, and
they do not have rules analogous to
$\textup{{I${}_{\circ}^{\pm}$}}/\textup{{E${}_{\circ}^{\pm}$}}$.

#### Future work

The merely logical correspondence between $\lambda^{\textup{PRK}}$ and other
classical calculi is immediate, given the fact that $\lambda^{\textup{PRK}}$
refines second-order classical logic (Thm. 2.3). However, it is not obvious
what their relation is from the computational point of view.

In order to be able to build programming languages and proof assistants based
on the principles of $\lambda^{\textup{PRK}}$, it would be convenient to study
dependently typed extensions of the system. It is not a priori clear what such
an extension would look like.

It is known that, in classical logic, reductio ad absurdum can be postponed,
in such a way that it is used at most once, as the last rule in the derivation
[45, 23]. It would be interesting to see if this result can be reproduced in
PRK.

## References

  * [1] Zena M. Ariola, Paul Downen, Hugo Herbelin, Keiko Nakata, and Alexis Saurin.  Classical call-by-need sequent calculi: The unity of semantic artifacts.  In Tom Schrijvers and Peter Thiemann, editors, Functional and Logic Programming - 11th International Symposium, FLOPS 2012, Kobe, Japan, May 23-25, 2012. Proceedings, volume 7294 of Lecture Notes in Computer Science, pages 32–46. Springer, 2012.
  * [2] Zena M Ariola, Hugo Herbelin, and Alexis Saurin.  Classical call-by-need and duality.  In International Conference on Typed Lambda Calculi and Applications, pages 27–44. Springer, 2011.
  * [3] Franco Barbanera and Stefano Berardi.  A symmetric lambda calculus for “classical” program extraction.  In Masami Hagiya and John C. Mitchell, editors, Theoretical Aspects of Computer Software, pages 495–515, Berlin, Heidelberg, 1994. Springer Berlin Heidelberg.
  * [4] Pablo Barenbaum and Teodoro Freund.  A constructive logic with classical proofs and refutations.  In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1–13. IEEE, 2021.
  * [5] Gavin M. Bierman and Valeria CV de Paiva.  On an intuitionistic modal logic.  Studia Logica, 65(3):383–416, 2000.
  * [6] Corrado Böhm and Alessandro Berarducci.  Automatic synthesis of typed lambda-programs on term algebras.  Theor. Comput. Sci., 39:135–154, 1985.
  * [7] Thierry Coquand and Gérard P. Huet.  The calculus of constructions.  Inf. Comput., 76(2/3):95–120, 1988.
  * [8] Tristan Crolard.  Subtractive logic.  Theor. Comput. Sci., 254(1-2):151–185, 2001.  doi:10.1016/S0304-3975(99)00124-3.
  * [9] Pierre-Louis Curien and Hugo Herbelin.  The duality of computation, 2000.
  * [10] Pierre-Louis Curien and Guillaume Munch-Maccagnoni.  The duality of computation under focus.  In Cristian S. Calude and Vladimiro Sassone, editors, Theoretical Computer Science - 6th IFIP TC 1/WG 2.2 International Conference, TCS 2010, Held as Part of WCC 2010, Brisbane, Australia, September 20-23, 2010. Proceedings, volume 323 of IFIP Advances in Information and Communication Technology, pages 165–181. Springer, 2010.
  * [11] Brian A. Davey and Hilary A. Priestley.  Introduction to lattices and order.  Cambridge University Press, Cambridge, 1990.
  * [12] René David and Walter Py.  $\lambda$$\mu$-calculus and böhm’s theorem.  The Journal of Symbolic Logic, 66(1):407–413, 2001.
  * [13] Rowan Davies and Frank Pfenning.  A modal analysis of staged computation.  J. ACM, 48(3):555–604, 2001.
  * [14] Nicolaas Govert De Bruijn.  The mathematical language automath, its usage, and some of its extensions.  In Symposium on automatic demonstration, pages 29–61. Springer, 1970.
  * [15] Philippe de Groote.  An environment machine for the lambda-mu-calculus.  Math. Struct. Comput. Sci., 8(6):637–669, 1998.
  * [16] Daniel J. Dougherty, Silvia Ghilezan, and Pierre Lescanne.  Characterizing strong normalization in the curien-herbelin symmetric lambda calculus: Extending the coppo-dezani heritage.  Theor. Comput. Sci., 398(1-3):114–128, 2008.
  * [17] Paul Downen, Philip Johnson-Freyd, and Zena M. Ariola.  Abstracting models of strong normalization for classical calculi.  J. Log. Algebraic Methods Program., 111:100512, 2020.  doi:10.1016/j.jlamp.2019.100512.
  * [18] Matthias Felleisen, Daniel P. Friedman, Eugene E. Kohlbecker, and Bruce F. Duba.  A syntactic theory of sequential control.  Theor. Comput. Sci., 52:205–237, 1987.  doi:10.1016/0304-3975(87)90109-5.
  * [19] Gerhard Gentzen.  Untersuchungen über das logische schließen. i.  Mathematische zeitschrift, 39(1):176–210, 1935.
  * [20] Jean-Yves Girard.  Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur.  PhD thesis, Université Paris 7, 1972.
  * [21] Jean-Yves Girard.  Linear logic.  Theoretical computer science, 50(1):1–101, 1987.
  * [22] Timothy G Griffin.  A formulae-as-type notion of control.  In Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 47–58, 1989.
  * [23] Giulio Guerrieri and Alberto Naibo.  Postponement of $$\mathsf {raa}$$ raa and glivenko’s theorem, revisited.  Stud Logica, 107(1):109–144, 2019.  doi:10.1007/s11225-017-9781-5.
  * [24] Hugo Herbelin and Silvia Ghilezan.  An approach to call-by-name delimited continuations.  SIGPLAN Not., 43(1):383–394, jan 2008.  URL: https://doi.org/10.1145/1328897.1328484.
  * [25] Delia Kesner, Eduardo Bonelli, and Andrés Viso.  Strong bisimulation for control operators (invited talk).  In Maribel Fernández and Anca Muscholl, editors, 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain, volume 152 of LIPIcs, pages 4:1–4:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.
  * [26] Delia Kesner and Pierre Vial.  Non-idempotent types for classical calculi in natural deduction style.  Log. Methods Comput. Sci., 16(1), 2020.
  * [27] Jean-Louis Krivine.  Realizability in classical logic.  Panoramas et synthèses, 27, 01 2009.
  * [28] Olivier Laurent.  Polarized proof-nets and lambda-$\mathrm{\mu}$-calculus.  Theor. Comput. Sci., 290(1):161–188, 2003.
  * [29] Per Martin-Löf.  A theory of types, 1971.
  * [30] Nax Paul Mendler.  Inductive types and type constraints in the second-order lambda calculus.  Annals of pure and Applied logic, 51(1-2):159–172, 1991.
  * [31] Étienne Miquey.  A classical sequent calculus with dependent types.  ACM Trans. Program. Lang. Syst., 41(2):8:1–8:47, 2019.
  * [32] Guillaume Munch-Maccagnoni.  Focalisation and classical realisability.  In Erich Grädel and Reinhard Kahle, editors, Computer Science Logic, 23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL, Coimbra, Portugal, September 7-11, 2009. Proceedings, volume 5771 of Lecture Notes in Computer Science, pages 409–423. Springer, 2009.  doi:10.1007/978-3-642-04027-6\\_30.
  * [33] David Nelson.  Constructible falsity.  The Journal of Symbolic Logic, 14(1):16–26, 1949.
  * [34] Tobias Nipkow.  Higher-order critical pairs.  In Proceedings 1991 Sixth Annual IEEE Symposium on Logic in Computer Science, pages 342–343. IEEE Computer Society, 1991.
  * [35] Michel Parigot.  Free deduction: An analysis of "computations" in classical logic.  In Andrei Voronkov, editor, Logic Programming, First Russian Conference on Logic Programming, Irkutsk, Russia, September 14-18, 1990 - Second Russian Conference on Logic Programming, St. Petersburg, Russia, September 11-16, 1991, Proceedings, volume 592 of Lecture Notes in Computer Science, pages 361–380. Springer, 1991.  doi:10.1007/3-540-55460-2\\_27.
  * [36] Michel Parigot.  $\lambda$$\mu$-calculus: An algorithmic interpretation of classical natural deduction.  In Andrei Voronkov, editor, Logic Programming and Automated Reasoning, pages 190–201, Berlin, Heidelberg, 1992. Springer Berlin Heidelberg.
  * [37] Pierre-Marie Pédrot and Alexis Saurin.  Classical by-need.  In European Symposium on Programming, pages 616–643. Springer, 2016\.
  * [38] Andrew M. Pitts.  Parametric polymorphism and operational equivalence.  Math. Struct. Comput. Sci., 10(3):321–359, 2000.  URL: http://journals.cambridge.org/action/displayAbstract?aid=44651.
  * [39] Emmanuel Polonovski.  Strong normalization of $\lambda$$\mu$$\mu$-calculus with explicit substitutions.  Lecture Notes in Computer Science, pages 423–437, 2004.
  * [40] Dag Prawitz.  Natural deduction: a proof-theoretical study.  PhD thesis, Almqvist & Wiksell, 1965.
  * [41] John C Reynolds.  Towards a theory of type structure.  In Programming Symposium, pages 408–425. Springer, 1974.
  * [42] Ian Rumfitt.  "yes" and "no".  Mind, 109(436):781–823, 2000.
  * [43] Alexis Saurin.  Separation with streams in the/spl lambda//spl mu/-calculus.  In 20th Annual IEEE Symposium on Logic in Computer Science (LICS’05), pages 356–365. IEEE, 2005.
  * [44] Alexis Saurin.  On the relations between the syntactic theories of lambda-mu-calculi.  In Michael Kaminski and Simone Martini, editors, Computer Science Logic, 22nd International Workshop, CSL 2008, 17th Annual Conference of the EACSL, Bertinoro, Italy, September 16-19, 2008. Proceedings, volume 5213 of Lecture Notes in Computer Science, pages 154–168. Springer, 2008.
  * [45] Jonathan P. Seldin.  On the proof theory of the intermediate logic MH.  J. Symb. Log., 51(3):626–647, 1986.  doi:10.2307/2274019.
  * [46] Steffen van Bakel.  Completeness and partial soundness results for intersection and union typing for lambda${}^{\mbox{{\\_}}}$$\mathrm{\mu}$$\mathrm{\mu}$${}^{\mbox{{\\_}}}$.  Ann. Pure Appl. Log., 161(11):1400–1430, 2010.
  * [47] Yoriyuki Yamagata.  Strong normalization of a symmetric lambda calculus for second-order classical logic.  Arch. Math. Log., 41(1):91–99, 2002.
  * [48] Yoriyuki Yamagata.  Strong normalization of the second-order symmetric lambda mu -calculus.  Inf. Comput., 193(1):1–20, 2004.
  * [49] Noam Zeilberger.  On the unity of duality.  Ann. Pure Appl. Log., 153(1-3):66–96, 2008.  doi:10.1016/j.apal.2008.01.001.

##  Appendix A Second-Order Natural Deduction

######  Definition A.1 (Second-Order Natural Deduction).

Formulas are given by:

$\begin{array}[]{rrl}A&::=&\alpha\mid\bot\mid A\land A\mid A\lor A\mid
A\rightarrow A\mid A\ltimes A\mid\neg
A\mid\forall\alpha.\,A\mid\exists\alpha.\,A\end{array}$

The intuitionistic second-order natural deduction system NJ is given by the
following inference rules.

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 14.85251pt\hbox{$\displaystyle\penalty
1\vphantom{{}^{@}}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=33.62503pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{{ax}}}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma,A\vdash
A$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt
plus 0.0001fil\hbox{\kern 1.125pt\hbox{$\displaystyle\penalty
1\Gamma\vdash\bot$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=22.87503pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{{E$\bot$}}}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash A$}}}}\end{array}$

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash A\hskip
14.22636pt\Gamma\vdash B$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.225pt,depth=0.225pt,width=60.50455pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{{I$\land$}}}}}$}}}\hbox{\kern
10.17569pt\hbox{$\displaystyle\Gamma\vdash A\land
B$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt
plus 0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash A_{1}\land
A_{2}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=42.66507pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{{E$\land_{i}$}}}}}$}}}\hbox{\kern
9.02686pt\hbox{$\displaystyle\Gamma\vdash A_{i}$}}}}\end{array}$
$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 9.02686pt\hbox{$\displaystyle\penalty 1\Gamma\vdash
A_{i}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=42.66508pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{{I$\lor_{i}$}}}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash A_{1}\lor
A_{2}$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash A\lor B\hskip
14.22636pt\Gamma,A\vdash C\hskip 14.22636pt\Gamma,B\vdash C$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=135.03654pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{{E$\lor$}}}}}$}}}\hbox{\kern
55.91765pt\hbox{$\displaystyle\Gamma\vdash C$}}}}\end{array}$

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 3.25pt\hbox{$\displaystyle\penalty 1\Gamma,A\vdash
B$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=39.65317pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{{I$\rightarrow$}}}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash A\rightarrow
B$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt
plus 0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash A\rightarrow B\hskip
14.22636pt\Gamma\vdash A$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.225pt,depth=0.225pt,width=76.75458pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{{E$\rightarrow$}}}}}$}}}\hbox{\kern
26.67572pt\hbox{$\displaystyle\Gamma\vdash B$}}}}\end{array}$
$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash\neg A\hskip
14.22636pt\Gamma\vdash B$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.225pt,depth=0.225pt,width=68.00456pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{{I$\ltimes$}}}}}$}}}\hbox{\kern
13.42569pt\hbox{$\displaystyle\Gamma\vdash A\ltimes
B$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt
plus 0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash A\ltimes B\hskip
14.22636pt\Gamma,\neg A,B\vdash C$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=107.10896pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{{E$\ltimes$}}}}}$}}}\hbox{\kern
41.95386pt\hbox{$\displaystyle\Gamma\vdash C$}}}}\end{array}$

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma,A\vdash\bot$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=30.37505pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{{I$\lnot$}}}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash\lnot
A$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt
plus 0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash\neg A\hskip
14.22636pt\Gamma\vdash A$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.225pt,depth=0.225pt,width=67.47644pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{{E$\lnot$}}}}}$}}}\hbox{\kern
23.4257pt\hbox{$\displaystyle\Gamma\vdash\bot$}}}}\end{array}$

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash A\hskip
14.22636pt\alpha\not\in\mathsf{fv}(\Gamma)$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=78.23376pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{{I$\forall$}}}}}$}}}\hbox{\kern
20.0507pt\hbox{$\displaystyle\Gamma\vdash\forall\alpha.\,A$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
9.62503pt\hbox{$\displaystyle\penalty 1\Gamma\vdash\forall\alpha.\,B$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=60.41054pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{{E$\forall$}}}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash B\\{\alpha:=A\\}$}}}}\end{array}$
$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash B\\{\alpha:=A\\}$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=60.41052pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{{I$\exists$}}}}}$}}}\hbox{\kern
9.62503pt\hbox{$\displaystyle\Gamma\vdash\exists\alpha.\,B$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\Gamma\vdash\exists\alpha.\,A\hskip 14.22636pt\Gamma,A\vdash B\hskip
14.22636pt\alpha\not\in\mathsf{fv}(\Gamma,B)$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=153.64874pt\hbox{\kern
2.70003pt$\textsc{\footnotesize{{{{E$\exists$}}}}}$}}}\hbox{\kern
65.1228pt\hbox{$\displaystyle\Gamma\vdash B$}}}}\end{array}$

The classical second-order natural deduction system NK is obtained by
extending NJ with the law of excluded middle:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 26.18045pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=52.3609pt\hbox{\kern
3.00003pt$\textsc{\footnotesize{{{{lem}}}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash A\lor\neg A$}}}}\end{array}$

Furthermore, the following rules are admissible in NJ and NK.

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 1.04167pt\hbox{$\displaystyle\penalty 1\Gamma\vdash
A$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=27.49991pt\hbox{\kern
3.00003pt$\textsc{\footnotesize{{{{W}}}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Delta\vdash
A$}}}}\end{array}\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt
plus 0.0001fil\hbox{$\displaystyle\penalty 1\Gamma,B\vdash A\hskip
14.22636pt\Gamma\vdash B$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=77.06639pt\hbox{\kern
3.00003pt$\textsc{\footnotesize{{{{Cut}}}}}$}}}\hbox{\kern
25.8249pt\hbox{$\displaystyle\Gamma\vdash A$}}}}\end{array}$

We write $\Gamma\vdash_{\mathsf{NJ}}A$ (respectively,
$\Gamma\vdash_{\mathsf{NK}}A$) if the sequent $\Gamma\vdash A$ holds in NJ
(respectively, NK).

##  Appendix B Subject Reduction for $\lambda^{\textup{PRK}}$

######  Lemma B.1.

The substitution rule is admissible in $\lambda^{\textup{PRK}}$:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 57.2344pt\hbox{$\displaystyle\penalty 1\Gamma\vdash
t:P$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=152.13872pt\hbox{\kern
3.00003pt$\textsc{\footnotesize{{{{SubT}}}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\\{\alpha:=A\\}\vdash
t\\{\alpha:=A\\}:P\\{\alpha:=A\\}$}}}}\end{array}$

######  Proposition B.2 (Subject Reduction).

If $\Gamma\vdash_{\textup{PRK}}t:P$ and $t\xrightarrow{}s$, then
$\Gamma\vdash_{\textup{PRK}}s:P$.

######  Proof B.3.

This extends the proof of Prop. 24 from [4]. The proof follows the usual
methodology, by case analysis on the derivation of the reduction step. We
focus on the more interesting cases, namely the second-order quantifiers. We
only study the positive cases, the negative cases being symmetric.

$\mathsf{\beta{}^{+}_{\forall}}\,/\,\mathsf{\beta{}^{-}_{\exists}}$ rule. Let:

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
18.30148pt\hbox{$\displaystyle\penalty 1\pi$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=42.30324pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash t:B{}^{\oplus}$}}}}\hskip 5.0pt plus
1.0fil\penalty 2\hskip 14.22636pt\alpha\not\in\mathsf{fv}(\Gamma)$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=136.45103pt\hbox{\kern
3.00003pt${\textsc{{{I${}_{\forall}^{+}$}}}}$}}}\hbox{\kern
29.05879pt\hbox{$\displaystyle\Gamma\vdash\lambda{}^{+}_{\alpha}.\,t:\forall\alpha.\,B{}^{+}$}}}}\hskip
5.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=177.39209pt\hbox{\kern
3.00003pt${\textsc{{{E${}_{\forall}^{+}$}}}}$}}}\hbox{\kern
25.68483pt\hbox{$\displaystyle\Gamma\vdash(\lambda{}^{+}_{\alpha}.\,t)@{}^{+}A:B{}^{\oplus}\\{\alpha:=A\\}$}}}}$

Then:

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
21.5098pt\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
18.30148pt\hbox{$\displaystyle\penalty 1\pi$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=42.30324pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash t:B{}^{\oplus}$}}}}\hskip 5.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=119.54166pt\hbox{\kern
3.00003pt${\textsc{{{{SubT}}}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash
t\\{\alpha:=A\\}:B{}^{\oplus}\\{\alpha:=A\\}$}}}}$

Note that $\Gamma=\Gamma\\{\alpha:=A\\}$ holds since
$\alpha\not\in\mathsf{fv}(\Gamma)$.

$\mathsf{\beta{}^{+}_{\exists}}\,/\,\mathsf{\beta{}^{-}_{\forall}}$ rule. Let:

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
38.30553pt\hbox{$\displaystyle\penalty 1\pi$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=82.31133pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash t:B{}^{\oplus}\\{\alpha:=A\\}$}}}}\hskip
5.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=116.53015pt\hbox{\kern
3.00003pt${\textsc{{{I${}_{\exists}^{+}$}}}}$}}}\hbox{\kern
14.09825pt\hbox{$\displaystyle\Gamma\vdash\langle
A,t\rangle^{\pm}:(\exists\alpha.\,B){}^{+}$}}}}\hskip 5.0pt plus
1.0fil\penalty 2\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{\kern 29.27623pt\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=65.79272pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma,x:B{}^{\oplus}\vdash s:P$}}}}\hskip 5.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=257.48276pt\hbox{\kern
3.00003pt${\textsc{{{E${}_{\exists}^{+}$}}}}$}}}\hbox{\kern
76.99902pt\hbox{$\displaystyle\Gamma\vdash\nabla{}^{+}\,\langle
A,t\rangle{}^{+}[_{(\alpha,x)}.s]:P$}}}}$

where $\alpha\not\in\mathsf{fv}(\Gamma,P)$. Then:

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
38.30553pt\hbox{$\displaystyle\penalty 1\pi$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=82.31133pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash t:B{}^{\oplus}\\{\alpha:=A\\}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
21.50981pt\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
29.27623pt\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=65.79272pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma,x:B{}^{\oplus}\vdash s:P$}}}}\hskip 5.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=143.03117pt\hbox{\kern
3.00003pt${\textsc{{{{SubT}}}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma,x:B{}^{\oplus}\\{\alpha:=A\\}\vdash
s\\{\alpha:=A\\}:P$}}}}\hskip 5.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=317.6691pt\hbox{\kern
3.00003pt${\textsc{{{CCut}}}}$}}}\hbox{\kern
103.12752pt\hbox{$\displaystyle\Gamma\vdash s\\{\alpha:=A\\}\\{x:=t\\}:P$}}}}$

$\mathsf{{\RHD\\!\\!\\!\LHD_{\forall}}}$ rule. Let:

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
18.30148pt\hbox{$\displaystyle\penalty 1\pi$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=42.30324pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash t:B{}^{\oplus}$}}}}\hskip 5.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=76.52206pt\hbox{\kern
3.00003pt${\textsc{{{I${}_{\forall}^{+}$}}}}$}}}\hbox{\kern
0.48317pt\hbox{$\displaystyle\Gamma\vdash\lambda{}^{+}_{\alpha}.\,t:\forall\alpha.\,B{}^{+}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\hskip
5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 38.07372pt\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=83.3877pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash
s:B{}^{\ominus}\\{\alpha:=A\\}$}}}}\hskip 5.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=117.60652pt\hbox{\kern
3.00003pt${\textsc{{{I${}_{\forall}^{-}$}}}}$}}}\hbox{\kern
20.47603pt\hbox{$\displaystyle\Gamma\vdash\langle
A,s\rangle{}^{-}:\forall\alpha.\,B{}^{-}$}}}}\hskip 5.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=276.0107pt\hbox{\kern
3.00003pt${\textsc{{{Abs}}}}$}}}\hbox{\kern
87.91777pt\hbox{$\displaystyle\Gamma\vdash(\lambda{}^{+}_{\alpha}.\,t)\mathrel{{\RHD\\!\\!\\!\LHD_{P}}}\langle
A,s\rangle{}^{-}:P$}}}}$

where $\alpha\not\in\mathsf{ftv}(\Gamma)$. Then:

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
21.5098pt\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
18.30148pt\hbox{$\displaystyle\penalty 1\pi$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=42.30324pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash t:B{}^{\oplus}$}}}}\hskip 5.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=119.54166pt\hbox{\kern
3.00003pt${\textsc{{{{SubT}}}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash
t\\{\alpha:=A\\}:B{}^{\oplus}\\{\alpha:=A\\}$}}}}\hskip 5.0pt plus
1.0fil\penalty 2\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{\kern 38.07372pt\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=83.3877pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash
s:B{}^{\ominus}\\{\alpha:=A\\}$}}}}\hskip 5.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=295.25595pt\hbox{\kern
3.00003pt${\textsc{{{Abs}}}}$}}}\hbox{\kern
100.50871pt\hbox{$\displaystyle\Gamma\vdash
t\\{\alpha:=A\\}\mathrel{\bowtie_{P}}s:P$}}}}$

$\xrightarrow{\mathsf{{\RHD\\!\\!\\!\LHD_{\exists}}}}$ rule. Symmetric to
$\xrightarrow{\mathsf{{\RHD\\!\\!\\!\LHD_{\forall}}}}$.

##  Appendix C $\lambda^{\textup{PRK}}$ Refines Classical Second-Order Logic

The proof that $\lambda^{\textup{PRK}}$ refines classical second-order logic
is an extension of analogous results for classical propositional logic in [4].
The proof of Thm. 2.3 is split into two lemmas: Classical Conservativity (Lem.
C.1) proves the implication $1\implies 2$, and Classical Embedding (Lem. C.9)
proves the implication $2\implies 1$.

######  Lemma C.1 (Classical Conservativity).

If $P_{1},\ldots,P_{n}\vdash Q$ holds in $\lambda^{\textup{PRK}}$, then
$\iota(P_{1}),\ldots,\iota(P_{n})\vdash\iota(Q)$ holds in
$\lambda^{\textup{PRK}}$.

######  Proof C.2.

By induction on the derivation of $P_{1},\ldots,P_{n}\vdash Q$, it suffices to
show that all rules of $\lambda^{\textup{PRK}}$ are, from the logical point of
view, admissible in classical second-order logic. The formal target system is
the classical second-order natural deduction system NK described in Section A
of the appendix.

Recall that double negation $A\leftrightarrow\neg\neg A$, as well as all De
Morgan’s laws hold in classical second-order logic; for example
$\vdash_{\mathsf{NK}}\neg(A\land B)\leftrightarrow\neg A\lor\neg B$ and
$\vdash_{\mathsf{NK}}\neg\forall\alpha.\,A\leftrightarrow\exists\alpha.\,\neg
A$. Hence the proof can be reduced to studying the rules for positive
connectives, noting that the proof for the negative rule for the dual
connective must be symmetric:

  1. 1.

Ax: Let $\Gamma\vdash_{\textup{PRK}}x:P$ where $(x:P)\in\Gamma$. Then
$\iota(\Gamma)\vdash_{\mathsf{NK}}\iota(P)$ by ax.

  2. 2.

Abs: Note that $\vdash_{\mathsf{NK}}A\rightarrow\neg A\rightarrow\iota(P)$.

  3. 3.

I${}_{\circ}^{+}$: Let
$\Gamma\vdash_{\textup{PRK}}\mathsf{\textup{\Circle}}{}^{+}_{(x:A{}^{\ominus})}.\,t:A{}^{\oplus}$
be derived from $\Gamma,x:A{}^{\ominus}\vdash_{\textup{PRK}}t:A{}^{+}$. By IH
we have that $\iota(\Gamma),\neg A\vdash_{\mathsf{NK}}A$ which, classically,
implies $\iota(\Gamma)\vdash_{\mathsf{NK}}A$.

  4. 4.

E${}_{\circ}^{+}$: Let
$\Gamma\vdash_{\textup{PRK}}t\bullet\\!\\!{}^{+}\,s:A{}^{+}$ be derived from
$\Gamma\vdash_{\textup{PRK}}t:A{}^{\oplus}$ and
$\Gamma\vdash_{\textup{PRK}}s:A{}^{\ominus}$. By IH on the first premise, we
have that $\iota(\Gamma)\vdash_{\mathsf{NK}}A$, as required.

  5. 5.

I${}_{\land}^{+}$: Note that $\vdash_{\mathsf{NK}}A\rightarrow
B\rightarrow(A\land B)$.

  6. 6.

E${}^{+}_{\land{i}}$: Note that $\vdash_{\mathsf{NK}}(A_{1}\land
A_{2})\rightarrow A_{i}$.

  7. 7.

I${}^{+}_{\lor{i}}$: Note that $\vdash_{\mathsf{NK}}A_{i}\rightarrow(A_{1}\lor
A_{2})$.

  8. 8.

E${}_{\lor}^{+}$: Let
$\Gamma\vdash_{\textup{PRK}}\delta{}^{+}t\,[_{x:A{}^{\oplus}}.s][_{y:B{}^{\oplus}}.u]:P$
be derived from $\Gamma\vdash_{\textup{PRK}}t:(A\lor B){}^{+}$ and
$\Gamma,x:A{}^{\oplus}\vdash_{\textup{PRK}}s:P$ and
$\Gamma,y:B{}^{\oplus}\vdash_{\textup{PRK}}u:P$. By IH,
$\iota(\Gamma)\vdash_{\mathsf{NK}}A\lor B$ and
$\iota(\Gamma),A\vdash_{\mathsf{NK}}\iota(P)$ and
$\iota(\Gamma),B\vdash_{\mathsf{NK}}\iota(P)$, which imply
$\iota(\Gamma)\vdash_{\mathsf{NK}}\iota(P)$ by E$\lor$.

  9. 9.

I${}_{\rightarrow}^{+}$: Let
$\Gamma\vdash_{\textup{PRK}}\lambda{}^{+}_{(x:A{}^{\oplus})}.{t}:(A\rightarrow
B){}^{+}$ be derived from
$\Gamma,x:A{}^{\oplus}\vdash_{\textup{PRK}}t:B{}^{\oplus}$. By IH,
$\iota(\Gamma),A\vdash_{\mathsf{NK}}B$, which implies
$\iota(\Gamma)\vdash_{\mathsf{NK}}A\rightarrow B$ by I$\rightarrow$.

  10. 10.

E${}_{\rightarrow}^{+}$: Note that $\vdash_{\mathsf{NK}}(A\rightarrow
B)\rightarrow A\rightarrow B$.

  11. 11.

I${}_{\ltimes}^{+}$: Note that $\vdash_{\mathsf{NK}}\neg A\rightarrow
B\rightarrow(A\ltimes B)$.

  12. 12.

E${}_{\ltimes}^{+}$: Note that $\vdash_{\mathsf{NK}}(A\ltimes
B)\rightarrow(\neg A\rightarrow B\rightarrow C)\rightarrow C$.

  13. 13.

I${}_{\lnot}^{+}$: Note that $\vdash_{\mathsf{NK}}\neg A\rightarrow\neg A$.
For the dual rule I${}_{\lnot}^{-}$, note that
$\vdash_{\mathsf{NK}}A\rightarrow\neg\neg A$.

  14. 14.

E${}_{\lnot}^{+}$: Note that $\vdash_{\mathsf{NK}}\neg A\rightarrow\neg A$.
For the dual rule E${}_{\lnot}^{-}$, note that $\vdash_{\mathsf{NK}}\neg\neg
A\rightarrow A$, which holds classically.

  15. 15.

I${}_{\forall}^{+}$: Let
$\Gamma\vdash_{\textup{PRK}}\lambda{}^{+}_{\alpha}.\,t:(\forall\alpha.\,A){}^{+}$
be derived from $\Gamma\vdash_{\textup{PRK}}t:A{}^{\oplus}$, where
$\alpha\notin\mathsf{ftv}(\Gamma)$. By IH,
$\iota(\Gamma)\vdash_{\mathsf{NK}}A$. Moreover, note that
$\alpha\notin\mathsf{ftv}(\iota(\Gamma))$ since
$\alpha\notin\mathsf{ftv}(\Gamma)$. Hence by I$\forall$ we have that
$\iota(\Gamma)\vdash_{\mathsf{NK}}\forall\alpha.\,A$.

  16. 16.

E${}_{\forall}^{+}$: Let
$\Gamma\vdash_{\textup{PRK}}t@{}^{+}A:B{}^{\oplus}\\{\alpha:=A\\}$ be derived
from $\Gamma\vdash_{\textup{PRK}}t:(\forall\alpha.\,B){}^{+}$. By IH,
$\iota(\Gamma)\vdash_{\mathsf{NK}}\forall\alpha.\,B$, which implies
$\iota(\Gamma)\vdash_{\mathsf{NK}}B\\{\alpha:=A\\}$ by E$\forall$.

  17. 17.

I${}_{\exists}^{+}$: Let $\Gamma\vdash_{\textup{PRK}}\langle
A,t\rangle{}^{+}:(\exists\alpha.\,B){}^{+}$ be derived from
$\Gamma\vdash_{\textup{PRK}}t:B{}^{\oplus}\\{\alpha:=A\\}$. By IH,
$\iota(\Gamma)\vdash_{\mathsf{NK}}B\\{\alpha:=A\\}$, which implies
$\iota(\Gamma)\vdash_{\mathsf{NK}}\exists\alpha.\,B$ by I$\exists$.

  18. 18.

E${}_{\exists}^{+}$: Let
$\Gamma\vdash_{\textup{PRK}}\nabla{}^{+}\,t[_{(\alpha,x)}.s]:P$ be derived
from $\Gamma\vdash_{\textup{PRK}}t:(\exists\alpha.\,A){}^{+}$ and
$\Gamma,x:A{}^{\oplus}\vdash_{\textup{PRK}}s:P$, where
$\alpha\not\in\mathsf{ftv}(\Gamma,P)$. By IH we have that
$\iota(\Gamma)\vdash_{\mathsf{NK}}\exists\alpha.\,A$ and
$\iota(\Gamma),A\vdash_{\mathsf{NK}}\iota(P)$. Moreover, note that
$\alpha\notin\mathsf{ftv}(\iota(\Gamma),\iota(P))$. Hence by E$\exists$ we
have $\iota(\Gamma)\vdash_{\mathsf{NK}}\iota(P)$, as required.

Before proving embedding, we recall some auxiliary lemmas from [4]:

######  Lemma C.3 (Excluded middle and non-contradiction).

For every pure type $A$, there exist terms $\pitchfork^{+}_{A}$ and
$\pitchfork^{-}_{A}$ such that:

  1. 1.

Excluded middle. $\Gamma\vdash_{\textup{PRK}}\pitchfork^{+}_{A}:(A\lor\neg
A){}^{\oplus}$

  2. 2.

Non-contradiction. $\Gamma\vdash_{\textup{PRK}}\pitchfork^{-}_{A}:(A\land\neg
A){}^{\ominus}$

######  Proof C.4.

For excluded middle, take:

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