From Gabbay-style rules to labelled deduction

Patrick Blackburn

Abstract

Is there a link between Gabbay-style rules, modal languages with nominals, and labelled deduction? It seems there should be: though they differ in many ways, all share the idea that state-names are important in modal deduction. I shall show how to move from a Gabbay-style rule to labelled deduction via the basic hybrid language. I finish with a discussion of the place of state-names in modal logic.

Contents

1 The basic hybrid language 2

2 From Gabbay-style rules to sequent calculus 2

3 From sequent calculus to labeled deduction 4

4 Sorting and modality 6

1 The basic hybrid language

Fix a set of nominals (typically written i, j, k) and a set of propositional variables (typically written p, q, r) and define:

WFF := i | p | ¬φ | φ ∧ ψ | φ ∨ ψ | φ → ψ | ◇φ | □φ | @_{i}φ.

For any nominal i, the symbol sequence @_{i} is called a satisfaction operator. The basic hybrid language is interpreted on models M = (W, R, V) where V is a valuation that assigns every nominal a singleton subset of W; we call the unique element of V (i) the denotation of i. The language is interpreted in the expected way (nominals are just atomic formulas), the clause for satisfaction operators being:

M, w ⊧ @_{i}φ iff M, i ⊧ φ, where i is the denotation of i under V.

Note that each satisfaction operator is a normal modal operator.

The satisfiability problem for the basic hybrid language is no more complex than that for ordinary modal logic (that is, PSPACE-complete; see Areces, Blackburn and Marx [1]) so the basic hybrid language seems to be offering something for nothing. But what exactly? The power to create modal theories of state equality and state succession: @_{i}j says that the states denoted by i and j are identical, while @_{i}◇j says that the denotation of j is an R-successor of the denotation of i. This is precisely what is required to turn Gabbay-style rules into sequent calculus.

2 From Gabbay-style rules to sequent calculus

Nearly twenty years ago, Dov Gabbay [9] augmented the standard Hilbert axiomatization of modal logic with a new kind of proof rule. His idea has proved influential and a wide range of similar rules have been developed for many modal languages. Now, such rules trade on the idea of labeling states; what do they look like when we have nominals at our disposal?

One answer is provided by the COV rule, the workhorse of the Sophia school (see Passy and Tinchev [13], Gargov and Goranko [10]). Here’s a (somewhat simpler) answer. Let s and t be metavariables over nominals, and let ◇_{s}φ be an abbreviation for ◇(s ∧ φ). Then:

\frac{⊢ ◇_{t} ⋯ ◇_{s}◇_{a}φ → σ}{⊢ ◇_{t} ⋯ ◇_{s}◇φ → σ} [Gabbay]

(Here a is a nominal distinct from s, ⋯, t that does not occur in φ or σ.)

This is a genuinely useful rule. With its help we can build models in which each state is labelled by a nominal, and thus prove general completeness proofs very straightforwardly. But it’s still rather complex: its “active” part (the occurrence of the new nominal a) is embedded under arbitrarily deep embeddings of diamonds.

Here’s where the satisfaction operators help. Instead of laboriously chaining our way through from t to s, we can use @_{s} to enforce the desired behavior at s directly. Doing so collapses the stack of nested diamonds to depth one:

\frac{⊢ @_{s}◇_{a}φ → σ}{⊢ @_{s}◇φ → σ} [Paste]

But this is just a thinly disguised sequent rule: get rid of the ⊢ symbols, turn the material implication arrow → into the sequent arrow ⟶, expand the ◇_{a} abbreviation, and simplify the conjunction:

\frac{@_{s}◇a, @_{a}φ ⟶ σ}{@_{s}◇φ ⟶ σ}

This works in arbitrary deductive contexts, so add a lefthand context Γ, and turn σ into a righthand context Σ, thus obtaining a diamond-on-the-left sequent rule:

\frac{@_{s}◇a, @_{a}φ, Γ ⟶ Σ}{@_{s}◇φ, Γ ⟶ Σ} [◇L]

