\underline{\underline{\underline{11}}} Processing ambiguity non-deterministically: A modal logic for disambiguation

March 11, 1997

1. Introduction

An obvious step in interpreting a set E of (possibly) ambiguous expressions is to associate with each expression e ∈ E a set δ(e) ⊆ Φ of unambiguous formulas from some set Φ, for which

δ(e) ≈ {φ ∈ Φ : e can be disambiguated as φ} .

Such a function δ : E → Pow(Φ) does not, however, take context-sensitivity into account: δ(e) says only what formulas (in Φ) e can be disambiguated to, and nothing about the contexts under which e is disambiguated to a particular φ ∈ δ(e). Accordingly, functions [·, ·, ·] : (E × E × E) → E, with Φ ⊂ E, are considered in Fernando [3], subject to the intuition that for all expressions l, e, r ∈ E,

[l, e, r] ≈ an expression disambiguating e, assuming

l occurs to the left (or past) of e , and r to the right (or future) of e .

(As with δ, different choices of [·, ·, ·] are possible, the point being to study the consequences of such choices.) The disambiguation of e by [l, e, r] is, unlike δ(e), not only

(a) sensitive to the context l, r

but also

(b) deterministic, insofar as [l, e, r] is a specific expression, rather than a set of unambiguous formulas

and

(c) partial, in the sense that [l, e, r] may (assuming e ∈ E −Φ) well be an element of E − Φ.

In particular, if the context l, r provides no information to disambiguate an ambiguous expression e ∈ E − Φ, it is natural to expect [l, e, r] = e. In this sense, [l, e, r] allows for lazy disambiguation, the strategy being to wait for an extension l′, r′ of the context l, r that would disambiguate e. But what if no such extension exists? Then it would make sense to guess some value from δ(e). Now, having introduced non-determinism, the present paper goes whole hog, by considering a “total” disambiguation strategy in which an unambiguous formula can be extracted from [l, e, r] by guessing an extension r′ of r for which [l, e, r′] ∈ Φ. To keep things from getting out of hand, these guesses are recorded in states, structured by a labeled transition system, with a modal logic.

1.1. Transitions disambiguating expressions. More formally, let us assume that the set E of expressions is closed under a concatenation connective ; and write ee′ for e; e′. To describe cases of deadlock mentioned above in disambiguating an expression e, with l occuring to its left and r to its right, let us define e to be l, r-stuck if for every r′ ∈ E, [l, e, r] = [l, e, rr′]. We will assume that

(A0) for all l, r ∈ E and φ ∈ Φ, [l, φ, r] = φ from which it follows that every φ ∈ Φ is l, r-stuck (for all l, r ∈ E). Next, let us weaken the function [·, ·, ·] into a relation D(l, e, r, φ) ⊆ E × E × E × Φ, given by

D(l, e, r, φ) iff [l, e, r] = φ or
(e is l, r-stuck and φ ∈ δ([l, e, r])) .

Note that the first disjunct would be subsumed by the second (and can therefore be eliminated) if δ(φ) = {φ} for every φ ∈ Φ (complementing (A0)), and [·, ·, ·] is right-monotonic in the sense that for all l, e, r ∈ E,

[l, e, r] ∈ Φ implies (∀r′ ∈ E) [l, e, r] = [l, e, rr′] .

For now, however, let us refrain from making such potentially problematic assumptions about [·, ·, ·].

Next, let us pair up sequences of expressions in E with unambiguous formulas in Φ disambiguating those expressions as follows. Let us call a finite sequence φ_{1} ⋯ φ_{n} ∈ Φ^{∗} a fully disambiguated alternative (fda) to a sequence e_{1} ⋯ e_{m} in E^{∗} if n = m and there is some \overline{r} ∈ E^{∗} such that for every i ∈ \{1, …, n\},

D(e_{1} ⋯ e_{i−1}, e_{i}, e_{i+1} ⋯ e_{n}\overline{r}, φ_{i}) ,

where the empty sequence of expressions in E is, by convention, identified with a distinguished element ⊤ in Φ (⊆ E), and the parenthesization in e_{1}e_{2} ⋯ e_{n} is to the left:

(⋯ (e_{1}e_{2}) ⋯ e_{n}).

Note that the non-determinism in fda’s arises not only through δ (via D), but also through guessing a continuation \overline{r}. Now, let State be the set of all pairs (\overline{e}, \overline{φ}) such that \overline{φ} is an fda to \overline{e}. These states undergo transitions labeled by expressions e ∈ E as follows:

(\overline{e}, \overline{φ}) →^{e} (\overline{e′}, \overline{φ′}) iff \overline{e′} = \overline{e}e and (∃φ) \overline{φ′} = \overline{φ}φ
[and (\overline{e}, \overline{φ}), (\overline{e′}, \overline{φ′}) ∈ State] ,

as well as an equivalence relation

(\overline{e}, \overline{φ}) ∼ (\overline{e′}, \overline{φ′}) iff \overline{e′} = \overline{e}
[and (\overline{e}, \overline{φ}), (\overline{e′}, \overline{φ′}) ∈ State] ,

