LINEAR LOGIC AS A FRAMEWORK FOR SPECIFYING SEQUENT CALCULUS

DALE MILLER AND ELAINE PIMENTEL

Abstract. In recent years, intuitionistic logic and type systems have been used in numerous computational systems as frameworks for the specification of natural deduction proof systems. As we shall illustrate here, linear logic can be used similarly to specify the more general setting of sequent calculus proof systems. Linear logic’s meta theory can be used also to analyze properties of a specified object-level proof system. We shall present several example encodings of sequent calculus proof systems using the Forum presentation of linear logic. Since the object-level encodings result in logic programs (in the sense of Forum), various aspects of object-level proof systems can be automated.

§1. Introduction. Logics and type systems have been exploited in recent years as frameworks for the specification of deduction in a number of logics. Such meta logics or logical frameworks have generally been based on intuitionistic logic in which quantification at (non-predicate) higher-order types is available. Identifying a framework that allows the specification of a wide range of logics has proved to be most practical since a single implementation of such a framework can then be used to provide various degrees of automation of object-logics. For example, Isabelle [26] and λProlog [25] are implementations of an intuitionistic logic subset of Church’s Simple Theory of Types, while Elf [27] is an implementation of a dependently typed λ-calculus [16]. These computer systems have been used as meta languages to automate various aspects of various logics.

Features of a meta-logic are often directly inherited by any object-logic. This inheritance can be, at times, a great asset. For example, if the meta-logic is rich enough to include λ-bindings in its syntax and to provide α and β conversion as part of its equality of syntax (as is the case for the systems mentioned above), the object-logics immediately inherit such simple and declarative treatments of binding constructs and substitutions. On the other hand, features of the meta-logic can limit the kinds of object-logics that can be directly and naturally encoded. For example, the structural rules of an intuitionistic meta-logic (weakening and contraction) are also inherited making it difficult to have natural encodings of any logic for which these structural rules are not intended. Also, intuitionistic

2 DALE MILLER AND ELAINE PIMENTEL

logic does not have an involutive negation, making it difficult to address directly dualities in object-logics.

In this paper, we make use of linear logic as a meta-logic and find that we can specify a variety of proof systems for object-level systems. By making use of classical linear logic, we are able to capture not only natural deduction proof systems but also many sequent calculus proof systems. We will present our scheme for encoding proof systems in linear logic and show several examples of making such specifications. Since the encodings of such logical systems are natural and direct the rich meta-theory of linear logic can be used to drawing conclusions about the object-level proof systems, and we illustrate such reasoning as well.

This paper is organized as follows: Section 2 gives an introduction to linear logic and Forum. Section 3 shows the representation of sequents and inference rules, while Forum encodings of the well-known proof systems for linear, classical and intuitionistic logics are presented in Section 4. Using the meta-theory, it is possible to prove the collapsing of some modal prefixes for the specified classical and intuitionistic systems. In Section 5 other sequent calculus for these logics are encoded where modal prefixes collapse less dramatically. In order to show how to represent systems that make use of polarities, Section 6 presents an encoding of the so called Logic of Unity (LU) proof system. Section 7 provides an overview of how one might proof search for both Forum and encoded object-level proof systems. We conclude and discuss some future research directions in Section 8.

Our main purpose in this paper is to illustrate via examples how linear logic can be used to both specify and reason about object-level sequent proof systems. We shall do this largely by presenting a series of examples. More extensive discussion of the material in this paper can be found in the PhD dissertation of the second author [28].

§2. Overview of Linear Logic and Forum. Linear Logic [13] uses the following logical connectives: the exponentials ! and ?; ⊗, ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} , ⊥, and 1 for the multiplicative conjunction, disjunction, false, and true; &, ⊕, 0, ⊤ for the additive version of these connectives; −∘ for linear implication, and ∀ and ∃ for universal and existential quantification. We shall assume that the reader is familiar with the sequent calculus presentation of linear logic and with its basic properties.

2.1. The Forum presentation of linear logic. The connectives of linear logic can be classified as synchronous and asynchronous [2] depending on whether or not the right introduction rule for that connective needs to “synchronize” with its surrounding context. The de Morgan dual of a connective in one of these

LINEAR LOGIC AS A FRAMEWORK FOR SPECIFYING SEQUENT CALCULUS 3

classes yields a connective in the other class. Given this division of connectives, Miller proposed in [23] the Forum presentation of linear logic in which formulas are build using only the asynchronous connectives, namely, ?, ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} , ⊥, &, ⊤, −∘, and ∀, along with the intuitionistic version of implication (B ⇒ C denotes ! B −∘ C). The synchronous connectives are implicitly available in Forum since a two sided sequent is used: connectives appearing on the left of the sequent arrow behave synchronously. Proof search in the Forum presentation of linear logic resembles the search involved in logic programming [24, 22]: introducing asynchronous connectives corresponds to goal-directed search and introducing synchronous connectives corresponds to backchaining over logic program clauses.

Forum is a presentation of all of linear logic since it contains a complete set of connectives. The connectives missing from Forum are directly definable using the following logical equivalences:

B^{⊥} ≡ B −∘ ⊥  0 ≡ ⊤ −∘ ⊥  1 ≡ ⊥ −∘ ⊥  ∃x.B ≡ (∀x.B^{⊥})^{⊥}
! B ≡ (B ⇒ ⊥) −∘ ⊥  B ⊕ C ≡ (B^{⊥} & C^{⊥})^{⊥}  B ⊗ C ≡ (B^{⊥} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} C^{⊥})^{⊥}

The collection of connectives in Forum is not minimal. For example, ? and ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} , can be defined in terms of the remaining connectives:

? B ≡ (B −∘ ⊥) ⇒ ⊥ and B ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} C ≡ (B −∘ ⊥) −∘ C.

Here, the equivalence B ≡ C means that the universal closure of the expression (B −∘ C) & (C −∘ B) is provable in linear logic.

To help make the connection between proof search in Forum and logic programming, it is useful to introduce the notions of goal and clause into Forum. A formula is a Forum clause if it is of the form

∀ȳ(G_{1} ↪ ⋯ ↪ G_{m} ↪ G_{0}), (m ≥ 0)

where G_{0}, …, G_{m} are arbitrary Forum formulas and occurrences of ↪ are either occurrences of −∘ or ⇒. A formula of Forum is a flat goal if it does not contain occurrences of −∘ and ⇒ and all occurrences of ? have atomic scope. A Forum clause is a flat clause if G_{0}, …, G_{m} are flat goals. It is possible to also add the restriction that the formula G_{0}, the head of the clause, is of the form B_{1} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⋯ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B_{n}, where n ≥ 0 and each B_{i} is an atom. If n = 0 then we write the head as simply ⊥ and say that the head is empty. A flat clause is essentially a clause of the LinLog system [2] except that heads of flat clauses may be empty. It will be the case that all formulas used to specify sequent calculus inferences rules in this paper will be flat Forum clauses.

As in Church’s Simple Theory of Types [6], both terms and formulas are built using a simply typed λ-calculus. We assume the usual rules of α, β, and ηconversion and we identify terms and formulas up to α-conversion. A term is

4 DALE MILLER AND ELAINE PIMENTEL

λ-normal if it contains no β and no η redexes. All terms are λ-convertible to a term in λ-normal form, and such a term is unique up to α-conversion. The substitution notation B[t/x] denotes the λ-normal form of the β-redex (λx.B)t. Following [6], we shall also assume that formulas of Forum have type o.

2.2. Proof system for Forum. The proof system for Forum, F, is given in Figure 1. Sequents in F have the form

Σ: Ψ; Δ ⟶ Γ; Υ and Σ: Ψ; Δ ⟶^{B} Γ; Υ,

where Σ is a signature, Δ and Γ are multisets of formulas, Ψ and Υ are sets of formulas, and B is a formula. All formulas in sequents are composed of the asynchronous connectives listed above (together with ⇒) and contain at most the non-logical symbols present in Σ (such formulas are called Σ-formulas). The intended meanings of these two sequents in linear logic are

! Ψ, Δ ⟶ Γ,? Υ and ! Ψ, Δ, B ⟶ Γ,? Υ,

respectively. In the proof system of Figure 1, the only right rules are those for sequents of the form Σ: Ψ; Δ ⟶ Γ; Υ. The syntactic variable A in Figure 1 denotes a multiset of atomic formulas. Left rules are applied only to the formula B that labels the sequent arrow in Σ: Ψ; Δ ⟶^{B} A; Υ.

We use the turnstile symbol as the mathematical-level judgment that a sequent is provable: that is, Δ ⊢ Γ means that the two-sided sequent Δ ⟶ Γ has a linear logic proof. The following correctness theorem for F is given in [23] and is based on the focusing result of Andreoli in [2].

Theorem 2.1. Let Σ be a signature, Δ and Γ be multisets of Σ-formulas, and Ψ and Υ be sets of Σ-formulas. The sequent Σ: Ψ; Δ ⟶ Γ; Υ has a proof in F if and only if ! Ψ, Δ ⊢ Γ,? Υ.

We shall use the term backchaining to refer to an application of either the decide or the decide! inference rule followed by a series of applications of leftintroduction rules (reading a proof bottom-up). This notion of backchaining generalizes the usual notion found in the logic programming literature.

When presenting examples of Forum code we often use ∘− and ⇒ to be the converses of −∘ and ⇐ since they provide a more natural operational reading of clauses (similar to the use of :- in Prolog). We will assume that when parsing expressions, ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} and & bind tighter than ∘− and ⇐.

Multiset rewriting can be captured naturally in proof search. Consider, for example, the clause

a ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} b ∘− c ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} d ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} e.

and the sequent Σ: Ψ; Δ ⟶ a, b, Γ; Υ, where the clause displayed above is a member of Ψ. A proof for this sequent can then end with the following inference

\overline{Σ: Ψ; Δ ⟶ ⊤, Γ; Υ} ⊤R

\frac{Σ: Ψ; Δ ⟶ B, Γ; Υ Σ: Ψ; Δ ⟶ C, Γ; Υ}{Σ: Ψ; Δ ⟶ B & C, Γ; Υ} & R

\frac{Σ: Ψ; Δ ⟶ Γ; Υ}{Σ: Ψ; Δ ⟶ ⊥, Γ; Υ} ⊥R \frac{Σ: Ψ; Δ ⟶ B, C, Γ; Υ}{Σ: Ψ; Δ ⟶ B ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} C, Γ; Υ} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} R

