Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic

We assume the following: for arbitrary base B, and formulae $\phi, \psi, \chi$: IPL*-Monotone — If $\forces^{*}_{B} \phi,$ then $\forces^{*}_{C} \phi$ for any C $\supseteq$ B. IPL*-AndCut — If $\forces^{*}_{B} \phi \land \psi$ and $\phi, \psi \forces^{*}_{B} \chi,$ then $\forces^{*}_{B} \chi.$ The first claim follows easily from (Inf). The second is a generalization of $(\land$); it follows by induction on the structure of $\chi—an$ analogous treatment of disjunction was given by Sandqvist [48].

They are proved at the end of this section. By Theorem 1, it suffices to show that $\Gamma \forces^{*} \phi$ iff $\Gamma \forces \phi$. For this, it suffices to show $\forces^{*}_{B} \theta$ iff $\forces_{B} \theta$ for arbitrary B and $\theta.$ We proceed by induction on the structure of $\theta.$ Since the two relations are defined identically except in the case when $\theta$ is a conjunction, we restrict our attention to this case. First, we show that $\forces_{B} \theta_1 \land\theta_2$ implies $\forces^{*}_{B} \theta_1 \land\theta_2.$ By $(\land$), the conclusion is equivalent to the following: for any C $\supseteq$ B and p $\in$ A, if $\theta_1,\theta_2 \forces^{*}_{C} p$, then $\forces^{*}_{C} p$. Therefore, fix C $\supseteq$ B and p $\in$ A such that $\theta_1,\theta_2 \forces^{*}_{C} p$. By (Inf), this entails the following: if $\forces^{*}_{C} \theta_1$ and $\forces^{*}_{C} \theta_2,$ then $\forces^{*}_{C} p$. By $(\land)$ on the assumption (i.e., $\forces_{B} \theta_1 \land \theta_2),$ we obtain $\forces_{B} \theta_1$ and $\forces_{B} \theta_2.$ Hence, by the induction hypothesis (IH), $\forces^{*}_{B} \theta_1$ and $\forces^{*}_{B} \theta_2.$ Whence, by IPL*-Monotone,

$\forces^{*}_{C} \theta_1$ and $\forces^{*}_{C} \theta_2.$ Therefore, $\forces^{*}_{C} p$. We have thus shown $\forces^{*}_{B} \theta_1\land\theta_2,$ as required. Second, we show $\forces^{*}_{B} \theta_1 \land \theta_2$ implies $\forces_{B} \theta_1 \land \theta_2.$ It is easy to see that $\theta_1,\theta_2 \forces^{*}_{B} \theta_i$ obtains for i =1, 2. Applying IPL*-AndCut (setting $\phi$= $\theta_1,$ $\psi$= $\theta_2)$ once with $\chi$= $\theta_1$ and once with $\chi$= $\theta_2$ yields $\forces^{*}_{B} \theta_1$ and $\forces^{*}_{B} \theta_2.$ By the IH, $\forces_{B} \theta_1$ and $\forces_{B} \theta_2.$ Hence, $\forces_{B} \theta_1 \land \theta_2,$ as required. A curious feature of the new semantics is that the meaning of the contextformer (i.e., the comma) is not interpreted as $\land;$ that is, defining the contextformer as

$\forces^{*}_{B} \Gamma, \Delta$ iff $\forces^{*}_{B} \Gamma$ and $\forces^{*}_{B} \Delta$ we may express (Inf) with $\Gamma \forces^{*}_{B} \phi$ iff for any C $\supseteq$ B, if $\forces^{*}_{C} \Gamma,$ then $\forces^{*}_{C} \phi$ The clause for contexts is not the same as the clause for $\land$ in the new semantics. Nonetheless, as shown in the proof of Theorem 2, they are equivalent at every base—that is, $\forces^{*}_{B} \phi, \psi$ iff $\forces^{*}_{B} \phi \land \psi$ for any B. This equivalence of the two semantics yields the following:

□