supporting a jump to a different interpretation \overline{φ′} of \overline{e}. In addition, some “logic” can be injected through a logical consequence relation ⊳ on Φ — i.e., a relation on Φ^{∗} × Φ, capturing the intuition that φ_{1} ⋯ φ_{n} ⊳ φ iff φ is a consequence of φ_{1}, …, φ_{n}. Further assumptions are introduced below, as needed to push certain lines of investigation through.^{1} 1.2. Contents of the present paper. This paper explores a certain (meta- )strategy for non-determi-nistically processing ambiguous expressions, with particular attention to relating states, subject to transitions defined from possibly different choices, δ, [·, ·, ·], ⊳ and δ′, [·, ·, ·]′, ⊳′, of primitives (the first two ingredients of which, δ and [·, ·, ·], are particular disambiguation functions). The leap to modal logic in §2 is not surprising, given well-known modal characterizations of the notion of bisimulation equivalence (Park [6], Hennessy and Milner [4]), recalled in §2.2. This “logical” shift brings with it questions about valid formulas, investigated in §3, where a decidability result is established. Directions for further work are discussed in §4.

1As to exactly what end, the reader familiar with Discourse Representation Theory (DRT, Kamp and Reyle [5]) may, for orientation, wish to identify Φ with the set of DRSs, and E − Φ with a set of English sentences (or perhaps some more formal system of underspecified representations). The transitions →^{e} can then be seen as describing a DRS

2. A language for disambiguating transitions

When are two states of the form outlined in §1.1 “equivalent”? The present section considers two approaches that are shown to converge, the first of which builds on a formal (modal) language.

2.1. The modal language L(E, Φ). Let L(E, Φ), or L for short, consist of Lformulas A generated from formulas φ ∈ Φ and expressions e ∈ E as follows

(L-gen) A :== φ | ⟨e⟩A | ◇A | ¬A | A ∧ B . A pair of functions, δ : E → Pow(Φ) and [·, ·, ·] : (E × E × E) → E, induces, in the manner of §1.1, a set State of states (\overline{e}, \overline{φ}), relative to which, let us define, given a relation ⊳ ⊆ Φ^{∗} × Φ,

(\overline{e}, \overline{φ}) ⊧ φ iff \overline{φ} ⊳ φ
(\overline{e}, \overline{φ}) ⊧ ⟨e⟩A iff for some φ such that (\overline{e}e, \overline{φ}φ) ∈ State,
(\overline{e}e, \overline{φ}φ) ⊧ A
(\overline{e}, \overline{φ}) ⊧ ◇A iff for some \overline{φ′} such that (\overline{e}, \overline{φ′}) ∈ State,
(\overline{e}, \overline{φ′}) ⊧ A
(\overline{e}, \overline{φ}) ⊧ ¬A iff not (\overline{e}, \overline{φ}) ⊧ A
(\overline{e}, \overline{φ}) ⊧ A ∧ B iff (\overline{e}, \overline{φ}) ⊧ A and (\overline{e}, \overline{φ}) ⊧ B .

An infinitary extension L^{∞} of L is easily described by allowing an infinitary conjunction ⋀ on a set A of L^{∞}-formulas —

(L^{∞}-gen) A :== φ | ⟨e⟩A | ◇A | ¬A | ⋀ A with

(\overline{e}, \overline{φ}) ⊧ ⋀ A iff (∀A ∈ A) (\overline{e}, \overline{φ}) ⊧ A .

2.2. Transitions underlying L. To relate the language L to the transitions mentioned in §1.1, let us be a bit more careful to specify when the primitives δ, [·, ·, ·] and ⊳ are “good.” In compliance with standard practice in modal logic, we set apart the first two primitives from the third (⊳). A g-pair (for “good” or “generating” pair) is a pair of functions δ and [·, ·, ·] such that

(A1) for all φ ∈ Φ and l, r ∈ E, δ(φ) = {φ} and [l, φ, r] = φ and

construction algorithm, in which the previous English sentences processed and the DRSs constructed for them are recorded as states. Backtracking from guesses is allowed through the transitions ∼. More in §4.2 below.

(A2) for all e ∈ E, {[l, e, r] : l, r ∈ E} ∩ Φ ⊆ δ(e) . (A1) says that unambiguous formulas should be left alone, while (A2) says that for all l, r ∈ E, disambiguation by [l, ·, r] sharpens that by δ.^{2} For the record, let us define the L-frame induced by a g-pair δ, [·, ·, ·] to be the pair consisting of the set State (as defined in §1.1) and the transition relation → ⊆ State × (E + {◇}) × State satisfying

(\overline{e}, \overline{φ}) →^{e} (\overline{e′}, \overline{φ′}) iff \overline{e′} = \overline{e}e and (∃φ ∈ Φ) \overline{φ′} = \overline{φ}φ
(\overline{e}, \overline{φ}) →^{◇} (\overline{e′}, \overline{φ′}) iff \overline{e} = \overline{e′}

