Peano Arithmetic and MALL

# Peano Arithmetic and MALL

Matteo Manighetti
Inria Saclay
Saclay  France  Dale Miller
Inria-Saclay and LIX  Institut Polytechnique de Paris
Palaiseau  France

(Draft: )

###### Abstract

Formal theories of arithmetic have traditionally been based on either
classical or intuitionistic logic, leading to the development of Peano and
Heyting arithmetic, respectively. We propose a use MALL as a formal theory of
arithmetic based on linear logic. This formal system is presented as a sequent
calculus proof system that extends the standard proof system for
multiplicative-additive linear logic (MALL) with the addition of the logical
connectives universal and existential quantifiers (first-order quantifiers),
term equality and non-equality, and the least and greatest fixed point
operators. We first demonstrate how functions defined using MALL relational
specifications can be computed using a simple proof search algorithm. By
incorporating weakening and contraction into MALL, we obtain
$\hbox{LK}_{p}^{+}$, a natural candidate for a classical sequent calculus for
arithmetic. While important proof theory results are still lacking for
$\hbox{LK}_{p}^{+}$ (including cut-elimination and the completeness of
focusing), we prove that $\hbox{LK}_{p}^{+}$ is consistent and that it
contains Peano arithmetic. We also prove two conservativity results regarding
$\hbox{LK}_{p}^{+}$ over MALL.

##  1 Introduction

A feature of first-order logic is not only the presence of propositional
connectives, first-order quantifiers, and first-order terms but also the class
of non-logical constants called _predicates_ that denote relations between
terms. When we move from first-order logic to first-order arithmetic, we
introduce induction principles and banish undefined predicates by formally
defining relations between terms using those inductive principles. When moving
from classical logic to arithmetic in this fashion, one arrives at a
presentation of Peano Arithmetic. In this paper, we propose to study
arithmetic based instead on linear logic: in particular, we shall use the MALL
logic of [1, 2, 3] to capture this linearized version of arithmetic.

Linear logic has played various roles in computational logic. Many
applications rely on the ability of linear logic to capture the multiset
rewriting paradigm, which, in turn, can encode Petri nets [4], process calculi
[5, 6], and stateful computations [7, 8]. Our use of linear logic here will
have none of that flavor. While the sequent calculus we use to present MALL in
Section 3 is based on multisets of formulas, we shall not model computation as
some rewriting of multisets of atomic-formulas-as-tokens. In contrast, when we
use linear logic connectives within arithmetic, we capture computation and
deduction via familiar means that rely on relations between numerical
expressions. Our approach to linearized arithmetic is similar to that
expressed recently by Girard [9] about linear logic: “ _Linear_ logic is an
unfortunate expression that suggests a particular system, while it is the key
permitting the abandonment of all systems.”111The original French: “Logique
_linéaire_ est une expression malvenue qui suggère un système alors qu’il
s’agit de la clef permettant de les abandonner tous.” Here, we propose
linearized arithmetic not to have a new, non-standard arithmetic but to better
understand computation and reasoning in arithmetic.

Since we are interested in using MALL to study _arithmetic_ , we use first-
order structures to encode natural numbers and fixed points to encode
relations among numbers. This focus is in contrast to uses of the
propositional subset of MALL as a typing systems (see, for example, [10]). We
shall limit ourselves to using invariants to reason inductively about fixed
points instead of employing other methods, such as infinitary proof systems
(e.g., [11]) and cyclic proof systems (e.g., [12, 13]).

Our first step with the analysis of arithmetic starts by demonstrating that
functions defined using relational specifications in MALL can be computed
directly from that relational specification using unification and backtracking
search (Section 4). We also introduce a new proof system $\hbox{LK}_{p}^{+}$
that is identical to MALL except for the addition of weakening and
contraction. While adding weakening and contraction to MALL provides a natural
and well studied proof system for classical logic, the exact nature of
$\hbox{LK}_{p}^{+}$ is not well understood yet. In particular, for example, if
we denote by $\hbox{LK}_{p}$ the result of removing the cut-rule from
$\hbox{LK}_{p}^{+}$, we do not know if $\hbox{LK}_{p}$ and $\hbox{LK}_{p}^{+}$
prove the same sequents, and we do not know if the completeness of focusing
holds for $\hbox{LK}_{p}$. In this paper, we show that $\hbox{LK}_{p}^{+}$ is
consistent, that it contains Peano arithmetic (Section 6), and that
$\hbox{LK}_{p}$ has certain conservativity results with respect to MALL
(Section 7).

##  2 Terms and formulas

We use Church’s approach [14] to defining terms, formulas, and abstractions
over these by making them all simply typed $\lambda$-terms. The primitive type
$o$ denotes formulas (of linear and classical logics). For the scope of this
paper, we assume that there is a second primitive type $\iota$ and that the
(ambient) signature ${\bf P}_{0}$ contains the constructors $z\colon\iota$
(zero) and $s\colon\iota\rightarrow\iota$ (successor). We abbreviate the terms
$z$, $(s~{}z)$, $(s~{}(s~{}z))$, $(s~{}(s~{}(s~{}z)))$, etc by 0, 1, 2, 3,
etc.

###  2.1 Logical connectives involving type $\iota$

We first present the logical connectives that relate to first-order
structures. The two quantifiers $\forall$ and $\exists$ are both given the
type $(\iota\rightarrow o)\rightarrow o$: the terms $\forall(\lambda x.B)$ and
$\exists(\lambda x.B)$ of type $o$ are abbreviated as $\forall x.B$ and
$\exists x.B$, respectively. Equality $=$ and non-equality $\neq$ are both of
the type $\iota\rightarrow\iota\rightarrow o$. For $n\geq 0$, the least fixed
point operator of arity $n$ is written as $\mu_{n}$ and the greatest fixed
point operator of arity $n$ is written as $\nu_{n}$, and they both have the
type $(A\rightarrow A)\rightarrow A$ where $A$ is the type
$\iota\rightarrow\cdots\rightarrow\iota\rightarrow o$ in which there are $n$
occurrences of $\iota$. We seldom write explicitly the arity of fixed points
since that can usually be determined from context when its value is important.
The pairs of connectives $\langle\forall,\exists\rangle$,
$\langle\mu,\nu\rangle$, and $\langle=,\neq\rangle$ are De Morgan duals.

Our formalizations of arithmetic do not contain predicate symbols: we do not
admit any non-logical symbols of type
$\iota\rightarrow\cdots\rightarrow\iota\rightarrow o$. As a result, there are
no atomic formulas, usually defined as formulas with a non-logical symbol as
their head. Equality, non-equality, and the fixed point operators are treated
as logical connectives since they will all receive introduction rules in the
sequent calculus proof systems that we introduce soon.

###  2.2 Propositional connectives of linear logic

The eight linear logic connectives for MALL are the following.

|  conjunction |  true |  disjunction |  false
---|---|---|---|---
multiplicative | $\mathrel{\otimes}$ | $1$ | $\mathrel{\invamp}$ | $\bot$
additive | $\mathrel{\&}$ | $\top$ | $\mathrel{\oplus}$ | $0$

The four binary connectives have type $o\rightarrow o\rightarrow o$, and the
four units have type $o$. (The use of 0 and 1 as logical connectives is
unfortunate for a paper about arithmetic: as we mentioned above, numerals are
written in boldface.) Formulas involving the set of logical connectives in
Section 2.1 and these propositional connectives are called MALL formulas, a
logic that was first proposed in [1].222This logic was named simply
$\mu\mbox{{MALL}}$ in [1] but that name is often used to denote the subset of
that logic without $=$, $\neq$, $\forall$, and $\exists$: see, for example,
[15, 16]. As a result, we have renamed this logic here with the addition of
the equality sign to stress our interest in the structure of first-order
terms. Many of the proof-theoretic properties of MALL will be summarized in
Section 3.

We do not treat negation as a logical connective: when $B$ is a formula, we
write $\overline{B}$ to denote the formula resulting from taking the De Morgan
dual of $B$. We occasionally use the linear implication $B\multimap C$ as an
abbreviation for $\overline{B}\mathrel{\invamp}C$. We also use this overline
notation when $B$ is the body of a fixed point expression, i.e., when $B$ has
the form $\lambda p\lambda\vec{x}.C$ where $C$ is a formula, $p$ is a first-
order predicate variable, and $\vec{x}$ is a list of first-order variables,
then $\overline{B}$ is $\lambda p\lambda\vec{x}.\overline{C}$ [3, Definition
2.1]. For example, if $B$ is $[\lambda p\lambda x.x=z\mathrel{\oplus}\exists
y.x=(s~{}(s~{}y))\mathrel{\otimes}p~{}y]$ then $\overline{B}$ is $[\lambda
p\lambda x.x\neq z\mathrel{\&}\forall
y.x\neq(s~{}(s~{}y))\mathrel{\invamp}p~{}y]$.

###  2.3 Polarized and unpolarized formulas

The connectives of linear logic are given a _polarity_ as follows. The
_negative_ connectives are $\mathrel{\invamp}$, $\bot$, $\mathrel{\&}$,
$\top$, $\forall$, $\neq$, and $\nu$ while their De Morgan duals—namely,
$\mathrel{\otimes}$, $1$, $\mathrel{\oplus}$, $0$, $\exists$, $=$, and
$\mu$—are positive. A MALL formula is positive or negative depending only on
the polarity of its topmost connective. The polarity flips between $B$ and
$\overline{B}$. We shall also call MALL formulas _polarized formulas_.

_Unpolarized formulas_ are built using $\land$, tt, $\lor$, ff, $=$, $\not=$,
$\forall$, $\exists$, $\mu$, and $\nu$. Note that the six connectives with $i$
in their typing can appear in polarized and unpolarized formulas. Unpolarized
formulas are also called _classical logic formulas_. Note that unpolarized
formulas do not contain negations. We shall extend the notation $\overline{B}$
to unpolarized formulas $B$ in the same sense as used with polarized formulas.
For convenience, we will occasionally allow implications in unpolarized
formulas: in those cases, we treat $P\supset Q$ as $\overline{P}\lor Q$.

A polarized formula $\hat{Q}$ is a _polarized version_ of the unpolarized
formula $Q$ if every occurrence of $\mathrel{\&}$ and $\mathrel{\otimes}$ in
$\hat{Q}$ is replaced by $\wedge$ in $Q$, every occurrence of
$\mathrel{\invamp}$ and $\mathrel{\oplus}$ in $\hat{Q}$ is replaced by $\vee$
in $Q$, every occurrence of $1$ and $\top$ in $\hat{Q}$ is replaced by tt in
$Q$, and every occurrence of $0$ and $\bot$ in $\hat{Q}$ is replaced by ff in
$Q$. Notice that if $Q$ has $n$ occurrences of propositional connectives, then
there are $2^{n}$ formulas $\hat{Q}$ that are polarized versions of $Q$.

