Skolemisation for Intuitionistic Linear Logic

Abstract

Focusing is a known technique for reducing the number of proofs while preserving derivability. Skolemisation is another technique designed to improve proof search, which reduces the number of back-tracking steps by representing dependencies on the term level and instantiate witness terms during unification at the axioms or fail with an occurs-check otherwise. Skolemisation for classical logic is well understood, but a practical skolemisation procedure for focused intuitionistic linear logic has been elusive so far. In this paper we present a focused variant of first-order intuitionistic linear logic together with a sound and complete skolemisation procedure.

1 Introduction

Modern proof search paradigms are built on variants of focused logics first introduced by Andreoli [1]. Focused logics eliminate sources of non-determinism while preserving derivability. In this paper we consider the focused logic LJF [2]. By categorising the logical connectives according to the invertibility of its left or right rules, we obtain a so-called polarised logic [2]. For example, the $\forall$-right rule is invertible, making $\forall$ a negative (or asynchronous) connective, and the $\exists$-left rule is invertible, making $\exists$ a positive (or synchronous) connective.

But even a focused proof system does not eliminate all non-determinism. There is still residual non-determinism in-between focusing steps. It is well known that we can control this non-determinism using different search strategies, such as forcing backward-chaining and forward-chaining using the atom polarity. Another remaining source of non-determinism comes from the order of quantifier openings, as choosing the wrong order may lead to additional back-tracking.

For example, consider the following judgment in multiplicative linear logic:

$$\begin{aligned} \forall x. A(x) {-\!\!\circ }B(x), \forall y. \exists u.A(u) \vdash \exists z. B(z) \end{aligned}$$

Variables u introduced by the well-known rules $\exists L^u$ and $\forall R^u$ (and written next to the rule name) are fresh and called Eigen-variables, which we can use to construct witness terms for the universal variables on the left or the existential variables on the right. Because quantifier rules do not permute freely with other rules, one needs to resolve quantifiers in a particular order, or otherwise risk an exponential blow-up in the proof search. This fact has already been observed by Shankar [8] for LJ, who proposed to capture the necessary dependencies using Skolem functions to encode the permutation properties of LJ inference rules, guaranteeing reconstruction of LJ proofs from their skolemised counterparts.

However, naïve Skolemisation is unsound in linear logic. As first noted by Lincoln [3], the sequent

$$\begin{aligned} \forall x. A \mathbin {\otimes }B(x) \vdash A \mathbin {\otimes }\forall u. B(u) \end{aligned}$$

does not admit a derivation in linear logic, but its naïve skolemisation does: $A \mathbin {\otimes }B(x) \vdash A \mathbin {\otimes }B(u())$, where x denotes an existential and u() a universal variable that must not depend on x. Introducing replication creates a similar problem, where the following sequent does not admit a derivation:

$$\begin{aligned} \forall x. !A(x) \vdash !\forall u. A(u) \end{aligned}$$

however again its naïve skolemisation loses the relative order between quantifier openings and replication, thus admitting a proof: $!A(x) \vdash !A(u())$.

In this paper we show that the ideas of skolemisation for classical logic and intuitionistic logic for LJ [8] carry over quite naturally to focused intuitionistic linear logics (LJF) [2]. We propose a quantifier-free version of LJF that encodes the necessary constraints called skolemised intuitionistic linear logic (SLJF). Our main contribution is to define a skolemisation procedure from LJF to SLJF that we show to be both sound and complete: any derivation in LJF is provable in SLJF after skolemisation and, vice versa, any derivation in SLJF of a skolemised formula allows to reconstruct a proof of the original formula. Hence we eliminate back-tracking points introduced by first-order quantifiers. We do not eliminate any back-tracking points introduced by propositional formulae.

The paper proceeds as follows: Sect. 2 introduces focused intuitionistic linear logic (LJF), Sect. 3 presents skolemised focused intuitionistic linear logic (SLJF), Sect. 4 presents a novel skolemisation procedure, Sect. 5 presents soundness and completeness results, and Sect. 6 presents our conclusion and related work.

Contributions: This work is to our knowledge the first work that successfully defines skolemisation for a variant of linear logic. The benefit is that during proof search any back-tracking caused by resolving quantifiers in the wrong order is eliminated and replaced by an admissibility check on the axioms.

2 Focused Intuitionistic Linear Logic

We consider the focused and polarised formulation of linear logic LJF [2] that we now present. The syntactic categories are defined as usual: we write u, v for Eigen-variables and x, y for existential variables that may be instantiated by other terms, finally N for negative formulas and P for positive formulas. We also distinguish between negative and positive atoms, written as $A^-$ and $A^+$. We write $\uparrow$ to embed a positive formula into a negative, and $\downarrow$ for the inverse. The rest of the connectives should be self-explanatory.

$$ \begin{array}{lrcl} \text{ Atom } &{} A,B &{}\mathrel {::=}&{} q(t_1 \dots t_n) \\ \text{ Negative } \text{ formula } &{}N&{} \mathrel {::=}&{} A^- \mid P {-\!\!\circ }N \mid \forall x. N \mid \uparrow P \\ \text{ Positive } \text{ formula } &{}P&{} \mathrel {::=}&{} A^+ \mid P_1 \mathbin {\otimes }P_2 \mid !N \mid \exists x. P \mid \downarrow N \\ \end{array} $$

