Isabelle work on Interpolation for the Display Calculus for Tense Logic

Jeremy E. Dawson

November 15, 2012

1 Introduction

This document describes my attempts to prove interpolation for tense logic, using techniques similar to those used for classical logic, as described in the papers

James Brotherston & Rajeev Goré, Craig Interpolation in Displayable Logics (TABLEAUX 2011)

and the draft paper by Jeremy Dawson, James Brotherston & Rajeev Goré, currently called

“Machine-checked Interpolation Theorems for Substructural Logics using Display Calculi”.

Alternatively, this note could be read in conjunction with my note “Isabelle work on Interpolation for Display Calculi”

2 Comparison with Tableau Proofs

Recall that the general method of proof of the result for classical logic was to consider the property ldi below, which approximates to LADI in Brotherston & Goré, which is the property, of a given sequent S, that all sequents which are display-equivalent to S have interpolants.

This property was proved by induction over a derivation, which requires that each derivation rule preserves that property.

We can compare a proof by such a method to a proof using methods similar to those of Nguyen, Studia Logica 69 (2001), 41-57, whose proofs were for tableau systems. His method expressed in terms of a sequent system, could be described thus. Given a partition of the propositional variables into two sets, which we could call red and green, and a given sequent Γ_{R}, Γ_{G} ⊢ Δ_{R}, Δ_{G}, an interpolant K is a formula such that Γ_{R} ⊢ Δ_{R}, K and K, Γ_{G} ⊢ Δ_{G} where the variables in K appear both in Γ_{R}, Δ_{R} and in Γ_{G}, Δ_{G}.

Then, for a display rule such as X ⊢ A, Y ≡ X, ∗A ⊢ Y, supposing that A is a single variable, and so is either red or green (say it is red), then the requirements for an interpolant K of X ⊢ A, Y would be X_{R} ⊢ A, Y_{R}, K and K, X_{G} ⊢ Y_{G} whereas an interpolant K of X, ∗A ⊢ Y would satisfy X_{R}, ∗A ⊢ Y_{R}, K and K, X_{G} ⊢ Y_{G}. That is, this rule preserves interpolants.

This approach presupposes that the structure A is either red or green, and that X and Y are comma-separated lists of substuctures which are either red or green. Briefly, this mapping of Nguyen’s approach into display logic works because of the rules giving associativity and commutativity of the comma, and because a structure ∗(U, V) is display-equivalent to ∗U, ∗V.

When we consider the rule

\frac{X ⊢ A, B}{X ⊢ A ∨ B}  \frac{X ⊢ A X ⊢ B}{X ⊢ A ∧ B}

we must also note that the partition of variables into red and green is determined by the end-sequent which is simply X_{R} ⊢ Y_{G} — thus A and B in the rules above are the same colour.

Thus the proof method of Brotherston & Goré amounts to proving, inductively, that each derivable sequent, for each red-green colouring, has an interpolant in the red-green sense described above, by a proof method analogous to that of Nguyen.

We now discuss our attempts to extend the proof method of Brotherston & Goré to handle the display calculus for tense logic, and the problems that arose. It is interesting to reflect that attempting to extend Nguyen’s approach to tense logic would look rather different, and we will comment also on the difficulties in doing this.

3 Extending Brotherston & Goré to tense logic

Recall that the general method of proof is that, given a rule S′ ⟹ S we want to prove that it preserves the extended display interpolation property (EDI), that is, it satisfies the local display interpolation property (LDI). Thus, where S ≡ T , we want to find T′ such that S′ ≡ T′ and it is easy to see that, if T′ has an interpolant, then so does T . Then, if S′ satisfies EDI, then T′ has an interpolant, so T has an interpolant: that is, S satisfies EDI.

Furthermore, we generally define an appropriate relation between sequents T′ and T to facilitate the proof. For example, where S′ ⟹ S is an instance of the weakening rule, we consider the relation where T′ consists of T with a similar weakening, possibly “deep” (ie, weakening applied to some substructure). Or where S′ ⟹ S is the (⊢ □) rule, X ⊢ •A ⟹ X ⊢ □A, then the required relation is that T′ has •A in some antecedent position where T has □A instead.

The display rule which generally is involved in the difficulties is the (•) rule, X ⊢ •Y ≡ •X ⊢ Y.

3.1 The Contraction Rule

