# Transforming intuitionistic propositional validities into validities of linear logic

A tableaux method for linear logic is briefly discussed in

D'Agostino writes (p.418-9):

''It is straightforward to translate the Linear Logic deductive policy into a stricter criterion of use: a Linear proof is a Relevant proof in which each formula is used exactly once. This suggests that a tableau method for Linear Logic can be easily obtained from the relevant tableau method of the previous section by simply imposing such a stricter use requirement. This conjecture has been shown to be correct in [Meyer et al., 1995]. The reader can check that the tableau for the Contraction axiom given in Figure 2, though being relevantly closed, is not closed. according to this stricter use requirement, since the formula-occurrence at node 4 is used twice. On the other hand, the tableau in Figure 3 is closed linearly, as well as relevantly, since each formula-occurrence is used exactly once.''

I'm interested in proofs in linear logic with the sole connective ⊸. Basically contraction corresponds to using a premiss in the tableaux $\textit{more than once}$ and weakening in the tableaux corresponds to not using a premiss in a tableaux proof. So if I want to see whether a given proof of the implicational fragment of Intuitionistic logic is valid in the fragment of linear logic with the sole connective ⊸, I just check the tableaux to see if each line was used exactly only once to derive a further line.

However, I'm not sure how to apply D'Agostino's suggested method in practice when using, for example the tableaux system for the modal intuitionistic propositional logic discussed in

I'm not sure whether some of the rules they propose violate the ban against contraction and weakening in linear logic. For example, consider the rule

$$\frac{S, \textbf{T}(\bigcirc A \rightarrow B) } {S, \hspace{0.2cm} \textbf{F}\bigcirc A, \hspace{0.2cm} \textbf{T}(\bigcirc A \rightarrow B)|S, \hspace{0.2cm} \textbf{T}B } \hspace{0.4cm}\textbf{T}_{\rightarrow\bigcirc}$$

This creates two branches: one on which $S, \hspace{0.2cm} \textbf{F}\bigcirc A, \hspace{0.2cm} \textbf{T}(\bigcirc A \rightarrow B)$ hold and the other on which $S, \textbf{T}B$ holds. It seems to involve repetition of $\textbf{T}(\bigcirc A \rightarrow B)$. Is it therefore an instance of contraction and thus incorrect in linear logic (which bans contraction and weakening)?

$\textbf{QUESTION: Given the rules proposed by Avellone and Ferrari}$ $\textbf{specifically for the implicational fragment of the intuitionistic propositional}$ $\textbf{calculus with modality}$ $\bigcirc$, $\textbf{how can I check which rules don't flout the ban on contraction and weakening}$ $\textbf{that linear logic imposes?}$ $\textbf{Another way of putting my question would be this: which rules in the purely}$ $\textbf{implicational fragment of their intuitionistic modal logic, with the modality}$ $\bigcirc$ $\textbf{employed therein, would be unacceptable}$ $\textbf{in the purely implicational fragment of linear logic with the modality}$ $\bigcirc?$