We use the standard two-zone notation for judgments with unrestricted context $\Gamma$ and linear context $\Delta$: we write $\Gamma ; \Delta \vdash N$ for the judgment, where at most one formula $[N] \in \Delta$ or $N=[P]$ can be in focus. All formulas in $\Gamma$ are negative and all other formulas in $\Delta$ are positive. When $[N] \in \Delta$ we say that we focus on the left, whereas when $N=[P]$ we focus on the right, and we are in an inversion phase when no formula is in focus. To improve readability, we omit the leading $\cdot ;$ when the unrestricted context is empty. The rules defining LJF [2] are depicted in Fig. 1. We comment on a few interesting aspects of this logic. There are two axiom rules ${\text{ ax }}^-$ and ${\text{ ax }}^+$ where, intuitively, ${\text{ ax }}^-$ triggers backwards-chaining, and ${\text{ ax }}^+$ forward-chaining [6]. Hence we can assign polarities to atoms to select a particular proof search strategy. Once we focus on a formula, the focus is preserved until a formula with opposite polarity is encountered, in which case the focus is lost or blurred. After blurring, we enter a maximal inversion phase, where all rules without focus are applied bottom-up until no more invertible rules are applicable. The next focusing phase then commences.

Focusing is both sound and complete. i.e. every derivation (written as $\Gamma ;\Delta \vdash _{\tiny \text{ ILL }}F$) can be focused and every focused derivation can be embedded into plain linear logic [2]. In particular, in our own proofs in Sect. 5, we make use of the soundness of focusing.

Theorem 1

(Focusing). If $\Gamma ; \Delta \vdash _{\tiny \text{ ILL }}F$ and $\Gamma '$, $\Delta '$ and $F'$ are the result of polarising $\Gamma$, $\Delta$ and F respectively by inserting $\uparrow$ and $\downarrow$ appropriately, then $\Gamma '; \Delta ' \vdash F'$ in focused linear logic [2].

We now present three examples of possible derivations of sequents in LJF. We will use these examples to illustrate key aspects of our proposed skolemisation.

Fig. 1.

Focused intuitionistic linear logic (LJF)

Example 1

Consider the motivating formula from the introduction that we would like to derive in LJF, assuming that the term algebra has a term $t_0$.

$$ \downarrow (\forall x. (\downarrow {A(x)}^-) {-\!\!\circ }{B(x)}^-), \downarrow (\forall x. \uparrow \exists u.\downarrow {A(u)}^-) \vdash \uparrow (\exists x. \downarrow {B(x)}^-) $$

All formulas are embedded formulas, which means that there is a non-deterministic choice to be made, namely on which formula to focus next. As this example shows, it is quite important to pick the correct formula, otherwise proof search will get stuck and back-tracking is required. This observation also holds if we determine the instantiation of universal quantifiers on the left and existential quantifiers on the right by unification instead of choosing suitable terms when applying the $\forall L$ or $\exists R$ rule.

Focusing on the first assumption before the second will not yield a proof. The Eigen-variable that eventually is introduced by the nested existential quantifier inside the second assumption is needed to instantiate the universal quantifier in the first assumption. If we start by focusing on the first assumption then none of the subsequent proof states is provable, as the following two proof states $(\downarrow {A(t_0)}^-) {-\!\!\circ }{B(t_0)}^-, {A(t_1)}^- \vdash {B(t_0)}^-$ and $(\downarrow {A(t_0)}^-) {-\!\!\circ }{B(t_0)}^-, {A(t_1)}^- \vdash {B(t_1)}^-$ demonstrate. Back-tracking becomes inevitable.

To construct a valid proof we must hence focus on the second assumption before considering the first. The result is a unique and complete proof tree that is depicted in Fig. 2.    $\square$

Fig. 2.

Example 1, unique and complete proof

Example 2

Consider the sequent $\downarrow (\forall x. \uparrow (\downarrow {A}^- \mathbin {\otimes }\downarrow {B}^-(x))) \vdash \uparrow (\downarrow {A}^- \mathbin {\otimes }\downarrow \forall u. {B}^-(u))$. This sequent is not derivable in LJF: note that $\forall L$ needs to be above the $\forall R$ rule, but this step requires that $\mathbin {\otimes }R$ is applied first. However, to apply $\mathbin {\otimes }R$, we would need to have applied $\mathbin {\otimes }L$ first, which requires that $\forall L$ is applied first. This cyclic dependency cannot be resolved.    $\square$

Example 3

Consider the sequent $\downarrow \forall x. \uparrow ! {A}^- (x) \vdash \uparrow ! \forall u. {A}^-(u)$. This sequent is not derivable in LJF either: note that the $\forall L$-rule needs to be above the $\forall R$ rule, but this step requires the !R rule to be applied first. However, to apply the !R rule we would need to apply the $\forall L$ rule first to ensure that the linear context is empty when we apply the !R rule. This is another cyclic dependency.    $\square$

Focusing removes sources of non-determinism from the propositional layer, but not from quantifier instantiation. In the next section we present a quantifier-free skolemised logic, SLJF, where quantifier dependencies are represented through skolemised terms. This way, proof search no longer needs to back-track on first-order variables, as the constraints capture all dependencies. Instead, unification at the axioms will check if the proof is admissible.

3 Skolemised Focused Intuitionistic Linear Logic

We begin now with the definition of a skolemised, focused, and polarised intuitionistic linear logic (SLJF), with the following syntactic categories:

$$ \begin{array}{lrcl} \text{ Atom } &{} A,B &{}\mathrel {::=}&{} q(t_1 \dots t_n) \\ \text{ Negative } \text{ formula } &{} N &{}\mathrel {::=}&{} {A}^-_\Phi \mid P {-\!\!\circ }N \mid \uparrow P \\ \text{ Positive } \text{ formula } &{} P &{}\mathrel {::=}&{} {A}^+_\Phi \mid P \mathbin {\otimes }P \mid !_{(a;\Phi ; \sigma )} N \mid \downarrow N \\[1ex] \text{ Variable } &{} v &{} \mathrel {::=}&{} x \mid u \mid a \\ \text{ Term } &{} t &{} \mathrel {::=}&{} v \mid f(t) \mid (t, \ldots , t)\\ \text{ Variable } \text{ context } &{} \Phi &{}\mathrel {::=}&{} \cdot \mid \Phi , v\\ \text{ Modal } \text{ context } &{} \Gamma &{}\mathrel {::=}&{} \cdot \mid \Gamma , (a;\Phi ; \sigma ):N \\ \text{ Linear } \text{ context } &{} \Delta &{}\mathrel {::=}&{} \cdot \mid \Delta , P \\[1ex] \text{ Parallel } \text{ substitution } &{} \sigma &{}\mathrel {::=}&{} \cdot \mid \sigma , t/x \mid \sigma , u(t)/u \mid \sigma , t/a \end{array} $$

