@cite{bruening-2001} — QR Obeys Superiority

@cite{bruening-2001} @cite{larson-1988} @cite{may-1985} @cite{pylkkanen-2008}

Bruening's Linguistic Inquiry paper "QR Obeys Superiority: Frozen Scope and ACD" — both the empirical scope-freezing data set and the theoretical Minimalist analysis (QR locality + superiority + phase-theoretic barriers).

Part I: Empirical data

Theory-neutral scope-freezing examples primarily compiled from @cite{bruening-2001}, with contributions from @cite{larson-1988} (double-object construction examples) and @cite{may-1985} (foundational scope-availability vocabulary). Was formerly Phenomena/Quantification/Data.lean; renamed per the provenance-tracking policy.

Downstream consumer Steedman2000.lean imports from here.

Part II: Theoretical analysis (Minimalist QR)

Bruening's central thesis — QR obeys Superiority — is derived formally: double-object scope freezing follows from asymmetric c-command in @cite{pylkkanen-2008}'s Voice + low-Appl tree, where the goal asymmetrically c-commands the theme. Other freezing contexts (possessor, passive, attitude) are analyzed via DP-phase / adjunct-island / clause-boundary barriers.

Was formerly Phenomena/Quantification/MinimalismScope.lean; absorbed here per the "study files own the analysis they advance" policy (CLAUDE.md).

Sections

• ScopeFreezing: Empirical configurations where inverse scope is unavailable
• ScopeWordOrder: Word order effects on scope in verb-final constructions
• MinimalistAnalysis: Theoretical derivation of freezing from Minimalist QR

inductive Phenomena.Quantification.Bruening2001.Availability : Type

Available scope readings for a sentence

• ambiguous : Availability
• surfaceOnly : Availability
• inverseOnly : Availability

@[implicit_reducible]

instance Phenomena.Quantification.Bruening2001.instDecidableEqAvailability : DecidableEq Availability

Equations

• Phenomena.Quantification.Bruening2001.instDecidableEqAvailability x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Quantification.Bruening2001.instReprAvailability.repr : Availability → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Quantification.Bruening2001.instReprAvailability : Repr Availability

Equations

• Phenomena.Quantification.Bruening2001.instReprAvailability = { reprPrec := Phenomena.Quantification.Bruening2001.instReprAvailability.repr }

@[implicit_reducible]

instance Phenomena.Quantification.Bruening2001.instInhabitedAvailability : Inhabited Availability

Equations

• Phenomena.Quantification.Bruening2001.instInhabitedAvailability = { default := Phenomena.Quantification.Bruening2001.instInhabitedAvailability.default }

def Phenomena.Quantification.Bruening2001.instInhabitedAvailability.default : Availability

Equations

• Phenomena.Quantification.Bruening2001.instInhabitedAvailability.default = Phenomena.Quantification.Bruening2001.Availability.ambiguous

inductive Phenomena.Quantification.Bruening2001.Confidence : Type

Confidence in the judgment

• clear : Confidence
• gradient : Confidence
• controversial : Confidence

@[implicit_reducible]

instance Phenomena.Quantification.Bruening2001.instDecidableEqConfidence : DecidableEq Confidence

Equations

• Phenomena.Quantification.Bruening2001.instDecidableEqConfidence x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Quantification.Bruening2001.instReprConfidence : Repr Confidence

Equations

• Phenomena.Quantification.Bruening2001.instReprConfidence = { reprPrec := Phenomena.Quantification.Bruening2001.instReprConfidence.repr }

def Phenomena.Quantification.Bruening2001.instReprConfidence.repr : Confidence → ℕ → Std.Format

Equations

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

def Phenomena.Quantification.Bruening2001.instInhabitedConfidence.default : Confidence

Equations

• Phenomena.Quantification.Bruening2001.instInhabitedConfidence.default = Phenomena.Quantification.Bruening2001.Confidence.clear

@[implicit_reducible]

instance Phenomena.Quantification.Bruening2001.instInhabitedConfidence : Inhabited Confidence

Equations

• Phenomena.Quantification.Bruening2001.instInhabitedConfidence = { default := Phenomena.Quantification.Bruening2001.instInhabitedConfidence.default }

inductive Phenomena.Quantification.Bruening2001.DataSource : Type

Source of the judgment

• introspective : DataSource
• experimental : DataSource
• corpus : DataSource

@[implicit_reducible]

