∀v((u1 6= v ∧ . . . ∧ (un 6= v) → V (v)(i) = V (v)(j)) ,
a term which expresses that states i and j differ at most in u1 ,. . . ,un; i[ ]j
will stand for the formula ∀v(V (v)(i) = V (v)(j)). We impose the following
axioms.
AX1 ∀i∀v∀x ∃j (i [v]j ∧ V(v)(j) = x)
AX2 ∀i∀j (i [ ]j → i = j)
AX3 u 6= u0, for each two different discourse referents (con-
stants of type π) u and u0 .
AX1 requires that for each state, each pigeon-hole and each object, there
must be a second state that is just like the first one, except that the given
object is an occupant of the given pigeon-hole. AX2 says that two states
cannot be different if they agree in all pigeon-holes. AX3 makes sure that
different discourse referents refer to different pigeon-holes, so that an update
on one discourse referent will not result in a change in some other discourse
referent’s value.
Type logic enriched with these three first-order non-logical axioms has
the very useful property that it allows us to have a form of the ‘unselec-
tive binding’ that seems to be omnipresent in natural language (see Lewis
[1975]). Since states correspond to lists of items, quantifying over states cor-
responds to quantifying over such lists. The following lemma gives a precise
formulation of this phenomenon; it has an elementary proof.
Unselective Binding Lemma. Let u1 ,. . . ,un be constants of type π, let
x 1,... ,xn be distinct variables of type e, let φ be a formula that does not
contain j and let = be the result of the simultaneous substitution of V(u 1 )(j)
for x 1 and ... and V(un)(j) for xn in φ, then:
=AX ∀i (∃j (i [u 1,... ,u n ]j ∧ φ0) → ∃x 1... ∃x n φ)
=AX ∀i (∀j (i [u 1,... ,U n ]j → ψ0) ^ ∀x 1... ∀x n φ)
We now come to the emulation of the DRT language in type logic. Let us fix
some type s variable i and define (u = = V(u)(i) for each discourse referent
(constant of type π) u and (t = = t for each type e term t, and let us agree
to write
P τ for λiP (τ=,
τ 1 Rτ 2 for λi (R(τ 1 = (τ 2= ),
τ 1 is τ2 for λi((τ 1 = = (τ2= ),