A Computational Interpretation of Modal Proofs

Simone Martini Andrea Masini ^{∗}

Abstract

The usual (e.g. Prawitz’s) treatment of natural deduction for modal logics involves a complicated rule for the introduction of the necessity, since the naive one does not allow normalization. We propose natural deduction systems for the positive fragments of the modal logics K, K4, KT, and S4, extending previous work by Masini on a two-dimensional generalization of Gentzen’s sequents (2sequents). The modal rules closely match the standard rules for an universal quantifier and different logics are obtained with simple conditions on the elimination rule for □. We give an explicit term calculus corresponding to proofs in these systems and, after defining a notion of reduction on terms, we prove its confluence and strong normalization.

1. Introduction

The proof theoretical approach has been proved of valuable importance in several computer science areas. The functional programming field, for instance, has received a good momentum from the so-called Curry-Howard isomorphism, the observation that typed functional programs can be considered as (and, in fact, are the same thing as) natural deduction proofs of the formulas corresponding to their types. Theories already well developed by their own sake — normalization, confluence, type inference, denotational semantics, category theory, to name just a few of them — could then merge together, suggesting new sound extensions to existing languages and guiding the design of new systems and new implementations. The leading example here is the language Standard ML [MTH90], whose design has been inspired by proof theory from scratch, but we can think also of CAML, the ML dialect developed in Paris [CCM85], whose (efficient) implementation is directly derived from the categorical semantics of natural deduction intuitionistic proofs, or of the several laboratory languages (both for programming and program verification) derived from higher order logic, e.g. [Con86, PHH93].

Also the logic programming field, whose evolution has been mainly driven by model theoretic issues (with the exception of resolution-related matters, of course) has recently discovered that a sound and deep rooting in proof theory can offer a key insight for the design of good, well balanced extensions to the paradigm. The work of Miller et al. [MNPS91], relating resolution to the search for suitable “uniform” proofs in extensions of Horn logic, or of Andreoli and Pareschi [AP90], connecting logic programming and linear logic, are paradigmatic of this trend.

The mathematical theory of concurrency, finally, has also drawn off ideas, techniques and systems from proof theory: both the π-calculus of Milner [MPW89], and the concurrent rewriting logic of Meseguer [Mes92] — once again to name just two recent papers — are proof theoretical in spirit and matter.

The situation is very different for the applications of modal logics. The pioneering work in this field is due to Pnueli [Pnu77], whose basic idea (and, in fact, of most of the papers on this topic) was to make the modal quantifier □ range over computations of concurrent systems. In this way the formula □σ would assert that the property σ has to be true in each state of each possible computation.

Following this approach, and depending on the kind of observations one allows over a computation, a large variety of modal logics (usually called “temporal logics” in computer science) have been proposed. It is interesting to observe that all of them are essentially multimodal logics obtained by combining in a suitable way the well known modal systems K, KD, T, S4, S5.

∗Dipartimento di Informatica Università di Pisa Corso Italia, 40 I-56125 Pisa Italy {martini,masini}@di.unipi.it

A quick analysis of the literature shows that all these logics have been introduced and studied following an approach à la Hilbert: a logic is characterized by the class of its models, which, in turn, is characterized by a set of axioms. Since any application of a formalism reflects the features of that formalism, it is no wonder that most applications of modal logics are based on their model theory (think, for instance, to the technique of model checking [EH85, MMS92]).

However, if model theory is a rich and developed field, the same is not true for modal proof theory, thus explaining the lack of applications of this kind. Proof theory of modal logics, though largely studied since the fifties, has always been a delicate subject, the main reason being the apparent impossibility to obtain elegant, natural systems for intensional operators (with the excellent exception of intuitionistic logic). For example Segeberg, not earlier than 1984 [BS84], observed that the Gentzen format, which works so well for truth functional and intuitionistic operators, cannot be a priori expected to remain valid for modal logics; carrying to the limit this observation one could even assert that “logics with no good proof theory are innatural.” In such a way we should mark as “innatural” all modal logics (with great delight of a large number of logicians!).

One of the main drawbacks of modal proof theory is well exemplified, in the context of the logics K, KT, and KD, by Scott’s sequent rule:

{Γ ⊢ σ \atop □Γ ⊢ □σ} .

This rule, though allowing the proof of a cut elimination theorem, is neither a left nor a right rule, thus destroying the deep symmetries of the sequent calculus. The situation is even worse with the natural deduction formulation of the same logics, where either there are no explicit modal introduction and elimination rules, as in [BS84], or the rule is formulated as

□Γ [Γ] ; \begin{matrix}· \\ · \\ · \end{matrix} ; σ ; □K ; □σ

which is neither an introduction nor an elimination rule and in which the same formula(s) appear in the premise twice, one boxed and once unboxed.

The situation is somehow better for S4, with reasonable sequent rules,

Γ, τ ⊢ σ ; □ ⊢ ; Γ, □τ ⊢ σ  □Γ ⊢ σ ; ⊢ □ ; □Γ ⊢ □σ

but, once again, problematic natural deduction. The sequent rules appear strictly related to those for the universal quantifier, and following this analogy Prawitz [Pra65] attempted the definition of a natural deduction system styled after the first order system. This naive approach, however, does not work, and in order to obtain normalization, Prawitz was forced to introduce more elaborated concepts and rules (see Section 4.1.).

In the last few years, however, it has been discovered by several authors that the difficulty was in a too strict interpretation of the “Gentzen format” and that several extensions [Dos85, BM92, GdQ92, Mas92, Mas93] allow a good and “natural” proof theory for modal logics.

We will focus here on the proposal by the second author for the logic KD, whose main idea is a two-dimensional generalization of the notion of sequent. Instead of asserting provability (⊢) between two sequences of formulas, provability is asserted between two-dimensional sequences of formulas.

Developed in [Mas92] as a sequent calculus for classical KD, in [Mas93] the approach is tailored to the intuitionistic framework, for which it is also given an equivalent natural deduction system.

The goal of the present paper is to study the computational properties of the system in [Mas93] and of several extensions to other logics, namely the positive fragments of K4, KT, and S4.

To this aim, we introduce first a complete natural deduction system for each of the logics at hand. All the rules of these systems are local (they act only on the conclusions of the deductions they are applied to), no introduction rule has a premise containing the introduced connective (as it is case for rule □K, for instance), and the modal rules strictly match the standard rules for an universal quantifier, the side conditions on variables becoming a side condition on levels.

One the main features of the approach is its scalability, the various logics differring only in one parameter of the elimination rule for □. This allows both a compact treatment and the study of the “fine structure” of the □ modality (that is, how several sublogics interact to obtain a larger logic, in this case S4).

By defining a suitable notion of reduction on the terms representing proofs (extending standard β-reduction for λ-terms), we obtain a natural computational interpretation for proofs, which is proved strongly normalizing and confluent.

Finally, this local, two dimensional approach enforces remarkable global properties of the resulting deductions. Though this is not the main subject of the paper, in Section 4.1. we will show that all deductions in our system for S4, in fact satisfy Prawitz’ global requirements on proofs, thus giving an immediate forgetful translation of our system in Prawitz’ one.

2. Systems

Before introducing formally the systems we will deal with, we briefly, and informally recall the natural deduction approach taken in [Mas93]. Let us denote formulas with lowercase greek letters α, β, σ, …, and sequences of formulas with lowercase gothic letters 𝔖, 𝔅, …, while ε will be the empty sequence. An intuitionistic 2-sequent is a two dimensional expression of the form

\begin{matrix}𝔖_{1} & & ε \\ 𝔖_{2} & & ε \\ ⋮ & ⊢ & ⋮ \\ 𝔖_{k} & & σ \end{matrix}  (1)

whose intended meaning is the formula

⋀ 𝔖_{1} ⊃ □(⋀ 𝔖_{2} ⊃ … □(⋀ 𝔖_{k} ⊃ σ) …).

Note that the formula σ, the conclusion of the deduction, lies at a level, k, which is greater than, or equal to, the level of any assumption it depends on (any of the 𝔖_{j}’s may be empty, of course). The propositional rules act over these two dimensional stuctures in the expected way, just “respecting the levels”. The rules for ⊃, for instance, can be expressed as:

\begin{matrix}𝔖_{1} & & ε \\ 𝔖_{2} & & ε \\ ⋮ & ⊢ & ⋮ \\ 𝔖_{k}, σ & & τ \end{matrix} ; ⊃I ; \begin{matrix}𝔖_{1} & & ε \\ 𝔖_{2} & & ε \\ ⋮ & ⊢ & ⋮ \\ 𝔖_{k} & & σ ⊃ τ \end{matrix}  \begin{matrix}𝔖_{1} & & ε \\ 𝔖_{2} & & ε \\ ⋮ & ⊢ & ⋮ \\ 𝔖_{k} & & σ ⊃ τ \end{matrix}  \begin{matrix}𝔅_{1} & & ε \\ 𝔅_{2} & & ε \\ ⋮ & ⊢ & ⋮ \\ 𝔅_{k} & & σ \end{matrix} ; ⊃E ; \begin{matrix}𝔖_{1}, 𝔅_{1} & & ε \\ 𝔖_{2}, 𝔅_{2} & & ε \\ ⋮ & ⊢ & ⋮ \\ 𝔖_{k}, 𝔅_{k} & & τ \end{matrix}