for all (\overline{e}, \overline{φ}), (\overline{e′}, \overline{φ′}) ∈ State (writing a →^{e} b to mean (a, e, b) belongs to →). (The connection with L should be evident: →^{e} supports the modal operator ⟨e⟩, while →^{◇} supports ◇.) Now, to ground the language L in Φ, it remains to equip an L-frame with a valuation V : Φ → Pow(State), defined from a suitable relation ⊳ as

V (φ) = \{(\overline{e}, \overline{φ}) ∈ State : \overline{φ} ⊳ φ\} .

We shall refer to the resulting structure ⟨State, →, V ⟩ as the L-model induced by the g-triple δ, [·, ·, ·], ⊳.

Putting the language L aside for a moment now, let us fix two ternary relations → ⊆ S × L × S and →′ ⊆ S′ × L × S′. Let ·^{bf} be the “back-and-forth” operator that maps a binary relation R ⊆ S × S′ to the binary relation R^{bf} consisting of all pairs (a, a′) ∈ S × S′ such that for every l ∈ L,

[“forth”] for every b ∈ S such that a →^{l} b, there exists b′ ∈ S′ such that

a′ →′^{l} b′ and bRb′

and

[“back”] for every b′ ∈ S′ such that a′ →′^{l} b′, there exists b ∈ S such

that a →^{l} b and bRb′.

A bisimulation between ⟨S, →⟩ and ⟨S′, →′⟩ is a binary relation R ⊆ S ×S′ for which R ⊆ R^{bf}. It is well-known that the ⊆-largest bisimulation \underline{↔} between ⟨S, →⟩ and ⟨S′, →′⟩ exists, and can be calculated (co-inductively) as ⋂_{α} \underline{↔}_{α}, where \underline{↔}_{0} = S×S′, \underline{↔}_{α+1} = \underline{↔}_{α}^{bf}, and \underline{↔}_{λ} = ⋂_{α<λ} \underline{↔}_{α} for limit ordinals λ.

Returning to L, note that an L-model ⟨State, →, V ⟩ can be repackaged as ⟨State, → + ⇝⟩, where ⇝ ⊆ State × Φ × State is defined by

(\overline{e}, \overline{φ}) ⇝^{φ} (\overline{e′}, \overline{φ′}) iff (\overline{e}, \overline{φ}) = (\overline{e′}, \overline{φ′}) ∈ V (φ) .

With this understanding, we can, given L-models M and M′ and states (\overline{e}, \overline{φ}) and (\overline{e′}, \overline{φ′}) in M and M′ respectively, write M, (\overline{e}, \overline{φ}) \underline{↔} M, (\overline{e′}, \overline{φ′}) to mean that the largest bisimulation between M and M′ relates (\overline{e}, \overline{φ}) to (\overline{e′}, \overline{φ′}). Next, define M, (\overline{e}, \overline{φ}) ≡_{L} M′, (\overline{e′}, \overline{φ′}) to hold if for all A ∈ L,

(\overline{e}, \overline{φ}) ⊧_{M} A iff (\overline{e′}, \overline{φ′}) ⊧_{M′} A .

Similarly, for ≡_{L^{∞}} (replacing L by L^{∞}).

2The possibility that an expression might get stuck in the sense of §1.1 precludes a straightforward converse to (A2) for cases other than in (A1).

Theorem 1. Let M = ⟨State, →, V ⟩ and M′ = ⟨State′, →′, V′⟩ be the L-models induced by g-triples δ, [·, ·, ·], ⊳ and δ′, [·, ·, ·]′, ⊳′, respectively. For all (\overline{e}, \overline{φ}) ∈ State and (\overline{e′}, \overline{φ′}) ∈ State′,

M, (\overline{e}, \overline{φ}) \underline{↔} M′, (\overline{e′}, \overline{φ′}) iff M, (\overline{e}, \overline{φ}) ≡_{L^{∞}} M′, (\overline{e′}, \overline{φ′}) .

If for every e ∈ E, δ(e) and δ′(e) are finite sets, then the equivalence holds with L^{∞} replaced by L.

Proof. A direct consequence of \underline{↔} = ⋂_{α} \underline{↔}_{α}. The additional assumption that δ(e) ∪ δ′(e) is finite for every e ∈ E implies, by (A2), that \underline{↔} = \underline{↔}_{ω}. ⊣

3. L-validities under minimal assumptions on E

The present section is concerned with capturing L-formulas A that are L-valid in the sense that for any g-triple, A holds at every state of the L-model induced by that triple. Given a specific relation ⊳ of interest, it is natural to specialize the notion of validity to that choice, and call A L(⊳)-valid if for every g-pair δ, [·, ·, ·], A holds at every state of the L-model M induced by the g-triple δ, [·, ·, ·], ⊳. In this connection, it is useful to state a few rules sound for many choices of ⊳.

(Ref) \overline{φ ⊳ φ}  (Weak) \frac{\overline{φ} ⊳ φ}{\overline{φ}ψ ⊳ φ} \frac{\overline{φ} ⊳ φ}{ψ\overline{φ} ⊳ φ}

