def Minimalism.matrixTriggersTToC (ct : ClauseType) (tPos : TPosition) : Prop

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

Equations

• Minimalism.matrixTriggersTToC ct tPos = (ct = ClauseType.matrixQuestion → tPos = Minimalism.TPosition.inC)

def Minimalism.embeddedNoTToC (ct : ClauseType) (tPos : TPosition) : Prop

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

Equations

• Minimalism.embeddedNoTToC ct tPos = (ct = ClauseType.embeddedQuestion → tPos = Minimalism.TPosition.inT)

theorem Minimalism.matrix_has_t_before_subject (tPos : TPosition) (h : matrixTriggersTToC ClauseType.matrixQuestion tPos) : tPrecedesSubject tPos = true

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

theorem Minimalism.embedded_has_subject_before_t (tPos : TPosition) (h : embeddedNoTToC ClauseType.embeddedQuestion tPos) : subjectPrecedesT tPos = true

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

structure Minimalism.Clause : Type

A clause: words + structural info

• words : List Word
• tPosition : TPosition
• clauseType : ClauseType

def Minimalism.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 Minimalism.wellFormed (c : Clause) : Prop

Well-formed clause

Equations

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

def Minimalism.licenses (ws : List Word) (ct : ClauseType) : Prop

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

Equations

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

theorem Minimalism.licenses_matrix_t_first (ws : List Word) (h : auxPrecedesSubject ws = true) : licenses ws ClauseType.matrixQuestion

Matrix questions with T-first word order are licensed

theorem Minimalism.not_licenses_matrix_subject_first (ws : List Word) (h : auxPrecedesSubject ws = false) : ¬licenses ws ClauseType.matrixQuestion

Matrix questions with subject-first are NOT licensed

theorem Minimalism.licenses_embedded_subject_first (ws : List Word) (h : subjectPrecedesAux ws = true) : licenses ws ClauseType.embeddedQuestion

Embedded questions with subject-first are licensed

theorem Minimalism.not_licenses_embedded_t_first (ws : List Word) (h : subjectPrecedesAux ws = false) : ¬licenses ws ClauseType.embeddedQuestion

Embedded questions with T-first are NOT licensed