Chierchia (1984): Topics in the Syntax and Semantics of Infinitives and Gerunds

@cite{chierchia-1984}

UMass Amherst dissertation (advisor: Barbara Hall Partee).

Core Thesis

Infinitival and gerundive complements denote properties (type ⟨e,t⟩), not propositions (type ⟨s,t⟩). Control is not syntactic movement of PRO but semantic entailment: a verb taking a property complement entails that one of its individual arguments has that property.

The Control Principle (CP)

If a verb α takes individual arguments x₁...xₙ and a property argument P, then α(x₁)...(P)...(xₙ) → P(xᵢ) for some designated controller xᵢ.

The controller is determined by predicate class, not syntactic configuration. This makes control a semantic universal: any verb that takes a property argument will exhibit control, because entailment is a semantic relation.

Three Control Classes

Chierchia distinguishes three classes by their closure properties under argument-structure operations (Ch IV §1):

1. Obligatory control (try, persuade, force, promise, want, enjoy, manage, begin): the verb entails that a specific argument has the complement property. The controller must be overtly present and bears a specific θ-role. Includes both subject control (try) and object control (persuade) verbs — the distinction is subject vs. object, not obligatory vs. semi-obligatory.
2. Semi-obligatory control (decide, signal, recommend): all the properties of obligatory control EXCEPT mandatory controller presence. The controller can be implicit or contextually recovered (e.g., "It was decided to leave").
3. Prominence control (bother, be dangerous, denounce): the controller is determined by discourse prominence, not by the CP. None of the six OC properties hold — no locality, no thematic uniqueness, split antecedents possible, long-distance control possible.

Modal Qualification

Control predicates involve modal qualification (Ch IV §2.2):

• try(P)(j) ↔ □_{try,j} P(j) — in all situations where what j tries will eventually succeed, j has property P
• force(P)(x)(y) ↔ □_{force,y} P(x) — in all situations compatible with what y imposes on x, x has property P

Chierchia adopts @cite{kratzer-1981}'s theory of conversational backgrounds to formalize this. Each control verb selects a conversational background type (deontic for force, buletic for try) and a modal relation (necessity or possibility). The formalization below uses the later two-parameter framework (modal base + ordering source) from @cite{kratzer-1991}, which refines Kratzer (1981)'s single-parameter approach.

Visser's and Bach's Generalizations (derived)

• Visser (Ch IV §1.1, ex. 11): Subject control verbs cannot passivize. If try(P)(j) → P(j), passivizing removes j from the argument structure, leaving P(?) without a controller.
• Bach (attributed by Bresnan 1982; Ch IV §1.1, ex. 13-14): Object control verbs cannot detransitivize. If persuade(P)(x)(j) → P(x), detransitivizing removes x, leaving P(?) without a controller.

Both follow from the entailment approach: removing the controller breaks the meaning postulate.

Connections

• The VP=Property hypothesis is the direct ancestor of @cite{chierchia-1998}'s ∩/∪ operators (which generalize to kinds) and of @cite{grano-2024}'s eventuality abstraction approach.
• The modal qualification of control connects to Kratzer's conversational backgrounds (already formalized in Semantics.Modality.Kratzer).
• The three control classes cut differently from Landau's predicative/logophoric split: Chierchia classifies ALL verbs with the CP as obligatory (including attitude verbs like want), while Landau separates attitude verbs as logophoric.

@[reducible, inline]

abbrev Chierchia1984.World : Type

Equations

• Chierchia1984.World = Fin 4

def Chierchia1984.allWorlds : List World

Equations

• Chierchia1984.allWorlds = [0, 1, 2, 3]

The VP = Property Hypothesis

The central type-theoretic claim: infinitival and gerundive complements denote properties (functions from individuals to truth values), not propositions (functions from worlds to truth values).

We derive the property/proposition classification from two existing infrastructure layers:

1. ComplementType.isFinite (VerbEntry.lean): finite = true for .finiteClause and .question
2. ComplSemLayer (TypeShifting.lean): the property/proposition distinction as a semantic type layer

The connection: nonfinite complements denote properties; finite complements denote propositions. This is not a new definition but a bridge between existing infrastructure.

def Chierchia1984.complSemLayer : Semantics.Lexical.ComplementType → Option Semantics.Composition.TypeShifting.ComplSemLayer

