11institutetext: The “Simion Stoilow” Institute of Mathematics of the Romanian
Academy
11email<EMAIL_ADDRESS>22institutetext: Faculty of Mathematics and
Informatics, Sofia University “St. Kliment Ohridski”
22email<EMAIL_ADDRESS>
# Modal functional interpretations
(variant with extended††thanks: In the present paper we give a more detailed
treatment of the induction for naturals and we correct the typo in the
definition of the weak compatibility rule $\mathtt{CMP}$: on page 1382 of
[10], it is $s$ instead of $x$ and $t$ instead of $y$; we also give the
treatment of $\mathtt{CMP}$ under Dialectica light. Appendix)

Mircea-Dan Hernest The first author gratefully acknowledges financial support
by the Romanian National Agency for Scientific Research grant PN-II-RU-
TE-2011-3-0122.11 Trifon Trifonov The second author gratefully acknowledges
the financial support of the Bulgarian National Science Fund within project
DTK 02/69-2009.22

###### Abstract

We extend our light Dialectica interpretation [10] to usual and light modal
formulas and prove it sound for pseudo-modal arithmetics based on Gödel’s
${\sf T}$ and classical $S_{4}$. The range of this light modal Dialectica
interpretation is the usual (non-modal) classical Arithmetic in all finite
types. We also illustrate the use of the new tools for optimized program
synthesis with new examples.

This recent work comes in addition to the program extraction technology
outlined in our previous paper [10] by adding a useful device for combining
the effect of previous optimizations by semi- and non-computational
quantifiers in a compact one-step content eraser, namely the modal operator
$\Box$ (and its weak co-modality
$\Diamond^{\\!\mathnormal{c}}\mathnormal{\hskip 0.5pt\equiv\hskip
0.5pt}\lnot\Box\lnot$). Beside the seemingly cosmetic improvement, we bring
the following new result: while the modal propositional axioms of system
$S_{4}$ are realizable, the defining axiom of $S_{5}$ is generally not
realizable under (light) modal Dialectica.

The use and interpretation of modal operators in this paper were inspired by
work of Oliva (partly joint with the first author, see [9]) at the linear
logic sublevel, see [14, 15]. It is no coincidence that, at formulas level,
our interpretation of $\Box A$ is syntactically the same as Oliva’s modified
realizability interpretation of $!A$ in intuitionistic linear logic. However,
a bureaucratic detour would be needed in order to simulate $\Box A$ in terms
of $!A$, which seems less suitable for an efficient computer implementation.

The second author independently noticed the possibility of using the same
supra-linear modal operators for light program extraction in [18], see also
[19]. However, the initiative of studying the full employment of $\Box$ for
more efficient program synthesis in the formal context of a classical first-
order modal logic (in the sense of Schütte, [16]) belongs to the first author.
As we will see, for our extractive purposes it is useful to depart from
Schütte’s original semantics for quantified modal logic. E.g., the
propositional fragments of our first-order modal systems are no longer modal,
but purely boolean, as $\Box p\equiv p\equiv\Diamond^{\\!\mathnormal{c}}p$ for
propositional atoms $p$. We thus design _pseudo_ (i.e., non-standard) modal
arithmetics for program extraction, with relative soundness syntactically
given via our (light) modal functional interpretation by the target system,
namely classical predicate Arithmetic with higher-type functionals, in a
Natural Deduction presentation.

We stress the fact that we are only concerned with fragments of Arithmetics
without undecidable predicates: all propositional atoms of our systems are a
priori decidable.

For an easier presentation we will give up the ‘pseudo’ prefix. Throughout the
paper, our modal Arithmetics are pseudo-modal. Note that soundness of
Schütte’s predicate modal logics (e.g., $S^{\star}_{4}$) is proved non-
constructively, using models, see [16].

##  1 Arithmetical systems for Modal Dialectica extraction

We build upon functional arithmetical systems ${\sf NA}$ and (the light
annotated) $\sf NA_{\mathnormal{l}}$ from [10]. While _verifying system_ ${\sf
NA}$ basically is the Arithmetic $Z$ of Berger, Buchholz and Schwichtenberg
[4] in a slightly different presentation which is more suitable for light
functional synthesis and features full classical logic (without strong
existence) and full extensionality111As inherited from system $Z$, our ${\sf
NA}$ is mostly a Natural Deduction presentation of the so-called ‘negative
arithmetic’ from [20], basically a double-negation, Gödel-Gentzen embedding of
classical into Heyting Arithmetic ${\sf HA}^{\omega}$., its light counterpart
$\sf NA_{\mathnormal{l}}$ is only partly classical. Moreover, the _input
system_ $\sf NA_{\mathnormal{l}}$ is weakly extensional and its contraction
(and hence also induction) rule is restricted for soundness of the (light)
functional interpretation of $\sf NA_{\mathnormal{l}}$ into ${\sf NA}$. In
computing terms, the program synthesis algorithm provided by the light
Dialectica (of [10], as inherited from the one222The restriction on
extensionality is at its turn inherited from the pure Gödel’s functional
interpretation [1, 6], whereas the restriction on contraction was first added
by Hernest, as it was imposed by the necessity of decidability of the
translation of light contraction formulas. of [7]) terminates without error
only modulo the above-mentioned restrictions on Extensionality and
Contraction333These restrictions are more relaxed than those from the first
author’s PhD thesis and weaker than Gödel’s restriction on extensionality,
Kreisel’s avoiding of contraction in his Modified Realizability [12] and
Girard’s total elimination of contraction in his original Linear Logic [5]..

For (light) modal functional synthesis we will use the same verifying system
${\sf NA}$. The simpler input system $\sf NA^{\\!\mathnormal{m}}$ is obtained
by adding $\Box$ to a restricted variant of ${\sf NA}$. This modal Arithmetic
will be proved sound via the modal Dialectica interpretation. The fully-
fledged input system $\sf NA^{\\!\mathnormal{m}}_{\mathnormal{l}}$ adds to
$\sf NA^{\\!\mathnormal{m}}$ all light universal quantifiers and is a modal
extension of $\sf NA_{\mathnormal{l}}$; its soundness will be given by the
light modal Dialectica interpretation. We will not detail here the arithmetics
${\sf NA}$ and $\sf NA_{\mathnormal{l}}$, but rather refer the reader to [10].
We mostly enumerate the new items that are added in order to get $\sf
NA^{\\!\mathnormal{m}}$ and respectively $\sf
NA^{\\!\mathnormal{m}}_{\mathnormal{l}}$. (Systems ${\sf NA}$ and $\sf
NA_{\mathnormal{l}}$ are retaken in the Appendix section 5 .)

The sets of finite types $\mathnormal{T}\hskip 0.5pt,$ terms $\mathcal{T}$ (of
Gödel’s ${\sf T}$), formulas $\mathcal{F}$ (of ${\sf NA}$) and, with the
addition of $\Box$, formulas $\mathcal{F}^{m}$ of $\sf NA^{\\!\mathnormal{m}}$
and $\mathcal{F}^{m}_{l}$ of $\sf NA^{\\!\mathnormal{m}}_{\mathnormal{l}}$ are
defined as follows:

$\displaystyle\mathnormal{T}\quad$ $\displaystyle\rho,\sigma$ $\displaystyle\
\mathtt{::=}\quad\iota\;|\;o\;|\;(\rho\sigma)$ $\displaystyle\mathcal{T}\quad$
$\displaystyle s,t$ $\displaystyle\ \mathtt{::=}\quad
x^{\rho}\;|\;\mathtt{T}^{o}\;|\;\mathtt{F}^{o}\;|\;\mathtt{0}^{\iota}\;|\;\mathtt{S}^{\iota\iota}\;|\;\mathtt{If}^{o\rho\rho\rho}\;|\;\mathtt{R}^{\iota\rho(\iota\rho\rho)\rho}\;|\;(\lambda
x^{\rho}.\,t^{\sigma})^{\rho\sigma}\;|\;(t^{\rho\sigma}s^{\rho})^{\sigma}$
$\displaystyle\mathcal{F}\quad$ $\displaystyle A,B$ $\displaystyle\
\mathtt{::=}\quad\mathtt{at}(t^{o})\;|\;A\rightarrow B\;|\;A\land
B\;|\;\forall x^{\rho}A\;|\;\,\widetilde{\exists}x^{\rho}A\;\mathnormal{\
:\equiv\ }\;\lnot\forall x^{\rho}\lnot A$ $\displaystyle\mathcal{F}^{m}\quad$
$\displaystyle A,B$ $\displaystyle\
\mathtt{::=}\quad\mathtt{at}(t^{o})\;|\;A\rightarrow B\;|\;A\land
B\;|\;\forall x^{\rho}A\;|\;\,\Box
A\;|\;\Diamond^{\\!\mathnormal{c}}A\;\mathnormal{\ :\equiv\ }\;\lnot\Box\lnot
A$ $\displaystyle\mathcal{F}^{m}_{l}\quad$ $\displaystyle A,B$ $\displaystyle\
\mathtt{::=}\quad\mathtt{at}(t^{o})\;|\;A\rightarrow B\;|\;A\land
B\;|\;\forall x^{\rho}A\;|\;\Box
A\;|\;\,\forall_{\left\\{\emptyset,+,-,\pm\right\\}}x^{\rho}A$

Recall that we employ just two basic types: integers $\iota$ and booleans
$o\hskip 0.5pt,$ and use $\rho\sigma\tau$ for $(\rho(\sigma\tau))\hskip
0.5pt.$ Building blocks for terms are the usual constructors for booleans
($\mathtt{T},\mathtt{F}$) and integers ($\mathtt{0},\mathtt{S}$), case
distinction $\mathtt{If}$ and Gödel recursion $\mathtt{R}\hskip 0.5pt.$

The operator ${\sf FV}(\cdot)$ returns the set of free variables of its
argument $t\in\mathcal{T}$ or $A\in\mathcal{F}$. Atomic formulas are decidable
by definition, as they are identified with boolean terms. In particular, we
have decidable falsity $\bot\hskip 1.0pt\mathnormal{\hskip 0.5pt:\equiv\hskip
0.5pt}\hskip 1.0pt\mathtt{at}(\mathtt{F})$ and truth $\top\hskip
1.0pt\mathnormal{\hskip 0.5pt:\equiv\hskip 0.5pt}\hskip
1.0pt\mathtt{at}(\mathtt{T})\hskip 0.5pt.$ As usual, we abbreviate
$A\rightarrow\bot$ by $\lnot A\hskip 0.5pt.$
For the necessity operator $\Box$ we have the following enhanced introduction
rule, which applies to many more premise sequents than usual (as the context
$\Gamma$ may be inhabited, see also Remark 4 in Section 2 for an extended
motivation):
$\begin{array}[]{rl}\Box^{i}:&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 3.8889pt\hbox{$\displaystyle\penalty 1\Gamma\hskip
0.5pt\vdash\hskip 0.5ptA$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=34.19437pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\hskip 0.5pt\vdash\hskip 0.5pt\Box
A$}}}}\end{array}$ ,  where $\Gamma$ is restricted depending on the
translation of the (sub)proof of the premise sequent, in ways that will be
described below for each of the two proof translations: modal and light modal.
The following axioms of modal propositional logic $S_{4}$ are part of $\sf
NA^{\\!\mathnormal{m}}$ and $\sf NA^{\\!\mathnormal{m}}_{\mathnormal{l}}$:
$\begin{array}[]{l@{\qquad\qquad\qquad}l}\mathtt{AxT}:\ \Box A\rightarrow
A&\mathtt{AxT^{c}}:\ A\rightarrow\Diamond^{\\!\mathnormal{c}}A\\\\[3.0pt]
\mathtt{Ax4}:\ \Box A\rightarrow\Box\Box
A&\mathtt{Ax4^{c}}:\Diamond^{\\!\mathnormal{c}}\Diamond^{\\!\mathnormal{c}}A\rightarrow\Diamond^{\\!\mathnormal{c}}A\\\\[3.0pt]
\lx@intercol\mathtt{AxK}:\ [\Box(A\rightarrow B)\land\Box A]\rightarrow\Box
B\hfil\lx@intercol\end{array}$
In fact only $\mathtt{AxT}$ is needed as axiom of our non-standard modal
systems. Of course, $\mathtt{AxT^{c}}$ and $\mathtt{Ax4^{c}}$ were
syntactically deducible from $\mathtt{AxT}$ and respectively $\mathtt{Ax4}$
already in the propositional modal system $S_{4}$, only using minimal logic
(the proof of $\mathtt{Ax4^{c}}$ also uses $\mathtt{AxK}$ and the empty-
context $\Box^{i}$). It turns out that also $\mathtt{Ax4}$ and $\mathtt{AxK}$
are easily deducible in $\sf NA^{\\!\mathnormal{m}}$/$\hskip 1.0pt\sf
NA^{\\!\mathnormal{m}}_{\mathnormal{l}}$ just from $\mathtt{AxT}$ (and only
using minimal logic), given our very liberal necessity introduction rule, see
Definition 3 below. Note that Stability $\lnot\lnot B\rightarrow B$ needs to
be restricted already for $\sf NA^{\\!\mathnormal{m}}$, due to the necessary
restriction on Contraction, see Remark 3 further below, Remark 5 in Section 2
and Section 3.1 of [10].
We denote by $A\rightarrow_{k}B\;\mathnormal{\hskip 0.5pt:\equiv\hskip
0.5pt}\;\Box A\rightarrow B$ the so-called ‘Kreisel implication’, since its
translation by modal Dialectica coincides with its Modified Realizability
interpretation.

######  Definition 1 (modal Dialectica interpretation)

_The interpretation does not change atomic 444Any decidable formula can (and
should) be given via its associated boolean term, e.g., one should rather use
$\mathtt{at}(\mathtt{Odd}(x))$ instead of the more verbose $\forall y(2y\neq
x)\hskip 0.5pt,$ which is refutation relevant in a somewhat artificial and
probably unintended way. formulas, i.e., $|\mathtt{at}(t^{o})|\mathnormal{\
:\equiv\ }\mathtt{at}(t^{o})\hskip 0.5pt.$ Assuming
$|A|^{\boldsymbol{x}}_{\boldsymbol{y}}$ and
$|B|^{\boldsymbol{u}}_{\boldsymbol{v}}$ are already defined,_