Fixed point expression, such as $((\mu\lambda P\lambda x(B~{}P~{}x))~{}t)$,
introduce variables of predicate type (here, $P$). In the case of the $\mu$
fixed point, any expression built using that predicate variable will be
considered positively polarized. If the $\nu$ operator is used instead, any
expressions built using the predicate variables it introduces are considered
negatively polarized.

###  2.4 The polarization hierarchy

A formula is _purely positive_ (resp., _purely negative_) if every logical
connective it contains is positive (resp., negative). Taking inspiration from
the familiar notion of the arithmetical hierarchy, we define the following
collections of formulas. The formulas in ${\bf P}_{1}$ are the purely positive
formulas, and the formulas in ${\bf N}_{1}$ are the purely negative formulas.
More generally, for $n\geq 1$, the ${\bf N}_{n+1}$-formulas are those negative
formulas for which every positive subformula occurrence is a ${\bf
P}_{n}$-formula. Similarly, the ${\bf P}_{n+1}$-formulas are those positive
formulas for which every negative subformula occurrence is a ${\bf
N}_{n}$-formula. A formula in ${\bf P}_{n}$ or in ${\bf N}_{n}$ has at most
$n-1$ alternations of polarity. Clearly, the dual of a ${\bf P}_{n}$-formula
is a ${\bf N}_{n}$-formula, and vice versa. We shall also extend these
classifications of formulas to abstractions over terms: thus, we say that the
term $\lambda x.B$ of type $i\rightarrow o$ is in ${\bf P}_{n}$ if $B$ is a
${\bf P}_{n}$-formula.

Note that for all $n\geq 1$, if $B$ is an unpolarized $\Pi_{n}^{0}$-formula
(in the usual arithmetic hierarchy) then there is a polarized version of $B$
that is ${\bf N}_{n}$. Similarly, if $B$ is an unpolarized
$\Sigma_{n}^{0}$-formula then there is a polarized version of $B$ that is
${\bf P}_{n}$.

##  3 Linear and classical proof systems for polarized formulas

###  3.1 The MALL and $\hbox{LK}_{p}^{+}$ proof systems

The MALL proof system [1, 3] for polarized formulas is the one-sided sequent
calculus proof system given in Figure 3. The variable $y$ in the
$\forall$-introduction rule is an _eigenvariable_ : it is restricted to not be
free in any formula in the conclusion of that rule. The application of a
substitution $\theta$ to a signature $\Sigma$ (written $\Sigma\theta$ in the
$\neq$ rule in Figure 3) is the signature that results from removing from
$\Sigma$ the variables in the domain of $\theta$ and adding back any variable
that is free in the range of $\theta$. In the $\neq$-introduction rule, if the
terms $t$ and $t^{\prime}$ are not unifiable, the premise is empty and
immediately proves the conclusion.

The choice of using Church’s $\lambda$-notation provides an elegant treatment
of higher-order substitutions (needed for handling induction invariants) and
provides a simple treatment of fixed point expressions and the binding
mechanisms used there. In particular, we shall assume that formulas in
sequents are always treated modulo $\alpha\beta\eta$-conversion. We usually
display formulas in $\beta\eta$-long normal form when presenting sequents.
Note that formula expressions such as $B~{}S~{}\vec{t}$ (see Figure 3) are
parsed as $(\cdots((B~{}S)t_{1})\cdots t_{n})$ if $\vec{t}$ is the list of
terms $t_{1},\ldots,t_{n}$.

$\begin{array}[]{c@{\strut\qquad}c@{\strut\qquad}c@{\strut\qquad}c}\vdash\Gamma,\Delta,B\mathrel{\otimes}C\lx@proof@logical@and\vdash\Gamma,B\vdash\Delta,C&\vdash
1&\vdash\Gamma,B\mathrel{\invamp}C\vdash\Gamma,B,C&\vdash\Gamma,\bot\vdash\Gamma\\\
\vdash\Gamma,B\mathrel{\&}C\lx@proof@logical@and\vdash\Gamma,B\vdash\Gamma,C&\vdash\Delta,\top&\vdash\Gamma,B_{0}\mathrel{\oplus}B_{1}\vdash\Gamma,B_{i}\\\
\vdash\Gamma,t\neq
t^{\prime}\\{~{}\vdash\Gamma\theta:\theta=mgu(t,t^{\prime})~{}\\}&\vdash
t=t&\vdash\Gamma,\exists x.Bx\vdash\Gamma,Bt&\vdash\Gamma,\forall
x.Bx\vdash\Gamma,By\end{array}$

$\begin{array}[]{c@{\strut\qquad}c@{\strut\qquad}c@{\strut\qquad}c}\vdash\Gamma,\nu
B\vec{t}\lx@proof@logical@and\vdash\Gamma,S\vec{t}\vdash
BS\vec{x},\overline{(S\vec{x})}&\vdash\Gamma,\mu B\vec{t}\vdash\Gamma,B(\mu
B)\vec{t}&\vdash\mu B\vec{t},\nu\overline{B}\vec{t}\end{array}$

Figure 1: The inference rules for the MALL proof system

$\vdash\Gamma,\nu B\vec{t}\vdash\Gamma,B(\nu B)\vec{t}\qquad\vdash
B,\overline{B}\qquad\vdash\Gamma,\Delta\vdash\Gamma,B\quad\vdash\Delta,\overline{B}$

Figure 2: Three rules admissible in MALL

$\vdash\Gamma,B\vdash\Gamma,B,B\qquad\vdash\Gamma,B\vdash\Gamma$

Figure 3: Two structural rules

If we were working in a two-sided calculus, the $\nu$-rule in Figure 3 would
split into the two rules

$\Gamma\vdash\nu B\vec{t},\Delta\Gamma\vdash\Delta,S\vec{t}\quad
S\vec{x}\vdash BS\vec{x}\Gamma,\mu
B\vec{t}\vdash\Delta\Gamma,S\vec{t}\vdash\Delta\quad BS\vec{x}\vdash S\vec{x}$

That is the one rule for $\nu$ yields both coinduction and induction. In
general, we shall speak of the higher-order substitution term $S$ used in both
of these rules as the _invariant_ of that rule (i.e., we will not use the term
co-invariant even though that might be more appropriate in some settings).

We make the following observations about this proof system.

  1. 1.

The $\mu$ rule allows the $\mu$ fixed point to be unfolded. This rule
captures, in part, the identification of $\mu B$ with $B(\mu B)$; that is,
$\mu B$ is a fixed point of $B$. This inference rule allows one occurrence of
$B$ in $(\mu B)$ to be expanded to two occurrences of $B$ in $B(\mu B)$. In
this way, unbounded behavior can appear in MALL where it does not occur in
MALL.

  2. 2.

The proof rules for equality guarantee that function symbols are all treated
injectively; thus, function symbols will act only as term constructors. In
this paper, the only function symbols we employ are for zero and successor: of
course, a theory of arithmetic should treat these symbols injectively.

  3. 3.

The admissibility of the three rules in Figure 3 for MALL is proved in [3].
The general form of the initial rule is admissible, although the proof system
only dictates a limited form of that rule via the $\mu\nu$ rule. The unfold
rule in Figure 3, which simply unfolds $\nu$-expression, is admissible in MALL
by using the $\nu$-rule with the invariant $S=B(\nu B)$.

  4. 4.

While the weakening and contraction rules are not generally admissible in
MALL, they are both admissible for ${\bf N}_{1}$ formulas.

We could add the inference rules for equality, non-equality, and least and
greatest fixed points to Gentzen’s LK proof system for first-order classical
logic [17]. We take a different approach, however, in that we will only
consider proof systems for classical logic using polarized versions of
classical formulas. In particular, the $\hbox{LK}_{p}^{+}$ proof system is the
result of adding to the MALL proof system the rules for contraction $C$ and
weakening $W$ from Figure 3 as well as the cut rule.

###  3.2 Examples

The formula $\forall x\forall y[x=y\lor x\neq y]$ can be polarized as either

$\forall x\forall y[x=y\mathrel{\invamp}x\neq y]\hbox{\quad or \quad}\forall
x\forall y[x=y\mathrel{\oplus}x\neq y].$

These polarized formulas belong to ${\bf N}_{2}$ and ${\bf N}_{3}$,
respectively. Only the first of these is provable in MALL, although both
formulas are provable in $\hbox{LK}_{p}$.

Note that it is clear that if there exists a MALL proof of a ${\bf P}_{1}$
formula, then that proof does not contain the $\nu$ rule, i.e., it does not
contain the rules involving invariants. Finally, given that first-order Horn
clauses can interpret Turing machines [18], and given that Horn clauses can
easily be encoded using ${\bf P}_{1}$ formulas, it is undecidable whether or
not a ${\bf P}_{1}$ expression has a MALL proof. Similarly, ${\bf P}_{1}$
formulas can be used to specify any general recursive function. Obviously, the
provability of ${\bf N}_{1}$ formulas is also undecidable.

The unary relation for denoting the set of natural numbers and the ternary
relations for addition and multiplication can be axiomatized using Horn
clauses as follows.

$\displaystyle{\rm Nature}~{}{\bf 0}$ $\displaystyle\forall x({\rm
Nature}~{}x\supset\;$ $\displaystyle{\rm Nature}~{}(s~{}x))$
$\displaystyle\forall x($ $\displaystyle\hbox{\sl plus\/}~{}{\bf 0}~{}x~{}x)$
$\displaystyle\forall x\forall y\forall u(\hbox{\sl
plus\/}~{}x~{}y~{}u\supset\;$ $\displaystyle\hbox{\sl
plus\/}~{}(s~{}x)~{}y~{}(s~{}u))$ $\displaystyle\forall x($
$\displaystyle\hbox{\sl mult\/}~{}{\bf 0}~{}x~{}{\bf 0})$
$\displaystyle\forall x\forall y\forall u\forall w(\hbox{\sl
mult\/}~{}x~{}y~{}u\land\hbox{\sl plus\/}~{}y~{}u~{}w\supset\;$
$\displaystyle\hbox{\sl mult\/}~{}(s~{}x)~{}y~{}w)$

These Horn clauses can be mechanically transformed into the following least
fixed point definitions of these relations.