\frac{Σ: Ψ; B, Δ ⟶ C, Γ; Υ}{Σ: Ψ; Δ ⟶ B −∘ C, Γ; Υ} −∘ R \frac{Σ: B, Ψ; Δ ⟶ C, Γ; Υ}{Σ: Ψ; Δ ⟶ B ⇒ C, Γ; Υ} ⇒ R

\frac{y: τ, Σ: Ψ; Δ ⟶ B[y/x], Γ; Υ}{Σ: Ψ; Δ ⟶ ∀_{τ} x.B, Γ; Υ} ∀R \frac{Σ: Ψ; Δ ⟶ Γ; B, Υ}{Σ: Ψ; Δ ⟶ ? B, Γ; Υ} ? R

\frac{Σ: B, Ψ; Δ ⟶^{B} A; Υ}{Σ: B, Ψ; Δ ⟶ A; Υ} decide! \frac{Σ: Ψ; Δ ⟶ A, B; B, Υ}{Σ: Ψ; Δ ⟶ A; B, Υ} decide?

\frac{Σ: Ψ; Δ ⟶^{B} A; Υ}{Σ: Ψ; B, Δ ⟶ A; Υ} decide

\overline{Σ: Ψ; · ⟶^{A} A; Υ} initial \overline{Σ: Ψ; · ⟶^{A} ·; A, Υ} initial ?
\overline{Σ: Ψ; · ⟶^{⊥} ·; Υ} ⊥L  \frac{Σ: Ψ; Δ ⟶^{B_{i}} A; Υ}{Σ: Ψ; Δ ⟶^{B_{1}&B_{2}} A; Υ} & L_{i}  \frac{Σ: Ψ; B ⟶ ·; Υ}{Σ: Ψ; · ⟶^{? B} ·; Υ} ? L

\frac{Σ: Ψ; Δ_{1} ⟶^{B} A_{1}; Υ Σ: Ψ; Δ_{2} ⟶^{C} A_{2}; Υ}{Σ: Ψ; Δ_{1}, Δ_{2} ⟶^{B^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} C} A_{1}, A_{2}; Υ} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} L \frac{Σ: Ψ; Δ ⟶^{B[t/x]} A; Υ}{Σ: Ψ; Δ ⟶^{∀_{τ} x.B} A; Υ} ∀L

\frac{Σ: Ψ; Δ_{1} ⟶ A_{1}, B; Υ Σ: Ψ; Δ_{2} ⟶^{C} A_{2}; Υ}{Σ: Ψ; Δ_{1}, Δ_{2} ⟶^{B−∘C} A_{1}, A_{2}; Υ} −∘ L

\frac{Σ: Ψ; · ⟶ B; Υ Σ: Ψ; Δ ⟶^{C} A; Υ}{Σ: Ψ; Δ ⟶^{B⇒C} A; Υ} ⇒ L

Figure 1. The F proof system. The rule ∀R has the proviso that y is not declared in the signature Σ, and the rule ∀L has the proviso that t is a Σ-term of type τ. In &L_{i}, i = 1 or i = 2.

rules.

Σ: Ψ; Δ ⟶ c, d, e, Γ; Υ Σ: Ψ; Δ ⟶ c, d ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} e, Γ; Υ Σ: Ψ; Δ ⟶ c ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} d ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} e, Γ; Υ

Σ: Ψ; · ⟶^{a} a; Υ Σ: Ψ; · ⟶^{b} b; Υ

Σ: Ψ; · ⟶^{a^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} b} a, b; Υ

Σ: Ψ; Δ ⟶^{c^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} d^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} e−∘a^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} b} a, b, Γ; Υ

Σ: Ψ; Δ ⟶ a, b, Γ; Υ

We can interpret this proof fragment as a reduction of the multiset a, b, Γ to the multiset c, d, e, Γ by backchaining on the clause displayed above.

6 DALE MILLER AND ELAINE PIMENTEL

Of course, a clause may have multiple, top-level implications. In this case, the surrounding context must be manipulated properly to prove the sub-goals that arise in backchaining. Consider a clause of the form

G_{1} −∘ G_{2} ⇒ G_{3} −∘ G_{4} ⇒ B_{1} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B_{2}

labeling the sequent arrow in the sequent Σ: Ψ; Δ ⟶ B_{1}, B_{2}, A; Υ. An attempt to prove this sequent would then lead to attempt to prove the four sequents

Σ: Ψ; Δ_{1} ⟶ G_{1}, A_{1}; Υ Σ: Ψ; · ⟶ G_{2}; Υ
Σ: Ψ; Δ_{2} ⟶ G_{3}, A_{2}; Υ Σ: Ψ; · ⟶ G_{4}; Υ

where Δ is the multiset union of Δ_{1} and Δ_{2}, and A is the multiset union of A_{1} and A_{2}. In other words, those subgoals immediately to the left of an ⇒ are attempted with empty bounded contexts: the bounded contexts, here Δ and A, are divided up to be used to prove those goals immediately to the left of −∘.

2.3. Applications of Forum. Forum specifications have been presented for the operational semantics of programming languages containing side effects, concurrency features, references, exceptions, continuations, and objects [3, 5, 8, 23]. Chirimar [5] used Forum to present the semantics of a RISC processor and Chakravarty [4] used it to specify the logical and operational semantics of a parallel programming language. A specification of a sequent calculus for intuitionistic logic was given by Miller in [23]: that example was improved by Ricci [30], where a proof system for classical logic was also given. The examples in [23, 30] are significantly generalized in this paper.

§3. Representing sequents and inference rules. Since we now wish to represent one logic and proof system within another, we need to distinguish between the meta-logic, namely, linear logic as presented by Forum, and the various object-logics for which we wish to specify sequent proof systems. Formulas of the object-level will be identified with meta-level terms of type bool. Object-level logical connectives will be introduced as needed and as constructors of this type.

A two-sided sequent Δ ⟶ Γ is generally restricted so that Δ and Γ are either lists, multisets, or sets of formulas. Sets are used if all three structural rules (exchange, weakening, contraction) are implicit; multisets are used if exchange is implicit; and lists are used if no structural rule is implicit. Since our goal here is to encode object-level sequents into meta-level sequents as directly as possible, and since contexts in Forum are either multisets or sets, we will not be able to represent sequents that make use of lists. It is unlikely, for example, that non-commutative object-logics can be encoded into our linear logic meta theory along the lines we describe below.

LINEAR LOGIC AS A FRAMEWORK FOR SPECIFYING SEQUENT CALCULUS 7

3.1. Three schemes for encoding sequents. Consider the well known, two-sided sequent proof systems for classical, intuitionistic, and linear logic. A convenient distinction between these logics can be described, in part, by where the structural rules of thinning and contraction can be applied. In classical logic, these structural rules are allowed on both sides of the sequent arrow; in intuitionistic logic, no structural rules are allowed on the right of the sequent arrow; and in linear logic, they are not allowed on either sides of the arrow. Thus a classical sequent is a pairing of two sets; a linear logic sequent is a pairing of two multisets; and an intuitionistic sequent is the pairing of a set (for the lefthand side) and a multiset (for the right-hand side). This discussion suggests the following representation of sequents in these three systems. Let bool be the type of object-level propositional formulas and let ⌊·⌋ and ⌈·⌉ be two meta-level predicates, both of type bool → o.

We will identify three schemes for encoding sequents. The linear scheme encodes the (object-level) sequent B_{1}, …, B_{n} ⟶ C_{1}, …, C_{m} (n, m ≥ 0) by the meta-level formula ⌊B_{1}⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⋯ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌊B_{n}⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈C_{1}⌉ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⋯ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈C_{m}⌉ or by the Forum sequent

Σ: ·; · ⟶ ⌊B_{1}⌋, …, ⌊B_{n}⌋, ⌈C_{1}⌉, …, ⌈C_{m}⌉; ·.

The intuitionistic scheme encodes B_{1}, …, B_{n} ⟶ C_{1}, …, C_{m}, where n, m ≥ 0, with the meta-level formula ?⌊B_{1}⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⋯ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ?⌊B_{n}⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈C_{1}⌉ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⋯ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈C_{m}⌉ or by the Forum sequent

Σ: ·; · ⟶ ⌈C_{1}⌉, …, ⌈C_{m}⌉; ⌊B_{1}⌋, …, ⌊B_{n}⌋.

Often intuitionistic sequents are additionally restricted to having one formula on the right. Finally, the classical scheme encodes the sequent B_{1}, …, B_{n} ⟶ C_{1}, …, C_{m} (n, m ≥ 0) as the meta-level formula

?⌊B_{1}⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⋯ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ?⌊B_{n}⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ?⌈C_{1}⌉ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⋯ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ?⌈C_{m}⌉

or by the Forum sequent

Σ: ·; · ⟶ ·; ⌊B_{1}⌋, …, ⌊B_{n}⌋, ⌈C_{1}⌉, …, ⌈C_{m}⌉.

The ⌊·⌋ and ⌈·⌉ predicates are used to identify which object-level formulas appear on which side of the sequent arrow, and the ? modal is used to mark the formulas to which weakening and contraction can be applied.

3.2. Encoding additive and multiplicative inference rules. We first illustrate how to encode object-level inference rules using the linear scheme.

Consider the specification of the logical inference rules for object-level conjunction, represented here as the infix constant ∧ of type bool → bool → bool.

Consider first the additive inference rules for this connective.

\frac{Δ, A ⟶ Γ}{Δ, A ∧ B ⟶ Γ} ∧ L_{1} \frac{Δ, B ⟶ Γ}{Δ, A ∧ B ⟶ Γ} ∧ L_{2} \frac{Δ ⟶ Γ, A Δ ⟶ Γ, B}{Δ ⟶ Γ, A ∧ B} ∧ R

These three inference rules can be specified in Forum using the clauses

\begin{matrix}(∧L_{1}) & ⌊A ∧ B⌋ & ∘− ⌊A⌋. & (∧R) & ⌈A ∧ B⌉ & ∘− ⌈A⌉ & ⌈B⌉. \\ (∧L_{2}) & ⌊A ∧ B⌋ & ∘− ⌊B⌋. \end{matrix}

Let Ψ be a set of formulas that contains the three clauses. The Forum sequent

Σ: Ψ; · ⟶ ⌊B_{1}⌋, …, ⌊B_{n}⌋, ⌈C_{1}⌉, …, ⌈C_{m}⌉; ·

can be the conclusion of a decide! rule that selected (∧R) rule only if one of the ⌈·⌉-atoms, say ⌈C_{1}⌉, is of the form A ∧ B and the sequent

