inductive Minimalism.Phenomena.Scope.Position : Type

Structural positions relevant for scope

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

instance Minimalism.Phenomena.Scope.instDecidableEqPosition : DecidableEq Position

Equations

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

def Minimalism.Phenomena.Scope.instBEqPosition.beq : Position → Position → Bool

Equations

• Minimalism.Phenomena.Scope.instBEqPosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Minimalism.Phenomena.Scope.instBEqPosition : BEq Position

Equations

• Minimalism.Phenomena.Scope.instBEqPosition = { beq := Minimalism.Phenomena.Scope.instBEqPosition.beq }

def Minimalism.Phenomena.Scope.instReprPosition.repr : Position → ℕ → Std.Format

Equations

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

instance Minimalism.Phenomena.Scope.instReprPosition : Repr Position

Equations

• Minimalism.Phenomena.Scope.instReprPosition = { reprPrec := Minimalism.Phenomena.Scope.instReprPosition.repr }

def Minimalism.Phenomena.Scope.instInhabitedPosition.default : Position

Equations

• Minimalism.Phenomena.Scope.instInhabitedPosition.default = Minimalism.Phenomena.Scope.Position.specTP

instance Minimalism.Phenomena.Scope.instInhabitedPosition : Inhabited Position

Equations

• Minimalism.Phenomena.Scope.instInhabitedPosition = { default := Minimalism.Phenomena.Scope.instInhabitedPosition.default }

structure Minimalism.Phenomena.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.

instance Minimalism.Phenomena.Scope.instReprPositionedQuantifier : Repr PositionedQuantifier

Equations

• Minimalism.Phenomena.Scope.instReprPositionedQuantifier = { reprPrec := Minimalism.Phenomena.Scope.instReprPositionedQuantifier.repr }

def Minimalism.Phenomena.Scope.instReprPositionedQuantifier.repr : PositionedQuantifier → ℕ → Std.Format

Equations

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

structure Minimalism.Phenomena.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?

def Minimalism.Phenomena.Scope.instReprQROperation.repr : QROperation → ℕ → Std.Format

Equations

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

instance Minimalism.Phenomena.Scope.instReprQROperation : Repr QROperation

Equations

• Minimalism.Phenomena.Scope.instReprQROperation = { reprPrec := Minimalism.Phenomena.Scope.instReprQROperation.repr }

inductive Minimalism.Phenomena.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

instance Minimalism.Phenomena.Scope.instDecidableEqQRBarrier : DecidableEq QRBarrier

Equations

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

instance Minimalism.Phenomena.Scope.instBEqQRBarrier : BEq QRBarrier

Equations

• Minimalism.Phenomena.Scope.instBEqQRBarrier = { beq := Minimalism.Phenomena.Scope.instBEqQRBarrier.beq }

def Minimalism.Phenomena.Scope.instBEqQRBarrier.beq : QRBarrier → QRBarrier → Bool

Equations

• Minimalism.Phenomena.Scope.instBEqQRBarrier.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Minimalism.Phenomena.Scope.instReprQRBarrier : Repr QRBarrier

Equations

• Minimalism.Phenomena.Scope.instReprQRBarrier = { reprPrec := Minimalism.Phenomena.Scope.instReprQRBarrier.repr }

def Minimalism.Phenomena.Scope.instReprQRBarrier.repr : QRBarrier → ℕ → Std.Format

Equations

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

def Minimalism.Phenomena.Scope.instInhabitedQRBarrier.default : QRBarrier

Equations

• Minimalism.Phenomena.Scope.instInhabitedQRBarrier.default = Minimalism.Phenomena.Scope.QRBarrier.dpPhase

instance Minimalism.Phenomena.Scope.instInhabitedQRBarrier : Inhabited QRBarrier

Equations

• Minimalism.Phenomena.Scope.instInhabitedQRBarrier = { default := Minimalism.Phenomena.Scope.instInhabitedQRBarrier.default }

def Minimalism.Phenomena.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 Minimalism.Phenomena.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{pylkknen-2008}'s Voice + low-Appl tree derivation.

Equations

• Minimalism.Phenomena.Scope.superiorityFromTree tree q1 q2 = (Minimalism.cCommandsInB tree q1 q2 && !Minimalism.cCommandsInB tree q2 q1)

structure Minimalism.Phenomena.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 Minimalism.Phenomena.Scope.instReprScopeEconomy.repr : ScopeEconomy → ℕ → Std.Format

Equations

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

instance Minimalism.Phenomena.Scope.instReprScopeEconomy : Repr ScopeEconomy

Equations

• Minimalism.Phenomena.Scope.instReprScopeEconomy = { reprPrec := Minimalism.Phenomena.Scope.instReprScopeEconomy.repr }

def Minimalism.Phenomena.Scope.economyBlocksQR (e : ScopeEconomy) : Bool

QR is blocked by economy if interpretations are equivalent

Equations

• Minimalism.Phenomena.Scope.economyBlocksQR e = e.equivalent

theorem Minimalism.Phenomena.Scope.dp_phase_barrier_from_pic (tok : LIToken) (b : SyntacticObject) (h : labelCat ((SyntacticObject.leaf tok).node b) = some Cat.D) (h_phase : isDPhaseHead ((SyntacticObject.leaf tok).node b) = true) (strength : PICStrength) (goal : SyntacticObject) : contains b goal → phaseImpenetrable strength ((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.