Bhatt and Pancheva (2004): Late Merger of Degree Clauses

Bhatt and Pancheva propose that a degree clause, the than- or as-phrase, is merged countercyclically as the complement of the degree head after the head has raised to its scope position, so the surface site of the clause marks the scope of the comparison. This refines Williams's generalization: the degree head scopes at least as high as its clause, by countercyclic merger, and exactly as high, because Trace Conversion would otherwise intersect the clause into the second argument of the nonconservative -er and yield a contradiction.

Main results

• hkc_22, hkc_43: the Heim–Kennedy constraint excludes the LFs (22b) and (43b).
• at_least_as_high, exactly_as_high: the Extraposition-Scope Generalization, (39), on the rows.
• ellipsisScope: the Ellipsis-Scope Generalization, (59), on the LFs of (62).
• conditionC_scope: the Condition C–Scope Generalization on the LFs of (69).
• erSem_not_conservative: -er is not conservative, (86), so the clause merges only at the DegP's scope position.

Implementation notes

• LFs are category-free trees at the paper's bracketing, PhraseStructure.Tree Unit String, with non-branching and elided material written as one leaf; scope is Branching.cCommand and the constraint Degree.IsHeimKennedy on it.
• The comparative of (84) is erSem, proper inclusion of degree sets, and (85) is its value on [Ken99]'s positive extents; Trace Conversion itself is not formalized, only the second argument it hands -er.
• Section 4.2 is [Hei00]'s result and is Heim2001.forall_collapse; the ordering constraint between than- and result clauses, (48) and (50), and the ellipsis resolution of Section 6.3 are recorded as rows.

References

• [BP04b]
• [Hei00]
• [Wil74]
• [Leb88]
• [Ken99]

The Heim–Kennedy constraint (Section 4.1)

def BhattPancheva2004.lf22a : PhraseStructure.Tree Unit String

The LF (22a) of every girl is exactly 1 inch taller than that, with the quantifier over the DegP, is [every girl [λx [[DegP exactly 1 inch -er than that] [λd [x is d-tall]]]]].

Equations

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

def BhattPancheva2004.lf22b : PhraseStructure.Tree Unit String

The LF (22b) puts the DegP over the quantifier, [[DegP exactly 1 inch -er than that] [λd [every girl [λx [x is d-tall]]]]].

Equations

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

theorem BhattPancheva2004.hkc_22 : Degree.IsHeimKennedy (RoseTree.cCommand lf22a) { toList := [0] } { toList := [1, 0, 0] } { toList := [1, 0, 1, 0, 1, 0] } ∧ ¬Degree.IsHeimKennedy (RoseTree.cCommand lf22b) { toList := [1, 0, 0] } { toList := [0] } { toList := [1, 0, 1, 0, 1, 0] }

(24) admits (22a) and excludes (22b), where the quantifier's scope contains the degree trace but not the DegP, the configuration (25).

The Extraposition-Scope Generalization (Section 5.2)

def BhattPancheva2004.lf43a : PhraseStructure.Tree Unit String

The LF (43a) of Mary climbed higher than 1,000 feet before you did puts the before-clause over the DegP, [[Mary [[climbed [t high]] [DegP -er than 1,000 feet]]] [before you did]].

Equations

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

def BhattPancheva2004.lf43b : PhraseStructure.Tree Unit String

The LF (43b) puts the DegP over the before-clause, [[[Mary [climbed [t high]]] [before you did]] [DegP -er than 1,000 feet]].

Equations

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

theorem BhattPancheva2004.hkc_43 : Degree.IsHeimKennedy (RoseTree.cCommand lf43a) { toList := [1] } { toList := [0, 1, 1] } { toList := [0, 1, 0, 1, 0] } ∧ ¬Degree.IsHeimKennedy (RoseTree.cCommand lf43b) { toList := [0, 1] } { toList := [1] } { toList := [0, 0, 1, 1, 0] }

(43) has the reading with the before-clause over the comparison and not the reading with the comparison over the before-clause, in which the before-clause's scope contains the degree trace but not the DegP; (44), whose clause is merged above the before-clause, has only the LF (43b).

inductive BhattPancheva2004.Site : Type

The site of an extraposed clause relative to the operator the comparison may scope over.

• low : Site
• high : Site

@[instance_reducible]

instance BhattPancheva2004.instDecidableEqSite : DecidableEq Site

Equations

• BhattPancheva2004.instDecidableEqSite x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def BhattPancheva2004.instReprSite.repr : Site → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BhattPancheva2004.instReprSite : Repr Site

Equations

• BhattPancheva2004.instReprSite = { reprPrec := BhattPancheva2004.instReprSite.repr }

structure BhattPancheva2004.Row : Type

An extraposition datum records the clause's site, whether its associate is the bare DegP rather than a comparative DP, and whether the comparison's narrow and wide scope readings are available.

