Chierchia (1984): Topics in the syntax and semantics of infinitives and gerunds

This file formalizes the control theory of [Chi84]. Infinitival and gerundive complements denote properties, not propositions, and control is not movement of PRO but entailment: the Control Principle is a meaning postulate on a verb taking a property complement, that it holds of the property and its arguments exactly when a designated argument has the property throughout the situations the verb's conversational background selects ([Kra81b]), so the controller is fixed by the predicate's meaning rather than by syntactic configuration. Visser's and Bach's generalizations follow: a subject-control verb cannot passivize and an object-control verb cannot detransitivize, since either alternation removes the argument the postulate needs. The control classes of chapter IV are cut by whether the postulate applies and whether the controller must be expressed. The theorems derive the controller's having the property from the postulate, the blocking of each valency alternation from which argument controls, and check the Fragment's control verbs against both.

Implementation notes

• The conversational background is the two-parameter one of [Kra91], a modal base and an ordering source, and the entailment is necessity over it; the possibility that allow needs is not instantiated.

References

• [Chi84]
• [Kra81b]
• [Kra91]

The Control Principle (chapter IV)

structure Chierchia1984.ControlVerb (E : Type u_4) (W : Type u_5) (Args : Type u_6) : Type (max (max u_4 u_5) u_6)

A verb taking a property complement, with the Control Principle as its meaning postulate: the verb holds of a property and its arguments at a world exactly when the argument it controls has the property throughout the situations its conversational background selects, what is aimed at for try, what is imposed for force.

• sem : (E → W → Prop) → Args → W → Prop
• controller : Args → E
• accessible : Args → W → Set W
• control (P : E → W → Prop) (args : Args) (w : W) : self.sem P args w ↔ ∀ w' ∈ self.accessible args w, P (self.controller args) w'

@[reducible, inline]

abbrev Chierchia1984.SubjectControlVerb (E : Type u_4) (W : Type u_5) : Type (max u_4 u_5)

A subject-control verb's one argument is its controller.

Equations

• Chierchia1984.SubjectControlVerb E W = Chierchia1984.ControlVerb E W E

@[reducible, inline]

abbrev Chierchia1984.ObjectControlVerb (E : Type u_4) (W : Type u_5) : Type (max u_4 u_5)

An object-control verb controls the first of its object and subject.

Equations

• Chierchia1984.ObjectControlVerb E W = Chierchia1984.ControlVerb E W (E × E)

def Chierchia1984.ControlVerb.ofKratzer {E : Type u_1} {W : Type u_2} {Args : Type u_3} (base ordering : Modality.Background W) (controller : Args → E) : ControlVerb E W Args

A control verb from a modal base and an ordering source, [Kra91]'s form of the background: the controller has the property throughout the best accessible worlds.

Equations

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

