Complement sizes

A clausal complement is measured by its highest projected head. Wurmbrand classifies infinitival complements by the structure they project, a bare vP for restructuring, a TP for propositional attitudes and a modal projection for future infinitives, beside the full CP of a finite clause, and a complement is at most as large as another when its highest head is no higher in the functional sequence. Two sizes with distinct heads at one level, tense and negation for instance, are then equivalent but not equal, so the order is a preorder. The size of a clause spine is its highest head. On extended projections the extension order of spines, inclusion of labels, refines the size order, and the standard sizes are those of the standard spines.

Main definitions

• Minimalist.ComplementSize: a clausal complement measured by its highest head.
• Minimalist.ComplementSize.fLevel: the functional level of the highest head.
• Minimalist.ClauseSpine.size: the size of a spine, its highest head.
• Minimalist.ComplementSize.vP, Minimalist.ComplementSize.tP, Minimalist.ComplementSize.modP, Minimalist.ComplementSize.finP, Minimalist.ComplementSize.cP: the standard sizes.

Main results

• Minimalist.ComplementSize.le_def, Minimalist.ComplementSize.lt_def: the order is that of functional levels.
• Minimalist.ClauseSpine.size_le_size: on extended projections, the extension order refines the size order, so that the standard sizes ascend as their spines do (Minimalist.ComplementSize.vP_le_tP, Minimalist.ComplementSize.tP_le_cP).

References

• [Wur14]
• [Gri05b]

structure Minimalist.ComplementSize : Type

A clausal complement measured by the highest head it projects.

• highestHead : Cat

  The highest functional head in the complement.

@[instance_reducible]

instance Minimalist.instDecidableEqComplementSize : DecidableEq ComplementSize

Equations

• Minimalist.instDecidableEqComplementSize = Minimalist.instDecidableEqComplementSize.decEq

def Minimalist.instDecidableEqComplementSize.decEq (x✝ x✝¹ : ComplementSize) : Decidable (x✝ = x✝¹)

Equations

• Minimalist.instDecidableEqComplementSize.decEq { highestHead := a } { highestHead := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Minimalist.instReprComplementSize : Repr ComplementSize

Equations

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

def Minimalist.instReprComplementSize.repr : ComplementSize → ℕ → Std.Format

Equations

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

def Minimalist.ComplementSize.fLevel (cs : ComplementSize) : ℕ

The functional level of a complement is that of its highest head.

Equations

• cs.fLevel = cs.highestHead.fValue

@[instance_reducible]

instance Minimalist.ComplementSize.instPreorder : Preorder ComplementSize

Complement sizes are ordered by functional level, so that a complement is at most another when it projects no higher in the functional sequence.

Equations

• Minimalist.ComplementSize.instPreorder = Preorder.lift Minimalist.ComplementSize.fLevel

@[instance_reducible]

instance Minimalist.ComplementSize.instDecidableLE : DecidableLE ComplementSize

Equations

• a.instDecidableLE b = { decide := a.fLevel.ble b.fLevel, reflects_decide := ⋯ }

@[instance_reducible]

instance Minimalist.ComplementSize.instDecidableLT : DecidableLT ComplementSize

Equations

• a.instDecidableLT b = { decide := a.fLevel.succ.ble b.fLevel, reflects_decide := ⋯ }

theorem Minimalist.ComplementSize.le_def {a b : ComplementSize} : a ≤ b ↔ a.fLevel ≤ b.fLevel

theorem Minimalist.ComplementSize.lt_def {a b : ComplementSize} : a < b ↔ a.fLevel < b.fLevel

The size of a spine

def Minimalist.ClauseSpine.size (s : ClauseSpine) : ComplementSize

The size of a spine is its highest head; the empty spine has the size of a bare lexical head, the least size.

Equations

• s.size = { highestHead := s.heads.getLastD Minimalist.Cat.V }

theorem Minimalist.ClauseSpine.IsExtendedProjection.fValue_le_fLevel {s : ClauseSpine} {c : Cat} (hs : s.IsExtendedProjection) (hc : c ∈ s) : c.fValue ≤ s.size.fLevel

No head of an extended projection is higher than its highest head.

theorem Minimalist.ClauseSpine.size_le_size {s t : ClauseSpine} (h : s ≤ t) (ht : t.IsExtendedProjection) : s.size ≤ t.size

On extended projections, the extension order refines the size order: a spine whose heads another projects is no larger.

The standard sizes

def Minimalist.ComplementSize.vP : ComplementSize

The vP-sized complement of a restructuring infinitive, the size of the vP spine.

Equations

• Minimalist.ComplementSize.vP = Minimalist.ClauseSpine.vP.size

def Minimalist.ComplementSize.tP : ComplementSize

The TP-sized complement of a propositional infinitive, the size of the TP spine.

Equations

• Minimalist.ComplementSize.tP = Minimalist.ClauseSpine.tP.size

def Minimalist.ComplementSize.modP : ComplementSize

The modal complement of a future infinitive.

Equations

• Minimalist.ComplementSize.modP = { highestHead := Minimalist.Cat.Mod }

def Minimalist.ComplementSize.finP : ComplementSize

The FinP-sized complement, the lowest layer of the left periphery.

Equations

• Minimalist.ComplementSize.finP = { highestHead := Minimalist.Cat.Fin }

def Minimalist.ComplementSize.cP : ComplementSize

The CP-sized complement of a finite clause, the size of the CP spine.

Equations

• Minimalist.ComplementSize.cP = Minimalist.ClauseSpine.cP.size

theorem Minimalist.ComplementSize.vP_le_tP : vP ≤ tP

The standard sizes ascend as their spines do.

theorem Minimalist.ComplementSize.tP_le_cP : tP ≤ cP