${\rm Nature}=\mu\lambda N\lambda x(x={\bf 0}\oplus\exists
x^{\prime}(x=(s~{}x^{\prime})\mathrel{\otimes}N~{}x^{\prime}))$ $\hbox{\sl
plus\/}=\mu\lambda P\lambda x\lambda y\lambda u((x={\bf
0}\mathrel{\otimes}y=u)\mathrel{\oplus}\exists x^{\prime}\exists
u^{\prime}\exists
w(x=(s~{}x^{\prime})\mathrel{\otimes}u=(s~{}u^{\prime})\mathrel{\otimes}P~{}x^{\prime}~{}y~{}u^{\prime}))$
$\hbox{\sl mult\/}=\mu\lambda M\lambda x\lambda y\lambda w\big{(}(x={\bf
0}\mathrel{\otimes}u={\bf 0})\mathrel{\oplus}\exists x^{\prime}\exists
u^{\prime}\exists
w(x=(s~{}x^{\prime})\mathrel{\otimes}plus~{}y~{}u^{\prime}~{}w\mathrel{\otimes}M~{}x^{\prime}~{}y~{}w)\big{)}$

Both of these fixed point expressions are ${\bf P}_{1}$.

The following derivation verifies that 4 is a sum of 2 and 2.

$\vdash\exists p.\hbox{\sl plus\/}~{}{\bf 2}~{}{\bf
2}~{}p\mathrel{\otimes}{\rm Nature}~{}p\lx@proof@logical@and\vdash\hbox{\sl
plus\/}~{}{\bf 2}~{}{\bf 2}~{}{\bf 4}\vdash({\bf 2}={\bf
0}\mathrel{\otimes}{\bf 2}={\bf 4})\mathrel{\oplus}\exists n^{\prime}\exists
p^{\prime}({\bf 2}=(s~{}n^{\prime})\mathrel{\otimes}{\bf
4}=(s~{}p^{\prime})\mathrel{\otimes}P~{}n^{\prime}~{}{\bf
2}~{}p^{\prime})\vdash\exists n^{\prime}\exists p^{\prime}({\bf
2}=(s~{}n^{\prime})\mathrel{\otimes}{\bf
4}=(s~{}p^{\prime})\mathrel{\otimes}\hbox{\sl plus\/}~{}n^{\prime}~{}{\bf
2}~{}p^{\prime})\vdash{\bf 2}=(s~{}{\bf 1})\mathrel{\otimes}{\bf 4}=(s~{}{\bf
3})\mathrel{\otimes}\hbox{\sl plus\/}~{}{\bf 1}~{}{\bf 2}~{}{\bf 3}\vdash{\bf
2}=(s~{}{\bf 1})\quad\vdash{\bf 4}=(s~{}{\bf 3})\quad\vdash\hbox{\sl
plus\/}~{}{\bf 1}~{}{\bf 2}~{}{\bf 3}\vdash{\rm Nature}~{}{\bf 4}$

To complete this proof, we must construct the (obvious) proof of $\vdash{\rm
Nature}~{}{\bf 4}$ and a similar subproof verifying that $1+2=3$. Note that in
the bottom up construction of this proof, the witness used to instantiate the
final $\exists p$ is, in fact, the sum of 2 and 2. Thus, this proof
construction does not compute this sum’s value but instead simply checks that
4 is the correct value.

In contrast to the above example, the following proof of $\forall u(\hbox{\sl
plus\/}~{}{\bf 2}~{}{\bf 2}~{}u\supset{\rm Nature}~{}u)$ can be seen as a
_computation_ of the value of 2 plus 2. The proof of this sequent begins as
follows.

$\vdash\forall u(\overline{\hbox{\sl plus\/}~{}{\bf 2}~{}{\bf
2}~{}u}\mathrel{\invamp}{\rm Nature}~{}u)\vdash\overline{\hbox{\sl
plus\/}~{}{\bf 2}~{}{\bf 2}~{}u},{\rm Nature}~{}u\vdash{\bf 2}\neq{\bf
0}\mathrel{\invamp}{\bf 2}\neq u,{\rm Nature}~{}u~{}~{}\vdash\forall
x^{\prime}\forall u^{\prime}\forall w({\bf
2}\neq(s~{}x^{\prime})\mathrel{\invamp}u\neq(s~{}u^{\prime})\mathrel{\invamp}\overline{\hbox{\sl
plus\/}~{}x^{\prime}~{}{\bf 2}~{}u^{\prime}},{\rm Nature}~{}u)\vdash{\bf
2}\neq(s~{}x^{\prime}),u\neq(s~{}u^{\prime}),\overline{\hbox{\sl
plus\/}~{}x^{\prime}~{}{\bf 2}~{}u^{\prime}},{\rm
Nature}~{}u\vdash\overline{\hbox{\sl plus\/}~{}{\bf 1}~{}{\bf
2}~{}u^{\prime}},{\rm Nature}~{}(s~{}u^{\prime})$

In a similar fashion, the open premise above has a partial proof which reduces
its provability to the provability of the sequent $\vdash\overline{\hbox{\sl
plus\/}~{}{\bf 0}~{}{\bf 2}~{}u^{\prime}},{\rm
Nature}~{}(s~{}(s~{}u^{\prime}))$. This final sequent is similarly reduced to
$\vdash{\bf 0}\neq{\bf 0},{\bf 2}\neq u^{\prime},{\rm
Nature}~{}(s~{}(s~{}u^{\prime}))$, which is itself reduced to $\vdash{\rm
Nature}~{}{\bf 4}$, which has a trivial proof. Note that the bottom
construction of this proof involves the systematic computation of the value of
2 plus 2.

The previous two proofs involved with the judgment $2+2=4$ illustrates two
different ways to determine $2+2$: the first involves a “guess-and-check”
approach while the second involves a direct computation. We will return to
this relationship in Section 4.

Unpolarized formulas that state the _totality_ and _determinacy_ of the
function encoded by a binary relation $\phi$ can be written as

$\displaystyle[\forall x.$ $\displaystyle{\rm Nature}~{}x\supset\exists y.{\rm
Nature}~{}y\land\phi(x,y)]\;\land$ $\displaystyle[\forall x.$
$\displaystyle{\rm Nature}~{}x\supset\forall y_{1}.{\rm
Nature}~{}y_{1}\supset\forall y_{2}.{\rm
Nature}~{}y_{2}\supset\phi(x,y_{1})\supset\phi(x,y_{2})\supset y_{1}=y_{2}].$

If this formula is polarized so that the two implications are encoded using
$\mathrel{\invamp}$, the conjunction is replaced by $\with$, and the
expression $\phi$ is ${\bf P}_{1}$, then this formula is a ${\bf N}_{2}$
formula.

Given the definition of addition on natural numbers above, the following
totality and determinacy formulas

$\displaystyle[\forall x_{1}\forall x_{2}.$ $\displaystyle~{}{\rm
Nature}~{}x_{1}\supset{\rm Nature}~{}x_{2}\supset\exists y.(\hbox{\sl
plus\/}(x_{1},x_{2},y)\land{\rm Nature}~{}y)]$ $\displaystyle[\forall
x_{1}\forall x_{2}.$ $\displaystyle~{}{\rm Nature}~{}x_{1}\supset{\rm
Nature}~{}x_{2}\supset\forall y_{1}\forall y_{2}.~{}\hbox{\sl
plus\/}(x_{1},x_{2},y_{1})\supset\hbox{\sl plus\/}(x_{1},x_{2},y_{2})\supset
y_{1}=y_{2}]$

can be proved in MALL where $\supset$ is polarized using $\mathrel{\invamp}$
and the one occurrence of conjunction above is polarized using $\with$. These
proofs require both induction and the $\mu\nu$ rule.

The direct connection between proof search in MALL and the model checking
problems of reachability and bisimilarity (and their negations) has been
demonstrated in [19]. In particular, reachability problems were encoded as
${\bf P}_{1}$ formulas, while non-reachability problems were encoded as ${\bf
N}_{1}$ formulas. The paper [19] also showed that the specification of
simulation and bisimulation can be encoded as ${\bf N}_{2}$ formulas. Another
common form of ${\bf P}_{1}$ formulas arises when applying the Clark
completion [20] to Horn clause specifications.

###  3.3 Some known results concerning MALL

While MALL does not contain the contraction rule, it is still possible for the
number of occurrences of logical connectives to grow in sequents when
searching for a proof. In particular, the unfolding rule (when read from
conclusion to premise) can make a sequent containing $(\mu B\vec{t})$ into a
sequent containing $(B(\mu B)\vec{t})$: here, the abstracted formula $B$ is
repeated. Surprisingly, however, the subset of MALL that does not contain
occurrences of fixed points is still undecidable. In particular, consider the
following two sets of inductively defined classes of MALL formulas.

$\begin{array}[]{cl}\Phi~{}::=&\Phi\with\Phi\;|\;\exists x.\Phi\;|\;\forall
x.\Phi\;|\;\Psi\\\ \Psi~{}::=&t_{1}=t_{1}^{\prime}\multimap\cdots\multimap
t_{n}=t_{n}^{\prime}\multimap t_{0}=t_{0}^{\prime}\quad(n\geq 0)\end{array}$

If we also assume that there are exactly three constructors, one each of type
$\iota\rightarrow\iota$, $\iota\rightarrow\iota\rightarrow\iota$, and
$\iota\rightarrow\iota\rightarrow\iota\rightarrow\iota$, then it is
undecidable whether or not a given formula $\Phi$ is provable in MALL [21].

The two principle and major proof-theoretic results concerning MALL are the
admissibility of the cut rule (in Figure 3) and the completeness of a focusing
proof system.

###  3.4 Definable exponentials

As Baelde showed in [3], the following definitions

$\mathord{\mathop{?}}P=\mu(\lambda p.\bot\oplus(p\mathrel{\invamp}p)\oplus
P)\qquad\mathord{\mathop{!}}P={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathord{\mathop{?}}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\overline{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}P}}}}}$

approximate the exponentials of linear logic in the sense that the following
four rules—dereliction, contraction, weakening, and promotion—are admissible
in MALL.

$\vdash\mathord{\mathop{?}}B,\Gamma\vdash\Gamma\qquad\vdash\mathord{\mathop{?}}B,\Gamma\vdash\mathord{\mathop{?}}B,\mathord{\mathop{?}}B,\Gamma\qquad\vdash\mathord{\mathop{?}}B,\Gamma\vdash
B,\Gamma\qquad\vdash\mathord{\mathop{!}}B,\mathord{\mathop{?}}\Gamma\vdash
B,\mathord{\mathop{?}}\Gamma$

