Minimalist Analysis of Subject-Auxiliary Inversion

Inversion-specific constraints and licensing, plus the underlying clause structure (positions, dominance, structural precedence).

The Analysis

Matrix questions have [+Q] on C, which triggers T-to-C movement. Embedded questions have [+Q] satisfied by the embedding verb or wh-movement, so T-to-C doesn't occur.

This derives the word order asymmetry:

• Matrix: T-to-C → T precedes subject
• Embedded: no T-to-C → subject precedes T

inductive Minimalist.Position : Type

Positions in the clause structure

• specCP : Position
• headC : Position
• specTP : Position
• headT : Position
• specvP : Position
• headv : Position
• headV : Position

@[implicit_reducible]

instance Minimalist.instReprPosition : Repr Position

Equations

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

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

Equations

• Minimalist.instReprPosition.repr Minimalist.Position.specCP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Position.specCP")).group prec✝
• Minimalist.instReprPosition.repr Minimalist.Position.headC prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Position.headC")).group prec✝
• Minimalist.instReprPosition.repr Minimalist.Position.specTP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Position.specTP")).group prec✝
• Minimalist.instReprPosition.repr Minimalist.Position.headT prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Position.headT")).group prec✝
• Minimalist.instReprPosition.repr Minimalist.Position.specvP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Position.specvP")).group prec✝
• Minimalist.instReprPosition.repr Minimalist.Position.headv prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Position.headv")).group prec✝
• Minimalist.instReprPosition.repr Minimalist.Position.headV prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Position.headV")).group prec✝

@[implicit_reducible]

instance Minimalist.instDecidableEqPosition : DecidableEq Position

Equations

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

def Minimalist.dominates : Position → Position → Bool

Equations

• Minimalist.dominates Minimalist.Position.specCP x✝ = (x✝ != Minimalist.Position.specCP)
• Minimalist.dominates Minimalist.Position.headC x✝ = (x✝ != Minimalist.Position.specCP && x✝ != Minimalist.Position.headC)
• Minimalist.dominates Minimalist.Position.specTP x✝ = (x✝ == Minimalist.Position.specvP || x✝ == Minimalist.Position.headv || x✝ == Minimalist.Position.headV)
• Minimalist.dominates Minimalist.Position.headT x✝ = (x✝ == Minimalist.Position.specvP || x✝ == Minimalist.Position.headv || x✝ == Minimalist.Position.headV)
• Minimalist.dominates Minimalist.Position.specvP x✝ = (x✝ == Minimalist.Position.headv || x✝ == Minimalist.Position.headV)
• Minimalist.dominates Minimalist.Position.headv Minimalist.Position.headV = true
• Minimalist.dominates x✝¹ x✝ = false

def Minimalist.structurallyPrecedes : Position → Position → Bool

Structural precedence in English (Spec-Head-Complement order)

Equations

• Minimalist.structurallyPrecedes Minimalist.Position.specCP Minimalist.Position.headC = true
• Minimalist.structurallyPrecedes Minimalist.Position.specCP Minimalist.Position.specTP = true
• Minimalist.structurallyPrecedes Minimalist.Position.specCP Minimalist.Position.headT = true
• Minimalist.structurallyPrecedes Minimalist.Position.specCP Minimalist.Position.specvP = true
• Minimalist.structurallyPrecedes Minimalist.Position.specCP Minimalist.Position.headv = true
• Minimalist.structurallyPrecedes Minimalist.Position.specCP Minimalist.Position.headV = true
• Minimalist.structurallyPrecedes Minimalist.Position.headC Minimalist.Position.specTP = true
• Minimalist.structurallyPrecedes Minimalist.Position.headC Minimalist.Position.headT = true
• Minimalist.structurallyPrecedes Minimalist.Position.headC Minimalist.Position.specvP = true
• Minimalist.structurallyPrecedes Minimalist.Position.headC Minimalist.Position.headv = true
• Minimalist.structurallyPrecedes Minimalist.Position.headC Minimalist.Position.headV = true
• Minimalist.structurallyPrecedes Minimalist.Position.specTP Minimalist.Position.headT = true
• Minimalist.structurallyPrecedes Minimalist.Position.specTP Minimalist.Position.specvP = true
• Minimalist.structurallyPrecedes Minimalist.Position.specTP Minimalist.Position.headv = true
• Minimalist.structurallyPrecedes Minimalist.Position.specTP Minimalist.Position.headV = true
• Minimalist.structurallyPrecedes Minimalist.Position.headT Minimalist.Position.specvP = true
• Minimalist.structurallyPrecedes Minimalist.Position.headT Minimalist.Position.headv = true
• Minimalist.structurallyPrecedes Minimalist.Position.headT Minimalist.Position.headV = true
• Minimalist.structurallyPrecedes Minimalist.Position.specvP Minimalist.Position.headv = true
• Minimalist.structurallyPrecedes Minimalist.Position.specvP Minimalist.Position.headV = true
• Minimalist.structurallyPrecedes Minimalist.Position.headv Minimalist.Position.headV = true
• Minimalist.structurallyPrecedes x✝¹ x✝ = false