• site : Site
• degP : Bool
• narrow : Bool
• wide : Bool

def BhattPancheva2004.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance BhattPancheva2004.instDecidableEqRow : DecidableEq Row

Equations

• BhattPancheva2004.instDecidableEqRow = BhattPancheva2004.instDecidableEqRow.decEq

@[instance_reducible]

instance BhattPancheva2004.instReprRow : Repr Row

Equations

• BhattPancheva2004.instReprRow = { reprPrec := BhattPancheva2004.instReprRow.repr }

def BhattPancheva2004.instReprRow.repr : Row → ℕ → Std.Format

Equations

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

def BhattPancheva2004.Row.ofDatum (e : Datum) : Option Row

A row from the paper's features.

Equations

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

def BhattPancheva2004.rows : List Row

The extraposition data of Section 5.2, (41) to (46) and (53) to (54).

Equations

• BhattPancheva2004.rows = List.filterMap BhattPancheva2004.Row.ofDatum BhattPancheva2004.Examples.all

theorem BhattPancheva2004.at_least_as_high (r : Row) : r ∈ rows → r.site = Site.high → r.narrow = false

Countercyclic merger derives one half of (39), (38), since a clause merged above an operator leaves the comparison no scope below it, (42), (44), (46), (53b) and (54b).

theorem BhattPancheva2004.exactly_as_high : (∀ r ∈ rows, r.degP = true → r.site = Site.low → r.wide = false) ∧ ∀ r ∈ rows, r.degP = false → r.site = Site.low → r.wide = true

In the other half of (39), a bare DegP whose clause is merged below an operator has no scope above it, (43), (53a) and (54a), whereas a comparative DP raises with its clause, (41) and (45).

Ellipsis and Condition C mark the scope of the comparison (Section 6)

structure BhattPancheva2004.TellLF : Type

An LF of her father tells her to work harder than Mary's boss does, (62) and (69), records the tree and the positions of the DegP, the degree clause, the pronoun, the matrix predicate and the matrix and embedded VPs.

• tree : PhraseStructure.Tree Unit String
• degP : Core.Order.TreePath
• clause : Core.Order.TreePath
• pronoun : Core.Order.TreePath
• tells : Core.Order.TreePath
• matrixVP : Core.Order.TreePath
• embeddedVP : Core.Order.TreePath

def BhattPancheva2004.low : TellLF

With the clause merged low, at the embedded clause, the LF is (69a), [her father [tells [her [[λd PRO to work d-hard] [-er than Mary's boss does]]]]].

Equations

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

def BhattPancheva2004.high : TellLF

With the clause merged high, at the matrix clause, the LF is (69c), [[λd her father tells her to work d-hard] [-er than Mary's boss does]].

Equations

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

theorem BhattPancheva2004.ellipsisScope : (∀ lf ∈ [low, high], (lf.degP, lf.embeddedVP) ∈ RoseTree.cCommand lf.tree) ∧ (low.degP, low.matrixVP) ∉ RoseTree.cCommand low.tree ∧ (high.degP, high.matrixVP) ∈ RoseTree.cCommand high.tree

The Ellipsis-Scope Generalization, (59), holds on the LFs of (62). The scope of the DegP contains the embedded VP at either site and the matrix VP only at the high site, so the reading (62b), the clause merged low with the matrix VP elided, is the one missing.

theorem BhattPancheva2004.conditionC_scope (lf : TellLF) : lf ∈ [low, high] → ((lf.pronoun, lf.clause) ∈ RoseTree.cCommand lf.tree ↔ (lf.degP, lf.tells) ∉ RoseTree.cCommand lf.tree)

The Condition C–Scope Generalization, (69) and (70), holds, since the pronoun c-commands the name in the degree clause exactly when the comparison does not scope over the matrix predicate.

Nonconservativity forces late merger (Section 7)

def BhattPancheva2004.erSem {D : Type u_2} (A B : Set D) : Prop

The comparative degree quantifier, (84), holds when its first argument, the degree clause, is a proper subset of its second.

Equations

• BhattPancheva2004.erSem A B = (A ⊂ B)

theorem BhattPancheva2004.erSem_Iic_iff {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : erSem (Set.Iic (μ b)) (Set.Iic (μ a)) ↔ μ b < μ a

On [Ken99]'s positive extents -er compares the measures, (85).

theorem BhattPancheva2004.erSem_inter_contradictory {D : Type u_2} (A B : Set D) : ¬erSem A (A ∩ B)

Trace Conversion of an early-merged degree clause intersects it into the second argument, and A ⊂ A ∩ B is a contradiction, (86) and (87).

theorem BhattPancheva2004.erSem_not_conservative {D : Type u_2} [Nonempty D] : ¬Quantifier.GQ.Conservative erSem

A conservative quantifier is unaffected by the intersection, and -er is not conservative, (82) against (86).