We note first that in the display calculus for tense logic, contraction and weakening are sensibly considered as integral, rather than as optional extras. This is because they are required to prove even □A ∧ □B ⊢ □(A ∧ B), via the derived rule •X, •Y ⊢ Z ⟹ •(X, Y) ⊢ Z.

Consider where S′ ⟹ S is an instance of the contraction rule, say •X, •X ⊢ Y ⟹ •X ⊢ Y, and let T be X ⊢ •Y. Then the natural choice for the relation between T′ and T is that T is obtained from T′ by contraction (possibly by multiple or deep contractions). The natural choice for the T′ might seem to be X, X ⊢ •Y but this is not display-equivalent to •X, •X ⊢ Y.

By way of a further example, suppose that X = (X′, X′′), and let T be X′ ⊢ ∗X′′, •Y. Then it is perhaps even clearer that the natural choice for T′ is either X′, X′ ⊢ ∗X′′, ∗X′′ • Y or X′, X′ ⊢ ∗(X′′, X′′) • Y, but these are not display-equivalent to •X, •X ⊢ Y.

To solve this problem we changed the definition of the local display interpolation property, and the related extended display interpolation property (EDI): we say S satisfies the EDI property if all sequents T such that S ⟹_{D} T have interpolants, where ⟹_{D} refers to derivability using some set of rules, and need not be an equivalence.

We did a “proof-of-concept” of this sort of change for classical logic, allowing weakening to be included in the definition of ⟹_{D}: in fact the proofs go through nicely, more easily, in fact, than in the original proof.

So for tense logic we tried this approach where we included the •-distribution rules

\frac{•X, •Y ⊢ Z}{•(X, Y) ⊢ Z}  \frac{Z ⊢ •X, •Y}{Z ⊢ •(X, Y)}

Note that we could not use the variant of these rules which require X = Y because some other lemmas rely on all the symbols in the premise of a rule in ⟹_{D} to be distinct.

Doing this dealt with the contraction rule easily.

3.2 The □ ⊢ rule, and equivalents

Here is the □ ⊢ rule as often presented, and the version we used (these are, by the (•) rule, equivalent).

\frac{X ⊢ A}{•X ⊢ □A}  \frac{X ⊢ A}{X ⊢ •□A}

Now if X ⊢ •□A is display-equivalent to T (not using the (•) rule), then there exists T′ which is display-equivalent to X ⊢ A, and in fact T has the same interpolant as T′. Here the relevant relation between T and T′ is that T′ has A in some succedent position where T has •□A.

But where we allow the (•) rule, further sequents which are display-equivalent to X ⊢ •□A can be got using the (•) rule, to give, first, •X ⊢ □A. Consider which display rules can then be applied: apart from a reverse application of the (•) rule, the only possibilities are the rules which add two stars.

Pursuing this line of analysis, we define the relation between sequents T and T′, called lseqrep Blob: (T, [T′]) ∈ lseqrep Blob … iff there exist T_{l}, T_{b} such that • T_{b} is equivalent to T by the rules which delete two stars

• T_{l} = T_{b} or these are related by a single application of the (•) rule

• T_{l} is related to T′ by changing •□A to A

To prove that

• with this relation, given T display-equivalent to X ⊢ •□A, there exists a related T′ display-equivalent to X ⊢ A, and

• if T′ has an interpolant, then so does T

was more difficult than for the logical introduction rules in the usual form, but nonetheless feasible.

However if you also add the (•)-distribution rules to the definition of EDI and LDI, then it becomes much more complicated. For example:

\frac{S′}{S} = \frac{A, •G ⊢ D}{•□A, •G ⊢ D} ⟹_{D} \frac{A, •G ⊢ D}{•(□A, G) ⊢ D} ≡ \frac{??A ⊢ ∗ • G, D??}{□A ⊢ ∗G, •D}

Here S is A, •G ⊢ D and S′ is •□A, •G ⊢ D (diagram, left). If we let T be •(□A, G) ⊢ D (diagram, centre) then we can use T′ = S′, but if we let T be □A ⊢ ∗G, •D (diagram, right) then what should we use for T′? If we let T′ be the sequent shown, A ⊢ ∗ • G, D, this is certainly display-equivalent to S, and if it has interpolant K then T has interpolant □K, but how can we describe the appropriate relation between T′ and T , if it exists?

Furthermore, let us make this example slightly more complicated by letting G = (B, ∗C). Then we could have

