Comments on Groeneveld and Veltman’s “Inference Systems for Update Semantics”

Johan van Benthem

This paper is an interesting theoretical contribution to understanding various forms of dynamic inference in update semantics. It contains many different motives and observations, but its guiding idea is the search for generality by bringing in standard perspectives from modal and dynamic logic. I will list some main improvements achieved over the existing literature, and mention some desiderata for further research. As a personal offering to DYANA, I start with some panoramic considerations on the broader research agenda in this area, partly inspired by Groeneveld and Veltman’s work.

Logical Foundations of Dynamic Inference

Dynamic inference may be loosely described as the kind of non-standard inference that comes up in various forms of dynamic semantics. Logical foundations in this area concern the broad picture. What is general and what is specific about the behaviour found in particular systems? Here are some major issues that come up.

Abstract and Concrete Update Semantics What kind of modelling is chosen for the relevant states, and also, what kind of update procedures over these? In particular, states can be highly abstract (labeled transition systems, Kripke models) or more concrete (variable assignments, sets of valuations, discourse representations), as in Amsterdam- or Utrecht-style manifestations of update semantics. Likewise, one can think of update procedures as abstract binary transition predicates (as in operational semantics for imperative programs) or as more specific deterministic functions. The more abstract perspective gives us some kind of general dynamic logic. A key question is what further effects arise from greater concreteness, perhaps, and preferably, particular to natural language.

What is Dynamic Inference? The easy technical answer to this question is: the proof theory of update semantics. Even so, there are some intriguing conceptual questions. Given such a system, which notion of inference is taken (e.g., test-test, update-test, update-update)? Is there just one good candidate? What are the relations between the proposals that have already been made? Can we get a uniform perspective on useful candidates? For instance, it seems significant in some sense that four notions of dynamic inference proposed for different purposes in Amsterdam fit together rather nicely as forward/ backward pairs. Groenendijk and Stokhof say ’if you can process your premises, then you can process your conclusion at the end’, while van Eyck & de Vries have ’if you can process your premises, then you can process your conclusion at the start’. Veltman says ’if you can process your premises, then the conclusion loops at the end’, while Beaver’s account of presupposition says ’if you can process your premises, then the conclusion loops at the start’. There is system to this variety. More radically, however, in the long run: should not we use this occasion, and completely rethink what ’inference’ is in a dynamic setting? For instance, the interplay between ’updating’ and ’inferring’ seems to suggest a division of labour unlike that found in standard conceptions of logical consequence. In that light, it is a moot point what the carriers of dynamic ’inference’ should be.

Relations with Traditional Logical Systems There are various effective translations running from systems of update semantics into classical logics over the same models. This simple point has generated some heat, but it really does not say more (or less) than similar observations elsewhere in logic, e.g., in modal logic vis-a-vis first-order predicate languages over possible worlds models. Sometimes, not always, meta-properties of dynamic systems can be predicted a priori from those for classical ones. Examples are effective axiomatizability and decidability for most current propositional update systems, whereas more delicate cases concern interpolation or preservation properties. This fruitful interaction is well-documented in the correspondence theory of modal logic. The new information one wants in any case lies in explicit axiomatizations for dynamic calculi, high-lighting their characteristic behaviour. A reasonable question, still, concerns the complexity of what emerges, with the classical analogy serving as a yard-stick of common sense. For instance, basic propositional update semantics is a subsystem of S5. It would be disappointing if its axiomatization turned out very complicated and hard to handle.

Proof Theory Which syntactic format is most suitable for axiomatizing dynamic inference? Most of us have followed the lead of the dominant tradition, both in classical proof theory and in the field of non-monotonic logics, employing Gentzen sequents. But there is an issue here (see above). Is dynamic inference naturally ’Gentzenizable’? Should it be? Whatever format is chosen, a certain hierarchy of principles will arise. There are bare structural rules defining the ’basic practice’ of some dynamic style of inference, there are ’logical rules’ governing the logical connectives of the language, and there may be various intermediate rules (such as structural rules only for special kinds of formulas). In all this, one may distinguish between what is already valid in the underlying abstract semantics, and what are concrete peculiarities of some specific class of update models. There will be certain technical differences in emphasis here. With abstract structural rules, one often gets by with simple representation theorems for dynamic inference styles, whereas the full language requires more elaborate completeness theorems.