Following the definition of LJF, we distinguish between positive and negative formulas and atoms. Backward and forward-chaining strategies are supported in SLJF, as well.

SLJF does not define any quantifiers as they are removed by skolemisation (see Sect. 4). Yet, dependencies need to be captured in some way. Quantifier rules for $\forall R^u$ and $\exists L^u$ introduce Eigen-variables written as u. Quantifier rules for $\forall L$ and $\exists R$ introduce existential variables, which we denote with x. And finally other rules, such as $\mathbin {\otimes }R$, ${-\!\!\circ }L$, and !R are annotated with special variables a capturing the dependencies between rules that do not freely commute. These special variables are crucial during unification at the axiom level to check that the current derivation is admissible.

The semantics of the bang connective ! in SLJF is more involved than in LJF because we have to keep track of the variables capturing dependencies and form closures: One way to define the judgmental reconstruction of the exponential fragment of SLJF is to introduce a validity judgment $(a;\Phi ;\sigma ) : N$, read as N is valid in world $(a;\Phi ;\sigma )$, which leads to a generalised, modal $\Gamma$ that no longer simply contains negative formulas N, but also closures of additional judgmental information. The special variable a is the “name” of the world in which $N\sigma$ is valid, where all possible dependencies are summarised by $\Phi$. $\Phi$ consists of variables, where we assume tacit variable renaming to ensure that no variable name occurs twice. We write $\llcorner {\Phi }\lrcorner$ for all existential and special variables declared in $\Phi$. In contrast to LJF, atomic propositions $A^-_\Phi$ and $A^+_\Phi$ are indexed by $\Phi$ capturing all potential dependencies, which we will inspect in detail in Definition 2 where we define admissibility, the central definition of this paper, resolving the non-determinism related to the order in which quantifier rules are applied. The linear context remains unchanged.

Terms t are constructed from variables (existential, universal, and special) and function symbols f that are declared in a global signature $\Sigma \mathrel {::=}\cdot \mid \Sigma , f$. Well-built terms are characterised by the judgment $\Phi \vdash t$. Substitutions constructed by unification and communicated through proof search capture the constraints on the order of application of proof rules, which guarantee that a proof in SLJF gives rise to a proof in LJF. Their definition is straightforward, and the typing rules for substitutions are depicted in Fig. 3. For a substitution $\sigma$ such that $\sigma :\Phi \rightarrow \Phi '$, we define the domain of $\sigma$ to be $\Phi$ and the co-domain of $\sigma$ to be $\Phi '$. For any context $\Phi$ and substitution $\sigma$ with co-domain $\Psi$ we write $\sigma _{\uparrow \Phi }$ for the substitution $\sigma$ restricted to $\Phi \cap \Psi$, i.e. $v\sigma _{\uparrow \Phi }$ is defined iff $v \in \Phi \cap \Psi$, and $v\sigma _{\uparrow \Phi } = v\sigma$ in this case. We write $\sigma \setminus \Phi$ for the substitution $\sigma$ restricted to $\Psi \setminus \Phi$, i.e. $v\sigma \setminus \Phi$ is defined iff $v \in \Psi \setminus \Phi$, and $v\sigma \setminus \Phi = v\sigma$ in this case. For any substitution $\sigma$ we define the substitution $\sigma ^n$ by induction over n to be $\sigma ^1 = \sigma$, and $v\sigma ^{n+1} = (v\sigma ^n)\sigma$.

Fig. 3.

Typing rules for substitutions

Definition 1

(Free Variables). We define the free variables of a skolemised formula K, written $\mathop {FV}(K)$ by induction over the structure of formulae by

$$\begin{array}{rcl} \mathop {FV}({A}^-_{\Phi }) &{}=&{} \mathop {FV}({A}^+_{\Phi }) = \Phi \\ \mathop {FV}(P_1 \mathbin {\otimes }P_2) &{}=&{} \mathop {FV}(P_1) \cup \mathop {FV}(P_2) \\ \mathop {FV}(P {-\!\!\circ }N) &{}=&{} \mathop {FV}(P) \cup \mathop {FV}(N) \\ \mathop {FV}(!_{(a;\Phi ; \sigma )}N) &{}=&{} \Phi \\ \end{array}$$

Now we turn to the definition of admissibility, which checks whether the constraints on the order of $\forall L$-and $\exists R$-rules (which instantiate quantifiers) and application of non-invertible propositional rules can be satisfied when re-constructing a LJF-derivation from an SLJF-derivation.

Definition 2

(Admissibility). We say $\sigma$ is admissible for $\Phi$ if firstly for all existential and special variables v and for all n, v does not occur in $v\sigma ^n$, and secondly for all special variables $a_L$ and $a_R$ respectively and for all n, if $x\sigma ^n$ contains a variable $a_L$ or $a_R$ for any x in the co-domain of $\sigma$, then the variable $a_R$ or $a_L$ respectively does not occur in $\Phi$.

The first condition in the definition of admissibility ensures that there are no cycles in the dependencies of $\forall L$-and $\exists R$-rules and non-invertible propositional rules. The second condition ensures that for each rule with two premises any Eigen-variable which is introduced in one branch is not used in the other branch. Examples of how this definition captures dependency constraints are given below.

Next, we define derivability in SLJF. The derivability judgment uses a substitution which captures the dependencies between $\forall L$-and $\exists R$-rules and non-invertible propositional rules.

Definition 3

