Incremental Dynamics
Jan van Eijck

Abstract:
An incremental semantics for a logic with dynamic binding is developed on the
basis of a variable free notation for dynamic logic that takes its cue from 
De Bruijn's variable free notation for lambda calculus. De Bruijn indexing 
replaces variables by indices which indicate the distance to their binders. 
We propose to use reverse De Bruijn indexing, which works almost the same, 
only now the indices refer to the depth of the binding operator in the 
formula. The indexing mechanism guarantees that active registers are never 
overwritten by new quantifier actions. The resulting system is analysed and 
applied to a new rational reconstruction of discourse representation theory. 
It is argued that the present system of incremental dynamic logic provides 
an explicit account of anaphoric context and yields new insight into the 
dynamics of anaphoric linking in reasoning. A calculus for dynamic reasoning 
with anaphora is presented and its soundness and completeness are established.

Keywords and Phrases: dynamic semantics of natural language, complete calculus 
  for dynamic reasoning with anaphora, incremental interpretation, monotonic
  semantics, anaphora and context.

Submitted for publication in the Journal of Logic, Language and Information.