\frac{S′}{S} = \frac{A, •(B, ∗C) ⊢ D}{•□A, •(B, ∗C) ⊢ D} ⟹_{D} \frac{A, •(B, ∗C) ⊢ D}{•(□A, (B, ∗C)) ⊢ D} ≡ \frac{??}{□A, B ⊢ C, •D} = \frac{T′}{T}

In this diagram, what T′ can we put in place of ?? such that S′ ⟹_{D} T′, and such that we can get an interpolant for T = □A, B ⊢ C, •D from an interpolant for T′?

3.3 Some examples

We looked at examples based on the situation above, and their interpolants. Most simply, we let B = □(A → H) and C = ♢(H∧¬D). Then ¬C ⇔ □(H → D), so B ∧ ¬C ⇒ □(A → D). (This result will hold in all our subsequent examples, though we will have different B and C). Thus (B, ∗C) ⊢ •(∗A, D) will be derivable, as will •(B, ∗C) ⊢ (∗A, D). From these we can derive any of the following:

□A, B ⊢ C, □D ♢A, B ⊢ C, ♢D A, ■B ⊢ ■C, D A, ♦B ⊢ ♦C, D

with interpolants, respectively, □H, ♢H, ♦⊤ → H and ♦⊤ ∧ H.

An easy way to see derivation of these is as follows:

\begin{matrix}(B → C) ∨ □(A → D) \\ ■(B → C) ∨ (A → D) \end{matrix} ; (♦B → ♦C) ∨ (A → D) ; A ∧ ♦B → ♦C ∨ D ; A, ♦B ⊢ ♦C, D

We now look at more complex formulae for B and C. Let

B_{M} = M → N ∧ □(A → H) C_{M} = M → N ∧ ♢(H ∧ ¬D)

As above, B_{M} ∧ ¬C_{M} ⇒ □(A → D) is derivable, and similarly for B_{N}, C_{N}. Alternatively, note that B → C ⇒ B_{M} → C_{M}. Thus, these are derivable:

□A, B_{M} ⊢ C_{M}, □D ♢A, B_{M} ⊢ C_{M}, ♢D A, ■B_{M} ⊢ ■C_{M}, D A, ♦B_{M} ⊢ ♦C_{M}, D

The first two of these have interpolants M → N ∧ □H and M → N ∧ ♢H. For the latter two it is more difficult. For A, ♦B_{M} ⊢ ♦C_{M}, D an interpolant is ■M → ♦N ∧ H. For A, ■B_{M} ⊢ ■C_{M}, D an interpolant is ■(M → N) ∧ (♦M → H), or, equivalently, ♦M → ■(M → N) ∧ H.

Alternatively, let

B_{N} = N ∧ (M → □(A → H)) C_{N} = N ∧ (M → ♢(H ∧ ¬D))

Again, B_{N} ∧ ¬C_{N} ⇒ □(A → D) is derivable, as are

□A, B_{N} ⊢ C_{N}, □D ♢A, B_{N} ⊢ C_{N}, ♢D A, ■B_{N} ⊢ ■C_{N}, D A, ♦B_{N} ⊢ ♦C_{N}, D

The first two of these have interpolants N ∧ (M → □H) and N ∧ (M → ♢H). For A, ■B_{N} ⊢ ■C_{N}, D an interpolant is ■N ∧ (♦M → H). For A, ♦B_{N} ⊢ ♦C_{N}, D an interpolant is ■(N → M) → ♦N ∧H, or, equivalently, ♦N ∧ (■(N → M) → H).

I couldn’t see any constructive way of deriving these interpolants. A particular difficulty is that any display logic proof of the sequents involves sequents such as •(B, ∗C) ⊢ (∗A, D), where either B and C appear together, or A and D appear together. So interpolants of such sequents don’t help in finding an interpolant of (eg) A, ■B ⊢ ■C, D.

3.4 Towards an alternative proof system which gives interpolants

We tried to find a proof system which doesn’t move variables from one side to another. We could also think of this as a system where variables are coloured red or green, and retain those colours throughout, and interpolants are defined as in §2. Here the sequent •(B, ∗C) ⊢ (∗A, D), where A and B are red, and C and D are green, becomes

B ⊢ C A ⊢ D

that is, a list of sequents. What it means, semantically, is that for any worlds u, v, where uRv, B(u)∧A(v) ⟹ C(u)∨D(v). Equivalently, either (B ⟹ C)(u) or (A ⟹ D)(v).

