Landau (2024): Control

Formalizes [Lan24] (Cambridge Elements in Generative Syntax), the survey synthesizing the state of control theory: the revised Visser's generalization ((19), [vU13]), the direct-discourse correlation behind embedded-speech-act theories ((33), [Pos70]) and its Korean jussive realization ((35)), the attitude-only distribution of partial control ((36)–(37)), the OC/NOC/NC trichotomy ((41)), NOC's dual topic/logophoric licensing ((52)), and the strict-vs-alternating adjunct split with the propositional-variant criterion ((84)/(89)). The dual theory of §5 rests on the neutral substrate (Syntax/Control/Defs.lean) and the tier system of Studies/Landau2015.lean; this file holds the Element's own empirical generalizations and the complement typing ((56)/(58)/(72)). Its (95) challenges — backward control, PC's residue, agreement under property theories, the OC-NC generalization's crosslinguistic variation ([Gan19]), overt-PRO licensing, adjunct loci — are the open frontier.

References

• I. Landau, Control

The OC/NOC/NC trichotomy

NOC is the non-OC behavior of clauses that can display OC; clauses that never can (finite complements, in most languages) are no control (NC). The Spanish paradigm (41): infinitival complements are OC, infinitival subjects NOC, finite clauses NC in either position.

inductive Landau2024.Status : Type

Control statuses: obligatory, non-obligatory, and no control.

• oc : Status
• noc : Status
• nc : Status

@[instance_reducible]

instance Landau2024.instDecidableEqStatus : DecidableEq Status

Equations

• Landau2024.instDecidableEqStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Landau2024.instReprStatus : Repr Status

Equations

• Landau2024.instReprStatus = { reprPrec := Landau2024.instReprStatus.repr }

def Landau2024.instReprStatus.repr : Status → ℕ → Std.Format

Equations

• Landau2024.instReprStatus.repr Landau2024.Status.oc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Landau2024.Status.oc")).group prec✝
• Landau2024.instReprStatus.repr Landau2024.Status.noc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Landau2024.Status.noc")).group prec✝
• Landau2024.instReprStatus.repr Landau2024.Status.nc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Landau2024.Status.nc")).group prec✝

structure Landau2024.Ex41Row : Type

A row of the Spanish paradigm (41): clause finiteness, whether the clause sits in complement position, and its control status.

• finite : Bool
• complement : Bool
• status : Status

def Landau2024.instDecidableEqEx41Row.decEq (x✝ x✝¹ : Ex41Row) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Landau2024.instDecidableEqEx41Row : DecidableEq Ex41Row

Equations

• Landau2024.instDecidableEqEx41Row = Landau2024.instDecidableEqEx41Row.decEq

def Landau2024.instReprEx41Row.repr : Ex41Row → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Landau2024.instReprEx41Row : Repr Ex41Row

Equations

• Landau2024.instReprEx41Row = { reprPrec := Landau2024.instReprEx41Row.repr }

def Landau2024.ex41 : List Ex41Row

The four configurations of (41).

Equations

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

theorem Landau2024.noc_only_in_oc_capable (r : Ex41Row) : r ∈ ex41 → r.status = Status.noc → r.finite = false

NOC occurs only in clauses that can display OC: never in finite clauses, whose uncontrolled behavior is NC.

theorem Landau2024.finite_is_nc (r : Ex41Row) : r ∈ ex41 → r.finite = true → r.status = Status.nc

Finite clauses are NC in every position.

The revised Visser's generalization

(19), [vU13]: implicit subjects cannot control if T agrees with a referential DP. The Norwegian minimal pair (20): the personal passive (T agrees with the promisee) blocks implicit control; the impersonal passive (expletive, no referential agreement) allows it. The interrogative complements of (22) are a genuine standing exception.

structure Landau2024.PassiveConfig : Type

A passive control configuration: does T agree with a referential DP, and is implicit control licensed?

• tAgreesReferential : Bool
• implicitControlOK : Bool

def Landau2024.instDecidableEqPassiveConfig.decEq (x✝ x✝¹ : PassiveConfig) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Landau2024.instDecidableEqPassiveConfig : DecidableEq PassiveConfig