(Proof Theory). Let $\Phi$ be a context of variables, $\Gamma$ the modal context (which refined the notion of unrestricted context from earlier in this paper), $\Delta$ the linear context, P a positive and N a negative formula, and $\sigma$ a substitution. We define two mutually dependent judgments $\Gamma ;\Delta \vdash N;\sigma$ and $\Gamma ;\Delta \vdash [P];\sigma$ to characterise derivability in SLJF. The rules defining these judgments are depicted in Fig. 4.

The !R-rule introduces additional substitutions which capture the dependency of the !R-rule on the $\forall L$-and $\exists R$-rules which instantiate the free variables in the judgment. An example of this rule is given below. The copy-rule performs a renaming of all the bound variables in N.

Fig. 4.

Skolemised intuitionistic linear logic

Example 4

We give a derivation of the translation of the judgment of Example 1 in skolemised intuitionistic linear logic. We omit the modal context $\Gamma = \cdot$. Furthermore, let the goal of proof search be the following judgment:

$$\begin{array}{l} \cdot ; \uparrow ( \downarrow A(x_1)^-_{(x_1, a_L)}) {-\!\!\circ }B(x_1)^-_{( x_1, a_R)}, \uparrow A(u)^-_{(x_2,u)} \vdash B(x_3)^-_{(x_3)}; \sigma \end{array} $$

where $\sigma$ must contain the substitution $u(x_2)/u$, which arises from skolemisation.

We observe that only focusing rules are applicable. Focusing on A will not succeed, since A was assumed to be a negative connective, so we focus on the right. Recall, that we will not be able to remove the non-determinism introduced on the propositional level. We obtain the derivation in Fig. 5, where $\sigma = \cdot , u/x_1, x_1/x_3, u(x_2)/u$. This derivation holds because $\sigma$ is admissible for $x_1, a_L, x_2$ and $x_1, a_R, x_3$. The constraint that the variable $x_2$ can be instantiated only after the $\forall R$-rule for u has been applied is captured by the substitution $u(x_2)/u$.

Fig. 5.

Example 4, unique complete proof

Example 5

Next, consider the sequent $\downarrow (\forall x. \uparrow (\downarrow {A}^- \mathbin {\otimes }\downarrow {B}^-{x})) \vdash \uparrow (\downarrow {A}^- \mathbin {\otimes }\downarrow \forall u.{B}^-(u))$ from Example 2. To learn if this sequent is provable, we translate it into $\downarrow {A}^-_x \mathbin {\otimes }\downarrow {B(x)}^-_x \vdash \uparrow (\downarrow A_{a_L} \mathbin {\otimes }\downarrow {B(u)}^-_{a_R;u})$. The only possible proof yields an axiom derivation $[{B}^-_{x}] \vdash {B}^-_{a_R;u}; \cdot , u(a_R)/x$ , which is not valid, as $\cdot , u/x, u(a_R)/u$ is not admissible for $x,a_L$. More precisely, the second condition of admissibility is violated.    $\square$

Example 6

Now, consider the sequent $\downarrow \forall x. \uparrow ! {A}^- (x) \vdash \uparrow ! \forall u. {A}^-(u)$ from Example 3. The skolemised sequent is $!_{(a;x;\cdot )}{A_{a,x}}^- \vdash \uparrow !_{(b;u;u(b)/u)} {A}^-(u)_{u,b})$. The only possible derivation produces the substitution $\cdot , u/x, x/b, u(b)/u$, which is not admissible for $\cdot , x, u, b, a$. More precisely, the first condition of admissibility is violated for the variable b. This expresses the fact that in any possible LJF-derivation the instantiation of x has to happen before the !R-rule and the !R -rule has to be applied before the instantiation of x, which is impossible.

4 Skolemisation

To skolemise first-order formulas in classical logic, we usually compute prenex normal forms of all formulas that occur in a sequent, where we replace all quantifiers that bind “existential” variables by Skolem constants. This idea can also be extended to intuitionistic logic [8]. This paper is to our knowledge the first to demonstrate that skolemisation can also be defined for focused, polarised, intuitionistic, first-order linear logic, as well. In this section, we show how.

Skolemisation transforms an LJF formula F (positive or negative) closed under $\Phi$ into an SLJF formula K and a substitution, which collects all variables introduced during skolemisation. Formally, we define two mutual judgments: $sk_L(\Phi ,F) = (K; \sigma )$ and $sk_R(\Phi ,F) = (K; \sigma )$. K is agnostic to polarity information, hence we prepend appropriate $\uparrow$ and $\downarrow$ connectives to convert K to the appropriate polarity by the conversion operations $\mathop {pos}(\cdot )$ and $\mathop {neg}(\cdot )$, depicted in Fig. 6. Alternatively, we could have chosen to distinguish positive and negative Ks syntactically, but this would have unnecessarily cluttered the presentation and left unnecessary backtrack points because of spurious $\uparrow \downarrow$ and $\downarrow \uparrow$ conversions.

Fig. 6.

Polarity adjustments

We return to the definition of skolemisation, depicted in Fig. 7. The main idea behind skolemisation is to record dependencies of quantifier rules as explicit substitutions. More precisely, if an Eigen-variable u depends on an existential variable x, a substitution u(x)/u is added during skolemisation. We do not extend the scope of an Eigen-variable beyond the !-operator as we have to distinguish between an Eigen-variable for which a new instance must be created by the copy-rule and one where the same instance may be retained.

Explicit substitutions model constraints on the order of quantifiers. The satisfiability of the constraints is checked during unification at the leaves via the admissibility condition (see Definition 2) which the substitution has to satisfy. Potential back-track points are marked by special variables a, which are associated with the ! connective. These annotations need to store enough information so that the set of constraints can be appropriately updated when copying a formula from the modal context into the linear context.

In our representation, any proof of the skolemised formula in SLJF captures an equivalence class of proofs under different quantifier orderings in LJF. Only those derivations where substitutions are admissible, i.e. do not give rise to cycles like u(x)/x or introduce undue dependencies between the left and right branches of a $\mathbin {\otimes }$ or ${-\!\!\circ }$, imply the existence of a proof in LJF.