This approach resembles the hypersequents of Restall, Proofnets for S5: sequents and circuits for modal logic, pages 151-172 in Logic Colloquium 2005, C. Dimitracopoulos, L. Newelski, and D. Normann (eds.), number 28 in Lecture Notes in Logic. Cambridge University Press, 2007. There a hypsersequent X_{1} ⊢ Y_{1}| … |X_{n} ⊢ Y_{n} means that given any worlds w_{1}, …, w_{n}, there is some i ∈ {1, …, n} such that X_{i} ⊢ Y_{i} holds at w_{i}.

Here are derivations in this system of some of the sequents derived above.

\begin{matrix}A, A → H ⊢ H ∧ ¬D, D & deep (□ ⊢), (⊢ ♢) & A, •□(A → H) ⊢ ∗ • ∗♢(H ∧ ¬D), D \\ (a) \\ □(A → H) ⊢  A ⊢ ∗ • ∗♢(H ∧ ¬D), D \end{matrix} ; (b) ; □(A → H) ⊢ ♢(H ∧ ¬D)  A ⊢ D ; B ⊢ C  A ⊢ D

Steps (a) and (b) allow moving a formula preceded by • or ∗•∗ to an adjacent sequent (creating it if necessary). Here the conclusion of (b) means ∀u, v such that uRv, either □(A → H) ⊢ ♢(H ∧ ¬D) at u or A ⊢ D at v.

The last sequent above is just an abbreviation of the previous one. Using purely classical logic steps we can get either of the following derivations

\frac{B ⊢ C  A ⊢ D}{B_{M} ⊢ C_{M}  A ⊢ D}  \frac{B ⊢ C  A ⊢ D}{B_{N} ⊢ C_{N}  A ⊢ D}

with B_{M}, C_{M}, B_{N}, C_{N} defined as shown, since, clearly, it is valid to perform any derivation on a single member of a list of sequents.

B_{M} = M → N ∧ □(A → H)  C_{M} = M → N ∧ ♢(H ∧ ¬D)
B_{N} = N ∧ (M → □(A → H))  C_{N} = N ∧ (M → ♢(H ∧ ¬D))

From B ⊢ C A ⊢ D (or, similarly, B_{M}, C_{M} or B_{N}, C_{N}) we can perform the following derivation

\begin{aligned}B ⊢ C  A ⊢ D & (c) & ⊢ C  A, ■B ⊢ D \\ & (d) \\ A, ■B ⊢ ■C, D \end{aligned}

∀u, v st uRv. (B ⟹ C)(u) or (A ⟹ D)(v)

∀u, v st uRv. C(u) or (A ∧ ■B ⟹ D)(v)

(A ∧ ■B ⟹ ■C ∨ D)(v)

\begin{aligned}B ⊢ C  A ⊢ D & (e) & B ⊢  A ⊢ ♦C, D \\ & (f) \\ A, ♦B ⊢ ♦C, D \end{aligned}

∀u, v st uRv. (B ⟹ C)(u) or (A ⟹ D)(v)
∀u, v st uRv. if B(u) then (A ⟹ ♦C ∨ D)(v)
(A ∧ ♦B ⟹ ♦C ∨ D)(v)

Each derivation is shown using rules for lists of sequents, with, on the right, the meanings of each of these sequents. Here the rules for steps (c) and (e) are instances of a general rule which permits moving a formula to a sequent to the right, with a ■ (antecedent) or ♦ (succedent). The rules for steps (d) and (f) permit introduction of ■ (succedent) or ♦ (antecedent) into the sequent on the right, which is only possible when the sequent on the left is being eliminated.

We also include all rules for a single sequent, applied to any sequent in a list, which do not shift a formula from left to right or vice versa. To compensate for the lack of a display property, we also allow “deep” application of inference rules. The rules involving • and multiple sequents in the list generalise to lists of sequents longer than just two, and we think that this approach gives a complete set of rules.

Now, hopefully the steps shown on the right have interpolants, which can be derived constructively, since the rules do not shift formulae from left to right, or vice versa.

Here we list the derivations on the right of the above (rewritten), without the ∀u, v, where

B = □(A → H) C = ♢(H ∧ ¬D)

\begin{matrix}A(v), B(u) ⊢ C(u), D(v) \\ A(v), (■B)(v) ⊢ C(u), D(v) \end{matrix} ; A(v), (■B)(v) ⊢ (■C)(v), D(v)

