Minimalist Scope Theory: QR and Scope Economy

@cite{bruening-2001} @cite{may-1985}

Formalization of quantifier scope in the Minimalist tradition.

Core Mechanisms

1. Quantifier Raising (QR): Covert A'-movement of quantifiers to adjoin to TP/CP
2. Scope Economy: QR only applies if it yields a distinct interpretation
3. Locality: QR is clause-bounded and blocked by certain structural barriers

Scope Freezing in Minimalism

Inverse scope is unavailable when:

• Possessor: Quantifier inside possessor DP cannot escape (DP is a phase/barrier)
• Double Object: Indirect object c-commands direct object; QR would violate locality
• Passive: By-phrase is an adjunct; QR from adjuncts is blocked

Superiority from C-Command (not stipulation)

In earlier versions, PositionedQuantifier carried a stipulated inDoubleObject : Bool flag. This has been replaced: the theory layer provides superiorityFromTree, which derives superiority from asymmetric c-command in a SyntacticObject tree. Bridge files in Phenomena/ use this to connect DOC scope freezing to @cite{larson-1988}'s tree derivation.

inductive Minimalist.Scope.Position : Type

Structural positions relevant for scope

• specTP : Position
• specVP : Position
• adjunct : Position
• embedded : Position
• complement : Position

@[implicit_reducible]

instance Minimalist.Scope.instDecidableEqPosition : DecidableEq Position

Equations

• Minimalist.Scope.instDecidableEqPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalist.Scope.instReprPosition.repr : Position → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.Scope.instReprPosition : Repr Position

Equations

• Minimalist.Scope.instReprPosition = { reprPrec := Minimalist.Scope.instReprPosition.repr }

@[implicit_reducible]

instance Minimalist.Scope.instInhabitedPosition : Inhabited Position

Equations

• Minimalist.Scope.instInhabitedPosition = { default := Minimalist.Scope.instInhabitedPosition.default }

def Minimalist.Scope.instInhabitedPosition.default : Position

Equations

• Minimalist.Scope.instInhabitedPosition.default = Minimalist.Scope.Position.specTP

structure Minimalist.Scope.PositionedQuantifier : Type

A quantifier with its structural position

• quantifier : String
• position : Position
• insideDP : Bool

  Is this inside another DP?

• so : Option SyntacticObject

  The SyntacticObject this quantifier corresponds to in the tree. When provided, superiority can be derived from c-command.

@[implicit_reducible]

instance Minimalist.Scope.instReprPositionedQuantifier : Repr PositionedQuantifier

Equations

• Minimalist.Scope.instReprPositionedQuantifier = { reprPrec := Minimalist.Scope.instReprPositionedQuantifier.repr }

def Minimalist.Scope.instReprPositionedQuantifier.repr : PositionedQuantifier → ℕ → Std.Format

Equations

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

structure Minimalist.Scope.QROperation : Type

Quantifier Raising (QR) as covert movement.

QR adjoins a quantifier to a clausal node (TP or CP), allowing it to take scope over material it c-commands at LF.

• target : PositionedQuantifier

  The quantifier being raised

• landingSite : Position

  Landing site

• createsNewScope : Bool

  Does this create a new scope relation?

@[implicit_reducible]

instance Minimalist.Scope.instReprQROperation : Repr QROperation

Equations

• Minimalist.Scope.instReprQROperation = { reprPrec := Minimalist.Scope.instReprQROperation.repr }

def Minimalist.Scope.instReprQROperation.repr : QROperation → ℕ → Std.Format

Equations

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

inductive Minimalist.Scope.QRBarrier : Type

Barriers to QR movement.

Following phase theory and earlier barrier theory, certain nodes block extraction/QR.

• dpPhase : QRBarrier
• clauseBoundary : QRBarrier
• adjunctIsland : QRBarrier
• superiority : QRBarrier

@[implicit_reducible]

instance Minimalist.Scope.instDecidableEqQRBarrier : DecidableEq QRBarrier

Equations