The judgments can be easily extended to the case of contexts $\Gamma$ and $\Delta$ for which we write $sk_L(\Phi ;\Gamma )$ and $sk_L(\Phi ;\Delta )$. Note that tacit variable renaming is in order, to make sure that no spurious cycles are accidentally introduced in the partial order defined by the constraints.

Example 7

We return to Example 1 and simply present the skolemisation of the three formulas that define the judgment:

$$ \downarrow (\forall x. (\downarrow A(x)) {-\!\!\circ }B(x)), \downarrow (\forall x. \uparrow \exists u.\downarrow A(u)) \vdash \uparrow (\exists x. \downarrow B(x)) $$

First, we skolemise each of the formulas individually.

$$\begin{aligned} \text{ sk}_L({\cdot };{\downarrow (\forall x. (\downarrow A(x)) {-\!\!\circ }B(x))}) = & {} ( \downarrow A(x)_{( x, a_L)}) {-\!\!\circ }B(x)_{( x, a_R)}; \cdot \\ \text{ sk}_L({\cdot };{\downarrow (\forall x. \uparrow \exists u.\downarrow A(u))}) = & {} A(u)_{(x,u)} ; u(x)/u \\ \text{ sk}_R({\cdot };{\uparrow (\exists x. \downarrow B(x))}) = & {} B(x)_{(x)}; \cdot \end{aligned}$$

Second, we assemble the results into a judgment in SLJF, which then looks as follows. To this end, we $\alpha$-convert the variables,

$$\begin{array}{l} ( \downarrow A(x_1)_{(x_1, a_L)}) {-\!\!\circ }B(x_1)_{( x_1, a_R)}, A(u)_{(x_2,u)} \vdash B(x_3)_{(x_3)}; u(x_2)/u \end{array} $$

The attentive reader might have noticed that we already gave a proof of this judgment in the previous section in Example 1, after turning the first two formulas positive, because they constitute the linear context.

5 Meta Theory

We begin now with the presentation of the soundness result (see Sect. 5.1) and the completeness result (see Sect. 5.2). Together they imply that skolemisation preserves provability. These theorems also imply that proof search in SLJF will be more efficient than in LJF since it avoids quantifier level back-tracking. Proof search in skolemised form will not miss any solutions.

Fig. 7.

Skolemisation

5.1 Soundness

For the soundness direction, we show that any valid derivation in LJF can be translated into a valid derivation in SLJF after skolemisation.

Lemma 1

(Weakening).