Note that the third line doesn’t follow from the second as written: the omitted “∀u” in the second line justifies this inference. In each case the interpolant is H(v). The following example is similar, and again the interpolant is H(v).

\begin{matrix}A(v), B(u) ⊢ C(u), D(v) \\ A(v), B(u) ⊢ (♦C)(v), D(v) \end{matrix} ; A(v), (♦B)(v) ⊢ (♦C)(v), D(v)

That is, the interpolant for both A, ■B ⊢ ■C, D and A, ♦B ⊢ ♦C, D is H.

3.4.1 Some more complex examples, using B_{M}, C_{M} or B_{N}, C_{N}

Now let us try more complex examples, replacing B, C with B_{M}, C_{M} or B_{N}, C_{N}, where

B_{M} = M → N ∧ □(A → H)  C_{M} = M → N ∧ ♢(H ∧ ¬D)
B_{N} = N ∧ (M → □(A → H))  C_{N} = N ∧ (M → ♢(H ∧ ¬D))

Examples, using B_{M}, C_{M} Then A(v), B_{M}(u) ⊢ C_{M}(u), D(v) has interpolant M(u) → N(u)∧H(v), as do A(v), (■B_{M})(v) ⊢ C_{M}(u), D(v) and A(v), B_{M}(u) ⊢ (♦C_{M})(v), D(v).

That is, for all u such that uRv (and where we write ∀u or ∃u, this implies u such that uRv), the following hold:

A(v), (■B_{M})(v) ⊢ M(u) → N(u) ∧ H(v)
A(v), (■B_{M})(v) ⊢ (∀u. M(u) → N(u) ∧ H(v))
A(v), (■B_{M})(v) ⊢ (∀u. M(u) → N(u)) ∧ ((∃u. M(u)) → H(v))
A(v), (■B_{M})(v) ⊢ (■(M → N))(v) ∧ ((♦M)(v) → H(v))
A, ■B_{M} ⊢ ■(M → N) ∧ (♦M → H)

Likewise, for all u such that uRv, we have:

M(u) → N(u) ∧ H(v) ⊢ C_{M}(u), D(v)
(∀u. M(u) → N(u) ∧ H(v)) ⊢ (∀u. C_{M}(u)), D(v)
■(M → N) ∧ (♦M → H) ⊢ ■C_{M}, D

so (■(M → N)) ∧ (♦M → H) is an interpolant for A, ■B_{M} ⊢ ■C_{M}, D By similar argument we have, for all u such that uRv,

A(v), B_{M}(u) ⊢ M(u) → N(u) ∧ H(v)
A(v), (∃u. B_{M}(u)) ⊢ (∃u. M(u) → N(u) ∧ H(v))
A(v), (♦B_{M})(v) ⊢ (∀u. M(u)) → (∃u. N(u)) ∧ H(v))
A, ♦B_{M} ⊢ ■M → ♦N ∧ H

Likewise, for all u such that uRv,

M(u) → N(u) ∧ H(v) ⊢ (♦C_{M})(v), D(v)
(∃u. M(u) → N(u) ∧ H(v)) ⊢ (♦C_{M})(v), D(v)
■M → ♦N ∧ H ⊢ ♦C_{M}, D

so ■M → ♦N ∧ H is an interpolant for A, ♦B_{M} ⊢ ♦C_{M}, D. A simpler approach to these particular examples follows: we have

∀v. ∀u. A(v), B_{M}(u) ⊢ M(u) → N(u) ∧ H(v) ⊢ C_{M}(u), D(v)

Therefore the following hold, for all v:

∀u. A(v), B_{M}(u) ⊢ ∀u. M(u) → N(u) ∧ H(v) ⊢ ∀u. C_{M}(u), D(v) ∃u. A(v), B_{M}(u) ⊢ ∃u. M(u) → N(u) ∧ H(v) ⊢ ∃u. C_{M}(u), D(v)

Now, except if there are no u such that uRv, we have

∀u. A(v), B_{M}(u) ≡ A(v), (■B_{M})(v)
∀u. C_{M}(u), D(v) ≡ (■C_{M})(v), D(v)
∃u. A(v), B_{M}(u) ≡ A(v), (♦B_{M})(v)
∃u. C_{M}(u), D(v) ≡ (♦C_{M})(v), D(v)

Finally, we have that