Map a ComplementType to the semantic layer it inhabits.

Returns none for complement types that are not clausal (NP, PP, etc.). For clausal types, the rule is: nonfinite → property, finite → proposition. This derives from ComplementType.isFinite, not a new stipulation.

Equations

• Chierchia1984.complSemLayer Semantics.Lexical.ComplementType.infinitival = some Semantics.Composition.TypeShifting.ComplSemLayer.property
• Chierchia1984.complSemLayer Semantics.Lexical.ComplementType.gerund = some Semantics.Composition.TypeShifting.ComplSemLayer.property
• Chierchia1984.complSemLayer Semantics.Lexical.ComplementType.smallClause = some Semantics.Composition.TypeShifting.ComplSemLayer.property
• Chierchia1984.complSemLayer Semantics.Lexical.ComplementType.finiteClause = some Semantics.Composition.TypeShifting.ComplSemLayer.proposition
• Chierchia1984.complSemLayer Semantics.Lexical.ComplementType.question = some Semantics.Composition.TypeShifting.ComplSemLayer.proposition
• Chierchia1984.complSemLayer Semantics.Lexical.ComplementType.none = none
• Chierchia1984.complSemLayer Semantics.Lexical.ComplementType.np = none
• Chierchia1984.complSemLayer Semantics.Lexical.ComplementType.np_np = none
• Chierchia1984.complSemLayer Semantics.Lexical.ComplementType.np_pp = none

theorem Chierchia1984.infinitival_is_property : complSemLayer Semantics.Lexical.ComplementType.infinitival = some Semantics.Composition.TypeShifting.ComplSemLayer.property

Nonfinite clausal complements are property-denoting.

theorem Chierchia1984.gerund_is_property : complSemLayer Semantics.Lexical.ComplementType.gerund = some Semantics.Composition.TypeShifting.ComplSemLayer.property

theorem Chierchia1984.finiteClause_is_proposition : complSemLayer Semantics.Lexical.ComplementType.finiteClause = some Semantics.Composition.TypeShifting.ComplSemLayer.proposition

Finite clausal complements are proposition-denoting.

theorem Chierchia1984.question_is_proposition : complSemLayer Semantics.Lexical.ComplementType.question = some Semantics.Composition.TypeShifting.ComplSemLayer.proposition

theorem Chierchia1984.np_no_layer : complSemLayer Semantics.Lexical.ComplementType.np = none

Non-clausal complement types have no semantic layer.

The Control Principle (CP)

The CP is a meaning postulate on verbs that take property arguments: if a verb takes a property P and individual arguments, it entails that one of those individuals has property P.

We formalize this as a structure bundling the verb's semantics with its control entailment. The entailment is by construction: the entails field witnesses that the semantics forces P to hold of the controlled argument.

Chierchia's full CP (Ch IV ex. 43) is a biconditional: □ α(x₁)..(P)..(xₙ) ↔ M_a P(xᵢ) We formalize the left-to-right direction (the entailment) because this is the load-bearing direction for control: it guarantees that the controller has the complement property whenever the matrix verb holds.

structure Chierchia1984.ControlVerb (E Args : Type) : Type

A control verb with the Control Principle built in.

The CP states: for any property P and world w where the verb's meaning holds, some designated argument has property P. The controller function selects which argument (from the full argument tuple) serves as controller.

Parameterized over an argument tuple type Args — subject control verbs use Args = E (just the subject), object control verbs use Args = E × E (object, subject).

• sem : (E → Bool) → Args → World → Bool

  The verb's semantics: property → arguments → world → Bool

• controller : Args → E

  Select the controlled argument from the argument tuple

• entails (P : E → Bool) (args : Args) (w : World) : self.sem P args w = true → P (self.controller args) = true

  The Control Principle: verb(P)(args)(w) → P(controller(args))

@[reducible, inline]

abbrev Chierchia1984.SubjControlVerb (E : Type) : Type

Subject control verb: Args = E, controller is the identity.

Equations

• Chierchia1984.SubjControlVerb E = Chierchia1984.ControlVerb E E

@[reducible, inline]

abbrev Chierchia1984.ObjControlVerb (E : Type) : Type

Object control verb: Args = E × E (object, subject), controller selects the object (first component).

Equations