In particular, we use $\hbox{MALL}(\mathord{\mathop{!}},\mathord{\mathop{?}})$
to denote the extension of MALL with the two exponentials
$\mathord{\mathop{!}}$ and $\mathord{\mathop{?}}$ and the above four proof
rules. Thus, every
$\hbox{MALL}(\mathord{\mathop{!}},\mathord{\mathop{?}})$-provable same sequent
can be mapped to a MALL-provable sequent by simply replacing the exponentials
for their corresponding fixed point definition.

##  4 Using proof search to compute functions

We say that a binary relation $\phi$ encodes a function $f$ if $\phi(x,y)$
holds if and only if $f(x)=y$. Of course, this correspondence is only well
defined if we know that the _totality_ and _determinacy_ properties hold for
$\phi$. For example, let plus be the definition of addition on natural numbers
given in Section 3. The following polarized formulas encoding totality and
determinacy are ${\bf N}_{2}$ formulas.

$\displaystyle[\forall x_{1}\forall x_{2}.$ $\displaystyle~{}{\rm
Nature}~{}x_{1}\multimap{\rm Nature}~{}x_{2}\multimap\exists y.{\rm
Nature}~{}y\mathrel{\otimes}\hbox{\sl plus\/}~{}x_{1}~{}x_{2}~{}y]$
$\displaystyle[\forall x_{1}\forall x_{2}.$ $\displaystyle~{}{\rm
Nature}~{}x_{1}\multimap{\rm Nature}~{}x_{2}\multimap\forall y_{1}\forall
y_{2}.~{}\hbox{\sl plus\/}~{}x_{1}~{}x_{2}~{}y_{1}\multimap\hbox{\sl
plus\/}~{}x_{1}~{}x_{2}~{}y_{2}\multimap y_{1}=y_{2}]$

These formulas can be proved in MALL.

One approach to computing the function that adds two natural numbers is to
follow the Curry-Howard approach of relating proof theory to computation [22].
First, extract from a natural deduction proof of the totality formula above a
typed $\lambda$-term. Second, apply that $\lambda$-term to the $\lambda$-terms
representing the two proofs of, say, ${\rm Nature}~{}n$ and ${\rm
Nature}~{}m$. Third, use a non-deterministic rewriting process that
iteratively selects $\beta$-redexes for reduction. In most typed
$\lambda$-calculus systems, all such sequences of rewritings will end in the
same normal form, although some sequences of rewrites might be very long, and
others can be very short. The resulting normal $\lambda$-term should encode
the proof of ${\rm Nature}~{}p$, where $p$ is the sum of $n$ and $m$. In this
section, we will present an alternative mechanism for computing functions from
their relational specification that relies on using proof search mechanisms
instead of this proof-normalization mechanism.

The totality and determinacy properties of some binary relation $\phi$ can be
expressed equivalently as: for any natural number $n$, the expression $\lambda
y.\phi(n,y)$ denotes a singleton set. Of course, the sole member of that
singleton set is the value of the function it encodes. If our logic contained
a choice operator, such as Church’s _definite description_ operator $\iota$
[14], then this function can be represented via the expression $\lambda
x.\iota y.\phi(x,y)$. The search for proofs can, however, be used to provide a
more computational approach to computing the function encoded by $\phi$.
Assume that $P$ and $Q$ are predicates of arity one and that $P$ denotes a
singleton. In this case, the (unpolarized) formulas $\exists x[Px\land Qx]$
and $\forall x[Px\supset Qx]$ are logically equivalent, although the proof
search semantics of these formulas are surprisingly different. In particular,
if we attempt to prove $\exists x[Px\land Qx]$, then we must _guess_ a term
$t$ and then _check_ that $t$ denotes the element of the singleton (by proving
$P(t)$). In contrast, if we attempt to prove $\forall x[Px\supset Qx]$, we
allocate an eigenvariable $y$ and attempt to prove the sequent $\vdash
Py\supset Qy$. Such an attempt at building a proof might _compute_ the value
$t$ (especially if we can restrict proofs of that implication not to involve
the general form of induction). This difference was illustrated in Section 3
with the proof of $\vdash\exists p.\hbox{\sl plus\/}~{}{\bf 2}~{}{\bf
2}~{}p\mathrel{\otimes}{\rm Nature}~{}p$ (which guesses and checks that the
value of 2 plus 2 is 4) versus the proof of $\forall u(\overline{\hbox{\sl
plus\/}~{}{\bf 2}~{}{\bf 2}~{}u}\mathrel{\invamp}{\rm Nature}~{}u)$ (which
incrementally constructs the sum of 2 and 2).

Assume that $P$ is a ${\bf P}_{1}$ predicate expression of type $i\rightarrow
o$ and that we have a MALL proof of $\forall x[Px\supset{\rm Nature}~{}x]$. If
this proof does not contain the induction rule, then that proof can be seen as
computing the sole member of $P$. As the following example shows, it is not
the case that if there is a MALL proof of $\forall x[Px\supset{\rm
Nature}~{}x]$ then it has a proof in which the only form of the induction rule
is unfolding. To illustrate this point, let $P$ be $\mu(\lambda R\lambda
x.x={\bf 0}\oplus(R~{}(s~{}x)))$. Clearly, $P$ denotes the singleton set
containing zero. There is also a MALL proof that $\forall x[Px\supset{\rm
Nature}~{}x]$, but there is no (cut-free) proof of this theorem that uses
unfolding instead of the more general induction rule: just using unfoldings
leads to an unbounded proof search attempt, which follows the following
outline.

$\vdash\overline{P~{}y},{\rm Nature}~{}y\lx@proof@logical@and\vdash{\rm
Nature}~{}{\bf 0}\vdash\overline{P~{}(s~{}y)},{\rm
Nature}~{}y\vdash\overline{P~{}(s~{}(s~{}y))},{\rm Nature}~{}y\vdots$

Although proof search can contain potentially unbounded branches, we can still
use the proof search concepts of unification and non-deterministic search to
compute the value within a singleton. We now define a non-deterministic
algorithm to do exactly that. The _state_ of this algorithm is a triple of the
form

$\langle x_{1},\ldots,x_{n}\,;~{}B_{1},\ldots,B_{m}\,;~{}t\rangle,$

where $t$ is a term, $B_{1},\ldots,B_{m}$ is a multiset of ${\bf P}_{1}$
formulas, and all variables free in $t$ and in the formulas
$B_{1},\ldots,B_{m}$ are in the set of variables $x_{1},\ldots,x_{n}$. A
_success state_ is one of the form $\langle\cdot\,;~{}\cdot\,;~{}t\rangle$
(that is, when $n=m=0$): such a state is said to have _value_ $t$.

Given the state $S=\langle\Sigma\,;~{}B_{1},\ldots,B_{m}\,;~{}t\rangle$ with
$m\geq 1$, we can non-deterministically select one of the $B_{i}$ formulas:
for the sake of simplicity, assume that we have selected $B_{1}$. We define
the transition $S\Rightarrow S^{\prime}$ of state $S$ to state $S^{\prime}$ by
a case analysis of the top-level structure of $B_{1}$.

  * •

If $B_{1}$ is $u=v$ and the terms $u$ and $v$ are unifiable with most general
unifier $\theta$, then we transition to
$\langle\Sigma\theta\,;~{}B_{2}\theta,\ldots,B_{m}\theta\,;~{}t\theta\rangle.$

  * •

If $B_{1}$ is $B\mathrel{\otimes}B^{\prime}$ then we transition to
$\langle\Sigma\,;~{}B,B^{\prime},B_{2},\ldots,B_{m}\,;~{}t\rangle$.

  * •

If $B_{1}$ is $B\mathrel{\oplus}B^{\prime}$ then we transition to either
$\langle\Sigma\,;~{}B,B_{2},\ldots,B_{m}\,;~{}t\rangle$ or
$\langle\Sigma\,;~{}B^{\prime},B_{2},\ldots,B_{m}\,;~{}t\rangle$.

  * •

If $B_{1}$ is $\mu B\vec{t}$ then we transition to $\langle\Sigma\,;~{}B(\mu
B)\vec{t},B_{2},\ldots,B_{m}\,;~{}t\rangle$.

  * •

If $B_{1}$ is $\exists y.~{}B~{}y$ then we transition to
$\langle\Sigma,y\,;~{}B~{}y,B_{2},\ldots,B_{m}\,;~{}t\rangle$ assuming that
$y$ is not in $\Sigma$.

This non-deterministic algorithm is essentially applying left-introduction
rules in a bottom-up fashion and, if there are two premises, selecting (non-
deterministically) just one premise to follow.

###### Lemma 4.1

Assume that $P$ is a ${\bf P}_{1}$ expression of type $i\rightarrow o$ and
that $\exists y.Py$ has a MALL proof. There is a sequence of transitions from
the initial state $\langle y\,;~{}P~{}y\,;~{}y\rangle$ to a success state with
value $t$ such that $P~{}t$ has a MALL proof.

###### Proof 4.2

An _augmented state_ is a structure of the form
$\langle\Sigma{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\theta}\,;~{}B_{1}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\Xi_{1}},\ldots,B_{m}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\Xi_{m}}\,;~{}t\rangle,$
where

  * •

$\theta$ is a substitution with domain equal to $\Sigma$ and which has no free
variables in its range, and

  * •

for all $i\in\\{1,\ldots,m\\}$, $\Xi_{i}$ is a MALL proof of $\theta(B_{i})$.

Clearly, if we strike out the augmented items (in red), we are left with a
regular state. Given that we have a MALL proof of $\exists y.Py$, we must have
a MALL proof $\Xi_{0}$ of $P~{}t$ for some term $t$. Note that there is no
occurrence of the induction rule in $\Xi_{0}$. We now set the initial
augmented state to $\langle
y{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,[y\mapsto
t]}\,;~{}Py{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\Xi_{0}}\,;~{}y\rangle$.
As we detail now, the proof structures $\Xi_{i}$ provide oracles that steer
this non-deterministic algorithm to a success state with value $t$. Given the
augmented state
$\langle\Sigma{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\theta}\,;~{}B_{1}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\Xi_{1}},\ldots,B_{m}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\Xi_{m}}\,;~{}s\rangle$,
we consider selecting the first pair
$B_{1}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\Xi_{1}}$
and consider the structure of $B_{1}$.

  * •