Gabbay-style rules are usually thought of as additions to modal Hilbert systems. But once we have seen that @ lends itself towards defining sequent rules, the way lies open to eliminating the Hilbert component altogether. Here’s a selection of @-driven sequent rules for other connectives (and a diamond-on-the-right rule). As before, s and t are metavariables over nominals, and a is a metavariable over new nominals:

\frac{Γ ⟶ Σ, @_{s}φ}{@_{s}¬φ, Γ ⟶ Σ} [¬L]  \frac{@_{s}φ, Γ ⟶ Σ}{Γ ⟶ Σ, @_{s}¬φ} [¬R]

\frac{Γ ⟶ Σ, @_{s}φ @_{s}ψ, Γ ⟶ Σ}{@_{s}(φ → ψ), Γ ⟶ Σ} [→L]  \frac{@_{s}φ, Γ ⟶ Σ, @_{s}ψ}{Γ ⟶ Σ, @_{s}(φ → ψ)} [→R]

\frac{@_{t}φ, Γ ⟶ Σ}{@_{s}@_{t}φ, Γ ⟶ Σ} [@L]  \frac{Γ ⟶ Σ, @_{t}φ}{Γ ⟶ Σ, @_{s}@_{t}φ} [@L]

\frac{@_{s}◇a, @_{a}φ, Γ ⟶ Σ}{@_{s}◇φ, Γ ⟶ Σ} [◇L]  \frac{Γ ⟶ Σ, @_{t}φ}{@_{s}◇t, Γ ⟶ Σ, @_{s}◇φ} [◇R]

\frac{@_{t}φ, Γ ⟶ Σ}{@_{s}□φ, @_{s}◇t, Γ ⟶ Σ} [□L]  \frac{@_{s}◇a, Γ ⟶ Σ, @_{a}φ}{Γ ⟶ Σ, @_{s}□φ} [□R]

The basic hybrid language embodies theories, namely modal theories of state equality and state succession, so we need to cope with these too. The following rules handle the theory of state equality:

\frac{@_{s}s, Γ ⟶ Σ}{Γ ⟶ Σ} [Ref] \frac{@_{s}t, Γ ⟶ Σ}{@_{t}s, Γ ⟶ Σ} [Sym] \frac{@_{s}φ, Γ ⟶ Σ}{@_{s}t, @_{t}φ, Γ ⟶ Σ} [Nom]

(Note that transitivity is covered by Nom; simply instantiate φ to any nominal.) To cope with the theory of state succession we add:

\frac{@_{s}◇φ, Γ ⟶ Σ}{@_{s}◇t, @_{t}φ, Γ ⟶ Σ} [Bridge]

And (together with weakening and contraction) that’s it. Jerry Seligman [16, 17], in his work on situated deduction, seems to have been the first to use satisfaction operators to drive sequent calculi. The Paste rule is from Blackburn and Tzakova [4].

3 From sequent calculus to labeled deduction

Sequent calculi are somewhat abstract. Let’s convert this calculus into a more concrete tableau system. Doing so will lead us to labelled deduction (see Fitting [7], Gabbay [8]). Here are the rules for the connectives:

\frac{@_{s}¬φ}{¬@_{s}φ} [¬]  \frac{¬@_{s}¬φ}{@_{s}φ} [¬¬]

\frac{@_{s}(φ → ψ)}{¬@_{s}φ | @_{s}ψ} [→]  \frac{¬@_{s}(φ → ψ)}{@_{s}φ} [¬→]
¬@_{s}ψ
\frac{@_{s}@_{t}φ}{@_{t}φ} [@]  \frac{¬@_{s}@_{t}φ}{¬@_{t}φ} [¬@]

\frac{@_{s}◇φ}{@_{s}◇a} [◇]  \frac{¬@_{s}◇φ @_{s}◇t}{¬@_{t}φ} [¬◇]
@_{a}φ
\frac{@_{s}□φ @_{s}◇t}{@_{t}φ} [□]  \frac{¬@_{s}□φ}{@_{s}◇a} [¬□]
¬@_{a}φ