Σ: Ψ; · ⟶ ⌊B_{1}⌋, …, ⌊B_{n}⌋, ⌈A⌉ & ⌈B⌉, ⌈C_{2}⌉, …, ⌈C_{m}⌉; ·

is provable. This formula is provable if and only if the two sequents

Σ: Ψ; · ⟶ ⌊B_{1}⌋, …, ⌊B_{n}⌋, ⌈A⌉, ⌈C_{2}⌉, …, ⌈C_{m}⌉; ·

and

Σ: Ψ; · ⟶ ⌊B_{1}⌋, …, ⌊B_{n}⌋, ⌈B⌉, ⌈C_{2}⌉, …, ⌈C_{m}⌉; ·

are provable in Forum. Thus, backchaining on the (∧R) clause above can be used to reduce the problem of finding an object-level proof of

B_{1}, …, B_{n} ⟶ A ∧ B, C_{2}, …, C_{m}

to the problem of finding object-level proofs for

B_{1}, …, B_{n} ⟶ A, C_{2}, …, C_{m} and B_{1}, …, B_{n} ⟶ B, C_{2}, …, C_{m}.

Thus, we have successfully captured this right introduction rule for conjunction using decide! with the clause corresponding to (∧R). A similar and simpler argument shows how left introduction for ∧ is also correctly encoded using the two clauses for (∧L). Notice that the two clauses for left introduction could be written equivalently in linear logic as the one formula

⌊A ∧ B⌋ ∘− ⌊A⌋ ⊕ ⌊B⌋.

(Although ⊕ is not a connective of Forum, we shall use it in this fashion in order to write two Forum clauses as one formula.) Thus, these additive rules make use of two (dual) meta-level additive connectives: & and ⊕.

Now consider encoding the multiplicative version of conjunction introduction.

\frac{Δ, A, B ⟶ Γ}{Δ, A ∧ B ⟶ Γ} ∧ L \frac{Δ_{1} ⟶ Γ_{1}, A Δ_{2} ⟶ Γ_{2}, B}{Δ_{1}, Δ_{2} ⟶ Γ_{1}, Γ_{2}, A ∧ B} ∧ R

LINEAR LOGIC AS A FRAMEWORK FOR SPECIFYING SEQUENT CALCULUS 9

It is an easy matter to check that the following two clauses encode these two inference rules.

(∧L) ⌊A ∧ B⌋ ∘− ⌊A⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌊B⌋.  (∧R) ⌈A ∧ B⌉ ∘− ⌈A⌉ ∘− ⌈B⌉.

Notice that the clause for right introduction could be written equivalently in linear logic as

⌈A ∧ B⌉ ∘− ⌈A⌉ ⊗ ⌈B⌉.

Thus, these multiplicative rules make use of two (dual) meta-level multiplicative connectives: ⊗ and ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} .

Consider now using the classical scheme for representing sequents and consider writing the additive version of the (∧R) rule as

⌈A ∧ B⌉ ∘− ?⌈A⌉ & ?⌈B⌉.

In that case, backchaining on this clause would reduce proof search of the sequent

Σ: Ψ; · ⟶ ·; ⌊B_{1}⌋, …, ⌊B_{n}⌋, ⌈C_{1}⌉, …, ⌈C_{m}⌉

(where for some i, C_{i} is A ∧ B) to finding proofs for the two sequents

Σ: Ψ; · ⟶ ?⌈A⌉; ⌊B_{1}⌋, …, ⌊B_{n}⌋, ⌈C_{1}⌉, …, ⌈C_{m}⌉

and

Σ: Ψ; · ⟶ ?⌈B⌉; ⌊B_{1}⌋, …, ⌊B_{n}⌋, ⌈C_{1}⌉, …, ⌈C_{m}⌉

which in turn are provable if and only if the sequents

Σ: Ψ; · ⟶ ·; ⌊B_{1}⌋, …, ⌊B_{n}⌋, ⌈A⌉, ⌈C_{1}⌉, …, ⌈C_{m}⌉

and

Σ: Ψ; · ⟶ ·; ⌊B_{1}⌋, …, ⌊B_{n}⌋, ⌈B⌉, ⌈C_{1}⌉, …, ⌈C_{m}⌉

are provable.

If we had used, instead, the multiplicative encoding of conjunctive introduction,

⌈A ∧ B⌉ ∘− ?⌈A⌉ ⊗?⌈B⌉.

a slightly different meta-level proof would have made the same reduction.

It seems natural to consider using a question mark in the head of a clause describing a right or left-introduction rule for classical logic (or just the leftintroduction rule for intuitionistic logic). For example, the (∧R) rule could have been encoded as

?⌈A ∧ B⌉ ∘− ?⌈A⌉ & ?⌈B⌉.

This encoding style was used in [23, 30], for example. We shall prefer, instead, to encode inference rules without occurrences of question marks in the head of clauses since the structure of meta-level proofs often does not correspond to the structure of object-level proofs. For example, although the sequent

10 DALE MILLER AND ELAINE PIMENTEL

A ∧ B ∧ C ⟶ B is provable in classical logic, there is no equivalent object-level proof for the proof displayed below. Here, signatures are not displayed in sequents, Γ = ⌈B⌉, ⌊A ∧ B ∧ C⌋, and Ψ is a set of formulas that contains the clause displayed above and Initial (see Section 3.4).

{Ψ; · ⟶^{⌊A∧B⌋} ·; ⌊A ∧ B⌋, Γ \atop Ψ; ⌊A ∧ B⌋ ⟶ ·; ⌊A ∧ B⌋, Γ} ; Ψ; ⌊A ∧ B⌋ ⟶ ?⌊A ∧ B⌋; Γ {Ψ; · ⟶^{⌊A∧B∧C⌋} ·; Γ \atop Ψ; ⌊A ∧ B ∧ C⌋ ⟶ ·; Γ} ; Ψ; · ⟶^{?⌊A∧B∧C⌋} ·; Γ

Ψ; ⌊A ∧ B⌋ ⟶^{?⌊A∧B∧C⌋∘−?⌊A∧B⌋} ·; Γ

Ψ; ⌊A ∧ B⌋ ⟶ ·; Γ

Ψ; · ⟶^{?⌊A∧B⌋} ·; Γ

{Ψ; · ⟶^{⌈B⌉} ·; ⌊B⌋, Γ \atop Ψ; ⌈B⌉ ⟶ ·; ⌊B⌋, Γ} ; Ψ; · ⟶^{?⌈B⌉} ·; ⌊B⌋, Γ {Ψ; · ⟶^{⌊B⌋} ·; ⌊B⌋, Γ \atop Ψ; ⌊B⌋ ⟶ ·; ⌊B⌋, Γ} ; Ψ; · ⟶^{?⌊B⌋} ·; ⌊B⌋, Γ

Ψ; · ⟶^{?⌈B⌉............................................................................................... ?⌊B⌋} ·; ⌊B⌋, Γ

Ψ; · ⟶ ·; ⌊B⌋, Γ

Ψ; · ⟶ ?⌊B⌋; Γ

Ψ; · ⟶^{?⌊A∧B⌋∘−?⌊B⌋} ·; Γ

Ψ; · ⟶ ·; Γ decide!

The fact that “focus” is lost when a question mark is encountered on a formula labeling a sequent arrow means that it is much harder to control the structure of meta-level proofs and to relate them to object-level proofs.

3.3. Encoding quantifier introduction rules. Using the quantification of higher-order types that is available in Forum, it is a simple matter to encode the inference rules for object-level quantifiers. For example, if we use the linear scheme for representing sequents, then the left and right introduction rules for object-level universal quantifier can be written as

(∀L) ⌊∀B⌋ ∘− ⌊Bx⌋.  (∀R) ⌈∀B⌉ ∘− ∀x⌈Bx⌉.

Here, the symbol ∀ is used for both meta-level and object-level quantification: at the object-level ∀ has the type (i → bool) → bool. Thus the variable B above has the type i → bool. Consider the Forum sequent Σ: Ψ; · ⟶ ⌈∀B⌉, Θ; · where Ψ contains the above two clauses. Using decide! with the clause for (∀R) would cause the search for a proof of the above sequent to be reduced to the search for a proof of the sequent Σ, y : i: Ψ; · ⟶ ⌈By⌉, Θ; · where y is not present in the signature Σ. Here, the meta-level eigen-variable y also serves the role of an object-level eigen-variable. Dually, consider the Forum sequent Σ: Ψ; · ⟶ ⌊∀B⌋, Θ; ·. Using the decide! with the clause for (∀L) would cause proof search to reduce this sequent to the sequent Σ: Ψ; · ⟶ ⌊Bt⌋, Θ; · where t is a Σ-term of type i. If we restrict appropriately the use of the type i by constants in Σ, then Σ-terms of type i can be identified with object-level terms.

Notice that the clause for (∀L) is logically equivalent to the formula

⌊∀B⌋ ∘− ∃x⌊Bx⌋.

LINEAR LOGIC AS A FRAMEWORK FOR SPECIFYING SEQUENT CALCULUS 11

Thus, these quantifier rules make use of two (dual) meta-level quantifiers.

3.4. The cut and initial rules. Up to this point, all the Forum clauses used to specify an inference figure have been such that the head of the clause has been an atom. Clauses specifying the cut and initial rules will have heads of rather different structure.

Consider specifying the initial rule (the one asserting that the sequent B ⟶ B is provable) using the linear scheme for encoding sequents. The clause

(Initial) ⌊B⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈B⌉.

will properly encode this rule. Notice that this clause has a head with two atoms (and an empty body). Similarly, the cut rule

\frac{Δ_{1} ⟶ Γ_{1}, B Δ_{2}, B ⟶ Γ_{2}}{Δ_{1}, Δ_{2} ⟶ Γ_{1}, Γ_{2}} Cut

can be specified simply as the clause

(Cut) ⊥∘− ⌊B⌋ ∘− ⌈B⌉.

Dually to the initial rule, this clause has an empty head and two bodies.

3.5. Advantages of such encodings. The encoding of an object-level proof system as Forum clauses has certain advantages over encoding them as inference figures. For example, the Forum specifications do not deal with context explicitly and instead they focus on the formulas that are directly involved in the inference rule. The distinction between making the inference rule additive or multiplicative is achieved in inference rule figures by explicitly presenting contexts and either splitting or copying them. The Forum clause representation achieves the same distinction using meta-level additive or multiplicative connectives. Object-level quantifiers can be handled directly using the meta-level quantification. Similarly, the structural rules of contraction and thinning can be captured together using the ? modal. Finally, since the encoding of proof systems is natural and direct, we hope to be able to use the rich meta-theory of linear logic to help in drawing conclusions about object-level proof systems. An example of this kind of meta-level reason will be illustrated in Section 4.4 where a sequent calculus presentation of intuitionistic logic is transformed into a natural deduction presentation by rather simple linear logic equivalences.