If $B_{1}$ is $B^{\prime}\mathrel{\otimes}B^{\prime\prime}$ then the last
inference rule of $\Xi_{1}$ is $\mathrel{\otimes}$ with premises
$\Xi^{\prime}$ and $\Xi^{\prime\prime}$, and we make a transition to
$\langle\Sigma{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\theta}\,;~{}B^{\prime}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\Xi^{\prime}},B^{\prime\prime}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\Xi^{\prime\prime}},\ldots,B_{m}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\Xi_{m}}\,;~{}s\rangle$.

  * •

If $B_{1}$ is $B^{\prime}\mathrel{\oplus}B^{\prime\prime}$ then the last
inference rule of $\Xi_{1}$ is $\mathrel{\oplus}$, and that rule selects
either the first or the second disjunct. In either case, let $\Xi^{\prime}$ be
the proof of its premise. Depending on which of these disjuncts is selected,
we make a transition to either
$\langle\Sigma{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\theta}\,;~{}B^{\prime}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\Xi^{\prime}},B_{2}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\Xi_{2}},\ldots,B_{m}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\Xi_{m}}\,;~{}s\rangle$
or
$\langle\Sigma{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\theta}\,;~{}B^{\prime\prime}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\Xi^{\prime}},B_{2}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\Xi_{2}},\ldots,B_{m}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\Xi_{m}}\,;~{}s\rangle$,
respectively.

  * •

If $B_{1}$ is $\mu B\vec{t}$ then the last inference rule of $\Xi_{1}$ is
$\mu$. Let $\Xi^{\prime}$ be the proof of the premise of that inference rule.
We make a transition to
$\langle\Sigma{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\theta}\,;~{}B(\mu
B)\vec{t}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\Xi^{\prime}},B_{2}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\Xi_{2}},\ldots,B_{m}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\Xi_{m}}\,;~{}s\rangle$.

  * •

If $B_{1}$ is $\exists y.~{}B~{}y$ then the last inference rule of $\Xi_{1}$
is $\exists$. Let $r$ be the substitution term used to introduce this
$\exists$ quantifier and let $\Xi^{\prime}$ be the proof of the premise of
that inference rule. Then, we make a transition to
$\langle\Sigma,w{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\theta\mathbin{\circ}\varphi}\,;~{}B~{}w{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\Xi^{\prime}},B_{2}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\Xi_{2}},\ldots,B_{m}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\Xi_{m}}\,;~{}s\rangle$,
where $w$ is a variable not in $\Sigma$ and $\varphi$ is the substitution
$[w\mapsto r]$. Here, we assume that the composition of substitutions
satisfies the equation $(\theta\mathbin{\circ}\varphi)(x)=\varphi(\theta(x))$.

  * •

If $B_{1}$ is $u=v$ and the terms $u$ and $v$ are unifiable with most general
unifier $\varphi$, then we make a transition to
$\langle\Sigma\varphi{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\rho}\,;~{}\varphi(B_{2}){\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\Xi_{2}},\ldots,\varphi(B_{m}){\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\,\mathrel{|}\,\Xi_{m}}\,;~{}(\varphi
t)\rangle$ where $\rho$ is the substitution such that
$\theta=\varphi\mathbin{\circ}\rho$.

We must show that the transition is made to an augmented state in each of
these cases. This is easy to show in all but the last two rules above. In the
case of the transition due to $\exists$, we know that $\Xi^{\prime}$ is a
proof of $\theta(B~{}r)$, but that formula is simply $\varphi(\theta(B~{}w))$
since $w$ is new and $r$ contains no variables free in $\Sigma$. In the case
of the transition due to equality, we know that $\Xi_{1}$ is a proof of the
formula $\theta(u=v)$ which means that $\theta u$ and $\theta v$ are the same
terms and, hence, that $u$ and $v$ are unifiable and that $\theta$ is a
unifier. Let $\varphi$ be the most general unifier of $u$ and $v$. Thus, there
is a substitution $\rho$ such that $\theta=\varphi\mathbin{\circ}\rho$ and,
for $i\in\\{2,\ldots,m\\}$, $\Xi_{i}$ is a proof of
$(\varphi\mathbin{\circ}\rho)(B_{i})$. Finally, termination of this algorithm
is ensured since the number of occurrences of inference rules in the included
proofs decreases at every step of the transition. Since we have shown that
there is an augmented path that terminates, we have that there exists a path
of states to a success state with value $t$.

This lemma ensures that our search algorithm can compute a member from a non-
empty set, given a MALL proof that that set is non-empty. We can now prove the
following theorem about singleton sets. We abbreviate $(\exists
x.P~{}x)\land(\forall x_{1}\forall x_{2}.P~{}x_{1}\supset P~{}x_{2}\supset
x_{1}=x_{2})$ by $\exists!x.P~{}x$ in the following theorem.

###### Theorem 4.3

Assume that $P$ is a ${\bf P}_{1}$ expression of type $i\rightarrow o$ and
that $\exists!y.Py$ has a MALL proof. There is a sequence of transitions from
the initial state $\langle y\,;~{}P~{}y\,;~{}y\rangle$ to a success state of
value $t$ if and only if $P~{}t$ has a MALL proof.

###### Proof 4.4

Given a (cut-free) MALL proof of $\exists!y.Py$, that proof contains a MALL
proof of $\exists y.Py$. Since this formula is ${\bf P}_{1}$, there is a MALL
proof for $\exists y.Py$. The forward direction is immediate: given a sequence
of transitions from the initial state $\langle y\,;~{}P~{}y\,;~{}y\rangle$ to
the success state $\langle\cdot\,;~{}\cdot\,;~{}t\rangle$, it is easy to build
a MALL proof of $P~{}t$. Conversely, assume that there is a MALL proof of
$P~{}t$ for some term $t$. By conservativity, there is a MALL proof of $P~{}t$
and, hence, of $\exists y.P~{}y$. By Lemma 4.1, there is a sequence of
transitions from initial state $\langle y\,;~{}P~{}y\,;~{}y\rangle$ to the
success state $\langle\cdot\,;~{}\cdot\,;~{}s\rangle$, where $P~{}s$ has a
MALL proof. Given that the three formulas $Pt$ and $Ps$ and $\forall
x_{1}\forall x_{2}.P~{}x_{1}\supset P~{}x_{2}\supset x_{1}=x_{2}$, the
admissibility of cut for MALL allows us to conclude that $t=s$.

Thus, a (naive) proof-search algorithm involving both unification and non-
deterministic search is sufficient for computing the functions encoded in
relations in this setting.

##  5 The totality of the Ackermann function

The question of the expressivity of MALL has been analyzed by Baelde [2,
Section 3.5], who provided a lower bound to it by characterizing a subset of
MALL where proofs can be interpreted as primitive recursive functions, and cut
elimination corresponds to computing those functions. The ideas behind the
encoding can be used in order to express primitive recursive functions as
fixpoints and provide proofs of the totality of these functions in a similar
fashion to what we did for the $plus$ relation. However, Baelde noted that
this encoding is insufficient for a computational interpretation of
Ackermann’s function. We can add that it is also insufficient to obtain a
proof that the underlying relation represents a total function.

We show here a different method, based on the extension to
$\hbox{MALL}(\mathord{\mathop{!}},\mathord{\mathop{?}})$ provided in Section
3.4, that allows us to prove the totality of Ackermann’s function. The
encoding of Ackermann’s function in MALL is based on the following relational
specification.

$\begin{split}ack&=\mu(\lambda ack\lambda m\lambda n\lambda
a(m=0\mathrel{\otimes}a=s~{}n)\\\ &\mathrel{\oplus}\exists
p(m=s~{}p\mathrel{\otimes}n=0\mathrel{\otimes}ack~{}p~{}(s~{}0)~{}a)\\\
&\mathrel{\oplus}\exists p\exists q\exists
b(m=s~{}p\mathrel{\otimes}n=s~{}q\mathrel{\otimes}ack~{}m~{}q~{}b\mathrel{\otimes}ack~{}p~{}b~{}a))\end{split}$

In order to prove that this three-place relation determines a total function,
we need to prove _determinacy_ (that the first two argument uniquely determine
the third argument) and _totality_ (that for every choice of the first two
arguments, there exists a value for the third argument). Here we focus on
totality since the proof of determinacy is simpler and more straightforward.
The formula stating totality that we wish to prove is the following.

$\forall m\forall n(nat~{}m\multimap nat~{}n\multimap\exists
a.~{}(ack~{}m~{}n~{}a\mathrel{\otimes}nat~{}a))$

We will now illustrate a proof of this formula. In doing so, we will highlight
the crucial use of the encoded exponentials available in
$\hbox{MALL}(\mathord{\mathop{!}},\mathord{\mathop{?}})$. For greater clarity,
we will use $\multimap$ as a shorthand, and we will keep the retain the
overline syntax for negation instead of computing the explicit De Morgan
duality. The proof begins by introducing the universal quantifiers and then
applying twice the $\mathrel{\invamp}$ rule:

$\forall m\forall n(nat~{}m\multimap nat~{}n\multimap\exists
a.~{}ack~{}m~{}n~{}a)\vdash\overline{nat~{}m},\overline{nat~{}n},\exists
a.~{}ack~{}m~{}n~{}a$

At this point, we need to use the induction rule twice with the
$\overline{nat~{}n}$ and $\overline{nat~{}m}$ formulas. The invariants we
introduce for these inductions will be the places where we exploit the
encoding of the exponentials. In the first induction, we use as invariant the
negation of the remaining context of the sequent with a $\mathord{\mathop{!}}$
added, that is $\overline{\lambda m\mathord{\mathop{!}}(\forall
n~{}nat~{}n\multimap\exists a(ack~{}m~{}n~{}a\mathrel{\otimes}nat~{}a))}$.
This invariant needs to be contracted on at a later stage of the proof, hence
the need for the exponential. The left premise of the $\nu$ rule is
immediately verified, since the invariant starts with a $\mathord{\mathop{?}}$
which we can derelict away, and we can conclude immediately after by using the
fact that a generalized initial rule $\vdash\Gamma,\Gamma^{\bot}$ is
admissible in MALL.333If $\Gamma$ is the multiset $\\{B_{1},\ldots,B_{n}\\}$
then $\Gamma^{\bot}$ is
$\overline{B_{1}}\mathrel{\otimes}\cdots\mathrel{\otimes}\overline{B_{n}}\\}$.
The right premise of the $\nu$ rule then yields the base and inductive steps.
In the base case, we need to prove $\vdash\mathord{\mathop{!}}(\forall
n~{}nat~{}n\multimap\exists a(ack~{}{\bf
0}~{}n~{}a\mathrel{\otimes}nat~{}a))$, and we do this by promoting away the
exponential and then unfolding the base case of the $ack$ definition. The
inductive step gives us:

$\vdash\overline{\mathord{\mathop{!}}(\forall n~{}nat~{}n\multimap\exists
a(ack~{}x~{}n~{}a\mathrel{\otimes}nat~{}a))},\mathord{\mathop{!}}(\forall
n~{}nat~{}n\multimap\exists
a(ack~{}(s~{}x)~{}n~{}a\mathrel{\otimes}nat~{}a))\vdash\overline{\mathord{\mathop{!}}(\forall
n~{}nat~{}n\multimap\exists
a(ack~{}x~{}n~{}a\mathrel{\otimes}nat~{}a))},\overline{nat~{}n},\exists
a(ack~{}(s~{}x)~{}n~{}a\mathrel{\otimes}nat~{}a)$

Thanks to the fact that the invariant starts with a question mark, we can
promote the dualized invariant and continue the proof. We now have exposed
once again the dualized $\overline{nat~{}n}$ predicate, over which we can
perform the second induction. As before, we take the entire sequent
(abstracted over $n$) and negate it, but this time there is no need to add
another occurrence of an exponential, obtaining the invariant

$\overline{\lambda k\mathord{\mathop{!}}(\forall n~{}nat~{}n\multimap\exists
a(ack~{}x~{}n~{}a\mathrel{\otimes}nat~{}a))\multimap\exists
a(ack~{}(s~{}x)~{}k~{}a\mathrel{\otimes}nat~{}a)}.$

The left hand premise of the $\nu$ rule is now exactly an instance of
$\vdash\Gamma,\Gamma^{\bot}$. The base case and the inductive steps for this
second induction remove to be proved. The base case (where we need to prove
the invariant for $k$ being $0$) is again proved by a routine inspection of
the definition of $ack$. The antecedent part of the invariant can be used
directly since it starts with $\mathord{\mathop{?}}$.

The final step is the inductive case, where we need to prove the invariant for
$(s~{}k)$ given the invariant for $k$: that is, we need to prove the sequent

$\begin{split}\vdash&\overline{{\mathord{\mathop{!}}\,\forall
x(nat~{}x\multimap\exists
a(ack~{}y~{}x~{}a\mathrel{\otimes}nat~{}a))}\multimap\exists
a(ack~{}(s~{}y)~{}k~{}a\mathrel{\otimes}nat~{}a)},\\\
&\mathord{\mathop{!}}\,\forall x(nat~{}x\multimap\exists
a(ack~{}y~{}x~{}a\mathrel{\otimes}nat~{}a))\multimap\exists
a(ack~{}(s~{}y)~{}(s~{}k)~{}a\mathrel{\otimes}nat~{}a)\end{split}$

Introducing the second linear implication gives the dual of the antecedent,
which starts with $\mathord{\mathop{?}}$ and, hence, is a contractable copy of
the invariant from the previous induction:

$\mathord{\mathop{?}}\overline{\forall x(nat~{}x\multimap\exists
a(ack~{}y~{}x~{}a\mathrel{\otimes}nat~{}a))}.$

The entire reason to be using
$\hbox{MALL}(\mathord{\mathop{!}},\mathord{\mathop{?}})$ to state invariants
in this proof is to make this contraction possible. Now we can decompose the
new invariant, which is a universally quantified implication, and use the two
copies we have obtained: one copy is provided to the antecedent of the
implication and one copy is used to continue the proof. The two premises of
this occurrence of the $\nu$ rule are:

$\begin{split}\vdash&{\mathord{\mathop{!}}\forall x(nat~{}x\multimap\exists
a(ack~{}y~{}x~{}a\mathrel{\otimes}nat~{}a))},\mathord{\mathop{?}}\overline{\forall
x(nat~{}x\multimap\exists
a(ack~{}y~{}x~{}a\mathrel{\otimes}nat~{}a))}\\\\[4.0pt]
\vdash&\overline{\exists
a(ack~{}(s~{}y)~{}k~{}a\mathrel{\otimes}nat~{}a)},\mathord{\mathop{?}}\overline{\forall
x(nat~{}x\multimap\exists a(ack~{}y~{}x~{}a\mathrel{\otimes}nat~{}a))},\exists
a(ack~{}(s~{}y)~{}(s~{}k)~{}a\mathrel{\otimes}nat~{}a)\end{split}$

The first one is immediately proved thanks to the fact that the exponentials
are dual. The second sequent is also easily proved by unfolding the definition
of $ack$ using its third case; the exponential can be derelicted, and all the
arising premises can be proved without the exponentials.

Given that we have a $\hbox{MALL}(\mathord{\mathop{!}},\mathord{\mathop{?}})$
proof (hence, also a MALL proof) of the totality of the Ackermann relation, we
can use the proof search method in Section 4 in order to actually compute the
Ackermann function. Additionally, from the cut-elimination theorem of MALL, we
obtain an interpretation as a computation via proof normalization.

##  6 $\hbox{LK}_{p}^{+}$ contains Peano Arithmetic

The consistency of MALL follows immediately from its cut-elimination theorem.
It is worth noting that adding contraction to some consistent proof systems
with weak forms of fixed points can make the new proof system inconsistent.
For example, both Girard [23] and Schroeder-Heister [24] describe a variant of
linear logic with unfolding fixed points that is consistent, but when
contraction is added, it becomes inconsistent. In their case, negations are
allowed in the body of fixed point definitions. (See also [25].) The following
theorem proves that adding contraction to MALL does not lead to inconsistency.

###### Theorem 6.1

$\hbox{LK}_{p}^{+}$ is consistent: that is, the empty sequent is not provable.

###### Proof 6.2

Consider the sequent $\vdash B_{1},\ldots,B_{n}$, where $n\geq 0$ and where
all the free variables of formulas in this sequent are contained in the list
of variables $x_{1},\ldots,x_{m}$ ($m\geq 0$) all of type $\iota$. We say that
this sequent is _true_ if for all substitutions $\theta$ that send the
variables $x_{1},\ldots,x_{m}$ to closed terms of type $\iota$ (numerals), the
disjunction of the unpolarized versions of the formula $B_{1}\theta,\ldots
B_{n}\theta$ is _true_ (in the standard model). A straightforward induction on
the structure of $\hbox{LK}_{p}^{+}$ proofs shows that all of the inference
rules in Figures 3, 3, and 3 are sound (meaning that when the premises are
true, the conclusion is true). Thus we have the following soundness result: if
the sequent $\vdash B_{1},\ldots,B_{n}$ is provable in $\hbox{LK}_{p}^{+}$,
then that sequent is true. As a result, the empty sequent is not provable.

We now show that Peano arithmetic is contained in $\hbox{LK}_{p}^{+}$. The
terms of Peano arithmetic are identical to the terms introduced in Section 2
for encoding numerals. The formulas of Peano arithmetic are similar to
unpolarized formulas except that they are built from $=$, $\neq$, the
propositional logical connectives $\land$, tt, $\lor$, ff, and the two
quantifiers $\hat{\forall}$ and $\hat{\exists}$ (both of type $(i\rightarrow
o)\rightarrow o$). Such formulas can be _polarized_ to get a polarized formula
as described in Section 2.3. Finally, all occurrences of $\hat{\forall}$ and
$\hat{\exists}$ are replaced by $\lambda B.\forall x~{}(\overline{{\rm
Nature}~{}x}\mathrel{\invamp}(Bx))$ and $\lambda B.\exists x~{}({\rm
Nature}~{}x\mathrel{\otimes}(Bx))$, respectively. Here, ${\rm Nature}$ is an
abbreviation for $\mu\lambda N\lambda n(n={\bf 0}\mathrel{\oplus}\exists
m(n=(s~{}m)\mathrel{\otimes}N~{}m)))$.

Most presentations of Peano arithmetic incorporate the addition and
multiplication of natural numbers as either binary function symbols or as
three place relations. Formally, we will avoid introducing the extra
constructors $+$ and $\cdot$, and choose to encode addition and
multiplications as relations. In particular, these are defined as the fixed
point expressions plus and mult given in Section 3. The relation between these
two presentation is such that the equality $x+y=w$ corresponds to $\hbox{\sl
plus\/}\,x\,y\,w$ and the equality $x\cdot y=w$ corresponds to $\hbox{\sl
mult\/}\,x\,y\,w$. A more complex expression, such as $\forall x\forall
y.~{}(x\cdot s\,y=(x\cdot y+x))$, can similarly be written as either

$\forall x\forall y\forall u.~{}\hbox{\sl
mult\/}~{}x~{}(s\,y)~{}u\supset~{}\forall v.~{}\hbox{\sl
mult\/}~{}x~{}y~{}v\supset\forall w.\hbox{\sl plus\/}~{}v~{}x~{}w\supset u=w$

or as

$\forall x\forall y\exists u.~{}\hbox{\sl
mult\/}~{}x~{}(s\,y)~{}u\land~{}\exists v.~{}\hbox{\sl
mult\/}~{}x~{}y~{}v\land\exists w.\hbox{\sl plus\/}~{}v~{}x~{}w\land u=w.$

A general approach to making such an adjustment to the syntax of expressions
using functions symbols to expressions using relations is discussed from a
proof-theoretic perspective in [26].

Proof in Peano arithmetic can be specified using the following six axioms

$\begin{array}[]{l@{\qquad}l}\forall x.~{}(s\,x)\neq{\bf 0}&\forall x\forall
y.~{}(x+s\,x)=s(x+y)\\\ \forall x\forall y.~{}(s\,x=s\,y)\supset(x=y)&\forall
x.~{}(x\cdot{\bf 0}={\bf 0})\\\ \forall x.~{}(x+{\bf 0}=x)&\forall x\forall
y.~{}(x\cdot s\,y=(x\cdot y+x))\end{array}$

and the axiom scheme (which we write using the predicate variable $A$)

$(A{\bf 0}\land\forall x.~{}(Ax\supset A(s~{}x)))\supset\forall x.\,Ax.$

We also admit the usual inference rules of modus ponens and universal
generalization.

######  Theorem 6.3 ($\hbox{LK}_{p}^{+}$ contains Peano arithmetic)

Let $Q$ be any unpolarized formula and let $\hat{Q}$ be a polarized version of
$Q$. If $Q$ is provable in Peano arithmetic then $\hat{Q}$ is provable in
$\hbox{LK}_{p}^{+}$.

###### Proof 6.4