Equations

• Landau2024.instDecidableEqPassiveConfig = Landau2024.instDecidableEqPassiveConfig.decEq

def Landau2024.instReprPassiveConfig.repr : PassiveConfig → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Landau2024.instReprPassiveConfig : Repr PassiveConfig

Equations

• Landau2024.instReprPassiveConfig = { reprPrec := Landau2024.instReprPassiveConfig.repr }

def Landau2024.ex20 : List PassiveConfig

The Norwegian pair (20): personal vs impersonal passive of 'promise'.

Equations

• Landau2024.ex20 = [{ tAgreesReferential := true, implicitControlOK := false }, { tAgreesReferential := false, implicitControlOK := true }]

theorem Landau2024.rvg (c : PassiveConfig) : c ∈ ex20 → c.implicitControlOK = !c.tAgreesReferential

The revised Visser's generalization on (20): implicit control is licensed exactly where T does not agree with a referential DP.

The direct-discourse correlation and Korean jussives

[Pos70]'s generalization ((33)): if the direct-discourse counterpart's subject is second person, the controller is the object; if first person, the subject. The Korean jussive markers realize the correlation grammatically ((35), with mal 'say' held fixed): the volitional marker is speaker-oriented and induces subject control, the imperative addressee-oriented inducing object control, the exhortative speaker+addressee-oriented inducing split control; the indicative induces no control.

inductive Landau2024.DDSubject : Type

The subject of the direct-discourse counterpart.

• speaker : DDSubject
• addressee : DDSubject
• speakerPlusAddressee : DDSubject

@[instance_reducible]

instance Landau2024.instDecidableEqDDSubject : DecidableEq DDSubject

Equations

• Landau2024.instDecidableEqDDSubject x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Landau2024.instReprDDSubject : Repr DDSubject

Equations

• Landau2024.instReprDDSubject = { reprPrec := Landau2024.instReprDDSubject.repr }

def Landau2024.instReprDDSubject.repr : DDSubject → ℕ → Std.Format

Equations

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

inductive Landau2024.Choice : Type

Which matrix argument controls.

• subject : Choice
• object : Choice
• split : Choice

@[instance_reducible]

instance Landau2024.instDecidableEqChoice : DecidableEq Choice

Equations

• Landau2024.instDecidableEqChoice x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Landau2024.instReprChoice.repr : Choice → ℕ → Std.Format

Equations

• Landau2024.instReprChoice.repr Landau2024.Choice.subject prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Landau2024.Choice.subject")).group prec✝
• Landau2024.instReprChoice.repr Landau2024.Choice.object prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Landau2024.Choice.object")).group prec✝
• Landau2024.instReprChoice.repr Landau2024.Choice.split prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Landau2024.Choice.split")).group prec✝

@[instance_reducible]

instance Landau2024.instReprChoice : Repr Choice

Equations

• Landau2024.instReprChoice = { reprPrec := Landau2024.instReprChoice.repr }

def Landau2024.postalChoice : DDSubject → Choice

[Pos70]'s correlation (33), stated over discourse roles: speaker-subject direct discourse → subject control, addressee-subject → object control, joint → split.

Equations

• Landau2024.postalChoice Landau2024.DDSubject.speaker = Landau2024.Choice.subject
• Landau2024.postalChoice Landau2024.DDSubject.addressee = Landau2024.Choice.object
• Landau2024.postalChoice Landau2024.DDSubject.speakerPlusAddressee = Landau2024.Choice.split

inductive Landau2024.Jussive : Type

The Korean control-inducing jussive markers ((35b–d)).

• volitional : Jussive

  volitional keyss

• imperative : Jussive

  imperative la

• exhortative : Jussive

  exhortative ca

@[instance_reducible]

instance Landau2024.instDecidableEqJussive : DecidableEq Jussive

Equations

• Landau2024.instDecidableEqJussive x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Landau2024.instReprJussive : Repr Jussive

Equations

• Landau2024.instReprJussive = { reprPrec := Landau2024.instReprJussive.repr }