theorem Chierchia1984.ControlVerb.controller_has {E : Type u_1} {W : Type u_2} {Args : Type u_3} (v : ControlVerb E W Args) {P : E → W → Prop} {args : Args} {w : W} (h : v.sem P args w) (w' : W) : w' ∈ v.accessible args w → P (v.controller args) w'

The controller has the property in every situation the background selects.

theorem Chierchia1984.ControlVerb.controller_has_self {E : Type u_1} {W : Type u_2} {Args : Type u_3} (v : ControlVerb E W Args) (hrefl : ∀ (args : Args) (w : W), w ∈ v.accessible args w) {P : E → W → Prop} {args : Args} {w : W} (h : v.sem P args w) : P (v.controller args) w

Over a reflexive background the controller has the property at the world itself.

Visser's and Bach's generalizations (chapter IV)

theorem Chierchia1984.visser {E : Type u_1} {W : Type u_2} (v : SubjectControlVerb E W) (pass : (E → W → Prop) → W → Prop) (faithful : ∀ (P : E → W → Prop) (w : W), pass P w → ∃ (x : E), v.sem P x w) {P : E → W → Prop} {w : W} (h : pass P w) : ∃ (x : E), ∀ w' ∈ v.accessible x w, P (v.controller x) w'

Visser's generalization: a faithful passive of a subject-control verb, one whose truth witnesses a truth of the active, can only guarantee that some entity has the property in the selected situations; the argument the postulate would name is gone.

theorem Chierchia1984.bach {E : Type u_1} {W : Type u_2} (v : ObjectControlVerb E W) (detrans : (E → W → Prop) → E → W → Prop) (faithful : ∀ (P : E → W → Prop) (y : E) (w : W), detrans P y w → ∃ (args : E × E), v.sem P args w) {P : E → W → Prop} {y : E} {w : W} (h : detrans P y w) : ∃ (args : E × E), ∀ w' ∈ v.accessible args w, P (v.controller args) w'

Bach's generalization: the same for a faithful detransitive of an object-control verb.

Control classes (chapter IV, section 1)

inductive Chierchia1984.ControlClass : Type

The three control classes: obligatory control, where the Control Principle fixes a controller that must be expressed, try and persuade alike; semi-obligatory control, where the controller may stay implicit, decide, recommend; and prominence control, where discourse rather than the postulate fixes it, bother, be dangerous.

• obligatory : ControlClass
• semiObligatory : ControlClass
• prominence : ControlClass

@[instance_reducible]

instance Chierchia1984.instDecidableEqControlClass : DecidableEq ControlClass

Equations

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

def Chierchia1984.instReprControlClass.repr : ControlClass → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Chierchia1984.instReprControlClass : Repr ControlClass

Equations

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

def Chierchia1984.ControlClass.HasControlPrinciple : ControlClass → Prop

The Control Principle governs the first two classes.

Equations

• Chierchia1984.ControlClass.obligatory.HasControlPrinciple = True
• Chierchia1984.ControlClass.semiObligatory.HasControlPrinciple = True
• Chierchia1984.ControlClass.prominence.HasControlPrinciple = False

@[instance_reducible]

instance Chierchia1984.instDecidablePredControlClassHasControlPrinciple : DecidablePred ControlClass.HasControlPrinciple

Equations

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

def Chierchia1984.ControlClass.ofVerb (v : Verb) : Option ControlClass

The class of a Fragment verb: every verb the Fragment marks for control has a fixed controller and is obligatory control, the Fragment recording neither an implicit controller nor the prominence verbs.

Equations

• Chierchia1984.ControlClass.ofVerb v = if v.controlType = ControlType.none ∧ v.altControlType = ControlType.none then none else some Chierchia1984.ControlClass.obligatory

Which alternations the postulate blocks

def Chierchia1984.controllerRole : ControlType → Option Voice.TermRole

The argument the postulate needs: the agent-like term of a subject-control verb, the patient-like term of an object-control verb, none for raising.

Equations

• Chierchia1984.controllerRole ControlType.subjectControl = some Voice.TermRole.A
• Chierchia1984.controllerRole ControlType.objectControl = some Voice.TermRole.P
• Chierchia1984.controllerRole ControlType.raising = none
• Chierchia1984.controllerRole ControlType.none = none

def Chierchia1984.Blocks (ct : ControlType) (va : Voice) : Prop

The Control Principle blocks a valency alternation that removes the controller from core-term status.

Equations

• Chierchia1984.Blocks ct va = ∃ role ∈ Chierchia1984.controllerRole ct, (va.fateOfRole role).RemovesFromCoreStatus

@[instance_reducible]

instance Chierchia1984.instDecidableBlocks (ct : ControlType) (va : Voice) : Decidable (Blocks ct va)

Equations

• Chierchia1984.instDecidableBlocks ct va = Chierchia1984.instDecidableBlocks._aux_1 ct va

def Chierchia1984.Passivizable (ct : ControlType) : Prop

A control type passivizes when the postulate does not block passivization.

Equations

• Chierchia1984.Passivizable ct = ¬Chierchia1984.Blocks ct Voice.passive

@[instance_reducible]

instance Chierchia1984.instDecidablePredControlTypePassivizable : DecidablePred Passivizable

Equations

• Chierchia1984.instDecidablePredControlTypePassivizable ct = { decide := !decide (Chierchia1984.Blocks ct Voice.passive), reflects_decide := ⋯ }

theorem Chierchia1984.subjectControl_blocks_passive : Blocks ControlType.subjectControl Voice.passive

Visser's generalization at the level of alternations: passivization demotes the agent-like term, which subject control needs.

theorem Chierchia1984.objectControl_passivizable : Passivizable ControlType.objectControl

Passivization keeps the patient-like term, so object control survives it.

theorem Chierchia1984.objectControl_blocks_antipassive : Blocks ControlType.objectControl Voice.antipassive

Bach's generalization at the level of alternations: antipassivization demotes the patient-like term, which object control needs.

theorem Chierchia1984.subjectControl_not_blocks_antipassive : ¬Blocks ControlType.subjectControl Voice.antipassive

Antipassivization keeps the agent-like term, so subject control survives it, promise to come beside promise Bill to come.

The Fragment's control verbs

theorem Chierchia1984.fragment_control_verbs (v : Verb) : v ∈ [English.Verbs.try_.toVerb, English.Verbs.manage.toVerb, English.Verbs.begin_.toVerb, English.Verbs.stop.toVerb, English.Verbs.continue_.toVerb, English.Verbs.fail.toVerb, English.Verbs.persuade.toVerb, English.Verbs.force.toVerb, English.Verbs.want.toVerb, English.Verbs.hope.toVerb, English.Verbs.promise.toVerb] → v.controlType ≠ ControlType.none ∨ v.altControlType ≠ ControlType.none

Every control verb of the Fragment, the attitude verbs want, hope and promise included, is a control verb in the dissertation's sense, with a fixed controller whether subject or object.

theorem Chierchia1984.passivizable_iff (v : Verb) : v ∈ [English.Verbs.try_.toVerb, English.Verbs.persuade.toVerb, English.Verbs.force.toVerb] → (Passivizable v.controlType ↔ v.passivizable = true)

At each Fragment control verb the passivizability the postulate derives agrees with the stored flag: subject control blocks passivization and object control does not.

def Chierchia1984.complementTy (fr : ArgumentFrame) : Option Montague.Ty

The semantic type of a clausal complement: a finite clause denotes a proposition and a nonfinite one a property, the type distinction of chapter I.

Equations

• Chierchia1984.complementTy fr = if fr.HasClausal then some (if fr.HasFinite then Montague.Ty.t else Montague.Ty.et) else none

theorem Chierchia1984.control_complements_property : (∀ v ∈ [English.Verbs.try_.toVerb, English.Verbs.want.toVerb], v.valency.frames.head?.bind complementTy = some Montague.Ty.et) ∧ English.Verbs.believe.valency.frames.head?.bind complementTy = some Montague.Ty.t ∧ English.Verbs.believe.controlType = ControlType.none

Control verbs take property-denoting complements; believe, no control verb, takes a finite clause denoting a proposition.