• (i) Assume $\Gamma ; \Delta \vdash K;\sigma$ Then also $\Gamma , (a;\Phi ; \sigma ') :N; \Delta \vdash K;\sigma$.

• (ii) Assume $\Gamma ; \Delta \vdash [K];\sigma$ Then also $\Gamma , (a;\Phi ; \sigma ') :N; \Delta \vdash [K];\sigma$.

• (iii) Assume $\Gamma ; \Delta , [K'] \vdash K;\sigma$ Then also $\Gamma , (a;\Phi ; \sigma ') :N; \Delta , [K'] \vdash K;\sigma$.

Proof

The proof is a simple induction over derivation in all three cases.

Next, we prove three admissibility properties for $\mathbin {\otimes }$R, ${-\!\!\circ }$L, and copy, respectively, that we will invoke from within the proof of the soundness theorem. In the interest of space, we provide a proof only for the first of the three lemmas.

Lemma 2

(Admissibility of $\mathbin {\otimes }$R). Assume $\Gamma ; \Delta _1 \vdash \mathop {neg}(K_1); \sigma$ and $\Gamma ; \Delta _2 \vdash \mathop {neg}(K_2);\sigma$ with proofs of height at most n such that the first application of the focus-rule is the focus R-rule. Then also $\Gamma ; \Delta _1 ,\Delta _2 \vdash \mathop {neg}(\mathop {pos}(K_1) \mathbin {\otimes }\mathop {pos}(K_2)); \sigma$.

Proof

We prove this property by induction over n. There are several cases. Firstly, assume that there is any positive formula in $\Delta _1$ or $\Delta _2$ which is not an atom. Again, there are several cases. We start by assuming $\Delta _1 = K_1' \mathbin {\otimes }K_2', \Delta _1'$ and the derivation is

Hence by induction hypothesis we have $\Gamma ; K_1', K_2', \Delta _1', \Delta _2 \vdash \mathop {neg}(\mathop {pos}(K_1) \mathbin {\otimes }\mathop {pos}(K_2)); \sigma$ and hence also $\Gamma ; K_1' \mathbin {\otimes }K_2', \Delta _1', \Delta _2 \vdash \mathop {neg}(\mathop {pos}(K_1) \mathbin {\otimes }\mathop {pos}(K_2)); \sigma \; .$ Now assume that $\Delta _1 = !_{(a;\Phi ; \sigma ')}N, \Delta _1'$ and the derivation is

By Lemma 1, we also have $\Gamma , (a;\Phi ; \sigma ') :N; \Delta _2 \vdash \mathop {neg}(K_2);\sigma$. By induction hypothesis we have $\Gamma , (a;\Phi ; \sigma ') :N; \Delta _1', \Delta _2 \vdash \mathop {neg}(\mathop {pos}(K_1) \mathbin {\otimes }\mathop {pos}(K_2)); \sigma$ and hence also $\Gamma ; !_{(a;\Phi ; \sigma ')}N, \Delta _1', \Delta _2 \vdash \mathop {neg}(\mathop {pos}(K_1) \mathbin {\otimes }\mathop {pos}(K_2)); \sigma .$

Secondly, assume that $K_1= N_1$, where $N_1$ is a negative formula and $K_2= P_2$, where $P_2$ is a positive formula. By assumption there is a derivation

There is also a derivation

Hence we also have the following derivation:

By assumption we obtain $\Gamma ; \Delta _1, \Delta _2 \vdash \uparrow (\downarrow N_1 \mathbin {\otimes }P_2); \sigma$. All other cases of $K_1$ and $K_2$ being positive or negative are similar.

Lemma 3

(Admissibility of ${-\!\!\circ }$L). Assume

$$\Gamma ; \Delta _1 \vdash \mathop {neg}(K_1); \sigma \;\; \text{ and } \;\;\Gamma ; \Delta _2, \mathop {pos}(K_2) \vdash K;\sigma $$

with proofs of height at most n such that the first application of the focus-rule is the focus L-rule for $K_1$. and the focus R-rule for $K_2$. Then also

$$\Gamma ; \Delta _1 ,\Delta _2 , \mathop {neg}(\mathop {pos}(K_1) {-\!\!\circ }\mathop {pos}(K_2))\vdash K ; \sigma $$

Proof

Similar to the proof of Lemma 2.    $\square$

Lemma 4

(Admissibility of copy). Assume

$$\Gamma , (a;\Phi ; \sigma '):N; \mathop {pos}(N\{\vec {v}'/\vec {v}\}), \Delta \vdash \mathop {neg}(K); \sigma , \sigma '\{\vec {v}'/\vec {v}\}$$

with a proof of height at most n such that the first application of the focus-rule is the focus L-rule applied to $\mathop {pos}(N\{\vec {v}'/\vec {v}\})$. Then also $\Gamma , (a;\Phi ; \sigma '):N; \Delta \vdash \mathop {neg}(K) ; \sigma$.

Proof

Similar to the proof of Lemma 2.    $\square$

Theorem 2

(Soundness). Let $\Phi$ be a context which contains all the free variables of $\Gamma$, $\Delta$ and F. Let $\sigma :\Phi \rightarrow \Phi$ be a substitution. Assume $\Gamma \sigma _{\uparrow \llcorner {\Phi }\lrcorner }; \Delta \sigma _{\uparrow \llcorner {\Phi }\lrcorner } \vdash F\sigma _{\uparrow \llcorner {\Phi }\lrcorner }$ in focused intuitionistic linear logic. Let $sk_L(\Phi ; \Gamma ) = \Gamma '; \sigma _{\Gamma '}$, $sk_L(\Phi ;\Delta ) = \Delta '; \sigma _{\Delta '}$ and $sk_R(\Phi ; F)= K; \sigma _K$. Let $\tau = \sigma _{\Gamma '}, \sigma _{\Delta '}, \sigma _K$. Let $\Phi ' = (FV(\Gamma ') \cup FV(\Delta ') \cup FV(\Phi _F)) \setminus \Phi$. Assume that $\sigma$ does not contain any bound variables of $\Gamma$, $\Gamma '$, $\Delta$, $\Delta '$, F or K. Moreover, assume whenever $\Phi$ contains a variable $a_L$ or $a_R$, then the corresponding variable $a_R$ or $a_L$ respectively does not occur in $\Phi$. Then there exists a substitution $\sigma ' :\Phi , \Phi ' \rightarrow \Phi '$ such that

$$ \mathop {neg}(\Gamma '); \Delta ' \vdash K;\sigma , \tau ,\sigma '\; . $$

Proof

Induction over the derivation of $\Gamma \sigma _{\uparrow \llcorner {\Phi }\lrcorner }; \Delta \sigma _{\uparrow \llcorner {\Phi }\lrcorner } \vdash F\sigma _{\uparrow \llcorner {\Phi }\lrcorner }$. The axiom case follows from the definition of admissibility, $\mathbin {\otimes }$R follows from Lemma 2, and ${-\!\!\circ }$L from Lemma 3. Now we consider the case of $\forall$L. By definition, $\text{ sk}_L({\Phi };{\forall x.F}) = \text{ sk}_L({(x, \Phi )};{F})$. Moreover, t contains only variables in $\Phi$. Hence we can apply the induction hypothesis with replacing $\Phi$ by $\Phi , x$. The next case is $\forall$R. Consider any formula $\forall u.F$. Skolemisation introduces another Eigen-variable u. Hence we can apply the induction hypothesis with replacing $\Phi$ by $\Phi , u$. The case for copy is a direct consequence of Lemma 4. All other cases are immediate.   $\square$

5.2 Completeness

We now prove the completeness direction of skolemisation, which means that we can turn a proof in SLJF directly into a proof in LJF, by inserting at appropriate places quantifier rules, as captured by the constraints. We introduce an order relation to capture constraints on the order of rules in the proof.

Definition 4

For any substitution $\sigma$, define an order < by $x < u$ or $x < a$ if a or u occur in $x\sigma$, and $u < x$ or $u < a$ if the variable x or a occurs in $u(z_1, \ldots , z_n)$.

Lemma 5

(Strengthening).

• (i) Assume $\Gamma , (a';\Phi ; \sigma '):K; \Delta _1 \vdash K'; \sigma$ and there exists a free variable x in K such that $a_R$ occurs in $x\sigma$. Moreover assume that $a_L$ occurs in every axiom of $K'$. Then also $\Gamma ; \Delta _1 \vdash K' \sigma$.

• (ii) Assume $\Gamma , (a';\Phi ; \sigma '):K; \Delta _2 \vdash K'; \sigma$ and there exists a free variable x in K such that $a_L$ occurs in $x\sigma$. Then also $\Gamma ; \Delta _2 \vdash K'; \sigma$.

Proof

(i) If the copy-rule for K is applied during the derivation, the linear context contains the free variable x such that $a_R$ occurs in $x\sigma$. As $a_L$ occurs in all atoms of $K'$, the variable x must not occur in any of the linear formulae in the axioms in the derivation of $\Gamma , (a';\Phi ; \sigma '):K; \Delta _1 \vdash K'; \sigma$ because of the admissibility condition. Hence no subformula of K can occur in the linear formulae in the axioms in this derivation either. Hence there is also a derivation of $\Gamma ; \Delta _1 \vdash K'; \sigma$, which does not involve K. (ii) A similar argument applies.    $\square$

Lemma 6

Assume $\Gamma ; \Delta _1, \Delta _2 \vdash \uparrow (K_1 \mathbin {\otimes }K_2);\sigma$. Furthermore assume that each formula K in $\Delta _1$ and $\Delta _2$ is either a formula $\downarrow K'$, or there exists a free existential variable x in K such that $a_L$ or $a_R$ occurs in $x\sigma$, where $a_L$ and $a_R$ are the special variables introduced by the skolemisation of $K_1 \mathbin {\otimes }K_2$. Moreover assume that the first focusing rule applied is the focus R-rule. Then $\Gamma ; \Delta _1 \vdash K_1; \sigma$ and $\Gamma ; \Delta _2 \vdash K_2; \sigma$.

Proof

We use an induction over the structure of $\Delta _1$ and $\Delta _2$. Firstly, consider the case $\Gamma ; K_1' \mathbin {\otimes }K_2', \Delta _1, \Delta _2 \vdash \uparrow (K_1 \mathbin {\otimes }K_2);\sigma$. We have a derivation

By induction hypothesis we have $\Gamma ; \Delta _1'; \vdash K_1; \sigma$ and $\Gamma ; \Delta _2' \vdash K_2; \sigma$. Assume $a_L$ occurs in $x\sigma$. Because $\sigma$ is admissible for $\Gamma ; \Delta _2'$, $K_1'$ and $K_2'$ must be part of $\Delta _1'$. Hence $\Delta _1' = K_1', K_2', \Delta _1$ and $\Delta _2' = \Delta _2$. An application of the $\mathbin {\otimes }L$-rule now produces $\Gamma ; K_1' \mathbin {\otimes }K_2', \Delta _1; \vdash K_1; \sigma$.

Next we consider the case $\Gamma ; !_{(a'\Phi ; \sigma ')}K, \Delta _1, \Delta _2 \vdash \uparrow (K_1 \mathbin {\otimes }K_2); \sigma$. Assume without loss of generality $a_R$ occurs in $x\sigma$. We have a derivation

By induction hypothesis we have $\Gamma , (a';\Phi ; \sigma '):K; \Delta _1; \vdash K_1; \sigma$ and $\Gamma , (a';\Phi ; \sigma '):K; \Delta _2 \vdash K_2; \sigma$. An application of the !L-rule yields $\Gamma ; !_{(a';\Phi ; \sigma ')}K, \Delta _1; \vdash K_1; \sigma$ and Lemma 5 yields $\Gamma ; \Delta _2 \vdash K_2; \sigma$.    $\square$

Lemma 7

Assume $\Gamma ; \Delta _1, \Delta _2, \downarrow (K_1 {-\!\!\circ }K_2)\vdash K; \sigma$. Furthermore assume that each formula $K'$ in $\Delta _1$, $\Delta _2$ and K is either a formula $\downarrow K''$, or there exists a free existential variable x in $K'$ such that $a_L$ or $a_R$ occurs in $x\sigma$. Moreover assume that the first focusing rule applied is the focus L-rule for $K_1 {-\!\!\circ }K_2$. Then $\Gamma ; \Delta _1 \vdash K_1; \sigma$ and $\Gamma ; \Delta _2, K_2 \vdash K; \sigma$.

Proof

Similar to the proof of Lemma 6.    $\square$

Lemma 8

Assume $\Gamma ; \Delta \vdash \downarrow !_{(a, \phi ; \sigma ')} K; \sigma$ and the first occurrence of the focus-rule is the focus R-rule followed by !R with $\Gamma '$ containing the side formulae. Let x be a free variable x of $\Gamma$, $\Delta$ or $!_{(a, \phi ; \sigma ')} K$.

• (i) If the variable u occurs in $x\sigma$, then u is a free variable of $\Gamma '$ or $!_{(a, \phi ; \sigma ')} K$.

• (ii) The variable a does not occur in $x\sigma$.

Proof

(i) By induction over the number of steps before application of the focus R-rule. Assume that the first rule applied is the focus R-rule. There are several cases. Firstly, assume u occurs bound in $\Gamma$. We consider here only the case that u occurs in $(a_1, \Phi _1, \sigma _1):N_1$, which is part of $\Gamma$; all other cases are similar. By assumption we have $u < a_1$ and $x < u$. The !R-rule implies $a_1 < a$. If x occurs freely in $\Gamma$, we also have $a < x$ via the !R-rule, which is a contradiction. If x occurs freely in K, then we also have $a_1 < x$ via the !R-rule, which is a contradiction. Secondly, assume u occurs bound in K. Hence x cannot be a free variable of K. In this case we have $u < a$ and $x < u$ by assumption, together with $a <x$ by the !R-rule, which is a contradiction. The step case is true because there are fewer free variables in the conclusion of a rule than in the premises.

(ii) Assume $x < a$. Then there must exist a u such that $x <u$ and $u < a$. The latter implies u is a bound variable in K, which is a contradiction to (i).

Theorem 3

(Completeness). Let $\Phi$ be a set of Eigen-, special, and existential variables which contains all the free variables of $\Gamma$, $\Delta$ and F. Let $\sigma :\Phi \rightarrow \Phi$ be a substitution. Let $sk_L(\Phi ; \Gamma ) = (\Gamma '; \sigma _{\Gamma '})$, $sk_L(\Phi ; \Delta ) = (\Delta ';\sigma _{\Delta '})$ and $sk_R(\Phi ; F)= (K; \sigma _K)$. Let $\Phi ' = (FV(\Gamma ') \cup FV(\Delta ') \cup FV(K)) \setminus \Phi$ and $\tau = \sigma _{\Gamma '}, \sigma _{\Delta '}, \sigma _K$. Let $\sigma ':\Phi ,\Phi '\rightarrow \Phi '$ be a substitution.

• (i) If $\mathop {neg}(\Gamma '); \Delta ' \vdash K; \sigma , \tau , \sigma '$ then $\Gamma \sigma _{\uparrow \llcorner {\Phi }\lrcorner }; \Delta \sigma _{\uparrow \llcorner {\Phi }\lrcorner } \vdash F\sigma _{\uparrow \llcorner {\Phi }\lrcorner }$ in focused intuitionistic linear logic.

• (ii) If $\Delta ' = \Delta '', \downarrow K'$ and $\mathop {neg}(\Gamma '); \Delta '', [K'] \vdash K; \sigma , \tau , \sigma '$ then $\Gamma \sigma _{\uparrow \llcorner {\Phi }\lrcorner }; \Delta \sigma _{\uparrow \llcorner {\Phi }\lrcorner } \vdash F\sigma _{\uparrow \llcorner {\Phi }\lrcorner }$ in focused intuitionistic linear logic.

• (iii) If $\mathop {neg}(\Gamma '); \Delta ' \vdash [K]; \sigma , \tau , \sigma '$ then $\Gamma \sigma _{\uparrow \llcorner {\Phi }\lrcorner }; \Delta \sigma _{\uparrow \llcorner {\Phi }\lrcorner } \vdash F\sigma _{\uparrow \llcorner {\Phi }\lrcorner }$ in focused intuitionistic linear logic.

Proof

We use firstly an induction over the derivation of $\mathop {neg}(\Gamma '); \Delta ' \vdash K; \sigma , \tau , \sigma '$ and secondly an induction over the structure of $\Delta , F$. Let $\Delta = F_1, \ldots , F_n$ and $\Delta ' = K_1, \ldots , K_n$. Let $V = \{x_1,\ldots ,$ $x_k, u_1, \ldots , u_m\}$ be the set of outermost bound variables of $\Delta ', K$ (including names). There are several cases. Firstly, if there exists a i such that $1 \le i \le n$ and $F_i$ is a tensor product or a formula !N, or F is a linear implication, we apply the corresponding inference rule and then the induction hypothesis.

Secondly, assume there exists an Eigen-variable $u \in V$. Assume $F = \forall u.F'$. Hence by induction hypothesis we have $\Gamma \sigma _{\uparrow \llcorner {\Phi }\lrcorner }; \Delta \sigma _{\uparrow \llcorner {\Phi }\lrcorner } \vdash F'\sigma _{\uparrow \llcorner {\Phi }\lrcorner }$. By assumption, u does not occur in $x\sigma$ for any variable x in the co-domain of $\sigma$. Now the $\forall R$-rule yields the claim. Now assume $F = \exists u.F'$. This case is similar to $\forall R$.

Thirdly, assume there exists an existential variable in V. Let x be an existential variable which is maximal in V. Assume $F = \exists x.F'$. We show that every Eigen-variable u of $x\sigma '$ is a free variable of $\Delta , F$. By definition, we have $x <u$. Assume u is a bound variable in $\Delta , F$. If u is a bound variable of F, we would have $u < x$, which is a contradiction. Hence u is a bound variable of $\Delta$. Because u is not an outermost bound variable, there exists a bound existential variable y such that $u < y$. Hence x is not a maximal bound variable. By induction hypothesis we have $\Gamma \sigma _{\uparrow \llcorner {\Phi }\lrcorner }; \Delta \sigma _{\uparrow \llcorner {\Phi }\lrcorner } \vdash F'\sigma _{\uparrow \llcorner {\Phi }\lrcorner }$, and now we apply the $\exists R$-rule. Now assume $F_1 = \forall x.F_1'$. Similar to the $\exists R$-case.

Next, assume there are no maximal first-order variables in V. By definition, the special variables corresponding to the last rule applied to the skolemised version where the principal formula is asynchronous are now the only maximal elements in V. $\mathbin {\otimes }R$ and ${-\!\!\circ }L$ are direct consequences of Lemma 6 and Lemma 7, respectively. For !R, let x be any outermost bound variable in $\Gamma$, $\Delta$ or K which is not maximal in V. Because $x \not < a$, there exists a variable y or u in V such that $x < y$ or $x < u$, which is a contradiction. Hence we can use the !R-rule of the skolemised calculus and the induction hypothesis. Finally, the axiom rule in the skolemised calculus implies $n=1$, and hence $\Gamma \sigma _{\uparrow \llcorner {\Phi }\lrcorner };F_1\sigma _{\uparrow \llcorner {\Phi }\lrcorner } \vdash F\sigma _{\uparrow \llcorner {\Phi }\lrcorner }$.    $\square$

6 Conclusion

In this paper, we revisit the technique of skolemisation and adopt it for proof search in first-order focused and polarised intuitionistic linear logic (LJF). The central idea is to encode quantifier dependencies by constraints, and the global partial order in which quantifier rules have to be applied by a substitution. We propose a domain specific logic called SLJF, which avoids back-tracking during proof search when variable instantiations are derived by unification.

Related Work: Shankar [8] first propose an adaptation of skolemisation to LJ. Our paper can be seen as a generalisation of this work to focused and polarised linear logic. Reis and Paleo [7] propose a technique called epsilonisation to characterise the permutability of rules in LJ. Their approach is elegant but impractical, because it trades an exponential growth in the search space with an exponential growth in the size of the proof terms. McLaughlin and Pfenning [4] propose an effective proof search technique based on the inverse method for focused and polarised intuitionistic logic. To our knowledge, the resulting theorem prover Imogen [5] would benefit from the presentation of skolemisation in our paper, since it requires backtracking to resolve the first-order non-determinism during proof search.

Applications: There are ample of applications for skolemisation. To our knowledge, proof search algorithms for intuitionistic or substructural logic are good at removing non-determinism from the propositional level, but don’t solve the problem at the first-order level. Skolemisation can also be applied to improve intuitionistic theorem provers further, such as Imogen. With the results in this paper we believe that we are able to achieve such results without much of a performance penalty.