Since the encodings of object-level encodings result in logic programs (in the sense of Forum) and since there is significant knowledge and tools available to provide automatic and interactive tools to compute with those logic programs, encodings such as those described here can be important for the automation of various proof systems (see Section 7).

12 DALE MILLER AND ELAINE PIMENTEL

There are, of course, some disadvantages to using linear logic as a meta-theory, the principle one being that it will not be possible to capture all proof systems, such as those for non-commutativity. As we shall see, however, significant and interesting proof systems can be encoded into linear logic and for these systems, broad avenues of meta-level reasoning and automation should be available.

§4. Linear, classical, and intuitionistic logics. In this section, we present Forum encodings of well-known proof systems for linear, classical, and intuitionistic logics. Object-level linear logic will be encoded reusing the same symbols that appear at the meta-level, namely, !, ?, ⊗, ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} , ⊥, 1, &, ⊕, 0, ⊤ −∘, ∀_{l}, and ∃_{l}. Classical logic is encoded using ∧, ∨, ⇒, f_{c}, t_{c}, ∀_{c}, and ∃_{c} for conjunction, disjunction, implication, false, true, and universal and existential quantification, respectively, while intuitionistic logic is encoded with ∩, ∪, ⊃, f_{i}, t_{i}, ∀_{i}, and ∃_{i} for conjunction, disjunction, implication, false, true, and universal and existential quantification, respectively.

We use the type i to denote object-level individuals and bool to denote objectlevel formulas (our object-logics will all be first-order). All binary connectives have type bool → bool → bool and will be written as infix. Object-level constants representing quantification are all of the second order type (i → bool) → bool: we abbreviated expressions such as ∀_{i}(λx.B) as simply ∀_{i}xB.

The three signatures Σ_{l}, Σ_{c}, and Σ_{j} will denote the signatures for the objectlogics for linear, classical, and intuitionistic, respectively. We assume that each of these signatures also contains the two predicates ⌊·⌋ and ⌈·⌉.

4.1. Three proof systems. Let LL, LK, and LJ denote the be the set of clauses displayed in Figures 2, 3, and 4, respectively.

Proposition 4.1. The following three correctness statements hold.

1. The sequent B_{1}, …, B_{n} ⟶ C_{1}, …, C_{m} (m, n ≥ 0) has a linear logic proof [13] iff Σ_{l}: LL; · ⟶ ⌊B_{1}⌋, …, ⌊B_{n}⌋, ⌈C_{1}⌉, …, ⌈C_{m}⌉; · has a F-proof.

2. The sequent B_{1}, …, B_{n} ⟶ C_{1}, …, C_{m} (m, n ≥ 0) has an LK-proof [12] iff Σ_{c}: LK; · ⟶ ·; ⌊B_{1}⌋, …, ⌊B_{n}⌋, ⌈C_{1}⌉, …, ⌈C_{m}⌉ has a F-proof.

3. The sequent B_{1}, …, B_{n} ⟶ B_{0} has an LJ-proof [12] if and only if the sequent Σ_{j}: LJ; · ⟶ ⌈B_{0}⌉; ⌊B_{1}⌋, …, ⌊B_{n}⌋ has a F-proof and the sequent B_{1}, …, B_{n} ⟶ has an LJ-proof iff Σ_{j}: LJ; · ⟶ ·; ⌊B_{1}⌋, …, ⌊B_{n}⌋ has a F-proof (n ≥ 0).

Proofs are by structural induction of over proof structures. In all cases, proofs in Forum match closely proofs in the corresponding object-logic.

(−∘L) ⌊A −∘ B⌋ ∘− ⌈A⌉ ∘− ⌊B⌋.  (−∘R)  ⌈A −∘ B⌉ ∘− ⌊A⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈B⌉.
(⊗L) ⌊A ⊗ B⌋ ∘− ⌊A⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌊B⌋.  (⊗R)  ⌈A ⊗ B⌉ ∘− ⌈A⌉ ∘− ⌈B⌉.
(&L_{1}) ⌊A & B⌋ ∘− ⌊A⌋.  (&R)  ⌈A & B⌉ ∘− ⌈A⌉ & ⌈B⌉.
(&L_{2}) ⌊A & B⌋ ∘− ⌊B⌋.  (⊕R_{1})  ⌈A ⊕ B⌉ ∘− ⌈A⌉.
(⊕L) ⌊A ⊕ B⌋ ∘− ⌊A⌋ & ⌊B⌋.  (⊕R_{2})  ⌈A ⊕ B⌉ ∘− ⌈B⌉.
(^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} L) ⌊A ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B⌋ ∘− ⌊A⌋ ∘− ⌊B⌋.  (^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} R)  ⌈A ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B⌉ ∘− ⌈A⌉ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈B⌉.
(! L)  ⌊! B⌋ ∘− ?⌊B⌋.  (! R)  ⌈! B⌉ ⇐ ⌈B⌉.
(? L)  ⌊? B⌋ ⇐ ⌊B⌋.  (? R)  ⌈? B⌉ ∘− ?⌈B⌉.
(∀_{l}L)  ⌊∀_{l}B⌋ ∘− ⌊Bx⌋.  (∀_{l}R)  ⌈∀_{l}B⌉ ∘− ∀x⌈Bx⌉.
(∃_{l}L)  ⌊∃_{l}B⌋ ∘− ∀x⌊Bx⌋.  (∃_{l}R)  ⌈∃_{l}B⌉ ∘− ⌈Bx⌉.
(1L)  ⌊1⌋ ∘−⊥ .  (1R)  ⌈1⌉ ⇐ ⊤.
(⊥ L)  ⌊⊥⌋ ⇐ ⊤.  (⊥ R)  ⌈⊥⌉ ∘−⊥ .
(0L)  ⌊0⌋ ∘− ⊤.  (⊤R)  ⌈⊤⌉ ∘− ⊤.
(Cut)  ⊥ ∘− ⌊B⌋ ∘− ⌈B⌉.  (Initial) ⌊B⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈B⌉.

Figure 2. Forum specification of the LL sequent calculus.

(⇒ L) ⌊A ⇒ B⌋ ∘− ?⌈A⌉ ∘− ?⌊B⌋. (⇒ R)  ⌈A ⇒ B⌉ ∘− ?⌊A⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ?⌈B⌉.
(∧L_{1}) ⌊A ∧ B⌋ ∘− ?⌊A⌋.  (∧R)  ⌈A ∧ B⌉ ∘− ?⌈A⌉ & ?⌈B⌉.
(∧L_{2}) ⌊A ∧ B⌋ ∘− ?⌊B⌋.  (∨R_{1})  ⌈A ∨ B⌉ ∘− ?⌈A⌉.
(∨L) ⌊A ∨ B⌋ ∘− ?⌊A⌋ & ?⌊B⌋. (∨R_{2})  ⌈A ∨ B⌉ ∘− ?⌈B⌉.
(∀_{c}L)  ⌊∀_{c}B⌋ ∘− ?⌊Bx⌋.  (∀_{c}R)  ⌈∀_{c}B⌉ ∘− ∀x?⌈Bx⌉.
(∃_{c}L)  ⌊∃_{c}B⌋ ∘− ∀x?⌊Bx⌋.  (∃_{c}R)  ⌈∃_{c}B⌉ ∘− ?⌈Bx⌉.
(f_{c}L)  ⌊f_{c}⌋ ∘− ⊤.  (t_{c}R)  ⌈t_{c}⌉ ∘− ⊤.
(Cut)  ⊥ ∘− ?⌊B⌋ ∘− ?⌈B⌉. (Initial) ⌊B⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈B⌉.

Figure 3. Forum specification of the LK sequent calculus.

(⊃ L) ⌊A ⊃ B⌋ ∘− ⌈A⌉ ∘− ?⌊B⌋.  (⊃ R)  ⌈A ⊃ B⌉ ∘− ?⌊A⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈B⌉.
(∩L_{1}) ⌊A ∩ B⌋ ∘− ?⌊A⌋.  (∩R)  ⌈A ∩ B⌉ ∘− ⌈A⌉ & ⌈B⌉.
(∩L_{2}) ⌊A ∩ B⌋ ∘− ?⌊B⌋.  (∪R_{1})  ⌈A ∪ B⌉ ∘− ⌈A⌉.
(∪L) ⌊A ∪ B⌋ ∘− ?⌊A⌋ & ?⌊B⌋.  (∪R_{2})  ⌈A ∪ B⌉ ∘− ⌈B⌉.
(∀_{i}L)  ⌊∀_{i}B⌋ ∘− ?⌊Bx⌋.  (∀_{i}R)  ⌈∀_{i}B⌉ ∘− ∀x⌈Bx⌉.
(∃_{i}L)  ⌊∃_{i}B⌋ ∘− ∀x?⌊Bx⌋.  (∃_{i}R)  ⌈∃_{i}B⌉ ∘− ⌈Bx⌉.
(f_{i}L)  ⌊f_{i}⌋ ∘− ⊤.  (t_{i}R)  ⌈t_{i}⌉ ∘− ⊤.
(Cut)  ⊥ ∘− ?⌊B⌋ ∘− ⌈B⌉.  (Initial) ⌊B⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈B⌉.

Figure 4. Specification of the LJ sequent calculus.

\begin{matrix}(⇒ L) & ⌊A ⇒ B⌋ & ∘− ⌈A⌉ ∘− ⌊B⌋. & (⇒ R) & ⌈A ⇒ B⌉ & ∘− ⌊A⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈B⌉. \\ (∧L_{1}) & ⌊A ∧ B⌋ & ∘− ⌊A⌋. & (∧R) & ⌈A ∧ B⌉ & ∘− ⌈A⌉ & ⌈B⌉. \\ (∧L_{2}) & ⌊A ∧ B⌋ & ∘− ⌊B⌋. & (∨R_{1}) & ⌈A ∨ B⌉ & ∘− ⌈A⌉. \\ (∨L) & ⌊A ∨ B⌋ & ∘− ⌊A⌋ & ⌊B⌋. & (∨R_{2}) & ⌈A ∨ B⌉ & ∘− ⌈B⌉. \\ (∀_{c}L) & ⌊∀_{c}B⌋ & ∘− ⌊Bx⌋. & (∀_{c}R) & ⌈∀_{c}B⌉ & ∘− ∀x⌈Bx⌉. \\ (∃_{c}L) & ⌊∃_{c}B⌋ & ∘− ∀x⌊Bx⌋. & (∃_{c}R) & ⌈∃_{c}B⌉ & ∘− ⌈Bx⌉. \\ (f_{c}L) & ⌊f_{c}⌋ & ∘− ⊤. & (t_{c}R) & ⌈t_{c}⌉ & ∘− ⊤. \end{matrix}