instance Phenomena.Quantification.Bruening2001.instDecidableEqDataSource : DecidableEq DataSource

Equations

• Phenomena.Quantification.Bruening2001.instDecidableEqDataSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Quantification.Bruening2001.instReprDataSource : Repr DataSource

Equations

• Phenomena.Quantification.Bruening2001.instReprDataSource = { reprPrec := Phenomena.Quantification.Bruening2001.instReprDataSource.repr }

def Phenomena.Quantification.Bruening2001.instReprDataSource.repr : DataSource → ℕ → Std.Format

Equations

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

def Phenomena.Quantification.Bruening2001.instInhabitedDataSource.default : DataSource

Equations

• Phenomena.Quantification.Bruening2001.instInhabitedDataSource.default = Phenomena.Quantification.Bruening2001.DataSource.introspective

@[implicit_reducible]

instance Phenomena.Quantification.Bruening2001.instInhabitedDataSource : Inhabited DataSource

Equations

• Phenomena.Quantification.Bruening2001.instInhabitedDataSource = { default := Phenomena.Quantification.Bruening2001.instInhabitedDataSource.default }

inductive Phenomena.Quantification.Bruening2001.FreezingContext : Type

Types of configurations that induce scope freezing

• none : FreezingContext
• possessor : FreezingContext
• doubleObject : FreezingContext
• passive : FreezingContext
• heavyNP : FreezingContext
• weakCrossover : FreezingContext
• adjunct : FreezingContext
• attitude : FreezingContext

@[implicit_reducible]

instance Phenomena.Quantification.Bruening2001.instDecidableEqFreezingContext : DecidableEq FreezingContext

Equations

• Phenomena.Quantification.Bruening2001.instDecidableEqFreezingContext x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Quantification.Bruening2001.instReprFreezingContext.repr : FreezingContext → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Quantification.Bruening2001.instReprFreezingContext : Repr FreezingContext

Equations

• Phenomena.Quantification.Bruening2001.instReprFreezingContext = { reprPrec := Phenomena.Quantification.Bruening2001.instReprFreezingContext.repr }

@[implicit_reducible]

instance Phenomena.Quantification.Bruening2001.instInhabitedFreezingContext : Inhabited FreezingContext

Equations

• Phenomena.Quantification.Bruening2001.instInhabitedFreezingContext = { default := Phenomena.Quantification.Bruening2001.instInhabitedFreezingContext.default }

def Phenomena.Quantification.Bruening2001.instInhabitedFreezingContext.default : FreezingContext

Equations

• Phenomena.Quantification.Bruening2001.instInhabitedFreezingContext.default = Phenomena.Quantification.Bruening2001.FreezingContext.none

structure Phenomena.Quantification.Bruening2001.Example : Type

A scope freezing example with empirical judgment

• id : String
• sentence : String
• quant1 : String
• quant2 : String
• context : FreezingContext
• observed : Availability
• confidence : Confidence
• source : DataSource
• surfaceGloss : String
• inverseGloss : String
• notes : String

@[implicit_reducible]

instance Phenomena.Quantification.Bruening2001.instReprExample : Repr Example

Equations

• Phenomena.Quantification.Bruening2001.instReprExample = { reprPrec := Phenomena.Quantification.Bruening2001.instReprExample.repr }

def Phenomena.Quantification.Bruening2001.instReprExample.repr : Example → ℕ → Std.Format

Equations

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

def Phenomena.Quantification.Bruening2001.possessor_baseline : Example

Equations

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

def Phenomena.Quantification.Bruening2001.possessor_frozen : Example

Equations

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

def Phenomena.Quantification.Bruening2001.possessor_variant1 : Example

Equations

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

def Phenomena.Quantification.Bruening2001.possessor_variant2 : Example

Equations

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

def Phenomena.Quantification.Bruening2001.dative_baseline : Example

Equations

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

def Phenomena.Quantification.Bruening2001.dative_frozen : Example

Equations

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

def Phenomena.Quantification.Bruening2001.dative_variant : Example

Equations

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

def Phenomena.Quantification.Bruening2001.passive_baseline : Example

Equations

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

def Phenomena.Quantification.Bruening2001.passive_frozen : Example

Equations

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

def Phenomena.Quantification.Bruening2001.passive_variant : Example

Equations

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

def Phenomena.Quantification.Bruening2001.heavy_baseline : Example

Equations

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

def Phenomena.Quantification.Bruening2001.heavy_frozen : Example

Equations

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

