Incremental dynamics (Q5939955)

The author addresses the problem of arriving at an incremental interpretation of anaphoric relationships in natural language texts (NLT). E.g. the sequence `A man entered. He smiled.' requires `a man' and the pronoun `he' to be coreferential. In standard predicate logics with their static variable binding mechanism one cannot get this interpretation in a compositional way. In dynamic approaches to NLT, quantification is interpreted as the operation of random assignment to a variable. The meaning of \(\exists x\) becomes a relation between variables states \(f\), \(g\) such that \(f\) and \(g\) differ at most in the value assigned to \(x\): \(_f[ [\exists x] ]_g\) iff \(f[x]g\). This leads to the problem of destructive variable assignment: using the same existential quantifier-variable combination twice destroys the anaphoric possibilities set up by the first occurrence of \(\exists\). E.g. after \(\exists xPx;\exists xQx\), only the individual introduced by the interpretation of \(\exists xQx\) is available for future anaphoric reference whereas the individual introduced by \(\exists xPx\) has become inaccessible by extensions of the present context. Ruling out destructive variable assignments by imposing the constraint to always use a fresh variable when a given context is extended by one or more sentences has the effect of making the interpretation of a sentence at least partly dependent on the context in which it occurs. The solution to the problem presented by the author consists in replacing the dynamic variable binding mechanism from dynamic predicate logic with an indexing mechanism. The latter is based on the de Bruijn notation for lambda calculus where variables get replaced by indices that indicate the distance to the binding lambda operator. A variable context is represented as a stack of registers and quantification is interpreted as the operation of pushing a new element on top of the context stack. Since quantifiers always bind the next available variable register, the indexing mechanism guarantees that active registers are never overwritten by new quantifier actions. In contrast to other dynamic approaches to NLT, the induced consequence relation is transitive (section 5). In sections (6) and (7) an axiomatization is presented. Sections (8) and (9) show the completeness of the system relative to the intended semantics and establish the equivalence of the system with first-order logic.