$\begin{array}[]{r@{\quad}c@{\quad}l@{\qqquad} r@{\quad}c@{\quad}l}|A\land
B|^{\boldsymbol{x},\boldsymbol{u}}_{\boldsymbol{y},\boldsymbol{v}}&\mathnormal{\hskip
0.5pt:\equiv\hskip
0.5pt}&|A|^{\boldsymbol{x}}_{\boldsymbol{y}}\land|B|^{\boldsymbol{u}}_{\boldsymbol{v}}\hfil\qquad\quad&|\forall
z\hskip 1.0ptA(z)|^{\boldsymbol{f}}_{z,\boldsymbol{y}}&\mathnormal{\hskip
0.5pt:\equiv\hskip 0.5pt}&|A(z)|^{\boldsymbol{f}z}_{\boldsymbol{y}}\\\\[8.0pt]
|A\rightarrow
B|^{\boldsymbol{f},\boldsymbol{g}}_{\boldsymbol{x},\boldsymbol{v}}&\mathnormal{\hskip
0.5pt:\equiv\hskip
0.5pt}&|A|^{\boldsymbol{x}}_{\boldsymbol{f}\boldsymbol{x}\boldsymbol{v}}\rightarrow|B|^{\boldsymbol{g}\boldsymbol{x}}_{\boldsymbol{v}}\hfil\qquad\quad&|\Box
A|^{\boldsymbol{x}}&\mathnormal{\hskip 0.5pt:\equiv\hskip
0.5pt}&\forall\boldsymbol{y}|A|^{\boldsymbol{x}}_{\boldsymbol{y}}\end{array}$

_As an immediate consequence,_

$\begin{array}[]{r@{\quad}c@{\quad}l}|\Diamond^{\\!\mathnormal{c}}A\,\mathnormal{\;\equiv\;}(\lnot\Box\lnot
A)|_{\boldsymbol{f}}&\mathnormal{\;\equiv\;}&\widetilde{\exists}\boldsymbol{x}|A|^{\boldsymbol{x}}_{\boldsymbol{f}\boldsymbol{x}}\\\\[6.0pt]
|A\rightarrow_{k}B\,\mathnormal{\;\equiv\;}(\Box A\rightarrow
B)|^{\boldsymbol{g}}_{\boldsymbol{x},\boldsymbol{v}}&\mathnormal{\;\equiv\;}&\forall\boldsymbol{y}|A|^{\boldsymbol{x}}_{\boldsymbol{y}}\rightarrow|B|^{\boldsymbol{g}\boldsymbol{x}}_{\boldsymbol{v}}\\\\[8.0pt]
|\widetilde{\exists}z\hskip 1.0ptA(z)\,\mathnormal{\;\equiv\;}(\lnot\forall
z\lnot
A(z))|^{Z,\boldsymbol{f}}_{\boldsymbol{g}}&\mathnormal{\;\equiv\;}&\lnot\lnot|A(Z\boldsymbol{g})|^{\boldsymbol{f}\boldsymbol{g}}_{\boldsymbol{g}(Z\boldsymbol{g})(\boldsymbol{f}\boldsymbol{g})}\end{array}$

######  Definition 2 (light modal Dialectica interpretation)

_The following are added to the above (the deduced translation of
$\widetilde{\exists}_{\emptyset}z$ is outlined below for use at the end of
Section 2):_

$\begin{array}[]{r@{\ \ }c@{\ \ }l@{\qquad}r@{\ \ }c@{\ \
}l}|\forall_{\\!+}z\hskip
1.0ptA(z)|^{\boldsymbol{f}}_{\boldsymbol{y}}&\mathnormal{\,:\equiv\,}&\forall
z\hskip 1.0pt|A(z)|^{\boldsymbol{f}z}_{\boldsymbol{y}}&|\forall_{\\!-}z\hskip
1.0ptA(z)|^{\boldsymbol{x}}_{z,\boldsymbol{y}}&\mathnormal{\,:\equiv\,}&|A(z)|^{\boldsymbol{x}}_{\boldsymbol{y}}\\\\[6.0pt]
|\forall_{\\!\emptyset}z\hskip
1.0ptA(z)|^{\boldsymbol{x}}_{\boldsymbol{y}}&\mathnormal{\,:\equiv\,}&\forall
z\hskip
1.0pt|A(z)|^{\boldsymbol{x}}_{\boldsymbol{y}}&|\widetilde{\exists}_{\emptyset}z\hskip
1.0ptB(z)|^{\boldsymbol{f}}_{\boldsymbol{g}}&\mathnormal{\;\equiv\;}&\widetilde{\exists}z\hskip
1.0pt|B(z)|^{\boldsymbol{f}\boldsymbol{g}}_{\boldsymbol{g}(\boldsymbol{f}\boldsymbol{g})}\end{array}$

###### Remark 1

The light modal translation of formulas only adds $|\Box
A|^{\boldsymbol{x}}\mathnormal{\,:\equiv\,}\forall\boldsymbol{y}|A|^{\boldsymbol{x}}_{\boldsymbol{y}}$
to our light functional translation from [10].

The definition of computation relevance of (light) modal formulas $A$ is
basically the same as for non-modal formulas, relative to the enhanced
syntactic context. Namely, $A$ is realization relevant also under (light)
modal Dialectica if the tuple of witness variables $\boldsymbol{x}$ of its
translation $|A|^{\boldsymbol{x}}_{\boldsymbol{y}}$ is not empty and similarly
$A$ is refutation relevant if the tuple of challenge variables
$\boldsymbol{y}$ is not empty. See Remark 1 in Section 3 of [10].
Correspondingly, $A$ is realization irrelevant if it is not realization
relevant (i.e., $\boldsymbol{x}$ is an empty tuple), and $A$ is refutation
irrelevant if it is not refutation relevant (i.e., $\boldsymbol{y}$ is an
empty tuple), see also the more technical Definition 1 in Section 2 of [10].

######  Definition 3 (Necessity Introduction)

The restriction on $\Box^{i}$ depends on programs synthesized from the proof
of the premise $A$ of this rule, unless all formulas in the context $\Gamma$
are refutation irrelevant or $A$ is refutation irrelevant, see the paragraph
following Theorem 2.1 in Section 2 below. Thus input proofs are inductively
defined together with their extracted programs (and their corresponding output
proofs).

######  Remark 2 (restriction violation for $\Box^{i}$)

In an automated interactive search for modal input proofs of a given
specification, we can temporarily allow $\Box^{i}$ and postpone the validity
check for when the proof of its premise is fully constructed. This approach
would be similar to the ‘nc-violations’ check in the actual MinLog system, see
[17], and to the so-called ‘computationally correct proofs’ from [19].

For efficiency reasons, we recommend the use of modal operators whenever
possible instead of the above partly (or non) computational quantifiers
$\forall_{\\!+}$, $\forall_{\\!-}$, $\forall_{\\!\emptyset}$ and
$\widetilde{\exists}_{\emptyset}$. Thus it makes sense to study the (pure)
modal Dialectica in itself, as the use of such light quantifiers may not be
necessary in many cases of interest. It should be much easier to construct a
purely modal (i.e., without light quantifiers) input proof, also for a (semi)
automated proof-search algorithm. Nevertheless, it is the light variant of
modal Dialectica which provides the larger range of possibilities,
particularly for situations where the simpler, ‘heavier’ modal Dialectica does
not suffice.

######  Remark 3 (Contraction restriction)

We upgrade the $\bigstar$ restriction from [10] on the computationally
relevant contractions (those on refutation relevant open assumptions $A$),
such that the interpretation $|A|$ must be decidable (rather than strictly
quantifier-free). In the new modal context one needs to take into account also
the translation of the necessity operator, as this introduces new quantifiers.
These may alter the decidability of the translated formula (relative to the
corresponding non-modal formula obtained by wiping out all instances of
$\Box$). E.g., let $T(x,y,z)$ be a decidable predicate s.t.
$H(x,y)\mathnormal{\ :\equiv\ }\widetilde{\exists}z\hskip 0.5ptT(x,y,z)$ is
not decidable (take Kleene’s $T$ predicate which is expressible in Peano
Arithmetic, hence also in ${\sf NA}$, so that $H$ expresses the Halting
Problem “program with code $x$ halts on input $y$”). Then $P(x)\mathnormal{\
:\equiv\ }\forall y\hskip 0.5pt\forall z\hskip 0.5pt\lnot\hskip 0.5ptT(x,y,z)$
can be a contraction formula, whereas $P^{\Box}(x)\mathnormal{\ :\equiv\
}\forall y\hskip 0.5pt\Box\hskip 0.5pt\forall z\hskip 0.5pt\lnot\hskip
0.5ptT(x,y,z)$ cannot, as its translation is $\forall z\hskip 0.5pt\lnot\hskip
0.5ptT(x,y,z)$, an undecidable formula, since ${\sf NA}\hskip 0.5pt\hskip
0.5pt\vdash\hskip 0.5pt\hskip 0.5pt|P^{\Box}(x)|_{y}\hskip
0.5pt\leftrightarrow\hskip 0.5pt\lnot\hskip 0.5ptH(x,y)$.
On the other hand, both $\forall z(3z\neq x)\land\forall y(2y\neq x)$ and
$\forall z(3z\neq x)\land\Box\hskip 1.0pt\forall y(2y\neq x)$ can be
contraction formulas, since $\forall y(2y\neq x)$ is decidable.

##  2 Modal and light modal functional interpretations

The following metatheorem gives the general pattern in which soundness
theorems for Dialectica-based interpretations can be expressed, in a Natural
Deduction setting.

######  Theorem 2.1 (general soundness for Dialectica interpretations; $[\
\mathrm{ISys},\,\mathrm{VSys}\ ]$)

Let $A_{0},A_{1},\ldots,A_{n}$ be a sequence of formulas of $\mathrm{ISys}$
with $\boldsymbol{w}$ all their free variables. If the sequent $\,\hskip
0.5pta_{1}\\!:\\!A_{1}\hskip 0.5pt,\ldots,\hskip 0.5pta_{n}\\!:\\!A_{n}\hskip
0.5pt\hskip
0.5pt\vdash\\!\\!\\!\raisebox{-2.58334pt}{\scriptsize$l$}\,A_{0}\,$ is
provable in $\mathrm{ISys}\hskip 0.5pt,$ then terms
$\boldsymbol{t}_{0},\ldots,\boldsymbol{t}_{n}$ can be automatically
synthesized from its formal proof, such that the translated sequent $\hskip
0.5pta_{1}\\!:\\!|A_{1}|^{\boldsymbol{x}_{1}}_{\boldsymbol{t}_{1}}\hskip
0.5pt,\ldots,\hskip
0.5pta_{n}\\!:\\!|A_{n}|^{\boldsymbol{x}_{n}}_{\boldsymbol{t}_{n}}\hskip
0.5pt\hskip 0.5pt\vdash\hskip
0.5pt|A_{0}|^{\boldsymbol{t}_{0}}_{\boldsymbol{x}_{0}}\,$ is provable in
$\mathrm{VSys}\hskip 0.5pt,$ where the following _free variable condition_ (c)
holds: ${\sf
FV}(\boldsymbol{t}_{i})\subseteq\\{\boldsymbol{w},\boldsymbol{x}_{0},\ldots,\boldsymbol{x}_{n}\\}$
and $\boldsymbol{x}_{0}\not\in{\sf FV}(\boldsymbol{t}_{0})\hskip 0.5pt.$ Here
$\boldsymbol{x}_{0},\ldots,\boldsymbol{x}_{n}$ are tuples of fresh variables,
s.t. equal avars share a common such tuple.

In [10] the above was thoroughly proved for $\mathrm{ISys}\equiv\sf
NA_{\mathnormal{l}}$ and $\mathrm{VSys}\equiv{\sf NA}$. Below we prove that
(meta)Theorem 2.1 remains valid also for the pairs $[\sf
NA^{\\!\mathnormal{m}},{\sf NA}]$ (modal Dialectica) and $[\sf
NA^{\\!\mathnormal{m}}_{\mathnormal{l}},{\sf NA}]$ (light modal Dialectica),
which share the same $\mathrm{VSys}\equiv{\sf NA}$.
We can now complete the definition of $\Box^{i}$: the restriction is that
$\boldsymbol{x}_{0}\not\in\cup_{i=1}^{n}{\sf FV}(\boldsymbol{t}_{i})$ in the
translated premise sequent $\hskip
0.5pta_{1}\\!:\\!|A_{1}|^{\boldsymbol{x}_{1}}_{\boldsymbol{t}_{1}}\hskip
0.5pt,\ldots,\hskip
0.5pta_{n}\\!:\\!|A_{n}|^{\boldsymbol{x}_{n}}_{\boldsymbol{t}_{n}}\hskip
0.5pt\hskip 0.5pt\vdash\hskip
0.5pt|A_{0}|^{\boldsymbol{t}_{0}}_{\boldsymbol{x}_{0}}\,\hskip 0.5pt.$ This
ensures that the introduction rule $\forall^{i}$ can be applied for variables
$\boldsymbol{x}_{0}$ and thus the conclusion sequent $\,\hskip
0.5pta_{1}\\!:\\!A_{1}\hskip 0.5pt,\ldots,\hskip 0.5pta_{n}\\!:\\!A_{n}\hskip
0.5pt\hskip 0.5pt\vdash\\!\\!\\!\raisebox{-2.58334pt}{\scriptsize$l$}\,\Box
A_{0}\,$ is witnessed by the same realizers as the premise.

######  Lemma 1 (interpretation of $S_{4}$ modal axioms)

Axioms $\mathtt{AxT}$, $\mathtt{AxT^{c}}$, $\mathtt{Ax4}$, $\mathtt{Ax4^{c}}$
and $\mathtt{AxK}$ are realizable in ${\sf NA}$ under the (light) modal
Dialectica translation.

Proof: The translation of $\mathtt{AxT}$ is $|\Box A\rightarrow
A|^{\boldsymbol{g}}_{\boldsymbol{x},\boldsymbol{y}}\equiv\forall\boldsymbol{v}|A|^{\boldsymbol{x}}_{\boldsymbol{v}}\rightarrow|A|^{\boldsymbol{g}\boldsymbol{x}}_{\boldsymbol{y}}$
and we can take $\boldsymbol{g}$ to be the identity
$\lambda\boldsymbol{x}.\,\boldsymbol{x}$. Similarly, the translation of
$\mathtt{AxT^{c}}$ is
$|A\rightarrow\Diamond^{\\!\mathnormal{c}}A|^{\boldsymbol{f}}_{\boldsymbol{x},\boldsymbol{y}}\equiv|A|^{\boldsymbol{x}}_{\boldsymbol{f}\boldsymbol{x}\boldsymbol{y}}\rightarrow\widetilde{\exists}\boldsymbol{u}|A|^{\boldsymbol{u}}_{\boldsymbol{y}}$
and we can take $\boldsymbol{f}$ to be the projection
$\lambda\boldsymbol{x}\boldsymbol{y}.\,\boldsymbol{y}$. For $\mathtt{Ax4}$ and
$\mathtt{Ax4^{c}}$ it is immediate that $|\Box A|\equiv|\Box\Box A|$ and also
$|\Diamond^{\\!\mathnormal{c}}A|\equiv|\Diamond^{\\!\mathnormal{c}}\Diamond^{\\!\mathnormal{c}}A|$,
thus the realizer is again the identity in both cases. In the translation of
$\mathtt{AxK}$ below, we take $\boldsymbol{U}\mathnormal{\hskip
0.5pt:\equiv\hskip
0.5pt}\lambda\boldsymbol{f},\boldsymbol{g},\boldsymbol{x}.\,\boldsymbol{g}\boldsymbol{x}$,
which can easily be proved to be a realizer.

