Landau (2024): Control

This file formalizes the empirical generalizations of [Lan24a], the Element surveying control theory. The trichotomy of obligatory control, non-obligatory control, and no control is read off finiteness and position on the Spanish paradigm (41): finite clauses show no control in either position, infinitival complements obligatory control, and infinitival subjects non-obligatory control, so non-obligatory control arises only in clauses that can display obligatory control (Status.of, noc_only_in_oc_capable). The revised Visser's generalization of [vU13] (19) bars implicit control when T agrees with a referential DP, the Norwegian personal and impersonal passives of promise (20) being the minimal pair (RVG, norwegian_rvg). The direct-discourse correlation of [Pos70] (33) predicts the controller from the person of the direct-discourse counterpart's subject, and the Korean jussive markers (35) realize it grammatically: the volitional, imperative, and exhortative markers induce subject, object, and split control under one verb of saying (korean_realizes_postal). Partial control is confined to attitude complements ((36), (37)): a predicative complement is saturated by its controller, which the library's saturating dependencies deny a partial reading (manage_excludes_pc), and only propositional complements host lexical subjects ((56), (58), (72), after [Gra15]). Non-obligatory control is licensed by topicality or by logophoric centrality, each sufficient and neither necessary ((52), (55), Antecedent.MayControl), and controlled adjuncts split into strict and alternating types by whether their head also builds a propositional variant ((84), (89), alternates_iff_propositional_variant).

Implementation notes

The tier system is that of Studies/Landau2015.lean; the generalizations are stated over the Element's own configurations, and the partial-control row is the one derived from the substrate. The strict/alternating split records both columns of table (89), the criterion being validated on the English inventory rather than derived.

References

• [Lan24a]
• [vU13]
• [Pos70]
• [Gra15]

The trichotomy (41)

inductive Landau2024a.Status : Type

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

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

@[instance_reducible]

instance Landau2024a.instDecidableEqStatus : DecidableEq Status

Equations

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

def Landau2024a.Status.of (finite complement : Bool) : Status

The control status of a clause by its finiteness and its position, the Spanish paradigm (41): finite clauses show no control anywhere, infinitival complements obligatory control, and infinitival subjects non-obligatory control.

Equations

• Landau2024a.Status.of finite complement = if finite = true then Landau2024a.Status.nc else if complement = true then Landau2024a.Status.oc else Landau2024a.Status.noc

theorem Landau2024a.noc_only_in_oc_capable (f c : Bool) : Status.of f c = Status.noc → f = false

Non-obligatory control occurs only in clauses that can display obligatory control, the infinitives; an uncontrolled finite clause is no control.

theorem Landau2024a.finite_is_nc (c : Bool) : Status.of true c = Status.nc

Finite clauses are no control in every position.

The revised Visser's generalization (19), (20)

structure Landau2024a.PassiveConfig : Type

A passive control configuration: whether T agrees with a referential DP, and whether implicit control obtains.

• tAgreesReferential : Bool
• implicitControl : Bool

@[instance_reducible]

instance Landau2024a.instDecidableEqPassiveConfig : DecidableEq PassiveConfig

Equations

• Landau2024a.instDecidableEqPassiveConfig = Landau2024a.instDecidableEqPassiveConfig.decEq

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

Equations

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

def Landau2024a.RVG (c : PassiveConfig) : Prop

The revised Visser's generalization of [vU13] (19): an implicit subject cannot control when T agrees with a referential DP.

Equations

• Landau2024a.RVG c = (c.tAgreesReferential = true → c.implicitControl = false)

@[instance_reducible]

instance Landau2024a.instDecidableRVG (c : PassiveConfig) : Decidable (RVG c)

Equations

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

def Landau2024a.personalPassive : PassiveConfig

The Norwegian personal passive of promise (20a): T agrees with the promisee, and the implicit agent cannot control.

Equations

• Landau2024a.personalPassive = { tAgreesReferential := true, implicitControl := false }

def Landau2024a.impersonalPassive : PassiveConfig

The impersonal passive (20b): an expletive, no referential agreement, and implicit control.

Equations

• Landau2024a.impersonalPassive = { tAgreesReferential := false, implicitControl := true }

theorem Landau2024a.norwegian_rvg : RVG personalPassive ∧ RVG impersonalPassive

The pair obeys the generalization, and the impersonal passive shows that the absence of referential agreement is what frees implicit control.

The direct-discourse correlation (33) and the Korean jussives (35)

inductive Landau2024a.DDSubject : Type

The subject of the direct-discourse counterpart.

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

@[instance_reducible]

instance Landau2024a.instDecidableEqDDSubject : DecidableEq DDSubject

Equations

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

inductive Landau2024a.Choice : Type

Which matrix argument controls.

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

@[instance_reducible]

