Degree Movement

@cite{bhatt-pancheva-2004} @cite{heim-2000} @cite{williams-1974}

The interpretation of degree clauses requires them to take scope at LF. Their syntactic placement is constrained by late merger (@cite{bhatt-pancheva-2004}); their semantic scope is constrained by the Heim-Kennedy Constraint (@cite{heim-2000}). Both constraints relate the LF position of a DegP to the LF position of any quantificational DP whose trace appears inside it.

Specializes lateMergerBleeds for degree clauses, formalizes the Heim-Kennedy Constraint as a structural filter, derives the Williams correlation as a corollary, and adds the @cite{bhatt-takahashi-2011} §4 (43) base-position generalization.

Heim-Kennedy Constraint (@cite{heim-2000})

If the scope of a quantificational DP contains the trace of a DegP, it also contains that DegP itself.

Mechanically: any LF in which a QP scopes between a DegP and the DegP's trace is illicit. Equivalently, a binding dependency QP → DegP-trace forces the DegP to scope at or above the QP.

Williams 1974 generalization (@cite{williams-1974}; B&P §5.2)

DegPs cannot escape an intensional verb whose subject's trace is in the DegP's restrictor.

This is the contrapositive of HKC: the only way for a DegP to scope above the intensional verb is if no binding dependency forces it down. B&P §5.2 derives this from HKC + the assumption that intensional subjects bind into degree predicates.

structure Minimalist.DegreeMovement.DegreeChainPosition : Type

A position on a movement chain that could host a degree clause. height is structural position; scopeOK records whether merging the degree clause at this position would yield a Heim-Kennedy- compliant LF (i.e., DegP-scope is at or above any QP whose trace it contains).

• height : ℕ
• scopeOK : Bool

def Minimalist.DegreeMovement.instDecidableEqDegreeChainPosition.decEq (x✝ x✝¹ : DegreeChainPosition) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Minimalist.DegreeMovement.instDecidableEqDegreeChainPosition : DecidableEq DegreeChainPosition

Equations

• Minimalist.DegreeMovement.instDecidableEqDegreeChainPosition = Minimalist.DegreeMovement.instDecidableEqDegreeChainPosition.decEq

def Minimalist.DegreeMovement.instReprDegreeChainPosition.repr : DegreeChainPosition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.DegreeMovement.instReprDegreeChainPosition : Repr DegreeChainPosition

Equations

• Minimalist.DegreeMovement.instReprDegreeChainPosition = { reprPrec := Minimalist.DegreeMovement.instReprDegreeChainPosition.repr }

def Minimalist.DegreeMovement.degreeClauseLateMergerBleeds (chain : List DegreeChainPosition) (binderHeight : ℕ) : Bool

The B&P specialization of lateMergerBleeds for degree clauses: the degree clause can late-merge above a Condition-C-relevant binder iff there is a scope-licit chain position above the binder.

Equations

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

theorem Minimalist.DegreeMovement.scopeOK_above_binder_bleeds (chain : List DegreeChainPosition) (binderHeight h : ℕ) (hgt : h > binderHeight) : degreeClauseLateMergerBleeds ({ height := h, scopeOK := true } :: chain) binderHeight = true

A scope-licit position above the binder bleeds Condition C for degree-clause late merger. Specialization of admissible_above_binder_bleeds.

theorem Minimalist.DegreeMovement.no_scopeOK_forces_reconstruction (chain : List DegreeChainPosition) (binderHeight : ℕ) (h : ∀ p ∈ chain, p.scopeOK = false) : degreeClauseLateMergerBleeds chain binderHeight = false

If no chain position is scope-licit, the degree clause is forced to reconstruct. Specialization of no_admissible_no_bleed.

structure Minimalist.DegreeMovement.ScopeBinding : Type

A scope binding records the LF heights of a DegP and a QP, plus whether the QP's trace appears inside the DegP's restrictor. qpBasePosition records the QP's base (theta) position separately from its surface-scope position qpHeight; this is needed for @cite{bhatt-takahashi-2011} §4 (43), which states the than-phrase- internal scope generalization in terms of the QP's base position relative to the degree trace, not its surface-scope position. For B&P 2004 / Heim 2001 usages where the distinction is irrelevant, set qpBasePosition := qpHeight.

• degHeight : ℕ

  LF height at which the DegP takes scope.

• qpHeight : ℕ

  LF height at which the QP takes scope.

• qpBasePosition : ℕ

  LF height of the QP's base (theta) position. For the B&T 2011 §4 (43) generalization this can differ from qpHeight; for the B&P / Heim usage it should equal qpHeight.

• qpBindsDeg : Bool

  Whether the QP binds into the DegP's restrictor (i.e., the DegP contains a trace of the QP).

def Minimalist.DegreeMovement.instDecidableEqScopeBinding.decEq (x✝ x✝¹ : ScopeBinding) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Minimalist.DegreeMovement.instDecidableEqScopeBinding : DecidableEq ScopeBinding

Equations

• Minimalist.DegreeMovement.instDecidableEqScopeBinding = Minimalist.DegreeMovement.instDecidableEqScopeBinding.decEq

@[implicit_reducible]

instance Minimalist.DegreeMovement.instReprScopeBinding : Repr ScopeBinding

Equations