(Cut) \frac{\overline{φ} ⊳ ψ  \overline{φ}ψ ⊳ φ}{\overline{φ} ⊳ φ}

The rules (Weak) and (Cut) are formulated in a slightly non-standard way^{3} to simplify the proof of the following encoding of ⊳ into L via ∧ and ¬.

Proposition 2. If ⊳ satisfies (Ref), (Weak) and (Cut), then for all φ_{1}, …, φ_{n}, φ ∈ Φ,

φ_{1} ⋯ φ_{n} ⊳ φ iff (φ_{1} ∧ ⋯ ∧ φ_{n}) ⊃ φ is L(⊳)-valid

(where, as usual, A ⊃ B abbreviates ¬(A ∧ ¬B)).

Proof. The direction ⇒ follows from repeated applications of (Cut) and both sides of (Weak). As for ⇐, check satisfaction at the state (φ_{1} ⋯ φ_{n}, φ_{1} ⋯ φ_{n}), appealing to (Ref) and both sides of (Weak). ⊣.

Proposition 2 implies that the complexity of L(⊳)-validities could not possibly be less than that of ⊳, if the rules (Ref), (Weak) and (Cut) are sound in ⊳. (And this is to say nothing of modal L-formulas that follow from (Ref), (Weak), and (Cut); more in §3.1 below.) A general decidability result for L(⊳)-validities is thus out of the question, unless the notion of computability is relativized to an oracle for ⊳ (in uncomputable cases such as that of first-order logic) — throwing in, whenever φ_{1} ⋯ φ_{n} ⊳ φ, the L-formula (φ_{1} ∧ ⋯ ∧ φ_{n}) ⊃ φ as an axiom into a proof system for L(⊳)-validities (assuming ⊳ verifies (Ref), (Weak) and (Cut)).

(Con) \frac{\overline{φ}φφ ⊳ ψ}{\overline{φ}φ ⊳ ψ}  (Exc) \frac{\overline{φ}φψ\overline{ψ} ⊳ φ′}{\overline{φ}ψφ\overline{ψ} ⊳ φ′}

3(Ref), (Weak) and (Cut) together imply contraction and exchange — which may seem surprising until one notices that not only is an application of (Exc)

implicit in doubling (Weak), but so is an application of (Con) in halving the conclusion of (Cut) from \overline{φ} \overline{φ} ⊳ φ to \overline{φ} ⊳ φ.

For the moment, let us set our sights on L-validities rather than on some fixed choice of ⊳, while at the same time being sensitive to the sort of consequence relation ⊳ that we work with. More specifically, we will attack the problem of a completeness theorem for L-validities, by building models for an L-formula A based on relations ⊳ familiar from ordinary propositional logic, except that the internal structure of every formula φ ∈ Φ − {⊤} occurring in A is abstracted away. Notice that all formulas in Φ (however complex) are atomic relative to the generation (Lgen) of L-formulas.^{4} In particular, it is implicit in (L-gen) that for all A, B ∈ L, none of ⟨e⟩A, ◇A, ¬A and A ∧ B is in E. Whatever connectives E or Φ has ought not to be confused with these. If we require, however, that the relation ⊳ in a g-triple satisfy \overline{φ} ⊳ ⊤ (for every \overline{φ} ∈ Φ^{∗}, where ⊤ is the formula in Φ mentioned previously as, by convention, the representative in E of the empty sequence with respect to ;), then ⊤ is L-valid. Throughout this section, our definition of a g-triple will be amended to incorporate the requirement

(A3) the rules (Ref), (Weak) and (Cut) are sound in ⊳, as is

\overline{∅ ⊳ ⊤} .

3.1. A proof system for L. It is easy enough to list a number of proof principles sound for L-models:

(i) tautologies (relative to ∧ and ¬)

(ii) the rule of modus ponens (iii) the rule of “uniform substitution” (of arbitrary formulas for atomic formulas) (iv) for every e ∈ E, the normal logic K for ⟨e⟩, plus for every φ ∈ Φ,

⟨φ⟩A ≡ [φ]A

(where, as usual, A ≡ B abbreviates (A ⊃ B) ∧ (B ⊃ A), while [e] and □ abbreviate ¬⟨e⟩¬ and ¬◇¬, respectively)

(v) the modal system S5 for ◇, plus

⟨e⟩◇A ⊃ ◇⟨e⟩A
◇⟨e⟩A ⊃ [e]◇A

(vi) consequences of ⊳ under (A3)

⊤
⟨φ⟩φ ∧ [φ][e]φ [by (Ref) and (Weak)]
φ ⊃ [e]φ  [by (Weak)]
(φ ∧ ⟨φ⟩ψ) ⊃ ψ  [by (Cut)] .

But what else should we add?

An instructive test for a complete proof system is provided by the notion of an (n, E_{∘})-diagram, where n is some natural number, and E_{∘} is a finite subset of E. This is defined by induction on n.