$\begin{array}[]{r@{\quad}c@{\quad}l}|\mathtt{AxK}|&\equiv&[\,\forall\boldsymbol{x},\boldsymbol{v}(|A|^{\boldsymbol{x}}_{\boldsymbol{f}\boldsymbol{x}\boldsymbol{v}}\rightarrow|B|^{\boldsymbol{g}\boldsymbol{x}}_{\boldsymbol{v}})\
\land\
\forall\boldsymbol{y}|A|^{\boldsymbol{{x}^{\prime}}}_{\boldsymbol{y}}\,]^{\boldsymbol{f},\boldsymbol{g},\boldsymbol{{x}^{\prime}}}\
\rightarrow\
\forall\boldsymbol{{v}^{\prime}}|B|^{\boldsymbol{u}}_{\boldsymbol{{v}^{\prime}}}\quad\equiv\\\\[4.0pt]
&\equiv&[\,\forall\boldsymbol{x},\boldsymbol{v}(|A|^{\boldsymbol{x}}_{\boldsymbol{f}\boldsymbol{x}\boldsymbol{v}}\rightarrow|B|^{\boldsymbol{g}\boldsymbol{x}}_{\boldsymbol{v}})\
\land\ \forall\boldsymbol{y}|A|^{\boldsymbol{{x}^{\prime}}}_{\boldsymbol{y}}\
\rightarrow\
\forall\boldsymbol{{v}^{\prime}}|B|^{\boldsymbol{U}(\boldsymbol{f},\boldsymbol{g},\boldsymbol{{x}^{\prime}})}_{\boldsymbol{{v}^{\prime}}}\,]^{\boldsymbol{U}}_{\boldsymbol{f},\boldsymbol{g},\boldsymbol{{x}^{\prime}}}\end{array}$

Given the above Lemma and comments, we have completely established the
following:

######  Theorem 2.2 (soundness of modal Dialectica)

Theorem 2.1 $[\ \sf NA^{\\!\mathnormal{m}},\,{\sf NA}\ ]$.

######  Theorem 2.3 (soundness of light modal Dialectica)

Theorem 2.1 $[\ \sf NA^{\\!\mathnormal{m}}_{\mathnormal{l}},\,{\sf NA}\ ]$.

The next result pictures the limits of our modal extension of Dialectica
interpretation.

######  Theorem 2.4 (unrealizability of $S_{5}$ defining axiom)

Axiom
$\mathtt{Ax5}:\Diamond^{\\!\mathnormal{c}}A\rightarrow\Box\Diamond^{\\!\mathnormal{c}}A$
is generally not realizable under the (light) modal Dialectica translation.

Proof: The translation of $\mathtt{Ax5}$ is a formula of shape
$B(\boldsymbol{x})\rightarrow\forall\boldsymbol{y}B(\boldsymbol{y})$ which
only holds true when $\boldsymbol{x}$ is the empty tuple, special case when
$\mathtt{Ax5}$ requires no realizer at all.

Notice that $\Diamond^{\\!\mathnormal{c}}\widetilde{\exists}\boldsymbol{x}A$
is akin to Berger’s uniform existence $\\{\exists\boldsymbol{x}\\}A$ from [2],
where one does not care about the witness for $\exists\boldsymbol{x}$ (which
is actually deleted from the extraction). We can thus see
$\Diamond^{\\!\mathnormal{c}}$ as an extension of Berger’s tool to more
general formulas than just existential ones. On the other hand there are
situations when $\Box$ and $\Diamond^{\\!\mathnormal{c}}$ are too general
tools and separate annotations for each quantifier are a better answer for the
problem at hand. In some of these cases it may still be possible to use the
modal operators if one changes the input specification and its proof.

######  Remark 4 (Necessity Introduction revisited)

The usual restriction on the introduction rule for the necessity operator
$\Box^{i}$ is that $\Gamma\equiv\emptyset$. In the natural deduction
presentation of modal logic, $\Box^{i}$ cannot be unrestricted or
$A\rightarrow\Box A$ becomes a theorem, thus all occurrences of $\Box$
becoming redundant. Our restriction on $\Box^{i}$ is strictly weaker, as,
e.g., allows any context $\Gamma$ whose formulas are all refutation irrelevant
and any context at all if the conclusion is refutation irrelevant. Thus,
$A\rightarrow\Box A$ not only is possible in our pseudo-modal systems, it even
defines a very interesting class of formulas, see below.

######  Definition 4 (necessary formulas)

Formulas $A$ s.t. $\hskip 1.0pt\hskip 0.5pt\vdash\hskip 0.5pt\hskip
0.5ptA\rightarrow\Box A\,$ in $\sf NA^{\\!\mathnormal{m}}$ or $\sf
NA^{\\!\mathnormal{m}}_{\mathnormal{l}}$.

Also due to $\mathtt{AxT}$, it follows that $\hskip 1.0pt\hskip
0.5pt\vdash\hskip 0.5pt\hskip 0.5ptA\leftrightarrow\Box A\,$ for any necessary
formula, thus placing $\Box$ in front of such $A$ would be logically
redundant. We say that an occurrence of $\Box$ is meaningful (i.e., non-
redundant) in front of any formula that is not necessary.

Note that all refutation irrelevant formulas are necessary formulas. It is
easy to see that some of the refutation relevant formulas are necessary, e.g.,
$\forall\boldsymbol{x}\bot$ and $\forall\boldsymbol{x}\top$ (in fact any $A$
s.t. $\hskip 1.0pt\hskip 0.5pt\vdash\hskip 0.5ptA\hskip 1.0pt$ or $\hskip
1.0pt\hskip 0.5pt\vdash\hskip 0.5pt\hskip 0.5pt\lnot A\hskip 1.0pt$ in $\hskip
1.0pt\sf NA^{\\!\mathnormal{m}}$ or $\hskip 1.0pt\sf
NA^{\\!\mathnormal{m}}_{\mathnormal{l}}$). However, even if such formulas
syntactically do require challengers, these functionals turn out to be
redundant and can be soundly discarded by a $\Box$, without the need to change
any other component of the input proof. In fact, a formula $A$ is necessary
iff it can be proved equivalent (in $\hskip 1.0pt\sf NA^{\\!\mathnormal{m}}$
or $\hskip 1.0pt\sf NA^{\\!\mathnormal{m}}_{\mathnormal{l}}$) to a refutation
irrelevant formula $B$. Indeed, for a necessary $A$ take
$B\mathnormal{\,:\equiv\,}\Box A$. For the converse we can use the long
implication $A\rightarrow B\rightarrow\Box B\rightarrow\Box A$, where for the
last implication a contextless $\Box^{i}$ together with $\mathtt{AxK}$ was
used.

Therefore, the ‘necessary’ class captures those formulas whose negative
computational content can always be erased regardless of the context in which
they are used. On the other hand, there are cases when $\Box$ can soundly be
applied to a non-necessary formula, leading to cleaner and more efficient
extracted programs (see Section 3 below).

######  Remark 5 (modal vs. pseudo-modal)

It would appear that our input Arithmetic $\sf NA^{\\!\mathnormal{m}}$ is able
to prove new modal theorems and even sentences that are invalid in Schütte’s
semantics. On the other hand, our $\bigstar$ restriction on contraction is not
present in the usual first-order modal logic systems, thus some of the
classical modal theorems will no longer be theorems of $\sf
NA^{\\!\mathnormal{m}}$. Therefore, we say that our input systems are ‘pseudo-
modal’ rather than modal. See [13] for extensive comments on the design of
formalisms for predicate modal logic, particularly on the yet-unsatisfactory
definition of necessity introduction in Natural Deduction systems. Contraction
restriction notwithstanding, we give the optimal restriction for $\Box^{i}$ in
view of automated program synthesis. However, this does not solve the issue
for general, fully-fledged first-order modal logics.

###  2.1 Modal induction rule

As first argued in [9], induction (for natural numbers, but more generally
also for lists, as naturals $\iota$ are a particular case of inductively
defined lists) should rather be treated in a Modified Realizability style
whenever possible under Dialectica extraction. In our non-standard modal
context we can introduce the following modal induction rule of systems $\sf
NA^{\\!\mathnormal{m}}$ and $\sf NA^{\\!\mathnormal{m}}_{\mathnormal{l}}$,
which is defined with a Kreisel implication at the step:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\ \hskip 0.5pt\vdash\hskip 0.5pt\
\Box A(\mathtt{0})\qquad\Box\Delta\ \hskip 0.5pt\vdash\hskip 0.5pt\ \Box
A(n)\;\rightarrow\;A(\mathtt{S}n)$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=187.75447pt\hbox{\kern 3.00003pt$\ {\
\mathtt{Ind^{m}_{\iota}}}$}}}\hbox{\kern
52.94556pt\hbox{$\displaystyle\Gamma\,,\,\Box\Delta\ \hskip 0.5pt\vdash\hskip
0.5pt\ \Box A(n)$}}}}\end{array}$

This is an upgrade of the similar rule from [9] (given at the linear logic
sublevel, see also [15]), as it allows for non-empty contexts. While the base
context $\Gamma$ is unrestricted, the step context $\Box\Delta$ is made
entirely of refutation irrelevant assumptions of shape $\Box D$. Thus the step
context restriction as for $\mathtt{Ind^{\iota}_{\mathnormal{l}}}$ (see
Appendix) is bluntly satisfied, since this only concerned refutation relevant
assumptions (whose translations in ${\sf NA}$ had to be quantifier-free, as
their decidability was needed for case distinction in their corresponding
challenge realizers). Note that if $D$ already is refutation irrelevant,
placing $\Box$ in front of $D$ is somewhat redundant. We could refine
$\mathtt{Ind^{m}_{\iota}}$ by splitting the step context into
${\Delta}^{\prime}$ which consists of refutation irrelevant assumptions not of
shape $\Box D$ and ${\Delta}^{\prime\prime}\mathnormal{\;\equiv\;}\Box\Delta$.
Nonetheless such ${\Delta}^{\prime}$ were made of necessary formulas (cf.
Definition 4).

The treatment of $\mathtt{Ind^{m}_{\iota}}$ under (light) modal Dialectica is
much easier than the one of $\mathtt{Ind^{\iota}_{\mathnormal{l}}}$. In fact
$\mathtt{Ind^{m}_{\iota}}$ is a good simplification of
$\mathtt{Ind^{\iota}_{\mathnormal{l}}}$ for situations when the whole context
is made entirely of refutation irrelevant assumptions but $A(n)$ is a
refutation relevant formula. The challenger for $A(n)$ in the step conclusion
would be unneededly produced during the treatment of such
$\mathtt{Ind^{\iota}_{\mathnormal{l}}}$, as it becomes no part of any of the
witnesses for the conclusion sequent. Placing $\Box$ in front of the
negatively positioned $A(n)$ thus ensures a minimal optimization brought by
$\mathtt{Ind^{m}_{\iota}}$, in this particular case simply by elimination of
redundancy: the conclusion witnessing terms are the same as for
$\mathtt{Ind^{\iota}_{\mathnormal{l}}}$.

A more serious optimization concerns the challengers of $|C|$ for refutation
relevant assumptions $C$ from the $\Gamma$ context. These are simply preserved
by $\mathtt{Ind^{m}_{\iota}}$, while under
$\mathtt{Ind^{\iota}_{\mathnormal{l}}}$ they had to include the challengers
for the step $A(n)$. If $A(n)$ were refutation irrelevant, it would still make
sense to use $\mathtt{Ind^{m}_{\iota}}$ instead of
$\mathtt{Ind^{\iota}_{\mathnormal{l}}}$, if one is not interested in the
challengers for the refutation relevant assumptions from the step context.
While for such particular $\mathtt{Ind^{\iota}_{\mathnormal{l}}}$ we already
have the preservation of challengers for refutation relevant assumptions
strictly from $\Gamma$, still challengers for the refutation relevant step
assumptions are more complex in the conclusion sequent (they include a
meaningful Gödel recursion, even though here a challenger for the step
negative $A(n)$ is no longer comprised since it does not exist). Thus
$\mathtt{Ind^{m}_{\iota}}$ can bring an improvement over
$\mathtt{Ind^{\iota}_{\mathnormal{l}}}$ by wiping out the step challengers
altogether, should these not be needed in the global construction of the
topmost realizers for the goal specification.

It turns out that $\mathtt{Ind^{m}_{\iota}}$ strictly optimizes
$\mathtt{Ind^{\iota}_{\mathnormal{l}}}$ in many (if not most) situations. Yet
$\mathtt{Ind^{\iota}_{\mathnormal{l}}}$ will have to be used also in our non-
standard modal context, practically whenever $\mathtt{Ind^{m}_{\iota}}$ simply
cannot be applied for the goal at hand.

##  3 Examples

The weak extensionality of modal input systems $\sf NA^{\\!\mathnormal{m}}$
and $\sf NA^{\\!\mathnormal{m}}_{\mathnormal{l}}$ can better be expressed by
means of the following modal compatibility axiom (the usual compatibility
axiom, but with the outward implication changed to a Kreisel implication)

$\mathtt{CmpAx^{m}}:\
\Box(\boldsymbol{x}=_{\rho}\boldsymbol{y})\,\rightarrow\,A(\boldsymbol{x})\rightarrow
A(\boldsymbol{y})$

By straightforward calculations, it is easy to see that $\mathtt{CmpAx^{m}}$
is realizable under (light) modal Dialectica by simple projection functionals,
with the verification in the fully extensional ${\sf NA}$ given by the
corresponding compatibility axiom $\mathtt{CmpAx}$, see [10].

In [9] the following class of examples was considered: theorems of the form

$\forall\boldsymbol{x}A\to\forall\boldsymbol{y}B\to\forall\boldsymbol{z}C$ (1)