def Phenomena.Quantification.Bruening2001.crossover_baseline : Example

Equations

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

def Phenomena.Quantification.Bruening2001.crossover_frozen : Example

Equations

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

def Phenomena.Quantification.Bruening2001.attitude_frozen : Example

Equations

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

def Phenomena.Quantification.Bruening2001.possessorExamples : List Example

Equations

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

def Phenomena.Quantification.Bruening2001.doubleObjectExamples : List Example

Equations

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

def Phenomena.Quantification.Bruening2001.passiveExamples : List Example

Equations

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

def Phenomena.Quantification.Bruening2001.heavyNPExamples : List Example

Equations

• Phenomena.Quantification.Bruening2001.heavyNPExamples = [Phenomena.Quantification.Bruening2001.heavy_baseline, Phenomena.Quantification.Bruening2001.heavy_frozen]

def Phenomena.Quantification.Bruening2001.crossoverExamples : List Example

Equations

• Phenomena.Quantification.Bruening2001.crossoverExamples = [Phenomena.Quantification.Bruening2001.crossover_baseline, Phenomena.Quantification.Bruening2001.crossover_frozen]

def Phenomena.Quantification.Bruening2001.attitudeExamples : List Example

Equations

• Phenomena.Quantification.Bruening2001.attitudeExamples = [Phenomena.Quantification.Bruening2001.attitude_frozen]

def Phenomena.Quantification.Bruening2001.allExamples : List Example

Equations

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

def Phenomena.Quantification.Bruening2001.possessorFreezingIsClear : Bool

Possessor freezing is robust (clear judgments)

Equations

• Phenomena.Quantification.Bruening2001.possessorFreezingIsClear = (Phenomena.Quantification.Bruening2001.possessor_frozen.confidence == Phenomena.Quantification.Bruening2001.Confidence.clear)

def Phenomena.Quantification.Bruening2001.doubleObjectFreezingIsClear : Bool

Double object freezing is robust

Equations

• Phenomena.Quantification.Bruening2001.doubleObjectFreezingIsClear = (Phenomena.Quantification.Bruening2001.dative_frozen.confidence == Phenomena.Quantification.Bruening2001.Confidence.clear)

def Phenomena.Quantification.Bruening2001.passiveFreezingIsGradient : Bool

Passive freezing is more gradient

Equations

• Phenomena.Quantification.Bruening2001.passiveFreezingIsGradient = (Phenomena.Quantification.Bruening2001.passive_frozen.confidence == Phenomena.Quantification.Bruening2001.Confidence.gradient)

def Phenomena.Quantification.Bruening2001.frozenCount : ℕ

Count frozen examples

Equations

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

def Phenomena.Quantification.Bruening2001.ambiguousCount : ℕ

Count ambiguous baselines

Equations

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

inductive Phenomena.Quantification.Bruening2001.VerbOrder : Type

Word order patterns in verb-final constructions.

• verbRaising : VerbOrder
• verbProjectionRaising : VerbOrder

@[implicit_reducible]

instance Phenomena.Quantification.Bruening2001.instDecidableEqVerbOrder : DecidableEq VerbOrder

Equations

• Phenomena.Quantification.Bruening2001.instDecidableEqVerbOrder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Quantification.Bruening2001.instReprVerbOrder.repr : VerbOrder → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Quantification.Bruening2001.instReprVerbOrder : Repr VerbOrder

Equations

• Phenomena.Quantification.Bruening2001.instReprVerbOrder = { reprPrec := Phenomena.Quantification.Bruening2001.instReprVerbOrder.repr }

def Phenomena.Quantification.Bruening2001.instInhabitedVerbOrder.default : VerbOrder

Equations

• Phenomena.Quantification.Bruening2001.instInhabitedVerbOrder.default = Phenomena.Quantification.Bruening2001.VerbOrder.verbRaising

@[implicit_reducible]

instance Phenomena.Quantification.Bruening2001.instInhabitedVerbOrder : Inhabited VerbOrder

Equations

• Phenomena.Quantification.Bruening2001.instInhabitedVerbOrder = { default := Phenomena.Quantification.Bruening2001.instInhabitedVerbOrder.default }

def Phenomena.Quantification.Bruening2001.blocksInverseScope : VerbOrder → Bool

Whether a word order blocks inverse scope

Equations

• Phenomena.Quantification.Bruening2001.blocksInverseScope Phenomena.Quantification.Bruening2001.VerbOrder.verbRaising = false
• Phenomena.Quantification.Bruening2001.blocksInverseScope Phenomena.Quantification.Bruening2001.VerbOrder.verbProjectionRaising = true

