Landau (2013): Control in Generative Grammar

[Lan13]'s OC signature ((74), §1.3): in a control construction, (a) the controller(s) must be co-dependent(s) of the clause, and (b) the controlled element (or part of it) must be interpreted as a bound variable. The familiar OC criteria are derived ((75)–(79)): co-dependence excludes arbitrary, long-distance, and non-c-commanding control and forces sloppy ellipsis readings; variable binding excludes strict readings under only. The Control.Excludes instance records that derivation, and the general Control.Profile machinery returns the book's characterizations: the OC signature admits no criterial configuration, its NOC mirror (§7.1) admits all.

Deliberately absent, per §1.3: obligatory de se is NOT criterial for OC — it is an attitude-tier property. Per §1.4, the lexical-subject diagnostic is rejected as an "obligatory nullness criterion" rather than an OC criterion — the separation the overt-PRO studies (Studies/Ostrove2026.lean, Studies/Allotey2021.lean) turn on. The full NOC signature (453) also adds a third, positive clause — PRO is [+human] — which the book (tentatively) defends as irreducible (§7.5; retracted by name in [Lan24]); the two-clause mirror covers only the criteria that (74)'s clauses derive.

inductive Landau2013.Clause74 : Type

The two clauses of [Lan13]'s OC signature ((74)): the co-dependence clause admits implicit, split, and (via "part of it") partial control.

• codependent : Clause74

  (74a): the controller(s) must be co-dependent(s) of the clause.

• boundVariable : Clause74

  (74b): the controlled element is interpreted as a bound variable.

@[instance_reducible]

instance Landau2013.instDecidableEqClause74 : DecidableEq Clause74

Equations

• Landau2013.instDecidableEqClause74 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Landau2013.instReprClause74.repr : Clause74 → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Landau2013.instReprClause74 : Repr Clause74

Equations

• Landau2013.instReprClause74 = { reprPrec := Landau2013.instReprClause74.repr }

@[instance_reducible]

instance Landau2013.instFintypeClause74 : Fintype Clause74

Equations

• Landau2013.instFintypeClause74 = { elems := { val := ↑Landau2013.Clause74.enumList, nodup := Landau2013.Clause74.enumList_nodup }, complete := Landau2013.instFintypeClause74._proof_1 }

@[instance_reducible]

instance Landau2013.instExcludesClause74 : Control.Excludes Clause74

The derivation of the criteria from the signature ((75)–(79)): co-dependence excludes the three antecedence configurations and strict ellipsis readings; variable binding excludes strict only-readings.

Equations

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

def Landau2013.ofNoncoreferential (noncoreferential : Bool) : Control.Profile Clause74

The profile determined by whether a clause type licenses noncoreferential subjects: free reference fails both clauses, obligatory coreference forces both.

Equations

• Landau2013.ofNoncoreferential noncoreferential x✝ = !noncoreferential

@[simp]

theorem Landau2013.isObligatory_ofNoncoreferential {b : Bool} : (ofNoncoreferential b).IsObligatory ↔ b = false