possibly with parameters, where the negative information on $\boldsymbol{x}$
is irrelevant, while the one on $\boldsymbol{y}$ is of our interest. Then it
must be possible to adapt the proof of (1) to a proof in $\sf
NA^{\\!\mathnormal{m}}$ or $\sf NA^{\\!\mathnormal{m}}_{\mathnormal{l}}$ of
$(\Box\forall\boldsymbol{x}A)\to\forall\boldsymbol{y}B\to\forall\boldsymbol{z}C$.
As noticed by Oliva in [15], the Fibonacci example first treated with
Dialectica in [8] falls into this category.

Oliva also suggested an interesting example, which motivated the definition of
our positively computational quantifier $\forall_{\\!+}$ (see [10]): “Any
infinite set $P$ of natural numbers contains numbers which are arbitrarily
apart”. The claim can be formalized as follows:

$\forall x\widetilde{\exists}y(y>x\land P(y))\rightarrow\forall
d\widetilde{\exists}{n_{1},n_{2}}\big{(}n_{2}>n_{1}+d\land P(n_{1})\land
P(n_{2})\big{)}$ (2)

This statement can be proved only via a contraction on the premise, and as a
result $x$ is refuted by a term involving case distinction on $|P|$. However,
if only the witnesses of $n_{1}$ and $n_{2}$ are needed, then the redundant
challenge for $x$ can be discarded by using a $\Box$ in front of the premise,
effectively applying a Kreisel implication. This example is of the form (1)
and can be treated both with the hybrid Dialectica from [9] and with the
extended light Dialectica interpretation from [10].

The example can be extended so that the premise becomes more involved [19]:

$\forall
m(\widetilde{\exists}n\,Q(n,m)\rightarrow\widetilde{\exists}n_{1}\,Q(n_{1},\mathtt{S}m))\rightarrow\widetilde{\exists}n_{0}\,Q(n_{0},\mathtt{0})\rightarrow\widetilde{\exists}n_{2}\,Q(n_{2},\mathtt{S}\mathtt{S}\mathtt{0})$
(3)

Again, a contraction must be used, and two semi-computational quantifiers need
to be applied to erase the negative computational content:

$\forall_{\\!+}m(\widetilde{\exists}_{+}n\,Q(n,m)\rightarrow\widetilde{\exists}n_{1}\,Q(n_{1},\mathtt{S}m))\rightarrow\widetilde{\exists}n_{0}\,Q(n_{0},\mathtt{0})\rightarrow\widetilde{\exists}n_{2}\,Q(n_{2},\mathtt{S}\mathtt{S}\mathtt{0})$
(4)

However, this solution is not desirable, as the light annotations would only
apply to a special class of binary relations $Q$ for which the witness $n_{1}$
for $Q(n_{1},\mathtt{S}m)$ does not depend computationally on the witness $n$
for $Q(n,m)$ for any $m$, hence reducing the generality of the claim. One of
the solutions would be to extend the light annotations to implications as in
[19], however a much simpler and more elegant approach would be to use a
Kreisel implication. The negative content of the premise will be fully erased
and the positive one will be fully preserved, achieving a Modified
Realizability effect.

We will consider another relevant case study, known as the “integer root
example”, which was suggested by Berger and Schwichtenberg in [3]: “every
unbounded integer function has an integer root function”. The example can be
formalized as follows:

$\forall x\widetilde{\exists}y(f(y)>x)\rightarrow\forall
m\Big{(}f(\mathtt{0})\leq m\rightarrow\widetilde{\exists}n\big{(}f(n)\leq
m<f(\mathtt{S}n)\big{)}\Big{)}$ (5)

The claim can be proved by contradiction using induction on the formula
$f(n)\leq m$. However, in addition to computing the integer root, the (heavy)
Dialectica also extracts a complicated recursive counterexample for $x$, with
a case distinction on each step [19]. This term challenges the outermost
premise, which forms the refutation relevant induction context shared by the
base and the step formulas. The undesired negative content can be erased by a
Kreisel implication, which converts the context to a necessary one, allowing
the application of the modal induction rule. As a result, only the integer
root is extracted, and additional artifacts are omitted. Note that, in
contrast to the previous two examples, this proof is classical, so Modified
Realizability is not applicable in this case. However, using $\forall_{\\!+}x$
would still achieve the same cleaning effect [19].

##  4 Conclusions and future work

Modal Dialectica provides the means of using both Modified Realizability and
Gödel’s Dialectica at the same time for more efficient program extraction.
This was already the case for the hybrid Dialectica of [9], but here we
eliminate the detour to the linear logic sublevel. Disregarding the light
quantifiers, (pure) modal Dialectica represents (directly at the supra-linear
logic level) a good combination of the original proof interpretations, with
the possibility of carrying out both in a sound way on certain input proofs.
All one needs is that some implications of the input proof can be seen as
Kreisel implications.

A natural continuation of the work reported in this paper concerns the
addition to our input systems of strong (intuitionistic) elements. Besides the
strong $\exists$ and its light associated $\exists_{\emptyset}$ (originally
from [7] where it was denoted $\overline{\exists}$, see also [19]), strong
possibility $\Diamond$ also needs to be considered as the intuitionistic dual
of necessity $\Box$.

The following clauses would then be added to Definition 1 for getting the
strong modal Dialectica interpretation $|\exists z\hskip
1.0ptA(z)|^{z,\boldsymbol{f}}_{\boldsymbol{y}}\ \mathnormal{\hskip
0.5pt:\equiv\hskip 0.5pt}\ |A(z)|^{\boldsymbol{f}}_{\boldsymbol{y}}$ and
$|\Diamond A|_{\boldsymbol{y}}\ \mathnormal{\hskip 0.5pt:\equiv\hskip 0.5pt}\
\exists\boldsymbol{x}|A|^{\boldsymbol{x}}_{\boldsymbol{y}}$, and further
$|\exists_{\emptyset}z\hskip 1.0ptA(z)|^{\boldsymbol{x}}_{\boldsymbol{y}}\
\mathnormal{\hskip 0.5pt:\equiv\hskip 0.5pt}\ \exists z\hskip
1.0pt|A(z)|^{\boldsymbol{x}}_{\boldsymbol{y}}$ to Definition 2 in order to
obtain the strong light modal Dialectica interpretation.

Intuitionistic (light) modal arithmetical systems will first be considered at
input for ‘strong’ program synthesis. Then their enhanced classical
counterparts will be interpreted, modulo some negative translation. Such
systems will soundly extend $\sf NA^{\\!\mathnormal{m}}$ with $\Diamond$ and
$\exists$, and $\sf NA^{\\!\mathnormal{m}}_{\mathnormal{l}}$ also with
$\exists_{\emptyset}$. Nevertheless certain restrictions may need to be
applied on $\sf NA^{\\!\mathnormal{m}}$ and/or $\sf
NA^{\\!\mathnormal{m}}_{\mathnormal{l}}$ before attempting such extensions
with intuitionistic elements.

Acknowledgements: Our first reading of predicate modal logic was [16], a rare
small and complete presentation of the topic, recommended by Prof.
Schwichtenberg, to whom we are grateful. Thanks to Diana Ratiu for providing
us a copy of this book. Many thanks to Paulo Oliva for valuable comments on an
early draft of this paper.

## References

  * [1] J. Avigad and S. Feferman.  Gödel’s functional (“Dialectica”) interpretation.  In S. R. Buss, editor, Handbook of proof theory, volume 137 of Studies in Logic and the Foundations of Mathematics, pages 337–405. North Holland, Amsterdam, 1998.
  * [2] U. Berger.  Program extraction from normalization proofs.  In M. Bezem, editor, Typed Lambda Calculi and Applications, volume 664 of Lecture Notes in Computer Science, pages 91–106. Springer Verlag, 1993.
  * [3] U. Berger and H. Schwichtenberg.  Program extraction from classical proofs.  In D. Leivant, editor, Logic and Computational Complexity Workshop (LCC’94), volume 960 of Lecture Notes in Computer Science, pages 77–97. Springer, Berlin, 1995.
  * [4] U. Berger, H. Schwichtenberg, and W. Buchholz.  Refined program extraction from classical proofs.  Annals of Pure and Applied Logic, 114:3–25, 2002.
  * [5] J.-Y. Girard.  Linear logic.  Theoretical Computer Science, 50(1):1–102, 1987.
  * [6] K. Gödel.  Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes.
Dialectica, 12:280–287, 1958.

  * [7] M.-D. Hernest.  Optimized programs from (non-constructive) proofs by the light (monotone) Dialectica interpretation.  PhD Thesis, École Polytechnique and Universität München, 2006.  http://www.cs.au.dk/~danher/teza/thesfull.pdf.
  * [8] M.-D. Hernest.  Light Dialectica program extraction from a classical Fibonacci proof.
Electronic Notes in Theoretical Computer Science, 171(3):43–53, 2007.

  * [9] M.-D. Hernest and P. Oliva.  Hybrid functional interpretations.  In A. Beckmann, C. Dimitracopoulos, and B. Löwe, editors, Logic and Theory of Algorithms: 4th “Computability in Europe” conference, Athens, Greece, volume 5028 of Lecture Notes in Computer Science, pages 251–260. Springer Verlag, 2008.
  * [10] M.-D. Hernest and T. Trifonov.  Light dialectica revisited.  Annals of Pure and Applied Logic, 161:1379–1389, 2010.  http://dx.doi.org/10.1016/j.apal.2010.04.008.
  * [11] U. Kohlenbach.  A note on Spector’s quantifier-free rule of extensionality.
Archive for Mathematical Logic, 40:89–92, 2001.

  * [12] G. Kreisel.  Interpretation of analysis by means of constructive functionals of finite types.  In A. Heyting, editor, Constructivity in Mathematics, pages 101–128. North Holland, 1959.
  * [13] S. Negri and J. von Plato.  Proof analysis.  Manuscript, 2009.  243 pp.
  * [14] P. Oliva.  Modified realizability interpretation of classical linear logic.  In Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science. IEEE Press, 2007.
  * [15] P. Oliva.  Hybrid functional interpretations of linear and intuitionistic logic.  Journal of Logic and Computation, 2010.  http://dx.doi.org/10.1093/logcom/exq007.
  * [16] K. Schütte.  Vollständige System modaler und institutionstischer Logik.  Springer, 1968.
  * [17] H. Schwichtenberg.  Minlog system documentation.  http://www.math.lmu.de/~logik/minlog/documentation.php, December 2011.
  * [18] T. Trifonov.  Dialectica interpretation with fine computational control.  In K. Ambos-Spies, B. Löwe, and W. Merkle, editors, Mathematical Theory and Computational Practice: 5th “Computability in Europe” conference, Heidelberg, Germany, volume 5635 of Lecture Notes in Computer Science, pages 467–477. Springer Verlag, 2009.
  * [19] T. Trifonov.  Analysis of methods for extraction of programs from non-constructive proofs.  PhD thesis, University of Munich, Germany, 2011.
  * [20] A. S. Troelstra.  Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, volume 344 of Lecture Notes in Mathematics.  Springer-Verlag, 1973.