inductive Phenomena.Quantification.Bruening2001.ScopeAvailability : Type

Available scope readings for a sentence.

• surfaceOnly : ScopeAvailability
• ambiguous : ScopeAvailability

@[implicit_reducible]

instance Phenomena.Quantification.Bruening2001.instDecidableEqScopeAvailability : DecidableEq ScopeAvailability

Equations

• Phenomena.Quantification.Bruening2001.instDecidableEqScopeAvailability x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Quantification.Bruening2001.instReprScopeAvailability : Repr ScopeAvailability

Equations

• Phenomena.Quantification.Bruening2001.instReprScopeAvailability = { reprPrec := Phenomena.Quantification.Bruening2001.instReprScopeAvailability.repr }

def Phenomena.Quantification.Bruening2001.instReprScopeAvailability.repr : ScopeAvailability → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Quantification.Bruening2001.instInhabitedScopeAvailability : Inhabited ScopeAvailability

Equations

• Phenomena.Quantification.Bruening2001.instInhabitedScopeAvailability = { default := Phenomena.Quantification.Bruening2001.instInhabitedScopeAvailability.default }

def Phenomena.Quantification.Bruening2001.instInhabitedScopeAvailability.default : ScopeAvailability

Equations

• Phenomena.Quantification.Bruening2001.instInhabitedScopeAvailability.default = Phenomena.Quantification.Bruening2001.ScopeAvailability.surfaceOnly

def Phenomena.Quantification.Bruening2001.wordOrderToAvailability : VerbOrder → ScopeAvailability

Convert word order to scope availability

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Quantification.Bruening2001.wordOrderToAvailability Phenomena.Quantification.Bruening2001.VerbOrder.verbRaising = Phenomena.Quantification.Bruening2001.ScopeAvailability.ambiguous

structure Phenomena.Quantification.Bruening2001.GermanScopeExample : Type

German sentence data from Bayer/Kayne.

• surface : String
• translation : String
• wordOrder : VerbOrder
• observed : ScopeAvailability

def Phenomena.Quantification.Bruening2001.instReprGermanScopeExample.repr : GermanScopeExample → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Quantification.Bruening2001.instReprGermanScopeExample : Repr GermanScopeExample

Equations

• Phenomena.Quantification.Bruening2001.instReprGermanScopeExample = { reprPrec := Phenomena.Quantification.Bruening2001.instReprGermanScopeExample.repr }

def Phenomena.Quantification.Bruening2001.german_96 : GermanScopeExample

Equations

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

def Phenomena.Quantification.Bruening2001.german_97 : GermanScopeExample

Equations

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

structure Phenomena.Quantification.Bruening2001.WestFlemishScopeExample : Type

West Flemish data from @cite{haegeman-van-riemsdijk-1986}.

• surface : String
• translation : String
• wordOrder : VerbOrder
• observed : ScopeAvailability

@[implicit_reducible]

instance Phenomena.Quantification.Bruening2001.instReprWestFlemishScopeExample : Repr WestFlemishScopeExample

Equations

• Phenomena.Quantification.Bruening2001.instReprWestFlemishScopeExample = { reprPrec := Phenomena.Quantification.Bruening2001.instReprWestFlemishScopeExample.repr }

def Phenomena.Quantification.Bruening2001.instReprWestFlemishScopeExample.repr : WestFlemishScopeExample → ℕ → Std.Format

Equations

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

def Phenomena.Quantification.Bruening2001.westFlemish_98a : WestFlemishScopeExample

Equations

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

def Phenomena.Quantification.Bruening2001.westFlemish_98b : WestFlemishScopeExample

Equations

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

structure Phenomena.Quantification.Bruening2001.DutchScopeExample : Type

Dutch equi verb data from @cite{steedman-2000}.

• surface : String
• translation : String
• wordOrder : VerbOrder
• observed : ScopeAvailability
• quantifiers : List String

def Phenomena.Quantification.Bruening2001.instReprDutchScopeExample.repr : DutchScopeExample → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Quantification.Bruening2001.instReprDutchScopeExample : Repr DutchScopeExample

Equations

• Phenomena.Quantification.Bruening2001.instReprDutchScopeExample = { reprPrec := Phenomena.Quantification.Bruening2001.instReprDutchScopeExample.repr }