It is easy to prove that mult and $plus$ describe precisely the multiplication
and addition operations on natural numbers. Given the presence of contraction
and weakening, it is possible to show the equivalence of all the different
polarizations of $Q$. Furthermore, the translations of the Peano Axioms can
all be proved in $\hbox{LK}_{p}^{+}$. We illustrate just one of these axioms
here: a polarization of the translation of the induction scheme is

$\overline{\big{(}A{\bf 0}\mathrel{\otimes}\forall
x.~{}(\overline{nat~{}x}\mathrel{\invamp}\overline{Ax}\mathrel{\invamp}A(s~{}x))\big{)}}\mathrel{\invamp}\forall
x.~{}(\overline{nat~{}x}\mathrel{\invamp}Ax)$

An application of the $\nu$ rule to the second occurrence of
$\overline{nat~{}x}$ can provide an immediate proof of this axiom. Finally,
the cut rule in $\hbox{LK}_{p}^{+}$ allows us to encode the inference rule of
modus ponens.

##  7 Conservativity results for linearized arithmetic

A well-known result in the study of arithmetic is the following.

> Peano arithmetic is $\Pi_{2}$-conservative over Heyting arithmetic: if Peano
> arithmetic proves a $\Pi_{2}$-formula $A$, then $A$ is already provable in
> Heyting arithmetic [27].

This result inspires the two conservativity theorem we prove in this section.
The following theorem is our first conservativity result of (cut-free)
$\hbox{LK}_{p}$ over MALL.

###### Theorem 7.1

$\hbox{LK}_{p}$ is conservative over MALL for ${\bf P}_{1}$-formulas. That is,
if $B$ is a ${\bf P}_{1}$ formula, then $\vdash B$ has a $\hbox{LK}_{p}$ proof
if and only if $\vdash B$ has a MALL proof.

###### Proof 7.2

The converse direction of this theorem is immediate. Now consider a sequent of
the form $\vdash B_{1},\ldots,B_{n}$ that contains only formulas from ${\bf
P}_{1}$. A straightforward argument shows that if this sequent has a
$\hbox{LK}_{p}$ proof then there is an $i\in\\{1,\ldots,n\\}$ so that $\vdash
B_{i}$ has a MALL proof.

Our next conservativity result requires restricting the complexity of
invariants used in the induction rule $\nu$. We say that a sequent has a
$\hbox{LK}_{p}({\bf P}_{1})$ proof if it has a $\hbox{LK}_{p}$ proof in which
all invariants of the proof are ${\bf P}_{1}$. This restriction on proofs is
similar to the restriction that yields the $I\Sigma_{1}$ fragment of Peano
Arithmetic [28].

###### Theorem 7.3

$\hbox{LK}_{p}({\bf P}_{1})$ is conservative over MALL for ${\bf
N}_{2}$-formulas. That is, if $B$ is a ${\bf N}_{2}$-formula such that $\vdash
B$ has a $\hbox{LK}_{p}({\bf P}_{1})$ proof, then $\vdash B$ has a MALL proof.

The proof of this result would be aided greatly if we had a focusing theorem
for $\hbox{LK}_{p}$. If we take the focused proof system for MALL given in [3,
1] and add contraction and weakening in the usual fashion, we have a natural
candidate for a focused proof system for $\hbox{LK}_{p}$. However, the
completeness of that proof system is currently open. As Girard points out in
[29], the completeness of such a focused (cut-free) proof system would allow
the extraction of the constructive content of classical $\Pi^{0}_{2}$
theorems, and we should not expect such a result to follow from the usual ways
that we prove cut-elimination and the completeness of focusing. As a result of
not possessing such a focused proof system for $\hbox{LK}_{p}$, we must now
reproduce aspects of focusing in order to prove Theorem 7.3.

We find it convenient to introduce the following inference rule.

$\vdash\Gamma,\nu B\vec{t}\vdash\Gamma,S\vec{t},U\vec{t}\quad\vdash
BU\vec{x},\overline{U\vec{x}}\quad\vdash BS\vec{x},\overline{S\vec{x}}$

This rule is justified by the following combination of $\nu$ and contraction
rules.

$\vdash\Gamma,\nu B\vec{t}\vdash\Gamma,\nu B\vec{t},\nu
B\vec{t}\lx@proof@logical@and\vdash\Gamma,\nu
B\vec{t},S\vec{t}\vdash\Gamma,S\vec{t},U\vec{t}\quad\vdash
BU\vec{x},\overline{U\vec{x}}\vdash BS\vec{x},\overline{S\vec{x}}$

Since we are working within $\hbox{LK}_{p}({\bf P}_{1})$, the invariants $S$
and $U$ are ${\bf P}_{1}$.

If $\Gamma_{1}$ and $\Gamma_{2}$ are reduced sequents, we say that
$\Gamma_{1}$ _contains_ $\Gamma_{2}$ if $\Gamma_{2}$ is a sub-multiset of
$\Gamma_{1}$. A _reduced sequent_ is a sequent that contains only ${\bf
N}_{1}$, ${\bf P}_{1}$, and ${\bf N}_{2}$ formulas. We say that a reduced
sequent is a _pointed_ sequent if it contains exactly one formula that is
either ${\bf P}_{1}$ or ${\bf N}_{2}$.

Finally, we need two additional notions. A _positive region_ is a (cut-free)
$\hbox{LK}_{p}({\bf P}_{1})$ proof that contains only the inference rules
$\mu\nu$, contraction, weakening, and the introduction rules for the positive
connectives. A _negative region_ is a (cut-free) $\hbox{LK}_{p}({\bf P}_{1})$
_possibly partial_ proof in which the open premises are all reduced sequent
and where the only inference rules are introductions for negative connectives
plus the $C\nu\nu$ rule.

###### Lemma 7.4

If a reduced sequent $\Gamma$ has a positive region proof then $\Gamma$
contains $\Gamma^{\prime}$ such that $\Gamma^{\prime}$ is a pointed sequent
and has a MALL proof.

###### Proof 7.5

This proof is a simple generalization of the proof of Theorem 7.1.

###### Lemma 7.6

If every premise of a negative region contains a pointed sequent with a MALL
proof, then the conclusion of the negative region contains a pointed sequent
with a MALL proof.

###### Proof 7.7

This proof is by induction on the height of the negative region. The most
interesting case to examine is the one where the last inference rule of the
negative region is the $C\nu\nu$ rule. Referring to the inference rule
displayed above, the inductive hypothesis ensures that the reduced sequent
$\vdash\Gamma,S\vec{t},U\vec{t}$ contains a pointed sequent $\Delta,C$ where
$\Delta$ is a multiset of ${\bf N}_{1}$ formulas in $\Gamma$ and where the
formula $C$ (that is either ${\bf P}_{1}$ or ${\bf N}_{2}$) is either a member
of $\Gamma$ or is equal to either $S\vec{t}$ or $U\vec{t}$. In the first case,
$\Delta,C$ is also contained in the endsequent $\Gamma,\nu B\vec{t}$. In the
second case, we have one of the following proofs:

$\vdash\Gamma,\nu B\vec{t}\lx@proof@logical@and\vdash\Delta,S\vec{t}\vdash
BS\vec{x},\overline{S\vec{x}}\qquad\vdash\Gamma,\nu
B\vec{t}\lx@proof@logical@and\vdash\Delta,U\vec{t}\vdash
BU\vec{x},\overline{U\vec{x}}$

depending on whether or not $C$ is $S\vec{t}$ or $U\vec{t}$.

###### Lemma 7.8

If the reduced sequent $\Gamma$ has a cut-free $\hbox{LK}_{p}({\bf P}_{1})$
proof then $\Gamma$ has a proof that can be divided into a negative region
that proves $\Gamma$ in which all its premises have positive region proofs.

###### Proof 7.9

This lemma is proved by appealing to the permutation of inference rules. As
shown in [3], the introduction rules for negative connectives permute down
over all inference rules in MALL. Not considered in that paper is how such
negative introduction rules permute down over contractions. It is easy to
check that such permutations do, in fact, happen except in the case of the
$\nu$ rule. In general, contractions below a $\nu$ rule will not permute
upwards, and, as a result, the negative region is designed to include the
$C\nu\nu$ rule (where contraction is stuck with the $\nu$ rule). As a result,
negative rules (including $C\nu\nu$) permute down while contraction and
introductions of positive connectives permute upward. This gives rise to the
two-region proof structure.

By combining the results above, we have a proof of Theorem 7.3. Note that when
a relational specification is given by a ${\bf P}_{1}$ specification, the
_totality_ and _determinacy_ formulas related to that specification (see
Section 4) are ${\bf N}_{2}$ formulas. The proof of the totality of the
Ackermann function discussed in Section 5 goes beyond Theorem 7.3 by using
complex invariants that include universal quantifiers, implications, and the
fixed point definitions for the exponential. We can also strengthen Theorem
4.3 to be a theorem about provability in $\hbox{LK}_{p}$ instead of in MALL.

###### Theorem 7.10

Assume that $P$ is a ${\bf P}_{1}$ expression of type $i\rightarrow o$ and
that $\exists!y.Py$ has a $\hbox{LK}_{p}$ proof. There is a sequence of
transitions from the initial state $\langle y\,;~{}P~{}y\,;~{}y\rangle$ to a
success state of value $t$ if and only if $P~{}t$ has a $\hbox{LK}_{p}$ proof.

###### Proof 7.11

Given a (cut-free) $\hbox{LK}_{p}$ proof of $\exists!y.Py$, that proof
contains a $\hbox{LK}_{p}$ proof of $\exists y.Py$. Since this formula is
${\bf P}_{1}$, there is a MALL proof for $\exists y.Py$. The result follows
using Lemma 4.1 and Theorem 7.1.

##  8 Related work

The main difference between the hierarchy of ${\bf P}_{n}/{\bf N}_{n}$
formulas used in this paper and the familiar classes of formulas in the
arithmetic hierarchy (based on quantifier alternations) is the occurrences of
fixed points within formulas. In that regard, our principle proof systems MALL
and $\hbox{LK}_{p}$ are probably more easily related to the extension of Peano
Arithmetic based on general inductive definitions in [30].

Circular proof systems for logics with fixed points have received much
attention in recent years, especially within the context of linear logic [31,
32, 10] and intuitionistic logic [33]. Such proof systems generally eschew all
first-order term structures (along with first-order quantification). They also
eschew the use of explicit invariants and use cycles within proofs as an
implicit approach to discovering invariants.