def Landau2024.instReprJussive.repr : Jussive → ℕ → Std.Format

Equations

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

def Landau2024.Jussive.orientation : Jussive → DDSubject

The discourse orientation of each jussive marker.

Equations

• Landau2024.Jussive.volitional.orientation = Landau2024.DDSubject.speaker
• Landau2024.Jussive.imperative.orientation = Landau2024.DDSubject.addressee
• Landau2024.Jussive.exhortative.orientation = Landau2024.DDSubject.speakerPlusAddressee

def Landau2024.Jussive.controller : Jussive → Choice

The controller each marker induces under mal 'say' ((35b–d)).

Equations

• Landau2024.Jussive.volitional.controller = Landau2024.Choice.subject
• Landau2024.Jussive.imperative.controller = Landau2024.Choice.object
• Landau2024.Jussive.exhortative.controller = Landau2024.Choice.split

theorem Landau2024.korean_realizes_postal (j : Jussive) : j.controller = postalChoice j.orientation

The Korean jussive table realizes [Pos70]'s correlation: controller choice is the direct-discourse role of the marker's orientation — determined by the embedded mood, not the (fixed) matrix verb.

Partial control is attitude-only

(36)–(37): PC is attested in attitude complements and unavailable under implicatives — *John managed to gather at 6 (37a). On the dual theory this is Control.IsSaturating.not_isPartial: implicative complements are predicative, and predication saturates, sharing the referent exhaustively. The (37a) configuration refutes saturating status for its hypothetical PC reading, never the other way around.

def Landau2024.tierDenotation : Landau2015.Tier → Semantics.Composition.TypeShifting.ComplementDenotation

The semantic layer a tier's complement inhabits ((56)/(58)): predicative complements are properties, logophoric ones propositions.

Equations

• Landau2024.tierDenotation Landau2015.Tier.predicative = Semantics.Composition.TypeShifting.ComplementDenotation.property
• Landau2024.tierDenotation Landau2015.Tier.logophoric = Semantics.Composition.TypeShifting.ComplementDenotation.proposition

theorem Landau2024.lexicalSubject_iff_logophoric (t : Landau2015.Tier) : tierDenotation t = Semantics.Composition.TypeShifting.ComplementDenotation.proposition ↔ t = Landau2015.Tier.logophoric

Generalization (72): a lexical subject saturates a property, so exactly the propositional (logophoric, attitude) complements license one (the generalization originates with [Gra15]).

def Landau2024.ex37Dependency : SetRel (Fin 2) (Fin 2)

The (37a) configuration: matrix controller position 0, embedded subject position 1.

Equations

• Landau2024.ex37Dependency = {(0, 1)}

def Landau2024.ex37Val : Fin 2 → ℕ

The PC reading's referent sizes: the controller (John) is properly contained in the gathering group.

Equations

• Landau2024.ex37Val p = if p = 0 then 1 else 2

theorem Landau2024.manage_excludes_pc : ¬Control.IsSaturating ex37Val ex37Dependency

A partial-control reading is incompatible with a saturating dependency: (37a)'s star, from exhaustive sharing.

NOC: dual licensing by topic and logophoric center

(52): topicality and logophoricity are each sufficient for NOC antecedence and neither is necessary — (52a) is NOC by a [−top, +log] antecedent (an implicit passive agent), (52b) by [+top, −log] (an established topic with no mental perspective on the event). The [+human] character of logophoric antecedents follows from mental perspective; topical antecedents are only preferentially human — the (55b) default [+topic] → [+human], with (49) the resisting data and (50) the attested overrides.

structure Landau2024.Antecedent : Type

A candidate NOC antecedent's discourse status.

• topic : Bool
• logophoricCenter : Bool

@[instance_reducible]

instance Landau2024.instDecidableEqAntecedent : DecidableEq Antecedent

Equations

• Landau2024.instDecidableEqAntecedent = Landau2024.instDecidableEqAntecedent.decEq

def Landau2024.instDecidableEqAntecedent.decEq (x✝ x✝¹ : Antecedent) : Decidable (x✝ = x✝¹)

Equations

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