Figure 5. LK_{0}: The introduction rules of LK with the ? dropped.

\begin{matrix}(⊃ L) & ⌊A ⊃ B⌋ & ∘− ⌈A⌉ ∘− ⌊B⌋. & (⊃ R) & ⌈A ⊃ B⌉ & ∘− ⌊A⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈B⌉. \\ (∩L_{1}) & ⌊A ∩ B⌋ & ∘− ⌊A⌋. & (∩R) & ⌈A ∩ B⌉ & ∘− ⌈A⌉ & ⌈B⌉. \\ (∩L_{2}) & ⌊A ∩ B⌋ & ∘− ⌊B⌋. & (∪R_{1}) & ⌈A ∪ B⌉ & ∘− ⌈A⌉. \\ (∪L) & ⌊A ∪ B⌋ & ∘− ⌊A⌋ & ⌊B⌋. & (∪R_{2}) & ⌈A ∪ B⌉ & ∘− ⌈B⌉. \\ (∀_{i}L) & ⌊∀_{i}B⌋ & ∘− ⌊Bx⌋. & (∀_{i}R) & ⌈∀_{i}B⌉ & ∘− ∀x⌈Bx⌉. \\ (∃_{i}L) & ⌊∃_{i}B⌋ & ∘− ∀x⌊Bx⌋. & (∃_{i}R) & ⌈∃_{i}B⌉ & ∘− ⌈Bx⌉. \\ (f_{i}L) & ⌊f_{i}⌋ & ∘− ⊤. & (t_{i}R) & ⌈t_{i}⌉ & ∘− ⊤. \end{matrix}

Figure 6. LJ_{0}: The introduction rules of LJ with the ? dropped.

(P os_{1}) ⌈B⌉ −∘!⌈B⌉.  (Neg_{1})  ⌊B⌋ −∘!⌊B⌋.
(P os_{2}) ⌊B⌋ ∘− ?⌊B⌋.  (Neg_{2})  ⌈B⌉ ∘− ?⌈B⌉.
(Cut)  ⊥ ∘− ⌊B⌋ ∘− ⌈B⌉.  (Initial) ⌊B⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈B⌉.

Figure 7. Some named formulas.

4.2. Modular presentations of classical and intuitionistic logics. The essential difference between the theories LJ and LK is the different set of occurrences of the ? modal. Consider the theories LK_{0} and LJ_{0} given in Figures 5 and 6. These result from removing the cut and initial rules as well as deleting from the introduction rules of the corresponding LK and LJ theories the ? modal. Define the two new theories

LJ′ = LJ_{0} ∪ {Cut, Initial, P os_{2}} and LK′ = LK_{0} ∪ {Cut, Initial, P os_{2}, Neg_{2}},

where the additional formulas are defined in Figure 7. While LJ′ is a strengthening of LJ, they can both prove the same object-level, intuitionistic sequents. Similarly for LK′ and LK.

Proposition 4.2. The following two correctness statements hold.

LINEAR LOGIC AS A FRAMEWORK FOR SPECIFYING SEQUENT CALCULUS 15

1. Let B_{0}, …, B_{n} (for n ≥ 0) be object-level, intuitionistic formulas. Then

Σ_{j}: LJ; ⟶ ⌈B_{0}⌉; ⌊B_{1}⌋, …, ⌊B_{n}⌋

has a F-proof if and only if Σ_{j}: LJ′; ⟶ ⌊B_{1}⌋, …, ⌊B_{n}⌋, ⌈B_{0}⌉; has a Fproof.

2. Let B_{1}, …, B_{n}, C_{1}, …, C_{m} (for n, m ≥ 0) be object-level, classical formulas. Then Σ_{c}: LK; ⟶; ⌊B_{1}⌋, …, ⌊B_{n}⌋, ⌈C_{1}⌉, …, ⌈C_{m}⌉ has a F-proof if and only if Σ_{c}: LK′; ⟶ ⌊B_{1}⌋, …, ⌊B_{n}⌋, ⌈C_{1}⌉, …, ⌈C_{m}⌉; has a F-proof.

Proof We prove the first of these cases since the second is similar.

A consequence of LJ′ is the equivalence ⌊B⌋ ≡ ?⌊B⌋. Thus we can rewrite the clauses of LJ′ into those of LJ by inserting the ? modal. Thus, assuming Σ_{j}: LJ; ⟶ ⌈B_{0}⌉; ⌊B_{1}⌋, …, ⌊B_{n}⌋ has a F-proof, we can use cut-elimination to conclude Σ_{j}: LJ′; ⟶ ⌈B_{0}⌉; ⌊B_{1}⌋, …, ⌊B_{n}⌋ has a F-proof. Using the P os_{2} clauses of LJ′ n-times, we can conclude that Σ_{j}: LJ′; ⟶ ⌊B_{1}⌋, …, ⌊B_{n}⌋, ⌈B_{0}⌉; has a F-proof.

To prove the converse, we prove the following lemma by induction on the height of proofs in Forum: Let L_{1} and L_{2} be multisets of left-atoms and let R be a rightatom. Then if Σ_{j}: LJ′; ⟶ R, L_{1}; L_{2} has a F-proof, then Σ_{j}: LJ; ⟶ R; L_{1}, L_{2} has a Forum proof. The proof proceeds by examining each case for how this sequent could be proved.

An immediate corollary of this Proposition and the correctness of LJ and LK is the correctness of LJ′ and LK′: namely, Σ_{j}: LJ′; ⟶ ⌊B_{1}⌋, …, ⌊B_{n}⌋, ⌈B_{0}⌉; has a F-proof if and only if the sequent B_{1}, …, B_{n} ⟶ B_{0} has an LJ-proof and Σ_{c}: LK′; ⟶ ⌊B_{1}⌋, …, ⌊B_{n}⌋, ⌈C_{1}⌉, …, ⌈C_{n}⌉; has an F-proof if and only if the sequent B_{1}, …, B_{n} ⟶ C_{1}, …, C_{n} has an LK-proof.

Notice that the inference rules for LJ_{0} and LK_{0} are identical except for a systematic renaming of logical constants. Thus one way to modularly describe the distinction between intuitionistic and classical logics is that the former logic assumes Pos_{2} while the latter logic assumes both Pos_{2} and Neg_{2}. This description amounts to saying that contraction is allowed on the right and left in classical proofs but only on the left in intuitionistic proofs.

4.3. Collapsing of modal prefixes. Note that the following equivalences are provable from the various encodings of proof systems:

1. The Cut and Initial rules of LL prove the equivalence ⌈B⌉ ≡ ⌊B⌋^{⊥}.

2. The Cut and Initial rules of LK prove the following equivalences: ⌈B⌉ ≡ ⌊B⌋^{⊥}, ?⌊B⌋ ≡ ⌊B⌋, ?⌈B⌉ ≡ ⌈B⌉, ?⌈B⌉ ≡ (?⌊B⌋)^{⊥}, ?⌈B⌉ ≡ !⌈B⌉, ?⌊B⌋ ≡ !⌊B⌋, !⌊B⌋ ≡ ⌊B⌋, and ?⌈B⌉ ≡ ⌈B⌉. As an example proof of such an equivalence, the Cut rule is equivalent to (?⌊B⌋)^{⊥} ∘− ?⌈B⌉. On the other hand,

\begin{matrix}\begin{matrix}{⌊B⌋ ⟶ ⌊B⌋ \atop ⌊B⌋ ⟶ ?⌊B⌋} & ⊥⟶⊥ \\ ⌊B⌋,?⌊B⌋−∘ ⊥⟶⊥ \end{matrix} & {⌈B⌉ ⟶ ⌈B⌉ \atop ⌈B⌉ ⟶ ?⌈B⌉} \\ ⌊B⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈B⌉,?⌊B⌋−∘ ⊥⟶ ?⌈B⌉ \end{matrix}

That is, the Initial rule implies (?⌊B⌋)^{⊥} −∘?⌈B⌉. Hence (?⌊B⌋)^{⊥} ≡ ?⌈B⌉ follows from them both.

3. The Cut and Initial rules of LJ prove the equivalences ⌈B⌉ ≡ (?⌊B⌋)^{⊥}, ⌈B⌉ ≡ !⌈B⌉, ⌊B⌋ ≡ ?⌊B⌋, and ⌈B⌉ ≡ ⌊B⌋^{⊥}.

Thus, the cut and initial rules show the (not surprising fact) that ⌊·⌋ and ⌈·⌉ are duals of each other. In the cases of LJ and LK, however, that duality also forces additional equivalences that cause the collapse of some of modals. As it is well known, linear logic has 7 distinct modalities, namely: the empty modality, !, ?, ? !, ! ?, ! ? !, and ? ! ?. Given the LK theory, however, all those modals collapse into just two when applied to a ⌊·⌋-atom or a ⌈·⌉-atom and in LJ, these modals collapse to four when applied to either the ⌈·⌉-atoms or the ⌊·⌋-atoms.

Such a collapse is certainly undesirable when specifications rely on proof search: we would like to have a lot of distinctions available to help us understanding how formulas are to be used within object-level proofs. It would be far more interesting to have proof systems for intuitionistic and classical logics, for example, in which these modals would not generally collapse. Recent advances in understanding sequent calculus for these logics provide just such proof systems. We illustrate some of them in Section 5.

4.4. Natural deduction. To illustrate an application of using meta-level reasoning to draw conclusions about an object-logic, we show how a specification for natural deduction in intuitionistic logic can be derived from a sequent calculus specification of intuitionistic logic. For simplicity, we consider a minimal logic fragment of intuitionistic logic involving only ⊃, ∩, and ∀_{i}: let LM be the subset of LJ from Figure 4 containing Cut, Initial, and introduction rules for those three connectives. (The disjoint sums are addressed in [23].)