The logic MALL was developed along with the construction of the Bedwyr model
checker [34]. Although that model checker was designed to prove judgments in
classical logic, it became clear that only linear logic principles were needed
to describe most of its behaviors. The paper [19] illustrates how MALL and its
(partial) implementation in Bedwyr can be used to determine standard model-
checking problems such as reachability and simulation. A small theorem proving
implementation, based on the focused proof system MALL, is described in [35]:
that prover was capable of proving automatically many of the theorems related
to establishing determinacy and totality of ${\bf P}_{1}$ relational
specifications.

Most of the results here are taken from Chapter 3 of the first author’s Ph.D.
dissertation [36].

##  9 Conclusions

In this paper, we have started to explore MALL as a linearized version of
arithmetic in a way that is similar to using Heyting Arithmetic as a
constructive version of arithmetic. In particular, we have considered three
different proof systems. The first is MALL, for which a cut-admissibility
theorem is known. The other two are natural variants of MALL that introduce
into MALL the rules of contraction and weakening, yielding $\hbox{LK}_{p}$, as
well as cut, yielding $\hbox{LK}_{p}^{+}$. We demonstrate that the third proof
system is consistent and powerful enough to encompass all of Peano Arithmetic.
While it is known that MALL can prove the totality of primitive recursive
function specifications, we demonstrate that the non-primitive recursive
Ackermann function can also be proved total in MALL. We have also demonstrated
that if we can prove in $\hbox{LK}_{p}$ that a certain ${\bf P}_{1}$
relational specification defines a function, then a simple proof search
algorithm can compute that function using unification and backtracking search.
This approach differs from the proof-as-program interpretation of a
constructive proof of totality of a relational specification.

Acknowledgment: We thank the anonymous reviewers of an earlier draft of this
paper for their valuable comments. We also thank Anupam Das for several
conversations and suggestions that helped shape this paper’s the overall
structure and results.

## References

  * [1] Baelde D, Miller D.  Least and greatest fixed points in linear logic.  In: Dershowitz N, Voronkov A (eds.), International Conference on Logic for Programming and Automated Reasoning (LPAR), volume 4790 of _LNCS_. 2007 pp. 92–106.  10.1007/978-3-540-75560-9_9.
  * [2] Baelde D.  A linear approach to the proof-theory of least and greatest fixed points.  Ph.D. thesis, Ecole Polytechnique, 2008.  URL http://arxiv.org/abs/0910.3383.
  * [3] Baelde D.  Least and greatest fixed points in linear logic.  _ACM Trans. on Computational Logic_ , 2012.  13(1):2:1–2:44.  10.1145/2071368.2071370.
  * [4] Gehlot V, Gunter C.  Normal Process Representatives.  In: 5th Symp. on Logic in Computer Science. IEEE Computer Society Press, Philadelphia, Pennsylvania, 1990 pp. 200–207.  10.1109/LICS.1990.113746.
  * [5] Kobayashi N, Yonezawa A.  Asynchronous communication model based on linear logic.  _Formal Aspects of Computing_ , 1995.  7(2):113–149.  10.1007/BF01211602.
  * [6] Miller D.  The $\pi$-calculus as a theory in linear logic: Preliminary results.  In: Lamma E, Mello P (eds.), 3rd Workshop on Extensions to Logic Programming, number 660 in LNCS. Springer, Bologna, Italy, 1993 pp. 242–265.  10.1007/3-540-56454-3_13.
  * [7] Hodas J, Miller D.  Logic Programming in a Fragment of Intuitionistic Linear Logic.  _Information and Computation_ , 1994.  110(2):327–365.  10.1006/inco.1994.1036.
  * [8] Miller D.  Forum: A Multiple-Conclusion Specification Logic.  _Theoretical Computer Science_ , 1996.  165(1):201–232.  10.1016/0304-3975(96)00045-X.
  * [9] Girard JY.  Schrödinger’s cut: La logique à la lumière du quantique, 2021.  Unpublished., URL http://girard.perso.math.cnrs.fr/chat.pdf.
  * [10] Ehrhard T, Jafarrahmani F.  Categorical models of Linear Logic with fixed points of formulas.  In: 36th ACM/IEEE Symposium on Logic in Computer Science (LICS 2021), Jun 2021, Rome, Italy. IEEE, 2021 pp. 1–13.  10.1109/LICS52264.2021.9470664.
  * [11] Brotherston J, Simpson A.  Sequent calculi for induction and infinite descent.  _J. of Logic and Computation_ , 2011.  21(6):1177–1216.  10.1093/logcom/exq052.
  * [12] Simpson A.  Cyclic Arithmetic Is Equivalent to Peano Arithmetic.  In: Esparza J, Murawski AS (eds.), Foundations of Software Science and Computation Structures - 20th International Conference, FoSSaCS, volume 10203 of _LNCS_. 2017 pp. 283–300.  10.1007/978-3-662-54458-7_17.
  * [13] Das A.  On the logical complexity of cyclic arithmetic.  _Log. Methods Comput. Sci_ , 2020.  16(1).  10.4230/LIPIcs.FSCD.2021.29.
  * [14] Church A.  A Formulation of the Simple Theory of Types.  _J. of Symbolic Logic_ , 1940.  5:56–68.  10.2307/2266170.
  * [15] Das A, De A, Saurin A.  Decision problems for linear logic with least and greatest fixed points.  In: 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2022 10.4230/LIPIcs.FSCD.2022.20.
  * [16] Horne R, Padovani L.  A Logical Account of Subtyping for Session Types.  In: Castellani I, Scalas A (eds.), Proc. 14th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, PLACES 2023, volume 378 of _EPTCS_. 2023 pp. 26–37.  10.4204/EPTCS.378.3.
  * [17] Gentzen G.  Investigations into Logical Deduction.  In: Szabo ME (ed.), The Collected Papers of Gerhard Gentzen, pp. 68–131. North-Holland, Amsterdam, 1935.  10.1007/BF01201353.  Translation of articles that appeared in 1934-35. Collected papers appeared in 1969.
  * [18] Tärnlund SA.  Horn Clause Computability.  _BIT_ , 1977.  17:215–226.  10.1007/BF01932293.
  * [19] Heath Q, Miller D.  A proof theory for model checking.  _J. of Automated Reasoning_ , 2019.  63(4):857–885.  10.1007/s10817-018-9475-3.
  * [20] Clark KL.  Negation as failure.  In: Gallaire J, Minker J (eds.), Logic and Data Bases, pp. 293–322. Plenum Press, New York, 1978.  10.1007/978-1-4684-3384-5_11.
  * [21] Miller D, Viel A.  Proof search when equality is a logical connective.  _Annals of Mathematics and Artificial Intelligence_ , 2022.  90(5):523–535.  10.1007/s10472-021-09764-0.  _Special Issue on Theoretical and Practical Aspects of Unification_.
  * [22] Howard WA.  The formulae-as-type notion of construction, 1969.  In: Seldin JP, Hindley R (eds.), To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, pp. 479–490. Academic Press, New York, 1980.
  * [23] Girard JY.  A Fixpoint Theorem in Linear Logic, 1992.  An email posting to<EMAIL_ADDRESS>archived at https://www.seas.upenn.edu/~sweirich/types/archive/1992/msg00030.html.
  * [24] Schroeder-Heister P.  Rules of Definitional Reflection.  In: Vardi M (ed.), 8th Symp. on Logic in Computer Science. IEEE Computer Society Press, IEEE, 1993 pp. 222–232.  10.1109/LICS.1993.287585.
  * [25] Grishin VN.  Predicate and set-theoretic calculi based on logic without contractions.  _Izvestiya Rossiiskoi Akademii Nauk. Seriya Matematicheskaya_ , 1981\.  45(1):47–68.
  * [26] Gérard U, Miller D.  Separating Functional Computation from Relations.  In: Goranko V, Dam M (eds.), 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), volume 82 of _LIPIcs_. 2017 pp. 23:1–23:17.  10.4230/LIPIcs.CSL.2017.23.
  * [27] Friedman HM.  Classically and Intuitionistically Provably Recursive Functions.  In: Müller GH, Scott DS (eds.), Higher Order Set Theory, pp. 21–27. Springer Verlag, Berlin, 1978.  10.1007/BFb0103100.
  * [28] Paris JB, Kerby LAS.  $\Sigma_{n}$-Collection Schemas in Arithmetic.  In: Macintyre A, Pacholski L, Paris J (eds.), Logic Colloquium ’77, volume 96 of _Studies in logic and the foundations of mathematics_. North-Holland, 1978 pp. 199–209.
  * [29] Girard JY.  A new constructive logic: classical logic.  _Math. Structures in Comp. Science_ , 1991.  1:255–296.  10.1017/S0960129500001328.
  * [30] Möllerfeld M.  Generalized inductive definitions.  Ph.D. thesis, 2002.  URL https://nbn-resolving.de/urn:nbn:de:hbz:6-85659549572.
  * [31] Baelde D, Doumane A, Kuperberg D, Saurin A.  Bouncing Threads for Circular and Non-Wellfounded Proofs: Towards Compositionality with Circular Proofs.  In: Baier C, Fisman D (eds.), LICS ’22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022. ACM, 2022 pp. 63:1–63:13.  10.1145/3531130.3533375.
  * [32] De A, Jafarrahmani F, Saurin A.  Phase Semantics for Linear Logic with Least and Greatest Fixed Points.  In: Dawar A, Guruswami V (eds.), 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2022, December 18-20, 2022, IIT Madras, Chennai, India, volume 250 of _LIPIcs_. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022 pp. 35:1–35:23.  10.4230/LIPICS.FSTTCS.2022.35.
  * [33] Curzi G, Das A.  Computational expressivity of (circular) proofs with fixed points.  In: 38th Symp. on Logic in Computer Science. 2023 pp. 1–13.  10.1109/LICS56636.2023.10175772.
  * [34] Baelde D, Gacek A, Miller D, Nadathur G, Tiu A.  The Bedwyr system for model checking over syntactic expressions.  In: Pfenning F (ed.), 21th Conf. on Automated Deduction (CADE), number 4603 in LNAI. Springer, New York, 2007 pp. 391–397.  10.1007/978-3-540-73595-3_28.  URL http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/cade2007.pdf.
  * [35] Baelde D, Miller D, Snow Z.  Focused Inductive Theorem Proving.  In: Giesl J, Hähnle R (eds.), Fifth International Joint Conference on Automated Reasoning, number 6173 in LNCS. 2010 pp. 278–292.  10.1007/978-3-642-14203-1_24.
  * [36] Manighetti M.  Developing proof theory for proof exchange.  Ph.D. thesis, Institut Polytechnique de Paris, 2022.  URL https://theses.hal.science/tel-04289251.