$\mbox{$\mathtt{T}\mathtt{Ax}$}:\quad\hskip 0.5pt\vdash\hskip 0.5pt\mathtt{at}(\mathtt{T})$ | $\mathtt{CmpAx}:\quad\hskip 0.5pt\vdash\hskip 0.5ptx=_{\rho}y\,\rightarrow\,A(x)\rightarrow A(y)$
---|---
Table 1: Basic axioms, with $\mathtt{CmpAx}$ replaced by $\mathtt{CMP}$ rule in $\sf NA_{\mathnormal{l}}$ $\hskip 0.5pta\\!:\\!A\hskip 0.5pt\hskip 0.5pt\vdash\hskip 0.5ptA\quad\mathrm{(id)}$ | tensy  $\displaystyle\penalty 1\Gamma,[\hskip 0.5pta\\!:\\!A\hskip 0.5pt]\hskip 0.5pt\vdash\hskip 0.5ptB$ $\ \mathnormal{\rightarrow^{\\!i}}$ $\displaystyle\Gamma\hskip 0.5pt\vdash\hskip 0.5ptA\rightarrow B$ | tensy  $\displaystyle\penalty 1\Gamma\hskip 0.5pt\vdash\hskip 0.5ptA\quad\Delta\hskip 0.5pt\vdash\hskip 0.5ptA\rightarrow B$ $\ \mathnormal{\rightarrow^{\\!e}}$ $\displaystyle\Gamma,\Delta\hskip 0.5pt\vdash\hskip 0.5ptB$ | tensy  $\displaystyle\penalty 1\Gamma\hskip 0.5pt\vdash\hskip 0.5ptA$ $\ \forall^{i}$ $\displaystyle\Gamma\hskip 0.5pt\vdash\hskip 0.5pt\forall zA$
---|---|---|---
tensy  $\displaystyle\penalty 1\Gamma\hskip 0.5pt\vdash\hskip 0.5ptA\land B$ $\ \mathnormal{\land^{\\!e}_{l}}$ $\displaystyle\Gamma\hskip 0.5pt\vdash\hskip 0.5ptA$ | tensy  $\displaystyle\penalty 1\Delta\hskip 0.5pt\vdash\hskip 0.5ptA\land B$ $\ \mathnormal{\land^{\\!e}_{r}}$ $\displaystyle\Delta\hskip 0.5pt\vdash\hskip 0.5ptB$ | tensy  $\displaystyle\penalty 1\Gamma\hskip 0.5pt\vdash\hskip 0.5ptA\quad\Delta\hskip 0.5pt\vdash\hskip 0.5ptB$ $\ \mathnormal{\land^{\\!i}}$ $\displaystyle\Gamma,\Delta\hskip 0.5pt\vdash\hskip 0.5ptA\land B$ | tensy  $\displaystyle\penalty 1\Gamma\hskip 0.5pt\vdash\hskip 0.5pt\forall zA$ $\ \forall^{e}$ $\displaystyle\Gamma\hskip 0.5pt\vdash\hskip 0.5ptA[t/z]$
Table 2: Logical rules, with $z\not\in{\sf FV}(\Gamma)$ at $\forall^{i}$ and certain explicit contractions at $\mathnormal{\rightarrow^{\\!e}}$ and $\mathnormal{\land^{\\!i}}$ tensy  $\displaystyle\penalty 1\Gamma\hskip 0.5pt\vdash\\!\\!\\!\raisebox{-2.58334pt}{\scriptsize$l$}\,A$ $\ \forall_{\\!\pm}^{i}$ $\displaystyle\Gamma\hskip 0.5pt\vdash\\!\\!\\!\raisebox{-2.58334pt}{\scriptsize$l$}\,\forall_{\\!\pm}zA$ | tensy  $\displaystyle\penalty 1\Gamma\hskip 0.5pt\vdash\\!\\!\\!\raisebox{-2.58334pt}{\scriptsize$l$}\,A$ $\ \forall_{\\!+}^{i}$ $\displaystyle\Gamma\hskip 0.5pt\vdash\\!\\!\\!\raisebox{-2.58334pt}{\scriptsize$l$}\,\forall_{\\!+}zA$ | tensy  $\displaystyle\penalty 1\Gamma\hskip 0.5pt\vdash\\!\\!\\!\raisebox{-2.58334pt}{\scriptsize$l$}\,A$ $\ \forall_{\\!-}^{i}$ $\displaystyle\Gamma\hskip 0.5pt\vdash\\!\\!\\!\raisebox{-2.58334pt}{\scriptsize$l$}\,\forall_{\\!-}zA$ | tensy  $\displaystyle\penalty 1\Gamma\hskip 0.5pt\vdash\\!\\!\\!\raisebox{-2.58334pt}{\scriptsize$l$}\,A$ $\ \forall_{\\!\emptyset}^{i}$ $\displaystyle\Gamma\hskip 0.5pt\vdash\\!\\!\\!\raisebox{-2.58334pt}{\scriptsize$l$}\,\forall_{\\!\emptyset}zA$
---|---|---|---
tensy  $\displaystyle\penalty 1\Gamma\hskip 0.5pt\vdash\\!\\!\\!\raisebox{-2.58334pt}{\scriptsize$l$}\,\forall_{\\!\pm}zA$ $\ \forall_{\\!\pm}^{e}$ $\displaystyle\Gamma\hskip 0.5pt\vdash\\!\\!\\!\raisebox{-2.58334pt}{\scriptsize$l$}\,A[t/z]$ | tensy  $\displaystyle\penalty 1\Gamma\hskip 0.5pt\vdash\\!\\!\\!\raisebox{-2.58334pt}{\scriptsize$l$}\,\forall_{\\!+}zA$ $\ \forall_{\\!+}^{e}$ $\displaystyle\Gamma\hskip 0.5pt\vdash\\!\\!\\!\raisebox{-2.58334pt}{\scriptsize$l$}\,A[t/z]$ | tensy  $\displaystyle\penalty 1\Gamma\hskip 0.5pt\vdash\\!\\!\\!\raisebox{-2.58334pt}{\scriptsize$l$}\,\forall_{\\!-}zA$ $\ \forall_{\\!-}^{e}$ $\displaystyle\Gamma\hskip 0.5pt\vdash\\!\\!\\!\raisebox{-2.58334pt}{\scriptsize$l$}\,A[t/z]$ | tensy  $\displaystyle\penalty 1\Gamma\hskip 0.5pt\vdash\\!\\!\\!\raisebox{-2.58334pt}{\scriptsize$l$}\,\forall_{\\!\emptyset}zA$ $\ \forall_{\\!\emptyset}^{e}$ $\displaystyle\Gamma\hskip 0.5pt\vdash\\!\\!\\!\raisebox{-2.58334pt}{\scriptsize$l$}\,A[t/z]$
Table 3: Additional rules for $\sf NA_{\mathnormal{l}}\hskip 0.5pt,$ with extra restrictions on $\forall_{\\!+}^{i}\hskip 0.5pt,$ $\forall_{\\!-}^{i}$ and $\forall_{\\!\emptyset}^{i}$ tensy  $\displaystyle\penalty 1\Delta,\hskip 0.5pta\\!:\\!A\hskip 0.5pt,\hskip 0.5pta\\!:\\!A\hskip 0.5pt\hskip 0.5pt\vdash\hskip 0.5ptB$ C $\displaystyle\Delta,\hskip 0.5pta\\!:\\!A\hskip 0.5pt\hskip 0.5pt\vdash\hskip 0.5ptB$ | tensy  $\displaystyle\penalty 1\Delta,\hskip 0.5pta\\!:\\!A\hskip 0.5pt,\hskip 0.5pta\\!:\\!A\hskip 0.5pt\hskip 0.5pt\vdash\\!\\!\\!\raisebox{-2.58334pt}{\scriptsize$l$}\,B$ $\mathcal{C}_{l}$ $\displaystyle\Delta,\hskip 0.5pta\\!:\\!A\hskip 0.5pt\hskip 0.5pt\vdash\\!\\!\\!\raisebox{-2.58334pt}{\scriptsize$l$}\,B$
---|---
Table 4: Contraction anti-rules C for ${\sf NA}$ and (restricted) $\mathcal{C}_{l}$ for $\sf NA_{\mathnormal{l}}$ tensy  $\displaystyle\penalty 1\Gamma\hskip 0.5pt\vdash\hskip 0.5ptA(\mathtt{T})\quad\Delta\hskip 0.5pt\vdash\hskip 0.5ptA(\mathtt{F})$ $\ \mathtt{Ind}_{o}$ $\displaystyle\Gamma,\Delta\hskip 0.5pt\vdash\hskip 0.5ptA(b)$ | tensy  $\displaystyle\penalty 1\Gamma\hskip 0.5pt\vdash\hskip 0.5ptA(\mathtt{0})\quad\Delta\hskip 0.5pt\vdash\hskip 0.5ptA(n)\rightarrow A(\mathtt{S}n)$ $\ \mathtt{Ind}_{\iota}$ $\displaystyle\Gamma,\Delta\hskip 0.5pt\vdash\hskip 0.5ptA(n)$
---|---
Table 5: Induction rules, with $\Gamma\uplus\Delta$ instead of
‘$\Gamma,\Delta$’ and $\Delta$ restricted at $\mathtt{Ind}_{\iota}$ of $\sf
NA_{\mathnormal{l}}$

##  5 Appendix

We use a special Natural Deduction (abbreviated “ND”) presentation of our
systems, where proofs are represented as sequents $\Gamma\hskip
0.5pt\vdash\hskip 0.5ptB\hskip 0.5pt,$ meaning that formula $B$ is the root of
the ND tree whose leaves $\Gamma$ are typed assumption variables (abbreviated
“avars”) $\hskip 0.5pta\\!:\\!A\hskip 0.5pt\hskip 0.5pt.$ Here formula $A$ is
the type of the avar $a\hskip 0.5pt,$ and $\Gamma$ is a multiset (since there
may be more leaves labeled with the same $\hskip 0.5pta\\!:\\!A\hskip 0.5pt$).

###  5.1 The verifying system ${\sf NA}$

The logical rules of system ${\sf NA}$ are presented in Table 2 , with the
usual restriction on universal quantifier introduction $\forall^{i}$ that

$\begin{array}[]{rcl}z&\not\in&{\sf FV}(\Gamma)\hskip 1.0pt\mathnormal{\
:\equiv\ }\bigcup_{\hskip 0.5pta:A\hskip 0.5pt\in\Gamma}{\sf
FV}(A)\end{array}$

At $\mathnormal{\rightarrow^{\\!i}}\hskip 0.5pt,$ $[\hskip
0.5pta\\!:\\!A\hskip 0.5pt]$ denotes the multisubset of all occurrences of
$\hskip 0.5pta\\!:\\!A\hskip 0.5pt$ in the multiset of assumptions of the
premise sequent of $\mathnormal{\rightarrow^{\\!i}}\hskip 0.5pt.$ Thus $\hskip
0.5pta\\!:\\!A\hskip 0.5pt\not\in\Gamma\hskip 0.5pt,$ hence $\hskip
0.5pta\\!:\\!A\hskip 0.5pt$ is no longer an assumption in the conclusion
sequent of $\mathnormal{\rightarrow^{\\!i}}\hskip 0.5pt.$ In the ND tree, this
means that all the leaves labeled $\hskip 0.5pta\\!:\\!A\hskip 0.5pt$ are
inactivated (or “discharged” as one usually says in Natural Deduction
terminology).

Whereas in ${\sf NA}$ alone we could have safely let all contractions be
handled implicitly at $\mathnormal{\rightarrow^{\\!i}}\hskip 0.5pt,$ in
relationship with the architecture of input system $\sf NA_{\mathnormal{l}}$
(see Section 5.2) we are compelled to introduce for ${\sf NA}$ the
_contraction anti-rule_ C in association with $\mathcal{C}_{l}$ of $\sf
NA_{\mathnormal{l}}$, see Table 4. We refer to contraction as “anti-rule”,
rather than “rule” because, despite the sequent-like representation of our
calculi, in fact our formalisms are ND and in the ND directed tree the
representation of explicit contractions is by convergent arrows that go in the
direction which is reverse to the direction of all the other rules.

We find it convenient to introduce induction for booleans and naturals as the
rules presented in Table 5 . Here we assume that the induction variables
$b^{o}$ and respectively $n^{\iota}$ do not occur freely in $\Gamma\hskip
0.5pt,$ nor $\Delta\hskip 0.5pt,$ and that they do occur in the formula
$A\hskip 0.5pt.$

Computation in ${\sf NA}$ is expressed via the usual $\beta$-reduction rule
$(\lambda x.t)s\hookrightarrow t[x\mapsto s]\hskip 0.5pt,$ plus rewrite rules
defining the computational meaning of $\mathtt{If}$ and $\mathtt{R}\hskip
0.5pt:$

$\begin{array}[]{rlrl}\mathtt{If}\,\mathtt{T}\,s\,t&\hookrightarrow\;s&\qquad\qquad\mathtt{R}\,\mathtt{0}\,s\,t&\hookrightarrow\;s\\\\[2.0pt]
\mathtt{If}\,\mathtt{F}\,s\,t&\hookrightarrow\;t&\qquad\qquad\mathtt{R}\,(\mathtt{S}n)\,s\,t&\hookrightarrow\;t\,n\,(\mathtt{R}\,n\,s\,t)\end{array}$

Since this typed term system is confluent and strongly normalizing (cf. [17]),
we are free not to fix a particular evaluation strategy. For simplicity, we
assume that all terms occurring in proofs are automatically in normal form. In
fact, normalization is necessary only when matching terms in formulas. We only
avoid introducing equality axioms $\mathtt{AxEQL}$ as in [7] and skip the
corresponding easy applications of $\mathtt{CmpAx}$. When building proofs,
some computation is thus carried out implicitly, behind the scene.

Using recursion at higher types we can define any provably total function of
ground arithmetic, including decidable predicates such as equality
$\mathtt{Eq}_{\hskip 0.5pto}$ for booleans and $\mathtt{Eq}_{\hskip
0.5pt\iota}$ for natural numbers:

$\begin{array}[]{r@{\ \;}c@{\ \;}l}\mathtt{Eq}_{\hskip
0.5pto}^{ooo}&\mathnormal{\hskip 0.5pt:\equiv\hskip 0.5pt}&\lambda
x.\mathtt{If}\,x\,(\lambda y.y)\,(\lambda
y.\mathtt{If}\,y\,\mathtt{F}\,\mathtt{T})\\\\[3.0pt] \mathtt{Eq}_{\hskip
0.5pt\iota}^{\iota\iota o}&\mathnormal{\hskip 0.5pt:\equiv\hskip
0.5pt}&\lambda x.\mathtt{R}\,x\,\big{(}\lambda
y.\mathtt{R}\,y\,\mathtt{T}\,(\lambda
n,q^{o}.\mathtt{F})\big{)}\,\big{(}\lambda m,p^{\iota
o},y.\mathtt{R}\,y\,\mathtt{F}\,(\lambda n,q^{o}.p\,n)\big{)}\end{array}$

The $\mathtt{at}(\cdot)$ construction allows us to view boolean programs as
decidable predicates. Given $\mathtt{Ind}_{o}\hskip 0.5pt,$ its logical
meaning is settled by the truth axiom $\mbox{$\mathtt{T}\mathtt{Ax}$}\hskip
0.5pt,$ see Table 1 . In this way we can define predicate equality at base
types as $s=_{\sigma}t\ \mathnormal{\hskip 0.5pt:\equiv\hskip 0.5pt}\
\mathtt{at}(\mathtt{Eq}\,s\,t)$ for $\sigma\in\left\\{o,\iota\right\\}$ and
further at higher types extensionally as usual $s=_{\rho\tau}t\
\mathnormal{\hskip 0.5pt:\equiv\hskip 0.5pt}\forall
x^{\rho}(sx=_{\tau}tx)\hskip 0.5pt.$ It is straightforward to prove by
induction on $\rho$ that $=_{\rho}$ is reflexive, symmetric and transitive at
any type $\rho\hskip 0.5pt.$

To complete our system, we must include in ${\sf NA}$ also the compatibility
(i.e., extensionality) axiom $\mathtt{CmpAx}\hskip 0.5pt,$ see Table 1 . Note
that ex falso quodlibet ($\mathtt{EFQ}$) $\hskip 0.5pt\bot\rightarrow A\hskip
1.0pt$ and stability ($\mathtt{Stab}$) $\hskip 0.5pt\lnot\lnot A\hskip
0.5pt\rightarrow\hskip 0.5ptA\hskip 1.0pt$ are fully provable in ${\sf NA}$
(cf. [17], by induction on $A\hskip 0.5pt,$ using $\mathtt{T}\mathtt{Ax}$ and
$\mathtt{Ind}_{o}$).

###  5.2 The input system $\sf NA_{\mathnormal{l}}$

Light formulas $\mathcal{F}_{l}$ are built over usual formulas $\mathcal{F}$
of ${\sf NA}$ by adding the three light universal quantifiers: the non-
computational $\forall_{\\!\emptyset}$ and the two semi-computational
$\forall_{\\!+}$ and $\forall_{\\!-}\hskip 0.5pt.$ In order to stress the
distinction of $\sf NA_{\mathnormal{l}}$ from ${\sf NA}$ it is convenient to
rename ${\sf NA}$’s $\forall$ to $\forall_{\\!\pm}$ in $\sf
NA_{\mathnormal{l}}$ (which marks the whole computational content, both
positive and negative)

$\displaystyle\mathcal{F}_{l}\quad$ $\displaystyle A,B$ $\displaystyle\
\mathtt{::=}\quad\mathtt{at}(t^{o})\;|\;A\rightarrow B\;|\;A\land
B\;|\;\forall_{\diamond}\,x^{\rho}A\quad\text{ for
}\diamond\in\left\\{\emptyset,+,-,\pm\right\\}$