theorem Minimalist.subject_precedes_t_base : structurallyPrecedes Position.specTP Position.headT = true

theorem Minimalist.c_precedes_subject : structurallyPrecedes Position.headC Position.specTP = true

theorem Minimalist.c_precedes_t : structurallyPrecedes Position.headC Position.headT = true

theorem Minimalist.spec_cp_is_first : structurallyPrecedes Position.specCP Position.headC = true ∧ structurallyPrecedes Position.specCP Position.specTP = true ∧ structurallyPrecedes Position.specCP Position.headT = true

inductive Minimalist.HeadPosition : Type

• base : Position → HeadPosition
• movedTo : Position → HeadPosition

def Minimalist.instReprHeadPosition.repr : HeadPosition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprHeadPosition : Repr HeadPosition

Equations

• Minimalist.instReprHeadPosition = { reprPrec := Minimalist.instReprHeadPosition.repr }

@[implicit_reducible]

instance Minimalist.instDecidableEqHeadPosition : DecidableEq HeadPosition

Equations

• Minimalist.instDecidableEqHeadPosition = Minimalist.instDecidableEqHeadPosition.decEq

def Minimalist.instDecidableEqHeadPosition.decEq (x✝ x✝¹ : HeadPosition) : Decidable (x✝ = x✝¹)

Equations