Let $\top$ be any formula such that $\forces \top$—for example, $\top := p \land (p \to q) \to q$. The proof uses $\top$ to transition between the two definitions of $\land$: $$\begin{aligned} \forces_{B} \phi \;&\text{iff}\; \forces_{B} \phi \text{ and } \forces_{B} \top && (\text{def. of } \top) \\ &\text{iff}\; \forces_{B} \phi \land \top && (\land) \\ &\text{iff}\; \forall X \supseteq B\ \forall p \in A,\ \text{if } \top \forces_{X} p, \text{ then } \forces_{B} p && (\land') \\ &\text{iff}\; \forall X \supseteq B\ \forall p \in A,\ \text{if } \phi \forces_{X} p, \text{ then } \forces_{B} p && (\text{def. of } \top) \end{aligned}$$ This establishes the desired equivalence.

□

By (Inf), the conclusion $\Gamma \forces^{*}_{C} \phi$ means: for every D $\supseteq$ C , if $\forces^{*}_{D} \gamma$ for every $\gamma \in \Gamma,$ then $\forces^{*}_{D} \phi.$ Since D $\supseteq$ C $\supseteq$ B, this follows by (Inf) on the hypothesis $\Gamma \forces^{*}_{B} \phi.$

□

We proceed by induction on the structure of $\chi:$– $\chi$=p $\in$ A. This follows immediately by expanding the hypotheses with $(\land)$ and (Inf), choosing the atom to be $\chi.$– $\chi$= $\chi_1 \to \chi_2.$ By $(\to),$ the conclusion is equivalent to $\chi_1 \forces^{*}_{B} \chi_2.$ By (Inf), this is equivalent to the following: for any C $\supseteq$ B, if $\forces^{*}_{C} \chi_1,$ then $\forces^{*}_{C} \chi_2.$ Therefore, fix an arbitrary C $\supseteq$ B such that $\forces^{*}_{C} \chi_1.$ By the induction hypothesis (IH), it suffices to show: (1) $\forces^{*}_{C} \phi \land \psi$ and (2) for any D $\supseteq$ C , if $\forces^{*}_{D} \phi$ and $\forces^{*}_{D} \psi,$ then $\forces^{*}_{D} \chi_2.$ By IPL*-Monotone on the first hypothesis we immediately get (1). For (2), fix an arbitrary base D $\supseteq$ C such that

$\forces^{*}_{D} \phi,$ and $\forces^{*}_{D} \psi.$ By the second hypothesis, we obtain $\forces^{*}_{D} \chi_1 \to \chi_2$—that is, $\chi_1 \forces^{*}_{D} \chi_2.$ Hence, by (Inf) and IPL*-Monotone (since D $\supseteq$ B) we have

$\forces^{*}_{D} \chi_2,$ as required.

– $\chi$= $\chi_1 \land \chi_2.$ By $(\land$), the conclusion is equivalent to the following: for any C $\supseteq$ B and atomic p, if $\chi_1,\chi_2 \forces^{*}_{C} p$, then $\forces^{*}_{C} p$. Therefore, fix arbitrary C $\supseteq$ B and p such that $\chi_1,\chi_2 \forces^{*}_{C} p$. By (Inf), for any D $\supseteq$ C , if $\forces^{*}_{D} \chi_1$ and $\forces^{*}_{D} \chi_2,$ then $\forces^{*}_{Y} p$. We require to show $\forces^{*}_{C} p$. By the IH, it suffices to show the following: (1) $\forces^{*}_{C} \phi \land \psi$ and (2), for any E $\supseteq$ C , if

$\forces^{*}_{E} \phi$ and $\forces^{*}_{E} \psi,$ then $\forces^{*}_{E} p$. Since B $\subseteq$ C , By IPL*-Monotone on the first hypothesis we immediately get (1). For (2), fix an arbitrary base E $\supseteq$ C such that $\forces^{*}_{E} \phi$ and $\forces^{*}_{E} \psi.$ By the second hypothesis, we obtain $\forces^{*}_{D} p$, as required.

– $\chi$= $\chi_1 \lor\chi_2.$ By $(\lor),$ the conclusion is equivalent to the following: for any C $\supseteq$ B and atomic p, if $\chi_1 \forces^{*}_{C} p$ and $\chi_2 \forces^{*}_{C} p$, then $\forces^{*}_{C} p$. Therefore, fix an arbitrary base C $\supseteq$ B and atomic p such that $\chi_1 \forces^{*}_{C} p$ and $\chi_2 \forces^{*}_{C} p$. By the IH, it suffices to prove the following: (1) $\forces^{*}_{C} \phi \land \psi$ and (2). for any D $\supseteq$ C , if $\forces^{*}_{D} \phi$ and $\forces^{*}_{D} \psi,$ then $\forces^{*}_{D} p$. By IPL*-Monotone on the first hypothesis we immediately get (1). For (2), fix an arbitrary D $\supseteq$ C such that $\forces^{*}_{D} \phi$ and $\forces^{*}_{D} \psi.$ Since D $\supseteq$ B, we obtain $\forces^{*}_{D} \chi_1 \lor \chi_2$ by the second hypothesis. By $(\lor),$ we obtain $\forces^{*}_{D} p$, as required.

– $\chi$= $\bot.$ By $(\bot),$ the conclusion is equivalent to the following: $\forces^{*}_{B} r$ for all atomic r. By the IH, it suffices to prove the following: (1) $\forces^{*}_{B} \phi \land \psi$ and (2), for any C $\supseteq$ B, if $\forces^{*}_{C} \phi$ and $\forces^{*}_{C} \psi,$ then $\forces^{*}_{C} r$. By the first hypothesis we have (1). For (2), fix an arbitrary C $\supseteq$ B such that $\forces^{*}_{C} \phi$ and $\forces^{*}_{C} \psi.$ By the second hypothesis, $\forces^{*}_{C} \bot$ obtains. By $(\bot),$ we obtain $\forces^{*}_{C} r$, as required. This completes the induction.

□

We define the degree of IMLL formulae as follows: $$deg(\phi) := \begin{cases} 1 & \text{if } \phi = p \in A \\ 2 & \text{if } \phi = I \\ deg(\phi_1) + deg(\phi_2) + 1 & \text{if } \phi = \phi_1 \otimes \phi_2 \\ deg(\phi_1) + deg(\phi_2) + 1 & \text{if } \phi = \phi_1 \multimap \phi_2 \end{cases}$$ Note that for each of (I), $(\otimes)$, and $(\multimap)$, the formulae appearing in the definitional clauses all have strictly smaller degrees than the formula itself, and the atomic case $\forces_{B}^{S}$ is defined by the derivability relation as $S \vdash_{B} p$. Therefore this is a valid inductive definition. We read (Inf) as saying that $\Gamma \forces_{B}^{S} \phi$ (for $\Gamma \neq \emptyset$) means, for any extension X of B, if $\Gamma$ is supported in X with some resources U (i.e. $\forces_{X}^{U} \Gamma$), then $\phi$ is also supported by combining the resources U with the resources S (i.e., $\forces_{X}^{S,U} \phi$). The treatment of the context-former , is consistent with the case where $\Gamma,\Delta$ is a singleton. The following observation on the monotonicity of the semantics with regard to base extensions follows immediately by unfolding definitions:

□

By (Inf), it suffices to show the following: for any $B \in \mathcal{B}$, any $S \in \mathcal{M}(A)$, and any $\phi \in \mathcal{F}$, if $\forces_{B}^{S} \phi$ and $C \supseteq B$, then $\forces_{C}^{S} \phi$. We proceed by induction on $\forces^{*}$ (see Definition 14).

– base case. In this case, $\forces_{B}^{S} \phi$ is of the form $\forces_{B}^{S} p$, where $p \in A$. By (At), infer $S \vdash_{B} p$. Since $C \supseteq B$, every rule in B is also a rule in C, so $S \vdash_{C} p$. By (At), conclude $\forces_{C}^{S} p$.

– inductive step. For the inductive cases $(\otimes)$, (I), $(\multimap)$ (expanded using (Inf) and (,)), note that each takes an arbitrary extension of B—that is, says ‘for every $X \supseteq B$, . . . ’—so the conclusion follows immediately. If the statement takes place over an arbitrary $C \supseteq B$, such extensions also holds; that is, we choose $X \supseteq C$. Therefore the inductive steps also pass. To see an example, consider $\phi$ of the form $\sigma \multimap \tau$. Assume $\forces_{B}^{S} \sigma \multimap \tau$ and $C \supseteq B$, we show that $\forces_{C}^{S} \sigma \multimap \tau$. According to $(\multimap)$, the goal is $\sigma \forces_{C}^{S} \tau$. By (Inf), we fix some arbitrary $D \supseteq C$ and $T \in \mathcal{M}(A)$ such that $\forces_{D}^{T} \sigma$, and show $\forces_{D}^{S,T} \tau$.

This follows immediately from $\forces_{B}^{S} \sigma \multimap \tau$, since $D \supseteq C \supseteq B$. This completes the induction.

□

Let (1) be the statement $P, S \vdash_{B} q$ and (2) be the statement: $\forall X \supseteq B$ and $\forall T_1, \ldots, T_n \in \mathcal{M}(A)$, if $T_i \vdash_{X} p_i$ for $i = 1, \ldots, n$, then $T_1, \ldots, T_n, S \vdash_{X} q$. It is straightforward to see that (2) entails (1): we take X to be B, and $T_i$ to be $[p_i]$ for each $i = 1, \ldots, n$. Since $p_1 \vdash_{B} p_1, \ldots, p_n \vdash_{B} p_n$ all hold by ref, it follows from (2) that $p_1, \ldots, p_n, S \vdash_{B} q$, namely $P, S \vdash_{B} q$. As for (1) entails (2), we proceed by induction on how $P, S \vdash_{B} q$ is derived (see Definition 13).

– $P, S \vdash_{B} q$ holds by ref. That is, $P, S = [q]$, and $q \vdash_{B} q$ follows by ref. Here are two subcases, depending on which of P and S is $[q]$.

– Suppose $P = [q]$ and $S = \emptyset$. So (2) becomes: for every $X \supseteq B$ and T, if $T \vdash_{X} q$, then $T \vdash_{X} q$. This holds a fortiori.

– Suppose $S = [q]$ and $P = \emptyset$. Since $P = \emptyset$, (2) becomes: for every $X \supseteq B$, $S \vdash_{X} q$. This holds by ref. – $P, S \vdash_{B} q$ holds by app. We assume that $P = P_1, \ldots, P_k$, $S = S_1, \ldots, S_k$, and the following hold for some $Q_1, \ldots, Q_k$ and $r_1, \ldots, r_k$: $$P_1, S_1, Q_1 \vdash_{B} r_1, \ldots, P_k, S_k, Q_k \vdash_{B} r_k \tag{3}$$ $$(Q_1 \rhd r_1, \ldots, Q_k \rhd r_k) \Rightarrow q \text{ is in } B \tag{4}$$ In order to prove (2), we fix some arbitrary base $C \supseteq B$ and atomic multisets $T_1, \ldots, T_n$ such that $T_1 \vdash_{C} p_1, \ldots, T_n \vdash_{C} p_n$, and show $T_1, \ldots, T_n, S \vdash_{C} q$. Let us assume $P_i = p_{i1}, \ldots, p_{i\ell_i}$ for each $i = 1, \ldots, k$. We apply IH to every $P_i, S_i, Q_i \vdash_{B} r_i$ from 3, and get $T_{i1}, \ldots, T_{i\ell_i}, S_i, Q_i \vdash_{C} r_i$. Moreover, the atomic rule from 4 is also in C, since $C \supseteq B$. Therefore we can apply app and get $$T_{11}, \ldots, T_{1\ell_1}, S_1, \ldots, T_{k1}, \ldots, T_{k\ell_k}, S_k \vdash_{C} q.$$ By the definition of $S_i$ and $T_{ij}$, this is precisely $T_1, \ldots, T_n, S \vdash_{C} q$. This completes the inductive proof. It remains to prove soundness and completeness.

□

We proceed by induction on the structure of $\chi$:

– $\chi = p \in A$. This case follows immediately from (I).

– $\chi = I$. Fix $C \supseteq B$, $W \in \mathcal{M}(A)$, and $q \in A$ such that $\forces_{C}^{W} q$. It suffices to prove that $\forces_{C}^{S,T,W} q$. By (I) on (1) using $\forces_{C}^{W} q$, infer $\forces_{C}^{S,W} q$. By monotonicity on (2), infer $\forces_{C}^{T} q$. By (I) on (1) using this, infer $\forces_{C}^{S,T,W} q$, as required.

– $\chi = \sigma \otimes \tau$. By $(\otimes)$, the conclusion (3) is equivalent to the following: $\forall X \supseteq B$, $U$ $\forall p \in A$, if $\sigma, \tau \forces_{X}^{U} p$, then $\forces_{X}^{S,T,U} p$. Therefore, fix $C \supseteq B$, $W \in \mathcal{M}(A)$, and $q \in A$ such that $\sigma, \tau \forces_{C}^{W} q$; we require to show $\forces_{C}^{S,T,W} q$. By (2) and monotonicity, infer $\forces_{C}^{T} \sigma \otimes \tau$. By Lemma 12, infer $\forces_{C}^{T,W} q$. By (I) on (1), conclude $\forces_{C}^{S,T,W} q$, as required.

– $\chi = \sigma \multimap \tau$. By $(\multimap)$, the conclusion (3) is equivalent to $\sigma \forces_{B}^{S,T} \tau$. Fix some base $C \supseteq B$ and $W \in \mathcal{M}(A)$ such that $\forces_{C}^{W} \sigma$. By (Inf), it suffices to show that $\forces_{C}^{S,T,W} \tau$. By the IH, from $\forces_{C}^{S} I$ and $\forces_{C}^{W} \sigma$, infer $\forces_{C}^{S,W} \sigma$. By (I) on (2), infer $\forces_{C}^{S,T,W} \tau$, as required. This completes the induction.

□

We proceed by induction on the structure of $\chi$:

– $\chi = p \in A$. This case follows immediately from $(\otimes)$.

– $\chi = I$. Expanding (3) with (I) yields: $\forall X \supseteq B\ \forall U \in \mathcal{M}(A)\ \forall p \in A$, if $\forces_{X}^{U} p$, then $\forces_{X}^{S,T,U} p$. Therefore, fix a base $C \supseteq B$, $Q \in \mathcal{M}(A)$, and $q \in A$, such that $\forces_{C}^{Q} q$, we require to show $\forces_{C}^{S,T,Q} q$. By $(\otimes)$, it suffices to show the following: $(\dagger)\ \forces_{C}^{S} \phi \otimes \psi$ and $(\dagger\dagger)\ \phi, \psi \forces_{C}^{T,Q} q$. We have $(\dagger)$ from (1) since $C \supseteq B$. For $(\dagger\dagger)$, fix $D \supseteq C$ and $R_1, R_2 \in \mathcal{M}(A)$ such that $\forces_{D}^{R_1} \phi$ and $\forces_{D}^{R_2} \psi$; we require to show $\forces_{D}^{T,Q,R_1,R_2} q$. By (Inf), condition (2) becomes $\phi, \psi \forces_{B}^{T} I$. Hence, together with $\forces_{D}^{R_1} \phi$ and $\forces_{D}^{R_2} \psi$, it follows that $\forces_{D}^{T,R_1,R_2} I$. By (I), infer $\forall X \supseteq D\ \forall U \in \mathcal{M}(A)\ \forall p \in A$, if $\forces_{X}^{U} p$, then $\forces_{X}^{T,R_1,R_2,U} p$. Since $\forces_{C}^{Q} q$ and $D \supseteq C$, infer $\forces_{D}^{Q} q$, therefore $\forces_{D}^{T,R_1,R_2,Q} q$, as required.

– $\chi = \sigma \multimap \tau$. By $(\multimap)$ and (Inf), condition (3) becomes: $\forall X \supseteq B\ \forall U \in \mathcal{M}(A)$, if $\forces_{X}^{U} \sigma$, then $\forces_{X}^{S,T,U} \tau$. Therefore, fix $C \supseteq B$ and $P \in \mathcal{M}(A)$ such that $\forces_{C}^{P} \sigma$; we require to show $\forces_{C}^{S,T,P} \tau$. By the IH, it suffices to show the following: $(\dagger)\ \forces_{C}^{S} \phi \otimes \psi$ and $(\dagger\dagger)\ \phi, \psi \forces_{C}^{T,P} \tau$. We have $(\dagger)$ from (1). For $(\dagger\dagger)$, fix $D \supseteq C$ and $Q \in \mathcal{M}(A)$ such that $\forces_{D}^{Q} [\phi, \psi]$; we require to show $\forces_{D}^{Q,T,P} \tau$. By (2) using $\forces_{D}^{Q} [\phi, \psi]$, infer $\forces_{D}^{Q,T} \sigma \multimap \tau$. By (I), infer $\sigma \forces_{D}^{Q,T} \tau$. Since $\forces_{C}^{P} \sigma$, by monotonicity we have $\forces_{D}^{P} \sigma$. Hence, by (Inf), conclude $\forces_{D}^{Q,T,P} \tau$, as required.

– $\chi = \sigma \otimes \tau$. Fix $C \supseteq B$, $P \in \mathcal{M}(A)$, $p \in A$ such that $\sigma, \tau \forces_{C}^{P} p$. By $(\otimes)$ on 3, it suffices to show $\forces_{C}^{S,T,P} p$. By the IH, it suffices to prove the following: $(\dagger)\ \forces_{C}^{S} \phi \otimes \psi$ and $(\dagger\dagger)\ \phi, \psi \forces_{C}^{T,P} p$. We have $(\dagger)$ from (1), by monotonicity.

For $(\dagger\dagger)$, fix $D \supseteq C$ and $Q \in \mathcal{M}(A)$ such that $\forces_{D}^{Q} \phi, \psi$; we require to show $\forces_{D}^{Q,T,P} p$. By (2), from $\forces_{D}^{Q} \phi, \psi$ infer $\forces_{D}^{Q,T} \sigma \otimes \tau$. By $(\otimes)$, infer $$\text{for every } Y \supseteq D,\ V \text{ and } q,\ \text{if } \sigma, \tau \forces_{Y}^{V} q, \text{ then } \forces_{Y}^{Q,T,V} q. \tag{1}$$ Since $\sigma, \tau \forces_{D}^{P} p$, conclude $\forces_{D}^{Q,T,P} p$, as required. This completes the induction.

□

(Theorem 13—Completeness) Assume $\Gamma \forces \phi$ and let M be the bespoke base for $\Gamma \rhd \phi$. By IMLL-Flat, $\Gamma^\flat \forces_M^\emptyset \phi^\flat$. Therefore, by IMLL-AtComp, we have $\Gamma^\flat \vdash_M \phi^\flat$. Finally, by IMLL-Nat, $\left(\Gamma^\flat\right)^\natural \vdash \left(\phi^\flat\right)^\natural$—that is, $\Gamma \vdash \phi$. The required lemmas for the simulation argument hold because of the close relationship between proof for IMLL, derivability in M, and the clauses of the semantics.

□

The equivalence follows immediately from Proposition 9. Let us assume that $P = [p_1, \ldots, p_n]$. Starting from $P \forces_B^S q$, by (Inf), it means for every base $X \supseteq B$ and atomic multisets $T_1, \ldots, T_n$, $\forces_X^{T_1} p_1, \ldots, \forces_X^{T_n} p_n$ implies $\forces_X^{S,T} q$. Spelling out the definition of $\forces_B$ for atoms IMLL-AtComp, $P \forces_B^S q$ is equivalent to that, for every base $X \supseteq B$ and atomic multisets $T_1, \ldots, T_n$, $T_1 \vdash_X p_1, \ldots, T_n \vdash_X p_n$ implies $S, T \vdash_X q$. This is precisely $P, S \vdash_B q$, given Proposition 9.

□

We fix an arbitrary base $B \supseteq M$ and atomic multiset S, and proceed by induction on the structure of $\xi$.

– $\xi$ is atomic. Then by definition, $\xi^\flat = \xi$, so the statement is a tautology.

– $\xi$ is I. $$\begin{array}{ll} & \forces_B^S I^\flat \\ \text{iff} & S \vdash_B I^\flat \quad \text{(IMLL-AtComp)} \\ \text{iff} & \forall X \supseteq B,\, U,\, p,\ \text{if } U \vdash_X p, \text{ then } S, U \vdash_X p \quad \text{(Lemma 14)} \\ \text{iff} & \forall X \supseteq B,\, U,\, p,\ \text{if } \forces_X^U p, \text{ then } \forces_X^{S,U} p \quad \text{(IMLL-AtComp)} \\ \text{iff} & \forces_B^S I \quad \text{(I)} \end{array}$$

– $\xi$ is of the form $\sigma \multimap \tau$. $$\begin{array}{ll} & \forces_B^S (\sigma \multimap \tau)^\flat \\ \text{iff} & S \vdash_B (\sigma \multimap \tau)^\flat \quad \text{(IMLL-AtComp)} \\ \text{iff} & \sigma^\flat \forces_B^S \tau^\flat \quad \text{(Lemma 14)} \\ \text{iff} & \sigma \forces_B^S \tau \quad \text{(IH)} \\ \text{iff} & \forces_B^S \sigma \multimap \tau \quad (\multimap) \end{array}$$

– $\xi$ is of the form $\sigma \otimes \tau$. $$\begin{array}{ll} & \forces_B^S (\sigma \otimes \tau)^\flat \\ \text{iff} & S \vdash_B (\sigma \otimes \tau)^\flat \quad \text{(IMLL-AtComp)} \\ \text{iff} & \forall X \supseteq B,\, U,\, p,\ \text{if } \sigma^\flat, \tau^\flat \forces_X^U p, \text{ then } \forces_X^{S,U} p \quad \text{(Lemma 14)} \\ \text{iff} & \forall X \supseteq B,\, U,\, p,\ \text{if } \sigma, \tau \forces_X^U p, \text{ then } \forces_X^{S,U} p \quad \text{(IH)} \\ \text{iff} & \forces_B^S \sigma \otimes \tau \quad (\otimes). \end{array}$$ This completes the induction.

□

By the definition of $\vdash_M$ (Definition 13), it suffices to show the following: $$p^\natural \vdash p^\natural \tag{2}$$ and $$\text{if } ((P_1 \rhd q_1), \ldots, (P_n \rhd q_n) \Rightarrow r) \in M, \text{ and } S_1^\natural, P_1^\natural \vdash q_1^\natural, \ldots, S_n^\natural, P_n^\natural \vdash q_n^\natural, \text{ then } S_1^\natural, \ldots, S_n^\natural \vdash r^\natural. \tag{3}$$ First, 2 follows immediately from ax. Second, for 3, we simply need to prove the statement for each atomic rule in base M, which according to the definition of M amounts to proving the following facts:

– Suppose $(\sigma^\flat \rhd \tau^\flat) \Rightarrow (\sigma \multimap \tau)^\flat$ is in M, and $S^\natural, (\sigma^\flat)^\natural \vdash (\tau^\flat)^\natural$, we show $S^\natural \vdash ((\sigma \multimap \tau)^\flat)^\natural$. By the definition of $(\cdot)^\natural$, $S^\natural, (\sigma^\flat)^\natural \vdash (\tau^\flat)^\natural$ is $S^\natural, \sigma \vdash \tau$, and the goal $S^\natural \vdash ((\sigma \multimap \tau)^\flat)^\natural$ is $S^\natural \vdash \sigma \multimap \tau$, which follows immediately from $\multimap$I.

– Suppose $(\rhd (\sigma \multimap \tau)^\flat), (\rhd \sigma^\flat) \Rightarrow \tau^\flat$ is in M. We show that $S_1^\natural \vdash ((\sigma \multimap \tau)^\flat)^\natural$ and $S_2^\natural \vdash (\sigma^\flat)^\natural$ implies $S_1^\natural, S_2^\natural \vdash (\tau^\flat)^\natural$. This is equivalent to that $S_1^\natural \vdash \sigma \multimap \tau$ and $S_2^\natural \vdash \sigma$ implies $S_1^\natural, S_2^\natural \vdash \tau$, which follows immediately from $\multimap$E.

– Suppose $(\rhd \sigma^\flat), (\rhd \tau^\flat) \Rightarrow (\sigma \otimes \tau)^\flat$ is in M. We show that $S_1^\natural \vdash (\sigma^\flat)^\natural$ and $S_2^\natural \vdash (\tau^\flat)^\natural$ implies $S_1^\natural, S_2^\natural \vdash ((\sigma \otimes \tau)^\flat)^\natural$. According to the definition of $(\cdot)^\natural$, this is equivalent to that $S_1^\natural \vdash \sigma$ and $S_2^\natural \vdash \tau$ implies $S_1^\natural, S_2^\natural \vdash \sigma \otimes \tau$, which follows immediately from $\otimes$I.

– Suppose $(\rhd (\sigma \otimes \tau)^\flat), (\sigma^\flat, \tau^\flat \rhd p) \Rightarrow p$ is in M. We show that $S^\natural \vdash ((\sigma \otimes \tau)^\flat)^\natural$ together with $T^\natural, (\sigma^\flat)^\natural, (\tau^\flat)^\natural \vdash p^\natural$ implies $S^\natural, T^\natural \vdash p^\natural$. According to the definition of $(\cdot)^\natural$, this is equivalent to that $S^\natural \vdash \sigma \otimes \tau$ and $T^\natural, \sigma, \tau \vdash p^\natural$ implies $S^\natural, T^\natural \vdash p^\natural$, which follows immediately from $\otimes$E.

– Suppose $\Rightarrow I$ is in M, then we show $\vdash I^\natural$, namely $\vdash I$. And this is exactly II.

– Suppose $(\rhd I^\flat), (\rhd \tau^\flat) \Rightarrow \tau^\flat$ is in M, we show that $S_1^\natural \vdash (I^\flat)^\natural$ together with $S_2^\natural \vdash (\tau^\flat)^\natural$ implies $S_1^\natural, S_2^\natural \vdash (\tau^\flat)^\natural$. By the definition of $(\cdot)^\natural$, this is equivalent to that $S_1^\natural \vdash I$ and $S_2^\natural \vdash \tau$ implies $S_1^\natural, S_2^\natural \vdash \tau$. This follows from IE.

This completes the case analysis.

□

This argument is similar to the one for Proposition 7. As before, we proceed by induction on $\sforces$ (see Definition 15).

– base case. In this case, $\Gamma \sforces_{B}^{S} \phi$ is of the form $\sforces_{B}^{S} p$, where $p \in A$. By (At), infer $S \vdash_B p$. Since $C \supseteq B$, every rule in B is also a rule in B, so $S \vdash_C p$. By (At), conclude $\forces_{C}^{S} p$.

– inductive step. For the inductive cases (I), $(\multimap)$ (expanded using (Inf) and (,)), note that each takes an arbitrary extension of B—that is, says ‘for every $X \supseteq B$, . . . ’—so follows immediately. If the statement takes place over an arbitrary $C \subseteq B$, such extensions also holds; that is, we choose $X \supseteq C$. Therefore, the inductive steps also pass. In the remaining case of $(\otimes)'$, the result follows from the induction hypothesis. This completes the induction.

□

This follows mutatis mutandis on the proof of Corollary 8 It remains to prove soundness and completeness.

□

It suffices to show the following:

$$\begin{aligned} \text{(Ax)} \quad& \phi \forces \phi \\ (\multimap\text{I}) \quad& \text{If } \Gamma, \phi \forces \psi, \text{ then } \Gamma \forces \phi \multimap \psi \\ (\multimap\text{E}) \quad& \text{If } \Gamma \forces \phi \multimap \psi \text{ and } \Delta \forces \phi, \text{ then } \Gamma, \Delta \forces \psi \\ (\otimes\text{I}) \quad& \text{If } \Gamma \forces \phi \text{ and } \Delta \forces \psi, \text{ then } \Gamma, \Delta \forces \phi \otimes \psi \\ (\otimes\text{E}) \quad& \text{If } \Gamma \forces \phi \otimes \psi \text{ and } \Delta, \phi, \psi \forces \chi, \text{ then } \Gamma, \Delta \forces \chi \\ (\text{II}) \quad& \forces I \\ (\text{IE}) \quad& \text{If } \Gamma \forces \chi \text{ and } \Delta \forces I, \text{ then } \Gamma, \Delta \forces \chi \end{aligned}$$

We prove each claim separately:

– (Ax). This statement is a tautology after applying (Inf), so it holds trivially.

– $(\multimap\text{I})$. Assume (1) $\Gamma, \phi \sforces \psi$, we require show (2) $\Gamma \forces \phi \multimap \psi$. Let $B \in \mathcal{B}$ and $P \in \mathcal{M}(A)$ be arbitrary such that $\sforces_B^P \Gamma$; by (Inf), (2) becomes (3) $\forces_B^P \phi \multimap \psi$. By $(\multimap)$, from (3) infer (4) $\phi \sforces_B^P \psi$. Let $C \supseteq B$ and $T \in \mathcal{M}(A)$ be arbitrary such that $\sforces_C^T \phi$; by (Inf), (4) becomes (5) $\sforces_C^{P,T} \psi$. Thus, we require to show that (1) implies (5) for bases and resource satisfying the give conditions. By Proposition 18 (monotonicity) on $\sforces_B^P \Gamma$, infer $\sforces_C^P \Gamma$. The desired result holds by (Inf) and (,) on (1).

– $(\multimap\text{E})$. Assume (1) $\Gamma \sforces \phi \multimap \psi$ and (2) $\Delta \sforces \phi$, we require to show (3) $\Gamma, \Delta \sforces \psi$. Let $B \in \mathcal{B}$ and $P \in \mathcal{M}(A)$ be arbitrary such that (4) $\sforces_B^P \Gamma, \Delta$; by (Inf), (3) becomes (5) $\sforces_B^P \psi$. Thus: we require to show that under the conditions given (e.g., (4)), (1) and (2) imply (5). By (,) on (4), $\exists P_1, P_2 \in \mathcal{M}(A)$ such that $P = P_1, P_2$, $\forces_B^{P_1} \Gamma$, and $\forces_B^{P_2} \Delta$. By (Inf) on (1) and (2), infer (6) $\sforces_B^{P_1} \phi \multimap \psi$ and (7) $\sforces_B^{P_2} \phi$. By $(\multimap)$ on (6) infer (8) $\phi \sforces_B^{P_1} \psi$. By (Inf) on (8) using (7), infer (5), as required.

– $(\otimes\text{I})$. Assume (1) $\Gamma \sforces \phi$ and (2) $\Delta \sforces \psi$, we require to show (3) $\Gamma, \Delta \sforces \phi \otimes \psi$. Let $B \in \mathcal{B}$ and $P \in \mathcal{M}(A)$ be arbitrary such that (4) $\sforces_B^P \Gamma, \Delta$; by (Inf), (3) becomes (5) $\sforces_B^P \phi \otimes \psi$. Thus, we require to show that (1) and (2) imply (5) for the given bases and resources. By (,) on (4), $\exists P_1, P_2 \in \mathcal{M}(A)$ such that (6) $\sforces_B^{P_1} \Gamma$ and (7) $\sforces_B^{P_2} \Delta$. By (Inf) on (1) and (2) using (6) and (7), respectively, infer (8) $\sforces_B^{P_1} \phi$ and (9) $\sforces_B^{P_2} \psi$. By $(\otimes)'$ using (8) and (9) infer (5), as required.

– $(\otimes\text{E})$. Assume (1) $\Gamma \sforces \phi \otimes \psi$ and (2) $\Delta, \phi, \psi \sforces \chi$, then (3) $\Gamma, \Delta \sforces \chi$. Let $B \in \mathcal{B}$ and $P \in \mathcal{M}(A)$ be arbitrary such that (4) $\sforces_B^P \Gamma, \Delta$; by (Inf), (3) becomes (5) $\sforces_B^P \chi$. Thus, we require to show that (1) and (2) imply (5) for the bases and resource given. By (,), $\exists P_1, P_2 \in \mathcal{M}(A)$ such that $P = P_1, P_2$, (6) $\sforces_B^{P_1} \Gamma$, and (7) $\sforces_B^{P_2} \Delta$. By (Inf) on (1) using (6) infer (8) $\sforces_B^{P_1} \phi \otimes \psi$. By $(\otimes)'$ and (,), infer (9) $\sforces_B^{P_1} \phi, \psi$. By (,) on (7) and (9), infer (10) $\sforces_B^P \Delta, \phi, \psi$. By (Inf) on (2) using (10), infer (5), as required.

– (II). By $(\multimap)$, $\sforces_B^\emptyset I$ for any $B \in \mathcal{B}$. This is precisely $\sforces I$.

– (IE). Assume (1) $\Gamma \sforces \chi$ and (2) $\Delta \sforces I$, then (3) $\Gamma, \Delta \sforces \chi$. Let $B \in \mathcal{B}$ and $P \in \mathcal{M}(A)$ be arbitrary such that (4) $\sforces_B^P \Gamma, \Delta$; by (Inf), (3) becomes (5) $\sforces_B^P \chi$. Thus, we require to show that (1) and (2) imply (5) for the given base and resources. By (,) on (4), $\exists P_1, P_2 \in \mathcal{M}(A)$ such that $P = P_1, P_2$, (6) $\sforces_B^{P_1} \Gamma$, and (7) $\sforces_B^{P_2} \Delta$. By (Inf) on (1) and (2) using (6) and (7), respectively, infer (8) $\sforces_B^{P_1} \chi$ and (9) $\sforces_B^{P_2} I$. By (I) on (9), $P_2 = \emptyset$; hence, $P = P_1$. Thus (8) is (5), which is the required result.

This completes the case analysis.

□

The right-to-left direction obtains immediately by $\multimap_B^{\text{I}}$ in Definition 16. For the left-to-right observe that $\xi_1^\flat \svdash_B \xi_1^\flat$ obtains by ref in Definition 16; the desired result follows $\multimap_B^{\text{E}}$ using the hypothesis.

□

The right-to-left direction obtains by $\otimes_B^{\text{I}}$. It remains to consider the left-to-right direction.

While Definition 16 has been given inductively as closure conditions of the relations $\svdash_{-}$, we assume its correspondence to natural deduction to make the proofs of the required propositions is self-evident. Let D be a derivation witnessing $S \svdash_B (\xi_1 \otimes \xi_2)^\flat$. If the last rule used in D is $\otimes\text{I}^\flat$, then we are done. Therefore, it suffices to show that such a derivation always exists. Suppose the given D does not conclude by $\otimes\text{I}^\flat$, then we transform D such that it is the case. To this end, we require some preliminary observations about the structure of D:

– Since $(\xi_1 \otimes \xi_2)^\flat \in B$ and ref in Definition 16 only applies to A the derivation D uses at least one instance of a condition that is not ref;

– At some point $\otimes_B^{\text{I}}$ is used to conclude $(\xi_1 \otimes \xi_2)^\flat$ as it is the only condition that can do so without the formula being a premiss or an assumption (e.g., in $\otimes_B^{\text{E}}$);

– Since $(\xi_1 \otimes \xi_2)^\flat \in B$ and the rules in B all conclude with an element of A, the last condition used must be of the auxillary closure conditions;

– The closure conditions that can conclude $(\xi_1 \otimes \xi_2)^\flat$ are $\otimes_B^{\text{I}}$, $\otimes_B^{\text{E}}$, $I_B^{\text{E}}$, $\multimap_B^{\text{E}}$.

Henceforth, we shall call the ‘closure conditions’ rules as we take the natural deduction perspective; the natural deduction proofs represent a trace through Definition 16. The height h of D is the number of nodes it contains; this corresponds to the total number of times a closure condition is used to witness the judgement. We proceed by induction on h to establish that there is a derivation concluding $(\xi_1 \otimes \xi_2)^\flat$ from S by $\otimes_B^{\text{I}}$:

– base case. $h = 1$. We are done as D must conclude by an instance of $\otimes_B^{\text{I}}$.

– inductive step. $h > 1$. If D concludes by $\otimes_B^{\text{I}}$, then we are done. Otherwise, following the observations above, it concludes by one of $\otimes_B^{\text{I}}$, $\otimes_B^{\text{E}}$, $I_B^{\text{E}}$, $\multimap_B^{\text{E}}$. We proceed by case analysis to replace D with a derivation $D'$ that has the same open assumptions and conclusion but concludes by $\otimes_B^{\text{I}}$.

To simplify matters, we eliminate the case in which D ends by $\multimap_B^{\text{E}}$. In this case, the given D is of the following form, with $S = S_1, S_2$: $$\dfrac{\dfrac{S_1}{\varepsilon^\flat}\,{\scriptstyle(D_1)} \qquad \dfrac{S_2}{(\varepsilon \multimap (\xi_1 \otimes \xi_2))^\flat}\,{\scriptstyle(D_2)}}{(\xi_1 \otimes \xi_2)^\flat}\,{\multimap}\text{E}$$ Observe that $D_2$ witnesses $S_2 \svdash_B (\varepsilon \multimap (\xi_1 \otimes \xi_2))^\flat$. By Proposition 22, infer $\varepsilon^\flat, S_2 \svdash_B (\xi_1 \otimes \xi_2)^\flat$. Let $D'_2$ be a derivation witnessing this judgement, $$\dfrac{\varepsilon^\flat, S_2}{(\xi_1 \otimes \xi_2)^\flat}\,{\scriptstyle(D'_2)}$$ We can remove the instance of $\multimap_B^{\text{I}}$ in D by composing $D_1$ with $D'_2$ to yield $D''_2$, $$\dfrac{S_1, S_2}{(\xi_1 \otimes \xi_2)^\flat}\,{\scriptstyle(D''_2)}$$ Importantly, $D''_2$ has strictly fewer such instance of $\multimap_B^{\text{I}}$ (reading upward) until another rule is used that concludes $(\varepsilon \multimap (\xi_1 \otimes \xi_2))^\flat$. Therefore, without loss of generality, we can assume that the given D does not conclude by $\multimap_B^{\text{I}}$.