These general considerations generate many more specific questions concerning proposed axiomatizations of update semantics. Here are a few, which will naturally occur to a reader of Groeneveld and Veltman’s paper. Which notion of validity should be chosen for structural rules: ’local’ (truth-to-truth, usually simple RE) or ’global’ (validity-to-validity, often complex)? Which vocabulary of dynamic connectives is appropriate? E.g., sometimes, purely structural behaviour is uninformative, whereas the natural principles only come out in the presence of composition. An example is the inference of Groenendijk & Stokhof. In its abstract form, it only satisfies Left Monotonicity. But, it does have Cut in the following form: X → A, A → B / X → A; B . Also, additional vocabulary may remove logical peculiarities of some initial semantic system. (E.g., the well-known failure of the deduction theorem in partial logic mainly signals the poverty of the initial language.) An interesting issue in the dynamic setting: do we want to iterate all dynamic logical constants in the language? For what does it matter? Then, once a language has been chosen, which valid principles form the abstract core, and what reflects specifics of concrete models? One sign of concreteness is failure of substitution for validities - which signals special treatment of atomic propositions. This happens in various systems considered in this paper. For any logic of this kind, one can define an obvious ’substitution-closed fragment’ which removes these more concrete, negotiable facts. What will these look like for update semantics? Finally, the term ’proof theory’ suggests standard business of a more combinatorial nature, such as proving Cut Elimination results, and exploring their usual consequences (subformula properties, constructive forms of interpolation). What results of this kind are available for dynamic inference? Evidently, the proof theory of update semantics and dynamic inference is a rich and challenging field of research.

Contributions by Groeneveld and Veltman

Perhaps the main contribution of this paper is its general modal perspective. Using this ’lingua franca’, there are lots of useful observations, connecting up with standard notions such as ’generated submodels, ’local versus global consequence’, etcetera. The first part on ’abstract representation’ proposes a modal semantics for updates and dynamic inference, guided by analogies with propositional dynamic logic (including fixed points). In particular, then, earlier separate representation theorems for sets of structural rules given by van Benthem can be made uniform, provided a model class is used with a suitable ’loops condition’. These uniform representations turn out to be a sort of standard Henkin-style models. The analysis also reveals the simplifying role played by ’idempotency’, a crucial feature of Veltman-style update systems. Less clear is the role played by the modal filtrations defined over these models. Is the outcome that all update systems satisfying the general conditions are decidable? For instance, the authors give an alternative proof of Kanazawa’s completeness theorem for update-test consequence with composition, but it is not clear whether its (non-trivial) decidability follows, too. In the more extensive concrete part of the paper, the authors analyze various proof systems of update logic with special operators (including ”might” and ”normally”), first given by Veltman, and (re-)prove their completeness using his general techniques. There seems to be a shift in emphasis here, from sequents-to-sequent consequence to mere universal validity of sequents. Presumably, the modal proof methods given also yield strong completeness with sequent premises. In this extensive part, two interesting special themes are the following. The authors mention the dynamic logic of van der Does, which enjoys elimination of Cautious Cut - but which does not quite coincide with a Veltman system. Can one turn the perspective around, and rather devise an adequate dynamic semantics for this calculus? Also, in the modal analysis of updates with ”normally”, an alternative Kripke-style semantics is proposed, which leads to a number of interesting new modal logics. Thus, ’static logic’ can profit from dynamic intuitions, too.

I would like to end with some further specific questions suggested by the above list. (1) The abstract representation has now been made general for at least two kinds of dynamic inference. Can it be generalized further to cover other existing kinds of complete representation, e.g., that for van Eyck & de Vries-style dynamic inference? (2) Can the dynamic logic analogy be exploited further to predict properties of dynamic styles? As Kanazawa observes, the Groenendijk & Stokhof style embeds into standard propositional dynamic logic, which makes it decidable. Update-test consequence goes into dynamic logic with loops, a decidable extension. By contrast, van Benthem’s update-to-update variant (’processing the premises achieves a transition for the conclusion’) requires a more complex new modal connective, and is undecidable. What is the general picture? (3) Can we show decidability for the general structural consequence problem from sets of sequents to sequents? (The authors express their optimism in a footnote.) (4) How do the various update calculi presented perform as actual proof systems? And in any case, what would be criteria for success?

Johan van Benthem

Institute for Logic, Language and Computation University of Amsterdam