Quantification, conjunction, and verbs of creation in dynamic approaches

[Darryl McAdams]

I've noticed what seems to be an unfortunate property of dynamic approaches to semantics (e.g. DRT, dynamic semantics, etc.), which is that the relationship between universal quantification and conjunction is lost.

consider the following formula in a non-dynamic system:

    1. (∀x. Px) ∧ Q

if x ranges over the set {a,b,c}, then this formula is equivalent to

    2. (Pa ∧ Pb ∧ Pc) ∧ Q

but this is not true of dynamic approaches. consider the slightly different formula

    3. (∀x. ∃y. Pxy) ∧ Q

with x ranging over the same set, this is definitely not equivalent to

    4. ((∃y. Pay) ∧ (∃y. Pby) ∧ (∃y. Pcy)) ∧ Q

in (3), y does not take scope in Q, but in (4) it does. slightly unappealingly, y is shadowed in (4), but that's a consequence of the choice of translation from quantified to conjunctive form. we could just as easily do

    5. ((∃y. Pay) ∧ (∃z. Pbz) ∧ (∃w. Pcw)) ∧ Q

and get y, z, and w in scope in Q.

so why should this matter? well, consider the sentence "John duplicated every file. He moved the copies to a new folder."

this sentence should mean something approximately like

    6. (∀x. File(x) → ∃y. Duplicate(j,x,y)) ∧ Move(j,...,aNewFolder)

perhaps we need some quantifier around the right conjunct, let's not worry about that right now.

so what is ...? we need ... to be the copies. that is to say, we need ... to be the y's from the left conjunct, but they're not in scope using a dynamic approach, precisely because the consequent of an implication doesn't scope out of the implication. and indeed, we can't just declare that it does, because then we would expect the universally quantified variable to scope as well and that's no good. what we need instead is something like the ability to get the whole implication to be accessible for the presupposition to use.

i would suggest that dependent types provide precisely the right mechanism for this. if we use a dependently typed logic, (6) would become

    7. Σ(p : Πx. Π(f:File(x)). Σy. Duplicate(j,x,y)). Move(j,...,aNewFolder)

Π types are essentially ∀'s, but constructively, that is to say, to prove Πx:A.B means to give a function from A to B (where the type B might depend on the argument x). Similarly, Σ is witnessed ∃: to prove Σx:A.B you must provide some x together with a proof B (which might depend on the value x). Π and Σ are also the same as implication and conjunction when dependency isn't present (= are very similar to dynamic implication and conjunction in that the antecendent/left conjunct is sort of available on the right).

this then makes it relatively easy to explain the ability for y to scope into the right conjunct: the proof of the left conjunct -- p -- is visible in the right conjunct, and that proof is itself a function that maps each x (and a proof that it's a file) to a pair consisting of y and a proof that it's the result of a duplication. That is to say, if `a' is a file, and `f' is a proof of File(a), then p(a,f) is a pair, and the first element of the pair -- fst(p(a,f)) -- is that y we want, and the second element -- snd(p(a,f)) -- is the proof that fst(p(a,f)) is the result of duplication.

now we can get ahold of the y's in the right conjunct without also bringing the x's into scope -- by supplying each x and then getting out the first element of the pair:

    8. Σ(p : Πx. Π(f:File(x)). Σy. Duplicate(j,x,y)). Move(j, { fst(p(a,f0)), fst(p(b,f1)), fst(p(c,f2)) } ,aNewFolder)

this also recovers the forall-conjunct relationship that i mentioned earlier:

    9.   Σ(p : Πx:A.B).C   =   Σ(q : B[a/x]). Σ(q' : B[b/x]). Σ(q'' : B[c/x]). C

this holds regardless of what B is, including if B is an existential/Σ type