It remains to consider the cases where it concludes by $\otimes_B^{\text{E}}$ and $I_B^{\text{E}}$. The transformations are as follows:

– $\otimes_B^{\text{E}}$. By the induction hypothesis (IH), the sub-derivation of the premisses both end by $\otimes_B^{\text{I}}$; that is, D is of the following form, where $\varepsilon_1^\flat, \varepsilon_2^\flat, S = S_1, S_2, S_3, S_4$: $$\dfrac{\dfrac{\dfrac{S_1}{\varepsilon_1^\flat}\,{\scriptstyle(D_1)} \quad \dfrac{S_2}{\varepsilon_2^\flat}\,{\scriptstyle(D_2)}}{(\varepsilon_1 \otimes \varepsilon_2)^\flat}\,{\otimes}\text{I} \qquad \dfrac{\dfrac{S_3}{\xi_1^\flat}\,{\scriptstyle(D_3)} \quad \dfrac{S_4}{\xi_2^\flat}\,{\scriptstyle(D_4)}}{(\xi_1 \otimes \xi_2)^\flat}\,{\otimes}\text{I}}{(\xi_1 \otimes \xi_2)^\flat}\,{\otimes}\text{E}$$ By definition of $\otimes_B^{\text{E}}$, we have $\varepsilon_1^\flat, \varepsilon_2^\flat \in S_3, S_4$. There are four possible distributions of $\varepsilon_1^\flat$ and $\varepsilon_2^\flat$ in $S_3, S_4$—namely: one, $\varepsilon_1^\flat, \varepsilon_2^\flat \in S_3$; two, $\varepsilon_1^\flat, \varepsilon_2^\flat \in S_4$; three, $\varepsilon_1^\flat \in S_3$ and $\varepsilon_2^\flat \in S_4$; four, $\varepsilon_1^\flat \in S_4$ and $\varepsilon_2^\flat \in S_3$. We illustrate case one and four, the others following by symmetry.