Thus, system $\sf NA_{\mathnormal{l}}$ refines the clone of ${\sf NA}$ (also
with $\mathtt{CMP}$ for $\mathtt{CmpAx}$ and $\mathcal{C}_{l}$ for C) with
introduction and elimination rules for the light quantifiers (see Table 3).
These are copies of the clone rules $\forall_{\\!\pm}^{e}$ and
$\forall_{\\!\pm}^{i}\hskip 0.5pt,$ but with the usual restriction ($\pm$) on
$\forall_{\\!\pm}^{i}$ that $z\not\in{\sf FV}(\Gamma)$ enhanced with the
following conditions referring to the LD-interpretation

  * ($+$)

at the $\forall_{\\!+}^{i}$ rule, $z$ may be used computationally only
positively, i.e.,
$z$ must not be free in the _challengers_ of the LD-translation of
$\Gamma\hskip 0.5pt\hskip 0.5pt.$

  * ($-$)

at the $\forall_{\\!-}^{i}$ rule, $z$ may be used computationally only
negatively, i.e.,
$z$ must not be free in the _witnesses_ of the LD-translation of $A\hskip
0.5pt\hskip 0.5pt.$

  * ($\emptyset$)

at $\forall_{\\!\emptyset}^{i}\hskip 0.5pt,$ $z$ may not be used
computationally at all, i.e., both ($+$) and ($-$).

Notice that the restrictions ($+$), ($-$) and ($\emptyset$) assume knowledge
of the LD-interpretation of whole proofs, in their full depth, thus forcing
the definition of $\sf NA_{\mathnormal{l}}$ proofs to go inductively in
parallel with the LD-extraction of part of their computational content (namely
free variables of the extracted terms). We simultaneously define the classes
of _realization irrelevant_ $A_{\oplus}$ and _refutation irrelevant_
$A_{\ominus}$ formulas as follows:

$\displaystyle A_{\oplus},B_{\oplus}$ $\displaystyle\ \mathtt{::=}\quad$
$\displaystyle\mathtt{at}(t)\;|\;A_{\oplus}\land
B_{\oplus}\;|\;A_{\ominus}\rightarrow B_{\oplus}\;|\;\forall_{\diamond}x\hskip
1.0ptA_{\oplus}\quad\text{ for }\diamond\in\left\\{\emptyset,+,-,\pm\right\\}$
$\displaystyle A_{\ominus},B_{\ominus}$ $\displaystyle\ \mathtt{::=}\quad$
$\displaystyle\mathtt{at}(t)\;|\;A_{\ominus}\land
B_{\ominus}\;|\;A_{\oplus}\rightarrow
B_{\ominus}\;|\;\forall_{\diamond}x\hskip 1.0ptA_{\ominus}\quad\text{ for
}\diamond\in\left\\{\emptyset,+\right\\}$

One necessary change when adopting principles from ${\sf NA}$ is to replace
$\mathtt{CmpAx}$ with a weak compatibility rule. This is because Dialectica is
unable to interpret full extensionality (cf. [11, 20]). We here employ an
upgraded variant of the $\mathtt{CMP}$ rule from [7]:

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
14.41693pt\hbox{$\displaystyle\penalty 1\Gamma_{\ominus}\hskip
0.5pt\vdash\\!\\!\\!\raisebox{-2.58334pt}{\scriptsize$l$}\,s=_{\rho}t$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=72.24852pt\hbox{\kern 3.00003pt$\
\mathtt{CMP}_{\rho}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma_{\ominus}\hskip
0.5pt\vdash\\!\\!\\!\raisebox{-2.58334pt}{\scriptsize$l$}\,B(s)\rightarrow
B(t)$}}}}$

where all formulas in $\Gamma_{\ominus}$ are refutation irrelevant.

The computationally irrelevant contractions in $\sf NA_{\mathnormal{l}}$ can
safely be handled implicitly at $\mathnormal{\rightarrow^{\\!i}}\hskip 0.5pt.$
The situation is different for those contractions whose formula is refutation
relevant (i.e., the computationally relevant contractions), as we want to
automatically ensure that their translation is decidable (instead of leaving
the task of decidability check to the user). We achieve this by including in
$\sf NA_{\mathnormal{l}}$ the _contraction anti-rule_ $\mathcal{C}_{l}$ (see
Table 4) for all formulas $A$ that are refutation relevant and ($\bigstar$) do
not contain any $\forall_{\\!+}\hskip 0.5pt,$ nor
$\forall_{\\!\emptyset}\hskip 0.5pt.$ This triggers the addition to ${\sf NA}$
of an explicit (unrestricted) contraction anti-rule C which is needed in the
construction of the verifying proof (it only applies to quantifier-free
formulas $|A|$). The restriction $\bigstar$ ensures that all contraction
formulas that require at least one challenger term for their LD-interpretation
will have quantifier-free (hence decidable) LD-translations. Their
decidability is necessary for attaining soundness. Being a purely syntactical
criterion, $\bigstar$ does not admit formulas whose LD-translations contain
quantifiers, but could nevertheless be decidable, e.g.,
$\mathtt{Odd}(x)\mathnormal{\;\equiv\;}\forall y(2y\neq x)\hskip 0.5pt.$

Moreover, in order to avoid having any computationally relevant contractions
implicit in $\mathnormal{\rightarrow^{\\!i}}\hskip 0.5pt,$ we constrain the
deduction rules of $\sf NA_{\mathnormal{l}}$ to disallow multiple occurrences
of refutation relevant assumptions in any of the premise sequents. Thus,
whenever a double occurrence of a refutation relevant assumption is created in
a conclusion sequent by one of the binary rules of $\sf
NA_{\mathnormal{l}}\hskip 0.5pt,$ such sequent cannot be directly a premise
for the application of an(other) $\sf NA_{\mathnormal{l}}$ rule: the anti-rule
$\mathcal{C}_{l}$ must be applied first, in order to eliminate the critical
double. If $\bigstar$ is not satisfied and yet $\hskip 0.5pta\\!:\\!A\hskip
0.5pt$ is a refutation relevant assumption occurring at least twice in some
conclusion sequent, this is a dead end: such sequent can only be the root of
the $\sf NA_{\mathnormal{l}}$ proof-tree.

While $\hskip 1.0pt\mathtt{EFQ}:\,\bot\hskip 0.5pt\rightarrow\hskip
0.5ptA\hskip 1.0pt$ remains fully provable also in $\sf NA_{\mathnormal{l}}$
(for all formulas $A\in\mathcal{F}_{l}$) the situation changes for $\hskip
1.0pt\mathtt{Stab}:\,\lnot\lnot A\hskip 0.5pt\rightarrow\hskip 0.5ptA\hskip
1.0pt$ in the case of many formulas $A$ that feature light quantifiers in
certain places. As noted in [7], the usual proof in ${\sf NA}$ of
$\mathtt{Stab}$ (constructed by induction on $A$) makes unavoidably use of
contractions over $\neg\neg(B\land C)$ for subformulas $(B\land C)$ of
$A\hskip 0.5pt,$ and these are subject to the $\bigstar$ restriction for
refutation relevant $B\land C\hskip 0.5pt.$ Even when such $B\land C$ obey
$\bigstar$, they may lead to the failure of restrictions ($+$), ($-$) or
($\emptyset$). On the other hand $\mathtt{Stab}$ is provable in $\sf
NA_{\mathnormal{l}}$ for $A\in\mathcal{F}$ or $A$ conjunction-free.

###  5.3 The light Dialectica interpretation (LD-interpretation)

With each formula $A$ of $\sf NA_{\mathnormal{l}}$ we associate its LD-
translation: a not necessarily quantifier-free formula
$|A|^{\boldsymbol{x}}_{\boldsymbol{y}}$ of ${\sf NA}$ where
$\boldsymbol{x},\boldsymbol{y}$ are tuples of fresh variables, not appearing
in $A\hskip 0.5pt.$ The variables $\boldsymbol{x}$ in the superscript are
called the _witness variables_ , while the subscript variables
$\boldsymbol{y}$ are called the _challenge variables_. Terms $\boldsymbol{t}$
substituting witness variables (like $|A|^{\boldsymbol{t}}_{\boldsymbol{y}}$)
are called _realizing terms_ or “witnesses” and terms $\boldsymbol{s}$
substituting challenge variables (like
$|A|^{\boldsymbol{x}}_{\boldsymbol{s}}$) are called _refuting terms_ or
“challengers”. Intuitively, the LD-interpretation of $A$ can be viewed as a
game in which first Eloise ($\exists$) and then Abelard ($\forall$) make one
move each by playing type-corresponding objects $\boldsymbol{t}$ and
$\boldsymbol{s}$ for the tuples $\boldsymbol{x}$ and respectively
$\boldsymbol{y}\hskip 0.5pt.$ Formula $|A|^{\boldsymbol{x}}_{\boldsymbol{y}}$
specifies the “adjudication relation”, here not necessarily decidable: Eloise
wins iff $\,{\sf NA}\hskip 0.5pt\vdash\hskip
0.5pt|A|^{\boldsymbol{t}}_{\boldsymbol{s}}\hskip 0.5pt\hskip 0.5pt.$ In our
light context as well, Eloise has a winning move whenever $A$ is provable in
$\sf NA_{\mathnormal{l}}\hskip 0.5pt:$ the LD-interpretation will explicitly
provide it from the input $\sf NA_{\mathnormal{l}}$ proof of $A$ as a tuple of
witnesses $\boldsymbol{t}$ (s.t. ${\sf FV}(\boldsymbol{t})\subseteq{\sf
FV}(A)$) together with the _verifying proof_ in ${\sf NA}$ of $\hskip
1.0pt\forall\boldsymbol{y}\hskip
0.5pt|A|^{\boldsymbol{t}}_{\boldsymbol{y}}\hskip 0.5pt$ (Eloise wins by
$\boldsymbol{t}$ regardless of the instances $\boldsymbol{s}$ for Abelard’s
$\boldsymbol{y}$).

######  Definition 5 (LD-translation of formulas)

The interpretation does not change atomic formulas, i.e.,
$|\mathtt{at}(t^{o})|\mathnormal{\hskip 0.5pt:\equiv\hskip
0.5pt}\mathtt{at}(t^{o})\hskip 0.5pt.$ Assuming
$|A|^{\boldsymbol{x}}_{\boldsymbol{y}}$ and
$|B|^{\boldsymbol{u}}_{\boldsymbol{v}}$ are already defined,

$\begin{array}[]{r@{\quad}c@{\quad}l}|A\land
B|^{\boldsymbol{x},\boldsymbol{u}}_{\boldsymbol{y},\boldsymbol{v}}&\mathnormal{\hskip
0.5pt:\equiv\hskip
0.5pt}&|A|^{\boldsymbol{x}}_{\boldsymbol{y}}\land|B|^{\boldsymbol{u}}_{\boldsymbol{v}}\\\\[6.0pt]
|A\rightarrow
B|^{\boldsymbol{f},\boldsymbol{g}}_{\boldsymbol{x},\boldsymbol{v}}&\mathnormal{\hskip
0.5pt:\equiv\hskip
0.5pt}&|A|^{\boldsymbol{x}}_{\boldsymbol{f}\boldsymbol{x}\boldsymbol{v}}\rightarrow|B|^{\boldsymbol{g}\boldsymbol{x}}_{\boldsymbol{v}}\quad.\end{array}$

The interpretation of the four universal quantifiers is (upon renaming, we
assume that quantified variables occur uniquely in a formula):

$\begin{array}[]{l@{\quad}c@{\quad}l@{\qqquad}l@{\quad}c@{\quad}l}|\forall_{\\!\pm}z\hskip
1.0ptA(z)|^{\boldsymbol{f}}_{z,\boldsymbol{y}}&\mathnormal{\hskip
0.5pt:\equiv\hskip
0.5pt}&|A(z)|^{\boldsymbol{f}z}_{\boldsymbol{y}}\hfil\qquad\quad&|\forall_{\\!+}z\hskip
1.0ptA(z)|^{\boldsymbol{f}}_{\boldsymbol{y}}&\mathnormal{\hskip
0.5pt:\equiv\hskip 0.5pt}&\forall z\hskip
1.0pt|A(z)|^{\boldsymbol{f}z}_{\boldsymbol{y}}\\\\[6.0pt]
|\forall_{\\!-}z\hskip
1.0ptA(z)|^{\boldsymbol{x}}_{z,\boldsymbol{y}}&\mathnormal{\hskip
0.5pt:\equiv\hskip
0.5pt}&|A(z)|^{\boldsymbol{x}}_{\boldsymbol{y}}\hfil\qquad\quad&|\forall_{\\!\emptyset}z\hskip
1.0ptA(z)|^{\boldsymbol{x}}_{\boldsymbol{y}}&\mathnormal{\hskip
0.5pt:\equiv\hskip 0.5pt}&\forall z\hskip
1.0pt|A(z)|^{\boldsymbol{x}}_{\boldsymbol{y}}\end{array}$

Since $|\bot|\mathnormal{\hskip 0.5pt\equiv\hskip 0.5pt}\bot\hskip 0.5pt,$ we
get

$\begin{array}[]{l@{\quad}c@{\quad}l@{\qqquad}l@{\quad}c@{\quad}l}|\lnot
A|^{\boldsymbol{f}}_{\boldsymbol{x}}&\mathnormal{\hskip 0.5pt\equiv\hskip
0.5pt}&\lnot|A|^{\boldsymbol{x}}_{\boldsymbol{f}\boldsymbol{x}}\hfil\qquad\quad&|\lnot\lnot
A|^{\boldsymbol{f}}_{\boldsymbol{g}}&\mathnormal{\hskip 0.5pt\equiv\hskip
0.5pt}&\lnot\lnot|A|^{\boldsymbol{f}\boldsymbol{g}}_{\boldsymbol{g}(\boldsymbol{f}\boldsymbol{g})}\end{array}$

It is straightforward to compute that

$\begin{array}[]{l@{\ }c@{\ }l@{\qquad}l@{\ }c@{\
}l}|\widetilde{\exists}_{\pm}z\hskip
1.0ptA(z)|^{Z,\boldsymbol{f}}_{\boldsymbol{g}}&\mathnormal{\hskip
0.5pt:\equiv\hskip
0.5pt}&\lnot\lnot|A(Z\boldsymbol{g})|^{\boldsymbol{f}\boldsymbol{g}}_{\boldsymbol{g}(Z\boldsymbol{g})(\boldsymbol{f}\boldsymbol{g})}&|\widetilde{\exists}_{+}z\hskip
1.0ptA(z)|^{\boldsymbol{f}}_{\boldsymbol{g}}&\mathnormal{\hskip
0.5pt:\equiv\hskip 0.5pt}&\widetilde{\exists}z\hskip
1.0pt|A(z)|^{\boldsymbol{f}\boldsymbol{g}}_{\boldsymbol{g}z(\boldsymbol{f}\boldsymbol{g})}\\\\[6.0pt]
|\widetilde{\exists}_{-}z\hskip
1.0ptA(z)|^{Z,\boldsymbol{f}}_{\boldsymbol{g}}&\mathnormal{\hskip
0.5pt:\equiv\hskip
0.5pt}&\lnot\lnot|A(Z\boldsymbol{g})|^{\boldsymbol{f}\boldsymbol{g}}_{\boldsymbol{g}(\boldsymbol{f}\boldsymbol{g})}&|\widetilde{\exists}_{\emptyset}z\hskip
1.0ptA(z)|^{\boldsymbol{f}}_{\boldsymbol{g}}&\mathnormal{\hskip
0.5pt:\equiv\hskip 0.5pt}&\widetilde{\exists}z\hskip
1.0pt|A(z)|^{\boldsymbol{f}\boldsymbol{g}}_{\boldsymbol{g}(\boldsymbol{f}\boldsymbol{g})}\end{array}$