• Chierchia1984.ObjControlVerb E = Chierchia1984.ControlVerb E (E × E)

Modal Qualification

@cite{chierchia-1984} Ch IV §2.2: control predicates involve modal qualification. The verb's meaning is not simply "x does P" but "in all situations compatible with certain conditions, x does P."

Chierchia adopts @cite{kratzer-1981}'s theory of conversational backgrounds: each control verb selects a conversational background type and a modal relation (necessity or possibility).

• try: buletic conversational background, necessity. try(P)(j) iff in all situations compatible with j's aims, j does P.
• force: deontic conversational background, necessity. force(P)(x)(y) iff in all situations compatible with what y imposes on x, x does P.
• allow: deontic conversational background, possibility. allow(P)(x)(y) iff there exists a situation compatible with what y imposes on x where x does P.

The formalization below uses the later two-parameter framework (modal base + ordering source) from @cite{kratzer-1991}, which refines Kratzer (1981)'s single-parameter approach. The ModalBase corresponds roughly to the circumstantial facts, and the OrderingSource to the conversational background type (bouletic, deontic, etc.). This is a modernization, not what Chierchia literally writes — he uses a single "conversational background" parameter.

Note: the property P here is extensional (E → Bool), so the modal quantification over bestWorlds checks that the controller has P whenever the accessible worlds are nonempty. A fully intensional version would use E → World → Bool, allowing P's extension to vary across worlds. We use the extensional version for simplicity, matching the level of abstraction in the ControlVerb structure.

structure Chierchia1984.ModalControl (E Args : Type) : Type

A modally qualified control verb: the verb's semantics is defined via Kratzer necessity over a modal base and ordering source.

The CP follows from the modal semantics + reflexivity (axiom T): if □P(x) and the actual world is among the best worlds, then P(x).

• base : Core.Logic.Intensional.ModalBase World

  Circumstantial modal base

• ordering : Core.Logic.Intensional.OrderingSource World

  Ordering source (bouletic for try, deontic for force, ...)

• controller : Args → E

  Select the controlled argument

• reflexive (w : World) : w ∈ Semantics.Modality.Kratzer.bestWorlds self.base self.ordering w

  Reflexivity: actual world is among best worlds (axiom T)

def Chierchia1984.ModalControl.toControlVerb (E Args : Type) (m : ModalControl E Args) : ControlVerb E Args

Construct a ControlVerb from a ModalControl.

The verb's semantics is: verb(P)(args)(w) = ∀w' ∈ bestWorlds(w). P(controller(args)). The CP follows from reflexivity.

Equations

• Chierchia1984.ModalControl.toControlVerb E Args m = { sem := fun (P : E → Bool) (args : Args) (_w : Chierchia1984.World) => P (m.controller args), controller := m.controller, entails := ⋯ }

Visser's and Bach's Generalizations

These follow from the CP: if an argument-structure operation removes the controller, the entailment cannot be satisfied.

• Visser (Ch IV §1.1, ex. 11): Subject control verbs cannot passivize. Passivization demotes the subject (A → oblique/unexpressed), but the CP requires P(subject). No subject → no entailment.
• Bach (attributed by Bresnan 1982; Ch IV §1.1, ex. 13-14): Object control verbs cannot detransitivize. Detransitivization removes the object, but the CP requires P(object).

We state these as: any faithful argument-reduction operation on a control verb preserves existential control (∃x. P(x)) but loses specific control (the guarantee that a particular argument has P).

theorem Chierchia1984.visser (E : Type) (v : SubjControlVerb E) (pass : (E → Bool) → World → Bool) (faithful : ∀ (P : E → Bool) (w : World), pass P w = true → ∃ (x : E), v.sem P x w = true) (P : E → Bool) (w : World) : pass P w = true → ∃ (x : E), P x = true

Visser's generalization: if a subject control verb is faithfully passivized (every passive truth witnesses some active truth), then P is satisfied by some entity — but the passive form cannot identify which entity. The CP guarantees existence.

theorem Chierchia1984.bach (E : Type) (v : ObjControlVerb E) (detrans : (E → Bool) → E → World → Bool) (faithful : ∀ (P : E → Bool) (y : E) (w : World), detrans P y w = true → ∃ (args : E × E), v.sem P args w = true) (P : E → Bool) (y : E) (w : World) : detrans P y w = true → ∃ (x : E), P x = true