∀u. M(u) → N(u) ∧ H(v) ≡ (∀u. M(u) → N(u)) ∧ (∀u. M(u) → H(v))
≡ (■(M → N))(v) ∧ (♦M → H)(v)
∃u. M(u) → N(u) ∧ H(v) ≡ (∀u. M(u)) → (∃u. N(u)) ∧ H(v)
≡ (■M → ♦N ∧ H)(v)

Examples, using B_{N}, C_{N} Similarly A(v), B_{N}(u) ⊢ C_{N}(u), D(v) has interpolant N(u) ∧ (M(u) → H(v)), as do A(v), (■B_{N})(v) ⊢ C_{N}(u), D(v) and A(v), B_{N}(u) ⊢ (♦C_{N})(v), D(v).

Then similar arguments to the above give A, ■B_{N} ⊢ ■N ∧ (♦M → H) and ■N ∧ (♦M → H) ⊢ ■C_{N}, D, so ■N ∧ (♦M → H) is an interpolant for A, ■B_{N} ⊢ ■C_{N}, D.

Likewise, using the fact that N(u) ∧ (M(u) → H(v)) = (N(u) → M(u)) → (N(u) ∧ H(v)), similar arguments give A, ♦B_{N} ⊢ ■(N → M) → ♦N ∧ H and ■(N → M) → ♦N ∧ H ⊢ ♦C_{N}, D, so ■(N → M) → ♦N ∧ H is an interpolant for A, ♦B_{N} ⊢ ♦C_{N}, D.

In more detail, the interpolant N(u) ∧ (M(u) → H(v)) gives interpolants in the modal logic as follows:

∀u. N(u) ∧ (M(u) → H(v)) ≡ (∀u. N(u)) ∧ (∀u. M(u) → H(v))
≡ (■N)(v) ∧ (♦M → H)(v)
∃u. N(u) ∧ (M(u) → H(v)) ≡ ∃u. (N(u) → M(u)) → (N(u) ∧ H(v))
≡ (∀u. N(u) → M(u)) → (∃u. N(u) ∧ H(v))
≡ (■(N → M))(v) → (♦N ∧ H)(v)

We now need to look at to what extent these construction of interpolants can be generalised. Recall that at the end of §3.3 we found these interpolants but said “I couldn’t see any constructive way of deriving these interpolants.” In §3.4 we have found these same interpolants in a more constructive way, but the question remains as to how much this can be generalised.

It should be possible to mimic derivations using lists of sequents by derivations involving expressions such as ∀u, v st uRv. A(v), B_{M}(u) ⊢ C_{M}(u), D(v) and since these derivations do not move formula from left to right or vice versa, it should be generally possible to construct an interpolant (such as M(u) → N(u) ∧ H(v) in this example).

From there we had the problem that we had to be able to express ∀u. M(u) → N(u) ∧ H(v) or ∃u. M(u) → N(u) ∧ H(v) as F (v) for some formula F. This should be generally possible, as in an example like the ones given (where we aim to get a sequent in terms of v by eliminating u), we could

• express the formula in conjunctive or disjunctive (respectively) normal form,

• in each conjunct (disjunct) collect the disjuncts (conjuncts) involving u together, and those involving v • apply the quantifier just to the disjuncts (conjuncts) involving u

• turn these into formulae using ■ or ♦

4 Using only rules which don’t move formulae from side to side

We tried to devise a proof system which has the property that formulae are not moved from side to side of a sequent. Then there should be no difficulty in showing that rules preserve the existence of an interpolant. For example, the standard sequent rule for modal logic, preserves interpolants because if K is an interpolant for the numerator, then □K is an interpolant for the denominator.

\frac{Γ ⊢ A}{□Γ ⊢ □A}(□)  \frac{X, Y ⊢ Z}{X ⊢ ∗Y, Z} (ca1)  \frac{X ⊢ Y}{∗Y ⊢ ∗X} (∗)  \frac{∗(X, Y) ⊢ Z}{∗X, ∗Y ⊢ Z} (∗-dist ⊢)

The obvious first requirement for this is that we do not use the comma rules such as (ca1) above (although it is alright to use the (*) rule, since an interpolant K for the numerator gives the interpolant ¬K for the denominator). Also we can allow certain derived rules such as (∗-dist ⊢), shown.

This means that we must allow deep application of rules, such as

\frac{X[A] ⊢ Y}{X[•□A] ⊢ Y} (□ ⊢)

where A is a succedent part of X[A], etc.

Now if we avoid using the rules like (ca1), this creates a problem for proofs like