Given the equivalences arising from the cut and initial rules in LJ listed in Section 4.3, the specification for (⊃ L) is equivalent to the following formulas.

?⌊B⌋ −∘ ⌈A⌉ −∘ ⌊A ⊃ B⌋ ≡ ⌊B⌋ −∘ ⌈A⌉ −∘ ⌊A ⊃ B⌋
≡ ⌈B⌉^{⊥} −∘ ⌈A⌉ −∘ ⌈A ⊃ B⌉^{⊥}
≡ ⌈A ⊃ B⌉ −∘ ⌈A⌉ −∘ ⌈B⌉

LINEAR LOGIC AS A FRAMEWORK FOR SPECIFYING SEQUENT CALCULUS 17

The later can be recognized as a specification of the ⊃ elimination rule. Similarly, the specification for (⊃ R) is equivalent to the following formulas.

?⌊A⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈B⌉ −∘ ⌈A ⊃ B⌉ ≡ ⌈A⌉^{⊥} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈B⌉ −∘ ⌈A ⊃ B⌉
≡ (! ⌈A⌉)^{⊥} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈B⌉ −∘ ⌈A ⊃ B⌉
≡ (⌈A⌉ ⇒ ⌈B⌉) −∘ ⌈A ⊃ B⌉

Continuing in such a manner, we can systematically replace all occurrences of ⌊·⌋ with occurrences of ⌈·⌉, as listed in Figure 8. The clauses in this figure, named NM, can easily be seen as specifying the introduction and elimination rules for this particular fragment of minimal logic. The usual specification of natural deduction rules for minimal logic [11, 16] has intuitionistic implications replacing the top-level linear implications in Figure 8, but as observed in [17], the choice of which implication to use for these top-level occurrences does not change the set of atomic formulas that are provable.

(⊃ I) ⌈A ⊃ B⌉ ∘− ⌈A⌉ ⇒ ⌈B⌉.  (⊃ E) ⌈B⌉ ∘− ⌈A⌉ ∘− ⌈A ⊃ B⌉.
(∀_{i}I) ⌈∀_{i}B⌉ ∘− ∀x⌈Bx⌉. (∀_{i}E) ⌈Bx⌉ ∘− ⌈∀_{i}B⌉.
(∩I) ⌈A ∩ B⌉ ∘− ⌈A⌉ & ⌈B⌉.  (∩E_{1}) ⌈A⌉ ∘− ⌈A ∩ B⌉.
(∩E_{2}) ⌈B⌉ ∘− ⌈A ∩ B⌉.

Figure 8. Specification of the NM natural deduction calculus.

As a result of this rather natural connection between clauses in LM and NM, the following Propositions have rather direct proofs (see [23] for details).

Proposition 4.3. ! LM ≡ ![(&NM) & Initial & Cut].

Proposition 4.4. If B is an object-level formula, then NM ⊢ ⌈B⌉ if and only if LM ⊢ ⌈B⌉.

As a consequence of the last Proposition and the correctness of representation of LM and NM, we can conclude that a formula B has a sequent calculus proof if and only if it has a natural deduction proof.

§5. More refined uses of modals. For the sake of presenting examples in this section, we shall consider the fragments of intuitionistic and classical logics that involve just implication and universal quantification. Gentzen’s LJ system for these two connectives is reproduced in Figure 9.

It is well known that proof search in the intuitionistic logic of these connectives can be focused, in the sense that left-introduction rules are only applied to a distinguished formula (such focusing is a justification for backchaining in

(⊃ L) ⌊A ⊃ B⌋ ∘− ⌈A⌉ ∘− ?⌊B⌋.  (⊃ R)  ⌈A ⊃ B⌉ ∘− ?⌊A⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈B⌉.
(∀_{i}L)  ⌊∀_{i}B⌋ ∘− ?⌊Bx⌋.  (∀_{i}R)  ⌈∀_{i}B⌉ ∘− ∀x⌈Bx⌉.
(Cut)  ⊥ ∘− ⌈A⌉ ∘− ?⌊A⌋.  (Initial) ⌊A⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈A⌉.

Figure 9. The {⊃, ∀_{i}}-fragment of LJ

logic programming). Danos et. al. [7] present the focused formulation of intuitionistic logic called ILU and displayed in Figure 10. Here, sequents have the form Π; Γ ⟶ A where Γ and Π denote multisets, and Π containing at most one formula. The ILU proof system can be encoded in Forum by representing such sequents as Σ: ·; · ⟶ ⌊Π⌋, ⌈A⌉; ⌊Γ⌋ and its inference rules as in Figure 11. (If Γ is a multiset or set of object-level formulas, we write ⌊Γ⌋ and ⌈Γ⌉ to be the corresponding multiset or set of meta-level formulas resulting from applying the corresponding predicate to all formulas in Γ.)

Proofs in ILU are focused in a sense that the left rules (⊃ L) and (∀_{i}L) can only be applied to formulas in the left linear context Π (in Forum, this is the ⌊·⌋-formula without the ?-modal prefix). This restriction, which is enforced using modals in the Forum encoding, constrains proof search significantly.

\overline{A; · ⟶ A} initial
\frac{Π; Γ_{1} ⟶ A A; Γ_{2} ⟶ B}{Π; Γ_{1}, Γ_{2} ⟶ B} head-cut  \frac{; Γ_{1} ⟶ A Π; A, Γ_{2} ⟶ B}{Π; Γ_{1}, Γ_{2} ⟶ B} mid-cut
\frac{Π; Γ ⟶ A}{Π; Γ, B ⟶ A} WL  \frac{Π; Γ, B, B ⟶ A}{Π; Γ, B ⟶ A} CL  \frac{B; Γ ⟶ A}{·; B, Γ ⟶ A} D

\frac{·; Γ ⟶ A B; Γ′ ⟶ C}{A ⊃ B; Γ, Γ′ ⟶ C} ⊃ L \frac{Π; Γ, A ⟶ B}{Π; Γ ⟶ A ⊃ B} ⊃ R

\frac{A[x/t]; Γ ⟶ B}{∀_{l}xA; Γ ⟶ B} ∀_{i}L \frac{Π; Γ ⟶ A[x/y]}{Π; Γ ⟶ ∀_{l}xA} ∀_{l}R

Figure 10. The sequent calculus ILU

(⊃ L) ⌊A ⊃ B⌋ ⇐ ⌈A⌉ ∘− ⌊B⌋.  (⊃ R)  ⌈A ⊃ B⌉ ∘− ?⌊A⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈B⌉.
(∀_{i}L)  ⌊∀_{i}B⌋ ⇐ ⌊Bx⌋.  (∀_{i}R)  ⌈∀_{i}B⌉ ∘− ∀x⌈Bx⌉.
(Head-cut)  ⊥ ∘− ⌈A⌉ ∘− ⌊A⌋. (Initial) ⌊A⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈A⌉.
(Mid-cut)  ⊥ ⇐ ⌈A⌉ ∘− ?⌊A⌋.

Figure 11. Specification of the calculus ILU

LINEAR LOGIC AS A FRAMEWORK FOR SPECIFYING SEQUENT CALCULUS 19

The two cut rules for ILU, head-cut and mid-cut, are encoded as two formulas in Figure 11 in such as way that the first implies the second: that is,

(⌊A⌋ −∘ ⌈A⌉−∘ ⊥) ⇒ (?⌊A⌋ −∘ ⌈A⌉ ⇒⊥).

is provable in linear logic. As a result, we shall refer to the head-cut as the cut rule. Observe that from the Cut and Initial rules of ILU, we can prove the equivalence ⌈B⌉ ≡ ⌊B⌋^{⊥} but we cannot prove any equivalences between linear logic modals. Note also that ILU is equivalent to the neutral fragment of intuitionistic implicational logic of LU (see Section 6), although it was formulated in order to obtain a sequent calculus for an inductive decoration strategy (see [7] for the definition) of intuitionistic logic into linear logic.

Two sequent calculi, LKQ and LKT, which provide a focused kind of proof system for classical logic are also presented in [7]. Sequents of the calculus LKQ (Figure 12), written as Γ ⟶ Δ; Π are encoded as Forum sequents Σ: ·; · ⟶ ⌈Π⌉; ⌊Γ⌋, ⌈Δ⌉ where Π represents a multiset containing at most one formula. Note that the rules are the same as the ones for the positive classical implicational fragment of LU (see Section 6) i.e., rules defined for positive formulas. However, LKQ cannot be identified with any proper fragment of LU since positive polarity is not preserved by the connectives ⇒ and ∀_{c}. Sequents of the LKT proof system (Figure 13), written as Γ ⟶ Δ; Π, are encoded as Σ: ·; · ⟶ ⌊Π⌋; ⌊Γ⌋, ⌈Δ⌉, where again Π is a multiset containing at most one formula. Observe that LKT is a classical equivalent of ILU; that is, the intuitionistic calculus is obtained from LKT by the usual restriction of having exactly one formula on the right side of the sequent. LKT is equivalent to the negative fragment of classical implicational logic of LU.

In both LKQ and LKT systems there is a collapse of modal prefixes:

1. The Cut and Initial rules of LKQ prove the equivalence ⌈B⌉ ≡ !⌈B⌉ and the modalities collapse to four when applied to ⌈·⌉-atoms. Thus, in LKQ the formula Pos_{1} holds.

2. The Cut and Initial rules of LKT prove the equivalence ⌊B⌋ ≡ !⌊B⌋ and the modalities collapse to four when applied to ⌊·⌋-atoms. Thus, in LKT the formula Neg_{1} holds.

We present one final example encoding of a proof system, by picking a system that deviates from the previous one in a few details. An optimized version of (the implicational fragment of) LJ is presented in Lincoln et. al. [19] (see also [9]). Their system, called IIL* (Figure 14) does not contain contraction or cut rules, and weakening is only allowed at the leafs of a proof; that is, when the Initial rule is applied (to atomic formulas). A key property of IIL* is that the principal formula is not duplicated in the premises of any of the rules. This

(⇒ L) ⌊A ⇒ B⌋ ⇐ ⌈A⌉ ⇐ ?⌊B⌋.  (⇒ R)  ⌈A ⇒ B⌉ ⇐ ?⌊A⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ?⌈B⌉.
(∀_{c}L)  ⌊∀_{c}B⌋ ⇐ ?⌊Bx⌋.  (∀_{c}R)  ⌈∀_{c}B⌉ ⇐ ∀x?⌈Bx⌉.
(Cut)  ⊥ ∘− ⌈A⌉ ∘− ?⌊A⌋. (Initial) ⌊A⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈A⌉.
⊥ ∘− ?⌈A⌉ ⇐ ?⌊A⌋.