• Minimalist.Scope.instDecidableEqQRBarrier x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Minimalist.Scope.instReprQRBarrier : Repr QRBarrier

Equations

• Minimalist.Scope.instReprQRBarrier = { reprPrec := Minimalist.Scope.instReprQRBarrier.repr }

def Minimalist.Scope.instReprQRBarrier.repr : QRBarrier → ℕ → Std.Format

Equations

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

def Minimalist.Scope.instInhabitedQRBarrier.default : QRBarrier

Equations

• Minimalist.Scope.instInhabitedQRBarrier.default = Minimalist.Scope.QRBarrier.dpPhase

@[implicit_reducible]

instance Minimalist.Scope.instInhabitedQRBarrier : Inhabited QRBarrier

Equations

• Minimalist.Scope.instInhabitedQRBarrier = { default := Minimalist.Scope.instInhabitedQRBarrier.default }

def Minimalist.Scope.qrIsBlocked (q : PositionedQuantifier) : Option QRBarrier

Check if QR is blocked for a given quantifier

Equations

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

def Minimalist.Scope.superiorityFromTree (tree q1 q2 : SyntacticObject) : Bool

Superiority derived from a tree: QR of q2 over q1 is blocked when q1 asymmetrically c-commands q2 in tree.

This is the theory-layer primitive. Bridge files use it to derive DOC scope freezing from @cite{pylkkanen-2008}'s Voice + low-Appl tree derivation.

Equations

• Minimalist.Scope.superiorityFromTree tree q1 q2 = decide (Minimalist.asymCCommandsIn tree q1 q2)

structure Minimalist.Scope.ScopeEconomy : Type

Scope Economy: QR is only licensed if it creates a truth-conditional difference.

"Covert scope-shifting operations are blocked if they don't have a semantic effect (i.e., if they yield a logically equivalent interpretation)."

• surfaceInterpretation : String

  Surface scope interpretation

• inverseInterpretation : String

  Would-be inverse interpretation

• equivalent : Bool

  Are they truth-conditionally equivalent?

def Minimalist.Scope.instReprScopeEconomy.repr : ScopeEconomy → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.Scope.instReprScopeEconomy : Repr ScopeEconomy

Equations

• Minimalist.Scope.instReprScopeEconomy = { reprPrec := Minimalist.Scope.instReprScopeEconomy.repr }

def Minimalist.Scope.economyBlocksQR (e : ScopeEconomy) : Bool

QR is blocked by economy if interpretations are equivalent

Equations

• Minimalist.Scope.economyBlocksQR e = e.equivalent

theorem Minimalist.Scope.dp_phase_barrier_from_pic (tok : LIToken) (b : SyntacticObject) (_h_phase : isPhaseHeadOf Cat.D ((SyntacticObject.leaf tok).node b) = true) (goal : SyntacticObject) : contains b goal → phaseImpenetrable ((SyntacticObject.leaf tok).node b) goal

DP-as-barrier follows from PIC: D is a phase head (under the extended phase inventory), so material inside DP's complement is frozen for QR.

This derives the previously-stipulated QRBarrier.dpPhase from deeper principles: if D is a phase head, then PIC makes DP-internal material inaccessible to operations outside DP.

The SO is decomposed as node (leaf tok) b — the head is a leaf (the D lexical item) and b is the complement. PIC freezes the complement domain, not the head/edge.

Phase 1.0 status. The proof previously used exact hcontains because under the planar TraceTree carrier phaseComplement? reduced definitionally on .node (leaf _) b to some b. With the nonplanar FreeCommMagma carrier, phaseComplement? picks the right daughter of the Quot.out representative — which may be either child after the swap quotient. The theorem statement presupposes a planar choice that the substrate cannot make.

Phase 2 plan. Replace phaseComplement? with a head-function- parameterized variant that picks the complement (the non-head daughter) rather than "the right daughter of an arbitrary representative." Once that lands, dp_phase_barrier_from_pic can be re-proved by a head-function argument: if tok is the head, the complement is b, so PIC freezes b's contents.