def Phenomena.Quantification.Bruening2001.dutch_99a : DutchScopeExample

Equations

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

def Phenomena.Quantification.Bruening2001.dutch_99b : DutchScopeExample

Equations

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

def Phenomena.Quantification.Bruening2001.dutch_100a : DutchScopeExample

Equations

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

def Phenomena.Quantification.Bruening2001.dutch_100b : DutchScopeExample

Equations

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

def Phenomena.Quantification.Bruening2001.allDutchExamples : List DutchScopeExample

Equations

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

def Phenomena.Quantification.Bruening2001.allWestFlemishExamples : List WestFlemishScopeExample

Equations

• Phenomena.Quantification.Bruening2001.allWestFlemishExamples = [Phenomena.Quantification.Bruening2001.westFlemish_98a, Phenomena.Quantification.Bruening2001.westFlemish_98b]

def Phenomena.Quantification.Bruening2001.allGermanExamples : List GermanScopeExample

Equations

• Phenomena.Quantification.Bruening2001.allGermanExamples = [Phenomena.Quantification.Bruening2001.german_96, Phenomena.Quantification.Bruening2001.german_97]

theorem Phenomena.Quantification.Bruening2001.wordOrder_predicts_dutch_99a : wordOrderToAvailability dutch_99a.wordOrder = dutch_99a.observed

Word order correctly predicts scope availability

theorem Phenomena.Quantification.Bruening2001.wordOrder_predicts_dutch_99b : wordOrderToAvailability dutch_99b.wordOrder = dutch_99b.observed

theorem Phenomena.Quantification.Bruening2001.wordOrder_predicts_dutch_100a : wordOrderToAvailability dutch_100a.wordOrder = dutch_100a.observed

theorem Phenomena.Quantification.Bruening2001.wordOrder_predicts_dutch_100b : wordOrderToAvailability dutch_100b.wordOrder = dutch_100b.observed

theorem Phenomena.Quantification.Bruening2001.wordOrder_predicts_german_96 : wordOrderToAvailability german_96.wordOrder = german_96.observed

theorem Phenomena.Quantification.Bruening2001.wordOrder_predicts_german_97 : wordOrderToAvailability german_97.wordOrder = german_97.observed

Connects Minimalist QR / Scope Economy theory to the empirical scope-freezing data above. The central claim is Bruening's "QR obeys superiority": double-object freezing falls out of asymmetric c-command in the @cite{pylkkanen-2008} ditransitive tree.

def Phenomena.Quantification.Bruening2001.analyzeFreezingContext : FreezingContext → Option Minimalist.Scope.QRBarrier

Analyze why a freezing context blocks inverse scope in Minimalism.

Equations

• Phenomena.Quantification.Bruening2001.analyzeFreezingContext Phenomena.Quantification.Bruening2001.FreezingContext.none = none
• Phenomena.Quantification.Bruening2001.analyzeFreezingContext Phenomena.Quantification.Bruening2001.FreezingContext.possessor = some Minimalist.Scope.QRBarrier.dpPhase
• Phenomena.Quantification.Bruening2001.analyzeFreezingContext Phenomena.Quantification.Bruening2001.FreezingContext.doubleObject = some Minimalist.Scope.QRBarrier.superiority
• Phenomena.Quantification.Bruening2001.analyzeFreezingContext Phenomena.Quantification.Bruening2001.FreezingContext.passive = some Minimalist.Scope.QRBarrier.adjunctIsland
• Phenomena.Quantification.Bruening2001.analyzeFreezingContext Phenomena.Quantification.Bruening2001.FreezingContext.heavyNP = none
• Phenomena.Quantification.Bruening2001.analyzeFreezingContext Phenomena.Quantification.Bruening2001.FreezingContext.weakCrossover = none
• Phenomena.Quantification.Bruening2001.analyzeFreezingContext Phenomena.Quantification.Bruening2001.FreezingContext.adjunct = some Minimalist.Scope.QRBarrier.adjunctIsland
• Phenomena.Quantification.Bruening2001.analyzeFreezingContext Phenomena.Quantification.Bruening2001.FreezingContext.attitude = some Minimalist.Scope.QRBarrier.clauseBoundary

def Phenomena.Quantification.Bruening2001.predictsFreezing (ctx : FreezingContext) : Bool

Does Minimalism predict freezing for this context?

Equations

• Phenomena.Quantification.Bruening2001.predictsFreezing ctx = (Phenomena.Quantification.Bruening2001.analyzeFreezingContext ctx).isSome

