In a previously published ENTCS paper ([18]), we introduced a
sequent calculus called for Minimal Implicational Propositional Logic
(). This calculus provides a proof search procedure for that works
in a bottom-up approach. We proved there that is sound and complete. We
also suggested a strategy to guarantee termination of the proof search
procedure. In this current paper, we refined this strategy and presented a
new strategy for termination. Considering this new strategy, we also
provide a (new) completeness proof for the system, which improves the
previous version. Besides that, we present explicit upper bounds on the
proof search procedure, derived from this new strategy. We also provide a
full soundness proof of the system.

Keywords: Logic; Propositional Minimal Implicational Logic; Sequent Calculus;
Proof Search; Counter-model Generation

§ INTRODUCTION

Propositional Minimal Implicational Logic () is the fragment of the
Propositional Minimal Logic () containing only the logical connective

The $TAUT$ problem for is the general problem of deciding if a formula
$\alpha \in \mil$ is always true. $TAUT$ is a PSPACE-Complete problem as stated
by [20], who also shows that this logic polynomially simulates
Propositional Intuitionistic Logic. Statman's simulation can also be used to
simulate Propositional Classical Logic polynomially.

[9] shows that can polynomially simulate not only
Propositional Classical and Intuitionistic Logic but also the full Propositional
Minimal Logic and any other decidable propositional logic with a Natural
Deduction system where the Subformula Principle holds (see [17]).

Moreover, has a strong relation with open questions about the Computational
Complexity Hierarchy, as we can see from the statements below.

* If $CoNP \neq NP$ then $NP \neq P$.

* If $PSPACE = NP$ then $CoNP = NP$.

* $CoNP=NP$, iff $\exists DS$, a deductive
system, such that $\forall\alpha\in$ $TAUT_{Cla}$, there is $\Pi$, a proof of $\alpha$ in $DS$, $size(\Pi_{DS}) \leq
Poly(|\alpha|)$ and the fact that $\Pi$ is a proof of $\alpha$ is verifiable
in polynomial time on the size of $\alpha$.

* $PSPACE=NP$ iff $\exists DS$, a deductive
system, such that $\forall\alpha\in$ $TAUT_{\mil}$, there is $\Pi$, a proof of $\alpha$ in $DS$, $size(\Pi_{DS}) \leq
Poly(|\alpha|)$ and the fact that $\Pi$ is a proof of $\alpha$ is verifiable
in polynomial time on the size of $\alpha$.

Those characteristics show us that is as hard to implement as the most
popular propositional logics. This fact, together with its straightforward language
(only one logical connective), makes a research object that can
provide us with many insights about the complexity class relationships
mentioned above and about the complexity of many other logics. Moreover, the
problem of conducting a proof search in a deductive system for has the
complexity of $TAUT$ as a lower bound. Thus, the size of propositional proofs
may be huge, and automated theorem provers (ATP) should take care of
super-polynomially sized proofs. Therefore, the study of deductive systems
for can directly influence in techniques to improve the way provers manage
such proofs.

In [18], we presented a sound and complete sequent calculus
for . We named it . This calculus establishes a bottom-up approach for
proof search in using a unified procedure either for provability and
counter-model generation. was designed to avoid the usage of loop
checkers and mechanisms for backtracking in its implementation.
Counter-model generation (using Kripke semantics) is achieved as a consequence
of the way the tree (produced by a failed proof search) is
constructed during a proof search process.

In this current work, we present an upper bound to the proof search procedure of
via translation functions from very known deductive systems for ,
Prawitz's Natural Deduction ([17]) and Gentzen's sequent calculus
([7]). These translation functions together with a strategy to
apply the rules of  provide termination for the proof search procedure.
Besides that, we show here all counter-model generation cases, including those
missed in [18].

We start in the next section with a brief discussion on the syntax and
semantics of used through this text. Section 3 discusses some related work
and state of the art in the field of deductive systems for . In Section
4 we present a study about the size of proofs in   to establish a bound for
proof search that can be used as a limit in the termination procedure of .
Section 5 presents  itself and its main features: termination, soundness,
and completeness (with the counter-model generation as a corollary). Section 6
concludes the paper discussing some open problems and future work.

§ MINIMAL IMPLICATIONAL LOGIC

We can formally define the language $\mathcal{L}$ for as follows.

The alphabet of $\mathcal{L}$ consists of:

* An enumerable set of propositional symbols, called atoms.

* The binary connective (or logical operator) for implication ($\imply$).

* parentheses: “$($” and “$)$”.

We can define the general notion of a formula in $\mathcal{L}$

* Every propositional symbol is a formula in $\mathcal{L}$. We call them
atomic formulas.

* If $A$ and $B$ are formulas in $\mathcal{L}$ then $(A \imply B)$ are

As usual, parentheses are used for disambiguation. We use the following
conventions through the text:

* Upper case letters to represent atomic formulas: $A$, $B$, $C$, …
* Lower Greek letters to represent generic formulas: $\alpha$, $\beta$,
* Upper case Greek letters are used to represent sets of formulas. For
example $\Delta$, $\Gamma$, …
* If parentheses are omitted, implications are interpreted right nested.

The semantics of is the intuitionistic semantics restricted to
only. Thus, given a propositional language $\mathcal{L}$, a model
is a structure $\left< U,\preceq, \mathcal{V} \right>$, where $U$ is a non-empty
set (worlds), $\preceq$ is a partial order relation on $U$ and $\mathcal{V}$ is
a function from $U$ into the power set of $\mathcal{L}$, such that if $i,j\in U$
and $i\preceq j$ then $\mathcal{V}(i)\subseteq\mathcal{V}(j)$. Given a model,
the satisfaction relationship $\models$ between worlds in models and formulas is
defined as in Intuitionistic Logic, namely:

* $\left< U,\preceq, \mathcal{V} \right>\models_{i}p$, $p\in\mathcal{L}$,
iff, $p\in\mathcal{V}(i)$

* $\left< U,\preceq, \mathcal{V} \right>\models_{i}\alpha_1\imply\alpha_2$,
iff, for every $j\in U$, such that $i\preceq j$, if $\left< U,\preceq,
\mathcal{V} \right>\models_{j}\alpha_1$ then $\left< U,\preceq, \mathcal{V}
\right>\models_{j}\alpha_2$.

As usual a formula $\alpha$ is valid in a model $\mathcal{M}$, namely
$\mathcal{M}\models\alpha$, if and only if, it is satisfiable in every world $i$
of the model, namely $\forall i\in U, \mathcal{M}\models_{i}\alpha$. A formula
is a tautology, if and only if, it is valid in every model.

§ RELATED WORK

It is known that Prawitz's Natural Deduction System for Propositional Minimal
Logic with only the -rules (-Elim and -Intro) is sound and
complete for the regarding Kripke semantics. As a consequence of this,
Gentzen's system ([7]) containing only right and left
-rules is also sound and complete.

In [7] , Gentzen proved the decidability of the Propositional
Intuitionistic Logic (), which also includes the cases for and .

However, Gentzen's approach was not conceived to be a bottom-up proof search
procedure. Figure <ref> shows structural and logic rules of an
adapted Gentzen's sequent calculus for , called . We restrict the
right side of a sequent to one and only one formula (we are in ; thus,
sequents with an empty right side does not make sense). This restriction implies
that structural rules can only be considered for main formulas on the left side
of a sequent. incorporates contraction in the -left, with the
repetition of the main formula of the conclusion on the premises. We use those
adaptations to explain the difficulties in using sequent calculus systems for
proof search in , , and . In [4], Dyckhoff describes
in detail the evolution of those adaptations over Gentzen's original system.
Those adaptations are attempting to improve bottom-up proof search mechanisms
for .

A central aspect when considering mechanisms for proof search in (and also
for ) is the application of the -left rule. The system proposed by
[7], the sequent calculus for Classical Logic, with some
adaptations (e.g., [19]) can ensure that each rule reduces the
degree (the number of atomic symbols occurrences and connectives in a formula)
of the main formula of the sequent (the formula to which the rule is applied),
when applied in a bottom-up manner during the proof search. This fact implies
the termination of the system. However, the case for is more complicated.
First, we have the “context-splitting” (using an expression from
[4]) nature of -left, i.e., the formula on the right side
of the conclusion sequent is lost in the left premise of the rule application.
Second, as we can reuse a hypothesis in different parts of a proof, the main
formula of the conclusion must be available to be used again by the generated
premises. Thus, the -left rule has the repetition of the main formula in
the premises, a scenario that allows the occurrence of loops in automatic

Δ, γγ

weakening (w)
α, Δγ

α, α, Δγ
contraction (c)
α, Δγ

Γ, α, β, Δγ
exchange (e)
Γ, β, α, Δγ

α, Γγ
Δ, Γγ

Δ, αβ
$\imply$-right ($\imply$-r)

Δ, αβα
Δ, αβ, βγ
$\imply$-left ($\imply$-l)
Δ, αβγ

Rules of Gentzen's

Since Gentzen, many others have explored solutions to deal with the challenges
mentioned above, proposing new calculi (sets of rules), strategies and proof
search procedures to allow more automated treatment to the problem.

Unfortunately, the majority of these results are focused on , with very few
works dedicated explicitly to or . Thus, we needed to concentrate our
literature review in the case, adjusting the found results to the
context by ourselves.

A crucial source of information was the work of [4], appropriately
entitled “Intuitionistic decision procedures since Gentzen” that
summarizes in chronological order the main results of this field. In the next paragraphs, we
highlight the most important of those results presented in [4].

A common way to control the proof search procedure in (and in ) is by
the definition of routines for loop verification as proposed
in [22]. Dyckhoff present loop checkers as very expensive
procedures for automatic reasoning ([4]), although they are
effective to guarantee termination of proof search procedures. The work in
[11] and [13] are examples of techniques that can be
used to minimize the performance problems that can arise with the usage of such

To avoid the use of loop checkers, [3] proposed a terminating
contraction-free sequent calculus for , named ,
using a technique based on the work of  [23] in the 50s.
[16] extended this work showing a method to generate
counter-examples in this system. They proposed two calculi, one for proof search
and another for counter-model generation, forming a way to decide about the
validity or not of formulas in . A characteristic of their systems is that
the subformula property does not hold on them. In [6], a similar
approach is presented using systems where the subformula property holds. They
also proposed a single decision procedure for , which guarantees minimal depth

Focused sequent calculi appeared initially in the Andreoli's work on linear
logic [1]. The author identified a subset of proofs from
Gentzen-style sequent calculus, which is complete and tractable.
[15] proposed the focused sequent calculi
where they used a mapping of into linear logic and adapted the Andreoli's
system to work with the image. [5] presented the focused system
that work direct in . Focusing is used in their
system as a way to implement restrictions in the -left rule as proposed by
[23] and [14]. The work of [5]
follows from the calculus with the same name presented in [10].

[4] also identify a list of features particularly of interest
when evaluating mechanisms for proof search in that we will follow when
comparing our solution to the other existent ones. They are:
termination (proof search procedure stops both for theorems and
non-theorem formulas), bicompleteness (extractability of models from
failed proof searches), avoidance of backtracking (backtracking being a
very immediate approach to deal with the context split in -left, but it is
also a complex procedure to implement), simplicity (allows easier
reasoning about systems).

§ THE SIZE OF PROOFS IN

Hirokawa has presented an upper bound for the size of normal form Natural
Deduction proofs of implicational formulas in   (that correspond to
formulas). [12] showed that for a formula $\alpha \in
\mil$, this limit is $|\alpha| \cdot 2^{|\alpha| + 1}$. As the Hirokawa result
concerns normal proofs in Natural Deduction we present now a translation of this
system to a cut-free sequent calculus, following the  rules presented in
Section <ref>, thus we can establish the limit for proof search
in  too.

Figure <ref> presents a recursively defined function[We use a
semicolon to separate arguments of functions (in function definitions and
function calls) instead of the most common approach to using commas. This
change in convention aims to avoid confusion with the commas used to separate
formulas and sets of formulas in sequent notation.] to translate Natural
Deduction normal proofs of  formulas into  proofs (in a version of
the system without the cut rule).

\begin{equation*}
F(\alpha; \Gamma) = \Seq{\Gamma, \alpha}{\alpha}
\end{equation*}

Case of Introduction:

\begin{eqnarray*}
\begin{minipage}{0.5\textwidth}
\begin{equation*}
\alwaysNoLine
\AxiomC{[$\alpha]^1$}
\def\extraVskip{2pt}
\UnaryInfC{$\prod$}
\alwaysSingleLine
\UnaryInfC{$\beta$}
\RightLabel{$\imply$-I$^1$}
\UnaryInfC{$\alpha\imply\beta$}
\DisplayProof;
\Gamma
\right)
\end{equation*}
\end{minipage} & \hspace{-.13\textwidth} = &
\begin{minipage}{0.5\textwidth}
\prftree[r]{$\imply\mathrm{r}$}
\alwaysNoLine
\AxiomC{$\alpha$}
\def\extraVskip{2pt}
\UnaryInfC{$\prod$}
\alwaysSingleLine
\UnaryInfC{$\beta$}
\DisplayProof;
\{\alpha\} \cup \Gamma
\right)}
\end{minipage}
\end{eqnarray*}

Case of Elimination:

\begin{equation*}
\alwaysNoLine
\def\extraVskip{2pt}
\AxiomC{$\prod_1$}
\UnaryInfC{$\alpha$}
\alwaysSingleLine
\AxiomC{$\alpha\imply\beta$}
\BinaryInfC{$\beta$}
\alwaysNoLine
\UnaryInfC{$\prod_2$}
\UnaryInfC{$C$}
\DisplayProof;
\Gamma
\right) =
\end{equation*}

{αβ} ∪Γ)
{αβ} ∪Γ)

{αβ} ∪Γ)
{αβ} ∪Γ)

A recursively defined function to translate Natural Deduction proofs into

In this definition, $c$ is a function that returns the conclusion (last sequent)
of a  demonstration as showed in (<ref>). Also,
$\imply-lc$ is a function that receives two  sequents and a formula to
construct the conclusion of a $\imply-left$ rule application, as defined
in (<ref>).

\begin{equation}
\label{eq:c-function}
\alwaysNoLine
\AxiomC{$\prod$}
\def\extraVskip{2pt}
\UnaryInfC{$\Seq{\Gamma}{\gamma}$}
\DisplayProof
\right) = \Seq{\Gamma}{\gamma}
\end{equation}

\begin{equation}
\label{eq:imply-lc-function}
\imply-lc(\Seq{\Gamma}{\alpha}; \Seq{\beta, \Gamma}{\gamma}; \alpha\imply\beta) = \Seq{\Gamma, \alpha\imply\beta}{\gamma}
\end{equation}

, a normal Natural Deduction derivation and $\Gamma$, the set
of undischarged formulas in $\Gamma$ then,