Formulas may change their level only by means of modal rules:

\begin{matrix}𝔖_{1} & & ε \\ 𝔖_{2} & & ε \\ ⋮ & ⊢ & ⋮ \\ 𝔖_{k} & & ε \\ ε & & σ \end{matrix} ; □I ; \begin{matrix}𝔖_{1} & & ε \\ 𝔖_{2} & & ε \\ ⋮ & ⊢ & ⋮ \\ 𝔖_{k} & & □σ \end{matrix}  \begin{matrix}𝔖_{1} & & ε \\ 𝔖_{2} & & ε \\ ⋮ & ⊢ & ⋮ \\ 𝔖_{k} & & □σ \end{matrix} ; □E ; \begin{matrix}𝔖_{1} & & ε \\ 𝔖_{2} & & ε \\ ⋮ & ⊢ & ⋮ \\ 𝔖_{k} & & ε \\ ε & & σ \end{matrix}

Thus, the only way to introduce a modality on a formula occurrence σ at level k is that σ is the only formula present at that level. As a result of the rule, the introduced formula is lifted one level up. Vice versa, the elimination rule pushes a formula down one level (but there is no restriction on its premise). The levels thus represent in the calculus a notion of modal dependence: the conclusion σ at level k modally depends on the assumptions at the same level. If there are not any such assumption, than we are allowed to assert the σ is necessary.

As proved in [Mas93], the given rules for □ characterize the minimal normal modal logic K.^{1} In this paper we will extend this approach to a class of modal logics based on K, KT, K4, S4, focusing on the computational aspects of the resulting proofs.

Before going into the details of the systems, we adopt a more compact representation for 2sequents. Instead of writing two-dimensional judgements, we will denote each formula σ at level k with σ^{k} and write the judgment (1) as Γ ⊢ σ^{k}, where

Γ = 𝔖_{1} ; 𝔖_{2} ; ⋮ ; 𝔖_{k}

will be seen as a multiset {τ_{1}^{i_{1}}, …, τ_{n}^{i_{n}}}. The usefulness of this representation will be especially clear in Section 5. The reader should always bear in mind, however, that the indexes on formulas are only a metatheoretical notation for two dimensional structures.

2.1. Basic definitions

Formally, formulas are built out of atoms (ranged over by p); compound formulas are obtained with the connectives: □ (unary), ∧ and ⊃ (binary). Any formula of the calculus will be marked with a level index, varying in ℕ^{+}; an indexed formula σ of level i will be written σ^{i}.

The following definition will introduce a calculus of terms and formulas, such that to any term M there will correspond a unique indexed formula σ^{i}, called its type; this fact will be denoted with M : σ^{i}. For any indexed formula σ^{i} we assume the existence of a numberable set {x_{1}^{i}, x_{2}^{i}, …} of variables of type σ^{i}. A set of assumptions (called sometimes also a basis, or a context) is a set Γ = {x_{1}^{i_{1}} : σ_{1}^{i_{1}}, …, x_{n}^{i_{n}} : σ_{n}^{i_{n}}}, where all the variables are different: if x^{k} : σ^{k} ∈ Γ and x^{h} : τ^{h} ∈ Γ, then σ^{k} = τ^{h} (and in particular k = h). No variable name, hence, can appear in a set of assumptions with two different levels; we will refer to this as to the level variable convention. For such a set of assumptions Γ, define #Γ = max{k_{j} | x_{k}^{k_{j}} : σ_{k}^{k_{j}} ∈ Γ}; #Γ = 0 when Γ is empty.

1More precisely, [Mas93] introduces a system for the minimal deontic normal modal logic KD, that in absence of negation and ◇ is equivalent to K.

Moreover, Γ^{<i} = {x^{k} : σ^{k} ∈ Γ | k < i}; the set Γ^{≥i} is defined analogously. Finally, for n ∈ ℤ, Γ(n) = {x^{k+n} : σ^{k+n} | x^{k} : σ^{k} ∈ Γ}.

Definition 2.1. [Calculus λ^{ℓ}] Terms and derivations are inductively defined by the following rules.

x^{k} : σ^{k}

\begin{aligned}Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; M : σ^{k} & Δ ; \begin{matrix}· \\ · \\ · \end{matrix} ; N : τ^{k} \\ & ∧I \\ ⟨M, N⟩^{k} : σ ∧ τ^{k} \end{aligned}  Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; M : σ ∧ τ^{k} ; ∧E_{l} ; (fst M)^{k} : σ^{k}  Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; M : σ ∧ τ^{k} ; ∧E_{r} ; (snd M)^{k} : τ^{k}

Γ [x^{k} : σ^{k}] ; \begin{matrix}· \\ · \\ · \end{matrix} ; M : τ^{k} ; ⊃I ; (λx^{k}:σ^{k}.M)^{k} : σ ⊃ τ^{k}  \begin{aligned}Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; M : σ ⊃ τ^{k} & Δ ; \begin{matrix}· \\ · \\ · \end{matrix} ; N : σ^{k} \\ & ⊃E \\ (MN)^{k} : σ^{k} \end{aligned}

While we will always attach a level to a formula, in the exposition we will be more liberal for terms, writing both M : σ^{k} and M^{k} : σ^{k}, since no confusion may arise in this way.

If S is one of the systems introduced below, we write Γ ⊢_{S} M^{i} : σ^{i} when in S there is a derivation:

Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; M^{i} : σ^{i}

Γ ⊢_{S} σ^{i} holds when there is a term M^{i} such that Γ ⊢_{S} M^{i} : σ^{i}.

2.2. System λ^{ℓ}K