structure Phenomena.Quantification.Bruening2001.MinimalistScopeConfig : Type

Minimalist representation of a scope configuration.

• q1 : Minimalist.Scope.PositionedQuantifier

  Higher quantifier (typically subject)

• q2 : Minimalist.Scope.PositionedQuantifier

  Lower quantifier (typically object)

• freezingContext : FreezingContext

  Freezing context if any

• tree : Option Minimalist.SyntacticObject

  The tree in which q1 and q2 are positioned. When provided, superiority is derived from c-command rather than stipulated.

def Phenomena.Quantification.Bruening2001.instReprMinimalistScopeConfig.repr : MinimalistScopeConfig → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Quantification.Bruening2001.instReprMinimalistScopeConfig : Repr MinimalistScopeConfig

Equations

• Phenomena.Quantification.Bruening2001.instReprMinimalistScopeConfig = { reprPrec := Phenomena.Quantification.Bruening2001.instReprMinimalistScopeConfig.repr }

def Phenomena.Quantification.Bruening2001.superiorityBlocked (config : MinimalistScopeConfig) : Bool

Check if superiority blocks QR in this configuration.

When a tree and SO positions are provided, superiority is DERIVED from asymmetric c-command. Otherwise falls back to the freezing context annotation.

Equations

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

def Phenomena.Quantification.Bruening2001.availableReadings (config : MinimalistScopeConfig) : Availability

Compute available scope readings in Minimalism.

Equations

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

def Phenomena.Quantification.Bruening2001.configFromExample (ex : Example) : MinimalistScopeConfig

Build config from a freezing example (fallback path — no tree).

Equations

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

def Phenomena.Quantification.Bruening2001.predictAvailability (ex : Example) : Availability

Minimalism's prediction for an example.

Equations

• Phenomena.Quantification.Bruening2001.predictAvailability ex = Phenomena.Quantification.Bruening2001.availableReadings (Phenomena.Quantification.Bruening2001.configFromExample ex)

def Phenomena.Quantification.Bruening2001.correctlyPredicts (ex : Example) : Bool

Check if Minimalism correctly predicts the example.

Equations

• Phenomena.Quantification.Bruening2001.correctlyPredicts ex = (Phenomena.Quantification.Bruening2001.predictAvailability ex == ex.observed)

theorem Phenomena.Quantification.Bruening2001.possessor_freezes_scope : predictsFreezing FreezingContext.possessor = true

Possessor freezing follows from DP being a phase.

theorem Phenomena.Quantification.Bruening2001.double_object_freezes_scope : predictsFreezing FreezingContext.doubleObject = true

Double object freezing follows from superiority.

theorem Phenomena.Quantification.Bruening2001.passive_freezes_scope : predictsFreezing FreezingContext.passive = true

Passive freezing follows from adjunct island.

theorem Phenomena.Quantification.Bruening2001.heavy_np_not_grammatically_frozen : predictsFreezing FreezingContext.heavyNP = false

Heavy NP is NOT predicted to freeze (it's processing).

theorem Phenomena.Quantification.Bruening2001.baseline_is_ambiguous : predictsFreezing FreezingContext.none = false

Baseline (no context) is predicted ambiguous.

@cite{pylkkanen-2008}'s low-Appl tree (ditransitiveTree) produces the DOC structure where V takes ApplP as complement, so the goal in Spec-ApplP asymmetrically c-commands the theme in complement of Appl. QR of the theme over the goal is blocked by superiority, derived from c-command rather than stipulated.

def Phenomena.Quantification.Bruening2001.docScopeConfig : MinimalistScopeConfig

DOC scope freezing config with @cite{pylkkanen-2008}'s tree: superiority is derived from goal asymmetrically c-commanding theme in the Voice + low-Appl structure.

Equations

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

theorem Phenomena.Quantification.Bruening2001.doc_superiority_from_tree : superiorityBlocked docScopeConfig = true

Superiority in the DOC is DERIVED from c-command in @cite{pylkkanen-2008}'s tree: goal (Mary) asymmetrically c-commands theme (a letter) via low Appl, so QR of theme over goal is blocked.

Summary

Context	Minimalist Explanation
Possessor	DP phase blocks QR
Double object	Superiority: goal c-commands theme (@cite{pylkkanen-2008} tree)
Passive	Adjunct island
Heavy NP	NOT grammatical (processing)
Attitude	Clause boundary