instance Landau2024a.instDecidableEqChoice : DecidableEq Choice

Equations

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

def Landau2024a.postalChoice : DDSubject → Choice

The correlation of [Pos70] (33): a first-person direct-discourse subject gives subject control, a second-person one object control, and a joint one split control.

Equations

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

inductive Landau2024a.Jussive : Type

The Korean control-inducing jussive markers (35): volitional keyss, imperative la, exhortative ca.

• volitional : Jussive
• imperative : Jussive
• exhortative : Jussive

@[instance_reducible]

instance Landau2024a.instDecidableEqJussive : DecidableEq Jussive

Equations

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

def Landau2024a.Jussive.orientation : Jussive → DDSubject

The discourse orientation of each marker.

Equations

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

def Landau2024a.Jussive.controller : Jussive → Choice

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

Equations

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

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

The jussive table realizes the correlation: the controller is fixed by the embedded mood's orientation, not by the matrix verb, which is held constant.

Partial control is confined to attitude complements (36), (37)

def Landau2024a.tierTy : Landau2015.Tier → Montague.Ty

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

Equations

• Landau2024a.tierTy Landau2015.Tier.predicative = Montague.Ty.et
• Landau2024a.tierTy Landau2015.Tier.logophoric = Montague.Ty.t

theorem Landau2024a.lexicalSubject_iff_logophoric (t : Landau2015.Tier) : tierTy t = Montague.Ty.t ↔ t = Landau2015.Tier.logophoric

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

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

The configuration of (37a), John managed to gather at 6: the matrix controller in position 0, the embedded subject in position 1.

Equations

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

def Landau2024a.ex37Val : Fin 2 → ℕ

The partial-control reading's referent sizes: the controller is properly contained in the gathering group.

Equations

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

theorem Landau2024a.manage_excludes_pc : ¬Control.IsSaturating ex37Val ex37Dependency

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

Non-obligatory control: topic and logophoric center (52), (55)

structure Landau2024a.Antecedent : Type

A candidate antecedent's discourse status.

• topic : Bool
• logophoricCenter : Bool

@[instance_reducible]

instance Landau2024a.instDecidableEqAntecedent : DecidableEq Antecedent

Equations

• Landau2024a.instDecidableEqAntecedent = Landau2024a.instDecidableEqAntecedent.decEq

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

Equations

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

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

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

Equations

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

@[instance_reducible]

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

Equations

• Landau2024a.instDecidableMayControl a = { decide := decide (a.topic = true) || decide (a.logophoricCenter = true), reflects_decide := ⋯ }

theorem Landau2024a.licensing_cases : { topic := false, logophoricCenter := true }.MayControl ∧ { topic := true, logophoricCenter := false }.MayControl ∧ ¬{ topic := false, logophoricCenter := false }.MayControl

(52): the implicit passive agent, a logophoric center that is no topic, controls (52a), and so does an established topic with no perspective on the event (52b), while a DP with neither status cannot.

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

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

Adjunct control: strict against alternating (84), (89)

inductive Landau2024a.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 Landau2024a.instDecidableEqAdjunctType : DecidableEq AdjunctType

Equations

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

def Landau2024a.AdjunctType.Alternates : AdjunctType → Prop

The observed split of (84): the adjunct type alternates between obligatory and non-obligatory control, or is strictly obligatory.

Equations

• Landau2024a.AdjunctType.goal.Alternates = False
• Landau2024a.AdjunctType.result.Alternates = False
• Landau2024a.AdjunctType.stimulus.Alternates = False
• Landau2024a.AdjunctType.subjectPurpose.Alternates = False
• x✝.Alternates = True

def Landau2024a.AdjunctType.HasPropositionalVariant : AdjunctType → Prop

The structural column of (89): the adjunct's head also builds a propositional variant, one hosting a lexical subject.

Equations

• Landau2024a.AdjunctType.goal.HasPropositionalVariant = False
• Landau2024a.AdjunctType.result.HasPropositionalVariant = False
• Landau2024a.AdjunctType.stimulus.HasPropositionalVariant = False
• Landau2024a.AdjunctType.subjectPurpose.HasPropositionalVariant = False
• x✝.HasPropositionalVariant = True

@[instance_reducible]

instance Landau2024a.instDecidablePredAdjunctTypeAlternates : DecidablePred AdjunctType.Alternates

Equations

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

@[instance_reducible]

instance Landau2024a.instDecidablePredAdjunctTypeHasPropositionalVariant : DecidablePred AdjunctType.HasPropositionalVariant

Equations

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

theorem Landau2024a.alternates_iff_propositional_variant (a : AdjunctType) : a.Alternates ↔ a.HasPropositionalVariant

The propositional-variant criterion on the English inventory: an adjunct type alternates into non-obligatory control exactly when its head has a propositional variant, so the strict types are the purely predicative ones.