– One. If $\varepsilon_1^\flat, \varepsilon_2^\flat \in S_3$, let $D'_3$ be the result of composing $D_1$ and $D_2$ with $D_3$. Let $S'_3 = S_3 - \varepsilon_1^\flat, \varepsilon_2^\flat$. The desired $D'$ is as follows: $$\dfrac{\dfrac{S_1, S_2, S'_3}{\xi_1^\flat}\,{\scriptstyle(D'_3)} \qquad \dfrac{S_4}{\xi_2^\flat}\,{\scriptstyle(D_4)}}{(\xi_1 \otimes \xi_2)^\flat}\,{\otimes}\text{I}$$

– Two. If $\varepsilon_1^\flat \in S_3$ and $\varepsilon_2^\flat \in S_4$. Let $D'_3$ and $D'_4$ be the results of composing $D_1$ and $D_2$ with $D_3$ and $D_4$, respectively. Let $S'_3 = S_3 - \varepsilon_1^\flat$ and $S'_4 = S_4 - \varepsilon_1^\flat, \varepsilon_2^\flat$. The desired $D'$ is as follows: $$\dfrac{\dfrac{S_1, S'_3}{\xi_1^\flat}\,{\scriptstyle(D'_3)} \qquad \dfrac{S_2, S'_4}{\xi_2^\flat}\,{\scriptstyle(D'_4)}}{(\xi_1 \otimes \xi_2)^\flat}\,{\otimes}\text{I}$$ This completes the case analysis.

– $I_B^{\text{E}}$. By the IH, the sub-derivation ending with $(\xi_1 \otimes \xi_2)^\flat$ conclude by $\otimes\text{I}$; that is, D is of the following form, where $S = S_1, S_2, S_3$: $$\dfrac{\dfrac{\dfrac{S_1}{\xi_1^\flat}\,{\scriptstyle(D_1)} \quad \dfrac{S_2}{\xi_2^\flat}\,{\scriptstyle(D_2)}}{(\xi_1 \otimes \xi_2)^\flat}\,{\otimes}\text{I} \qquad \dfrac{S_3}{I^\flat}\,{\scriptstyle(D_3)}}{(\xi_1 \otimes \xi_2)^\flat}\,I_B\text{E}$$ The desired $D'$ obtains by permuting the rules in either one of the two possible ways—for example, $$\dfrac{\dfrac{\dfrac{S_1}{\xi_1^\flat}\,{\scriptstyle(D_1)} \quad \dfrac{S_3}{I^\flat}\,{\scriptstyle(D_3)}}{\xi_1^\flat}\,I_B\text{E} \qquad \dfrac{S_2}{\xi_2^\flat}\,{\scriptstyle(D_2)}}{(\xi_1 \otimes \xi_2)^\flat}\,{\otimes}\text{I}$$ This completes the case analysis. This completes the induction.

□

The right-to-left obtains by $\multimap_B^{\text{I}}$ in Definition 16. The left-to-right proceeds as a simplified version of the proof of Proposition 23, because I is the unit of $\otimes$.

Observe that $\vdash_B$ and $\svdash_B$ are identical when restricted to A—that is, $S \vdash_B p$ iff $S \svdash_B p$ for $S, p \in \mathcal{M}(A)$. The elements of B are used as an intermediate step that moves us from the semantics of complex formulae (i.e., formulae in $\mathcal{F} - A$) to atomic formulae (i.e., formulae in A). To enable this shift we also use an auxiliary notion of support that is grounded in the auxiliary notion of derivability in a base.

□

This is the same as for the proof of IMLL-AtComp as it only concerns the base case of the relation and (Inf).

□

Fix an arbitrary $B \in \mathcal{B}$ and $P \in \mathcal{M}(A)$. We proceed by case analysis on the structure of $\xi$:

– $\xi$ is atomic. This follows from (At) and (At)$'$ by observing that $P \vdash_B p$ iff $P \svdash_B p$.

– $\xi$ is I. $$\begin{array}{ll} & \ssforces_B^P I^\flat \\ \text{iff} & P \svdash_B I^\flat \quad (\text{IMLL-AtComp}') \\ \text{iff} & P = \emptyset \quad (\text{Proposition 24}) \\ \text{iff} & \sforces_B^P I^\flat \quad (\text{I}) \end{array}$$

– $\xi$ is of the form $\xi_1 \multimap \xi_2$. $$\begin{array}{ll} & \ssforces_B^P (\xi_1 \multimap \xi_2)^\flat \\ \text{iff} & P \svdash_B (\xi_1 \multimap \xi_2)^\flat \quad (\text{IMLL-AtComp}') \\ \text{iff} & P, \xi_1^\flat \svdash_B \xi_2^\flat \quad (\text{Proposition 22}) \\ \text{iff} & \xi_1^\flat \ssforces_B^P \xi_2^\flat \quad (\text{IMLL-AtComp}') \\ \text{iff} & \xi_1^\flat \sforces_B^P \xi_2^\flat \quad (\text{IH}) \end{array}$$

– $\xi$ is of the form $\xi_1 \otimes \xi_2$. $$\begin{array}{ll} & \ssforces_B^P (\xi_1 \otimes \xi_2)^\flat \\ \text{iff} & P \svdash_B (\xi_1 \otimes \xi_2)^\flat \quad (\text{IMLL-AtComp}') \\ \text{iff} & \exists U, V \in \mathcal{M}(A) : P = (U, V),\ U \svdash_B \xi_1^\flat,\ \text{and } V \svdash_B \xi_2^\flat \quad (\text{Proposition 23}) \\ \text{iff} & \exists U, V \in \mathcal{M}(A) : P = (U, V),\ \ssforces_B^U \xi_1^\flat,\ \text{and } \ssforces_B^V \xi_2^\flat \quad (\text{IMLL-AtComp}) \\ \text{iff} & \exists U, V \in \mathcal{M}(A) : P = (U, V),\ \sforces_B^U \xi_1,\ \text{and } \sforces_B^V \xi_2 \quad (\text{IH}) \\ \text{iff} & \sforces_B^S \xi_1 \otimes \xi_2 \quad (\otimes') \end{array}$$

The (IH) refers to the induction hypothesis. This completes the induction.

□

This follows immediately from the fact that the defining conditions of $\svdash_{-}$ exactly simulate the rules defining $\vdash$ after $-^\natural$ has been applied.

□

Both the LHS and RHS are equivalent to $$\int_{x:\mathbb{C}} \mathbf{Set}\Big(\mathcal{G}(x), \mathcal{H}(x \otimes c \otimes -)\Big).$$

□

This follows by induction of the sequent $\Gamma \vdash \phi.$ In the base case, provability B is monotone on B. In the inductive steps we have $\phi(B,S) \subseteq \phi(C$, S) whenever C $\supseteq$ B; therefore, a natural transformation $\eta$: $\Gamma \Rightarrow \phi(-{\bullet}B,S)$ witnessing $\Gamma$ S B $\phi$ also witnesses $\Gamma$ S C $\phi.$ As in the B-eS in Figure 5, , and $\otimes$ are interpreted differently in the category-theoretic semantic, but have the expected behaviour:

□

The claim is that there is a natural transformation $\alpha^{,\otimes} : \llbracket\varphi\rrbracket \otimesDay \llbracket\psi\rrbracket \Rightarrow \llbracket\varphi \otimes \psi\rrbracket$. Thus, we require to show that there is a natural transformation of the form $$\llbracket\varphi\rrbracket \otimesDay \llbracket\psi\rrbracket \Rightarrow \prod_{p \in \mathbb{A}} \Big(\big(\llbracket\varphi\rrbracket \otimesDay \llbracket\psi\rrbracket \toDay \llbracket p\rrbracket\big) \toDay \llbracket p\rrbracket\Big)$$ Notice that the codomain is a product, so according to the universal mapping property (UMP) of products, it suffices to take an arbitrary $q \in \mathbb{A}$ and define a natural transformation $$\llbracket\varphi\rrbracket \otimesDay \llbracket\psi\rrbracket \Rightarrow \Big(\big(\llbracket\varphi\rrbracket \otimesDay \llbracket\psi\rrbracket \toDay \llbracket q\rrbracket\big) \toDay \llbracket q\rrbracket\Big)$$ One is induced from the evaluation natural transformation $\big(\llbracket\varphi\rrbracket \otimesDay \llbracket\psi\rrbracket\big) \otimesDay \big(\llbracket\varphi\rrbracket \otimesDay \llbracket\psi\rrbracket \toDay \llbracket q\rrbracket\big) \Rightarrow \llbracket q\rrbracket$ and the adjunction $(- \otimesDay \mathcal{F}) \dashv (\mathcal{F} \toDay -)$, as required. It is instructive to see how the semantics works with a concrete example.

□

We require to show that $S\,,\,P \vdash_{\mathcal{B}} q$ iff there exists a natural transformation of the form $\eta : \llbracket S\rrbracket \Rightarrow \llbracket q\rrbracket(\langle \mathcal{B}, P\rangle \bullet -)$. The ‘if’ direction. Assume there exists such an $\eta$. By definition, at $\langle\emptyset, S\rangle$, $\eta_{\langle\emptyset,S\rangle} : \llbracket S\rrbracket(\langle\emptyset, S\rangle) \to \llbracket q\rrbracket(\langle \mathcal{B}, S, P\rangle)$. By ref, $s \vdash_\emptyset s$ for every $s \in S$. They determine an element of $\llbracket S\rrbracket(\langle\emptyset, S\rangle)$, denoted ref. By definition, $\eta_{\langle\emptyset,S\rangle}(\mathit{ref}\,) \in \llbracket q\rrbracket(\langle \mathcal{B}, S, P\rangle)$. This determines a derivation witnessing $S\,,\,P \vdash_{\mathcal{B}} q$. The ‘only if’ direction. Assume $S\,,\,P \vdash_{\mathcal{B}} q$. Fix one such derivation, say $\Phi$. We first define $\eta$ at an arbitrary $\langle \mathcal{X}, U\rangle$. By definition of Day product as a coend and the coequalizer characterisation of coends in 5, every element in $\llbracket S\rrbracket(\langle \mathcal{X}, U\rangle)$ is an equivalence class of derivations $U \vdash_{\mathcal{X}} S$, and $\eta_{\langle \mathcal{X}, U\rangle}$ maps one such derivation to a derivation $U\,,\,P \vdash_{\mathcal{B} \cup \mathcal{X}} q$ by composition with $\Phi$, thus an element in $\llbracket q\rrbracket(\langle \mathcal{B}, P\rangle \bullet \langle \mathcal{X}, U\rangle)$. Second, the naturality of $\eta$ follows from that of derivation substitutions.

□

Recall that at each $\langle \mathcal{X}, U\rangle$, the morphism $\rho_{\langle \mathcal{X}, U\rangle}$ is of the type $$\bigotimes_{i}\Big(\llbracket S_i\rrbracket \toDay \llbracket q_i\rrbracket(\langle \mathcal{B}, T_i\rangle \bullet -)\Big)(\langle \mathcal{X}, U\rangle) \to \llbracket p\rrbracket(\langle \mathcal{B} \cup \mathcal{X}, T, U\rangle)$$ So, take an element in the Day product, namely a representative set of derivations $\{S_i\,,\,T_i\,,\,U_i \vdash_{\mathcal{X} \cup \mathcal{B}} q_i\}_{i=1,...,n}$ (where $U_1\,,\,...\,,\,U_n = U$), we turn them into a derivation for $S\,,\,U \vdash_{\mathcal{X} \cup \mathcal{B}} p$ by applying app of the given rule $(S_1 \rhd q_1, ..., S_n \rhd q_n) \Rightarrow p$ to $\Phi_1, ..., \Phi_n$. The naturality follows from the substitutions of derivations. We show soundness of the categorical notion of validity; that is, if $\Gamma \Vdash_{\mathcal{B}}^{S} \varphi$, then $\Gamma \vDash_{\mathcal{B}}^{S} \varphi$. We use the completeness result of the base-extension semantics (Theorem 13) and its proof, taking the derivability in bases as a bridge between B-eS validity and categorical validity. Fix a base $\mathcal{B}$, $\Gamma=[\gamma_1,...,\gamma_n] \in \mathbb{M}(\mathbb{F})$, $S \in \mathbb{M}(\mathbb{A})$, and $\varphi \in \mathbb{F}$. Let $(\cdot)^\flat$ and $\mathcal{M}$ be as in Section 4.3 for the sequent $\Gamma \rhd \varphi$. Without loss of generality, the image of $(\cdot)^\flat$ for non-atomic formulae are disjoint with the atoms appearing in $\mathcal{B}$ and S (disjoint). Let $\mathcal{B}^+$ be $\mathcal{B} \cup \mathcal{M}$. The following lemma is the key for soundness.

□

We proceed by induction on $Q\,,\,T\,,\,\Delta^\flat \vdash_{\mathcal{B}^+} p$ using Definition 13. We consider three cases separately: the judgement obtains by ref, the judgement obtains by the ruse of a rule $r \in \mathcal{B}$, the judgement obtains by the use of a rule from $r \in \mathcal{M}$.

We treat each case separately: First, $Q\,,\,T\,,\,\Delta^\flat \vdash_{\mathcal{B}^+} p$ is obtained by ref. This includes three subcases $Q, T, \Delta^\flat$: exactly one of Q, T, $\Delta^\flat$ is p, and the rest two are empty multisets.

– Q = p. The desired natural transformation is of the form $\eta : \llbracket p^\natural\rrbracket \Rightarrow \llbracket p^\natural\rrbracket(\langle \mathcal{B}, \emptyset\rangle \bullet -)$. Since $\llbracket p^\natural\rrbracket(\langle \mathcal{X}, U\rangle) \subseteq \llbracket p^\natural\rrbracket(\langle \mathcal{B} \cup \mathcal{X}, U\rangle)$ for all $\langle \mathcal{X}, U\rangle$, one can simply define $\eta_{\langle \mathcal{X}, U\rangle}$ as the identity function.

– T = p. The desired natural transformation is of the form $\eta : \mathbf{よ}\langle\emptyset, \emptyset\rangle \Rightarrow \llbracket p^\natural\rrbracket(\langle \mathcal{B}, p\rangle \bullet -)$ (recall that $\mathbf{よ}\langle\emptyset, \emptyset\rangle$ is the tensor unit for $\otimesDay$). At each $\langle \mathcal{X}, U\rangle$, $\eta_{\langle \mathcal{X}, U\rangle}$ is a function $\widehat{\mathbb{W}}(\langle \mathcal{X}, U\rangle, \langle\emptyset, \emptyset\rangle) \to \llbracket p^\natural\rrbracket(\langle \mathcal{B}, p\rangle \bullet \langle \mathcal{X}, U\rangle)$. The domain is nonempty precisely when $U = \emptyset$; in this case, the domain is a singleton set, say $\{\ast\}$. Also, according to disjoint, the image of $(\cdot)^\flat$ is disjoint with S, hence is disjoint with T. So $p^\natural$ is p. Then, the codomain of $\eta_{\langle \mathcal{X}, U\rangle}$ is $\llbracket p\rrbracket(\mathcal{B} \cup \mathcal{X}, p)$, and it has the element $p \vdash_{\mathcal{B} \cup \mathcal{X}} \mathit{ref} : p$, namely the proof obtained by ref on p. Then $\eta_{\langle \mathcal{X}, \emptyset\rangle}$ maps $\ast$ to ref. Naturality follows from that this is a constant function.

– $\Delta^\flat$ = p. The desired natural transformation is of the form $\eta : \llbracket p^\natural\rrbracket \Rightarrow \llbracket p^\natural\rrbracket(\langle \mathcal{B}, \emptyset\rangle \bullet -)$. At each $\langle \mathcal{X}, U\rangle$, $\eta_{\langle \mathcal{X}, U\rangle}$ is a function of the form $\llbracket p^\natural\rrbracket(\langle \mathcal{X}, U\rangle) \to \llbracket p^\natural\rrbracket(\langle \mathcal{B} \cup \mathcal{X}, U\rangle)$, and one can simply define it as the identity function, since $\llbracket p^\natural\rrbracket(\langle \mathcal{X}, U\rangle) \subseteq \llbracket p^\natural\rrbracket(\langle \mathcal{B} \cup \mathcal{X}, U\rangle)$.

Second, $r \in \mathcal{B}$. Let $r = (S_1 \rhd q_1, ..., S_n \rhd q_n) \Rightarrow p$. By app, $Q = Q_1\,,\,...\,,\,Q_n$, $T = T_1\,,\,...\,,\,T_n$, and $\Delta = \Delta_1\,,\,...\,,\,\Delta_n$ such that $Q_i\,,\,T_i\,,\,S_i\,,\,\Delta_i^\flat \vdash_{\mathcal{B}^+} q_i$ for i = 1,...,n. Hence, by the IH, there is a natural transformation $\eta_i : \llbracket Q_i^\natural, S_i\rrbracket \otimesDay \llbracket\Delta_i\rrbracket \Rightarrow \llbracket q_i^\natural\rrbracket(\langle \mathcal{B}, T_i\rangle \bullet -)$ for i = 1...n. By disjoint, the type of $\eta_i$ can be simplified as $\eta_i : \llbracket Q_i^\natural, S_i\rrbracket \otimesDay \llbracket\Delta_i\rrbracket \Rightarrow \llbracket q_i\rrbracket(\langle \mathcal{B}, T_i\rangle \bullet -)$. The desired natural transformation follows immediately by composing (the transposition of) the $\eta_i$s with the $\rho$ in Corollary 32. Third, $r \in \mathcal{M}$. We proceed by a case distinction on the atomic rules in $\mathcal{M}$:

– $r = (\rhd\psi_1^\flat, \rhd\psi_2^\flat) \Rightarrow (\psi_1 \otimes \psi_2)^\flat$. By app, there are $Q_1, Q_2, T_1, T_2 \in \mathbb{M}(\mathbb{A})$ and $\Delta_1, \Delta_2 \in \mathbb{M}(\mathbb{F})$ satisfying $Q_1\,,\,Q_2 = Q$, $T_1\,,\,T_2 = T$, $\Delta_1\,,\,\Delta_2 = \Delta$, such that $Q_i\,,\,T_i\,,\,\Delta_i^\flat \vdash_{\mathcal{B}^+} \psi_i^\flat$, for i = 1, 2. By the IH, there is a natural transformations $\eta^{\psi_i} : \llbracket\Delta_i\rrbracket \otimesDay \llbracket Q_i^\natural\rrbracket \Rightarrow \llbracket\psi_i\rrbracket(\langle \mathcal{B}, T_i\rangle \bullet -)$ for i = 1, 2. Let $\alpha^{,\otimes} : \llbracket\psi_1\rrbracket \otimesDay \llbracket\psi_2\rrbracket \Rightarrow \llbracket\psi_1 \otimes \psi_2\rrbracket$ be the natural transformation in Lemma 30. Observe that $(\eta^{\psi_1} \otimesDay \eta^{\psi_2})\,;\,\alpha^{,\otimes}_{\langle \mathcal{B},T\rangle\bullet-}$ is a natural transformation $\llbracket\Delta\rrbracket \otimesDay \llbracket Q\rrbracket \Rightarrow \llbracket(\psi^\flat)^\natural\rrbracket(\langle \mathcal{B}, T\rangle \bullet -)$, as required.

– $r = (\psi_1^\flat, \psi_2^\flat \rhd p, \rhd(\psi_1 \otimes \psi_2)^\flat) \Rightarrow p$. By App, there are $Q_1, Q_2, T_1, T_2 \in \mathbb{M}(\mathbb{A})$ and $\Delta_1, \Delta_2 \in \mathbb{M}(\mathbb{F})$ satisfying $Q_1\,,\,Q_2 = Q$, $T_1\,,\,T_2 = T$, $\Delta_1\,,\,\Delta_2 = \Delta$, such that $\Delta_1^\flat\,,\,Q_1\,,\,T_1\,,\,\psi_1^\flat\,,\,\psi_2^\flat \vdash_{\mathcal{B}} p$ and $\Delta_2^\flat\,,\,Q_2\,,\,T_2 \vdash_{\mathcal{B}} (\psi_1 \otimes \psi_2)^\flat$. By the IH, there are natural transformations $$\eta^{p} : \llbracket\Delta_1\rrbracket \otimesDay \llbracket Q_1^\natural\rrbracket \otimesDay \llbracket\psi_1\rrbracket \otimesDay \llbracket\psi_2\rrbracket \Rightarrow \llbracket p^\natural\rrbracket(\langle \mathcal{B}, T_1\rangle \bullet -)$$ $$\eta^{\psi_1\otimes\psi_2} : \llbracket\Delta_2\rrbracket \otimesDay \llbracket Q_2^\natural\rrbracket \Rightarrow \llbracket\psi_1 \otimes \psi_2\rrbracket(\langle \mathcal{B}, T_2\rangle \bullet -)$$ To finish the case, it suffices to find a natural transformation $\theta : \llbracket\psi_1 \otimes \psi_2\rrbracket \otimesDay (\llbracket\psi_1, \psi_2\rrbracket \toDay \llbracket p^\natural\rrbracket) \Rightarrow \llbracket p^\natural\rrbracket$, since the wanted natural transformation $\llbracket\Delta_1\,,\,\Delta_2\rrbracket \otimesDay \llbracket Q_1^\natural\,,\,Q_2^\natural\rrbracket \Rightarrow \llbracket p^\sharp\rrbracket(\langle \mathcal{B}, T\rangle \bullet -)$ can then be obtained as follows, omitting the evident applications of associativity and commutativity of $\otimesDay$: $$\begin{array}{c} \llbracket\Delta_1\,,\,\Delta_2\rrbracket \otimesDay \llbracket Q_1^\natural\,,\,Q_2^\natural\rrbracket \\ \big\downarrow{\scriptstyle\;\widehat{\eta^{p}} \otimes \eta^{\psi_1\otimes\psi_2}} \\ \big(\llbracket\psi_1\rrbracket \otimesDay \llbracket\psi_2\rrbracket\big) \toDay \llbracket p^\natural\rrbracket(\langle \mathcal{B}, T_1\rangle \bullet -) \otimesDay \llbracket\psi_1 \otimes \psi_2\rrbracket(\langle \mathcal{B}, T_2\rangle \bullet -) \\ \big\downarrow{\scriptstyle\;\simeq \text{ via Lem. 28}} \\ \big(\llbracket\psi_1\rrbracket \otimesDay \llbracket\psi_2\rrbracket \toDay \llbracket p^\natural\rrbracket\big)(\langle \mathcal{B}, T_1\rangle \bullet -) \otimesDay \llbracket\psi_1 \otimes \psi_2\rrbracket(\langle \mathcal{B}, T_2\rangle \bullet -) \\ \big\downarrow{\scriptstyle\;\simeq} \\ \Big(\big(\llbracket\psi_1\rrbracket \otimesDay \llbracket\psi_2\rrbracket \toDay \llbracket p^\natural\rrbracket\big) \otimesDay \llbracket\psi_1 \otimes \psi_2\rrbracket\Big) \circ \big((\langle \mathcal{B}, T_1\rangle \bullet -) \otimesDay (\langle \mathcal{B}, T_2\rangle \bullet -)\big) \\ \big\downarrow{\scriptstyle\;\theta\circ\simeq} \\ \llbracket p^\sharp\rrbracket \circ (\langle \mathcal{B}, T_1\,,\,T_2\rangle \bullet -) \end{array}$$ This is essentially a category-theoretic version of Lemma 12. We proceed by sub-induction on the structure of p.

– $p^\natural$ = p. This follows immediately from: $$\llbracket\psi_1 \otimes \psi_2\rrbracket = \prod_{p \in \mathbb{A}}\Big(\big(\llbracket\psi_1\rrbracket \otimesDay \llbracket\psi_2\rrbracket \toDay \llbracket p\rrbracket\big) \toDay \llbracket p\rrbracket\Big)$$ Simply apply the projection on p and evaluation for $\toDay$.

– $p^\natural = \chi_1 \otimes \chi_2$. We require to define a natural transformation $\theta^{\chi_1\otimes\chi_2}$ of the form $$\theta^{\chi_1 \otimes \chi_2} : \llbracket\psi_1 \otimes \psi_2\rrbracket \otimesDay \Big(\llbracket\psi_1, \psi_2\rrbracket \toDay \prod_{p \in \mathbb{A}} \big(\llbracket\chi_1\rrbracket \otimesDay \llbracket\chi_2\rrbracket \toDay \llbracket p\rrbracket\big) \toDay \llbracket p\rrbracket\Big) \Rightarrow \prod_{p \in \mathbb{A}} \big(\llbracket\chi_1\rrbracket \otimesDay \llbracket\chi_2\rrbracket \toDay \llbracket p\rrbracket\big) \toDay \llbracket p\rrbracket$$ Since the codomain is a product, according to the universal mapping property (UMP) of products, it suffices to define, for each q, $\theta^{\chi_1\otimes\chi_2}[q] : \mathrm{dom}(\theta^{\chi_1\otimes\chi_2}) \Rightarrow (\llbracket\chi_1\rrbracket \otimesDay \llbracket\chi_2\rrbracket \toDay \llbracket q\rrbracket) \toDay \llbracket q\rrbracket$. This is obtained by currying the composite of the following natural transformations, where on the arrows we only explicate the key components and omit the evident identity natural transformations: $$\begin{array}{c} \llbracket\psi_1 \otimes \psi_2\rrbracket \otimesDay \Big(\llbracket\psi_1,\psi_2\rrbracket \toDay \prod_{p\in\mathbb{A}}\big((\llbracket\chi_1\rrbracket\otimesDay\llbracket\chi_2\rrbracket\toDay\llbracket p\rrbracket)\toDay\llbracket p\rrbracket\big)\Big) \otimesDay \big(\llbracket\chi_1\rrbracket\otimesDay\llbracket\chi_2\rrbracket\toDay\llbracket q\rrbracket\big) \\ \big\downarrow{\scriptstyle\;\pi_q} \\ \llbracket\psi_1 \otimes \psi_2\rrbracket \otimesDay \Big(\llbracket\psi_1,\psi_2\rrbracket \toDay \big((\llbracket\chi_1\rrbracket\otimesDay\llbracket\chi_2\rrbracket\toDay\llbracket q\rrbracket)\toDay\llbracket q\rrbracket\big)\Big) \otimesDay \big(\llbracket\chi_1\rrbracket\otimesDay\llbracket\chi_2\rrbracket\toDay\llbracket q\rrbracket\big) \\ \big\downarrow{\scriptstyle\;\text{reass}} \\ \llbracket\psi_1 \otimes \psi_2\rrbracket \otimesDay \Big(\big(\llbracket\chi_1\rrbracket\otimesDay\llbracket\chi_2\rrbracket\toDay\llbracket q\rrbracket\big)\toDay\big(\llbracket\psi_1,\psi_2\rrbracket\toDay\llbracket q\rrbracket\big)\Big) \otimesDay \big(\llbracket\chi_1\rrbracket\otimesDay\llbracket\chi_2\rrbracket\toDay\llbracket q\rrbracket\big) \\ \big\downarrow{\scriptstyle\;id \otimesDay ev} \\ \llbracket\psi_1 \otimes \psi_2\rrbracket \otimesDay \big(\llbracket\psi_1\,,\,\psi_2\rrbracket \toDay \llbracket q\rrbracket\big) \\ \big\downarrow{\scriptstyle\;\theta^{q}} \\ \llbracket q\rrbracket \end{array}$$ Here reass is re-association.

– $p^\natural$ = I. Spelling out the definition of $\llbracket I\rrbracket$, it amounts to finding a natural transformation of the form: $$\theta : \prod_{p \in \mathbb{A}}\Big(\big(\llbracket\psi_1\rrbracket \otimesDay \llbracket\psi_2\rrbracket \toDay \llbracket p\rrbracket\big) \toDay \llbracket p\rrbracket\Big) \otimesDay \Big(\llbracket\psi_1\rrbracket \otimesDay \llbracket\psi_2\rrbracket \toDay \prod_{p \in \mathbb{A}}(\llbracket p\rrbracket \toDay \llbracket p\rrbracket)\Big) \Rightarrow \prod_{p \in \mathbb{A}}(\llbracket p\rrbracket \toDay \llbracket p\rrbracket)$$ Notice that the codomain is a product so by UMP of products, it suffices to find $\theta[q] : \mathrm{dom}(\theta) \Rightarrow (\llbracket q\rrbracket \toDay \llbracket q\rrbracket)$ for arbitrary fixed $q \in \mathbb{A}$. To this we define $\theta'[q] : \mathrm{dom}(\theta)\otimesDay \llbracket q\rrbracket \Rightarrow \llbracket q\rrbracket$ as the following composition: $$\begin{array}{c} \prod_{p\in\mathbb{A}}\Big(\big(\llbracket\psi_1\rrbracket\otimesDay\llbracket\psi_2\rrbracket\toDay\llbracket p\rrbracket\big)\toDay\llbracket p\rrbracket\Big) \otimesDay \Big(\llbracket\psi_1\rrbracket\otimesDay\llbracket\psi_2\rrbracket\toDay\prod_{p\in\mathbb{A}}(\llbracket p\rrbracket\toDay\llbracket p\rrbracket)\Big) \otimesDay \llbracket q\rrbracket \\ \big\downarrow{\scriptstyle\;\pi_q} \\ \Big(\big(\llbracket\psi_1\rrbracket\otimesDay\llbracket\psi_2\rrbracket\toDay\llbracket q\rrbracket\big)\toDay\llbracket q\rrbracket\Big) \otimesDay \Big(\llbracket\psi_1\rrbracket\otimesDay\llbracket\psi_2\rrbracket\toDay(\llbracket q\rrbracket\toDay\llbracket q\rrbracket)\Big) \otimesDay \llbracket q\rrbracket \\ \big\downarrow{\scriptstyle\;\pi_q} \\ \Big(\big(\llbracket\psi_1\rrbracket\otimesDay\llbracket\psi_2\rrbracket\toDay\llbracket q\rrbracket\big)\toDay\llbracket q\rrbracket\Big) \otimesDay \Big(\llbracket q\rrbracket\toDay(\llbracket\psi_1\rrbracket\otimesDay\llbracket\psi_2\rrbracket\toDay\llbracket q\rrbracket)\Big) \otimesDay \llbracket q\rrbracket \\ \big\downarrow{\scriptstyle\;id \otimesDay ev} \\ \Big(\big(\llbracket\psi_1\rrbracket \otimesDay \llbracket\psi_2\rrbracket \toDay \llbracket q\rrbracket\big) \toDay \llbracket q\rrbracket\Big) \otimesDay \big(\llbracket\psi_1\rrbracket \otimesDay \llbracket\psi_2\rrbracket \toDay \llbracket q\rrbracket\big) \\ \big\downarrow{\scriptstyle\;ev} \\ \llbracket q\rrbracket \end{array}$$

– $p^\natural = \chi_1 \multimap \chi_2$. By IH (for the case of $\chi_2$), there exists a natural transformation $\theta^{\chi_2} : \llbracket\psi_1 \otimes \psi_2\rrbracket \otimesDay (\llbracket\psi_1\rrbracket \otimesDay \llbracket\psi_2\rrbracket \toDay \llbracket\chi_2\rrbracket) \Rightarrow \llbracket\chi_2\rrbracket$. Then the desired natural transformation $\theta^{\chi_1\multimap\chi_2}$ is obtained by currying the following composed natural transformation: $$\begin{array}{c} \llbracket\psi_1 \otimes \psi_2\rrbracket \otimesDay \Big(\llbracket\psi_1\rrbracket \otimesDay \llbracket\psi_2\rrbracket \toDay \llbracket\chi_1 \multimap \chi_2\rrbracket\Big) \otimesDay \llbracket\chi_1\rrbracket \\ \big\downarrow{\scriptstyle\;\text{def}} \\ \llbracket\psi_1 \otimes \psi_2\rrbracket \otimesDay \Big(\llbracket\psi_1\rrbracket \otimesDay \llbracket\psi_2\rrbracket \toDay (\llbracket\chi_1\rrbracket \toDay \llbracket\chi_2\rrbracket)\Big) \otimesDay \llbracket\chi_1\rrbracket \\ \big\downarrow{\scriptstyle\;\text{reass}} \\ \llbracket\chi_1\rrbracket \otimesDay \llbracket\psi_1 \otimes \psi_2\rrbracket \otimesDay \Big(\llbracket\chi_1\rrbracket \toDay (\llbracket\psi_1\rrbracket \otimesDay \llbracket\psi_2\rrbracket \toDay \llbracket\chi_2\rrbracket)\Big) \\ \big\downarrow{\scriptstyle\;id \otimesDay ev} \\ \llbracket\psi_1 \otimes \psi_2\rrbracket \otimesDay \big(\llbracket\psi_1\rrbracket \otimesDay \llbracket\psi_2\rrbracket \toDay \llbracket\chi_2\rrbracket\big) \\ \big\downarrow{\scriptstyle\;\theta^{\chi_2}} \\ \llbracket\chi_2\rrbracket \end{array}$$

– $\multimap$-I case. The last rule is: $(\psi_1^\flat \rhd \psi_2^\flat) \Rightarrow (\psi_1 \multimap \psi_2)^\flat$. Then $\Delta^\flat\,,\,Q\,,\,T\,,\,\psi_1^\flat \vdash_{\mathcal{B}^+} \psi_2^\flat$. By IH, there exists a natural transformation $$\eta : \llbracket\Delta\rrbracket \otimesDay \llbracket Q^\natural\rrbracket \otimesDay \llbracket\psi_1\rrbracket \Rightarrow \llbracket\psi_2\rrbracket(\langle \mathcal{B}, T\rangle \bullet -)$$ By adjunction, $\llbracket\Delta\rrbracket \otimesDay \llbracket Q^\natural\rrbracket \Rightarrow \big(\llbracket\psi_1\rrbracket \toDay \llbracket\psi_2\rrbracket(\langle \mathcal{B}, T\rangle \bullet -)\big)$, which is equivalently of the type $\llbracket\Delta\rrbracket \otimesDay \llbracket Q^\natural\rrbracket \Rightarrow \big(\llbracket\psi_1\rrbracket \toDay \llbracket\psi_2\rrbracket\big)(\langle \mathcal{B}, T\rangle \bullet -)$ (Lemma 28). The wanted natural $\eta$ is then obtained by adjunction.

– $\multimap$-E case. The last rule is: $((\psi_1 \multimap \psi_2)^\flat, \psi_1^\flat) \Rightarrow \psi_2^\flat$. So it is derived from $Q_1\,,\,T_1\,,\,\Delta_1^\flat \vdash_{\mathcal{B}^+} (\psi_1 \multimap \psi_2)^\flat$ and $Q_2\,,\,T_2\,,\,\Delta_2^\flat \vdash_{\mathcal{B}^+} \psi_1^\flat$ using app, where $Q_1\,,\,Q_2 = Q$, $T = T_1\,,\,T_2$, $\Delta_1\,,\,\Delta_2 = \Delta$. By IH, there are natural transformations $$\eta^{\psi_1\multimap\psi_2} : \llbracket\Delta_1\rrbracket \otimesDay \llbracket Q_1^\natural\rrbracket \Rightarrow \llbracket\psi_1 \multimap \psi_2\rrbracket(\langle \mathcal{B}, T_1\rangle \bullet -)$$ $$\eta^{\psi_1} : \llbracket\Delta_2\rrbracket \otimesDay \llbracket Q_2^\natural\rrbracket \Rightarrow \llbracket\psi_1\rrbracket(\langle \mathcal{B}, T_2\rangle \bullet -)$$ Then the following composition is the desired natural transformation: $$\begin{array}{c} \llbracket\Delta\rrbracket \otimesDay \llbracket Q^\natural\rrbracket \\ \big\downarrow{\scriptstyle\;\cong} \\ \llbracket\Delta_1\rrbracket \otimesDay \llbracket Q_1^\natural\rrbracket \otimesDay \llbracket\Delta_2\rrbracket \otimesDay \llbracket Q_2^\natural\rrbracket \\ \big\downarrow{\scriptstyle\;\eta^{\psi_1\multimap\psi_2} \otimesDay \eta^{\psi_1}} \\ \llbracket\psi_1 \multimap \psi_2\rrbracket \circ (\langle \mathcal{B}, T_1\rangle \bullet -) \otimesDay \llbracket\psi_1\rrbracket \circ (\langle \mathcal{B}, T_2\rangle \bullet -) \\ \big\downarrow{\scriptstyle\;\cong} \\ \Big(\big(\llbracket\psi_1\rrbracket \toDay \llbracket\psi_2\rrbracket\big) \otimesDay \llbracket\psi_1\rrbracket\Big) \circ \Big((\langle \mathcal{B}, T_1\rangle \bullet -) \otimesDay (\langle \mathcal{B}, T_2\rangle \bullet -)\Big) \\ \big\downarrow{\scriptstyle\;ev\circ\cong} \\ \llbracket\psi_2\rrbracket \circ (\langle \mathcal{B}, T_1\,,\,T_2\rangle \bullet -) \\ \big\downarrow{\scriptstyle\;\cong} \\ \llbracket\psi_2\rrbracket \circ (\langle \mathcal{B}, T\rangle \bullet -) \end{array}$$ Here the third step uses the fact that $\otimesDay$ is a (lax) monoidal product in $\widehat{\mathbb{W}}$.

– The last rule is: $\rhd I^\flat$. In this case, Q, T, $\Delta$ are all empty, and the assumption becomes $\emptyset \vdash_{\mathcal{B}^+} I^\flat$. The goal is to show a natural transformation $\theta : \llbracket\emptyset\rrbracket \Rightarrow \llbracket I\rrbracket(\langle \mathcal{B}, T\rangle \bullet -)$; that is, $\theta : \mathbf{よ}I \Rightarrow \big(\prod_{p\in\mathbb{A}}(\llbracket p\rrbracket \toDay \llbracket p\rrbracket)\big)(\langle \mathcal{B}, \emptyset\rangle \bullet -)$. Note that $\mathbf{よ}I = \mathbb{W}(-, \langle\emptyset, \emptyset\rangle)$, and $\mathbb{W}(\langle \mathcal{X}, U\rangle, \langle\emptyset, \emptyset\rangle)$ is nonempty precisely when $U = \emptyset$, in which case $\mathbb{W}(\langle \mathcal{X}, \emptyset\rangle, \langle\emptyset, \emptyset\rangle)$ is a singleton set, denoted $\{\ast\}$. So it suffices to define $\theta$ at $\langle \mathcal{X}, \emptyset\rangle$. We define the component at $p \in \mathbb{A}$ of $\theta_{\langle \mathcal{X}, \emptyset\rangle}(\ast)$ as the identity natural transformation Id, which is an element in $\widehat{\mathbb{W}}(\llbracket p\rrbracket, \llbracket p\rrbracket(\langle \mathcal{B} \cup \mathcal{X}, \emptyset\rangle \bullet -))$. More precisely, $Id_{\langle \mathcal{D}, S\rangle} : \llbracket p\rrbracket(\langle \mathcal{D}, S\rangle) \to \llbracket p\rrbracket(\langle \mathcal{B} \cup \mathcal{X} \cup \mathcal{D}, S\rangle)$ maps a derivation of $S \vdash_{\mathcal{D}} p$ to itself, which is also a derivation for $S \vdash_{\mathcal{B} \cup \mathcal{X} \cup \mathcal{D}} p$. The naturality is evident given the definition of the maps being the identities.

– The last rule is: $(I^\flat, p) \Rightarrow p$. Then $\Delta_1^\flat\,,\,T_1\,,\,Q_1 \vdash_{\mathcal{B}^+} I^\flat$ and $\Delta_2^\flat\,,\,T_2\,,\,Q_2 \vdash_{\mathcal{B}^+} p$. By IH, there exist natural transformations: $$\eta^{I} : \llbracket\Delta_1\rrbracket \otimesDay \llbracket Q_1^\natural\rrbracket \Rightarrow \llbracket I\rrbracket(\langle \mathcal{B}, T_1\rangle \bullet -)$$ $$\eta^{p} : \llbracket\Delta_2\rrbracket \otimesDay \llbracket Q_2^\natural\rrbracket \Rightarrow \llbracket p^\natural\rrbracket(\langle \mathcal{B}, T_2\rangle \bullet -)$$ Thus we have $\eta^{I} \otimesDay \eta^{p} : \llbracket\Delta\rrbracket \otimesDay \llbracket Q^\natural\rrbracket \Rightarrow (\llbracket I\rrbracket \otimesDay \llbracket p^\natural\rrbracket)(\langle \mathcal{B}, T\rangle \bullet -)$. Then, it suffices to define a natural deduction $\theta^{p^\natural} : \llbracket I\rrbracket \otimesDay \llbracket p^\natural\rrbracket \Rightarrow \llbracket p^\natural\rrbracket$. For this, we make an induction on $p^\natural$.

– $p^\natural$ = p. $\theta^{p} : \llbracket I\rrbracket \otimesDay \llbracket p\rrbracket \Rightarrow \llbracket p\rrbracket$ is the following composite: $$\begin{array}{c} \prod_{r\in\mathbb{A}}(\llbracket r\rrbracket \toDay \llbracket r\rrbracket) \otimesDay \llbracket p\rrbracket \\ \big\downarrow{\scriptstyle\;\pi_p \otimesDay id} \\ (\llbracket p\rrbracket \toDay \llbracket p\rrbracket) \otimesDay \llbracket p\rrbracket \\ \big\downarrow{\scriptstyle\;ev} \\ \llbracket p\rrbracket \end{array}$$

– $p^\natural$ is $\chi_1 \otimes \chi_2$. The goal is $\theta^{\chi_1\otimes\chi_2} : \llbracket I\rrbracket \otimesDay \llbracket\chi_1 \otimes \chi_2\rrbracket \Rightarrow \llbracket\chi_1 \otimes \chi_2\rrbracket$. Spelling out the definition of $\llbracket\chi_1 \otimes \chi_2\rrbracket$ in the codomain, using the UMP of products, it suffices to define its q-component $\theta^{\chi_1\otimes\chi_2}[q] : \llbracket I\rrbracket \otimesDay \llbracket\chi_1\otimes\chi_2\rrbracket \Rightarrow (\llbracket\chi_1\rrbracket \otimesDay \llbracket\chi_2\rrbracket \toDay \llbracket q\rrbracket) \toDay \llbracket q\rrbracket$, by currying the following natural transformation: $$\begin{array}{c} \llbracket I\rrbracket \otimesDay \llbracket\chi_1 \otimes \chi_2\rrbracket \otimesDay \big(\llbracket\chi_1\rrbracket \otimesDay \llbracket\chi_2\rrbracket \toDay \llbracket q\rrbracket\big) \\ \big\downarrow{\scriptstyle\;\pi_q \otimesDay \pi_q} \\ (\llbracket q\rrbracket \toDay \llbracket q\rrbracket) \otimesDay \Big(\big(\llbracket\chi_1\rrbracket \otimesDay \llbracket\chi_2\rrbracket \toDay \llbracket q\rrbracket\big) \toDay \llbracket q\rrbracket\Big) \otimesDay \big(\llbracket\chi_1\rrbracket \otimesDay \llbracket\chi_2\rrbracket \toDay \llbracket q\rrbracket\big) \\ \big\downarrow{\scriptstyle\;id \otimesDay ev} \\ (\llbracket q\rrbracket \toDay \llbracket q\rrbracket) \otimesDay \llbracket q\rrbracket \\ \big\downarrow{\scriptstyle\;ev} \\ \llbracket q\rrbracket \end{array}$$

– $p^\natural$ is I. Similar to the $\otimes$-case.

– $p^\natural$ is $\chi_1 \multimap \chi_2$. The goal is $\theta^{\chi_1\multimap\chi_2} : \llbracket I\rrbracket \otimesDay \llbracket\chi_1 \multimap \chi_2\rrbracket \Rightarrow \llbracket\chi_1 \multimap \chi_2\rrbracket$; that is, $\theta^{\chi_1\multimap\chi_2} : \llbracket I\rrbracket \otimesDay (\llbracket\chi_1\rrbracket \toDay \llbracket\chi_2\rrbracket) \Rightarrow \llbracket\chi_1\rrbracket \toDay \llbracket\chi_2\rrbracket$. This is obtained by currying the following natural transformation, using the $\theta^{\chi_2} : \llbracket I\rrbracket \otimesDay \llbracket\chi_2\rrbracket \Rightarrow \llbracket\chi_2\rrbracket$ from IH: $$\llbracket I\rrbracket \otimesDay (\llbracket\chi_1\rrbracket \toDay \llbracket\chi_2\rrbracket) \otimesDay \llbracket\chi_1\rrbracket \xrightarrow{\;id \otimesDay ev\;} \llbracket I\rrbracket \otimesDay \llbracket\chi_2\rrbracket \xrightarrow{\;\theta^{\chi_2}\;} \llbracket\chi_2\rrbracket$$ This completes the induction.

7 Conclusion

This paper has presented two sound and complete base-extension semantics (B-eS) for intuitionistic multiplicative linear logic (IMLL) and a variation of the B-eS for intuitionistic propositional logic. Our investigation builds upon work by Sandqvist [48]; particularily, we adopt the simulation approach to completeness in this work. Through a careful analysis, we identify definitional reflection (DR) as a fundamental principle underlying the B-eS of IPL. This informs the setup of the B-eS for IMLL to allow an analogous completeness proof.

A crucial insight gleaned from the B-eS of IPL is the essential role of the transmission of proof-theoretic content within B-eS. Specifically, a formula $\phi$ is supported in a base B relative to a context $\Gamma$ if, for any extension C of B, $\phi$ is supported in C whenever $\Gamma$ is supported in C . Leveraging this understanding, we extend our analysis to propose a ‘resource-sensitive’ adaptation of B-eS, aligning with the characteristics of intuitionistic multiplicative linear logic (IMLL). Three pivotal adjustments are made: rendering the notion of a base substructural, enriching the support relation to accommodate a multiset of atoms as ‘resources’, and providing a distinct treatment for the context-former and multiplicative conjunction.

This principled adaptation captures the intrinsic ‘resource reading’ of IMLL as articulated by Girard [18]. The logical constants’ clauses are derived through DR on their introduction rules, mirroring the approach taken for IPL. Furthermore, we address the intriguing question of a more intuitive semantics for the tensor, exploring the possibility of interpreting it as the combination of resources. Despite its intuitive appeal, this approach is shown to be incompatible with the standard completeness framework, prompting necessary adjustments in the completeness proof.

Beyond its contributions to IMLL, this paper marks a significant step in expanding proof-theoretic semantics (P-tS) beyond classical and intuitionistic propositional logics. The methodology proposed here serves as a blueprint for delivering B-eS for other substructural logics, including (intuitionistic) Linear Logic [18] (LL) and the logic of Bunched Implications [36] (BI). While the addition of the additive connectives of LL follows straightforwardly (see Gheorghiu et al. [13]), handling exponentials presents a challenge—see Buzoku [7]. For BI, accommodating the bunched structure of contexts and appropriately managing weakening and contraction in the additive contextformer pose significant hurdles—see Gheorghiu et al. [15].

The semantics of IMLL in this paper merits comparison with extant semantics for fragments of Linear Logic. In particular, the use of certain monoidal structure to deal with linearity is common. In [23], Hodas and Miller have given a semantics for logic programming in the hereditary Harrop formulae (hHf) fragment of intuitionistic linear logic (ILL), which employs monoid-indexed interpretations of formulae in Kripke structures. In this semantics, for example, the tensor product is interpreted as follows: $$K_{r,w} \vDash \varphi_1 \otimes \varphi_2 \;\text{ iff }\; \text{there are } r_1 \text{ and } r_2 \text{ such that } r = r_1 + r_2 \text{ and } K_{r_1,w} \vDash \varphi_1 \text{ and } K_{r_2,w} \vDash \varphi_2$$ where $r$, $r_1$, and $r_2$ are elements of a (commutative) monoid $\langle R, +, 0\rangle$ and the world w is an element of a partially ordered set $\langle W, \leq\rangle$.

Allwein and Dunn’s Kripke semantics for classical linear logic given in [2] also employs monoidal structure in similar ways to those discuss herein. Given these works, it is forseeable that certain monoidal structure is necessary to obtain a B-eS for IMLL from that for IPL, yet it is not obvious which monoidal structure to choose. In our case, the free commutative monoid over A (i.e., multisets of atoms) is integrated into the support relation to reflect the aforementioned resource reading. The relationships between these ideas also remain to be explored.

Moreover, it is interesting to explore whether such monoidal structures are canonical, in the sense that these semantics of (fragments of) linear logic could be obtained in a uniform way on top of those of (fragments of) intuitionistic and classical logic. The preceding semantics by Hodas and Miller [23] that is used as the basis for a semantics of logic programming in ILL suggests a possible connection to a line of research between base-extension semantics and logic programming: in [16], Gheorghiu and Pym have shown how the ‘least Herbrand model’ semantics of logic programming for the hereditary Harrop formulae (hHf) fragment of IPL (cf. [35]) can be used to understand Sandqvist’s base-extension semantics for IPL.

The sense in which Hodas and Miller’s semantics stands in a similar relationship to the base-extension semantics of IMLL presented here and the relationship between the least Herbrand semantics and the base-extension semantics for IPL given in [16] remains to be explored.

The development of P-tS for substructural logics is particularly valuable in the context of system verification and modelling. This approach has already demonstrated its utility in simulation modelling, as evidenced by the work of Kuorikoski and Reijula [24]. In a broader sense, the paper prompts a consideration of the conditions a logic must satisfy to lend itself to a B-eS. This exploration opens avenues for future research and underscores the potential of proof-theoretic semantics in advancing our understanding of diverse logical systems. Acknowledgements. We are grateful to Yll Buzoku, Diana Costa, Timo Eckhardt, Sonia Marin, Elaine Pimentel, Eike Ritter, and Edmund Robinson for many discussions on the P-tS for substructural logics, and to Tim Button for many discussions about the philosophical context of P-tS. We should also like to thank Timo Lang for supportive discussions on the treatment of $\otimes$ in the the revisited semantics for IMLL.

This article is a developed and expanded version of a paper presented at TABLEAUX 2023 [14].

Funding This work has been partially supported by the UK EPSRC Grants EP/S013008/1 and EP/R006865/1, and by Gheorghiu’s EPSRC Doctoral Studentship. Open Access. This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.

Publisher’s Note Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.