The typed λ-calculus λ^{ℓ}K is obtained by adding to λ^{ℓ} the two rules already discussed in the introduction of this section:

Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; M^{j} : σ^{j} ; □I _{j>#Γ} ; gen(M^{j})^{j−1} : □σ^{j−1}  Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; M^{j} : □σ^{j} ; □E ; ungen(M^{j})^{j+1} : σ^{j+1}

The informal meaning of these rules is thus the following.

□I If, from the hypotheses in Γ, we derive that σ holds at knowledge level j, and nothing else holds at any level greater than or equal to j, then □σ has to hold at level j − 1.

□E If, from the hypothesis in Γ, we derive that □σ holds true at knowledge level j, then σ has to be true at the next level.

Such an interpretation corresponds to the semantical property relative to the minimal normal modal logic K: System K is complete with respect to the set of Kripke frames whose accessibility relation is “irreflexive”, “asymmetric” and “intransitive.”

The characteristic axiom of K, □(α ⊃ β) ⊃ (□α ⊃ □β), is derived in λ^{ℓ}K in the following way.

x^{1} : □α^{1} ; □E ; ungen(x^{1})^{2} : α^{2}  y^{1} : □(α ⊃ β)^{1} ; □E ; ungen(y^{1})^{2} : α ⊃ β^{2}
⊃E
(ungen(y^{1})^{2}ungen(x^{1})^{2})^{2} : β^{2}
□I
gen((ungen(y^{1})^{2}ungen(x^{1})^{2})^{2})^{1} : □β^{1}
⊃I
λx^{1} :□α^{1}.gen((ungen(y^{1})^{2}ungen(x^{1})^{2})^{2})^{1} : □α ⊃ □β^{1}
⊃I

λy^{1} :□(α ⊃ β)^{1}.λx^{1} :□α^{1}.gen((ungen(y^{1})^{2}ungen(x^{1})^{2})^{2})^{1} : □(α ⊃ β) ⊃ (□α ⊃ □β)^{1}

2.3. System λ^{ℓ}KT

The typed λ-calculus λ^{ℓ}KT is obtained from λ^{ℓ}K by extending the elimination rule for □.

Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; M^{j} : □σ^{j}

□E _{k∈{j, j+1}}

ungen(M^{j})^{k} : σ^{k}

The informal meaning of such a rule is thus:

If, from the hypothesis in Γ, we derive that □σ holds at knowledge level j, then σ has to hold at the next (j + 1) and at the current (j) level.

We have a correspondence with the semantical property of the Hilbert type formulation of KT: System KT is complete with respect to the set of Kripke frames where the accessibility relation is “reflexive”, “asymmetric” and “intransitive.”

By using the above rule we can prove the characteristic axiom of KT, □α ⊃ α.

x^{1} : □α^{1}
□E
ungen(x^{1})^{1} : α^{1}
⊃I
(λx^{1} :□α^{1}.ungen(x^{1})^{1})^{1} : □α ⊃ α^{1}

2.4. System λ^{ℓ}K4

The typed λ-calculus λ^{ℓ}K4 is obtained from λ^{ℓ}K by extending the elimination rule for □.

Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; M^{j} : □σ^{j}

□E _{k>j}

ungen(M^{j})^{k} : σ^{k}

The informal meaning of such a rule is:

If, from the hypotheses in Γ, we derive that □σ holds at knowledge level j, then σ has to hold at any level greater than j.

We have a correspondence with the following semantical property of the Hilbert type formulation of K4: System KT is complete with respect to the set of frames with the accessibility relation “irreflexive”, “asymmetric,” and “transitive.”

The characteristic K4 axiom, □α ⊃ □□α, is proved in the following way.

x^{1} : □α^{1}
□E
ungen(x^{1})^{3} : α^{3}
□I
gen(ungen(x^{1})^{3})^{2} : □α^{2}
□I
gen(gen(ungen(x^{1})^{3})^{2})^{1} : □□α^{1}
⊃I
(λx^{1} :□α^{1}.gen(gen(ungen(x^{1})^{3})^{2})^{1})^{1} : □α ⊃ □□α^{1}

2.5. System λ^{ℓ}S4

The typed λ-calculus λ^{ℓ}S4 is obtained from λ^{ℓ}K by allowing both the λ^{ℓ}KT and the λ^{ℓ}K4 □ elimination rules.

Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; M^{j} : □σ^{j}

□E _{k≥j}

ungen(M^{j})^{k} : σ^{k}

The informal meaning of such a rule is:

If, from the hypotheses in Γ, we derive that □σ holds at knowledge level j, then σ has to hold at each level greater than or equal to j.

We have a correspondence with the following semantical property of the Hilbert type formulation of S4: System S4 is complete with respect to the set of Kripke frames whose accessibility relation is “reflexive”, “asymmetric,” and “transitive.”

Since the characteristic axioms of S4 are those of K, KT, and K4, they can be proved in λ^{ℓ}S4.

2.6. Implicitly typed λ-calculi

The implicitly typed λ-calculi λ^{∗}K, λ^{∗}KT, λ^{∗}K4, and λ^{∗}S4 are obtained from the previously defined calculi, by erasing from terms the level and type decorations. We loose a 1-to-1 correspondence between proofs and terms, but we gain in readability. The proof terms corresponding to the characteristic axioms of the various logic in the implicit form are the following.

⊢_{λ^{∗}K} λy.λx.gen(ungen(y)ungen(x)) : □(α ⊃ β) ⊃ (□α ⊃ □β)^{1}

⊢_{λ^{∗}KT} λx.ungen(x) : □α ⊃ α^{1}

⊢_{λ^{∗}K4} λx.gen(gen(ungen(x))) : □α ⊃ □□α^{1}

3. Hilbert style systems, a comparison

In this section we show that provability in the calculi λ^{ℓ}K, λ^{ℓ}KT, λ^{ℓ}K4, and λ^{ℓ}S4 is equivalent to provability in the positive fragment of the Hilbert style modal logics K, KT, K4, and S4. Let L be the positive fragment of one of the logics in {K, KT, K4, S4}.

For the purpose of this section, we omit the term labelling for the derivations in the calculus; moreover, if Γ = {σ_{1}^{i}, …, σ_{n}^{i}}, then Γ^{♭} = {σ_{1}, …, σ_{n}}.

Theorem 3.1.

⊢_{L} σ ⟺ ⊢_{λ^{ℓ}L} σ^{1}

The proof of this fact breaks down into the following lemmas.

Lemma 3.2. ⊢_{L} σ ⟹ ⊢_{λ^{ℓ}L} σ^{1}.

Proof. By induction on the lenght of the derivation. Propositional axioms and modus ponens are trivial. The proof in λ^{ℓ}L of the modal axioms of L has been given in the previous section. For the inference rule (Gen), suppose we proved ⊢_{L} σ. By induction hypothesis we have ⊢_{λ^{ℓ}L} σ^{1}. Replacing now any index level k in this deduction with k + 1, we obtain a deduction of ⊢_{λ^{ℓ}L} σ^{2}. An application of □I gives ⊢_{λ^{ℓ}L} □σ^{1}.

The following “translation function” corresponds to the intended meaning of our judgments.

Definition 3.3.

• 𝒯[Γ ⊢ α^{1}] = ⋀ Γ^{♭} ⊃ α

• 𝒯[Γ ⊢ α^{j+1}] = ⋀(Γ^{<2})^{♭} ⊃ □(𝒯[Γ^{≥2}(−1) ⊢ α^{j}])

where, ⋀ ∅ = ⊤ (any tautology).

Lemma 3.4. Γ ⊢_{λ^{ℓ}L} α^{j} ⟹ ⊢_{L} 𝒯[Γ ⊢ α^{j}].

Proof. By trivial, and long, induction on the deduction Γ ⊢_{λ^{ℓ}L} α^{j}.

4. Intermezzo

4.1. On the geometry of proofs

One of the most interesting properties of the system we have proposed (or better of the level machinery), is the geometry it enforces on its deductions. In particular, we show in this section that all (not necessary normal) deductions involving a □I have a very remarkable global structure.

Before showing the technical fact we have in mind, however, we recall a different natural deduction system for S4, namely the “third version” of the calculus discussed in Prawitz’ classical monograph [Pra65, Chapter VI, pag. 79]. The propositional rules of that system can be obtained from those of Definition 2.1 by simply erasing the level indexes (thus obtaining the usual rules for intuitionistic propositional logic). As for the rules for □, the elimination is the same as ours with the omission of levels, while the introduction rule (which we will call □I_{P}) is rather elaborate, in order to ensure normalization and the subformula property. An application of □I_{P} has the form:

\begin{matrix}D_{1}  D_{n} \\ [□τ_{1}  …  □τ_{n}] \\ D \end{matrix} ; σ
□I_{P}
□σ

where □τ_{1}, …, □τ_{n} are all the open assumptions of D, and no open assumption in the deductions D_{i} (of conclusion τ_{i}) is bound in D.^{2} In other words, an application of □I_{P} is obtained by taking a deduction

□τ_{1}  …  □τ_{n}
D
σ

2Prawitz’ original definition is formulated via the concept of essentially modal formula. It is not difficult to see that our formulation of □I_{P}, though not equivalent (it allows less deductions), it is still complete for the ∧, ⊃, □ fragment.

where all open assumptions (if any) are boxed, and plugging into these assumptions arbitrary derivations with the right conclusion. Rule □I_{P} is far from being “natural”: it allows normalization, but at the price of a globally stated constraint on its application.

Coming back to our system, we can show that all applications of □I, in fact, comply with Prawitz’ requirement. In order to give a clearer picture of the involved deductions we will dispense from terms.

Theorem 4.1. Let E be a deduction of Γ ⊢_{λ^{ℓ}S4} σ^{k}, with k > #Γ. Then E has the form

\begin{matrix}Γ_{1}  Γ_{n} \\ D_{1}  D_{n} \\ [□τ_{1}^{h_{1}}  …  □τ_{n}^{h_{n}}] \\ D \end{matrix} ; σ^{k}

where: (i) any Γ_{j} is non empty; (ii) the union of the Γ_{j}’s is Γ; (iii) any D_{j} is a deduction of Γ_{j} ⊢_{λ^{ℓ}S4} □τ_{j}^{h_{j}}; (iv) D is a deduction of □τ_{1}^{h_{1}}, …, □τ_{n}^{h_{n}} ⊢_{λ^{ℓ}S4} σ^{k}; (v) for any j, h_{j} < k.

Proof. If Γ is empty, then the statement is vacuous (n = 0 and D = E). Otherwise, the following informal algorithm will produce the required data.

Let r be any path in E from the conclusion σ^{k} to an occurrence of an open assumption ρ ∈ Γ. In r there must be an application of □E, since k > #Γ and □E is the only rule allowing its conclusion to be at a higher level of its premise. Pick the first application (starting from the conclusion up) of □E in which the level h of the premise (say, □τ^{h}) is strictly less than k. We choose this □τ^{h} as τ_{1}^{h_{1}}; D_{1} is the subtree of E rooted at □τ^{h}; Γ_{1} is the set of all open assumptions of the deduction D_{1} with conclusion □τ^{h}. Clearly ρ ∈ Γ_{1}, thus establishing (i) and (iii) for j = 1; in order to eventually establish (iv), we have to guarantee that no assumption in Γ_{1} can be discharged below □τ^{h}. However, this is obvious, because any formula appearing in the path r below □τ^{h} have a level l > h (by construction), while #Γ_{1} ≤ h, by Proposition 5.1, thus forbidding the application of a ⊃E at level l below □τ^{h}.

The previous procedure can be repeated until there are no more occurrences of assumptions in Γ not already allocated to some Γ_{i}.

When the algorithm terminates, (ii) is obvious, and (iv) follows by construction.

Writing ⊢_{P} for provability in Prawitz’ system and denoting with ( )^{♭} the obvious function stripping the level indexes out of a formula (deduction, etc.), the following is straightforward.

Corollary 4.2. If D is a deduction of Γ ⊢_{λ^{ℓ}S4} σ^{k}, then D^{♭} is a deduction of Γ^{♭} ⊢_{P} σ.

Not any proof in ⊢_{P} can be decorated with levels to become a proof in our system, as the following deduction shows:

□σ ; □I_{P} ; □□σ

Proofs in our system, however, are still enough for completeness and, moreover, seem to have a more direct interpretation as travelling in a Kripke model (cfr. [BM92]).

Many consequences can be drawn from Corollary 4.2. Since any reduction step in our system becomes also a reduction step in ⊢_{P} under the ( )^{♭} translation, we immediately obtain normalization for λ^{ℓ}S4 from the normalization theorem for ⊢_{P}. We will give a different proof of strong normalization for λ^{ℓ}S4, in Section 6.2..

Moreover, by adding to the usual clauses that, for any k, σ^{k} has to considered a subformula of σ^{h}, we also obtain the following subformula property.

Theorem 4.3 (Subformula principle) Any formula occurring in a normal deduction of Γ ⊢_{λ^{ℓ}S4} σ^{k} is a subformula of σ^{k} or of some formula in Γ.

Proof. (Sketch) It is enough to prove the theorem for ⊢_{P}, which can be obtained in the same way as the corresponding result for intuitionistic logic [Pra65, Theorem 2, pag. 53; cfr pag. 80].

Starting from a purely structural extension of the syntax (the levels) and adopting only local rules (in particular, □I as opposed to □I_{P}) we have recovered the global, elaborated constraint on the geometry of the deductions that other systems are forced to require from the beginning.

4.2. A proof theoretical request… fulfilled

One of the principal features of a good modal proof theory is its capability to suit a class of different modal logics without changing the way modal connectives are manipulated (e.g. introduced and eliminated). The differentiation between logics is instead delegated to the way (general) formulas are manipulated.

A clear discussion on this topics (in the case of modal systems) may be found in recent work of Wansing [Wan93] and Došen [Dos85]. This point of view (that [Wan93] calls Došen principle, but that should be traced back to Gentzen, for the differentiation of intuitionistic from classical logic) may be stated as:

The rules for the logical operations are never changed: all changes are made in the structural rules. [Dos85]

At first look our calculi violate this principle: different systems are obtained with different elimination rules.

One could attempt a “weak” defense, arguing that all the proposed elimination rules are equal in “spirit”, since they differ only in level decorations. But this would miss the point. Indeed, we totally agree with Došen principle and we claim that our approach does not violate it… when observed in the right context. The distinction between logical and structural rules, in fact, is only relevant in sequent calculi, and it is thus there that the challenge posed by Došen principle has to be attacked. The natural deduction system λ^{ℓ}K has an associated 2-sequent calculus (see [Mas93]), whose left and right □ introduction rules are the following:

\begin{matrix}𝔖_{1} & & ε \\ 𝔖_{2} & & ε \\ ⋮ & ⊢ & ⋮ \\ 𝔖_{k−1} & & ε \\ 𝔖_{k}, σ & & τ \end{matrix} ; □ ⊢ ; \begin{matrix}𝔖_{1} & & ε \\ 𝔖_{2} & & ε \\ ⋮ & ⊢ & ⋮ \\ 𝔖_{k−1}, □σ & & ε \\ 𝔖_{k} & & τ \end{matrix}  \begin{matrix}𝔖_{1} & & ε \\ 𝔖_{2} & & ε \\ ⋮ & ⊢ & ⋮ \\ 𝔖_{k} & & ε \\ ε & & σ \end{matrix} ; ⊢ □ ; \begin{matrix}𝔖_{1} & & ε \\ 𝔖_{2} & & ε \\ ⋮ & ⊢ & ⋮ \\ 𝔖_{k} & & □σ \end{matrix}

Sequent calculi for KT and K4 are now obtained by adding the structural rules (on levels) ⊢↑ (KT) and ⊢↓ (T 4), respectively:

\begin{matrix}𝔖_{1} & & ε \\ 𝔖_{2} & & ε \\ ⋮ & ⊢ & ⋮ \\ 𝔖_{k} & & ε \\ ε & & σ \end{matrix} ; ⊢↑ (KT) ; \begin{matrix}𝔖_{1} & & ε \\ 𝔖_{2} & & ε \\ ⋮ & ⊢ & ⋮ \\ 𝔖_{k} & & σ \end{matrix}  \begin{matrix}𝔖_{1} & & ε \\ 𝔖_{2} & & ε \\ ⋮ & ⊢ & ⋮ \\ 𝔖_{k} & & ε \\ ε & & σ \end{matrix} ; ⊢↓ (K4) ; \begin{matrix}𝔖_{1} & & ε \\ 𝔖_{2} & & ε \\ ⋮ & ⊢ & ⋮ \\ 𝔖_{k} & & ε \\ ε^{n} & & ε^{n} \\ ε & & σ \end{matrix}

where n ≥ 1 and

ε^{n} = ε ; ⋮ ; ε } n times