Bach's generalization: if an object control verb is faithfully detransitivized (losing the object argument), the CP still guarantees ∃x. P(x), but the detransitivized form cannot identify the specific x.

inductive Chierchia1984.ChierchiaControlClass : Type

@cite{chierchia-1984}'s three control classes (Ch IV §1), distinguished by their closure properties under argument-structure operations.

• obligatory: all six OC properties hold (locality, no arbitrary reading, thematic uniqueness, no split antecedents, obligatory controller presence, Visser/Bach sensitivity). Includes both subject control (try, manage, begin) and object control (persuade, force) verbs. (Ch IV §1.1, ex. 4-6, properties in ex. 17)
• semiObligatory: all OC properties EXCEPT obligatory controller presence — the controller can be implicit or contextually recovered. (Ch IV §1.2, ex. 18: decide, signal, recommend)
• prominence: controller determined by discourse prominence, not by the CP. None of the six OC properties hold. (Ch IV §1.3, ex. 25: bother, be dangerous, denounce)

• obligatory : ChierchiaControlClass
• semiObligatory : ChierchiaControlClass
• prominence : ChierchiaControlClass

@[implicit_reducible]

instance Chierchia1984.instDecidableEqChierchiaControlClass : DecidableEq ChierchiaControlClass

Equations

• Chierchia1984.instDecidableEqChierchiaControlClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Chierchia1984.instReprChierchiaControlClass.repr : ChierchiaControlClass → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Chierchia1984.instReprChierchiaControlClass : Repr ChierchiaControlClass

Equations

• Chierchia1984.instReprChierchiaControlClass = { reprPrec := Chierchia1984.instReprChierchiaControlClass.repr }

The six properties of obligatory control (Ch IV ex. 17)

The six classic properties that define the obligatory control class:

a. Locality: the controller must be a matrix argument b. No arbitrary reading: the controlled position has a specific referent c. Thematic uniqueness: the controller bears a specific θ-role d. No split antecedents: the controller is singular e. Obligatory controller presence: a controller must exist f. Visser/Bach sensitivity: removing the controller is impossible

All six follow from two facts: (A) the CP requires a specific argument to have property P, and (B) obligatory control verbs have a fixed, lexically determined controller.

Semi-obligatory control has (a-d) and (f) but not (e). Prominence control has none of the six.

def Chierchia1984.ChierchiaControlClass.hasCP : ChierchiaControlClass → Bool

Whether a control class has the CP (entailment-based control).

Equations

• Chierchia1984.ChierchiaControlClass.obligatory.hasCP = true
• Chierchia1984.ChierchiaControlClass.semiObligatory.hasCP = true
• Chierchia1984.ChierchiaControlClass.prominence.hasCP = false

theorem Chierchia1984.prominence_no_cp : ChierchiaControlClass.prominence.hasCP = false

Prominence control lacks the CP and relaxes all OC properties.

Per-Verb Classification

Derive @cite{chierchia-1984}'s control class from VerbCore fields.

In Chierchia's taxonomy, ALL control verbs with a fixed, lexically determined controller are obligatory — regardless of whether they are subject or object control, and regardless of whether they are attitude verbs. The subject/object distinction and the attitude/non-attitude distinction are orthogonal to the obligatory/semi-obligatory/prominence trichotomy.

The semi-obligatory class (decide, signal, recommend) requires a VerbCore field for controller optionality, which does not currently exist. The prominence class (bother, be dangerous) requires verbs not currently in the English Fragment. Therefore, all current Fragment control verbs are classified as obligatory.

def Chierchia1984.derivedChierchiaClass (v : Semantics.Lexical.VerbCore) : Option ChierchiaControlClass

Equations

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

Passivizability: Derived from Deeper Principles

Visser's and Bach's generalizations both follow from a single structural principle: an alternation is blocked by the CP iff it removes the controller from core-term status.

The derivation has three steps:

1. Which argument is the controller? Subject control verbs have their A (agent-like) argument as controller; object control verbs have their P (patient-like) argument. Raising and non-control verbs have no semantic controller.

2. What does the alternation do to that argument? Passivization denucleativizes A and maintains P (Syntax.ArgumentStructure.Alternation.passivization). Antipassivization (detransitivization) denucleativizes P and maintains A.

