Davidson and Gagne (2022): "More is up" for domain restriction in ASL

A plural pronoun, a directional verb or a quantifier of ASL signed higher in signing space than the neutral plane refers to, or quantifies over, a wider domain than the contextually given one: at neutral height all became vampires is about the friends who watched the film, at a higher locus about everyone in the world, a third level fits between them, and the heights are relative rather than absolute. The height is not emphasis or gesture, since it weakens rather than strengthens an existential and context cannot override it, and it is not the domain widening of free-choice indefinites, since it attaches to negative and proportional quantifiers as well. It enters only where the structure contains a pronoun: bare nouns cannot take it, plain verbs need a separate IX-arc, directional verbs incorporate it, and a quantifier incorporates it or takes a following IX-arc as its phonology allows. The paper analyses height as a presuppositional feature of the plural pronoun, the neutral height requiring the referent's parts to lie in the context and a marked height requiring the referent to properly contain it, with the convention that vertically ordered marked loci denote properly nested plurals; a quantifier composes with the pronoun through a partitive, so that its domain is the pronoun's referent.

We state the feature semantics, the partitive composition and the monotonicity argument over the mereology and presupposition substrate, classify the fragment's quantifier signs by how they realise the pronoun, and check the paper's examples.

Implementation notes

• The marked height is one binary feature, since the paper keeps a feature rather than a purely iconic mapping; the ordering among marked loci is the paper's convention (45), a strictly monotone map from heights to plurals, taken as a hypothesis where it is used.
• A context in which the neutral pronoun denotes the sum of the contextual individuals is the parts of that sum, which is how (50) recovers all of them as quantification over the context.

References

• K. Davidson and D. Gagne, "More is up" for domain restriction in ASL (2022)
• L. Bergen, Joint inference in pragmatic reasoning (2016)
• W. A. Ladusaw, Semantic constraints on the English partitive construction (1982)
• C. A. Padden, Interaction of morphology and syntax in American Sign Language (1988)
• P. Schlenker, J. Lamberton and M. Santoro, Iconic variables (2013)
• J. Stanley and Z. Gendler Szabó, On quantifier domain restriction (2000)

The height feature on plural pronouns

def DavidsonGagne2022.Arc {E : Type u_1} [PartialOrder E] (x : E) : Prop

⟦arc⟧ of (46a) says that the referent of the plural pronoun is not an atom.

Equations

• DavidsonGagne2022.Arc x = ¬Mereology.Atom x

def DavidsonGagne2022.Neutral {E : Type u_1} [PartialOrder E] (C : Set E) (x : E) : Prop

⟦neutral⟧ of (47c) says that every part of the referent lies in the contextual domain.

Equations

• DavidsonGagne2022.Neutral C x = (Set.Iic x ⊆ C)

def DavidsonGagne2022.Domain {E : Type u_1} [PartialOrder E] (C : Set E) (x : E) : Prop

⟦domain-k⟧ of (44) and (46b) says that the referent properly contains the contextual domain.

Equations

• DavidsonGagne2022.Domain C x = (C ⊂ Set.Iic x)

def DavidsonGagne2022.Contrast {E : Type u_1} (alt : E → Set E) (x : E) : Prop

⟦-a⟧ of (47b) says that a marked horizontal locus presupposes a distinct focus alternative.

Equations

• DavidsonGagne2022.Contrast alt x = ∃ y ∈ alt x, x ≠ y

inductive DavidsonGagne2022.Height : Type

The vertical feature of section 5, the neutral plane or a marked locus above it.

• neutral : Height
• marked : Height

@[instance_reducible]

instance DavidsonGagne2022.instDecidableEqHeight : DecidableEq Height

Equations

• DavidsonGagne2022.instDecidableEqHeight x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DavidsonGagne2022.Height.presup {E : Type u_1} [PartialOrder E] (C : Set E) : Height → E → Prop

The presupposition a height feature contributes in the context C.

Equations