• Minimalist.DegreeMovement.instReprScopeBinding = { reprPrec := Minimalist.DegreeMovement.instReprScopeBinding.repr }

def Minimalist.DegreeMovement.instReprScopeBinding.repr : ScopeBinding → ℕ → Std.Format

Equations

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

def Minimalist.DegreeMovement.IsHeimKennedy (b : ScopeBinding) : Prop

Heim-Kennedy Constraint (@cite{heim-2000}; B&P §4.1): a scope binding is licit iff either (a) there is no binding dependency from the QP into the DegP, OR (b) the DegP scopes at or above the QP.

Equations

• Minimalist.DegreeMovement.IsHeimKennedy b = (¬b.qpBindsDeg = true ∨ b.degHeight ≥ b.qpHeight)

@[implicit_reducible]

instance Minimalist.DegreeMovement.instDecidableIsHeimKennedy (b : ScopeBinding) : Decidable (IsHeimKennedy b)

Equations

• Minimalist.DegreeMovement.instDecidableIsHeimKennedy b = id inferInstance

theorem Minimalist.DegreeMovement.isHeimKennedy_no_dependency (degH qpH : ℕ) : IsHeimKennedy { degHeight := degH, qpHeight := qpH, qpBasePosition := qpH, qpBindsDeg := false }

Without a binding dependency, HKC imposes no scope constraint. qpBasePosition defaults to qpH (irrelevant to HKC).

theorem Minimalist.DegreeMovement.isHeimKennedy_dependency_requires_high_DegP (degH qpH : ℕ) (h : degH ≥ qpH) : IsHeimKennedy { degHeight := degH, qpHeight := qpH, qpBasePosition := qpH, qpBindsDeg := true }

With a binding dependency, HKC requires the DegP to scope at or above the binding QP.

theorem Minimalist.DegreeMovement.not_isHeimKennedy_QP_above_bound_DegP (degH qpH : ℕ) (h : degH < qpH) : ¬IsHeimKennedy { degHeight := degH, qpHeight := qpH, qpBasePosition := qpH, qpBindsDeg := true }

HKC's characteristic prohibition: a QP scoping strictly above a DegP it binds into is illicit.

theorem Minimalist.DegreeMovement.williams_scope_correlation (degH intH : ℕ) (h : degH < intH) : ¬IsHeimKennedy { degHeight := degH, qpHeight := intH, qpBasePosition := intH, qpBindsDeg := true }

Williams 1974 (@cite{williams-1974}; B&P §5.2 (37)): a DegP cannot take inverse scope over an intensional verb whose subject's trace is in the DegP's restrictor.

Stated as a contrapositive of HKC: if the QP (intensional subject) binds into the DegP and scopes strictly above it, the LF is illicit. The Williams generalization is therefore not a primitive constraint but a consequence of HKC + the assumption that intensional subjects bind into the degree predicate.

theorem Minimalist.DegreeMovement.williams_exempt_when_no_binding (degH intH : ℕ) : IsHeimKennedy { degHeight := degH, qpHeight := intH, qpBasePosition := intH, qpBindsDeg := false }

Conversely: when the intensional subject doesn't bind into the DegP, Williams's prohibition is lifted — the DegP is free to take wide scope. This is B&P's diagnosis of why the Williams generalization shows exceptions.

def Minimalist.DegreeMovement.IsBhattTakahashiScopeLicit (b : ScopeBinding) : Prop

@cite{bhatt-takahashi-2011} §4 (43): English allows than-phrase- internal scope for QPs whose base position does not c-command the degree trace. Stated as a structural filter on ScopeBinding, IsBhattTakahashiScopeLicit returns True when the QP's base position is at or below the DegP's height (no c-command of the degree trace from the base) — in which case than-internal scope is licensed.

Note this is distinct from HKC: HKC is over the QP's surface scope position relative to the DegP; B&T (43) is over the QP's base position. The two coincide for in-situ QPs (where surface = base) and diverge for QPs that have moved.

Equations

• Minimalist.DegreeMovement.IsBhattTakahashiScopeLicit b = (b.qpBasePosition ≤ b.degHeight)

@[implicit_reducible]

instance Minimalist.DegreeMovement.instDecidableIsBhattTakahashiScopeLicit (b : ScopeBinding) : Decidable (IsBhattTakahashiScopeLicit b)

Equations

• Minimalist.DegreeMovement.instDecidableIsBhattTakahashiScopeLicit b = id inferInstance

theorem Minimalist.DegreeMovement.not_isBhattTakahashiScopeLicit_base_above_DegP (degH qpH qpBase : ℕ) (qpBindsDeg : Bool) (h : qpBase > degH) : ¬IsBhattTakahashiScopeLicit { degHeight := degH, qpHeight := qpH, qpBasePosition := qpBase, qpBindsDeg := qpBindsDeg }

The structural witness of B&T (43): a QP whose base position is strictly above the DegP cannot license than-internal scope.

theorem Minimalist.DegreeMovement.isBhattTakahashiScopeLicit_base_below_DegP (degH qpH qpBase : ℕ) (qpBindsDeg : Bool) (h : qpBase ≤ degH) : IsBhattTakahashiScopeLicit { degHeight := degH, qpHeight := qpH, qpBasePosition := qpBase, qpBindsDeg := qpBindsDeg }

A QP whose base position is at or below the DegP licenses than-internal scope under B&T (43).