3. Does removing the controller break the CP? If the alternation denucleativizes or suppresses the controller, the CP cannot be satisfied → the alternation is blocked.

This replaces the stipulated predictedPassivizable case-split with a derivation from Syntax.ArgumentStructure.Alternation.passivization and ControlType.

def Chierchia1984.controllerRole : Semantics.Lexical.ControlType → Option Syntax.ArgumentStructure.Alternation.TRRole

Which TR-role serves as the controller, per @cite{chierchia-1984}'s CP.

Subject control: A is the controller (the subject has property P). Object control: P is the controller (the object has property P). Raising/none: no semantic controller (the CP does not apply).

Equations

• Chierchia1984.controllerRole Semantics.Lexical.ControlType.subjectControl = some Syntax.ArgumentStructure.Alternation.TRRole.A
• Chierchia1984.controllerRole Semantics.Lexical.ControlType.objectControl = some Syntax.ArgumentStructure.Alternation.TRRole.P
• Chierchia1984.controllerRole Semantics.Lexical.ControlType.raising = none
• Chierchia1984.controllerRole Semantics.Lexical.ControlType.none = none

def Chierchia1984.cpBlocksAlternation (ct : Semantics.Lexical.ControlType) (va : Syntax.ArgumentStructure.Alternation.ValencyAlternation) : Bool

The CP blocks an alternation iff the alternation removes the controller from core-term status (denucleativizes or suppresses it).

This is the general structural principle behind both Visser's generalization (passivization blocked for subject control) and Bach's generalization (detransitivization blocked for object control).

Equations

• Chierchia1984.cpBlocksAlternation ct va = match Chierchia1984.controllerRole ct with | some role => (va.fateOfRole role).removesFromCoreStatus | none => false

def Chierchia1984.derivedPassivizable (ct : Semantics.Lexical.ControlType) : Bool

Derived passivizability: a control verb can passivize iff the CP does not block passivization.