• DavidsonGagne2022.Height.presup C DavidsonGagne2022.Height.neutral = DavidsonGagne2022.Neutral C
• DavidsonGagne2022.Height.presup C DavidsonGagne2022.Height.marked = DavidsonGagne2022.Domain C

noncomputable def DavidsonGagne2022.ixArc {E : Type u_1} [PartialOrder E] {ι : Type u_2} (g : ι → E) (C : Set E) (h : Height) (i : ι) : Option E

⟦[ixᵢ]-arc-h⟧^{g,C} of (46e) and (47e) says that the pronoun denotes g i when that is a non-atomic plural meeting the height presupposition, and is otherwise undefined.

Equations

• DavidsonGagne2022.ixArc g C h i = if DavidsonGagne2022.Arc (g i) ∧ DavidsonGagne2022.Height.presup C h (g i) then some (g i) else none

theorem DavidsonGagne2022.not_domain_of_neutral {E : Type u_1} [PartialOrder E] {C : Set E} {x : E} (h : Neutral C x) : ¬Domain C x

A referent within the context does not properly extend it, so the two heights exclude each other.

theorem DavidsonGagne2022.neutral_iff {E : Type u_1} [PartialOrder E] {c x : E} : Neutral (Set.Iic c) x ↔ x ≤ c

When the context is the parts of its sum c, the neutral presupposition is parthood of c and the marked one is proper extension of c.

theorem DavidsonGagne2022.domain_iff {E : Type u_1} [PartialOrder E] {c x : E} : Domain (Set.Iic c) x ↔ c < x

theorem DavidsonGagne2022.domain_of_lt {E : Type u_1} [PartialOrder E] {H : Type u_2} [Preorder H] {ref : H → E} (hconv : StrictMono ref) {C : Set E} {k k' : H} (hk : Domain C (ref k)) (hkk' : k < k') : Domain C (ref k')

Under the convention (45) that vertical order maps marked loci to proper parts, the marked presupposition met at one locus is met at every higher one, as in (48).