• Minimalist.instDecidableEqHeadPosition.decEq (Minimalist.HeadPosition.base a) (Minimalist.HeadPosition.base b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Minimalist.instDecidableEqHeadPosition.decEq (Minimalist.HeadPosition.base a) (Minimalist.HeadPosition.movedTo a_1) = isFalse ⋯
• Minimalist.instDecidableEqHeadPosition.decEq (Minimalist.HeadPosition.movedTo a) (Minimalist.HeadPosition.base a_1) = isFalse ⋯
• Minimalist.instDecidableEqHeadPosition.decEq (Minimalist.HeadPosition.movedTo a) (Minimalist.HeadPosition.movedTo b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

inductive Minimalist.TPosition : Type

• inT : TPosition
• inC : TPosition

@[implicit_reducible]

instance Minimalist.instReprTPosition : Repr TPosition

Equations

• Minimalist.instReprTPosition = { reprPrec := Minimalist.instReprTPosition.repr }

def Minimalist.instReprTPosition.repr : TPosition → ℕ → Std.Format

Equations

• Minimalist.instReprTPosition.repr Minimalist.TPosition.inT prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.TPosition.inT")).group prec✝
• Minimalist.instReprTPosition.repr Minimalist.TPosition.inC prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.TPosition.inC")).group prec✝

@[implicit_reducible]

instance Minimalist.instDecidableEqTPosition : DecidableEq TPosition

Equations

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

def Minimalist.tPronouncedAt (tPos : TPosition) : Position

Equations

• Minimalist.tPronouncedAt Minimalist.TPosition.inT = Minimalist.Position.headT
• Minimalist.tPronouncedAt Minimalist.TPosition.inC = Minimalist.Position.headC

theorem Minimalist.t_to_c_precedes_subject : structurallyPrecedes (tPronouncedAt TPosition.inC) Position.specTP = true

theorem Minimalist.subject_precedes_t_no_movement : structurallyPrecedes Position.specTP (tPronouncedAt TPosition.inT) = true

theorem Minimalist.t_to_c_reverses_order : structurallyPrecedes Position.specTP Position.headT = true ∧ structurallyPrecedes Position.headC Position.specTP = true

def Minimalist.tPrecedesSubject (tPos : TPosition) : Bool

Equations

• Minimalist.tPrecedesSubject tPos = Minimalist.structurallyPrecedes (Minimalist.tPronouncedAt tPos) Minimalist.Position.specTP

def Minimalist.subjectPrecedesT (tPos : TPosition) : Bool

Equations

• Minimalist.subjectPrecedesT tPos = Minimalist.structurallyPrecedes Minimalist.Position.specTP (Minimalist.tPronouncedAt tPos)

theorem Minimalist.t_to_c_gives_t_first : tPrecedesSubject TPosition.inC = true

theorem Minimalist.no_movement_gives_subj_first : subjectPrecedesT TPosition.inT = true

def Minimalist.matrixTriggersTToC (ct : Features.ClauseForm) (tPos : TPosition) : Prop

Matrix questions trigger T-to-C movement (to check [+Q] on C)

Equations

• Minimalist.matrixTriggersTToC ct tPos = (ct = Features.ClauseForm.matrixQuestion → tPos = Minimalist.TPosition.inC)

def Minimalist.embeddedNoTToC (ct : Features.ClauseForm) (tPos : TPosition) : Prop

Embedded questions don't trigger T-to-C (C's [+Q] is checked otherwise)

Equations

• Minimalist.embeddedNoTToC ct tPos = (ct = Features.ClauseForm.embeddedQuestion → tPos = Minimalist.TPosition.inT)

theorem Minimalist.matrix_has_t_before_subject (tPos : TPosition) (h : matrixTriggersTToC Features.ClauseForm.matrixQuestion tPos) : tPrecedesSubject tPos = true

Matrix questions have T before subject (via T-to-C)

theorem Minimalist.embedded_has_subject_before_t (tPos : TPosition) (h : embeddedNoTToC Features.ClauseForm.embeddedQuestion tPos) : subjectPrecedesT tPos = true

Embedded questions have subject before T (no T-to-C)

structure Minimalist.Clause : Type

A clause: words + structural info

• words : List Word
• tPosition : TPosition
• clauseType : Features.ClauseForm

def Minimalist.wordOrderMatchesStructure (c : Clause) : Prop

Word order must match the structural prediction

Equations

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

def Minimalist.wellFormed (c : Clause) : Prop

Well-formed clause

Equations

• Minimalist.wellFormed c = (Minimalist.wordOrderMatchesStructure c ∧ Minimalist.matrixTriggersTToC c.clauseType c.tPosition ∧ Minimalist.embeddedNoTToC c.clauseType c.tPosition)

def Minimalist.licenses (ws : List Word) (ct : Features.ClauseForm) : Prop

A word sequence is licensed for a clause type if some T-position works

Equations

• Minimalist.licenses ws ct = ∃ (tPos : Minimalist.TPosition), Minimalist.wellFormed { words := ws, tPosition := tPos, clauseType := ct }

theorem Minimalist.licenses_matrix_t_first (ws : List Word) (h : Inversion.auxPrecedesSubject ws = true) : licenses ws Features.ClauseForm.matrixQuestion

Matrix questions with T-first word order are licensed

theorem Minimalist.not_licenses_matrix_subject_first (ws : List Word) (h : Inversion.auxPrecedesSubject ws = false) : ¬licenses ws Features.ClauseForm.matrixQuestion

Matrix questions with subject-first are NOT licensed

theorem Minimalist.licenses_embedded_subject_first (ws : List Word) (h : Inversion.subjectPrecedesAux ws = true) : licenses ws Features.ClauseForm.embeddedQuestion

Embedded questions with subject-first are licensed

theorem Minimalist.not_licenses_embedded_t_first (ws : List Word) (h : Inversion.subjectPrecedesAux ws = false) : ¬licenses ws Features.ClauseForm.embeddedQuestion

Embedded questions with T-first are NOT licensed