• Subject control: controller = A, passivization denucleativizes A → CP broken → blocked (Visser's generalization)
• Object control: controller = P, passivization maintains P → CP intact → allowed
• Raising/none: no CP → no constraint → allowed

Equations

• Chierchia1984.derivedPassivizable ct = !Chierchia1984.cpBlocksAlternation ct Syntax.ArgumentStructure.Alternation.passivization

theorem Chierchia1984.subjectControl_blocks_passivization : cpBlocksAlternation Semantics.Lexical.ControlType.subjectControl Syntax.ArgumentStructure.Alternation.passivization = true

Subject control blocks passivization: passivization denucleativizes A, but the controller IS A. Denucleativizing the controller breaks the CP (Visser's generalization).

theorem Chierchia1984.objectControl_allows_passivization : cpBlocksAlternation Semantics.Lexical.ControlType.objectControl Syntax.ArgumentStructure.Alternation.passivization = false

Object control allows passivization: passivization maintains P, and the controller IS P. The controller survives → CP intact.

theorem Chierchia1984.objectControl_blocks_detransitivization : cpBlocksAlternation Semantics.Lexical.ControlType.objectControl Syntax.ArgumentStructure.Alternation.antipassivization = true

Object control blocks detransitivization: antipassivization denucleativizes P, but the controller IS P (Bach's generalization).

theorem Chierchia1984.subjectControl_allows_detransitivization : cpBlocksAlternation Semantics.Lexical.ControlType.subjectControl Syntax.ArgumentStructure.Alternation.antipassivization = false

Subject control allows detransitivization: antipassivization maintains A, and the controller IS A. (e.g., "Mary promised Bill to come" → "Mary promised to come".)

theorem Chierchia1984.try_obligatory : derivedChierchiaClass Fragments.English.Predicates.Verbal.try_.toVerbCore = some ChierchiaControlClass.obligatory

All control verbs in the Fragment are obligatory control in Chierchia's sense — they have a fixed, lexically determined controller and exhibit all six OC properties.

theorem Chierchia1984.manage_obligatory : derivedChierchiaClass Fragments.English.Predicates.Verbal.manage.toVerbCore = some ChierchiaControlClass.obligatory

theorem Chierchia1984.begin_obligatory : derivedChierchiaClass Fragments.English.Predicates.Verbal.begin_.toVerbCore = some ChierchiaControlClass.obligatory

theorem Chierchia1984.stop_obligatory : derivedChierchiaClass Fragments.English.Predicates.Verbal.stop.toVerbCore = some ChierchiaControlClass.obligatory

theorem Chierchia1984.continue_obligatory : derivedChierchiaClass Fragments.English.Predicates.Verbal.continue_.toVerbCore = some ChierchiaControlClass.obligatory

theorem Chierchia1984.fail_obligatory : derivedChierchiaClass Fragments.English.Predicates.Verbal.fail.toVerbCore = some ChierchiaControlClass.obligatory

theorem Chierchia1984.persuade_obligatory : derivedChierchiaClass Fragments.English.Predicates.Verbal.persuade.toVerbCore = some ChierchiaControlClass.obligatory

"persuade" is obligatory control in Chierchia's system — it has a fixed controller (the object) and all six OC properties. The subject/object distinction does not affect the obligatory class.

theorem Chierchia1984.force_obligatory : derivedChierchiaClass Fragments.English.Predicates.Verbal.force.toVerbCore = some ChierchiaControlClass.obligatory

theorem Chierchia1984.want_obligatory : derivedChierchiaClass Fragments.English.Predicates.Verbal.want.toVerbCore = some ChierchiaControlClass.obligatory

"want" is obligatory control in Chierchia's system — the subject is the fixed controller. Despite being an attitude verb, it has all six OC properties. (Contrast Landau, who classifies "want" as logophoric because of its attitude status.)

theorem Chierchia1984.hope_obligatory : derivedChierchiaClass Fragments.English.Predicates.Verbal.hope.toVerbCore = some ChierchiaControlClass.obligatory

theorem Chierchia1984.promise_obligatory : derivedChierchiaClass Fragments.English.Predicates.Verbal.promise.toVerbCore = some ChierchiaControlClass.obligatory

theorem Chierchia1984.try_passivizability_derived : derivedPassivizable Fragments.English.Predicates.Verbal.try_.controlType = Fragments.English.Predicates.Verbal.try_.passivizable

"try" (subject control): CP blocks passivization, stipulated not passivizable.

theorem Chierchia1984.persuade_passivizability_derived : derivedPassivizable Fragments.English.Predicates.Verbal.persuade.controlType = Fragments.English.Predicates.Verbal.persuade.passivizable

"persuade" (object control): CP allows passivization, stipulated passivizable.

theorem Chierchia1984.force_passivizability_derived : derivedPassivizable Fragments.English.Predicates.Verbal.force.controlType = Fragments.English.Predicates.Verbal.force.passivizable

"force" (object control): CP allows passivization, stipulated passivizable.

theorem Chierchia1984.try_property_denoting : complSemLayer Fragments.English.Predicates.Verbal.try_.complementType = some Semantics.Composition.TypeShifting.ComplSemLayer.property

"try" takes an infinitival complement, which denotes a property.

theorem Chierchia1984.want_property_denoting : complSemLayer Fragments.English.Predicates.Verbal.want.complementType = some Semantics.Composition.TypeShifting.ComplSemLayer.property

"want" takes an infinitival complement, which denotes a property.

theorem Chierchia1984.believe_proposition_denoting : complSemLayer Fragments.English.Predicates.Verbal.believe.complementType = some Semantics.Composition.TypeShifting.ComplSemLayer.proposition

"believe" takes a finite clause, which denotes a proposition.

theorem Chierchia1984.believe_not_control : derivedChierchiaClass Fragments.English.Predicates.Verbal.believe.toVerbCore = none

"believe" is not a control verb — consistent with taking a propositional, not property-denoting, complement.

Bridge to Landau (2015)

@cite{chierchia-1984} and @cite{landau-2015} cut the control verb space differently:

• Chierchia: ALL verbs with the CP are obligatory control, regardless of attitude status. The CP is a meaning postulate that applies uniformly. The subject/object and attitude/non-attitude distinctions are orthogonal.
• Landau: attitude verbs (want, hope, promise, persuade) are logophoric (perspectival coordinate needed), non-attitude verbs (try, manage, force) are predicative.

The systematic divergence: Chierchia → obligatory → predicative for ALL control verbs, while Landau → logophoric for attitude verbs. The theories agree on non-attitude verbs (both predicative) and diverge precisely on attitude verbs.

def Chierchia1984.chierchiaToLandauTier : ChierchiaControlClass → Landau2015.ControlTier

Map Chierchia's control classes to Landau's control tiers.

Equations

• Chierchia1984.chierchiaToLandauTier Chierchia1984.ChierchiaControlClass.obligatory = Landau2015.ControlTier.predicative
• Chierchia1984.chierchiaToLandauTier Chierchia1984.ChierchiaControlClass.semiObligatory = Landau2015.ControlTier.predicative
• Chierchia1984.chierchiaToLandauTier Chierchia1984.ChierchiaControlClass.prominence = Landau2015.ControlTier.logophoric

theorem Chierchia1984.cp_iff_predicative (c : ChierchiaControlClass) : c.hasCP = true ↔ chierchiaToLandauTier c = Landau2015.ControlTier.predicative

The CP/no-CP distinction aligns with the predicative/logophoric distinction: CP-bearing classes are predicative, CP-lacking classes are logophoric.

theorem Chierchia1984.cp_requires_syntactic_controller (c : ChierchiaControlClass) (h : c.hasCP = true) : (chierchiaToLandauTier c).requiresSyntacticController = true

Predicative control requires a syntactic controller (Landau's condition (90)), which is the syntactic reflex of Chierchia's CP: the entailment needs a specific argument to serve as controller.

Non-attitude verbs: Chierchia and Landau agree

For verbs without an attitude builder (try, manage, begin, stop, force, fail), both systems classify them as predicative control.

theorem Chierchia1984.try_agrees : Option.map chierchiaToLandauTier (derivedChierchiaClass Fragments.English.Predicates.Verbal.try_.toVerbCore) = Landau2015.derivedControlTier Fragments.English.Predicates.Verbal.try_.toVerbCore

theorem Chierchia1984.manage_agrees : Option.map chierchiaToLandauTier (derivedChierchiaClass Fragments.English.Predicates.Verbal.manage.toVerbCore) = Landau2015.derivedControlTier Fragments.English.Predicates.Verbal.manage.toVerbCore

theorem Chierchia1984.force_agrees : Option.map chierchiaToLandauTier (derivedChierchiaClass Fragments.English.Predicates.Verbal.force.toVerbCore) = Landau2015.derivedControlTier Fragments.English.Predicates.Verbal.force.toVerbCore

Attitude verbs: systematic divergence

For verbs with an attitude builder (want, hope, promise, persuade), the two systems diverge: Chierchia classifies them as obligatory (→ predicative), while Landau classifies them as logophoric.

This is a genuine theoretical disagreement: Chierchia groups by entailment structure (all verbs with the CP are treated uniformly), Landau groups by attitude status (attitude verbs introduce a perspectival coordinate that changes the control mechanism).

theorem Chierchia1984.want_diverges : Option.map chierchiaToLandauTier (derivedChierchiaClass Fragments.English.Predicates.Verbal.want.toVerbCore) = some Landau2015.ControlTier.predicative ∧ Landau2015.derivedControlTier Fragments.English.Predicates.Verbal.want.toVerbCore = some Landau2015.ControlTier.logophoric

theorem Chierchia1984.hope_diverges : Option.map chierchiaToLandauTier (derivedChierchiaClass Fragments.English.Predicates.Verbal.hope.toVerbCore) = some Landau2015.ControlTier.predicative ∧ Landau2015.derivedControlTier Fragments.English.Predicates.Verbal.hope.toVerbCore = some Landau2015.ControlTier.logophoric

theorem Chierchia1984.promise_diverges : Option.map chierchiaToLandauTier (derivedChierchiaClass Fragments.English.Predicates.Verbal.promise.toVerbCore) = some Landau2015.ControlTier.predicative ∧ Landau2015.derivedControlTier Fragments.English.Predicates.Verbal.promise.toVerbCore = some Landau2015.ControlTier.logophoric

theorem Chierchia1984.persuade_diverges : Option.map chierchiaToLandauTier (derivedChierchiaClass Fragments.English.Predicates.Verbal.persuade.toVerbCore) = some Landau2015.ControlTier.predicative ∧ Landau2015.derivedControlTier Fragments.English.Predicates.Verbal.persuade.toVerbCore = some Landau2015.ControlTier.logophoric