Figure 12. The calculus LKQ

(⇒ L) ⌊A ⇒ B⌋ ⇐ ?⌈A⌉ ∘− ⌊B⌋. (⇒ R)  ⌈A ⇒ B⌉ ∘− ?⌊A⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ?⌈B⌉.
(∀_{c}L) ⌊∀_{c}B⌋ ⇐ ⌊Bx⌋. (∀_{c}R) ⌈∀_{c}B⌉ ∘− ∀x?⌈Bx⌉.
(Cut)  ⊥ ∘− ?⌈A⌉ ∘− ⌊A⌋. (Initial) ⌊A⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈A⌉.
⊥ ⇐ ?⌈A⌉ ∘− ?⌊A⌋.

Figure 13. The calculus LKT

(Initial)  ⌊A⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈A⌉ ∘− ⊤ ∘− atomic(A).
(⊃ R)  ⌈B ⊃ C⌉ ∘− ⌈B⌉ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌊C⌋.
(⊃ 1L)  ⌊A ⊃ B⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈D⌉ ∘− ⌈A⌉ & (⌊B⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈D⌉) ∘− atomic(A).
(⊃ 2L) ⌊(A ⊃ B) ⊃ C⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈D⌉ ∘− (⌊B ⊃ C⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈A ⊃ B⌉) & (⌊C⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈D⌉).

Figure 14. The calculus IIL* where atomic(·) is a predicate of type bool → o defined to hold for all atomic formulas.

suggests the encoding Σ: ·; · ⟶ ⌈D⌉, ⌊Γ⌋; · for the IIL* sequent Γ ⟶ D. It also requires encoding the Initial and ⊃ L rules differently than we have seen so far: the Initial rule uses the additive true, ⊤, to allow weakening, and the ⊃ L rules uses the additive conjunction, &, to copy the left context and uses a two headed clause so that the right context is not copied but is placed in the correct sequent of the premise.

§6. Using polarities in proof systems. In [14], Girard introduced the sequent system LU (logic of unity) in which classical, intuitionistic, and linear logics appear as fragments. In this logic, all three of these logics keep their own characteristics but they can also communicate via formulas containing connectives mixing these logics. The key to allowing these logics to share one proof system lies in using polarities. In terms of the encoding we have presented here, this corresponds to restricting the use of Pos_{2} and Neg_{2} rules to positive and negative formulas respectively and to split the rules for classical, intuitionistic, and linear connectives into cases, depending on the polarities of the subformulas involved.

LINEAR LOGIC AS A FRAMEWORK FOR SPECIFYING SEQUENT CALCULUS 21

We proceed to encode LU into Forum as follows. The LU sequent Γ; Γ′ ⟶ Δ′; Δ is encoded as the Forum sequent

Σ: ·; · ⟶ ⌊Γ⌋, ⌈Δ⌉; ⌊Γ′⌋, ⌈Δ′⌉.

(Notice the different convention used between LU sequents and Forum sequents with regard to which zones in a sequent allow structural rules.) To encode the polarity of object-level, LU formulas, we introduce three meta-level predicates, pos(·), neg(·), and neu(·), all of type bool → o. We can now encode the Identity and Structure rules on [14, page 206]. The Cut and Initial rules are encoded just as in linear logic. The Cut_{2} and Cut_{3} rules are, respectively,

⊥∘− ?⌈B⌉ ⇐ ⌊B⌋  and  ⊥⇐ ⌈B⌉ ∘− ?⌊B⌋.

Both of these formulas, however, are consequences of the Cut rule and are not needed in our encoding of LU. Similarly, the first structural rules are all simple consequences of using exponentials in encoding sequents. Finally, the fact that structural rules are allowed for positive and negative formulas is given as

\begin{matrix}(Neg) & ⌈N⌉ & ∘− ?⌈N⌉ ⇐ neg(N). \\ (P os) & ⌊P ⌋ & ∘− ?⌊P ⌋ ⇐ pos(P). \end{matrix}

Notice that if we use Cut and Initial to eliminate, say, ⌊·⌋ for ⌈·⌉ (as we did in Section 4.4), then the only non-trivial inference rules among those coding Identity and Structure rules in this presentation of LU are the (Neg) and (P os) rules.

The calculus for linear connectives in LU is equivalent to the usual one (see Fig. 2) and the rules do not depend on the polarities. Figure 15 specifies some polarities for classical and intuitionistic connectives (polarities for linear logic connectives can be given similarly). Many of the LU inference rules for classical and intuitionistic connectives are specified in Figure 16. The full encoding of the LU proof system is not given here, but most of it is contained in the union of the clauses in Figures 2, 15, and 16. Observe that the use of Forum to encode the LU proof system provides a reduced set of rules (compare e.g. 8 disjunction rules versus 24 that appear in [14]). Compaction is due partially to the fact that if B is positive then ⌈B⌉ ≡ !⌈B⌉ and ⌊B⌋ ≡ ?⌊B⌋ and if B is negative then ⌈B⌉ ≡ ?⌈B⌉ and ⌊B⌋ ≡ !⌊B⌋ (thus the expression A ⇐ ⌊B⌋ might also be equivalent to A ∘− ⌊B⌋). Further compaction occurs by departing from Forum syntax slightly and allowing occurrences of ⊕ and ! in the body of clauses. Such occurrences can be easily removed to form Forum clauses: for example, the formula (a ⊕! b) −∘ c is logically equivalent to (a −∘ c) & (b ⇒ c).

notpos(B) ⇐ neg(B) ⊕ neu(B).
notneg(B) ⇐ pos(B) ⊕ neu(B).
notneu(B) ⇐ pos(B) ⊕ neg(B).
pos(A ∧ B) ⇐ pos(A).
pos(A ∧ B) ⇐ pos(B).
neg(A ∧ B) ⇐ neg(A) ⇐ neg(B).
neg(A ∨ B) ⇐ neg(A).
neg(A ∨ B) ⇐ neg(B).
pos(A ∨ B) ⇐ notneg(A) ⇐ notneg(B).
neg(A ⇒ B) ⇐ pos(A).
neg(A ⇒ B) ⇐ neg(B).
pos(A ⇒ B) ⇐ notpos(A) ⇐ notneg(B).
neg(A ⊃ B) ⇐ neg(B).
neg(∀_{c}B).
pos(∃_{c}B).
neu(A ∧ B) ⇐ neu(A) ⇐ neu(B).
neu(A ∧ B) ⇐ neu(A) ⇐ neg(B).
neu(A ∧ B) ⇐ neg(A) ⇐ neu(B).
neu(A ⇒ B) ⇐ notneg(B).

Figure 15. Positive and negative polarities for intuitionistic and classical logic. See Table 2 in [14].

§7. Automation of proof systems. Since the specifications of proof systems are given as clauses in Forum and since Forum can be seen as an abstract logic programming language in the sense of [24], it is natural to ask if it is possible to turn these specifications into implementations.

One might attempt to do this using one of the available implementations of Forum [18, 20, 31]. It is, however, a simple matter to turn the specification of Forum given in Figure 1 into a naive interpreter using a logic programming language such as λProlog [25]. We will not present the details of such an implementation except to describe three aspects of it. First, it can be structured such that one inference rule in Figure 1 is translated to one λProlog clause: the resulting implementation is thus rather compact and declarative. Second, the quantification and substitution aspects of the object-logics can be captured directly using λProlog’s higher-order features: using a first-order logic programming language such as Prolog would have complicated the implementation significantly. Third, a counter can be used in the clauses of this interpreter to count the number of times a decide! or a decide rule is used along a particular Forum proof branch.

Identity and structure ⌊B⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈B⌉.

⊥ ∘− ⌊B⌋ ∘− ⌈B⌉.
⌈N⌉ ∘− ?⌈N⌉ ⇐ neg(N).
⌊P ⌋ ∘− ?⌊P ⌋ ⇐ pos(P).

Conjunction

⌈u ∧ v⌉ ⇐ ⌈u⌉ ⇐ ⌈v⌉  ⇐ pos(u) ⊕ pos(v).
⌈u ∧ v⌉ ∘− ⌈u⌉ & ⌈v⌉  ⇐ notpos(u) ⇐ notpos(v).
⌊u ∧ v⌋ ∘− ?⌊u⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ?⌊v⌋  ⇐ pos(u) ⊕ pos(v).
⌊u ∧ v⌋ ∘− ⌊u⌋ ⊕ ⌊v⌋  ⇐ notpos(u) ⇐ notpos(v).

Intuitionistic implication

⌈u ⊃ v⌉ ∘− ?⌊u⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈v⌉.
⌊u ⊃ v⌋ ⇐ ⌈u⌉ ∘− ⌊v⌋.

Quantifiers

⌈∀_{c}u⌉ ∘− ∀x?⌈ux⌉.
⌊∀_{c}u⌋ ⇐ ⌊ux⌋.
⌈∃_{c}u⌉ ⇐ ⌈ux⌉.
⌊∃_{c}u⌋ ∘− ∀x?⌊ux⌋.

Disjunction

⌈u ∨ v⌉ ∘− !⌈u⌉ ⊕!⌈v⌉  ⇐ notneg(u) ⇐ notneg(v).
⌈u ∨ v⌉ ∘− ?⌈u⌉ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ?⌈v⌉  ⇐ (pos(u) & neg(v)) ⊕ (neg(u) & notneu(v)).
⌈u ∨ v⌉ ∘− ⌈u⌉ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ? !⌈v⌉  ⇐ neg(u) ⇐ neu(v).
⌈u ∨ v⌉ ∘− ? !⌈u⌉ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⌈v⌉  ⇐ neu(u) ⇐ neg(v).
⌊u ∨ v⌋ ∘− ?⌊u⌋ & ?⌊v⌋  ⇐ notneg(u) ⇐ notneg(v).
⌊u ∨ v⌋ ⇐ ⌊u⌋ ⇐ ⌊v⌋  ⇐ (pos(u) & neg(v)) ⊕ (neg(u) & notneu(v)).
⌊u ∨ v⌋ ∘− ⌊u⌋ ⇐ ?⌊v⌋  ⇐ neg(u) ⇐ neu(v).
⌊u ∨ v⌋ ⇐ ?⌊u⌋ ∘− ⌊v⌋  ⇐ neu(u) ⇐ neg(v).

Classical implication