\alwaysNoLine
\AxiomC{$\Gamma$}
\UnaryInfC{$\prod$}
\UnaryInfC{$\alpha$}
\DisplayProof;
\emptyset
\right) =
\alwaysNoLine
\AxiomC{$\prod'$}
\UnaryInfC{$\Seq{\Gamma}{\alpha}$}
\DisplayProof

is a proof in .

By induction in the size of $\prod$.

As an example of the translation produced by the function of
Figure <ref>, we show below each step of the translation of a Natural
Deduction proof (<ref>) into an  proof (<ref>). To
shorten the size of the proofs we collapsed repeated occurrences of formulas
when passed as the hypothesis argument of the recursive function call.

\begin{equation}
\label{proof:nd}
\alwaysSingleLine
\def\extraVskip{2pt}
\AxiomC{$[B]^2$}
\AxiomC{$[A]^1$}
\AxiomC{$[A \imply (B \imply C)]^3$}
\RightLabel{$\imply$-E}
\BinaryInfC{$B \imply C$}
\RightLabel{$\imply$-E}
\BinaryInfC{$C$}
\RightLabel{$\imply$-I$^1$}
\UnaryInfC{$A \imply C$}
\RightLabel{$\imply$-I$^2$}
\UnaryInfC{$B \imply (A \imply C)$}
\RightLabel{$\imply$-I$^3$}
\UnaryInfC{$(A \imply (B \imply C)) \imply (B \imply (A \imply C))$}
\DisplayProof
\end{equation}

$[A \imply (B \imply C)]^3$
$B \imply (A \imply C)$
$(A \imply (B \imply C)) \imply (B \imply (A \imply C))$

$[B]^2, A \imply (B \imply C)$
$A \imply C$
$B \imply (A \imply C)$
{A (B C)}
(A (B C)) (B (A C))

$[A]^1, B, A \imply (B \imply C)$
$A \imply C$
{B, A (B C)}
A (B C)B (A C)

(A (B C)) (B (A C))

$A$     $A \imply (B \imply C)$
$B \imply C$
{A, B, A (B C)}
B, A (B C)A C

A (B C)B (A C)

(A (B C)) (B (A C))

In the following steps consider that $\Gamma = \{A, B, A \imply (B \imply C)\}$.

F(A; Γ)
$B \imply C$
F(A; Γ)
$B \imply C$
A(B C)

B, A (B C)A C

A (B C)B (A C)

(A (B C)) (B (A C))

F(B; {Γ, B C)}
F(C; {Γ, B C)}
-lc(c(F(B; {Γ, B C)});
c(F(C; {Γ, B C)});
B C)

B, A (B C)A C

A (B C)B (A C)

(A (B C)) (B (A C))

\begin{equation}
\label{proof:lj}
\prftree[r]{$\imply\mathrm{r}$}
\prftree[r]{$\imply\mathrm{r}$}
\prftree[r]{$\imply\mathrm{r}$}
\prfinterspace=8em
\prftree[r]{$\imply\mathrm{l}$}
\prftree[r]{$\imply\mathrm{l}$}
{\Seq{\Gamma, B \imply C}{B}}
{\Seq{\Gamma, B \imply C, C}{C}}
{\Seq{\Gamma, B \imply C}{C}}
{\Seq{B, A \imply (B \imply C)}{A \imply C}}
{\Seq{A \imply (B \imply C)}{B \imply (A \imply C)}}
{\Seq{}{(A \imply (B \imply C)) \imply (B \imply (A \imply C))}}
\end{equation}

The size of proofs in  considering only implicational tautologies is
the same of that in Natural Deduction, i.e. for an implicational formula
$\alpha$, a proof in  has maximum height of $|\alpha| \cdot
2^{|\alpha| + 1}$.

This proof follows directly from the translation function as each step in the
Natural Deduction proof is translated into precisely one step in the
resultant proof.

§ THE SEQUENT CALCULUS

In this section, we present a sound and complete sequent calculus for
. We call this system . We can prove for each rule that if all premises
are valid, then the conclusion is also valid, and if at least one premise is
invalid, then the conclusion also is. This proof is constructive, i.e.,
for any sequent, we have an effective way to produce either a
proof or a counter-model of it.

We start defining the concept of sequent used in the proposed calculus. A
sequent in our system has the following general form:

\begin{equation}
\label{eq:sequent}
\Seq{\{\Delta'\}, \Upsilon_1^{p_1}, \Upsilon_2^{p_2}, ..., \Upsilon_n^{p_n}, \Delta}{[p_1, p_2,..., p_n], \varphi}
\end{equation}

where $\varphi$ is a formula in $\mathcal{L}$ and $\Delta$,
$\Upsilon_1^{p_1}, \Upsilon_2^{p_2}, ..., \Upsilon_n^{p_n}$ are bags[A
bag (or a multiset) is a generalization of the concept of a set that, unlike a
set, takes repetitions into account: a bag {A, A, B} is not the same as the
bag {A, B}.] of formulas. Each $\Upsilon_i^{p_i}$ represents formulas
associated with an atomic formula $p_i$.

A sequent has two focus areas, one in the left side (curly
bracket)[Note that the symbols $\{$ and $\}$ here do not represent a
set. Instead, these symbols work as an annotation in the sequent to determine the left side
focused area. Therefore, $\Delta'$ instead is a set of formulas in the focused
area.] and another on the right (square bracket). Curly brackets are used to
control the application of the $\imply$-left rule and square brackets are used
to keep control of formulas that are related to a particular counter-model
definition. $\Delta'$ is a set of formulas and ${p_1, p_2,..., p_n}$ is a
sequence that does not allow repetition. We call context of the sequent a
pair $(\alpha, q)$, where $\alpha \in \Delta'$ and $\varphi = q$, where $q$ is
an atomic formula on the right side of the sequent.

The axioms and rules of  are presented in Figure <ref>. In each
rule, $\Delta' \subseteq \Delta$.

Rules are inspired by their backward application. In a -left rule
application, the atomic formula, $q$, on the right side of the conclusion goes
to the []-area in the left premise. $\Delta$ formulas in the conclusion are
copied to the left premise and marked with a label relating each of them with
$q$. The left premise also has a copy of $\Delta$ formulas without the
$q$-label. This mechanism keeps track of proving attempts. The form of the
restart rule is better understood in the completeness proof on
Section <ref>. A forward reading of rules can be achieved by
considering the notion of validity, as described in Section <ref>.

{Δ', q}, Υ_1^p_1, Υ_2^p_2, …, Υ_n^p_n, Δ[p_1, p_2, …, p_n], q

{Δ', α}, Υ_1^p_1, Υ_2^p_2, …, Υ_n^p_n, Δ, α[p_1, p_2, …, p_n], β
{Δ'}, Υ_1^p_1, Υ_2^p_2, …, Υ_n^p_n, Δ, α[p_1, p_2, …, p_n], β

{}, Υ_1, Υ_2, …, Υ_i, Υ_i+1^p_i+1, …, Υ_n^p_n, Δ^q[p_1, p_2, …, p_i+1, …, p_n, q], p_i
{Δ'}, Υ_1^p_1, Υ_2^p_2, …, Υ_i^p_i, Υ_i+1^p_i+1, …, Υ_n^p_n, Δ[p_1, p_2, …, p_i, p_i+1, …, p_n], q

{Δ'}, Υ_1^p_1, Υ_2^p_2, …, Υ_n^p_n, Δ, α[p_1, p_2, …, p_n], β
$\imply$-r$_{\alpha \imply \beta}$
{Δ'}, Υ_1^p_1, Υ_2^p_2, …, Υ_n^p_n, Δ[p_1, p_2, …, p_n], αβ

Considering $\overline{\Upsilon} = \displaystyle \bigcup_{i=1}^{n}{\Upsilon_i^{p_i}}$ and $\bar{p} = p_1, p_2, \ldots, p_n$, we have:

{αβ,Δ'},Υ, Δ^q, Δ[p̅, q], α
{αβ,Δ'},Υ, Δ, β[p̅], q
$\imply$-l$_{(\alpha \imply \beta, q)}$
{αβ,Δ'}Υ, Δ [p̅], q

Rules of

§.§ A Proof Search Strategy

The following is a general strategy to be applied with the rules of  to
generate proofs from an input sequent (a sequent that is a candidate to be the
conclusion of a proof), which is based on a bottom-up application of the rules.
From the proposed strategy, we can then state a proposition about the
termination of the proving process.

A goal sequent is a new sequent in the form of (<ref>). It is
a premise of one of the system's rules, generated by the application of this
rule on an open branch during the proving process. If the goal sequent is an
axiom, the branch where it is will stop. Otherwise, apply the first applicable
rule in the following order:

* Apply -right rule if it is possible, i.e., if the formula on the
right side of the sequent, outside the []-area, is not atomic. The premise
generated by this application is the new goal of this branch.

* Choose one formula on the left side of the sequent, not labeled yet, i.e.,
a formula $\alpha \in \Delta$ that is not occurring in $\Delta'$, then apply
the focus rule. The premise generated by this application is the new goal of
this branch.

* If all formulas on the left side have already been focused, choose the
first formula $\alpha \in \Delta'$ such that the context $(\alpha, q)$ was not
yet tried since the last application of a restart rule. We say that a context
$(\alpha, q)$ is already tried when a formula $\alpha$ on the left was
expanded (by the application of -left rule), with $q$ as the formula
outside the []-area on the right side of the sequent. The premises generated
by this application are new goals of the respective new branches.

* Choose the leftmost formula inside the []-area that was not chosen before
in this branch and apply the restart rule. The premise generated by this
application is the new goal of the branch.

From the proof strategy we can make the following observations about a tree
generated during a proving process:

*  A top sequent is the highest sequent of a
branch in the tree.

*  In a top sequent of a branch on the form of
sequent (<ref>), if $\varphi \in \Delta$ then the top sequent is
an axiom and the branch is called a closed branch. Otherwise, we say
that the branch is open and $\varphi$ is an atomic formula.

*  In every sequent of the tree, $\Delta' \subseteq
\Delta$.

*  For $i=1, \ldots n$, $\Upsilon_{i-1}^{p_{i-1}}
\subseteq \Upsilon_{i}^{p_{i}}$.

We call this strategy $\mathcal{S}$-. Figure <ref>
shows a generic schema of a completely expanded branch in a tree, not
necessarily a proof, generated by the application of $\mathcal{S}$-.

{Δ'}, Υ_1^p_1, Υ_2^p_2, Υ_i-1^p_i-1,…,Υ_i^p_i,Δ[p_1, p_2, …, p_i-1, p_i], p_k   (where k = 1, 2, …, i)
a sequence of focus, -left and -right
{}, Υ_1^p_1, Υ_2^p_2, …, Υ_i-1^p_i-1,Δ[p_1, p_2, …, p_i-1], p_i
a sequence of focus, -left, -right and restart (for each atomic formula in the []-area)
{φψ},Υ_2^p_2,…,Υ_i-1^p_i-1,Δ^p_i, Υ_1^p_1, Υ_1, φ_1,…,φ_n[p_2, …, p_i-1, p_i, p_1], p_2
{φψ},Υ_2^p_2,…,Υ_i-1^p_i-1,Δ^p_i, Υ_1^p_1, Υ_1[p_2, …, p_i-1, p_i, p_1], φ
{φψ}, Υ_2^p_2,…,Υ_i-1^p_i-1,Δ^p_i, Υ_1[p_2, …, p_i-1, p_i], p_1
{},Υ_2^p_2,…,Υ_i-1^p_i-1,Δ^p_i, Υ_1[p_2, …, p_i-1, p_i], p_1
{Δ'}, Υ_1^p_1, Υ_2^p_2,…,Υ_i-1^p_i-1,Δ[p_1, p_2, …, p_i-1], p_i
a sequence of focus, -left and -right
{φψ}, Υ_1^p_1, Υ_1, φ_1,…,φ_n[p_1], p_2
a sequence -right
{φψ}, Υ_1^p_1, Υ_1[p_1], φ
{φψ, ψ}, ψ, Υ_1[], p_1
{φψ}, ψ, Υ_1[], p_1
{φψ}, Υ_1[], p_1
{}, φψ, γ_1, …, γ_m[], p_1
{}, φψ[], γ
{}[], (φψ)γ

Generic schema of a tree generated following $\mathcal{S}$-

§.§ An Upper Bound for the Proof Search in

Using the same approach applied in Section <ref>, we now propose a
translation from  proofs into the system . The translation function
needs to adapt a sequent in  form to a sequent in  form.
Figure <ref> presents the definition of the translation
function[As in Section <ref>, we use semicolon to separate
function arguments here].

\begin{equation*}
F'\left(\Seq{\Gamma, \alpha}{\alpha}; \Delta; \Upsilon; \Sigma; \Pi\right) =
\alwaysNoLine
\AxiomC{$\Seq{\{\Delta\}, \Upsilon, \Gamma, \alpha}{[\Sigma], \alpha}$}
\def\extraVskip{2pt}
\UnaryInfC{$\prod$}
\DisplayProof
\end{equation*}

Last rule is -right:

\begin{equation*}
\alwaysNoLine
\AxiomC{$\mathcal{D}$}
\UnaryInfC{$\Seq{\Gamma, \alpha}{\beta}$}
\alwaysSingleLine
\RightLabel{$\imply$-r}
\UnaryInfC{$\Seq{\Gamma}{\alpha \imply \beta}$}
\DisplayProof;
\Delta;
\Upsilon;
\Sigma;
\Pi
\right) =
\end{equation*}

$\Seq{\Gamma, \alpha}{\beta}$
$\Seq{\{\Delta\}, \Upsilon, \Gamma}{[\Sigma], \alpha\imply\beta}$
{Δ}, Υ, Γ[Σ], αβ

Last rule is -left:

\begin{equation*}
\alwaysNoLine
\AxiomC{$\mathcal{D}_1$}
\UnaryInfC{$\Seq{\Gamma, \alpha \imply \beta}{\alpha}$}
\AxiomC{$\mathcal{D}_2$}
\UnaryInfC{$\Seq{\Gamma, \beta}{q}$}
\alwaysSingleLine
\RightLabel{$\imply$-l}
\BinaryInfC{$\Seq{\Gamma, \alpha \imply \beta}{q}$}
\DisplayProof;
\Delta;
\Upsilon;
\Sigma;
\Pi
\right) =
\end{equation*}

$\Seq{\{\Delta\}, \Upsilon, \Gamma, \alpha \imply \beta}{[\Sigma], q}$

A recursive function to translate  into

We use some abbreviations to shorten the function definition of
Figure <ref>. We present them below.

\begin{eqnarray*}
\hspace{-6cm}
\begin{minipage}{0.5\textwidth}
\end{minipage} & \hspace{-6.8cm}= &
\begin{minipage}{0.5\textwidth}\vspace{-.1cm}
\alwaysNoLine
\AxiomC{$\mathcal{D}_1$}
\UnaryInfC{$\Seq{\Gamma, \alpha \imply \beta}{\alpha}$}
\DisplayProof;
\Delta \cup \{\alpha \imply \beta\};
\Upsilon \cup \Gamma^q \cup \{(\alpha\imply\beta)^q\};
\Sigma \cup \{q\};
\Pi'
\right)$
\end{minipage}
\end{eqnarray*}

\begin{eqnarray*}
\hspace{-6cm}
\begin{minipage}{0.5\textwidth}
\end{minipage} & \hspace{-6.8cm}= &
\begin{minipage}{0.5\textwidth}\vspace{-.1cm}
\alwaysNoLine
\AxiomC{$\mathcal{D}_2$}
\UnaryInfC{$\Seq{\Gamma, \beta}{q}$}
\DisplayProof;
\Delta \cup \{\alpha \imply \beta\};
\Upsilon;
\Sigma;
\Pi'
\right)$
\end{minipage}
\end{eqnarray*}

\begin{eqnarray*}
\hspace{-6cm}
\begin{minipage}{0.5\textwidth}
\end{minipage} & \hspace{-6.8cm}= &
\begin{minipage}{0.5\textwidth}\vspace{-.1cm}
\alwaysNoLine
\AxiomC{$\Seq{\{\Delta\}, \Upsilon, \Gamma, \alpha \imply \beta}{[\Sigma], q}$}
\UnaryInfC{$\mathlarger{\mathlarger{\Pi}}$}
\DisplayProof
\right)
\right)$
\end{minipage}
\end{eqnarray*}

\begin{eqnarray*}
\hspace{-3cm}
\begin{minipage}{0.3\textwidth}
\end{minipage} & \hspace{-4cm}= &
\begin{minipage}{0.7\textwidth}\vspace{-.1cm}
means that all formulas of the set $\Gamma$ are labeled with a reference to the atomic formula $q$
\end{minipage}
\end{eqnarray*}

\begin{eqnarray*}
\hspace{-2cm}
\begin{minipage}{0.3\textwidth}
\end{minipage} & \hspace{-3cm}= &
\begin{minipage}{0.7\textwidth}\vspace{-.1cm}
means the same for the individual formula $\alpha \imply \beta$.
\end{minipage}
\end{eqnarray*}

The complicated case occurs when the function $F'$ is applied to a proof fragment in
which the last  rule applied is an -left. In this case, $F'$ needs
to inspect the proof fragment constructed until that point to identify whether
the context $(\alpha\imply\beta, q)$ was already used or not. This inspection
has to be done since  does not allow two or more applications of the same
context between two applications of the $restart$ rule. To deal with this, we
use some auxiliary functions described below.

$FOCUS$ is a function that receives a fragment of proof in  form and builds
one application of the focus rule on the top of the proof fragment received in
the case that the main formula of the rule is not already focused. The main
formula is also an argument of the function. In the function definition
(<ref>), we have the constraint that $\alpha \in \Gamma$.

\begin{equation*}
\alwaysNoLine
\AxiomC{$\Seq{\{\Delta\}, \Upsilon, \Gamma}{[\Sigma], \beta}$}
\def\extraVskip{2pt}
\UnaryInfC{$\prod$}
\UnaryInfC{$\Seq{\{\}}{[], \gamma}$}
\DisplayProof;
\alpha
\right) =
\end{equation*}

\begin{equation}
\label{eq:focus-function}
\left\{
\begin{array}{lr}
\alwaysSingleLine
\AxiomC{$\Seq{\{\Delta, \alpha\}, \Upsilon, \Gamma}{[\Sigma], \beta}$}
\RightLabel{$\mathrm{focus}$}
\UnaryInfC{$\Seq{\{\Delta\}, \Upsilon, \Gamma}{[\Sigma], \beta}$}
\alwaysNoLine
\def\extraVskip{2pt}
\UnaryInfC{$\prod$}
\UnaryInfC{$\Seq{\{\}}{[], \gamma}$}
\DisplayProof & \text{if }\alpha \notin \Delta \\
\\
\alwaysNoLine
\AxiomC{$\Seq{\{\Delta\}, \Upsilon, \Gamma}{[\Sigma], \beta}$}
\def\extraVskip{2pt}
\UnaryInfC{$\prod$}
\UnaryInfC{$\Seq{\{\}}{[], \gamma}$}
\DisplayProof & \text{otherwise} \\
\end{array}
\right\}
\end{equation}

The function $PROOFUNTIL$ also receives a fragment of a proof in  form where
$(\alpha \imply \beta, q)$ is one of the available contexts, applies the restart
rule with an atomic formula $p$ such that $p \in \Sigma$ in the top of this
fragment of proof and, then, conducts a sequence of  rule applications
following the $\mathcal{S}$-until the point that the context $(\alpha
\imply \beta, q)$ is available again. This mechanism has to be done in the case
that the context $(\alpha \imply \beta, q)$ is already applied in an
$\imply$-left application, some point after the last restart rule application in
the proof fragment received as the argument $\Pi$. Otherwise, the proof fragment
is returned unaltered. Function $PROOFUNTIL$ is described in the function
definition (<ref>).

\begin{equation*}
\alwaysNoLine
\AxiomC{$\Seq{\{\Delta, \alpha\imply\beta\}, \Upsilon, \Gamma}{[\Sigma], q}$}
\def\extraVskip{2pt}
\UnaryInfC{$\prod$}
\UnaryInfC{$\Seq{\{\}}{[], \gamma}$}
\DisplayProof
\right) =
\end{equation*}

\begin{equation}
\label{eq:proofuntil-function}
\left\{
\begin{array}{lr}
\alwaysSingleLine
\AxiomC{$\Seq{\{\Delta'', \alpha\imply\beta\}, \Upsilon'', \Gamma'}{[\Sigma''], q}$}
\UnaryInfC{\vdots}
\UnaryInfC{$\Seq{\{\}, \Upsilon', \Gamma^q, \Gamma}{[\Sigma'], p}$}
\RightLabel{$\mathrm{restart-}p$}
\UnaryInfC{$\Seq{\{\Delta, \alpha\imply\beta\}, \Upsilon, \Gamma}{[\Sigma], q}$}
\alwaysNoLine
\def\extraVskip{2pt}
\UnaryInfC{$\prod$}
\UnaryInfC{$\Seq{\{\}}{[], \gamma}$}
\DisplayProof & \imply\text{-left}(\alpha\imply\beta, q) \in \prod\\
\\
\bigskip
\\
\alwaysNoLine
\AxiomC{$\Seq{\{\Delta, \alpha\imply\beta\}, \Upsilon, \Gamma}{[\Sigma], q}$}
\def\extraVskip{2pt}
\UnaryInfC{$\prod$}
\UnaryInfC{$\Seq{\{\}}{[], \gamma}$}
\DisplayProof & \text{otherwise} \\
\end{array}
\right\}
\end{equation}

As an example of this translation, we use here the formula ${(((( A \to B ) \to
A ) \to A ) \to B ) \to B}$. We know from [2] that this formula
needs two repetitions of the hypothesis ${((( A \to B ) \to A ) \to A ) \to B}$
to be proved in . To shorten the proof tree we use the following
abbreviation: ${(( A \to B ) \to A ) \to A = \epsilon}$. Thus, its normal proof
in Natural Deduction can be represented as shown in
Proof (<ref>).

\begin{equation}
\label{proof:nd-twice}
\infer[\to \mbox{I}^3]
{(\epsilon \to  B ) \to  B}
{\infer[\to \mbox{E}]
{ B }
{\infer[\to \mbox{E}^2]
{\infer[\to \mbox{E}]
{ A }
{\infer[\to \mbox{I}^1]
{( A  \to  B )}
{\infer[\to \mbox{E}]
{ B }
{\infer[\to \mbox{I}^4]
{{[ A ]^1}
{[\epsilon \to  B]^3}
{[( A  \to  B ) \to  A]^2}
{[\epsilon \to  B]^3}
\end{equation}

Using the translation presented in Figure <ref>, we achieve the
following  cut-free proof. To shorten the proof, we numbered each
subformula of the initial formula that we want to prove and use these numbers to
refer to those subformulas all over the proof. Let us call this  version
of the proof $\mathcal{D}$ (Proof (<ref>)).

\begin{equation}
\label{proof:lj-twice}
\alwaysSingleLine
\def\extraVskip{2pt}
\AxiomC{$\Seq{\to_3, \to_1, A, \to_1}{A}$}
\RightLabel{$\imply$-R}
\UnaryInfC{$\Seq{\to_3, \to_1, A}{\to_2}$}
\AxiomC{$\Seq{\to_3, \to_1, A, B}{B}$}
\RightLabel{$\imply$-L}
\BinaryInfC{$\Seq{\to_3, \to_1, A}{B}$}
\RightLabel{$\imply$-R}
\UnaryInfC{$\Seq{\to_3, \to_1}{\to_0}$}
\AxiomC{$\Seq{\to_3, \to_1, A}{A}$}
\RightLabel{$\imply$-L}
\BinaryInfC{$\Seq{\to_3, \to_1}{A}$}
\RightLabel{$\imply$-R}
\UnaryInfC{$\Seq{\to_3}{\to_2}$}
\AxiomC{$\Seq{\to_3, B}{B}$}
\RightLabel{$\imply$-L}
\BinaryInfC{$\Seq{\to_3}{B}$}
\RightLabel{$\imply$-R}
\UnaryInfC{$\Seq{}{(((( A  \to_0  B ) \to_1  A ) \to_2  A ) \to_3  B ) \to_4  B}$}
\DisplayProof
\end{equation}

The translation to  starts by applying the function $F'$ to the full proof $\mathcal{D}$.

\begin{equation*}
\begin{array}{llcr}
\multirow{5}{*}{$\mathcal{D}$;} & \Gamma   &= & \emptyset;\\
& \Delta   &= & \emptyset;\\
& \Upsilon &= & \emptyset;\\
& \Sigma   &= & \emptyset;\\
& \Pi      &= & nil
\end{array}
\right)
\end{equation*}

This first call of $F'$ produces the end sequent of the proof in  and calls
the function $F'$ recursively to the rest of the original proof in .
This  fragment has now, as its last rule application, an -left.

∏    =     {}[], (((( A  →_0  B ) →_1  A ) →_2  A ) →_3  B ) →_4  B

$\Seq{\to_3, B}{B}$
;      Γ   =    ∅;

Δ   =    ∅;

Υ   =    ∅;

Σ   =    ∅;

Then, as the main formula $((( A \to_0 B ) \to_1 A ) \to_2 A ) \to_3 B$ (in the
proof represented only by $\to_3$) is not focused yet, the call of function $F'$
first constructs an application of the focus rule on the top of the $\Pi$
fragment received as a function argument. Also, the context $(\to_3, B)$ was not
expanded yet. Thus, the recursive step can proceed directly without the need of
a restart (this is controlled by the $PROOFUNTIL$ function as shown in $F'$
definition in Figure <ref>).

∏    =

{→_3},→_3[], B
{},→_3[], B

{}[], (((( A  →_0  B ) →_1  A ) →_2  A ) →_3  B ) →_4 B

;      Γ   =    {→_3};

Δ   =    {→_3};

Υ   =    {→_3^B};

Σ   =    {B};

$\Seq{\to_3, B}{B}$
;      Γ   =    {→_3};

Δ   =    {→_3};

Υ   =    ∅;

Σ   =    ∅;

The call of $F'$ on the right premise constructs an axiom. Thus this branch in
the  proof translation being built is closed. The next recursive call
"pastes" on the top of the right branch of the new version of $\Pi$ as follows.

∏    =

{→_3}, →_3^B, →_3[B], →_2
{→_3}, →_3, B[], B
{→_3},→_3[], B

{},→_3[], B

{}[], (((( A  →_0  B ) →_1  A ) →_2  A ) →_3  B ) →_4 B

$\Seq{\to_3, \to_1}{\to_0}$
$\Seq{\to_3, A}{A}$
$\Seq{\to_3, \to_1}{A}$
;      Γ   =    {→_3};

Δ   =    {→_3};

Υ   =    {→_3^B};

Σ   =    {B};

This process goes until a point where the context ${(\to_3, B)}$ is again found,
and the translation needs to deal with a restart in the  translated proof.
This situation happens when the recursion of $F'$ reaches the point below.

$\Seq{\to_3, \to_1, A}{\to_2}$
$\Seq{\to_3, \to_1, A, B}{B}$
$\Seq{\to_3, \to_1, A}{B}$
;      Γ   =    {→_1, A};

Δ   =    {→_3, →_1};

Υ   =    {→_3^B, →_3^A, →_1^A};

Σ   =    {B, A};

The $\Pi$ fragment constructed in this step of the recursion is presented below.

{}[], (((( A  →_0  B ) →_1  A ) →_2  A ) →_3  B ) →_4 B

{},→_3[], B

{→_3},→_3[], B

{→_3}, →_3^B, →_3[B], →_2

{→_3}, →_3^B, →_3, →_1[B], A

{→_3, →_1}, →_3^B, →_3, →_1[B], A

{→_3, →_1}, →_3^B, →_3^A, →_1^A, →_3, →_1[B, A], →_0

{→_3, →_1}, →_3^B, →_3, →_1, A[B], A

{→_3}, →_3, B[], B

The $\Pi'$ fragment in $\Pi$ is built as the result of a proof search from the
top sequent of the leftmost branch of $\Pi$ until the point that there is a
repetition of the context ${(\to_3, B)}$ and the $\imply$-left rule can be
applied again without offending the  strategy. This result is produced by
the $PROOFUNTIL$ call when applying $F'$ to an  fragment that end with a
-left rule application.

$\Seq{\{\to_3\}, \to_3^B, \to_3, \to_1, \to_1^B, A^B, \to_3^B}{[B], A}$
$\Seq{\{\}, \to_3^B, \to_3, \to_1, \to_1^B, A^B, \to_3^B}{[B], A}$
$\Seq{\{\to_3, \to_1\}, \to_3^B, \to_3^A, \to_1^A, \to_1, A, \to_3}{[B, A], B}$

where $\Pi_1'$ is:

$\Seq{\{\to_3, \to_1\}, \to_3^B, \to_3^A, \to_1^A, \to_1^B, A^B, \to_3^B, \to_3, \to_1, A}{[B, A], B}$
$\Seq{\{\to_3, \to_1\}, \to_3^B, \to_3^A, \to_1^A, \to_1^B, A^B, \to_3^B, \to_3, \to_1}{[B, A], \to_0}$
$\Seq{\{\to_3\}, \to_3^B, \to_3^A, \to_1^A, \to_1^B, A^B, \to_3^B, \to_3, \to_1, A}{[B, A], A}$
$\Seq{\{\to_3, \to_1\}, \to_3^B, \to_3^A, \to_1^A, \to_1^B, A^B, \to_3^B, \to_3, \to_1}{[B, A], A}$
$\Seq{\{\to_3\}, \to_3^B, \to_3^A, \to_1^A, \to_1^B, A^B, \to_3^B, \to_3, \to_1}{[B, A], A}$
$\Seq{\{\to_3\}, \to_3^B, \to_3^A, \to_1^A, \to_1^B, A^B, \to_3^B, \to_3, \to_1}{[B, A], \to_2}$

and $\Pi_2'$ is:

$\Seq{\{\to_3, \to_1\}, \to_3^B, \to_3^A, \to_1^A, \to_1^B, A^B, \to_3^B, B^A, \to_3, \to_1, B, A}{[B, A], B}$
$\Seq{\{\to_3, \to_1\}, \to_3^B, \to_3^A, \to_1^A, \to_1^B, A^B, \to_3^B, B^A, \to_3, \to_1, B}{[B, A], \to_0}$
$\Seq{\{\to_3, to_1\}, \to_3^B, \to_3, \to_1, \to_1^B, A^B, \to_3^B, B, A}{[B], A}$
$\Seq{\{\to_3, \to_1\}, \to_3^B, \to_3, \to_1, \to_1^B, A^B, \to_3^B, B}{[B], A}$
$\Seq{\{\to_3\}, \to_3^B, \to_3, \to_1, \to_1^B, A^B, \to_3^B, B}{[B], A}$

The top sequent of the fragment $\Pi_1'$ is the point where we can apply the
$\imply$-left rule to the context ${(\to_3, B)}$ again. Thus the next recursion
call becomes:

\begin{eqnarray*}
\hspace{-6cm}
\begin{minipage}{0.5\textwidth}
\end{minipage} & \hspace{-6.8cm}= &
\begin{minipage}{0.5\textwidth}\vspace{-.1cm}
\begin{array}{llcc}
\multirow{5}{*}{
\alwaysSingleLine
\def\extraVskip{2pt}
\AxiomC{$\Seq{\to_3, \to_1, A}{A}$}
\UnaryInfC{$\Seq{\to_3, \to_1, A}{\to_2}$}
\DisplayProof; } & \Gamma   &= &\{\to_3, \to_1, A\};\\
& \Delta   &= &\{\to_3, \to_1\};\\
& \Upsilon &= &\{\to_3^A, \to_1^A, \to_3^B, \to_1^B, A^B\};\\
& \Sigma   &= &\{B, A\};\\
& \Pi & &
\end{array}
\right)    $
\end{minipage}
\end{eqnarray*}

\begin{eqnarray*}
\hspace{-6cm}
\begin{minipage}{0.5\textwidth}
\end{minipage} & \hspace{-6.8cm}= &
\begin{minipage}{0.5\textwidth}\vspace{-.1cm}
\begin{array}{llcc}
\multirow{5}{*}{
\alwaysNoLine
\def\extraVskip{2pt}
\AxiomC{$\Seq{\to_3, \to_1, A, B}{B}$}
\DisplayProof; } & \Gamma   &= &\{\to_3, \to_1, A\};\\
& \Delta   &= &\{\to_3, \to_1\};\\
& \Upsilon &= &\{\to_3^A, \to_1^A, \to_3^B, \to_1^B, A^B\};\\
& \Sigma   &= &\{B, A\};\\
& \Pi & &
\end{array}
\right)
\end{minipage}
\end{eqnarray*}

Finally, after finish the translation process we obtained the translated proof
of (<ref>).

\begin{equation}
\label{proof:lmt-translated}
\infer[\imply\mathrm{r}]
{\Seq{\{\}}{[], (((( A  \to_0  B ) \to_1  A ) \to_2  A ) \to_3  B ) \to_4 B}}
\infer[\imply\mathrm{focus}]
{\Seq{\{\},\to_3}{[], B}}
\infer[\imply\mathrm{l}]
{\Seq{\{\to_3\},\to_3}{[], B}}
\infer[\imply\mathrm{r}]
{\Seq{\{\to_3\}, \to_3^B, \to_3}{[B], \to_2}}
\infer[\imply\mathrm{focus}]
{\Seq{\{\to_3\}, \to_3^B, \to_3, \to_1}{[B], A}}
\infer[\imply\mathrm{l}]
{\Seq{\{\to_3, \to_1\}, \to_3^B, \to_3, \to_1}{[B], A}}
\deduce
{\Seq{\{\to_3, \to_1\}, \to_3^B, \to_3^A, \to_1^A, \to_3, \to_1}{[B, A], \to_0}}
\deduce
\infer[\imply\mathrm{r}]
{\Seq{\{\to_3, \to_1\}, \to_3^B, \to_3^A, \to_1^A, \to_1^B, A^B, \to_3^B, \to_3, \to_1, A}{[B, A], \to_2}}
{\Seq{\{\to_3, \to_1\}, \to_3^B, \to_3^A, \to_1^A, \to_1^B, A^B, \to_3^B, \to_3, \to_1, A}{[B, A], A}}
{\Seq{\{\to_3, \to_1\}, \to_3^B, \to_3^A, \to_1^A, \to_1^B, A^B, \to_3^B, \to_3, \to_1, A}{[B, A], A}}
} &
{\Seq{\{\to_3, \to_1\}, \to_3^B, \to_3, \to_1, A}{[B], A}}
{\Seq{\{\to_3\}, \to_3, B}{[], B}}}
\end{equation}

§.§ Termination

To control the end of the proof search procedure of  our approach is to
define an upper bound limit to the size of its proof search tree. Then, we need
to show that the  strategy here proposed allows exploring all the possible
ways to expand the proof tree until it reaches this size.

From Theorem <ref>, we know that the upper bound for cut-free
proofs based on  is ${|\alpha| \cdot 2^{|\alpha| + 1}}$, where $\alpha$
is the initial formula that we want to prove. We use the translation presented
in Figure <ref> on the previous Section to find a similar limit
for proofs. We have to analyze three cases to establish an upper bound for

The cases are described below and are summarized in Table <ref>.

* Axioms of  maps one to one with axioms of ;

* $\imply$-right applications of  maps one to one with
$\imply$-right applications of ;

* $\imply$-left applications of  maps to  in three different
possible sub-cases, according to the context $(\alpha \imply \beta, q)$ in
which the rule is being applied in . We have to consider the fragment
of  already translated to decide the appropriate case.

* If the context is not yet focused neither expanded

Then, one application of -left in  maps to two applications
of rules in : first, a focus application, then an -left

* If the context is already focused but not yet expanded

Then, one application of -left in  maps to one application
of -left in .

* If the context $(\alpha \imply \beta, q)$ is already focused and

Then, the one application of -left in  maps to the height of
the  proof fragment produced by the execution of the $PROOFUNTIL$
function. Let this height be called $h$.

2c             Map

axiom                            2caxiom            1:1

-right                     2c-right     1:1

focused             expanded

3*-left     No                  No                 1:2     1 focus and 1 -left

Yes                 No                 1:1     1 -left

Yes                 Yes                1:h     1 to the size of $PROOFUNTIL$

Mapping the size of  proofs into

The height $h$ that defines the size of the proof fragment returned by the
function $PROOFUNTIL$ has a maximum limit of $2^{2log_2|\alpha|}$, where
$\alpha$ is the main formula of the initial sequent of the proof in .

Consider a proof $\prod_\ljarrow$ of an initial sequent in  with the
form $\Seq{}{\alpha}$. The process of translating $\prod_\ljarrow$ to
produces a proof $\prod_\lmt$ with the initial sequent in the form
$\Seq{\{\}}{[],\alpha}$. Consider that $\alpha$ has the form $\alpha_1 \imply
\alpha_2$. In some point of the translation to , we reach a point where a
context $(\psi \imply \varphi, q)$ is already focused and expanded in the
already translated part of the proof $\prod_\lmt$. At this point, the function
$PROOFUNTIL$ generates a fragment of the proof $\prod_\lmt$, call it $\Sigma$
of size $h$. The height $h$ is bound by the number of applications of
-left rules in $\Sigma$, which can be determined by the multiplication of
the degree of the formula $\alpha_1$ (that bounds the number of possible
implicational formulas in the left side of a sequent in ) by the maximum
number of atomic formulas ($n$) inside the []-area in the highest branch of
$\Sigma$ (each $p_i$ inside the []-area allows one application of the restart
rule). Thus we can formalize this in the following manner:

\begin{equation*}
\begin{array}{lcl}
h & = & n \times |\alpha_1| \\
h & = & |\alpha| \times |\alpha| \\
h & = & |\alpha|^2
\end{array}
\end{equation*}

\begin{equation*}
\begin{array}{lcl}
|\alpha|^2 & = & 2^{2 \cdot log_2|\alpha|}
\end{array}
\end{equation*}

Then, we have that

\begin{equation*}
\begin{array}{lcl}
h & = & 2^{2 \cdot log_2|\alpha|}
\end{array}
\end{equation*}

Let $\alpha$ be a  tautology. The size of any proof of $\alpha$ generated
by  $\mathcal{S}$-has an upper bound of $|\alpha| \cdot 2^{|\alpha| + 1 + 2 \cdot log_2|\alpha|}$.

Considering the size of proofs for a formula $\alpha$ using , the
mapping in Table <ref> and the Lemma <ref>, the proof
follows directly.

$\mathcal{S}$- always terminates.

To guarantee termination, we use the upper bound presented in
Theorem <ref> to limit the height of opened branches
during the  proof search process. The strategy presented in
Section <ref> forces an ordered application of rules that
produces all possible combinations of formulas to be expanded in the right and
left sides of generated sequents. In other words, when the upper bound is
reached, the proof search had, for sure, applied all possible expansion. The
procedure can only continue by applying an already done expansion.

* $\imply$-right rule is applied until we obtain an atomic formula on the
right side.

* focus rule is applied until every non-labeled formula becomes focused. The
same formula can not be focused twice unless a restart rule is applied.

* $\imply$-left rule can not be applied more than once to the same context
unless a restart rule is applied.

* between two applications of the restart rule in a branch there is only one
possible application of a $\imply$-left rule for a context $(\alpha, q)$.
$\alpha$ and $q$ are always subformulas of the initial formula.

* restart rule is applied for each atomic formula that appears on the right
side of sequents in a branch in the order of its appearance in the []-area,
which means that proof search will apply the restart rule for each $p_i, i =
1, \ldots n$ until the branch reaches the defined limit.

The proof of completeness of  is closely related to this strategy and with
the way the proof tree is labeled during the proving process. Section
<ref> presents the soundness proof of  and Section
<ref>, the completeness proof.

§.§ Soundness

In this section, we prove the soundness of . A few basic facts and
definitions used in the proof follow.

A sequent {Δ'}, Υ_1^p_1, Υ_2^p_2, …,
Υ_n^p_n, Δ[p_1, p_2, …, p_n], φ is valid,
if and only if, [color=yellow!100]ch04-lmt - Doubt: One of the members
of Dedukti argued that as the $\Upsilon$ sets includes the previous ones we
do not need this Union in the notation$\Delta', \Delta \models \varphi$ or
$\exists i \displaystyle (\bigcup_{k=1}^{i}{\Upsilon_k^{p_k}}) \models p_i$,
for $i=1, \ldots n$.

We say that a rule is sound, if and only if, in the case of the
premises of the sequent are valid sequents, then its conclusion also is.

A calculus is sound, if and only if, each of its rules is sound. We prove the
soundness of  by showing that this is the case for each one of its rules.

Considering validity of a sequent as defined in Definition <ref>,
is sound.

We show that supposing that premises of a rule are valid then, the validity of
the conclusion follows. In the sequel, we analyze each rule of .

-left We need to analyze both premises together. Thus we have
the combinations described below.

* Supposing the left premise is valid because $\alpha\imply\beta, \Delta',
\Delta \models \alpha$ and the right premise is valid because
$\alpha\imply\beta, \Delta', \Delta, \beta \models q$. We also know that
$\alpha \imply \beta \in \Delta$ and $\Delta' \subseteq \Delta$. In this
case, the conclusion holds:

* Supposing the left premise is valid because $\exists i \displaystyle (\bigcup_{k=1}^{i}{\Upsilon_k^{p_k}}) \models p_i$, for $i=1,\ldots,n$, the conclusion holds as it is the same. Supposing the left premise is true because $\Delta^q \models q$, the conclusion also holds, as $\Delta^q = \Delta$.

* Supposing the right premise is valid because $\exists i \displaystyle (\bigcup_{k=1}^{i}{\Upsilon_k^{p_k}}) \models p_i$, for $i=1,\ldots,n$, then conclusion also holds.

restart Here, we have three cases to evaluate.

* Supposing the premise is valid because $\Upsilon_1^{p_1}, \Upsilon_2^{p_2}, \ldots, \Upsilon_i^{p_i} \models p_i $, then $\exists i \displaystyle (\bigcup_{k=1}^{i}{\Upsilon_k^{p_k}}) \models p_i$, for $i=1,\ldots,n$. The conclusion is also valid.

* Supposing the premise is valid because $\exists j \displaystyle (\bigcup_{k=i+1}^{j}{\Upsilon_k^{p_k}}) \models p_j$, for $j=i+1,\ldots,n$, then conclusion also holds.

* Supposing the premise is valid because $\Delta^q \models q$, then $\Delta \models q$ and, as  $\Delta' \subseteq \Delta$, $\Delta', \Delta \models q$.

* Supposing the premise is valid because $\Upsilon_1^{p_1}, \Upsilon_2^{p_2}, \ldots, \Upsilon_i^{p_i} \models p_i $, then $\exists i \displaystyle (\bigcup_{k=1}^{i}{\Upsilon_k^{p_k}}) \models p_i$, for $i=1,\ldots,n$. This is also valid in the conclusion.

* Supposing the premise is valid because $\Delta', \Delta, \alpha \models \beta$, then every Kripke model that satisfies $\Delta'$, $\Delta$ and $\alpha$ also satisfies $\beta$. We know that $\Delta' \subseteq \Delta$. Those models also satisfies $\alpha \imply \beta$ and, then, conclusion also holds.

* Supposing the premise is valid because $\Upsilon_1^{p_1}, \Upsilon_2^{p_2}, \ldots, \Upsilon_i^{p_i} \models p_i $, then $\exists i \displaystyle (\bigcup_{k=1}^{i}{\Upsilon_k^{p_k}}) \models p_i$, for $i=1,\ldots,n$. This is also valid in the conclusion.

* Supposing the premise is valid because $\Delta', \alpha, \Delta, \alpha \models \beta$, then the conclusion also holds as $\Delta', \Delta, \alpha \models \beta$.

From Proposition <ref>, we conclude that  only prove tautologies.

§.§ Completeness

By Observation <ref>.<ref> we know that a top sequent of an open branch in an attempt proof tree has the general form below, where $q$ is an atomic formula:

\begin{equation*}
\Seq{\{\Delta'\}, \Upsilon_1^{p_1}, \Upsilon_2^{p_2}, ..., \Upsilon_n^{p_n}, \Delta}{[p_1, p_2,..., p_n], q}
\end{equation*}

From Definition <ref> and considering that $\Delta' \in \Delta$ in any sequent of an attempt proof tree following our proposed strategy, we can [color=yellow!100]ch04:lmt - Doubt: Jean-Pierre Jouannaud said that is not a definition, but a propositiondefine a invalid sequent as follows:

A sequent is invalid if and only if  $\Delta \nvDash q$ and $\forall i \displaystyle (\bigcup_{k=1}^{i}{\Upsilon_k^{p_k}}) \nvDash p_i$, for $i=1, \ldots, n$.

Our proof of completeness starts with a definition of atomic formulas on the left and right sides of a top sequent.

We can construct a Kripke counter-model $\mathcal{M}$ that satisfies atomic formulas on the right side of a top sequent, and that falsifies the atomic formula on the left. This construction can be done in the following way:

*  The model $\mathcal{M}$ has an initial world $w_0$.

*  By the proof strategy, we can conclude that, in any sequent of the proof tree, $\Upsilon_1^{p_1} \subseteq \Upsilon_2^{p_2} \subseteq \cdots \subseteq \Upsilon_n^{p_n} \subseteq \Delta$. We create a world in the model $\mathcal{M}$ corresponding for each one of these bags of formulas and, using the inclusion relation between them, we define a respective accessibility relation in the model $\mathcal{M}$ between such worlds. That is, we create worlds $w_{\Upsilon_1^{p_1}}, w_{\Upsilon_2^{p_2}}, \ldots, w_{\Upsilon_n^{p_n}}, w_{\Delta}$ related in the following form: $w_{\Upsilon_1^{p_1}} \preceq w_{\Upsilon_2^{p_2}} \preceq \cdots \preceq w_{\Upsilon_n^{p_n}} \preceq w_{\Delta}$. As $w_0$ is the first world of $\mathcal{M}$, it precedes $w_{\Upsilon_1^{p_1}}$, that is, $w_0 \preceq w_{\Upsilon_1^{p_1}}$ is also included in the accessibility relation. If $\Upsilon_i^{p_i} = \Upsilon_{i+1}^{p_{i+1}}$, for $i = 1, \ldots, n$, then the associated worlds that correspond to those sets have to be collapsed in a single world $w_{\Upsilon_i^{p_i}-\Upsilon_{i+1}^{p_{i+1}}}$. In this case, the previous relation $w_{\Upsilon_i^{p_i}} \preceq w_{\Upsilon_{i+1}^{p_{i+1}}}$ is removed from the $\preceq$ relation of the model $\mathcal{M}$ and the pairs $w_{\Upsilon_{i-1}^{p_{i-1}}} \preceq w_{\Upsilon_i^{p_i}}$ and $w_{\Upsilon_{i+1}^{p_{i+1}}} \preceq w_{\Upsilon_{i+2}^{p_{i+2}}}$ become respectively $w_{\Upsilon_{i-1}^{p_{i-1}}} \preceq w_{\Upsilon_i^{p_i}-\Upsilon_{i+1}^{p_{i+1}}}$ and $w_{\Upsilon_i^{p_i}-\Upsilon_{i+1}^{p_{i+1}}} \preceq w_{\Upsilon_{i+2}^{p_{i+2}}}$.

*  By the Definition <ref> of an invalid sequent, $\Delta \nvDash q$. The world $w_{\Delta}$ will be used to guarantee this. We set $q$ false in $w_{\Delta}$, i.e, $\mathcal{M} \nvDash_{w_{\Delta}} q$. We also set every atomic formula that is in $\Delta$ as true, i.e., $\forall p, p \in \Delta, \mathcal{M} \vDash_{w_{\Delta}} p$.

*  By the Definition <ref> of an invalid sequent, we also need that $\forall i \displaystyle (\bigcup_{k=1}^{i}{\Upsilon_k^{p_k}}) \nvDash p_i$, for $i=1, \ldots n$. Thus, for each $i, i=1, \ldots, n$ we  set $\mathcal{M} \nvDash_{w_{{\Upsilon_i^{p_i}}}} p_i$ and $\forall p, p \in \Upsilon_i^{p_i}$, being $p$ an atomic formula, $\mathcal{M} \vDash_{w_{{\Upsilon_i^{p_i}}}} p$. In the case of collapsed worlds, we keep the satisfaction relation of the previous individual worlds in the collapsed one.

*  In $w_0$ set every atomic formula inside the []-area (all of them are atomic) as false. That is, $\mathcal{M} \nvDash_{w_0} p_i$, for $i=1, \ldots, n$. We also set the atomic formula outside the []-area false in this world: $\mathcal{M} \nvDash_{w_0} q$. Those definitions make $w_0$ consistent with the $\preceq$ relation of $\mathcal{M}$.

The Figure <ref> shows the general shape of counter-models following the steps enumerated above. This procedure to construct counter-model allows us to state the following lemma:

$\nvDash p_1,\ldots, p_n$
$\nvDash q$ [.$\mathbf{w_{{\Upsilon_1^{p_1}}}}$
$\forall p, p \in \Upsilon_1^{p_1}$ , $p$ atomic, $\vDash p$
$\nvDash p_1$ [.$\vdots$ [.$\mathbf{w_{{\Upsilon_n^{p_n}}}}$
$\forall p, p \in \Upsilon_n^{p_n}$ , $p$ atomic, $\vDash p$
$\nvDash p_n$ [.$\mathbf{w_\Delta}$
$\forall p, p \in \Delta$ , $p$ atomic, $\vDash p$
$\nvDash q$ ]]]]]

General schema of counter-models

Let $S$ be a top sequent of an open branch in an attempt proof tree generated by the strategy presented in Section <ref>. Then we can construct a Kripke model $\mathcal{M}$ with a world $u$ where $\mathcal{M} \nvDash_u S$, using the proposed counter-model generation procedure.

We can prove this by induction on the degree of formulas in $\Delta$. From Definition <ref>, items <ref> and <ref> we know the value of each atomic formula in the worlds $w_\Delta$ and in each world $w_{\Upsilon_i^{p_i}}$. The inductive hypothesis is that every formula in $\Delta$ is true in $w_\Delta$. Thus, as $\Upsilon_1^{p_1} \subseteq \Upsilon_2^{p_2} \subseteq \cdots \subseteq \Upsilon_n^{p_n} \subseteq \Delta$, every formula in $\Upsilon_i^{p_i}$ is true in $w_{\Upsilon_i^{p_i}}$, for $i=1, \ldots, n$.

Thus, we have two cases to consider:

* The top sequent is in the rightmost branch of the proof tree ([]-area is empty).

Let $\alpha\imply\beta$ be a formula in  that is in $\Delta$. We show that $\mathcal{M} \vDash_{w_\Delta} \alpha\imply\beta$. In this case, by the proof strategy, $\beta \equiv (\beta_1 \imply (\beta_2 \imply \cdots \imply (\beta_m \imply p)))$, where $p$ is an atomic formula. By Definition <ref>.<ref> $\vDash_{w_\Delta} p$. As $w_\Delta$ has no accessible world from it (except for itself), $\vDash_{w_\Delta} \beta$. By the proof strategy, $\beta_m \imply p, \beta_{m-1} \imply \beta_m \imply p, \ldots, \beta_2 \imply \cdots \imply \beta_{m-1} \imply \beta_m \imply p, \beta_1 \imply \beta_2 \imply \cdots \imply \beta_{m-1} \imply \beta_m \imply p$ also are in $\Delta$. The degree of each of these formulas is less than the degree of $\alpha\imply\beta$ and, by the induction hypothesis, all of them are true in $w_\Delta$. Thus $\vDash_{w_\Delta} \beta$ and $\vDash_{w_\Delta} \alpha\imply\beta$.

As the []-area is empty, the sets $\Upsilon_i^{p_i}$ are also empty. The counter-model only has two words, $w_0$ and $w_\Delta$, following the properties described in Definition <ref>.

* The top sequent is in any other branch that is not the rightmost one ([]-area is not empty).

Let $\alpha\imply\beta$ be a formula in  that is in $\Delta$. We show that $\mathcal{M} \vDash_{w_\Delta} \alpha\imply\beta$. In this case, by the proof strategy, $\alpha \equiv (\alpha_1 \imply (\alpha_2 \imply \cdots \imply (\alpha_m \imply q)))$, where $q$ is the atomic formula in the right side of the sequent, out of the []-area. By Definition <ref>.<ref> $\nvDash_{w_\Delta} q$. By the proof strategy, $\alpha_1, \alpha_2, \dots, \alpha_m$ also are in $\Delta$. The degree of each of these formulas is less than the degree of $\alpha\imply\beta$ and, by the induction hypothesis, all of them are true in $w_\Delta$. This ensures $\nvDash_{w_\Delta} \alpha$ and $\vDash_{w_\Delta} \alpha\imply\beta$.

Considering now a formula $\alpha\imply\beta$ from  that is in $\Upsilon_i^{p_i}$. By Definition <ref>.<ref>, $\alpha\imply\beta$ also belongs to $\Delta$. From the last paragraph, we show that, for any formula $\alpha\imply\beta \in \Delta$, $\nvDash_{w_\Delta} \alpha$. As $\nvDash_{w_\Delta} \alpha$, by the accessibility relation of the Kripke model, $\nvDash_{w_{\Upsilon_i^{p_i}}} \alpha$, for each $i=1, \ldots, n$. Thus, the value of $\alpha \imply \beta$ is defined in any of these worlds by the value of $\alpha \imply \beta$ in $w_\Delta$, that we showed to be true. Thus, $\vDash_{w_{\Upsilon_i^{p_i}}} \alpha\imply\beta$.

As stated in Definition <ref>.<ref>, $\Upsilon_1^{p_1} \subseteq \Upsilon_2^{p_2} \subseteq \cdots \subseteq \Upsilon_n^{p_n} \subseteq \Delta$ and following the accessibility relation rule of the  semantic (relations are reflexive and transitive) we conclude that:

\begin{align*}
\mathcal{M} &\vDash_{w_0} \Upsilon_1^{p_1}, \nvDash_{w_0} p_1 \\
&\vDash_{w_0} \Upsilon_2^{p_2}, \nvDash_{w_0} p_2 \\
& \vdots \\
&\vDash_{w_0} \Upsilon_n^{p_n}, \nvDash_{w_0} p_n \\
&\vDash_{w_0} \Delta, \nvDash_{w_0} q \\
\end{align*}

Proving Lemma <ref>.

A rule is said invertible or double-sound iff the validity of
its conclusion implies the validity of its premises.

In other words, by Definition <ref>, we know that a counter-model for
a top sequent of a proof tree that can not be expanded anymore can be used to
construct a counter-model to every sequent in the same branch of the tree until
the conclusion (root sequent). In the case of the -right rule in our
system, not just if the premise of the rule has a counter-model, then so does the
conclusion, but the same counter-model will do. 24 called rules
with this property preserving counter model. Dyckhoff (personal
communication, 2015) proposed to call this kind of rules of strongly
invertible rules. In the case of the -left rule, this is the same when
one of the premises is valid, but, considering the case that both premises are
not valid, we need to mix the counter-models of both sides to construct the
counter-model for the conclusion of the rule. This way to produce counter-models
is what we call a weakly invertible rule.

The rules of are invertible.

We show that the rules of  are invertible when considering a proof tree
labeled in the schema presented in Section <ref>. We prove that
for the structural rules (focus and restart) and -right, from the
existence of a Kripke model that makes the premise of the rule invalid follows
that the conclusion is also invalid. For the -left rule, from the Kripke
models of the premises, we can construct a Kripke model that also makes the
conclusion of the rule invalid.

-right If the premise is invalid, then there is a Kripke model $\mathcal{M}$ where $\Delta', \Delta, \alpha \nvDash \beta$ and $\forall i \displaystyle (\bigcup_{k=1}^{i}{\Upsilon_k^{p_k}}) \nvDash p_i$, for $i=1, \ldots, n$ in a given world $u$ of $\mathcal{M}$. Thus, in the conclusion we have:

* By the definition of semantics of Section <ref>, there have to be a world $v$, $u \preceq v$, in the model $\mathcal{M}$ where $\Delta', \Delta, \alpha$ are satisfied and where $\beta$ is not. Thus, in $u$, $\alpha\imply\beta$ can not hold.

* By the model $\mathcal{M}$, for each $i$, exists a world $v_i$, $u \preceq v_i$, where $\vDash_{v_i} \Upsilon_i^{p_i}$ and $\nvDash_{v_i} p_i$.

* Thus, the conclusion is also invalid.

-left Considering that one of the premises of -left is not valid, the conclusion also is. We have to evaluate three cases:

* The right premise is invalid but the left premise is valid. Then there is a Kripke model $\mathcal{M}$ where $\alpha \imply \beta, \Delta', \Delta, \beta \nvDash q$ and $\forall i \displaystyle (\bigcup_{k=1}^{i}{\Upsilon_k^{p_k}}) \nvDash p_i$, for $i=1, \ldots, n$ from a given world $u$. Thus, in the conclusion we have:

* By the model $\mathcal{M}$, there have to be a world $v$, $u \preceq v$, in the model where $\alpha \imply \beta, \Delta', \Delta, \beta$ are satisfied and where $q$ is not.

* By the model $\mathcal{M}$, for each $i$, exists a world $v_i$, $u \preceq v_i$, where $\vDash_{v_i} \Upsilon_i^{p_i}$ and $\nvDash_{v_i} p_i$.

* Thus, the conclusion is invalid too.

* The left premise is invalid but the right premise is valid. Then there is a Kripke model $\mathcal{M}$ where $\alpha \imply \beta, \Delta', \Delta \nvDash \alpha$ and $\forall i \displaystyle (\bigcup_{k=1}^{i}{\Upsilon_k^{p_k}}) \nvDash p_i$, for $i=1, \ldots, n$, and $\Delta^q \nvDash q$ from a given world $u$. Thus, in the conclusion we have:

* By the model $\mathcal{M}$, there have to be a world $v$, $u \preceq v$, in the model where $\alpha \imply \beta, \Delta', \Delta$ are satisfied and where $\alpha$ is not.

* By the model $\mathcal{M}$, for each $i$, exists a world $v_i$, $u \preceq v_i$, where $\vDash_{v_i} \Upsilon_i^{p_i}$ and $\nvDash_{v_i} p_i$.

* We also know by $\mathcal{M}$ that there is a world $v_{\Delta^q}$, $u \preceq v_{\Delta^q}$, where $\vDash_{v_{\Delta^q}} \Delta^{q}$ and $\nvDash_{v_{\Delta^q}} q$. We also have that $\Delta^q = \Delta$ and that $\alpha \imply \beta \in \Delta$. Therefore, $\vDash_{v_{\Delta^q}} \Delta'$ and $\vDash_{v_{\Delta^q}} \alpha \imply \beta$.

* Thus, the conclusion can not be valid.

* Both left and right premises are invalid. Then there are two models $\mathcal{M}_1$ and $\mathcal{M}_2$, from the right and left premises respectively. In $\mathcal{M}_1$ there is a world $u_1$ that makes the right sequent invalid as described in item 1. In $\mathcal{M}_2$ there is a world $u_2$ that makes the sequent of the left premise invalid as described in item 2. Considering the way Kripke models are constructed based on Lemma <ref>, we know that $u_1$ and $u_2$ are root worlds of their respective counter-models. Thus, converting the two models into one, $\mathcal{M}_3$,  by mixing $u_1$ and $u_2$ in the root of $\mathcal{M}_3$, called $u_3$, we have that in $u_3$:

* $\alpha \imply \beta, \Delta', \Delta$ are satisfied and $\alpha$ is not.

* for $i=1, \ldots, n$, we have that $\vDash_{u_3} \Upsilon_i^{p_i}$ and $\nvDash_{u_3} p_i$.

* $\nvDash_{u_3} q$

* Thus, the conclusion is also invalid.

focus If we have a model that invalidates the premise, this model also invalidates the conclusion as the sequents in the premise and in the conclusion are the same despite the repetition of the focused formula $\alpha$.

restart If the restart premise is invalid, then there is a Kripke model $\mathcal{M}$ and a world $u$ from which $\Upsilon_1, \Upsilon_2, \ldots, \Upsilon_i \nvDash p_i$ and $\forall j \displaystyle (\bigcup_{k=1}^{j}{\Upsilon_k^{p_k}}) \models p_j$, for $j = i+1, \ldots, n$, and $\Delta^q \nvDash q$. Thus, in the conclusion we have:

* By the model $\mathcal{M}$, there have to be a world $v$, $u \preceq v$, in the model where $\Upsilon_1, \Upsilon_2, \ldots, \Upsilon_i$ are satisfied and where $p_i$ is not. Each $\Upsilon_k$ has the same formulas as $\Upsilon_k^{p_k}$ and, by the restart condition, we know that $\nvDash p_k$, for $k=1, \ldots, i$.

* By the model $\mathcal{M}$, for each $j$, exists a world $v_j$, $u \preceq v_j$, where $\vDash_{v_j} \Upsilon_j^{p_j}$ and $\nvDash_{v_j} p_j$.

* We also know by $\mathcal{M}$ that there is a world $v_q$, $u \preceq v_q$, where $\vDash_{v_q} \Delta^{q}$ and $\nvDash_{v_q} q$. We also have that $\Delta' \subseteq \Delta$. Therefore, $\vDash_{v_q} \Delta'$.

* Thus, the conclusion is invalid.

Now we can state a proposition about completeness of :

is complete regarding the proof strategy presented in Section <ref>

It follows direct from Proposition <ref> ( terminates) and
Lemma <ref> (we can construct a counter-model for a top
sequent in a terminated open branch of ) and Lemma <ref>
(the rules of  are invertible).

§.§ Examples

As an example, consider the Peirce formula, ${((A \to B) \to A) \to A}$, which
is very known to be a Classic tautology, but not a tautology in Intuitionistic
neither in Minimal Logic (which includes ). Proof (<ref>)
below shows the open branch of an attempt proof tree for this formula.
Following our termination criteria, this branch should be higher than the
fragment below, but, to help improve understanding, we stop that branch in the
point from which proof search just produces repetition (similar to the use of
a loop checker).

\begin{equation}
\label{proof:peirce}
\infer[\to\mbox{right}-\to_{2}]
{\color{black}{{\color{black}\{\}} {\color{black}\Rightarrow_{0}} (((A\to_{0}B)\to_{1}A)\to_{2}A),{\color{black}[]}}}{
\infer[\mbox{focus}-\to_{1}]
{\color{black}{{\color{black}\{\}},\to_{1} {\color{black}\Rightarrow_{1}} {\color{black}[]},A}}{
\infer[\to\mbox{left}-\to_{1}]
{\color{black}{\to_{1},{\color{black}\{}\to_{1}{\color{black}\}} {\color{black}\Rightarrow_{2}} {\color{black}[]},A}}{
\infer[\to\mbox{right}-\to_{0}]
{\color{black}{\to_{1},{\color{black}\{}\to_{1}{\color{black}\}},(\to_{1})^{A} {\color{black}\Rightarrow_{3}} {\color{black}[}A{\color{black}]},\to_{0}}}{
\infer[\mbox{focus}-A]
{\color{black}{\to_{1},{\color{black}\{}\to_{1}{\color{black}\}},(\to_{1})^{A},A {\color{black}\Rightarrow_{5}} {\color{black}[}A{\color{black}]},B}}{
\infer[\to\mbox{left}-\to_{1}]
{\color{black}{\to_{1},(\to_{1})^{A},A,{\color{black}\{}\to_{1},A{\color{black}\}} {\color{black}\Rightarrow_{6}} {\color{black}[}A{\color{black}]},B}}{
\vdots & \infer[\mbox{restart}-A]
{\color{black}{\to_{1},(\to_{1})^{A},A,{\color{black}\{}\to_{1},A{\color{black}\}} {\color{black}\Rightarrow_{9}} {\color{black}[}A{\color{black}]},B}}{
\infer[\mbox{focus}-\to_{1}]
{\color{black}{(\to_{1})^{B},\to_{1},(A)^{B},{\color{black}\{\}} {\color{black}\Rightarrow_{11}} {\color{black}[}B{\color{black}]},A}}{
\infer[\to\mbox{left}-\to_{1}]
{\color{black}{(\to_{1})^{B},\to_{1},(A)^{B},{\color{black}\{}\to_{1}{\color{black}\}} {\color{black}\Rightarrow_{12}} {\color{black}[}B{\color{black}]},A}}{
\infer[\to\mbox{right}-\to_{0}]
{\color{black}{(\to_{1})^{B},\to_{1},(A)^{B},{\color{black}\{}\to_{1}{\color{black}\}},(\to_{1})^{A} {\color{black}\Rightarrow_{13}} {\color{black}[}B,A{\color{black}]},\to_{0}}}{
\infer[\mbox{focus}-A]
{\color{black}{(\to_{1})^{B},\to_{1},(A)^{B},{\color{black}\{}\to_{1}{\color{black}\}},(\to_{1})^{A},A {\color{black}\Rightarrow_{16}} {\color{black}[}B,A{\color{black}]},B}}{
\infer[\to\mbox{left}-\to_{1}]
{\color{black}{(\to_{1})^{B},\to_{1},(A)^{B},(\to_{1})^{A},A,{\color{black}\{}\to_{1},A{\color{black}\}} {\color{black}\Rightarrow_{19}} {\color{black}[}B,A{\color{black}]},B}}{
\vdots & \infer[\mbox{restart}-B]
{\color{black}{(\to_{1})^{B},\to_{1},(A)^{B},(\to_{1})^{A},A,{\color{black}\{}\to_{1},A{\color{black}\}} {\color{black}\Rightarrow_{21}} {\color{black}[}B,A{\color{black}]},B}}{
\infer[\mbox{focus}-\to_{1}]
{\color{black}{\to_{1},A,(\to_{1})^{A},{\color{black}\{\}} {\color{black}\Rightarrow_{22}} {\color{black}[}A,B{\color{black}]},B}}{
\infer[\mbox{focus}-A]
{\color{black}{\to_{1},A,(\to_{1})^{A},{\color{black}\{}\to_{1}{\color{black}\}} {\color{black}\Rightarrow_{25}} {\color{black}[}A,B{\color{black}]},B}}{
\infer[\to\mbox{left}-\to_{1}]
{\color{black}{\to_{1},A,(\to_{1})^{A},{\color{black}\{}\to_{1},A{\color{black}\}} {\color{black}\Rightarrow_{26}} {\color{black}[}A,B{\color{black}]},B}}{
\vdots & {\color{black}{\to_{1},A,(\to_{1})^{A},{\color{black}\{}\to_{1},A{\color{black}\}} {\color{black}\Rightarrow_{28}} {\color{black}[}A,B{\color{black}]},B}}}
& \vdots
& \vdots
\end{equation}

From the top sequent of the open branch ($\Rightarrow_{28}$) we can generalize the sequent as:

Δ'     Υ_1^p_1     Δ    ⇒_28     [p_1, p_2]     q

{ 1, A}     _1^A     _1, A     ⇒_28     [A, B],     B

Thus, following the method described in Section <ref> we can
extract the counter-model below that falsifies the sequent:

\begin{equation}
\label{model:peirce-from-lmt}
\Tree [.{$\mathbf{w_0}$ \\ $\nvDash A$ \\ $\nvDash B$ \\ $\nvDash A \imply_0 B$ \\ $\vDash (A \imply_0 B) \imply_1 A$} [.{$\mathbf{w_{{\Upsilon^A}}}$ \\ $\nvDash A$ \\ $\nvDash B$ \\ $\nvDash A \imply_0 B$ \\ $\vDash (A \imply_0 B) \imply_1 A$} [.{$\mathbf{w_\Delta}$ \\ $\vDash A$ \\ $\nvDash B$ \\ $\nvDash A \imply_0 B$ \\ $\vDash (A \imply_0 B) \imply_1 A$} ]]]
\end{equation}

From Lemma <ref>, we can extend this counter-model to falsify
the initial sequent ($\Rightarrow_{0}$), showing that the Pierce rule does not
hold on .

As another example, we can consider the Dummett formula: $(A \imply B) \lor (B
\imply A)$. It is known that a Kripke counter-model that falsifies this
formula needs at least two branches in  and , so it is also in .
This example allows us to understand how to mix the right and left premises
counter-models to falsifies a conclusion sequent of a -left rule.

As we want to use , we need to convert the Dummett formula from the form
above to its implicational version. We use here the general translation
presented in [9]. Thus, the translated version is a formula
$\alpha$ as follows:

$\alpha \equiv ({((A \imply B) \imply A)} \imply {(((B \imply A) \imply A) \imply (C \imply A))}) \imply {(({((A \imply B) \imply B)} \imply {(((B \imply A) \imply B) \imply (C \imply B))}) \imply C)}$

To shorten the presentation, consider the following abbreviations:

α_1     =     ((A B) A) (((B A) A) (C A))

α_2     =     ((A B) B) (((B A) B) (C B))

The tree (<ref>), presents a shortened version of
a completely expanded attempt proof tree in for the Dummet formula in
implicational form. We concentrate in show the application of the operational
rules (-left and -right). We removed from the tree the focus
area on the left of each sequent and the applications of structural rules. We
also exclude from the tree the labeled formulas, just showing the necessary
formulas for the specific point in the tree. The list of sequents above the
boxed sequents in the tree represents the top sequents of each branch after the total
expansion of $\alpha_2$.

\begin{gather}
\AxiomC{$\overwrite{red}{\Seq{\ldots}{[C, A], A~(M_1)}}{$\Seq{\ldots}{[B,C], A}$ $\cancel{\Seq{\ldots,B}{[C], B}}$  $\Seq{\ldots}{[C,B],B}$  $\Seq{\ldots,A}{[C], B}$  $\Seq{\ldots}{[C], C}$  $\Seq{\ldots,B}{[ ], C}$}$}
\AxiomC{$\overwrite{red}{\Seq{\ldots, B}{[C], A~(M_2)}}{$\Seq{\ldots,B}{[B,C], A}$ $\cancel{\Seq{\ldots,B}{[C], B}}$  $\cancel{\Seq{\ldots,B}{[C,B],B}}$  $\cancel{\Seq{\ldots, B, A}{[C], B}}$  $\Seq{\ldots,B}{[C], C}$  $\Seq{\ldots,B}{[ ], C}$}$}
\BinaryInfC{$\Seq{\ldots, A \imply B}{[C], A}$}
\UnaryInfC{$\Seq{\ldots, }{[C], (A \imply B) \imply A}$}
\AxiomC{$\overwrite{red}{\Seq{\ldots}{[C, A], q~(M_1)}}{$\Seq{\ldots}{[B,C], A}$ $\cancel{\Seq{\ldots,B}{[C], B}}$  $\Seq{\ldots}{[C,B],B}$  $\Seq{\ldots,A}{[C], B}$  $\Seq{\ldots}{[C], C}$  $\Seq{\ldots,B}{[ ], C}$}$}
\AxiomC{$\cancel{\Seq{\ldots, A}{[C], A}}$}
\BinaryInfC{$\Seq{\ldots, B \imply A}{[C], A}$}
\UnaryInfC{$\Seq{\ldots, }{[C], (B \imply A) \imply A}$}
\AxiomC{$\overwrite{red}{\Seq{\ldots, }{[C], C~(M_1)}}{$\Seq{\ldots}{[B,C], A}$ $\cancel{\Seq{\ldots,B}{[C], B}}$  $\Seq{\ldots}{[C,B],B}$  $\Seq{\ldots,A}{[C], B}$  $\Seq{\ldots}{[C], C}$  $\Seq{\ldots,B}{[ ], C}$}$}
\AxiomC{$\overwrite{red}{\Seq{\ldots, A}{[ ], C~(M_3)}}{$\cancel{\Seq{\ldots,A}{[B,C], A}}$ $\cancel{\Seq{\ldots,A,B}{[C], B}}$  $\Seq{\ldots,A}{[C,B],B}$  $\Seq{\ldots,A}{[C], B}$  $\Seq{\ldots,A}{[C], C}$  $\Seq{\ldots,A,B}{[ ], C}$}$}
\BinaryInfC{$\Seq{\ldots, C \imply A}{[ ], C}$}
\BinaryInfC{$\Seq{\ldots, ((B \imply A) \imply A) \imply (C \imply A)}{[ ], C}$}
\RightLabel{$\imply-\text{left}_{(\alpha_1, C)}$}
\BinaryInfC{$\Seq{((A \imply B) \imply A) \imply (((B \imply A) \imply A) \imply (C \imply A)), \alpha_2}{[], C}$}
\UnaryInfC{$\Seq{\alpha_1, \alpha_2}{[], C}$}
\UnaryInfC{$\Seq{}{[], \alpha_1 \imply (\alpha_2 \imply C)}$}
\UnaryInfC{$\Seq{}{[], \alpha}$}
\DisplayProof
\label{proof:counter-model-gen-dummet}
\end{gather}

From the open branches of the tree (<ref>) we
extract the following three models. Models $M_1$ repeats in some branches. Thus,
we only represent it once here. We indicated in
tree (<ref>), in the top sequents of each branch,
the corresponding model generated on it, following the
Definition <ref>.

$\nvDash C$ [.$\mathbf{w_{11}}$
$\nvDash B$ $\mathbf{w_{12}}$
$\vDash A$ ]]
$\nvDash C$ [.$\mathbf{w_{21}}$
$\nvDash B$ $\mathbf{w_{22}}$
$\vDash B$ ]]
$\nvDash C$ $\mathbf{w_{31}}$
$\vDash A$
$\nvDash B$ ]
$\nvDash C$
$\nvDash C$
$\vDash B$

$\nvDash C$ [.$\mathbf{w_{11}'}$
$\nvDash B$ $\mathbf{w_{12}'}$
$\vDash B$
$\nvDash A$ ]]
$\nvDash C$ $\mathbf{w_{21}'}$
$\vDash B$
$\nvDash C$ ]

$\nvDash C$ [.$\mathbf{w_{11}''}$
$\nvDash B$ $\mathbf{w_{12}''}$
$\vDash A$
$\nvDash B$ ]]
$\nvDash C$ [.$\mathbf{w_{21}''}$
$\nvDash B$ $\mathbf{w_{22}''}$
$\vDash A$ ]]
$\nvDash C$ $\mathbf{w_{31}''}$
$\vDash A$
$\nvDash C$ ]
$\nvDash C$ $\mathbf{w_{41}''}$
$\vDash A$
$\nvDash B$
$\nvDash C$ ]

Therefore, at the point in the tree where the rule -left is applied to the
context $(\alpha_1, C)$ (the single labeled rule application in the
tree (<ref>)) we have the join of these models.
Counter-model $M_4$ below represent this unification (to legibility we remove
repeated branches in $M_4$). Thus, $M_4 \nvDash \alpha$:

$\nvDash C$ [.$\mathbf{w_{11}*}$
$\nvDash B$ $\mathbf{w_{12}*}$
$\vDash A$
$\nvDash B$ ]]
$\nvDash C$ [.$\mathbf{w_{21}*}$
$\nvDash B$ $\mathbf{w_{22}*}$
$\nvDash A$
$\vDash B$ ]]
$\nvDash C$ $\mathbf{w_{31}*}$
$\vDash A$
$\nvDash B$
$\nvDash C$ ]
$\nvDash C$
$\vDash B$
$\nvDash C$ $\mathbf{w_{51}*}$
$\vDash A$
$\vDash B$
$\nvDash C$ ]

§ CONCLUSION

We presented here the definition of a sequent calculus for proof search in the
context of the Propositional Minimal Implicational Logic (). Our calculus,
called , aims to perform the proof search for formulas in a bottom-up,
forward-always approach. Termination of the proof search is achieved without
using loop checkers during the process. is a deterministic process, which
means that the system does not need an explicit backtracking mechanism to be
complete. In this sense, is a bicomplete process, generating Kripke
counter-models from search trees produced by unsuccess proving processes.

In the definition of the calculus, we also presented some translations between
deductive systems for : ND to and to . We also
established a relation between and Fitting's Tableaux Systems for regards the counter-model generation in those systems.

We keep the development of a theorem prover for in

As future work, we can enumerate some features to be developed or
extended in the system as well as some new research topics that can be

* Precise upper bound for termination The upper bound used here for
achieving termination in is a very high bound. Many non-theorems can be
identified in a small number of steps. We can still explore options to shorten
the size of the proof search tree. Even with theorems, our labeling
mechanism, in conjunction with the usage of the restart rule, produces many
repetitions in the proof tree.

* Compression and sharing Following the techniques proposed by
[8] we can explore new ways to shorten the size of proofs
generated by .

* Minimal counter-models The size of the generated counter-model in
still takes into account every possible combination of subformulas,
yielding Kripke models with quite a lot of worlds. There is still work to be
done in order to produce smaller models. [21] presents an
implementation of the systems in [3] and in [16]
with the property of “minimally sized, normal natural deduction proofs of the
sequent, or it finds a "small" tree-based Kripke counter-model of the
sequent” using the words of the author. These references can be a good start
point to improve counter-model generation.

[1]
Andreoli, J.-M. (1992).
Logic programming with focusing proofs in linear logic.
Journal of Logic and Computation, 2(3):297–347.

[2]
Dowek, G. and Jiang, Y. (2006).
Eigenvariables, bracketing and the decidability of positive minimal
predicate logic.
Theoretical Computer Science, 360(1):193–208.

[3]
Dyckhoff, R. (1992).
Contraction-free sequent calculi for intuitionistic logic.
The Journal of Symbolic Logic, 57(03):795–807.

[4]
Dyckhoff, R. (2016).
Intuitionistic decision procedures since gentzen.
In Advances in Proof Theory, pages 245–267. Springer.

[5]
Dyckhoff, R. and Lengrand, S. (2006).
LJQ: a strongly focused calculus for intuitionistic logic.
In Logical Approaches to Computational Barriers, pages
173–185. Springer.

[6]
Ferrari, M., Fiorentini, C., and Fiorino, G. (2013).
Contraction-free linear depth sequent calculi for intuitionistic
propositional logic with the subformula property and minimal depth
Journal of automated reasoning, 51(2):129–149.

[7]
Gentzen, G. (1935).
Untersuchungen über das logische schließen. i.
Mathematische zeitschrift, 39(1):176–210.

[8]
Gordeev, L. and Haeusler, E. H. (2016).
NP vs PSPACE.
arXiv preprint arXiv:1609.09562.

[9]
Haeusler, E. H. (2015).
Propositional logics complexity and the sub-formula property.
Electronic Proceedings in Theoretical Computer Science,
Proceedings of DCM2014, Vienna, 2014.

[10]
Herbelin, H. (1995).
A $\lambda$-calculus structure isomorphic to Gentzen-style sequent
calculus structure.
In Computer Science Logic, pages 61–75. Springer.

[11]
Heuerding, A., Seyfried, M., and Zimmermann, H. (1996).
Efficient loop-check for backward proof search in some non-classical
propositional logics.
In Theorem Proving with Analytic Tableaux and Related Methods,
pages 210–225. Springer.

[12]
Hirokawa, S. (1991).
Number of proofs for implicational formulas.
Introduction to Mathematical Analysis (in Japanese),

[13]
Howe, J. M. (1997).
Two loop detection mechanisms: a comparison.
In Automated Reasoning with Analytic Tableaux and Related
Methods, pages 188–200. Springer.

[14]
Hudelmaier, J. (1993).
An O(n log n)-space decision procedure for intuitionistic
propositional logic.
Journal of Logic and Computation, 3(1):63–75.

[15]
Liang, C. and Miller, D. (2007).
Focusing and polarization in intuitionistic logic.
In Computer Science Logic, pages 451–465. Springer.

[16]
Pinto, L. and Dyckhoff, R. (1995).
Loop-free construction of counter-models for intuitionistic
propositional logic.
In Symposia Gaussiana, Conf A, pages 225–232. Walter de
Gruyter & Co (Berlin).

[17]
Prawitz, D. (2006).
Natural deduction: A proof-theoretical study.
Courier Dover Publications.

[18]
Santos, J. d. B., Vieira, B. L., and Haeusler, E. H. (2016).
A unified procedure for provability and counter-model generation in
minimal implicational logic.
Electronic Notes in Theoretical Computer Science, 324:165–179.

[19]
Seldin, J. P. (1998).
Manipulating proofs.

[20]
Statman, R. (1974).
Structural Complexity of Proofs.
PhD thesis, Stanford University.

[21]
Stoughton, A. (1996).
Porgi: a proof-or-refutation generator for intuitionistic
propositional logic.
In CADE Workshop on Proof-search in Type-theoretic Languages,
pages 109–116.

[22]
Underwood, J. (1990).
A constructive completeness proof for intuitionistic propositional
Technical report, Cornell University.

[23]
Vorob’ev, N. N. (1970).
A new algorithm for derivability in the constructive propositional
American Mathematical Society Translations, 94(2):37–71.

[24]
Weich, K. (1998).
Decision procedures for intuitionistic propositional logic by program
In Automated Reasoning with Analytic Tableaux and Related
Methods, pages 292–306. Springer.


March 7, 2022

# Extracting the $\Lambda$ Polarizing Fragmentation Function from Belle
$e^{+}e^{-}$ Data Within the TMD Formalism

Marco Zaccheddu1,2,∗ Umberto D’Alesio1,2 Leonard Gamberg3 and Francesco
Murgia2 1Dipartimento di Fisica1Dipartimento di Fisica Università di Cagliari
Università di Cagliari Cittadella Univ. Cittadella Univ. I-09042 Monserrato
(CA) I-09042 Monserrato (CA) Italy
2INFN Italy
2INFN Sezione di Cagliari Sezione di Cagliari Cittadella Univ. Cittadella
Univ. I-09042 Monserrato (CA) I-09042 Monserrato (CA) Italy
3Division of Science Italy
3Division of Science Penn State Berks Penn State Berks Reading Reading PA
19610 PA 19610 USA
∗Speaker. USA
∗Speaker<EMAIL_ADDRESS>
###### Abstract

Data from the Belle Collaboration for associated production (with a light
unpolarized hadron) and single-inclusive production of transversely polarized
$\Lambda$-hyperons in $e^{+}e^{-}$ annihilation processes allowed to extract
within a TMD approach, for the first time, the $\Lambda$ polarizing
fragmentation function. Recent theoretical developments on the computation of
cross sections for single-inclusive hadron production in $e^{+}e^{-}$
annihilation processes, within a Soft Collinear Effective Theory approach,
combined with the CSS formalism for the double-hadron production case, can be
used to perform a renewed analysis, adopting a full TMD factorization scheme.
Preliminary results and a comparison between the two analyses are presented.

TMD fragmentation functions, transverse polarization, polarizing FF, CSS
evolution equations

##  1 Introduction

Recent Belle data [1] for the transverse polarization of $\Lambda$’s, produced
in $e^{+}e^{-}\to\Lambda^{\uparrow}\pi^{\pm}/K^{\pm}+X$ and in
$e^{+}e^{-}\to\Lambda^{\uparrow}(jet)+X$, allowed to extract for the first
time the $\Lambda$ polarizing fragmentation function (pFF) [2]. Here we
present a renewed analysis of Belle data by exploiting the CSS evolution
equations and the recent theory developments on the factorization of single-
inclusive hadron production in $e^{+}e^{-}$ annihilation processes. The main
expressions for the polarization of a spin-$1/2$ hadron produced in
$e^{+}e^{-}\to h_{1}^{\uparrow}h_{2}+X$ and in $e^{+}e^{-}\to
h_{1}^{\uparrow}(jet)+X$ will be presented, along with the preliminary results
for the renewed extraction of the $\Lambda$ pFF.

##  2 Formalism

###  2.1 Double-hadron production: Transverse Polarization

We consider the process $e^{+}e^{-}\to h^{\uparrow}_{1}h_{2}+X$, where
$h_{1,2}$ are hadrons produced almost back-to-back, and, in the _hadron-frame_
configuration, $h_{1}$ has a small transverse momentum, $\bm{P}_{1T}$, with
respect to the $h_{2}$ direction (for full details on the kinematic
configuration see Ref. [3]). The transverse polarization for a spin-$1/2$
hadron $h_{1}$, produced with an unpolarized light-hadron $h_{2}$, as a
function of the light-cone momentum fractions, $z_{1,2}$, of the two final
state hadrons, is defined as the ratio of two $\bm{q}_{T}$-integrated
convolutions:

$P^{h}_{n}(z_{1},z_{2})=\frac{\int
d^{2}\bm{q}_{T}\,F^{\sin(\phi_{1}-\phi_{S_{1}})}_{TU}}{\int
d^{2}\bm{q}_{T}\,F_{UU}}=\frac{M_{h_{1}}\int
dq_{T}\;q_{T}\;d\phi_{1}\,\mathcal{B}_{1}\Big{[}\widetilde{D}^{\perp(1)}_{1T}\widetilde{\bar{D}}_{1}\Big{]}}{\int
dq_{T}\;q_{T}\;d\phi_{1}\,\mathcal{B}_{0}\Big{[}\widetilde{D}_{1}\widetilde{\bar{D}}_{1}\Big{]}}\,,$
(1)

where $M_{h_{1}}$ is the mass of $h_{1}$,
$F^{\sin(\phi_{1}-\phi_{S_{1}})}_{TU}$ and $F_{UU}$ are the convolutions
defined in the transverse momentum space [3], and
$\bm{q}_{T}=-\bm{P}_{1T}/z_{1}$. The light-cone fraction can be related to the
momentum fraction, $z_{p_{i}}={2|\bm{P}_{h_{i}}|}/{\sqrt{s}}$, and to the
usual energy fraction, $z_{h_{i}}={2E_{h_{i}}}/{\sqrt{s}}$, as
$z_{h/p}=z[1\pm{M^{2}_{h}}/{(z^{2}{Q}^{2})}]$. According to the TMD
factorization theorems and by exploiting the CSS evolution equations, the full
form of the $\mathcal{B}_{0}$ and $\mathcal{B}_{1}$ convolutions is given by
the following expressions:

$\begin{split}\mathcal{B}_{0}\Big{[}\widetilde{D}_{1}\widetilde{\bar{D}}_{1}\Big{]}=&\frac{\mathcal{H}^{(e^{+}e^{-})}(Q)}{z^{2}_{1}z^{2}_{2}}\sum_{q}e^{2}_{q}\int\frac{db_{T}}{2\pi}\,b_{T}J_{0}(b_{T}\,q_{T})\,d_{q/h_{1}}(z_{1};\bar{\mu}_{b})d_{\bar{q}/h_{2}}(z_{2};\bar{\mu}_{b})\,e^{-S_{\text{pert}}\,(\bar{\mu}_{b},Q)}\\\
\times&M_{D_{1}}(b_{c}(b_{T});b_{\text{max}})\,M_{D_{2}}(b_{c}(b_{T});b_{\text{max}})\exp\Bigg{\\{}-g_{K}(b_{c}(b_{T});b_{\text{max}})\ln{\bigg{(}\frac{Q^{2}z_{1}z_{2}}{M_{h_{1}}M_{h_{2}}}\bigg{)}}\Bigg{\\}}\,,\end{split}$
(2)

$\begin{split}\mathcal{B}_{1}\Big{[}\widetilde{D}^{\perp(1)}_{1T}\widetilde{\bar{D}}_{1}\Big{]}=&\frac{\mathcal{H}^{(e^{+}e^{-})}(Q)}{z^{2}_{1}z^{2}_{2}}\sum_{q}e^{2}_{q}\int\frac{db_{T}}{2\pi}\,b^{2}_{T}J_{1}(b_{T}\,q_{T})\widetilde{D}^{\perp(1)}_{1T}(z_{1};\bar{\mu}_{b})\,d_{\bar{q}/h_{2}}(z_{2};\bar{\mu}_{b})\,e^{-S_{\text{pert}}\,(\bar{\mu}_{b},Q)}\\\
\times&M^{\perp}_{D}(b_{c}(b_{T});b_{\text{max}})\,M_{D_{2}}(b_{c}(b_{T});b_{\text{max}})\exp\Bigg{\\{}-g_{K}(b_{c}(b_{T});b_{\text{max}})\ln{\bigg{(}\frac{Q^{2}z_{1}z_{2}}{M_{h_{1}}M_{h_{2}}}\bigg{)}}\Bigg{\\}}\,,\end{split}$
(3)

where $\mathcal{H}^{(e^{+}e^{-})}(Q)$ is the hard scattering part, for the
massless on-shell process $e^{+}e^{-}\to q\bar{q}$, at the center-of-mass
energy $Q$. By employing the integral definition of the Bessel functions of
the first kind $J_{0,1}$, we can see that both convolutions are given as
Fourier transforms in $\bm{b}_{T}$-space of different elements: $d_{q/h_{i}}$
are the unpolarized collinear fragmentation functions (FFs),
$\widetilde{D}^{\perp(1)}_{1T}$ is the first moment of the polarizing
fragmentation function, $M_{D_{i}}$ and $M^{\perp}_{D}$ are, respectively, the
parameterizations of the non-perturbative functions for the unpolarized hadron
and for the transversely polarized hadron, and they have to be extracted from
data. $g_{K}$ is a universal non-perturbative function, that takes into
account the effect of the recoil against the emission of soft gluons and,
lastly, $S_{\text{pert}}$ is the perturbative Sudakov form factor defined as
follows:

$S_{\text{pert}}\,(\bar{\mu}_{b},Q)=-\widetilde{K}(b_{*};\bar{\mu}_{b})\ln\frac{Q^{2}}{\bar{\mu}_{b}^{2}}-\int^{Q}_{\bar{\mu}_{b}}\frac{d\mu^{\prime}}{\mu^{\prime}}\,\bigg{[}2\gamma_{D}(g(\mu^{\prime});1)-\gamma_{K}(g(\mu^{\prime}))\ln{\frac{Q^{2}}{\mu^{\prime
2}}}\bigg{]}\,.$ (4)

The integration over the azimuthal dependence $d\phi_{1}$ in Eq. (1) gives a
factor of $2\pi$ that cancels in the polarization definition. Meanwhile for
the radial part, since the only terms inside the convolutions that depend on
$q_{T}$ are the Bessel functions, we can separately integrate them, obtaining
the following results:

$\begin{split}\int^{q_{T_{\text{max}}}}_{0}dq_{T}\,q_{T}J_{0}(b_{T}\,q_{T})=&\frac{q_{T_{\text{max}}}}{b_{T}}J_{1}(b_{T}\,q_{T_{\text{max}}})\\\
\end{split}$ (5)
$\begin{split}&\int^{q_{T_{\text{max}}}}_{0}dq_{T}\,q_{T}J_{1}(b_{T}\,q_{T})=\frac{\pi
q_{T_{\text{max}}}}{2b_{T}}\bigg{\\{}J_{1}(b_{T}\,q_{T_{\text{max}}})\bm{H}_{0}(b_{T}\,q_{T_{\text{max}}})-J_{0}(b_{T}\,q_{T_{\text{max}}})\bm{H}_{1}(b_{T}\,q_{T_{\text{max}}})\bigg{\\}}\,,\end{split}$
(6)

where ${\bm{H}}_{0,1}$ are the Struve functions of order zero and one
respectively. To fulfill the conditions of validity for the TMD factorization
we require that $q_{T_{\text{max}}}\ll Q$.

###  2.2 Single-inclusive hadron production: Transverse polarization

In a similar manner, it is possible to define the transverse polarization for
a spin-$1/2$ hadron, produced in $e^{+}e^{-}\to h^{\uparrow}_{1}(jet)+X$, as:

$\mathcal{P}(z_{1},j_{\perp})=\frac{{d\Delta\sigma}/{dz_{1}d^{2}\bm{j}_{\perp}}}{{d\sigma}/{dz_{1}d^{2}\bm{j}_{\perp}}}\,,$
(7)

where $\bm{j}_{\perp}$ is the hadron transverse momentum measured with respect
to the thrust axis. The polarization is defined again as the ratio of two
convolutions, derived in [4], whose full forms are given by the following
Fourier transforms (with $\bm{q}_{T}=-\bm{j}_{\perp}/z_{1}$):

$\begin{split}\frac{d\sigma}{dz_{1}d^{2}\bm{j}_{\perp}}=&\frac{\sigma_{0}}{z^{2}_{1}}\sum_{q}e^{2}_{q}\int\frac{db_{T}}{2\pi}\,b_{T}J_{0}(b_{T}\,q_{T})d_{q/h_{1}}(z_{1};\bar{\mu}_{b})\,U_{NG}(\bar{\mu}_{b},Q)\\\
&\times
M_{D_{1}}(b_{c}(b_{T});b_{\text{max}})\,\exp\Bigg{\\{}-g_{K}(b_{c}(b_{T});b_{\text{max}})\ln{\bigg{(}\frac{Qz_{1}}{M_{h_{1}}}\bigg{)}}\Bigg{\\}}\,e^{-S_{\text{pert}}\,(\bar{\mu}_{b},Q)/2},\end{split}$
(8)

$\begin{split}\frac{d\Delta\sigma}{dz_{1}d^{2}\bm{j}_{\perp}}=&\frac{\sigma_{0}}{z^{2}_{1}}\sum_{q}e^{2}_{q}\int\frac{db_{T}}{2\pi}\,b^{2}_{T}J_{1}(b_{T}\,q_{T})\widetilde{D}^{\perp(1)}_{1T}(z_{1},\bar{\mu}_{b})\,U_{NG}(\bar{\mu}_{b},Q)\\\
&\times
M^{\perp}_{D}(b_{c}(b_{T});b_{\text{max}})\,\exp\Bigg{\\{}-g_{K}(b_{c}(b_{T});b_{\text{max}})\ln{\bigg{(}\frac{Qz_{1}}{M_{h_{1}}}\bigg{)}}\Bigg{\\}}\,e^{-S_{\text{pert}}\,(\bar{\mu}_{b},Q)/2}.\end{split}$
(9)

The same elements, entering the double-hadron production case, also appear
here: namely $M^{\perp}_{D}$, up to NLO calculations, as well as the first
moment of the pFF, $\widetilde{D}^{\perp(1)}_{1T}$. Moreover, since soft
radiation is restricted to only one hemisphere, the cross section is a non-
global observable, which was also used in the study [5]. In both convolutions,
Eqs. (8) and (9), the function $U_{NG}$, accounts for the effect of such non-
global logarithms. We employ the parametrization given in Ref. [6]:

$U_{NG}(\mu_{b_{*}},Q)=\exp{\bigg{[}-C_{A}C_{F}\frac{\pi^{2}}{3}u^{2}\frac{1+(au)^{2}}{1+(bu^{c})}\bigg{]}}\,,$
(10)

with $a=0.85\,C_{A}$, $b=0.86\,C_{A}$, $c=1.33$ and

$u=\frac{1}{\beta_{0}}\ln{\bigg{[}\frac{\alpha_{s}(\mu_{b_{*}})}{\alpha_{s}(Q)}\bigg{]}}\,,$
(11)

where $\beta_{0}=\frac{11}{3}C_{A}-\frac{4}{3}T_{F}n_{f}$, with $T_{F}=1/2$
and $n_{f}$ is the number of the active flavors.

##  3 Phenomenology

We first perform a fit of the double-hadron production data alone, in order to
extract $\widetilde{D}^{\perp(1)}_{1T,\,\Lambda/q}$ and
$M^{\bot}_{D,\Lambda}$. The 126 Belle data points are given as a function of
$z_{\Lambda}$ and $z_{\pi/K}$, the energy fractions of the
$\Lambda$/$\bar{\Lambda}$ and $\pi/K$ particles. By imposing a cut for large
values of the light-hadron energy fractions, $z_{\pi/K}<0.5$, we are left with
only 96 data points. The first moment is parametrized as follows
($q=u,d,s,\text{sea}$):

$\begin{split}\widetilde{D}^{\perp(1)}_{1T,\,\Lambda/q}(z;\mu_{b})=\mathcal{N}^{p}_{q}(z)d_{q/\Lambda}(z;\mu_{b})\\\
\mathcal{N}^{p}_{q}(z)=N_{q}z^{a_{q}}(1-z)^{b_{q}}\frac{(a_{q}+b_{q})^{(a_{q}+b_{q})}}{a_{q}^{a_{q}}b_{q}^{b_{q}}}\,.\end{split}$
(12)

The best parameter choice is given by:
$N_{u},\,N_{d},\,N_{s},\,N_{\text{sea}},\,a_{s},\,b_{u},\,b_{\text{sea}}$,
with all other $a$ and $b$ parameters set to zero. Regarding the non-
perturbative functions $M_{D}$ and $g_{K}$, we have used various combinations
of them, and the best results are found by employing the following expressions
(see also [7]):

$\begin{split}M_{D}(b_{c}(b_{T});b_{\text{max}})&=\exp{\bigg{(}-\frac{\langle
p_{\perp}^{2}\rangle b^{2}_{T}}{4z^{2}_{p}}\bigg{)}}\qquad\text{Gaussian}\\\
M_{D}(b_{c}(b_{T});b_{\text{max}})&=\frac{2^{2-p}}{\Gamma(p-1)}\,(b_{T}m/z_{p})^{p-1}{K}_{p-1}(b_{T}m/z_{p})\qquad\text{Power-
Law (2)}\,,\\\ \end{split}$ (13)
$\begin{split}g_{K}(b_{c}(b_{T});b_{\text{max}})&=\frac{\alpha_{s}(C_{1}/b_{*})C_{F}}{\pi}\ln(1+b^{2}_{T}/b^{2}_{\text{max}})\qquad\text{Logarithmic}\\\
\end{split}$ (14)

Table 1: Best values of the $\chi^{2}_{\text{dof}}$ obtained fitting the double-hadron production data set only. Polarizing | Unpolarized | $g_{K}$ | $q_{T_{\text{max}}}/Q$ | $\chi^{2}_{\text{dof}}$
---|---|---|---|---
Power-Law (2) | Power-Law (2) | Logarithmic | $0.25$ | $1.203$
Power-Law (2) | Gaussian | Logarithmic | $0.25$ | $1.211$

leading to $\chi^{2}_{\text{dof}}\simeq 1.2$. In Tab. 1 we report the exact
$\chi^{2}_{\text{dof}}$ values according to the combination of the non-
perturbative functions employed for the unpolarized and polarizing FFs, and to
the $q_{T_{\text{max}}}/Q$ value used. Depending on the non-perturbative
functions utilized, 8 or 9 parameters have been extracted. In addition,
reasonable $\chi^{2}_{\text{dof}}$ values ($\chi^{2}_{\text{dof}}<1.37$) can
also be obtained with other combinations of the non-perturbative functions,
allowing for a good description of the experimental data. In Fig. 1 we show
the estimates, obtained adopting the parameters extracted with the Power-Law
model (2) (see first row of Tab. 1), of the transverse polarization of
$\Lambda$’s , produced in association with a light-hadron, compared to Belle
data [1] and to our previous fit results [2].

Figure 1: Best-fit estimates (red dashed lines) of the transverse polarization
for $\Lambda$’s produced in $e^{+}e^{-}\to\Lambda h+X$, for
$h=\pi^{\pm},K^{\pm}$, as a function of $z_{h}$ (of the associated hadron) for
different $z_{\Lambda}$ bins, obtained using the Power-Law model and compared
to our previous best-fit estimates (blue solid lines)[2]. Data are from Belle
[1].

We then perform a combined fit, including also the single-inclusive $\Lambda$
production data, on which we impose a cut for small values of the $\Lambda$
energy fraction, $z_{\Lambda}<0.3$. This leads to a total of 119 data points.
A good description is obtained by employing the following non-perturbative
functions:

$\begin{split}M_{D}(b_{c}(b_{T});b_{\text{max}})&=\frac{2^{2-p}}{\Gamma(p-1)}\,(b_{T}m)^{p-1}{K}_{p-1}(b_{T}m)\qquad\text{Power-
Law (1)}\\\ \end{split}$ (15)
$\begin{split}g_{K}(b_{c}(b_{T});b_{\text{max}})=g_{2}\ln\bigg{(}\frac{b_{T}}{b_{*}}\bigg{)}\quad
g_{2}=0.84\qquad\text{AFGR /
SIYY}\quad\text{\cite[cite]{[\@@bibref{}{afgr,siyy}{}{}]}}\,.\end{split}$ (16)

Figure 2: Best-fit estimates of the transverse polarization for $\Lambda$’s
produced in $e^{+}e^{-}\to\Lambda(jet)+X$, obtained using the Power-Law model,
as a function of the transverse momentum $j_{\perp}$ and for different
$z_{\Lambda}$ bins.

As reported in Tab. 2 the combined fit leads to a
$\chi^{2}_{\text{dof}}=1.58$. In Fig. 2 we show the estimates for the
transverse polarization against Belle data. As we can see, we are able to
describe the size and the pattern of the data, showing the possibility to
perform a combined fit of both data sets, and obtaining a better description
as compared to our previous analysis of the single-inclusive data set [2].

Table 2: Value of the $\chi^{2}_{\text{dof}}$ obtained with the combined fit of both the double-hadron and the single-inclusive hadron production data sets. Polarizing | Unpolarized | $g_{K}$ | $q_{T_{\text{max}}}/Q$ | $\chi^{2}_{\text{dof}}$
---|---|---|---|---
Power-Law (1) | Gaussian | AFGR/SIYY | $0.25$ | $1.58$

##  4 Conclusions

The main expressions for the transverse polarization of a spin-$1/2$ hadron
have been presented, both for double and single-inclusive hadron production in
$e^{+}e^{-}$ annihilation processes, in terms of convolutions in
$\bm{b}_{T}$-space, by employing the CSS evolution equations. We have then
illustrated the analyses of two fits, adopting different combinations of the
non-perturbative functions: one restricted to the double-hadron production
case and one including also the single-inclusive hadron production. A
comparison with a previous extraction has been discussed.

## References

  * [1] Y. Guan et al. [Belle Collaboration], Phys. Rev. Lett. 122, 042001 (2019).
  * [2] U. D’Alesio, F. Murgia and M. Zaccheddu, Phys. Rev. D 102, 054001 (2020).
  * [3] U. D’Alesio, F. Murgia and M. Zaccheddu, JHEP 10, 078 (2021).
  * [4] Z. Kang, D. Y. Shao and F. Zhao, JHEP 12, 127 (2020).
  * [5] L. Gamberg, Z. Kang, D. Y. Shao, J. Terry and F. Zhao, Phys. Lett. B 818, 136371 (2021).
  * [6] M. Dasgupta and G. P. Salam, Phys. Lett. B 512, 323 (2001).
  * [7] J. Collins and T. Rogers, Phys. Rev. D 91, 074020 (2015).
  * [8] C.A. Aidala, B. Field, L.P. Gamberg and T.C. Rogers, Phys. Rev. D 89, 094002 (2014).
  * [9] P. Sun, J. Isaacson, C.P. Yuan and F. Yuan, Int. J. Mod. Phys. A 33,1841006 (2018).