The length and types of the witnessing and challenging tuples are uniquely
determined.

###  5.4 Light Dialectica treatment of extensionality

We here give the LD-interpretation of the weak compatibility rule

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
14.41693pt\hbox{$\displaystyle\penalty 1\Gamma_{\ominus}\hskip
0.5pt\vdash\\!\\!\\!\raisebox{-2.58334pt}{\scriptsize$l$}\,s=_{\rho}r$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=73.42677pt\hbox{\kern 3.00003pt$\
\mathtt{CMP}_{\rho}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma_{\ominus}\hskip
0.5pt\vdash\\!\\!\\!\raisebox{-2.58334pt}{\scriptsize$l$}\,B(s)\rightarrow
B(r)$}}}}$

where all formulas in $\Gamma_{\ominus}$ are refutation irrelevant, i.e., the
negative position in their LD-translation is empty. By definition of equality
at higher types, $s=_{\rho}r$ is
$\forall\boldsymbol{z}.\,s\boldsymbol{z}=r\boldsymbol{z}$, a purely universal
formula. We are given that

$\begin{array}[]{rcl}\hskip
0.5pta_{1}\\!:\\!|A_{1}|^{\boldsymbol{x}_{1}}_{\boldsymbol{t}_{1}}\hskip
0.5pt,\ldots,\hskip
0.5pta_{n}\\!:\\!|A_{n}|^{\boldsymbol{x}_{n}}_{\boldsymbol{t}_{n}}&\hskip
0.5pt\vdash&|A_{0}|^{\boldsymbol{t}_{0}}_{\boldsymbol{x}_{0}}\end{array}$

where $|\Gamma_{\ominus}|\mathnormal{\hskip 0.5pt\equiv\hskip
0.5pt}\left\\{a_{1},\ldots,a_{n}\right\\}$,
$\boldsymbol{t}_{0}\mathnormal{\hskip 0.5pt\equiv\hskip
0.5pt}\boldsymbol{t}_{1}\mathnormal{\hskip 0.5pt\equiv\hskip
0.5pt}\ldots\boldsymbol{t}_{n}\mathnormal{\hskip 0.5pt\equiv\hskip
0.5pt}\sqcup$ (empty tuple), $A_{0}$ is $s=_{\rho}r$ and $\boldsymbol{x}_{0}$
corresponds to $\boldsymbol{z}$, thus the above is more conveniently rewritten
as

$\begin{array}[]{rcl}\hskip
0.5pta_{1}\\!:\\!|A_{1}|^{\boldsymbol{x}_{1}}\hskip 0.5pt,\ldots,\hskip
0.5pta_{n}\\!:\\!|A_{n}|^{\boldsymbol{x}_{n}}&\hskip
0.5pt\vdash&s\boldsymbol{x}_{0}=r\boldsymbol{x}_{0}\end{array}$

To this we can apply the generalization rule, as $\boldsymbol{x}_{0}$ are not
free in the translated context $|\Gamma_{\ominus}|$; indeed,
$\boldsymbol{x}_{0}$ are fresh variables and they could have appeared free
only via terms $\boldsymbol{t}_{1}$,…,$\boldsymbol{t}_{n}$, were these not
empty tuples (hence the need for restricting the original context). We thus
obtain $|\Gamma_{\ominus}|\,\hskip 0.5pt\vdash\hskip 0.5pt\,s=r$ and further
apply the extensionality Axiom to get $|\Gamma_{\ominus}|\,\hskip
0.5pt\vdash\hskip 0.5pt\,|B|(s)\rightarrow|B|(r)$. Note that the Axiom is
required here, as $|\Gamma_{\ominus}|$ may contain general formulas. With
$g\mathnormal{\ :\equiv\ }\lambda\boldsymbol{u}.\,\boldsymbol{u}$ and
$f\mathnormal{\ :\equiv\
}\lambda\boldsymbol{u},\boldsymbol{v}.\,\boldsymbol{v}$ we have thus
constructed a verifying proof

$\begin{array}[]{rcl}\hskip
0.5pta_{1}\\!:\\!|A_{1}|^{\boldsymbol{x}_{1}}\hskip 0.5pt,\ldots,\hskip
0.5pta_{n}\\!:\\!|A_{n}|^{\boldsymbol{x}_{n}}&\hskip
0.5pt\vdash&|B(s)|^{\boldsymbol{u}}_{f\boldsymbol{u}\boldsymbol{v}}\rightarrow|B(r)|^{g\boldsymbol{u}}_{\boldsymbol{v}}\
\,[\,\mathnormal{\hskip 0.5pt\equiv\hskip 0.5pt}\ \,|B(s)\rightarrow
B(r)|^{f,g}_{\boldsymbol{u},\boldsymbol{v}}\,]\end{array}$

The new realizing terms $f,g$ are closed, hence the free variable condition
trivially holds.

###  5.5 Light Dialectica treatment of induction for naturals

Since the induction rule (for naturals) corresponds to a virtually unbounded
number of contractions of each assumption from the step context $\Delta$ (cf.
[7], see Table 5), its clone in the system $\sf NA_{\mathnormal{l}}$ is
subject to a restriction like the one of $\mbox{$\mathcal{C}_{l}$}\hskip
0.5pt.$ Namely, we need to require that all refutation relevant avars in
$\Delta$ satisfy $\bigstar$. Moreover, since the contractions on
$a\in\Gamma\cap\Delta$ will be handled differently than for simple binary
rules like $\mathnormal{\rightarrow^{\\!e}}$ or
$\mathnormal{\land^{\\!i}}\hskip 0.5pt,$ it is more convenient to require that
naturals induction in $\sf NA_{\mathnormal{l}}$ implicitly contracts all its
refutation relevant assumptions (instead of using the explicit
$\mathcal{C}_{l}$) . We will use the notation $\Gamma\uplus\Delta$ for a
special multiset union in which refutation relevant assumptions appear only
once, even if they appear in both $\Gamma$ and $\Delta\hskip 0.5pt.$ Thus the
$\mathtt{Ind^{\iota}_{\mathnormal{l}}}$ rule of $\sf NA_{\mathnormal{l}}$ is
finally obtained by replacing ‘$\Gamma,\Delta$’ with ‘$\Gamma\uplus\Delta$’ in
the conclusion sequent of $\mathtt{Ind}_{\iota}\hskip 0.5pt.$

tensy  $\displaystyle\penalty 1\Gamma\ \hskip
0.5pt\vdash\\!\\!\\!\raisebox{-2.58334pt}{\scriptsize$l$}\,\
A(\mathtt{0})\qquad\Delta\ \hskip
0.5pt\vdash\\!\\!\\!\raisebox{-2.58334pt}{\scriptsize$l$}\,\
A(n)\;\rightarrow\;A(\mathtt{S}n)$ $\ {\
\mathtt{Ind^{\iota}_{\mathnormal{l}}}}$ $\displaystyle\Gamma\uplus\Delta\
\hskip 0.5pt\vdash\\!\\!\\!\raisebox{-2.58334pt}{\scriptsize$l$}\,\ A(n)$
---

We are given

$\displaystyle|\Gamma|^{\boldsymbol{u}}_{\boldsymbol{\gamma}[\boldsymbol{y}]}$
$\displaystyle\hskip 0.5pt\vdash\hskip 0.5pt$
$\displaystyle|A(\mathtt{0})|^{\boldsymbol{r}}_{\boldsymbol{y}}$ (6)

and

$\displaystyle|\Delta|^{\boldsymbol{z}}_{\boldsymbol{\delta}[\boldsymbol{x};\boldsymbol{v}]}$
$\displaystyle\hskip 0.5pt\vdash\hskip 0.5pt$
$\displaystyle|A(n)|^{\boldsymbol{x}}_{\boldsymbol{t}\boldsymbol{x}\boldsymbol{v}}\
\rightarrow\ |A(\mathtt{S}n)|^{\boldsymbol{s}\boldsymbol{x}}_{\boldsymbol{v}}$
(7)

We show that

$\displaystyle\forall\boldsymbol{v}\hskip
1.0pt\big{(}\,|\Gamma\uplus\Delta|^{\,\boldsymbol{u}\uplus\boldsymbol{z}}_{\,\boldsymbol{\zeta}[n]\boldsymbol{v}}\;\rightarrow\;|A(n)|^{\boldsymbol{{t}^{\prime}}[n]}_{\boldsymbol{v}}\,\big{)}$
(8)

is a theorem of $\ {\sf NA}$ , where

$\displaystyle{t}^{\prime}[n]$ $\displaystyle\mathnormal{\ :\equiv\ }$
$\displaystyle\mathtt{R}\,n\,r\,(\lambda n.s)$ (9)

for every corresponding pair $\,\langle
r\in\boldsymbol{r}/s\in\boldsymbol{s}\rangle\,$ and
$\,\boldsymbol{\zeta}[n]\,$ will be constructed as functional terms depending
on $\,\boldsymbol{v}$ . We here intentionally use the same variable $\,n\,$
that occurs freely in $\,s\,$ and $\,t$ . Implicitly, just $\,{t}^{\prime}\,$
denotes $\,{t}^{\prime}[n]$ . Also $\,\boldsymbol{\zeta}\,$ will be
constructed as the collection of all $\,\boldsymbol{{\zeta}^{\prime}}\,$
(corresponding to $\,\Gamma\setminus\Delta\,$) and
$\,\boldsymbol{{\zeta}^{\prime\prime}}\,$ (corresponding to $\,\Delta\,$).

Let $\,\hskip 0.5ptb\\!:\\!B\hskip 0.5pt\,$ be a refutation relevant avar in
$\,\Gamma\uplus\Delta$ . Let
$\,\boldsymbol{{\gamma}^{\prime}}\in\boldsymbol{\gamma}\,$ and/or
$\,\boldsymbol{{\delta}^{\prime}}\in\boldsymbol{\delta}\,$ be the challengers
for $\;b\;$ in $\;\Gamma\;$ and/or $\,\Delta$ . If $\;b\;$ appears only in
$\,\Gamma\,$ (hence not in $\,\Delta\,$) we define

$\displaystyle\boldsymbol{{\zeta}^{\prime}}[n]$
$\displaystyle\mathnormal{\hskip 0.5pt:\equiv\hskip 0.5pt}$
$\displaystyle\mathtt{R}\,n\,(\lambda\boldsymbol{v}.\boldsymbol{{\gamma}^{\prime}}[\boldsymbol{v}])\,\big{(}\lambda
n,p,\boldsymbol{v}.p(\boldsymbol{t}\,\boldsymbol{{t}^{\prime}}\boldsymbol{v})\big{)}$
(10)

If $\ b\ $ appears in $\ \Delta$ , then the decidability of $\ |B|\ $ is
needed at each recursive step to equalize the terms $\
p(\boldsymbol{t}\,\boldsymbol{{t}^{\prime}}\boldsymbol{v})\ $ obtained by the
recursive call with the corresponding terms
$\boldsymbol{{\delta}^{\prime}}\hskip 0.5pt.$ Thus the right stop point of the
backwards construction is provided. In fact an implicit contraction over
$\,b\,$ happens at each inductive step and  $\bigstar$ guarantees that
$\,|B|\,$ is decidable. For $\ b\in\Gamma\cap\Delta\ $ let

$\displaystyle\boldsymbol{{\zeta}^{\prime\prime}}[n]$
$\displaystyle\mathnormal{\hskip 0.5pt:\equiv\hskip 0.5pt}$
$\displaystyle\mathtt{R}\,n\,(\lambda\boldsymbol{v}.\boldsymbol{{\gamma}^{\prime}}[\boldsymbol{v}])\,\Big{(}\lambda
n,p,\boldsymbol{v}.\mathtt{If}(|B|^{\boldsymbol{{z}^{\prime}}}_{\boldsymbol{{\delta}^{\prime}}[\boldsymbol{{t}^{\prime}};\boldsymbol{v}]})\,\big{(}p(\boldsymbol{t}\,\boldsymbol{{t}^{\prime}}\boldsymbol{v})\big{)}\,\boldsymbol{{\delta}^{\prime}}[\boldsymbol{{t}^{\prime}};\boldsymbol{v}]\Big{)}$
(11)

and for $\ b\in\Delta\setminus\Gamma\ $ we define its
$\,\boldsymbol{{\zeta}^{\prime\prime}}[n]\,$ by replacing in (11) the
$\,\boldsymbol{{\gamma}^{\prime}}\,$ with canonical zeros. Here
$\,\boldsymbol{{z}^{\prime}}\,$ are the challenge variables corresponding to
formula $\,B$ . Notice that

$\displaystyle\hskip 0.5pt\vdash\hskip 0.5pt$ $\displaystyle\hskip
1.0pt{t}^{\prime}[\mathtt{S}n]\ =\ s\hskip 0.5pt{t}^{\prime}[n]$ (12)
$\displaystyle\hskip 0.5pt\vdash\hskip 0.5pt$ $\displaystyle\hskip
1.0pt\boldsymbol{{\zeta}^{\prime}}[\mathtt{S}n]\boldsymbol{v}\ =\
\boldsymbol{{\zeta}^{\prime}}[n](\boldsymbol{t}\,\boldsymbol{{t}^{\prime}}\boldsymbol{v})$
(13) $\displaystyle\hskip 0.5pt\vdash\hskip 0.5pt$ $\displaystyle\hskip
1.0pt\boldsymbol{{\zeta}^{\prime\prime}}[\mathtt{S}n]\boldsymbol{v}\ =\
\,\mathtt{If}\,(|B|^{\boldsymbol{{z}^{\prime}}}_{\boldsymbol{{\delta}^{\prime}}[\boldsymbol{{t}^{\prime}};\boldsymbol{v}]})\;\big{(}\boldsymbol{{\zeta}^{\prime\prime}}[n](\boldsymbol{t}\,\boldsymbol{{t}^{\prime}}\boldsymbol{v})\big{)}\
\,\boldsymbol{{\delta}^{\prime}}[\boldsymbol{{t}^{\prime}};\boldsymbol{v}]$
(14)