\begin{matrix}\begin{matrix}•B, C ⊢ ∗ • ∗X \\ •B, • ∗ X ⊢ ∗C \end{matrix} & (•-dist ⊢) & •(B, ∗X) ⊢ ∗C \\ B, ∗X ⊢ • ∗ C \end{matrix} ; B, ∗ • ∗C ⊢ X

We can simply include this (and others like it) as a derived rule. Our hope is that no proof really needs to bring (here) B and X together under a • since they eventually get separated (assuming the sequent to be proved eventually has B and X on the opposite sides.

There remains a problem with contraction. If we disallow rules such as (ca1), we need to allow the following rule:

\frac{A ⊢ ∗A, X}{A ⊢ X} (ctr)

which does not (obviously) preserve the property of having an interpolant.

4.1 Is contraction admissible?

So, can we do without contraction?

We need the rule (•-dist ⊢)

\frac{•(X, Y) ⊢ Z}{•X, •Y ⊢ Z} (•-dist ⊢)

which is proved using contraction — so let us include it as a derived rule (which does not cause a problem for interpolation). Having included this rule we can limit the need for contraction to formulae, by virtue of the rules (•-dist ⊢ ), (∗-dist ⊢), commutativity and associativity. This was proved in Isabelle, theorem fml ctr. This may make the proof of admissibility of contraction simpler.

Having included the (•-dist ⊢) rule, and shown that we then need contraction for (at most) formulae only, can we do without contraction completely? This would require modifying all the logical introduction rules to include a copy of the principal formula in the premises, for example changing the rule on the left below to the one on the right.

\frac{X ⊢ A, B}{X ⊢ A ∨ B}  \frac{X ⊢ A, B, A ∨ B}{X ⊢ A ∨ B}

4.1.1 Proof of some contraction admissibility result

The natural way of proving that contraction is admissible is to consider a sequent A, A ⊢ X, and prove it by induction on the derivation of that sequent. Thus, for example, when the previous step in the derivation of A, A ⊢ X is say A, A ⊢ X′, we assume as the inductive hypothesis that if A, A ⊢ X′ is derivable then A ⊢ X′ is derivable. Since A, A ⊢ X′ is derivable, we have that A ⊢ X′ is derivable and now the last step is that therefore A ⊢ X is derivable.

But if the last step is one of the display postulates, for example

\frac{A ⊢ X, ∗A}{A, A ⊢ X}  \frac{•(A, A) ⊢ X}{A, A ⊢ •X}  \frac{∗X ⊢ ∗(A, A)}{A, A ⊢ X}

this proof method doesn’t seem to work unless we set the property of a sequent S, to be proved by induction on the derivation of S is as follows: that any sequent S′, got by applying any sequence of rules from the set R to S, is derivable without using contraction. And considering the rules above, it appears that R needs to consist of at least the display postulates and formula contractions.

Note that the last step may be another contraction, from A, A, A ⊢ •X. Thus we need to allow the sequence of steps from S to S′ to contain multiple contraction steps.

Considering now the •-distribution rule, we may have the derivation step

\frac{•A, •A ⊢ X}{•(A, A) ⊢ X} ( = S)

Here, since display postulates (rules in R) and contraction give •A ⊢ X from S, we want to prove that •A ⊢ X is derivable without using contraction. For this we need to add •-distribution to R; then, since rules in R and contraction give •A ⊢ X from •A, •A ⊢ X the inductive hypothesis gives that •A ⊢ X is derivable without using contraction.

Now, to make contraction admissible the natural approach is to add the principal formula of logical introduction rules to the premises. Thus for example the rule on the left becomes the rule on the right.

\frac{A′ ⊢ X}{A ⊢ X}  \frac{A′, A ⊢ X}{A ⊢ X}

Then, any sequence of display postulates from A ⊢ X (to get, say, Z[A] ⊢ X) can be reproduced as a sequence of display postulates from A′, A ⊢ X to get Z[A′, A] ⊢ X. Then, when Z[A] ⊢ X admits contraction on A (say Z[A] is Y [A, A]), Z[A′, A] is Y [(A′, A), A], from which associativity and contraction gives Y [A′, A]. By the inductive hypothesis, the sequent Y [A′, A] ⊢ X is derivable without using contraction. Then the modified form of the introduction rule gives Y [A] ⊢ X, which is the result of contracting Z[A] ⊢ X. This is the usual way of proving contraction admissibility.

However, now that we have enlarged R to include the •-distribution rules, this does not seem to work. Consider the proof step (on the right) using the rule on the left.

\frac{•□A, A ⊢ X}{•□A ⊢ X}  \frac{•□A, A, •G ⊢ X}{•□A, •G ⊢ X} ( = S)

Now, from S a sequence of rules in R, where G′ ≡ G and from G′ you can obtain □A, G′′, gives

\begin{matrix}•□A, •G ⊢ D \\ •□A, •(□A, G′′) ⊢ D \end{matrix} (•-dist) •(□A, □A, G′′) ⊢ D

(ctr) •(□A, G′′) ⊢ D

So what can we get from the numerator that corresponds to this? We want to do a contraction on □A, see below.

\begin{matrix}•□A, A, •G ⊢ D \\ •□A, A, •(□A, G′′) ⊢ D \end{matrix} (•-dist) •(□A, □A, G′′), A ⊢ D

(ctr) •(□A, G′′), A ⊢ D

Then we have the inductive result that •(□A, G′′), A ⊢ D is derivable without the use of contraction. We then want to use the logical introduction rule to remove the A, but we can’t.

What to do?

Here the good news is that it is logically valid to go from •(□A, G′′), A ⊢ D to •(□A, G′′) ⊢ D. How to do this in a way which is simplest and most general?

4.1.2 The system DKt

In [2], a system DKt of rules is given for tense logic. DKt does not include contraction, and contains logical introduction rules for □, ■, ∧ and ∨ which have the principal formula copied into the premises. DKt is a deep inference system, working on multisets of formula (like the right-hand side of a sequent).

The rules called ♢_{1} and ♢_{2} are shown, translated into sequents, and with our connectives, without showing the deep inference.

\frac{X ⊢ •(Δ, A), ♢A}{X ⊢ •Δ, ♢A}(♢_{1})  \frac{X ⊢ ∗ • ∗(Δ, ♢A), A}{X ⊢ ∗ • ∗(Δ, ♢A)}(♢_{2})  \frac{•(□A, G′′), A ⊢ D}{•(□A, G′′) ⊢ D}

Here we note that the rule (♢_{2}) is equivalent to the rule on the right which is exactly what we need in the example discussed above.

We now have a complete contraction-free system. How does it go for proving interpolation? We need to consider interpolation in the sense where formula in the conclusion are coloured red or green. The rule (♢_{1}) does not look good for this because it may be that Δ is red and A is green, or vice versa, and they get put together in the premises.

However this rule could also be seen as (1) below

\frac{□B ⊢ □(B → D)}{□B ⊢ □D}(1) \frac{□B ⊢ □(B′ → D)}{□B ⊢ □B′ → □D}(2)

This can be proved using the interpolation-friendly rule (2) (by setting B′ = B), but then to prove □B ⊢ □B → □D requires propositional logic including contraction.

Can we replace (♢_{1}) with some interpolation-friendly rule without requiring contraction?

Alternatively, note that the rule is like a combination of the rule (3) (equivalent to (3’)) with contraction, and, given that weakening is admissible, (♢_{1}) makes (3) admissible.

\frac{X ⊢ •(Δ, A)}{X ⊢ •Δ, ♢A}(3) \frac{X ⊢ □(Δ, A)}{X ⊢ □Δ, ♢A}(3′)

5 Conclusion and Discussion

We have recounted the difficulties we found in adapting the proof of Brotherston & Goré of interpolation for the display calculus for classical propositional logic to tense logic. Considering the proof of Nguyen for tableau systems for modal logic we could relate his proof method to the proof for the display calculus for classical logic. However, when applied to tense logic, these two proof methods no longer show a simple correspondence. We described the difficulties encountered in attempting to use the display calculus proof method (involving the local display interpolation property) for tense logic.

Having devised some rather difficult examples, we examined how an interpolant for these might be constructed, and devised an alternative calculus for proofs in tense logic, involving lists of sequents, where each sequent in the list applies to different worlds. We gave examples of how to find interpolants for our difficult examples based on proofs using this calculus, suggesting that this calculus might enable a constructive proof of the interpolation property for tense logic.

References

[1] James Brotherston & Rajeev Goré. Craig Interpolation in Displayable Logics In Proc. Tableaux, 2011. DETAILS

[2] R Goré, L Postniece and A Tiu. On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics. Logical Methods in Computer Science 7 (2:8) 2011.