theorem DavidsonGagne2022.remainder {E : Type u_2} [GeneralizedCoheytingAlgebra E] {a d d' : E} (h : a ≤ d) (h' : d ≤ d') : a ⊔ d \ a = d ∧ d \ a ≤ d' \ a

The remainder of a plane less an established locus sums with it to the plane, and a higher plane's remainder contains the neutral plane's, as in (14).

Partitive composition

def DavidsonGagne2022.partitive {E : Type u_1} [PartialOrder E] (x : E) : E → Prop

The partitive ⟦of⟧ of (50b), after [Lad82], takes the pronoun's referent x to its parts, the y with y ≤ x.

Equations

• DavidsonGagne2022.partitive x x✝ = (x✝ ≤ x)

noncomputable def DavidsonGagne2022.fsAllOf {E : Type u_1} [PartialOrder E] {W : Type u_2} (pron : W → Option E) (Q : E → W → Prop) : W → SignType

FS(ALL) composed with a partitive pronoun over worlds W, as in (50e) and (51e), is defined where the pronoun is and asserts that every part of its referent satisfies the scope.

Equations

• DavidsonGagne2022.fsAllOf pron Q = Presupposition.presupOfReferent pron fun (x : E) (w : W) => Quantifier.GQ.every (DavidsonGagne2022.partitive x) fun (x : E) => Q x w

theorem DavidsonGagne2022.fsAllOf_ixArc_eq_zero_iff {E : Type u_1} [PartialOrder E] {W : Type u_2} {ι : Type u_3} {g : ι → E} {C : Set E} {h : Height} {i : ι} {Q : E → W → Prop} {w : W} : fsAllOf (fun (x : W) => ixArc g C h i) Q w = 0 ↔ ¬(Arc (g i) ∧ Height.presup C h (g i))

The quantifier presupposes what its pronoun presupposes, so FS(ALL)-of-[ixᵢ-arc-h] is undefined iff g i is not a non-atomic plural meeting the height presupposition.

theorem DavidsonGagne2022.fsAllOf_eq_one_iff {E : Type u_1} [PartialOrder E] {W : Type u_2} {pron : W → Option E} {Q : E → W → Prop} {w : W} {c : E} (h : pron w = some c) : fsAllOf pron Q w = 1 ↔ ∀ y ∈ Set.Iic c, Q y w

Where the neutral pronoun denotes the sum of the context, FS(ALL)-neutral quantifies over the context, as in (50e).

theorem DavidsonGagne2022.all_of_le {E : Type u_1} [PartialOrder E] {x x' : E} (h : x ≤ x') (Q : E → Prop) : Quantifier.GQ.every (partitive x') Q → Quantifier.GQ.every (partitive x) Q

With the marked pronoun denoting a plural containing the neutral one, FS(ALL) and NONE at the higher locus entail their neutral forms, while SOMEONE at the neutral locus entails its high form, as in section 4.

theorem DavidsonGagne2022.no_of_le {E : Type u_1} [PartialOrder E] {x x' : E} (h : x ≤ x') (Q : E → Prop) : Quantifier.GQ.no (partitive x') Q → Quantifier.GQ.no (partitive x) Q

theorem DavidsonGagne2022.some_of_le {E : Type u_1} [PartialOrder E] {x x' : E} (h : x ≤ x') (Q : E → Prop) : Quantifier.GQ.some (partitive x) Q → Quantifier.GQ.some (partitive x') Q

theorem DavidsonGagne2022.not_strengthening {E : Type u_1} [PartialOrder E] {x x' w : E} (hw : w ≤ x') (hwx : ¬w ≤ x) : ¬∀ (Q : E → Prop), Quantifier.GQ.some (partitive x') Q → Quantifier.GQ.some (partitive x) Q

Height is not intensification (section 4, after (36)), since a part of the wider plural outside the narrower one makes SOMEONE-high true where SOMEONE-neutral is false, so on no reading of height as strengthening, on which the high form would entail the neutral one as [Ber16] has for stressed quantifiers, does the existential come out right.

Realising the pronoun in the quantifier

def DavidsonGagne2022.incorporating : List ASL.Determiners.Sign

The quantifier signs that incorporate the pronoun and carry the height themselves ((32)–(36), (39)).

Equations

• One or more equations did not get rendered due to their size.

def DavidsonGagne2022.sequential : List ASL.Determiners.Sign

The quantifier signs whose phonology holds them in place, so that the height-marked IX-arc follows them ((37), (39)).

Equations

• DavidsonGagne2022.sequential = [ASL.Determiners.Sign.few, ASL.Determiners.Sign.each, ASL.Determiners.Sign.most, ASL.Determiners.Sign.allB, ASL.Determiners.Sign.many]

theorem DavidsonGagne2022.realization_rows (e : Datum) : e ∈ Examples.all → ∀ q ∈ ASL.Determiners.Sign.toList, e.feature? "quantifier" = some q.form → (e.feature? "realization" = some "simultaneous" → q ∈ incorporating) ∧ (e.feature? "realization" = some "sequential" → q ∈ sequential)

Each quantifier row realises height as its sign's class predicts.

theorem DavidsonGagne2022.no_double_marking (e : Datum) : e ∈ Examples.all → e.feature? "realization" = some "both" → e.judgment = Judgment.ungrammatical

A quantifier that incorporates the pronoun rejects a further height-marked IX-arc, as in (38).

theorem DavidsonGagne2022.verb_height_iff_directional (e : Datum) : e ∈ Examples.all → e.feature? "heightOn" = some "verb" → (e.judgment = Judgment.acceptable ↔ e.feature? "verbClass" = some "directional")

Height marks a verb itself only in [Pad88]'s directional class ((21)–(24)); a plain verb takes a separate IX-arc.

theorem DavidsonGagne2022.noun_no_widening (e : Datum) : e ∈ Examples.all → e.feature? "heightOn" = some "noun" → List.lookup "widened" e.readings = some Judgment.unacceptable

Height on a bare noun has no widened-domain reading, as in (27).