⌈u ⇒ v⌉ ∘− ?⌊u⌋ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ?⌈v⌉  ⇐ (neg(u) & neg(v)) ⊕ (pos(u) & notneu(v)).
⌈u ⇒ v⌉ ∘− ⌈v⌉ ⊕ ⌊u⌋  ⇐ neg(u) ⇐ pos(v).
⌊u ⇒ v⌋ ∘− ⌈u⌉ & ⌊v⌋  ⇐ neg(u) ⇐ pos(v).
⌊u ⇒ v⌋ ⇐ ⌈u⌉ ⇐ ⌊v⌋  ⇐ (neg(u) & neg(v)) ⊕ (pos(u) & notneu(v)).

Figure 16. LU rules

This counter can be used to limit the size of object-level proofs that are searched and in this way, the search for object-level proofs can be controlled in a simple fashion. In general, object-level proofs can be arbitrarily large, so setting a counter such as this is certainly not a complete proof strategy. It is the case,

24 DALE MILLER AND ELAINE PIMENTEL

however, that if there is a proof of height h in the object-level, then the interpreter will find a proof if the counter is set to this value. For a number of proofs that we claim below, the value of this counter is often rather small.

To use this prover to prove object-level formulas, one would initialize the prover with the encoding of an object-level proof system and the encoding of the objectlevel formula. For example, attempting to prove the Forum sequent LK ⇒ ⌈B⌉ for some object-level classical logic formula B would correspond to attempting to prove B using the rules of the classical sequent calculus LK. In particular, the single formula intended as LK is the &-conjunction of the universal closure of the clauses listed in Figure 3.

This prover can also be used determine if one collection of inference rules linearly entail other inference rules and equivalences. In particular, all the following can be proved automatically by setting the counter mentioned above to the value 3.

1. The clauses in Figure 3 encoding LK entails the clauses in Figure 4 encoding LJ, at least when these set of clauses are rewritten to use the same set of object-level constants.

2. The clauses in Figure 9 encoding a fragment of LJ entails the clauses in Figure 11 encoding the focused version of LJ called ILU.

3. The forward direction of Proposition 4.3 is easily proved: ⊢ LM ⇒ NM.

4. All the equivalences mentioned in Section 4.3 that arise from the different cut and initial rules used in linear, intuitionistic, and classical logics have simple proofs.

Of course, if such entailments hold, they have immediate consequences for the object-logics that they encode. For example, from the first point above, we know that any (object-level) formula provable in ILU is also provable in LJ.

§8. Conclusion and future work. In this paper, we showed one way that linear logic can be used to specify some sequent calculus proof systems. We presented several examples of such an encoding and argued that such meta-logical encodings can have numerous advantages over the more standard inference figure approach. Since the encodings of the object-level proof systems are natural and direct, the rich meta-theory of linear logic can be used to draw conclusions about object-level proof systems. Because the object-level encodings result in logic programs (in the sense of Forum), the proof systems mentioned in this paper can be easily implemented and some of their properties can be automatically checked.

There is clearly much more to do now that the feasibility of using linear logic in this specification task is clear.

LINEAR LOGIC AS A FRAMEWORK FOR SPECIFYING SEQUENT CALCULUS 25

We have not discussed how proof objects can be specified in this setting: adding λ-calculus representations of calculi with natural deduction proofs can probably be done as it is done using an intuitionistic logic meta-theory [10] but such “single-conclusion” proofs would not work in the general sequent calculus setting.

There have been various proposals for non-commutativity variants of classical linear logic [1, 15, 29]: it would be interesting to see if these can be used to capture non-commutative object-level logics in a manner done here.

One reason to use a well understood meta-logic for specification is that it should offer ways to automate many things about inference rules. For example, it seems quite likely that the question whether or not one proof system’s encoding linearly entails another proof system’s encoding should be decidable, at least in many cases. It is also likely that at least important parts of the proof of cutelimination for the encoded logic might similarly be automated.

Finally, most interesting proofs that relate provability in two proof systems generally require induction. It seems natural to consider adding to linear logic forms of induction along the lines found in [21, 28].

Acknowledgments. Miller has been funded in part by NSF grants CCR-9803971, INT-9815645, and INT-9815731. Pimentel has been funded by CAPES grant BEX0523/99-2. Pimentel was a visitor at Penn State from September 1999 to January 2001.

REFERENCES

[1] V. Michele Abrusci and Paul Ruet, Non-commutative logic I: The multiplicative fragment, Annals of Pure and Applied Logic, vol. 101 (1999), no. 1, pp. 29–64.

[2] Jean-Marc Andreoli, Logic programming with focusing proofs in linear logic, Journal of Logic and Computation, vol. 2 (1992), no. 3, pp. 297–347.

[3] Michele Bugliesi, Giorgio Delzanno, Luigi Liquori, and Maurizio Martelli, A linear logic calculus of objects, Proceedings of the Joint International Conference and Symposium on Logic Programming (M. Maher, editor), MIT Press, September 1996.

[4] Manuel M. T. Chakravarty, On the massively parallel execution of declarative programs, Ph.D. thesis, Technische Universität Berlin, Fachbereich Informatik, February 1997.

[5] Jawahar Chirimar, Proof theoretic approach to specification languages, Ph.D. thesis, University of Pennsylvania, February 1995.

[6] Alonzo Church, A formulation of the simple theory of types, The Journal of Symbolic Logic, vol. 5 (1940), pp. 56–68.

[7] Vicent Danos, Jean-Baptiste Joinet, and Harold Schellinx, LKQ and LKT: sequent calculi for second order logic based upon dual linear decompositions of classical implication, Workshop on linear logic (Girard, Lafont, and Regnier, editors), London Mathematical Society Lecture Notes 222, Cambridge University Press, 1995, pp. 211–224.

[8] Giorgio Delzanno and Maurizio Martelli, Objects in Forum, Proceedings of the International Logic Programming Symposium, 1995.

[9] Roy Dyckhoff, Contraction-free sequent calculi for intuitionistic logic, The Journal of Symbolic Logic, vol. 57 (1992), no. 3, pp. 795–807.

[10] Amy Felty, A logic program for transforming sequent proofs to natural deduction proofs, Extensions of Logic Programming: International Workshop, Tübingen (Peter Schroeder-Heister, editor), LNAI, vol. 475, Springer-Verlag, 1991, pp. 157–178.

[11] Amy Felty and Dale Miller, Specifying theorem provers in a higher-order logic programming language, Ninth International Conference on Automated Deduction (Argonne, IL), Springer-Verlag, May 1988, pp. 61–80.

[12] Gerhard Gentzen, Investigations into logical deductions, The Collected Papers of Gerhard Gentzen (M. E. Szabo, editor), North-Holland Publishing Co., Amsterdam, 1969, pp. 68–131.

[13] Jean-Yves Girard, Linear logic, Theoretical Computer Science, vol. 50 (1987), pp. 1–102.

[14] , On the unity of logic, Annals of Pure and Applied Logic, vol. 59 (1993), pp. 201–217.

[15] Alessio Guglielmi and Lutz Straßburger, Non-commutativity and MELL in the calculus of structures, CSL 2001 (L. Fribourg, editor), LNCS, vol. 2142, 2001, pp. 54–68.

[16] Robert Harper, Furio Honsell, and Gordon Plotkin, A framework for defining logics, Journal of the ACM, vol. 40 (1993), no. 1, pp. 143–184.

[17] Joshua Hodas and Dale Miller, Logic programming in a fragment of intuitionistic linear logic, Information and Computation, vol. 110 (1994), no. 2, pp. 327–365.

[18] Joshua Hodas, Kevin Watkins, Naoyuki Tamura, and Kyoung-Sun Kang, Efficient implementation of a linear logic programming language, Proceedings of the 1998 Joint International Conference and Symposium on Logic Programming (Joxan Jaffar, editor), 1998, pp. 145 – 159.

[19] Patrick Lincoln, Andre Scedrov, and Natarajan Shankar, Linearizing intuitionistic implication, Annals of Pure and Applied Logic, 1993, pp. 151–177.

[20] P. López and E. Pimentel, The UMA Forum linear logic programming language, implementation, January 1998.

[21] Raymond McDowell and Dale Miller, Cut-elimination for a logic with definitions and induction, Theoretical Computer Science, vol. 232 (2000), pp. 91–119.

[22] Dale Miller, The π-calculus as a theory in linear logic: Preliminary results, Proceedings of the 1992 Workshop on Extensions to Logic Programming (E. Lamma and P. Mello, editors), LNCS, no. 660, Springer-Verlag, 1993, pp. 242–265.

[23] , Forum: A multiple-conclusion specification language, Theoretical Computer Science, vol. 165 (1996), no. 1, pp. 201–232.

[24] Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov, Uniform proofs as a foundation for logic programming, Annals of Pure and Applied Logic, vol. 51 (1991), pp. 125–157.

[25] Gopalan Nadathur and Dale Miller, An Overview of λProlog, Fifth International Logic Programming Conference (Seattle), MIT Press, August 1988, pp. 810–827.

[26] Lawrence C. Paulson, The foundation of a generic theorem prover, Journal of Automated Reasoning, vol. 5 (1989), pp. 363–397.

[27] Frank Pfenning, Elf: A language for logic definition and verified metaprogramming, Fourth Annual Symposium on Logic in Computer Science (Monterey, CA), June 1989, pp. 313–321.

[28] Elaine Gouvêa Pimentel, Lógica linear e a especificação de sistemas computacionais, Ph.D. thesis, Universidade Federal de Minas Gerais, Belo Horizonte, M.G., Brasil, December 2001 (written in English).

[29] Christian Retoré, Pomset logic: a non-commutative extension of classical linear logic, Proceedings of TLCA, vol. 1210, 1997, pp. 300–318.

[30] Giorgia Ricci, On the expressive powers of a logic programming presentation of linear logic (FORUM), Ph.D. thesis, Department of Mathematics, Siena University, December 1998.

[31] Christian Urban, Forum and its implementations, Master’s thesis, University of St. Andrews, December 1997.

E-mail: dale@cse.psu.edu

COMPUTER SCIENCE AND ENGINEERING, 220 POND LAB, PENNSYLVANIA STATE UNIVERSITY, UNIVERSITY PARK, PA 16802-6106 USA

E-mail: pimentel@dcc.ufmg.br

DEPARTAMENTO DE CIÊNCIA DA COMPUTAÇÃO, UNIVERSIDADE FEDERAL DE MINAS GERAIS, BELO HORIZONTE, M.G. BRASIL