We attempt to extend (13) to the whole $\,\boldsymbol{\zeta}\,$ by proving
from (14) the following

$\displaystyle|B|^{\boldsymbol{{z}^{\prime}}}_{\boldsymbol{{\zeta}^{\prime\prime}}[\mathtt{S}n]\boldsymbol{v}}$
$\displaystyle\hskip 0.5pt\vdash\hskip 0.5pt$
$\displaystyle\boldsymbol{{\zeta}^{\prime\prime}}[\mathtt{S}n]\boldsymbol{v}\
=\
\boldsymbol{{\zeta}^{\prime\prime}}[n](\boldsymbol{t}\,\boldsymbol{{t}^{\prime}}\boldsymbol{v})$
(15)

We obtain this as an immediate consequence of

$\displaystyle|B|^{\boldsymbol{{z}^{\prime}}}_{\boldsymbol{{\zeta}^{\prime\prime}}[\mathtt{S}n]\boldsymbol{v}}$
$\displaystyle\hskip 0.5pt\vdash\hskip 0.5pt$
$\displaystyle|B|^{\boldsymbol{{z}^{\prime}}}_{\boldsymbol{{\delta}^{\prime}}[\boldsymbol{{t}^{\prime}};\boldsymbol{v}]}$
(16)

Assuming
$\,\neg|B|^{\boldsymbol{{z}^{\prime}}}_{\boldsymbol{{\delta}^{\prime}}[\boldsymbol{{t}^{\prime}};\boldsymbol{v}]}\,$
by (14) we get
$\,\boldsymbol{{\zeta}^{\prime\prime}}[\mathtt{S}n]\boldsymbol{v}=\boldsymbol{{\delta}^{\prime}}[\boldsymbol{{t}^{\prime}};\boldsymbol{v}]\,$
hence
$\,\neg|B|^{\boldsymbol{{z}^{\prime}}}_{\boldsymbol{{\zeta}^{\prime\prime}}[\mathtt{S}n]\boldsymbol{v}}\,$
and
thus (16) follows via $\,\mathtt{Stab}\,$ (which is fully available in the
verifying system).

We now prove (8) by an assumptionless induction on $\,n$ . Let
$\,\boldsymbol{\zeta^{*}}\,$ be the collection of all
$\,\boldsymbol{{\zeta}^{\prime}}\,$ and those
$\,\boldsymbol{{\zeta}^{\prime\prime}}\,$ corresponding to
$\,\Gamma\cap\Delta$ . For $\;n\mathnormal{\;\equiv\;}\mathtt{0}\;$ it is
sufficient that

$\displaystyle|\Gamma|^{\boldsymbol{u}}_{\boldsymbol{\zeta^{*}}[\mathtt{0}]\boldsymbol{v}}$
$\displaystyle\hskip 0.5pt\vdash\hskip 0.5pt$
$\displaystyle|A(\mathtt{0})|^{\boldsymbol{{t}^{\prime}}[\mathtt{0}]}_{\boldsymbol{v}}$

which follows from (6) since by definition (9) we have $\;\hskip
0.5pt\vdash\hskip
0.5pt\,\boldsymbol{{t}^{\prime}}[\mathtt{0}]=\boldsymbol{r}\;$ and by
definitions (10) and (11) we have $\ \hskip 0.5pt\vdash\hskip
0.5pt\,\boldsymbol{\zeta^{*}}[\mathtt{0}]=\lambda\boldsymbol{v}.\,\boldsymbol{\gamma}[\boldsymbol{v}]$
. Now given (8) we want to prove

$\displaystyle|\Gamma\uplus\Delta|^{\,\boldsymbol{u}\uplus\boldsymbol{z}}_{\,\boldsymbol{\zeta}[\mathtt{S}n]\boldsymbol{v}}$
$\displaystyle\hskip 0.5pt\vdash\hskip 0.5pt$
$\displaystyle|A(\mathtt{S}n)|^{\boldsymbol{{t}^{\prime}}[\mathtt{S}n]}_{\boldsymbol{v}}$
(17)

To (8) we apply $\
\forall^{e}_{\\![{\boldsymbol{v}\,\mapsto\,\boldsymbol{t}\,\boldsymbol{{t}^{\prime}}\boldsymbol{v}}]}\
$ and via easy deductions in $\,{\sf NA}\,$ we get

$\displaystyle|\Gamma\uplus\Delta|^{\,\boldsymbol{u}\uplus\boldsymbol{z}}_{\,\boldsymbol{\zeta}[n](\boldsymbol{t}\,\boldsymbol{{t}^{\prime}}\boldsymbol{v})}$
$\displaystyle\hskip 0.5pt\vdash\hskip 0.5pt$
$\displaystyle|A(n)|^{\boldsymbol{t}^{\prime}[n]}_{\boldsymbol{t}\,\boldsymbol{{t}^{\prime}}\boldsymbol{v}}$
(18)

With (13) and (15) we can rewrite (18) to

$\displaystyle|\Gamma\uplus\Delta|^{\,\boldsymbol{u}\uplus\boldsymbol{z}}_{\,\boldsymbol{\zeta}[\mathtt{S}n]\boldsymbol{v}}$
$\displaystyle\hskip 0.5pt\vdash\hskip 0.5pt$
$\displaystyle|A(n)|^{\boldsymbol{t}^{\prime}[n]}_{\boldsymbol{t}\,\boldsymbol{{t}^{\prime}}\boldsymbol{v}}$
(19)

In (7) we substitute $\ \boldsymbol{x}\,\mapsto\,\boldsymbol{{t}^{\prime}}[n]\
$ and get

$\displaystyle|\Delta|^{\boldsymbol{z}}_{\boldsymbol{\delta}[\boldsymbol{{t}^{\prime}};\boldsymbol{v}]}$
$\displaystyle\hskip 0.5pt\vdash\hskip 0.5pt$
$\displaystyle|A(n)|^{\boldsymbol{{t}^{\prime}}[n]}_{\boldsymbol{t}\boldsymbol{{t}^{\prime}}\boldsymbol{v}}\,\rightarrow\,|A(\mathtt{S}n)|^{\boldsymbol{s}\boldsymbol{{t}^{\prime}}[n]}_{\boldsymbol{v}}$

which gives (17) by means of easy $\,{\sf NA}\,$ deductions using  (12) , (16)
and  (19) .

We have treated the most general situation, with all context sets
$\,\Gamma\setminus\Delta$ , $\,\Gamma\cap\Delta\,$ and
$\,\Delta\setminus\Gamma\,$ inhabited by refutation relevant assumptions, and
conclusion formula $\,A\,$ accepting both witnesses and challengers. Many
particular situations amount to easier treatments, with simpler extracted
terms. These can be obtained as simplifications of the general witnesses and
challengers presented above, by means of the reduction properties of the empty
tuple, which was denoted $\,\epsilon\,$ in [17]. We outline below only those
particular cases which are relevant in connection with the modal induction
rule $\mathtt{Ind^{m}_{\iota}}\hskip 0.5pt.$

  * •

If $\Gamma\cup\Delta$ contains no refutation relevant assumption, but $A(n)$
is refutation relevant, then terms $\,\boldsymbol{t}\,$ are no part of the
realizers for the conclusion sequent, in this case only
$\,\boldsymbol{{t}^{\prime}}$ . Hence $\,\boldsymbol{t}\,$ would be
redundantly produced and a mechanism is needed to prevent their construction.
This is ensured by $\Box$ in front of the step $A(n)$ at
$\mathtt{Ind^{m}_{\iota}}\hskip 0.5pt.$

  * •

If $\,A(n)\,$ is refutation relevant, $\,\Delta\,$ has no refutation relevant
element but $\,\Gamma\,$ is refutation relevant inhabited, then
$\,\boldsymbol{\delta}\,$ and $\,\boldsymbol{{\zeta}^{\prime\prime}}\,$ are
empty. Yet
$\,\boldsymbol{\zeta^{*}}\mathnormal{\;\equiv\;}\boldsymbol{{\zeta}^{\prime}}\,$
has to be produced as (10) and includes $\,\boldsymbol{t}[n]$ , which is no
longer the case for $\,\mathtt{Ind^{m}_{\iota}}$ .

  * •

If $\,A(n)\,$ is refutation irrelevant then $\,\boldsymbol{v}$ ,
$\,\boldsymbol{t}\,$ and
$\,\boldsymbol{t}\,\boldsymbol{{t}^{\prime}}\boldsymbol{v}\,$ are empty
tuples. Thus
$\,\boldsymbol{{\zeta}^{\prime}}\mathnormal{\;\equiv\;}\boldsymbol{{\gamma}^{\prime}}\,$
and (11) simplifies to (recall $\,n\not\in{\sf
FV}(\boldsymbol{{\gamma}^{\prime}})$ , $\,n\in{\sf
FV}(\boldsymbol{{t}^{\prime}})$ , and possibly $\,n\in{\sf
FV}(\boldsymbol{{\delta}^{\prime}})$)

$\displaystyle\boldsymbol{{\zeta}^{\prime\prime}}[n]$
$\displaystyle\mathnormal{\hskip 0.5pt\equiv\hskip 0.5pt}$
$\displaystyle\mathtt{R}\;n\;\boldsymbol{{\gamma}^{\prime}}\,\Big{(}\,\lambda
n,p\,.\;\mathtt{If}\,(|B|^{\boldsymbol{{z}^{\prime}}}_{\boldsymbol{{\delta}^{\prime}}[\boldsymbol{{t}^{\prime}}]})\
p\ \boldsymbol{{\delta}^{\prime}}[\boldsymbol{{t}^{\prime}}]\,\Big{)}$

####  5.5.1 Modal induction rule - technical details

tensy  $\displaystyle\penalty 1\Gamma\ \hskip 0.5pt\vdash\hskip 0.5pt\ \Box
A(\mathtt{0})\qquad\Box\Delta\ \hskip 0.5pt\vdash\hskip 0.5pt\ \Box
A(n)\;\rightarrow\;A(\mathtt{S}n)$ $\ {\ \mathtt{Ind^{m}_{\iota}}}$
$\displaystyle\Gamma\,,\,\Box\Delta\ \hskip 0.5pt\vdash\hskip 0.5pt\ \Box
A(n)$
---

We are given

$\displaystyle|\Gamma|^{\boldsymbol{u}}_{\boldsymbol{\gamma}}$
$\displaystyle\hskip 0.5pt\vdash\hskip 0.5pt$
$\displaystyle\forall\boldsymbol{y}\,|A(\mathtt{0})|^{\boldsymbol{r}}_{\boldsymbol{y}}$
(20)

and

$\displaystyle|\Box\Delta|^{\boldsymbol{z}}$ $\displaystyle\hskip
0.5pt\vdash\hskip 0.5pt$
$\displaystyle\forall\boldsymbol{{y}^{\prime}}\,|A(n)|^{\boldsymbol{x}}_{\boldsymbol{{y}^{\prime}}}\,\rightarrow\,|A(\mathtt{S}n)|^{\boldsymbol{s}\boldsymbol{x}}_{\boldsymbol{v}}$

Since $\,\boldsymbol{v}\,\not\in\,{\sf FV}(|\Box\Delta|^{\boldsymbol{z}})\,$
and $\,\boldsymbol{v}\,\not\in\,{\sf
FV}(\forall\boldsymbol{{y}^{\prime}}\,|A(n)|^{\boldsymbol{x}}_{\boldsymbol{{y}^{\prime}}})\,$
from the latter we easily obtain

$\displaystyle|\Box\Delta|^{\boldsymbol{z}}$ $\displaystyle\hskip
0.5pt\vdash\hskip 0.5pt$
$\displaystyle\forall\boldsymbol{{y}^{\prime}}\,|A(n)|^{\boldsymbol{x}}_{\boldsymbol{{y}^{\prime}}}\,\rightarrow\,\forall\boldsymbol{v}\,|A(\mathtt{S}n)|^{\boldsymbol{s}\boldsymbol{x}}_{\boldsymbol{v}}$
(21)

With $\,t[n]\,\mathnormal{\ :\equiv\ }\,\mathtt{R}\,n\,r\,(\lambda n.s)\,$ for
every corresponding pair $\,\langle
r\in\boldsymbol{r}/s\in\boldsymbol{s}\rangle\,$ we show by induction on
$\,n\,$ in $\,{\sf NA}\,$ with base context
$\,|\Gamma|^{\boldsymbol{u}}_{\boldsymbol{\gamma}}\,$ and step context
$\,|\Box\Delta|^{\boldsymbol{z}}\,$ that

$\displaystyle|\Gamma|^{\boldsymbol{u}}_{\boldsymbol{\gamma}}\ ,\
|\Box\Delta|^{\boldsymbol{z}}$ $\displaystyle\hskip 0.5pt\vdash\hskip 0.5pt$
$\displaystyle\forall\boldsymbol{v}\,|A(n)|^{\boldsymbol{t}[n]}_{\boldsymbol{v}}$

As $\,\boldsymbol{t}[\mathtt{0}]\mathnormal{\;\equiv\;}\boldsymbol{r}\,$ the
base is given by (20) and the step follows from (21) with
$\,\boldsymbol{x}\mapsto\boldsymbol{t}[n]\,$ since
$\,\boldsymbol{t}[\mathtt{S}n]\,\mathnormal{\;\equiv\;}\,\boldsymbol{s}\,\boldsymbol{t}[n]$
. Thus challengers $\,\boldsymbol{\gamma}\,$ are simply preserved for
$\,|\Gamma|\,$ and witnesses $\,\boldsymbol{t}[n]\,$ are easily constructed
for $\,|\Box A(n)|\,$ in the conclusion sequent of
$\,\mathtt{Ind^{m}_{\iota}}$ .

###### Remark 6

Our modal induction rule is equivalent to a special case of
$\,\mathtt{Ind}_{\iota}$ , since a $\,\Box\,$ can be placed in front of
$\,A(\mathtt{S}n)\,$ from the step sequent of $\,\mathtt{Ind^{m}_{\iota}}$ .
The equivalence of the two formulations for the step sequent can easily be
proved using $\,\mathtt{AxT}$ , $\,\mathtt{Ax4}$ , $\,\mathtt{AxK}\,$ and
$\,\Box^{i}$ . Extracted terms are the same and the verifying proof only gets
more direct.