n = 0: A (0, E_{∘})-diagram is an L-formula of the form

⋀ (Φ_{∘} ∪ {¬φ : φ ∈ (Φ ∩ E_{∘}) − Φ_{∘}})
for some Φ_{∘} ⊆ Φ ∩ E_{∘}.

4Hence, the care taken in avoiding mention of Φ-connectives in Proposition 2 (and in the rules (Ref), (Weak) and (Cut)).

n + 1: An (n + 1, E_{∘})-diagram is an L-formula of the form

A ∧ ⋀ {([e] ⋁ A_{e}) ∧ ⋀⟨e⟩A_{e} : e ∈ E_{∘}}

where A is an (n, E_{∘})-diagram and for every e belonging to E_{∘}, A_{e} is a set of (n, E_{∘})-diagrams (and it is understood that ⋁ ∅ is a contradictory L-formula, while ⋀ ∅ is ⊤).

By a routine induction on n, it is easy to prove that for every n and finite set E_{∘} ⊆ E,

⋁ {A ∈ L : A is an (n, E_{∘})-diagram}

is L-valid. In fact, we can trim this disjunction, by adding a bit more structure to the notion of a diagram, reflecting (A3).

Towards that end, let us assume E_{∘} contains ⊤, and define an (n, E_{∘})-path to be a function from ⋃_{i=0}^{n} E_{∘}^{i} to Pow(Φ ∩ E_{∘}) such that for every \overline{e} ∈ dom(p),

p(\overline{e}) ≠ ∅ implies ⊤ ∈ p(\overline{e}) ,

and for every \overline{e}e ∈ dom(p) and φ ∈ Φ ∩ E_{∘},

p(\overline{e}e) ≠ ∅ implies p(\overline{e}) ≠ ∅ and p(\overline{e}) ⊆ p(\overline{e}e)
p(\overline{e}) ≠ ∅ implies p(\overline{e}φ) = p(\overline{e}) ∪ \{φ\} .

The intuition is that an (n, E_{∘})-path p assigns to every \overline{e} ∈ ⋃_{i=0}^{n} E_{∘}^{i} the set p(\overline{e}) of formulas in Φ that hold (along the path) after asserting \overline{e}. This is formalized by associating with every (n, E_{∘})-path p and \overline{e} ∈ dom(p) the L-formula

A_{p,\overline{e}} = ⋀ (p(\overline{e}) ∪ \{¬φ : φ ∈ (Φ ∩ E_{∘}) − p(\overline{e})\}) .

Now, for branching, let us introduce the notion of a tree as follows. A set P of (n, E_{∘})-paths defines a function t from ⋃_{i=0}^{n} E_{∘}^{i} to Pow(Pow(Φ ∩ E_{∘})) given by

t(\overline{e}) = \{p(\overline{e}) : p ∈ P \} .

If |t(∅)| = 1 (i.e., for all p, p′ ∈ P, p(∅) = p′(∅)), then the function t, so defined, is said to be an (n, E_{∘})-tree. Let us say an (n, E_{∘})-path p is a path through t if for all \overline{e} ∈ dom(p), p(\overline{e}) ∈ t(\overline{e}). For every \overline{e} = e_{1} ⋯ e_{i} ∈ dom(t) − \{∅\}, let A_{t,\overline{e}} be the L-formula

[e_{1}] ⋯ [e_{i}] ⋁\{A_{p,\overline{e}} : p is a path through t and p(\overline{e}) ≠ ∅\}
∧ ⋀\{⟨e_{1}⟩ ⋯ ⟨e_{i}⟩A_{p,\overline{e}} : p is a path through t and p(\overline{e}) ≠ ∅\}.

Collecting all such e’s together, and writing Φ_{t} for the unique element of t(∅), let A_{t} be the L-formula

⋀ (Φ_{t} ∪ \{A_{t,\overline{e}} : \overline{e} ∈ dom(t) − \{∅\}\})

encoding t.

Proposition 3. For every natural number n and finite set E_{∘} ⊆ E,

⋁ {A_{t} : t is an (n, E_{∘})-tree}

is L-valid.

Proof. Induct on n. ⊣ In addition to (i)-(vi) above, let us throw in all the L-valid formulas mentioned in Proposition 3 as axioms in our proof system,^{5} and, as usual, write |− A to mean that A can be derived in it. Call A consistent if not |− ¬A.

3.2. Completeness and decidability. Given a consistent L-formula A, how can we construct a g-triple inducing an L-model for A? We have no choice but to set [l, φ, r] = φ, δ(φ) = {φ} for all l, r ∈ E and φ ∈ Φ. As A is a finite string, it should not be surprising that we need only worry about a finite set E_{∘} of expressions in E (including formulas in Φ) that contains the set E(A) of expressions occurring in A. Accordingly, it will be useful to pick out a “rogue” expression @ ∈ E − (Φ ∪ E(A)), take δ(@) = ∅, and then set [l, e, r] = @ for all but finitely many choices of arguments l, e, r ∈ E. Just what those choices are will depend on some set s of L-formulas that will be required to meet certain properties, from which it follows that s yields, through a certain recipe, a g-triple inducing an L-model with a state in which A holds. Putting off what that recipe is for now, let us attend to what s is. Call a set s of L-formulas A-full if

