Degree movement

A degree quantifier, -er with its differential, is a quantificational argument of the gradable predicate and takes scope by Quantifier Raising ([Hei01]). The Heim–Kennedy constraint filters the LFs this produces: if the scope of a quantificational DP contains the trace of a DegP, it also contains that DegP ([Hei01], [BP04b]), so no quantifier intervenes between a degree abstraction and the variable it binds, the configuration *λd … QP … d. Scope is the c-command domain, so on a scope relation C the constraint relates three positions, the quantifier q, the DegP δ and its trace t: IsHeimKennedy C q δ t. [Ken99] reads the absence of the excluded readings as the absence of degree movement; [Hei01] keeps the movement and the filter, [BP04b] merges the degree clause at the DegP's scope position so that its surface site marks the scope the filter constrains, and the than-phrase-internal scope generalization of [BT11] is the constraint evaluated at the quantifier's base position.

References

• [Hei01]
• [BP04b]
• [BT11]
• [Ken99]

def Degree.IsHeimKennedy {Node : Type u_1} (C : Set (Node × Node)) (q δ t : Node) : Prop

The Heim–Kennedy constraint on the scope relation C: a quantifier q whose scope contains the trace t of the DegP δ has δ in its scope too.

Equations

• Degree.IsHeimKennedy C q δ t = ((q, t) ∈ C → (q, δ) ∈ C)

@[instance_reducible]

instance Degree.instDecidableIsHeimKennedyOfMemProdSetMk {Node : Type u_1} {C : Set (Node × Node)} {q δ t : Node} [Decidable ((q, t) ∈ C)] [Decidable ((q, δ) ∈ C)] : Decidable (IsHeimKennedy C q δ t)

Equations

• Degree.instDecidableIsHeimKennedyOfMemProdSetMk = { decide := if h : (q, t) ∈ C then decide ((fun (a : (q, t) ∈ C) => (q, δ) ∈ C) h) else true, reflects_decide := ⋯ }

theorem Degree.isHeimKennedy_of_not_mem {Node : Type u_1} {C : Set (Node × Node)} {q δ t : Node} (h : ¬(q, t) ∈ C) : IsHeimKennedy C q δ t

A quantifier whose scope excludes the trace is unconstrained.

theorem Degree.isHeimKennedy_of_mem {Node : Type u_1} {C : Set (Node × Node)} {q δ t : Node} (h : (q, δ) ∈ C) : IsHeimKennedy C q δ t

A quantifier whose scope contains the DegP is unconstrained.

theorem Degree.not_isHeimKennedy_iff {Node : Type u_1} {C : Set (Node × Node)} {q δ t : Node} : ¬IsHeimKennedy C q δ t ↔ (q, t) ∈ C ∧ ¬(q, δ) ∈ C

The excluded configuration *λd … QP … d: the quantifier's scope contains the trace but not the DegP.