These are essentially upside down versions of the sequent rules. Read the □-rule as follows: whenever a pair of formulas of the form @_{s}□φ and @_{s}◇t can be found on some branch of the tableau, we are free to extend that branch by adding @_{t}φ. The ¬◇-rule works similarly.

Next we must convert our sequent rules for the modal theory of state equality:

\frac{[s occurs on the branch]}{@_{s}s} [Ref]  \frac{@_{t}s}{@_{s}t} [Sym]  \frac{@_{s}t @_{t}φ}{@_{s}φ} [Nom]

Finally, here’s the tableau rule for the modal theory of state succession:

\frac{@_{s}◇t @_{t}φ}{@_{s}◇φ} [Bridge]

As is usual with tableau systems, we prove formulas by systematically trying to falsify them. So suppose we want to prove φ. Choose a nominal (say i) that does not occur in φ (this acts as a name for the putative falsifying state), prefix φ with ¬@_{i}, and start applying rules. Let’s apply this procedure to the modal distribution axiom □(p → q) → (□p → □q):

1  ¬@_{i}(□(p → q) → (□p → □q))
2  @_{i}□(p → q)  1, ¬→
2′  ¬@_{i}(□p → □q)  Ditto
3  @_{i}□p  2′, ¬→
3′  ¬@_{i}□q  Ditto
4  @_{i}◇j  3′, ¬□, j
4′  ¬@_{j}q  Ditto
5  @_{j}p  3, 4, □
6  @_{j}(p → q)  2, 4, □
7  ¬@_{j}p  | @_{j}q  6, →
⊗ 5, 7 ⊗  ⊗ 4′, 7 ⊗

I want to make two points about this system. The first is this: the link with Gabbay-style labelled deduction is transparent. Here’s the labelled deduction rule for ◇:

@_{s}◇φ
create a, sRa, and @_{a}φ

In essence, this is simply our ◇-rule (and hence, chasing back through the chain sketched above, the ◇L-rule, the Paste rule, and ultimately the Gabbay rule). In fact, the only real difference is that in Gabbay-style labelled deduction we manipulate labels metalinguistically (in effect, we make use of a programming language containing expressions such as ‘create’, ‘and’, ‘R’, ‘:’, and a supply of labels, to manipulate object language formulas) whereas the basic hybrid language is expressive enough to support the required deduction steps at the object level.

And this leads to my second point. Something interesting happens when we view labelled deduction through the lens of the basic hybrid language: labelling discipline becomes logic.

Gabbay has repeatedly emphasized that labelled deduction is as much about the labelling algebra that drives the proof process as it is about labels themselves. For example, he adapts modal labelled deduction to various frame classes by altering the rules that govern how the labelling algebra manipulates labels. But our labels are formulas. They play a full fledged role in the logical economy (they can be negated, conjoined, prefixed by modalities, and so on). There is no need to impose labelling discipline on nominals via an external algebra; discipline emerges from the semantics of the basic hybrid language. In fact, when used an axiom, any pure formula (that is, a formula containing no propositional variables) is complete with respect to the class of frames it defines. For example any instance of s → ¬◇s defines irreflexivity, and any instance of ◇◇s → ◇s defines transitivity, so if we are able to introduce these into tableau proofs, we obtain complete tableau system for strict pre-orders. (You may find it interesting to give a tableau proof of i → □(◇i → i), the formula which defines antisymmetry, with the help of these axioms.)

It has long been known that pure formulas lead to general completeness theorems: see for example see Bull [5], Passy and Tinchev [13], Gargov and Goranko [10], and Blackburn and Tzakova [4]. The link between tableau systems for the basic hybrid language and Gabbay-style labelled deduction is discussed in Blackburn [3]. Tableau systems intermediate between Gabbay-style labelled deduction and the pure object-level system just described are discussed in Tzakova [19]; similar “mixed level” sequent systems have been explored in recent unpublished work by Jerry Seligman.

4 Sorting and modality

The links I have sketched may be interesting, but are they genuinely modal? After all, the ‘glue’ was provided by the basic hybrid language, whose ability to form theories of state equality and succession is clear departure from modal orthodoxy.