(i) for every L-formula B, B ∈ s or ¬B ∈ s

and

(ii) for every finite sequence B_{1}, …, B_{n} in s, not |− (B_{1}∧⋯∧B_{n}) ⊃
¬A.

It follows that A is an element of every A-full set. Moreover, (as will come as no surprise to the cognoscenti)

Lemma 4. For every consistent L-formula A, there is an A-full set s.

Proof (folklore). Construct s = ⋃_{n<ω} s_{n} in stages from an enumeration A_{0}, A_{1}, … of L^{A}-formulas, with s_{0} = {A}, and

s_{n+1} = \{ \begin{matrix}s_{n} ∪ \{¬A_{n}\} & if |− (⋀ s_{n}) ⊃ ¬A_{n} \\ s_{n} ∪ \{A_{n}\} & otherwise . \end{matrix}

⊣

Turning next to the aforementioned recipe, we will require the following ingredients, in addition to an A-full set s, and an expression @ ∈ E − (Φ ∪ E(A)). Writing n_{∘} for the number of occurrences in A of modal operators of the form ⟨e⟩, and E_{∘} for E(A) ∪ {⊤}, fix

(a) an expression ê ∈ E − (Φ ∪ E(A) ∪ {@})

(b) for every (n_{∘}, E_{∘})-tree t, a distinct formula φ_{t} ∈ Φ − E(A)

(c) for every (n_{∘}, E_{∘})-path p, a distinct expression e_{p} ∈ E − E_{∘}.^{6} As long as E and Φ are infinite — an assumption that we can safely take for granted — such choices are possible (owing to the finiteness of E(A)). Now, let Φ_{0} be the finite subset (E_{∘} ∩ Φ) ∪ {φ_{t} : t is an (n_{∘}, E_{∘})-tree} of Φ, and Φ_{1} be some subset of Φ containing Φ_{0} with cardinality |Φ_{1}| = 2^{|Φ_{0}|}. Then there is a bijection ˜⋀ : Pow(Φ_{0}) → Φ_{1} such that for every φ ∈ Φ_{0}, ˜⋀{φ} = φ. Writing ˜· : Φ_{1} → Pow(Φ_{0}) for the inverse function of ˜⋀, define a relation ⊳ ⊆ Φ^{∗} × Φ inductively by closing the set

5We will not worry about deriving a simple and elegant proof theory here.

6Whether or not e_{p} ∈ Φ is immaterial (in contrast to (b), where φ_{t} must be an element of Φ).

{(φ_{1} ⋯ φ_{n}, ψ) ∈ Φ_{1}^{∗} × Φ_{1} : ψ̃ ⊆ φ̃_{1} ∪ ⋯ ∪ φ̃_{n}}

under the rules mentioned in (A3).

The idea then is to set for all l, r ∈ E, (n_{∘}, E_{∘})-trees t and (n_{∘}, E_{∘})-paths p through t,

[⊤, ê, re_{p}φ_{t}] = ˜⋀ (p(∅) ∪ {φ_{t}}) if ◇A_{t} ∈ s and p(∅) ≠ ∅

(which is independent of the choice of the path p through t, since |t(∅)| = 1) and

[êl, e, re_{p}φ_{t}] = ˜⋀ (p(le) ∪ {φ_{t}}) if ◇A_{t} ∈ s and p(le) ≠ ∅

(which is dependent on the choice of p). Note that the conjunction above is for Φ, as opposed to that for L. It is a routine matter to complete the definition of [·, ·, ·] elsewhere to @, and to arrange δ to satisfy (A2) by setting

δ(e) = Φ ∩ {[l, e, r] : l, r ∈ E} .

Observe that this recipe makes sense, whether s is A-full or not, and indeed with A replaced by n_{∘} and E_{∘}. But to simplify notation and focus on the most prominent ingredients, we will refer to the L-model so defined as one A-induced by s.

Next, leaving this L-model aside for the moment, let

(i) T (n_{∘}, E_{∘}) be the set of all (n_{∘}, E_{∘})-trees (ii) for every T ⊆ T (n_{∘}, E_{∘}), A^{T} be the L-formula

(⋀_{t∈T} ◇A_{t}) ∧ (□ ⋁_{t∈T} A_{t})

encoding the “forest” T (where A_{t} is as defined in §3.1) and

(iii) L[n_{∘}, E_{∘}] be the set of L-formulas B with at most n_{∘} occurrences of modal operators ⟨e⟩, and where all occurrences of expressions e ∈ E (including φ ∈ Φ) belong to E_{∘}.

Lemma 5. For every T ⊆ T (n_{∘}, E_{∘}), t ∈ T and B ∈ L[n_{∘}, E_{∘}], either (A^{T} ∧A_{t}) ⊃ B is L-valid or (A^{T} ∧ A_{t}) ⊃ ¬B is L-valid (or both).

Proof. By induction on B, noting that the reason for passing to forests is to take account of ◇. ⊣

Returning now to the L-model A-induced by s, we have

Lemma 6. Given an A-full set s, A holds at a state in the L-model A-induced by s.

Proof. Let T_{s} = {t : t ∈ T (n_{∘}, E_{∘}) and ◇A_{t} ∈ s}. T_{s} ≠ ∅ by Proposition 3 and the A-fullness of s. So, pick a t ∈ T_{s} and a path p through t, noting that

(ê, [⊤, ê, e_{p}φ_{t}]) ⊧ A^{T_{s}} ∧ A_{t} .

It follows by condition (ii) of A-fullness and Lemma 5 that

(ê, [⊤, ê, e_{p}φ_{t}]) ⊧ A .

⊣ An immediate consequence of Lemmas 4 and 6 is

Theorem 7. For every L-formula A, |− A iff A is L-valid.

Moreover, L enjoys the so-called finite model property (where the finite models amount to the formulas A^{T} ∧ A_{t} mentioned in Lemma 5), whence

Corollary 8. The set of L-valid formulas is decidable.

Can we establish Theorem 7 and Corollary 8, with L-validity replaced by L(⊳)- validity? By Proposition 2, our notion of proof must be beefed up to derive the L-formulas

φ_{1} ∧ ⋯ ∧ φ_{n} ⊃ φ

whenever φ_{1} ⋯ φ_{n} ⊳ φ, and our notion of computation equip-ped with an oracle for ⊳. Although I have yet to check all the details, I believe the argument above for Theorem 7 and Corollary 8 relativizes, provided we add to (A3) the assumption that Φ is closed under a connective ˜⋀ that behaves as conjunction (relative to ⊳).

4. Discussion

Although the subject of the present work is ambiguity, it is fair to say that the set E − Φ of ambiguous expressions has been kept largely in the background, and no mention made of the internal structure of these expressions. The attention instead has been on the language L, which is perhaps most naturally construed as a metalanguage, the connectives of which should be distinguished from any within E or Φ. It is true enough that, under (A3), the formula ⊤ ∈ Φ functions also as a valid L-formula, and that the difference between L-conjunction ∧ and Φ-conjunction ˜∧ (assuming Φ is closed under such a connective) is blurred by L-axioms such as

φ ∧ φ′ ≡ φ ˜∧ φ′ .

Nonetheless, the distinction must be maintained, as already in the case of a formula ⊥ ∈ Φ that is “absurd” insofar as for every φ ∈ Φ, ⊥ ⊳ φ, it is, as an L-formula, perfectly consistent: (⊥, ⊥) ⊧ ⊥. Of course, states at which ⊥ hold are special — special enough, in fact, to merit being collected in the set

⊥-State = \{(\overline{e}, \overline{φ}) ∈ State : \overline{φ} ⊳ ⊥\} ,

to which the valuation V : Φ → Pow(State) can be reduced, assuming

(A4) ⊳ is ⊥-reducible in the sense that for every φ ∈ Φ there is a formula φ^{c} ∈ Φ such that for all \overline{φ} ∈ Φ^{∗},

\overline{φ} ⊳ φ iff \overline{φ}φ^{c} ⊳ ⊥ .

Proposition 9. If ⊳ satisfies (A4), then for every L-model induced by a g-triple containing ⊳, and for every state (\overline{e}, \overline{φ}) of that model,

(\overline{e}, \overline{φ}) ⊧ φ iff (\overline{e}, \overline{φ}) ⊧ ⟨φ^{c}⟩⊥
iff (\overline{e}φ^{c}, \overline{φ}φ^{c}) ∈ ⊥-State

for every φ ∈ Φ, where φ^{c} is its complement stipulated by (A4).

Not only does Proposition 9 simplify an L-model ⟨State, →, V ⟩ to ⟨State, →, ⊥-State⟩, it also suggests a way of extending the language L to include not only formulas φ ∈ Φ but arbitrary expressions e ∈ E —

(L_{+}-gen) A :== e | ⟨e⟩A | ◇A | ¬A | A ∧ B with

(†) (\overline{e}, \overline{φ}) ⊧ e iff (\overline{e}, \overline{φ}) ⊧ ⟨e^{c}⟩⊥ .

Two problems plague (†).

(P1) Whereas the modalities ⟨φ⟩ and [φ] are interchangable (because →^{φ} is functional), ⟨e⟩ and [e] are, in general, not (especially if e is ambiguous).

(P2) Just what is the complement e^{c} of e? (P1) raises the question: should we really use ⟨e^{c}⟩ rather than [e^{c}] in formulating an expression e ∈ E as an L-formula ⟨e^{c}⟩⊥? Inasmuch as both ⟨e^{c}⟩⊥ and [e^{c}]⊥ are available as L-formulas, it may seem silly to insist on choosing between the two.^{7} The point, however, in explicitly introducing expressions e ∈ E into L_{+} is to investigate the problem of logical consequence between ambiguous expressions (in terms of L_{+}), and for this, some unambiguous choice would be helpful. As for (P2), there is no dismissing the importance of complementation ·^{c}, especially for matters such as presupposition, for which the so-called negation test suggests characterizing the presupposition of e as e ∨ e^{c} (with, as usual, A ∨ B abbreviating ¬(¬A ∧ ¬B)). (For this purpose, e^{c} had better not amount to ¬e, or else the presupposition, e∨e^{c}, of e would always be vacuous, whichever way e were formulated within L.) Having said precious little about E, let us close by peeking inside E, before reflecting on strategies that map E to Φ.

4.1. Ambiguous connectives. In addition to assumptions (A1)-(A4), it is natural also to impose the constraint

[l, ee′ , r] = [l, e, e′r] [le, e′, r] ,

leading to

⟨ee′⟩A ≡ ⟨e⟩⟨e′⟩A

(assuming the juxtaposition in φφ′ ⊳ ψ can be read ;), and

[l, e^{c} , r] = [l, e, r]^{c} .

Turning to the function δ : E → Pow(Φ), which comes into play when an expression e gets l, r-stuck (see §1.1), an explicit handle on δ is provided by assuming E is closed under a binary connective •, with

δ(e • e′) = δ(e) ∪ δ(e′)

and

[l, e • e′, r] = \{ \begin{matrix}[l, e, r] & if e ≺^{l,r} e′ \\ [l, e′, r] & if e′ ≺^{l,r} e \\ [l, e, r] • [l, e′, r] & otherwise \end{matrix}

for some function from pairs (l, r) ∈ E×E to asymmetric binary relations ≺^{l,r} on E. For motivation and intuitions, see Fernando [3]. In a different direction, ambiguous expressions can also be built through labeling and underspecification (e.g., Reyle [8], which is generalized in Bos [2], and, even further, in Asher and Fernando [1]).

7In fact, there are many more quantifiers to choose from than ∃ (⟨e⟩) and ∀ ([e]), a general scheme for which, incorporating context-dependent disambiguation, is given in Fernando [3].

In any event, the question arises: what are the consequences in L of the internal structure of expressions?

4.2. Guessing disambiguations. Just what those consequences in L are will depend partially on [·, ·, ·], which might, for instance, be required^{8} to be monotonic in the sense that whenever [l, e, r] ∈ Φ, [l′l, e, rr′] = [l, e, r]. Note that the functions [·, ·, ·] constructed for the proof of completeness in §3 can be safely assumed to be monotonic. Also, δ is of no real significance to the L-model induced, beyond the fact that δ(@) = ∅. The crucial mechanism used is that of guessing a continuation e_{p}φ_{t} to be appended to the sequence \overline{e}, which is then subjected to [·, ·, ·]-disambiguation. That guess, e_{p}φ_{t}, “explains” the “abduction” of a fully disambiguated alternative to \overline{e} from [·, ·, ·] (Peirce [7]). It could just as easily have been inserted to the left, rather than the right of \overline{e}, had the notion of a fully disambiguated alternative allowed for guessing the past (left), as opposed to the future (right). (Indeed, one might imagine inserting guesses anywhere relative to \overline{e}: to the left, right, middle ...) Nevertheless, some notion of direction does seem to be unavoidable in making sense of “real-life” phenomena such as presupposition, and in developing abstract tools such as the language L described above, the modal operators ⟨e⟩ of which look ahead to the future, with ◇ standing by just in case there is none.

References

[1] N. Asher and T. Fernando. Labeling representations for effective disambiguation. In Proc. Second International Workshop on Computational Semantics (IWCS II). Tilburg, The Netherlands, 1997.

[2] Johan Bos. Predicate logic unplugged. In P. Dekker and M. Stokhof, editors, Proc. Tenth Amsterdam Colloquium. ILLC, University of Amsterdam, 1996.

[3] Tim Fernando. Ambiguity under changing contexts. Manuscript, 1996. Preliminary version presented in Mathematics of Language 4 (Philadelphia, October 1995), and submitted for publication.

[4] M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. J. Assoc. Computing Machinery, 32(1), 1985.

[5] H. Kamp and U. Reyle. From Discourse to Logic. Kluwer Academic Publishers, Dordrecht, 1993.

[6] David Park. Concurrency and automata on infinite sequences. In P. Deussen, editor, Proc. 5th GI Conference, LNCS 104. Springer-Verlag, Berlin, 1981.

[7] Charles Sanders Peirce. Abduction and induction. In J. Buchler, editor, Philosophical Writings of Peirce. Dover Books, New York, 1955.

[8] Uwe Reyle. Dealing with ambiguities by underspecification: construction, representation and deduction. Journal of Semantics, 10(2), 1993.

Universität Stuttgart, IMS, Azenbergstrasse 12, D-70174 Stuttgart

E-mail address: fernando@ims.uni-stuttgart.de

8For the role of constraints in a co-inductive analysis of compositionality, see Fernando