The calculus for S4 is obtained by adding to the basic logical rules both ⊢↑ (KT) and ⊢↓ (T 4). Thus, in a sequent setting, the four systems are obtained by means of structural rules.

The structural rules of sequent calculi, on the other hand, should not be explicit in the corresponding natural deduction formulation. Intuitionistic contractions and weakenings, for instance, are realized by the convention on the discharging (meta-) operation. This is why our calculi do not contain rules like

Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; σ^{r} ; σ^{j}

Following the traditional natural deduction approach, such rules have been embedded into the (logical) □E rules.

5. Working with λ^{ℓ}S4 proofs

In this section ⊢ will stand for ⊢_{λ^{ℓ}S4}, whose rules are recalled in Figure 1.

Proposition 5.1. Let Γ ⊢ M^{i} : σ^{i}. Then i ≥ #Γ.

Proof. Inspection of the rules.

Definition 5.2. A derivation Γ ⊢ M^{i} : σ^{i} is concluded if i = 1 and #Γ ≤ 1.

Theorem 5.3. Any non concluded derivation can be extended to a concluded one.

Proof. Given a non concluded Γ ⊢ σ^{k}, first replace any σ^{h} ∈ Γ with:

□σ^{1} ; □E ; σ^{h}

At this point apply k − 1 times the rule □I to the conclusion, obtaining a formula of level 1.

x^{k} : σ^{k}

\begin{aligned}Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; M : σ^{k} & Δ ; \begin{matrix}· \\ · \\ · \end{matrix} ; N : τ^{k} \\ & ∧I \\ ⟨M, N⟩^{k} : σ ∧ τ^{k} \end{aligned}  Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; M : σ ∧ τ^{k} ; ∧E_{l} ; (fst M)^{k} : σ^{k}  Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; M : σ ∧ τ^{k} ; ∧E_{r} ; (snd M)^{k} : τ^{k}