But the history of modal logic is essentially the story of relatively rigid forms of semantic analysis, such as the state descriptions in Carnap [6], giving way to more flexible accounts, notably the relativized semantics of Kripke [11, 12], and, a decade later, the general frames of Thomason [18]. Most of the semantical freedom we currently enjoy stems either from the Kripkean parameter (the idea that by making the transition relation R explicit and varying its properties we can control logics) or the Thomasonian parameter (defining validity not in terms of all valuations on a frame, but in terms of some well-behaved subcollection).

Hybrid languages can be seen as exploiting a third semantic parameter, a parameter which emerged in the later work of Arthur Prior [14, 15]. Like the Thomasonian parameter, the Priorean parameter is based on the idea of restricting the available valuations, but it does so differently, and with different aims in mind: the point is not to liberalize the notion of validity, it is to make explicit the different sorts of proposition we are manipulating and reveal their logic. Thus it was that Prior (and Bull [5]) were led to the idea of sorted atomic symbols, of which the nominal is the simplest example. The glory of their idea is that the initial departure from standard syntax is minimal (what could be simpler than sorting the atomic symbols?), fruitful (even nominals lead to richer logics), and suggestive (it leads to novel ideas such as satisfaction operators and tools for binding nominals). And viewed from the present day perspective, when, largely thanks to the influence of Johan van Benthem (see for example [2]), modal logic is increasingly viewed as an abstract tool for manipulating information, Prior’s ideas seem strikingly prescient: via the familiar Kripkean parameter we gain control over how the information is distributed, and via Prior’s use of sorted propositions we gain additional insight into the way it is organized.

References

[1] C. Areces, P. Blackburn, and M. Marx. Hybrid logics. Characterization, Interpolation and Complexity. CLAUS-Report 104, 1999, http://www.coli.uni-sb.de/cl/claus.

[2] J. van Benthem. Language in Action. North-Holland, 1991.

[3] P. Blackburn. Internalizing labelled deduction. CLAUS-Report 102, 1998, Computerlinguistik, Universität des Saarlandes, http://www.coli.uni-sb.de/cl/claus. To appear in Journal of Logic and Computation.

[4] P. Blackburn and M. Tzakova. Hybrid languages and temporal logic. Logic Journal of the IGPL, 7(1):27–54, 1999. http://www.oup.co.uk/igpl.

[5] R. Bull. An approach to tense logic. Theoria, 36:282–300, 1970.

[6] R. Carnap. Modalities and quantification. Journal of Symbolic Logic, 11:33–64, 1946.

[7] M. Fitting. Proof Methods for Modal and Intuitionistic Logics. Reidel, 1983.

[8] D. Gabbay. Labelled Deductive Systems. Oxford University Press, 1996.

[9] D. Gabbay. An irreflexivity lemma. In U. Mönnich, editor, Aspects of Philosophical Logic, pages 67–89. Reidel, 1981.

[10] G. Gargov and V. Goranko. Modal logic with names. Journal of Philosophical Logic, 22(6):607–636, 1993.

[11] S. Kripke. A completeness theorem in modal logic. Journal of Symbolic Logic, 24:1–14, 1959.

[12] S. Kripke. Semantical considerations on modal logic. Acta Philosphica Fennica, 16:83– 94, 1963.

[13] S. Passy and T. Tinchev. An essay in combinatory dynamic logic. Information and Computation, 93:263–332, 1991.

[14] A. Prior. Past, Present and Future. Oxford University Press, Oxford, 1967.

[15] A. Prior and K. Fine. Worlds, Times, and Selves. University of Massachusetts Press, 1977.

[16] J. Seligman. A cut-free sequent calculus for elementary situated reasoning. Technical Report HCRC-RP 22, HCRC, Edinburgh, 1991.

[17] J. Seligman. The logic of correct description. In M. de Rijke, editor, Advances in Intensional Logic, pages 107–135. Applied Logic Series, Kluwer, 1997.

[18] S. Thomason. Semantic analysis of tense logic. Journal of Symbolic Logic, 37:150–158, 1972.

[19] M. Tzakova. Tableaux calculi for hybrid logics. To appear in proceedings of Tableaux ‘99.