def Landau2024.instReprAntecedent.repr : Antecedent → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Landau2024.instReprAntecedent : Repr Antecedent

Equations

• Landau2024.instReprAntecedent = { reprPrec := Landau2024.instReprAntecedent.repr }

def Landau2024.Antecedent.MayControl (a : Antecedent) : Prop

(55a): a DP may serve as NOC controller iff it is a topic or a logophoric center.

Equations

• a.MayControl = (a.topic = true ∨ a.logophoricCenter = true)

@[instance_reducible]

instance Landau2024.instDecidableMayControl (a : Antecedent) : Decidable a.MayControl

Equations

• Landau2024.instDecidableMayControl a = Landau2024.instDecidableMayControl._aux_1 a

theorem Landau2024.noc_by_log_alone : { topic := false, logophoricCenter := true }.MayControl

(52a): the implicit passive agent — a logophoric center that is no topic — controls.

theorem Landau2024.noc_by_topic_alone : { topic := true, logophoricCenter := false }.MayControl

(52b): the established topic with no perspective on the event controls.

theorem Landau2024.neither_licensor_necessary : (¬∀ (a : Antecedent), a.MayControl → a.topic = true) ∧ ¬∀ (a : Antecedent), a.MayControl → a.logophoricCenter = true

Neither licensor is necessary — each (52) case lacks the other's.

theorem Landau2024.no_status_no_control : ¬{ topic := false, logophoricCenter := false }.MayControl

A DP with neither status cannot serve as NOC controller.

Adjunct control: strict OC vs alternating OC/NOC

(84): English controlled adjuncts split into strict OC adjuncts and adjuncts alternating OC/NOC; strict NOC adjuncts are unattested. The propositional-variant criterion ((89)): an adjunct type alternates iff its head also builds a variant hosting a lexical subject — the P head s-selects a property only (strict) or a property/proposition ambiguously (alternating).

inductive Landau2024.AdjunctType : Type

The English controlled-adjunct types of (84).

• goal : AdjunctType
• result : AdjunctType
• stimulus : AdjunctType
• subjectPurpose : AdjunctType
• objectPurpose : AdjunctType
• rationale : AdjunctType
• temporal : AdjunctType
• absolutive : AdjunctType
• justification : AdjunctType
• telic : AdjunctType

@[instance_reducible]

instance Landau2024.instDecidableEqAdjunctType : DecidableEq AdjunctType

Equations

• Landau2024.instDecidableEqAdjunctType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Landau2024.instReprAdjunctType.repr : AdjunctType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Landau2024.instReprAdjunctType : Repr AdjunctType

Equations

• Landau2024.instReprAdjunctType = { reprPrec := Landau2024.instReprAdjunctType.repr }

def Landau2024.observedAlternates : AdjunctType → Bool

(84)'s observed split: does the adjunct type ever alternate into NOC?

Equations

• Landau2024.observedAlternates Landau2024.AdjunctType.goal = false
• Landau2024.observedAlternates Landau2024.AdjunctType.result = false
• Landau2024.observedAlternates Landau2024.AdjunctType.stimulus = false
• Landau2024.observedAlternates Landau2024.AdjunctType.subjectPurpose = false
• Landau2024.observedAlternates x✝ = true

def Landau2024.hasPropositionalVariant : AdjunctType → Bool

(89)'s structural column: does the adjunct head build a propositional variant (one hosting a lexical subject)?

Equations

• Landau2024.hasPropositionalVariant Landau2024.AdjunctType.goal = false
• Landau2024.hasPropositionalVariant Landau2024.AdjunctType.result = false
• Landau2024.hasPropositionalVariant Landau2024.AdjunctType.stimulus = false
• Landau2024.hasPropositionalVariant Landau2024.AdjunctType.subjectPurpose = false
• Landau2024.hasPropositionalVariant x✝ = true

theorem Landau2024.alternates_iff_propositional_variant (a : AdjunctType) : observedAlternates a = hasPropositionalVariant a

The propositional-variant criterion, validated on the English inventory: an adjunct type alternates into NOC exactly when its head has a propositional variant.