Γ [x^{k} : σ^{k}] ; \begin{matrix}· \\ · \\ · \end{matrix} ; M : τ^{k} ; ⊃I ; (λx^{k}:σ^{k}.M)^{k} : σ ⊃ τ^{k}  \begin{aligned}Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; M : σ ⊃ τ^{k} & Δ ; \begin{matrix}· \\ · \\ · \end{matrix} ; N : σ^{k} \\ & ⊃E \\ (MN)^{k} : σ^{k} \end{aligned}

Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; M : σ^{j} ; □I _{j>#Γ} ; gen(M)^{j−1} : □σ^{j−1}

Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; M : □σ^{j}

□E _{k≥j}

ungen(M)^{k} : σ^{k}

Figure 1: Rules for λ^{ℓ}S4

The following technical lemmas aim to show, given a deduction for Γ ⊢ σ^{k}, how to obtain a deduction for the same conclusion at a different level, possibly changing also some of the levels in Γ. We will see in Section 6. that this operation is essential for the computational interpretation of proofs. At first sight the operations on proof trees given in this section may appear heavy and difficult to grasp. Notice, however, that the problem we tackle is essentially the same as the one arising in the first order natural deduction system NJ, when, given a deduction for Γ ⊢ σ(x) and a term t, we want to obtain a deduction for Γ′ ⊢ σ(t). Many texts say, in this case, that all it is needed is the uniform substitution of t for x in the proof tree. A careful analysis of the process involved, however, shows that care must be taken in performing this operation; in particular, it is needed a strong discipline in the use of variables. A very clear account of the issues involved is given in [TvD88, Volume II, Ch. 10]. Levels in λ^{ℓ}S4 play a very similar role to variables of NJ; the following lemmas can then be seen as expressing concepts like “renaming,” “term substitution” and their properties.

Lemma 5.4. Let k > 0. Γ ⊢ α^{j} ⟹ ∀i ≤ j Γ^{<i}, Γ^{≥i}(+k) ⊢ α^{j+k}

Proof.

• α^{j} ⊢ α^{j} ⇒ α^{j} ∈ Γ^{≥i}(+k) then α^{j+k} ⊢ α^{j+k}

• if Γ, α^{j} ; ⋮ ; β^{j} ; \overline{α ⊃ β^{j}} then I.H. \{ Γ^{<i}, Γ^{≥i}(+k), α^{j+k} ; ⋮ ; β^{j+k} ; \overline{α ⊃ β^{j+k}}

• if Γ ; ⋮ ; α^{j} ; \overline{□α^{j−1}} then I.H. \{ Γ^{<i}, Γ^{≥i}(+k) ; ⋮ ; α^{j+k} ; \overline{□α^{j−1+k}}

• if Γ ; ⋮ ; □α^{j} ; \overline{α^{r}} we have two subcases:

(i ≤ j) in this case we have:

I.H. \{ Γ^{<i}, Γ^{≥i}(+k) ; ⋮ ; □α^{j+k} ; \overline{α^{r+k}}

(j < i ≤ r) in this case, without applying induction hypothesis and noting that Γ^{≥i} = ∅ by Proposition 5.1, we have:

Γ^{<i}, Γ^{≥i}(+k) ; ⋮ ; □α^{j} ; \overline{α^{r+k}}

Lemma 5.5. Let j ≤ 2. Γ ⊢ α^{j} ⟹ ∀i (2 ≤ i ≤ j) Γ^{<i}, Γ^{≥i}(−1) ⊢ α^{j−1}

Proof.

• α^{j} ⊢ α^{j} ⇒ α^{j−1} ∈ Γ^{≥i}(−1) then α^{j−1} ⊢ α^{j−1}

• if Γ, α^{j} ; ⋮ ; β^{j} ; \overline{α ⊃ β^{j}} then I.H. \{ Γ^{<i}, Γ^{≥i}(−1), α^{j−1} ; ⋮ ; β^{j−1} ; \overline{α ⊃ β^{j−1}}

• if Γ ; ⋮ ; α^{j} ; \overline{□α^{j−1}} then I.H. \{ Γ^{<i}, Γ^{≥i}(−1) ; ⋮ ; α^{j−1} ; \overline{□α^{j−2}}

• if Γ ; ⋮ ; □α^{j} ; \overline{α^{r}} we have two subcases:

(j ≥ 2, i ≤ j) in this case we have:

I.H. \{ Γ^{<i}, Γ^{≥i}(−1) ; ⋮ ; □α^{j−1} ; \overline{α^{r−1}}

(j < i ≤ r) in this case, without applying induction hypothesis and noting that Γ^{≥i} = ∅ by Proposition 5.1, we have:

Γ^{<i}, Γ^{≥i}(+k) ; ⋮ ; □α^{j} ; \overline{α^{r−1}}

The operations on deductions given in the proof of the two previous lemmas is explicitated on proof terms by the following definition.

Definition 5.6. [Level substitution] Let Γ ⊢ M : σ^{v} and i ≥ 1; let n ∈ {−1} ∪ ℕ if v ≥ 2, and n ∈ ℕ otherwise. We inductively define the level substitution [n]_{i}M (read: increment by n any levels greater than or equal to i). If v < i:

[n]_{i}M^{v} = M^{v}

If v ≥ i:

[n]_{i}x^{v} = x^{v+n}
[n]_{i}⟨M, N⟩^{v} = ⟨[n]_{i}M, [n]_{i}N⟩^{v+n}
[n]_{i}(fst M)^{v} = (fst [n]_{i}M)^{v+n}
[n]_{i}(snd M)^{v} = (snd [n]_{i}M)^{v+n}
[n]_{i}(λx^{v}:σ^{v}.M)^{v} = (λx^{v+n}:σ^{v+n}.[n]_{i}M)^{v+n}
[n]_{i}(MN)^{v} = ([n]_{i}M [n]_{i}N)^{v+n}
[n]_{i}gen(M)^{v} = gen([n]_{i}M)^{v+n}
[n]_{i}ungen(M)^{v} = ungen([n]_{i}M)^{v+n}

Whenever we write a level substitution [n]_{i}M, we assume that all the constraints of the definition are satisfied (in particular those on n). Note that [0]_{i}M^{v} = M^{v}. Lemmas 5.4 and 5.5 can then be reformulated as follows.

Lemma 5.7. Γ ⊢ M : α^{j} ⟹ ∀i ≤ j, Γ^{<i}, Γ^{≥i}(+k) ⊢ [+k]_{i}M : α^{j+k}

Lemma 5.8. Let j ≥ 2, then: Γ ⊢ M : α^{j} ⟹ ∀i, 2 ≤ i ≤ j, Γ^{<i}, Γ^{≥i}(−1) ⊢ [−1]_{i}M : α^{j−1}

We can picture the effect of the level substitution on proof trees as follows. It is not difficult to extend Theorem 4.1 to the following more general fact.

Theorem 5.9. Let E be a deduction of Γ ⊢ σ^{k}, and let i ≤ k. Then E has the form

\begin{matrix}Γ_{1}^{<i}  Γ_{n}^{<i} \\ D_{1}  D_{n} \\ [□τ_{1}^{h_{1}}  …  □τ_{n}^{h_{n}}] Γ^{≥i} \\ D \end{matrix} ; σ^{k}

where: (i) any Γ_{j}^{<i} is non empty; (ii) the union of the Γ_{j}^{<i}’s is Γ^{<i}; (iii) any D_{j} is a deduction of Γ_{j}^{<i} ⊢ □τ_{j}^{h_{j}}; (iv) D is a deduction of □τ_{1}^{h_{1}}, …, □τ_{n}^{h_{n}}, Γ^{≥i} ⊢ σ^{k}; (v) for any j, h_{j} < i.

Proof. A simple variant of the proof of Theorem 4.1, or, for the reader preferring recursion to iteration, by a routine induction on the lenght of E, similarly to Lemmas 5.4 and 5.5.

In the same hypotheses of the theorem, now, the deduction [m]_{i}E is the following

\begin{matrix}Γ_{1}^{<i}  Γ_{n}^{<i} \\ D_{1}  D_{n} \\ [□τ_{1}^{h_{1}}  …  □τ_{n}^{h_{n}}] Γ^{≥i}(m) \\ [m]_{i}D \end{matrix} ; σ^{k}

where all formulas appearing in D are affected by the level modification, while all the D_{j}’s deductions are left unchanged.

Next lemma shows how level substitution interact with term substitution.

Lemma 5.10. ([n]_{i}M)[[n]_{i}N/x^{k+n}] = [n]_{i}(M[N/x^{k}])

Proof. Just note that if x^{k} ∈ F V (M) then any subterm of M containing x^{k} has a level h ≥ k. If x^{k} ∉ F V (M) then the variable-level-convention ensures the thesis.

We show, next, a property of nested level substitutions.

Lemma 5.11 (Level substitution lemma) Let k ≥ 1, n ≥ −1, and j ≥ 0.

(i) If i ≤ k − 1, then for any l ≥ k, [n]_{i}[j − 1]_{k}M^{l} = [j − 1]_{k+n}[n]_{i}M^{l}.

(ii) If k − 1 < i ≤ k − 1 + j, then for any l ≥ k, [n]_{i}[j − 1]_{k}M^{l} = [j − 1 + n]_{k}M^{l}.

Proof. By induction on M^{l}. The base case and all the propositional cases are straigthforward. We give only the modal cases. (i)

M^{l} = ungen(N^{v})^{l}: [j − 1]_{k+n}[n]_{i}ungen(N^{v})^{l} = ungen([j − 1]_{k+n}[n]_{i}N^{v})^{l+n+j−1}, and [n]_{i}[j − 1]_{k}ungen(N^{v})^{l} = ungen([n]_{i}[j − 1]_{k}N^{v})^{l+n+j−1}. If v ≥ k, we apply the induction hypothesis. If i ≤ v < k, [j − 1]_{k+n}[n]_{i}N^{v} = [n]_{i}N^{v} = [n]_{i}[j − 1]_{k}N^{v}. If v < i ≤ k − 1, [j − 1]_{k+n}[n]_{i}N^{v} = N^{v} = [n]_{i}[j − 1]_{k}N^{v}.

M^{l} = gen(N^{l+1})^{l}: [j − 1]_{k+n}[n]_{i}gen(N^{l+1})^{l} = gen([j − 1]_{k+n}[n]_{i}N^{l+1})^{l+n+j−1}, and [n]_{i}[j − 1]_{k}gen(N^{l+1})^{l} = gen([n]_{i}[j − 1]_{k}N^{l+1})^{l+n+j−1}. Conclude by induction hypothesis.

(ii)

M^{l} = ungen(N^{v})^{l}: [j − 1 + n]_{k}ungen(N^{v})^{l} = ungen([j − 1 + n]_{k}N^{v})^{l+j−1+n}, and [n]_{i}[j − 1]_{k}ungen(N^{v})^{l} = ungen([n]_{i}[j − 1]_{k}N^{v})^{l+j−1+n}. If v ≥ k, conclude by the induction hypothesis. If v < k, [j − 1 + n]_{k}N^{v} = N^{v} = [n]_{i}[j − 1]_{k}N^{v}.

M^{l} = gen(N^{l+1})^{l}: [j − 1 + n]_{k}gen(N^{l+1})^{l} = gen([j − 1 + n]_{k}N^{l+1})^{l+j−1+n}, and [n]_{i}[j − 1]_{k}genN^{l+1})^{l} = gen([n]_{i}[j − 1]_{k}N^{l+1})^{l+j−1+n}. Conclude by the induction hypothesis.

6. Computations

In the previous section a class of modal typed λ-calculi has been introduced. It is now necessary to study their computational behavior, by introducing suitable notions of reduction extending the usual typed β-reduction and corresponding to the process of proof normalization. We will be able to show that this reduction is confluent (or Church-Rosser) and strongly normalizing (or nötherian).

Definition 6.1. [Contraction]

((λx^{j}:σ^{j}.M^{j})^{j}N^{j})^{j} ▷ [N^{j}/x^{j}]M^{j}
(fst ⟨M^{j}, N^{j}⟩^{j})^{j} ▷ M^{j}
(snd ⟨M^{j}, N^{j}⟩^{j})^{j} ▷ N^{j}
ungen(gen(M^{k})^{k−1})^{k−1+j} ▷ [j − 1]_{k}M^{k} (for j ∈ ℕ).

The compatible closure of ▷ (or one-step reduction) is denoted with →; its transitive closure is →^{+}, while ↠ (the reduction relation) is the transitive and reflexive closure.

The following theorem expresses the correctness of Definition 6.1 with respect to types.

Theorem 6.2. If Γ ⊢ M^{j} : σ^{j} and M^{j} ↠ N^{j}, then Γ ⊢ N^{j} : σ^{j}.

Proof. The only non standard case is when the reduction is a modal contraction. From M = ungen(gen(P^{k})^{k−1})^{k−1+j} we have Γ ⊢ P^{k} : □σ^{k} and k > #Γ. The level substitution in [j − 1]_{k}P^{k}, then, does not affect the free variables of P and Lemmas 5.7 and 5.8 give the thesis.

Reduction and level substitution match well: the former is preserved by the latter, as the following results will show.

Lemma 6.3. If M^{h} ▷ N^{h}, then for any i ≤ h and any n, [n]_{i}M^{h} ▷ [n]_{i}N^{h}.

Proof. By cases on the definition of contraction. We give only the modal case. Suppose that, for j ∈ ℕ,

ungen(gen(M^{k})^{k−1})^{k−1+j} ▷ [j − 1]_{k}M^{k}

and we have to prove, for any i ≤ k − 1 + j, that

[n]_{i}ungen(gen(M^{k})^{k−1})^{k−1+j} ▷ [n]_{i}[j − 1]_{k}M^{k}.

We distinguish two cases. If i ≤ k − 1:

[n]_{i}ungen(gen(M^{k})^{k−1})^{k−1+j} = ungen(gen([n]_{i}M^{k})^{k−1+n})^{k−1+j+n}
▷ [j − 1]_{k+n}[n]_{i}M^{k}
= [n]_{i}[j − 1]_{k}M^{k} by Lemma 5.11(i)

Otherwise, when i > k − 1:

[n]_{i}ungen(gen(M^{k})^{k−1})^{k−1+j} = ungen(gen(M^{k})^{k−1})^{k−1+j+n}
▷ [j − 1 + n]_{k}M^{k}
= [n]_{i}[j − 1]_{k}M^{k} by Lemma 5.11(ii)

Lemma 6.4. If M^{h} → N^{h} then for any i ≤ h and any n, [n]_{i}M^{h} → [n]_{i}N^{h}.

Proof. By induction on the definition of the relation →. If M^{h} ▷ N^{h}, use Proposition 6.3. The inductive steps are all straightforward, but the modal cases.

Let ungen(M^{v})^{k}) → ungen(N^{v})^{k}, with M^{v} → N^{v}, and let i ≤ k. We have to prove that [n]_{i}ungen(M^{v})^{k}) → [n]_{i}ungen(N^{v})^{k}, that is ungen([n]_{i}M^{v})^{k+n} → ungen([n]_{i}N^{v})^{k+n}. If i ≤ v, apply the induction hypotesis; otherwise [n]_{i}M^{v} = M^{v}, [n]_{i}N^{v} = N^{v} and conclude.

Let gen(M^{k+1})^{k} → gen(N^{k+1})^{k}, with M^{k+1} → N^{k+1}, and i ≤ k. We have to prove that [n]_{i}gen(M^{k+1})^{k}) → [n]_{i}gen(N^{k+1})^{k}, that is gen([n]_{i}M^{k+1})^{k+n} → gen([n]_{i}N^{k+1})^{k+n}. Conclude applying the induction hypothesis.

Theorem 6.5. If M^{h} ↠ N^{h}, then for any i ≤ h and any n, [n]_{i}M^{h} ↠ [n]_{i}N^{h}.

Proof. By induction on the lenght of the reduction, using lemma 6.4.

6.1. Confluence

We prove the Church-Rosser property for ↠, using Tait’s technique as formulated in [Gir87] or [Bar84], here adapted to modal terms. We define first a new auxiliary notion of reduction ( ⇉ ), corresponding to the (possible) parallel contraction of several non overlapping redexes; note that ⇉ is not transitive. Then, ⇉ is shown to respect both term and level substitution; from this we prove that “ ⇉ satisfy the diamond property,” Lemma 6.9. Since ↠ is obviously the transitive and reflexive closure of ⇉ , we have a standard proof that ↠ is Church-Rosser.

In the following proofs we will give only the main (modal) cases. For the others, which are standard, the reader is referred to the literature.

Definition 6.6. The one-step parallel reduction is defined by the following clauses.

i. M : α^{k} ⇉ M : α^{k};

ii. If M : α^{k} ⇉ M′ : α^{k} and N : β^{k} ⇉ N′ : β^{k}, then ⟨M, N⟩^{k} : α ∧ β^{k} ⇉ ⟨M′, N′⟩^{k} : α ∧ β^{k};

iii. If M : β^{k} ⇉ M′ : β^{k}, then (λx^{k}:α^{k}.M)^{k} : α ⊃ β^{k} ⇉ (λx^{k}:α^{k}.M′)^{k} : α ⊃ β^{k};

iv. If M : α^{k} ⇉ M′ : α^{k}, then gen(M)^{k−1} : □α^{k−1} ⇉ gen(M′)^{k−1} : □α^{k−1};

v. If M : α ∧ β^{k} ⇉ M′ : α ∧ β^{k}, then (fst M)^{k} : α^{k} ⇉ (fst M′)^{k} : α^{k} and (fst M)^{k} : α^{k} ⇉ (fst M′)^{k} : α^{k};

vi. If M : α^{k} ⇉ M′ : α^{k} and N : α ⊃ β^{k} ⇉ N′ : α ⊃ β^{k}, then (NM)^{k} : β^{k} ⇉ (N′M′)^{k} : β^{k};

vii. If M : □α^{k} ⇉ M′ : □α^{k}, then ungen(M)^{w} : α^{w} ⇉ ungen(M′)^{w} : α^{w};

viii. If M : α^{k} ⇉ M′ : α^{k} and N : β^{k} ⇉ N′ : β^{k}, then (fst ⟨M, N⟩^{k})^{k} : α^{k} ⇉ M′ : α^{k} and (snd ⟨M, N⟩^{k})^{k} : β^{k} ⇉ N′ : β^{k};

ix. If M : β^{k} ⇉ M′ : β^{k} and N : α^{k} ⇉ N′ : α^{k}, then ((λx^{k}:α^{k}.M)^{k}N^{k})^{k} : β^{k} ⇉ M′[N′/x^{k}] : β^{k};

x. If M : α^{k} ⇉ M′ : α^{k}, then ungen(gen(M)^{k−1})^{k−1+j} : α^{k−1+j} ⇉ [j − 1]_{k}M′ : α^{k−1+j}.

Lemma 6.7. If N : α^{k} ⇉ N′ : α^{k}, M : β^{h} ⇉ M′ : β^{h}, and x^{k} : α^{k}, then

M[N/x^{k}] : β^{h} ⇉ M′[N′/x^{k}] : β^{h}.

Proof. By induction on the lenght of the derivation of M : β^{h} ⇉ M′ : β^{h}.

Base case: M = M′. This case is established by a structural induction on M.

Induction step: by cases on the last clause used to derive M : β^{h} ⇉ M′ : β^{h}. We give some cases, labelled by the clause used.

(iv) gen(M)^{h} : □α^{h} ⇉ gen(M′)^{h} : □α^{h}, where M : α^{h+1} ⇉ M′ : α^{h+1}. By induction hypothesis, M[N/x^{k}] : α^{h+1} ⇉ M′[N′/x^{k}] : α^{h+1}, from which the thesis, since gen(M)^{h}[N/x^{k}] = gen(M[N/x^{k}])^{h} : □α^{h} and similarly for M′.

(vii) similarly to the previous case.

(x) ungen(gen(M)^{h−1})^{h−1+j} : α^{h−1+j} ⇉ [j − 1]_{h}M′ : α^{h−1+j}, where M : α^{h} ⇉ M′ : α^{h}. The thesis is now given by the following diagram:

ungen(gen(M)^{h−1})^{h−1+j}[N/x^{k}] : α^{h−1+j} ⇉^{?} ([j − 1]_{h}M′)[N′/x^{k}] : α^{h−1+j}
∥  ∥ (*)
ungen(gen(M)^{h−1}[N/x^{k}])^{h−1+j}  ⇉ [j − 1]_{h}(M′[N′/x^{k}]) : α^{h−1+j}

where the ⇉ in the bottom row is given by induction hypothesis and clause (x), while equality (*) holds as either x^{k} does not occur in M, or k < h.

Lemma 6.8. If M : α^{k} ⇉ M′ : α^{k}, then for any i and any n

[n]_{i}M : α^{k+n} ⇉ [n]_{i}M′ : α^{k+n}

Proof. If i > k the statement is trivial; otherwise we proceed by induction on the lenght of the derivation of M : α^{k} ⇉ M′ : α^{k}.

Basis: If M = M′ the thesis is trivial.

Induction step: we give only some typical cases, labelled by the last clause used.

(iii) M = (λx^{k} : α^{k}.N)^{k} : α ⊃ β^{k}, M′ = (λx^{k} : α^{k}.N′)^{k} : α ⊃ β^{k}, with N : β^{k} ⇉ N′ : β^{k}. By induction hypotesis [n]_{i}N : β^{k+n} ⇉ [n]_{i}N′ : β^{k+n}; now conclude by clause (iii) and definition of level substitution.

(iv) As the previous case.

(vii) M = ungen(N^{k−j})^{k} : α^{k} and M′ = ungen(N^{′k−j})^{k} : α^{k}, with N^{k−j} : β^{k−j} ⇉ N^{′k−j} : β^{k−j}. The thesis is given by the following diagram:

[n]_{i}ungen(N^{k−j})^{k} : α^{k+n}  ⇉^{?}  [n]_{i}ungen(N^{′k−j})^{k} : α^{k+n}
∥  ∥
ungen([n]_{i}N^{k−j})^{k+n} : α^{k+n} ⇉^{by IH} ungen([n]_{i}N^{′k−j})^{k+n} : α^{k+n}

(ix) M = ((λx^{k}:α^{k}.N)^{k}P^{k})^{k} : β^{k} and M′ = N^{′k}[P^{′k}/x^{k}] : β^{k}, with N : β^{k} ⇉ N′ : β^{k} and P^{k} : α^{k} ⇉ P^{′k} : α^{k}. The thesis is given by the following diagram:

[n]_{i}((λx^{k}:α^{k}.N)^{k}P^{k})^{k} : β^{k+n}  ⇉^{?}  [n]_{i}(N^{′k}[P^{′k}/x^{k}]) : β^{k+n}
∥  ∥ (*)
((λx^{k+n}:α^{k+n}.[n]_{i}N)^{k+n}([n]_{i}P^{k}))^{k+n} : β^{k+n} ⇉^{by IH} ([n]_{i}N′)^{k}[[n]_{i}P^{′k}/x^{k+n}] : β^{k+n}

where (*) is Lemma 5.10 and the ⇉ in the bottom row follows by induction hypothesis and clause ix.

(x) M = ungen(gen(N^{k−j+1})^{k−j})^{k} : α^{k} and M′ = [j − 1]_{k−j+1}N^{′k−j+1} : α^{k}, with N^{k−j+1} : α^{k−j+1} ⇉ N^{′k−j+1} : α^{k−j+1}, which by IH implies that

[n]_{i}N^{k−j+1} : [n]_{i}α^{k−j+1} ⇉ [n]_{i}N^{′k−j+1} : [n]_{i}α^{k−j+1}  (2)

We have two cases. If i ≤ k − j the thesis is given by the following diagram:

[n]_{i}ungen(gen(N^{k−j+1})^{k−j})^{k} : α^{k+n}  ⇉^{?} [n]_{i}[j − 1]_{k−j+1}N^{′k−j+1} : α^{k+n}
∥  ∥ (*)
ungen(gen([n]_{i}N^{k−j+1})^{k−j+n})^{k+n} : α^{k+n} ⇉^{(**)} [j − 1]_{k−j+1+n}[n]_{i}N^{′k−j+1} : α^{k+n}

where (*) is Lemma 5.11(i), and (**) follows by (2) and clause x. If i > k − j the following diagram establishes the thesis:

[n]_{i}ungen(gen(N^{k−j+1})^{k−j})^{k} : α^{k+n} ⇉^{?} [n]_{i}[j − 1]_{k−j+1}N^{′k−j+1} : α^{k+n}
∥  ∥ (*)
ungen(gen(N^{k−j+1})^{k−j})^{k+n} : α^{k+n} ⇉^{(**)} [j − 1 + n]_{k−j+1}N^{′k−j+1} : α^{k+n}

where (*) is Lemma 5.11(ii), and (**) follows by 2 and clause x.

Lemma 6.9 (Diamond Property) Suppose M : α^{k} ⇉ M′ : α^{k} and M : α^{k} ⇉ M′′ : α^{k}. Then we can find a term M′′′ : α^{k} such that

[figure: \begin{aligned}& M : α^{k} \\ M_{′′} : α_{k} & & M_{′} : α_{k} \\ & M′′′ : α^{k} \end{aligned}]

Proof. Let n′ and n′′ be the lenght of the derivations r′ of M : α^{k} ⇉ M′ : α^{k} and r′′ of M : α^{k} ⇉ M′′ : α^{k}. The thesis is extablished by induction on n′ + n′′. We give only the modal

cases. We write M : α^{k} ⇉^{n} M′ : α^{k} to denote that M : α^{k} ⇉ M′ : α^{k} is established with a deduction of lenght n.

• Both r′ and r′′ end with clause (iv).

gen(P)^{k} : □α^{k}
gen(P′′)^{k} : □α^{k}  gen(P′)^{k} : □α^{k}
gen(P′′′)^{k} : □α^{k}

[figure]
n′′

[figure]
n′

[figure] [figure] [figure] [figure] [figure] [figure]

where [figure: \begin{aligned}& P : α^{k−1} \\ P_{′′} : α_{k−1} & & P_{′} : α_{k−1} \\ & P′′′ : α^{k−1} \end{aligned}; n′′−1; n′−1]

is obtained by I.H.

• Both r′ and r′′ end with clause (vii). As the previous case.

• Both r′ and r′′ end with clause (x).

ungen(gen(P)^{k−j})^{k} : α^{k}
[j − 1]_{k−j+1}P′′ : α^{k}  [j − 1]_{k−j+1}P′ : α^{k}
[j − 1]_{k−j+1}P′′′ : α^{k}

[figure]
n′′

[figure]
n′

[figure] [figure] [figure] [figure] [figure] [figure]

Where [figure: \begin{aligned}& P : α^{k−1} \\ P_{′′} : α_{k−1} & & P_{′} : α_{k−1} \\ & P′′′ : α^{k−1} \end{aligned}; n′′−1; n′−1]

is obtained by I.H. and

[j − 1]_{k−j+1}P′ : α^{k} ⇉ [j − 1]_{k−j+1}P′′′ : α^{k} ⇇ [j − 1]_{k−j+1}P′′ : α^{k}

holds by Lemma 6.8.

• Last clause of r′ is (x) and last clause of r′′ is (vii).

ungen(gen(P)^{k−j})^{k} : α^{k}

ungen(Q^{k−j})^{k} : α^{k}  [j − 1]_{k−j+1}P′ : α^{k}

[j − 1]_{k−j+1}P′′′ : α^{k}

[figure]
n′′

[figure]
n′

[figure] [figure] [figure] [figure] [figure] [figure]

where

gen(P)^{k−j} : □α^{k−j} ⇉^{n′′−1} Q^{k−j} : □α^{k−j}

Observe now that Q^{k−j} = gen(P′′)^{k−j}, with

P : α^{k−j+1} ⇉^{<n′′} P′′ : α^{k−j+1}

since no clause for ⇉ may remove a toplevel gen. By induction hypothesis we obtain

[figure: \begin{aligned}& P : α^{k−j+1} \\ P_{′′} : α_{k−j+1} & & P_{′} : α_{k−j+1} \\ & P′′′ : α^{k−j+1} \end{aligned}; n′′−1; n′−1]

Lemma 6.8 allows to conclude.

Theorem 6.10 (Church-Rosser) The ↠ relation is confluent.

Proof. M ↠ N iff M = M_{0} ⇉ … ⇉ M_{n} = N with n ≥ 0. The usual Church-Rosser diamond can now be closed by using the previous lemma.

6.2. Strong normalization

We reduce the problem of strong normalization for λ^{ℓ}S4 to the strong normalization for the system of next definition.

Definition 6.11. [Calculus λS4] Terms and derivations are inductively defined by the following rules.

x : σ^{k}

\begin{aligned}Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; M : σ^{k} & Δ ; \begin{matrix}· \\ · \\ · \end{matrix} ; N : τ^{k} \\ & ∧I \\ ⟨M, N⟩ : σ ∧ τ^{k} \end{aligned}  Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; M : σ ∧ τ^{k} ; ∧E_{l} ; (fst M) : σ^{k}  Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; M : σ ∧ τ^{k} ; ∧E_{r} ; (snd M) : τ^{k}

Γ [x : σ^{k}] ; \begin{matrix}· \\ · \\ · \end{matrix} ; M : τ^{k} ; ⊃I ; λx.M : σ ⊃ τ^{k}  \begin{aligned}Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; M : σ ⊃ τ^{k} & Δ ; \begin{matrix}· \\ · \\ · \end{matrix} ; N : σ^{k} \\ & & ⊃E \\ MN : σ^{k} \end{aligned}

Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; M : σ^{j} ; □I _{j>#Γ} ; M : □σ^{j−1}  Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; M : □σ^{j} ; □E _{k≥j} ; M : σ^{k}

Derivations in λ^{ℓ}S4 can be obviously translated into λS4, by forgetting the type and level decoration as well as all the gen, ungen constructors. Writing M^{∘} for the term obtained in this way, the following is straightforward.

Proposition 6.12. Γ ⊢_{λ^{ℓ}S4} M : σ^{k} ⟺ Γ^{∘} ⊢_{λS4} M^{∘} : σ^{k}

Let λ be the intuitionistic lambda calculus with implication and conjunction. The types of λS4 can be interpreted into the types of λ by means of the following translation.

(p^{k})^{∗} = p
(α ⊃ β^{k})^{∗} = (α^{k})^{∗} ⊃ (β^{k})^{∗}
(α ∧ β^{k})^{∗} = (α^{k})^{∗} ∧ (β^{k})^{∗}
(□α^{k})^{∗} = (α^{k+1})^{∗}

Proposition 6.13. Γ ⊢_{λS4} M : σ^{k} ⟹ Γ^{∗} ⊢_{λ} M : σ^{∗}

Proof. Induction on the derivation, the modal rules becoming vacuous steps in λ.

It is well known (e.g. [Bar92]) that λ enjoys strong normalization. It is now easy to obtain as a corollary the same result for λ^{ℓ}S4.

Theorem 6.14. λ^{ℓ}S4 enjoys strong normalization.

Proof. Let Γ ⊢_{λ^{ℓ}S4} M : σ^{k} and suppose there is an infinite reduction sequence starting from M. Observe now that this sequence cannot be composed (from some point on) only of modal contractions, since a modal contraction strictly decreases the number of nodes of the proof tree. Hence the reduction sequence contains an infinite number of propositional reductions (that is, contractions of non modal redexes). But this is impossibile, because these propositional reductions would also be reductions of M^{∘}, which is typeable in λ, by the previous propositions, while λ enjoys strong normalization.

6.3. Computations in subsystems of λ^{ℓ}S4

While all the results of the previous sections are stated for the stronger system λ^{ℓ}S4, a careful inspection of the proofs shows that all the statements which apply to a given system still hold.

Theorem 6.15. Let λ^{ℓ}L one of λ^{ℓ}K, λ^{ℓ}KT, λ^{ℓ}K4, or λ^{ℓ}S4.

(i) Reduction in λ^{ℓ}L is confluent. (ii) Reduction in λ^{ℓ}L enjoys strong normalization.

7. Related work

In this brief section we relate our proposal to some of the recent work on natural deduction for modal logics. This is not the place for a detailed proof theoretical analysis of the different systems and, for this reason, we will discuss only those systems allowing a computational interpretation of proofs, the exception being the work presented next, which we take into account for its similarity with our system. For more detailed analysis of the proof theory of modal logic, we refer to [Min92] and [Wan93].

7.1. The “constructive” system of Benevides and Maibaum

Benevides and Maibaum [BM92], starting from a semantical intuition on Hintikka systems, propose a set of natural deduction rules for the □-based systems essentially analogous to our proposal. However, their semantical insight seems to hinder a full mastering of the level machinery. They introduce in their system redundant rules for the interaction between □ and the propositional connectives (see the rules R_{2} of their Section 3.2.2), which are derivable in the rest of the system. From a proof theoretical point of view these rules are hardly justified, since they do not obey to the tenet: “For each connective, (only) one introduction and (only) one elimination”. For this reason, it seems impossible to relate these systems to any clean sequent calculus for the same logics (see, contra, our Section 4.2.)

They prove the equivalence of their systems to the classical Hilbert style formulations. However, no notion of normalization of proofs is introduced. It is our belief that any study of the constructive content of a logical system cannot dispense from the study of proof normalization. If one does not tackle normalization, why not using the simple, naive approaches outlined in the Introduction?

7.2. The intuitionistic calculus of Bierman, Meré and de Paiva

In [BMdP92] is presented an approach to the □ modality essentially based on a variation of Prawitz proposal. The problematic □I rule has the form

Γ_{1} ; \begin{matrix}· \\ · \\ · \end{matrix} ; M_{1} : □σ_{1} … Γ_{n} ; \begin{matrix}· \\ · \\ · \end{matrix} ; M_{n} : □σ_{n}  [x_{1} : □σ_{1}, …, x_{n} : □σ_{n}] ; \begin{matrix}· \\ · \\ · \end{matrix} ; N : τ
□I
box N with M_{1}, …, M_{n} for x_{1}, …, x_{n} : □τ

For this system, the authors introduce several reduction rules corresponding to a categorical model and show its equivalence with the standard sequent calculus for S4.

It is clear that this system has some advantages over Prawitz’, since the rule □I is not as global as □I_{P} (see Section 4.1.) and allow a clearer reduction step. However, the approach seems specifically designed for S4, since it is not clear how the rule would scale to the normal subsystems of S4. Moreover, many of the critiques of the Introduction still apply to the proposed rule. In particular, a good introduction rule should construct its conclusion from all its premises and possibly some assumptions, a requirement clearly violated by the proposed □I.

7.3. The labelled natural deduction of Gabbay and de Queiroz

A completely different approach is the one proposed by Gabbay and de Queiroz in a sequel of papers, e.g. [GdQ92, GdQ91], as an attempt to give a general theory of natural deduction extending the Curry-Howard isomorphism to a large class of logics (classical, linear, relevant, modal). As for modalities, it offers a deductive (as opposed to model theoretic) account of the connections between modal logics and its propositional counterparts when world-variables are introduced in the functional calculus of the labels (i.e. when a little of the semantics is brought to the syntax, so to speak). [GdQ91]

The calculus is a kind of second order system, where second order objects, which syntactically are only variables, correspond to possible worlds. The basic rules for introduction and elimination of □ are:

Γ [𝕎 : U] ; \begin{matrix}· \\ · \\ · \end{matrix} ; M : σ ; □I ; Λ𝕎.M : □σ  \begin{aligned}Γ ; \begin{matrix}· \\ · \\ · \end{matrix} ; M : □σ & Δ ; \begin{matrix}· \\ · \\ · \end{matrix} ; 𝕋 : U \\ & □E \\ EX T R(M, 𝕋) : σ(𝕋) \end{aligned}

where U stands for an intended collection of “worlds.”

There is an certain analogy between our levels and the world-variables, which is especially clear in the case of the logic K. Moving to stronger logics, however, obscures this analogy. The characteristic axiom of KT, for instance, is not provable as is in their system; they can only prove its modal closure, □(□σ ⊃ σ) (it seems they would need a kind of second order constants to prove □σ ⊃ σ). In the case of K4, the proofs of the characteristic axioms are remarkably different in the two systems; while their proof consists of just a □I rule, in our case we have a □E followed by two □I.

References

[AP90] Jean-Marc Andreoli and Remo Pareschi. Logic programming with sequent systems: a linear logic approach. In Proc. of Workshop on Extensions of Logic Programming, Lecture Notes in Artificial Intelligence. Springer-Verlag, 1990.

[Bar84] Henk Barendregt. The Lambda Calculus: its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics. North-Holland, 1984. Revised Edition.

[Bar92] Henk Barendregt. Lambda calculus with types. In S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume II Background: Computational Structures, pages 118–310. Oxford University Press, 1992.

[BM92] M.R.F. Benevides and T.S.E. Maibaum. A constructive presentation for the modal connective of necessity (□). Journal of Logic and Computation, 2:31–50, 1992.

[BMdP92] Gavin Bierman, Claudia Meré, and Valeria de Paiva. Intuitionistic necessity revisited. In Logic at Work: Applied Logic Conference, 1992.

[BS84] R. Bull and K. Segeberg. Basic modal logic. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume II, pages 1–88. Reidel, 1984.

[CCM85] G. Cousineau, P.-L. Curien, and M. Mauny. The categorical abstract machine. In ACM Conference on Functional Programming and Computer Architecture, Nancy, France, 1985.

[Con86] Robert Constable. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986.

[Dos85] Kosta Dosen. Sequent-systems for modal logic. Journal of Symbolic Logic, 50:149–168, 1985.

[EH85] E. A. Emerson and J. Y. Halpern. Decision procedures and expressiveness in the temporal logic of branching time. Journal of Computer and System Science, 30:1–24, 1985.

[GdQ91] Dov M. Gabbay and Ruy J.G.B. de Queiroz. Labelled natural deduction. Imperial College, Preliminary Draft, 1991.

[GdQ92] Dov M. Gabbay and Ruy J.G.B. de Queiroz. Extending the curry-howard interpretation to linear, relevant and other resource logics. Journal of Symbolic Logic, 57:1319– 1365, 1992.

[Gir87] Jean-Yves Girard. Proof Theory and Logical Complexity. Bibliopolis, 1987.

[Mas92] Andrea Masini. 2-sequent calculus: A proof theory of modalities. Annals of Pure and Applied Logic, 58:229–246, 1992.

[Mas93] Andrea Masini. 2-sequent calculus: Intuitionism and natural deduction. Journal of Logic and Computation, 3:1–31, 1993. to appear.

[Mes92] José Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96:73–155, 1992.

[Min92] Grigori Mints. Selected Papers in Proof Theory. Bibliopolis, 1992.

[MMS92] Andrea Masini and Andrea Maggiolo-Schettini. TTL: A formalism to describe local and global properties of distributed systems. Theoretical Informatics and Applications, 2:115–149, 1992.

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

[MPW89] R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, I and II. Technical Report ECS-LFCS-89-85&86, University of Edinburgh, Dpt. of Computer Science, 1989.

[MTH90] Robin Milner, Mads Tofte, and Robert Harper. The Definition of Standard ML. The MIT Press, 1990.

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

[Pnu77] Amir Pnueli. The temporal logic of concurrent programs. In Proc. of ACM Symposium on Foundations of Computer Science, pages 45–57. IEEE, 1977.

[Pra65] Dag Prawitz. Natural Deduction. Acta Universitatis Stockholmiensis, Stockholm Studies in Philosophy 3. Almqvist & Wiksell, Stockholm, 1965.

[TvD88] Anne Troelstra and Dirk van Dalen. Constructivism in Mathematics, volume II. North-Holland, 1988.

[Wan93] H. Wansing. Sequent calculi for normal modal propositional logic. Journal of Logic and Computation, 1993. to appear.