Bruening (2021): implicit arguments in English double object constructions

An implicit second object of an English double object construction, like an implicit direct object or PP of the prepositional frame, is definite or indefinite as the verb dictates and licenses sluicing; an implicit first object is always definite and never does. Bruening concludes that the verb selects the second object and Appl the first. An argument of the verb is left implicit by a head ∃ or ι adjoined to it, an argument of Appl only by a passive head ApplPass, which binds it as a definite.

An implicit argument here is a diathesis of an English verb leaving a complement of its double object or prepositional frame unexpressed, so the four patterns of the paper's §2.4 are theorems over the whole lexicon.

Main definitions

• Argument.leaveImplicit: the voice leaving an internal argument of a ditransitive implicit.
• observed: the interpretations the lexicon gives an implicit argument.
• Binder, interps, Sluices: the heads that leave an argument implicit, the interpretations they give an argument of each head, and whether it licenses sluicing.

Main results

• observed_firstObject, observed_of_ne_firstObject: an implicit first object is definite, any other implicit argument definite or indefinite.
• interps_eq_observed_iff: these interpretations single out Appl as the head of the first object and the verb as that of the others.
• sluiced_rows: the sluicing judgments of (10) and (11) follow.
• objectDrop_secondObject, dropsInBothFrames: a verb with an implicit transitive object has no implicit second object, and no verb drops its direct object in both frames, except write.

Implementation notes

The fragment places an implicit argument where the construction it is understood in would express it, so an alternating verb's implicit goal is a first object or a PP as its entry says. Semantic types are those of Montague.Ty, in which events share the type e with individuals.

TODO

Appendix A's varieties of definite first objects and Appendix B's verbs with two implicit arguments are not formalized.

References

• [Bru21]
• [Lar88]
• [Mar93]
• [Pes95]
• [Pyl08]

Implicit arguments

inductive Bruening2021.Argument : Type

The internal arguments of a ditransitive, the first and second objects of the double object construction and the direct object and PP of the prepositional frame.

• firstObject : Argument
• secondObject : Argument
• directObject : Argument
• pp : Argument

@[instance_reducible]

instance Bruening2021.instDecidableEqArgument : DecidableEq Argument

Equations

• Bruening2021.instDecidableEqArgument x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Bruening2021.instFintypeArgument : Fintype Argument

Equations

• Bruening2021.instFintypeArgument = { elems := { val := ↑Bruening2021.Argument.enumList, nodup := Bruening2021.Argument.enumList_nodup }, complete := Bruening2021.instFintypeArgument._proof_1 }

@[instance_reducible]

instance Bruening2021.instReprArgument : Repr Argument

Equations

• Bruening2021.instReprArgument = { reprPrec := Bruening2021.instReprArgument.repr }

def Bruening2021.instReprArgument.repr : Argument → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Bruening2021.instReprArgument.repr Bruening2021.Argument.pp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bruening2021.Argument.pp")).group prec✝

def Bruening2021.Argument.leaveImplicit : Argument → ImplicitInterp → Voice

The voice leaving the argument unexpressed in its construction, interpreted as a.

Equations

• Bruening2021.Argument.firstObject.leaveImplicit x✝ = Voice.leaveImplicit ArgumentFrame.np_np 0 (some x✝)
• Bruening2021.Argument.secondObject.leaveImplicit x✝ = Voice.leaveImplicit ArgumentFrame.np_np 1 (some x✝)
• Bruening2021.Argument.directObject.leaveImplicit x✝ = Voice.leaveImplicit ArgumentFrame.np_pp 0 (some x✝)
• Bruening2021.Argument.pp.leaveImplicit x✝ = Voice.leaveImplicit ArgumentFrame.np_pp 1 (some x✝)

def Bruening2021.Argument.ofString? : String → Option Argument

The argument a feature of the examples names.

Equations

• Bruening2021.Argument.ofString? "firstObject" = some Bruening2021.Argument.firstObject
• Bruening2021.Argument.ofString? "secondObject" = some Bruening2021.Argument.secondObject
• Bruening2021.Argument.ofString? "directObject" = some Bruening2021.Argument.directObject
• Bruening2021.Argument.ofString? "pp" = some Bruening2021.Argument.pp
• Bruening2021.Argument.ofString? x✝ = none

def Bruening2021.Argument.host : Argument → Minimalist.Cat

In Bruening's analysis the first object is the argument of Appl, merged in its specifier above the verb phrase, and every other argument is the verb's.

Equations

• Bruening2021.Argument.firstObject.host = Minimalist.Cat.Appl
• x✝.host = Minimalist.Cat.V

def Bruening2021.observed (x : Argument) : Finset ImplicitInterp

The interpretations an implicit argument receives across the English verb lexicon.

Equations

• Bruening2021.observed x = {a : ImplicitInterp | ∃ v ∈ English.Verbs.verbs, v.Alternates (x.leaveImplicit a)}

theorem Bruening2021.observed_firstObject : observed Argument.firstObject = {ImplicitInterp.def}

theorem Bruening2021.observed_of_ne_firstObject {x : Argument} (hx : x ≠ Argument.firstObject) : observed x = {ImplicitInterp.indef, ImplicitInterp.def}

∃, ι, Pass and ApplPass

inductive Bruening2021.Binder : Type

The heads that leave an argument implicit, ∃ and ι adjoined to the verb and the passive heads Pass and ApplPass projecting over Voice and Appl.

• existential : Binder
• iota : Binder
• pass : Binder
• applPass : Binder

@[instance_reducible]

instance Bruening2021.instDecidableEqBinder : DecidableEq Binder

Equations

• Bruening2021.instDecidableEqBinder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Bruening2021.instFintypeBinder : Fintype Binder

Equations

• Bruening2021.instFintypeBinder = { elems := { val := ↑Bruening2021.Binder.enumList, nodup := Bruening2021.Binder.enumList_nodup }, complete := Bruening2021.instFintypeBinder._proof_1 }

def Bruening2021.instReprBinder.repr : Binder → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Bruening2021.instReprBinder.repr Bruening2021.Binder.iota prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bruening2021.Binder.iota")).group prec✝
• Bruening2021.instReprBinder.repr Bruening2021.Binder.pass prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bruening2021.Binder.pass")).group prec✝

@[instance_reducible]

instance Bruening2021.instReprBinder : Repr Binder

Equations

• Bruening2021.instReprBinder = { reprPrec := Bruening2021.instReprBinder.repr }

def Bruening2021.Binder.head : Binder → Minimalist.Cat

The head whose argument the binder closes off.

Equations

• Bruening2021.Binder.existential.head = Minimalist.Cat.V
• Bruening2021.Binder.iota.head = Minimalist.Cat.V
• Bruening2021.Binder.pass.head = Minimalist.Cat.Voice
• Bruening2021.Binder.applPass.head = Minimalist.Cat.Appl

def Bruening2021.Binder.interp : Binder → ImplicitInterp

∃ and Pass bind their argument as an indefinite, ι and ApplPass as a definite.

Equations

• Bruening2021.Binder.existential.interp = ImplicitInterp.indef
• Bruening2021.Binder.pass.interp = ImplicitInterp.indef
• Bruening2021.Binder.iota.interp = ImplicitInterp.def
• Bruening2021.Binder.applPass.interp = ImplicitInterp.def

def Bruening2021.Binder.Projects : Binder → Prop

Pass and ApplPass head phrases of their own; ∃ and ι form a complex head with the verb.

Equations

• Bruening2021.Binder.pass.Projects = True
• Bruening2021.Binder.applPass.Projects = True
• Bruening2021.Binder.existential.Projects = False
• Bruening2021.Binder.iota.Projects = False

@[instance_reducible]

instance Bruening2021.Binder.instDecidablePredProjects : DecidablePred Projects

Equations

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

def Bruening2021.interps (h : Minimalist.Cat) : Finset ImplicitInterp

The interpretations available to an implicit argument of the head h.

Equations

• Bruening2021.interps h = Finset.image Bruening2021.Binder.interp {x : Bruening2021.Binder | x.head = h}

def Bruening2021.Sluices (h : Minimalist.Cat) : Prop

An implicit argument of h licenses sluicing when a binder that does not project can close it off. Ellipsis needs a correlate in the elided clause for every maximal projection of the antecedent, which a sluice has for a head adjoined to the verb but not for PassP or ApplPassP.

Equations

• Bruening2021.Sluices h = ∃ (b : Bruening2021.Binder), b.head = h ∧ ¬b.Projects

@[instance_reducible]

instance Bruening2021.instDecidableSluices (h : Minimalist.Cat) : Decidable (Sluices h)

Equations

• Bruening2021.instDecidableSluices h = { decide := decide (∃ a ∈ Finset.univ, (fun (x : Bruening2021.Binder) => x.head = h ∧ ¬x.Projects) a), reflects_decide := ⋯ }

theorem Bruening2021.interps_eq_observed_iff (x : Argument) (h : Minimalist.Cat) : interps h = observed x ↔ h = x.host

The interpretations an implicit argument shows are those available to an argument of its head, and of no other head. The verb chooses ∃ or ι for its own arguments, so their interpretations vary from verb to verb, while ApplPass alone closes off the first object. An analysis on which the verb selects the first object, as Pesetsky's and Larson's do, predicts indefinite implicit first objects; a small-clause analysis, on which the verb selects neither, predicts no lexical variation in the second.

theorem Bruening2021.sluiced_rows (v : English.Verbs.Verb) : v ∈ English.Verbs.verbs → ArgumentFrame.np_np ∈ v.valency.frames → ∀ row ∈ Examples.all, row.feature? "verb" = some v.form → ∀ (x : Argument), (row.feature? "sluiced").bind Argument.ofString? = some x → (∃ (a : ImplicitInterp), v.Alternates (x.leaveImplicit a)) ∧ (row.judgment = Judgment.acceptable ↔ Sluices x.host)

In (10) and (11) every verb leaves the sluiced argument implicit, and the sluice is acceptable exactly when that argument's head licenses sluicing.

Implicit direct objects

theorem Bruening2021.objectDrop_secondObject : List.map (fun (x : English.Verbs.Verb) => x.form) (List.filter (fun (v : English.Verbs.Verb) => decide ((∃ (a : ImplicitInterp), v.Alternates (Argument.secondObject.leaveImplicit a)) ∧ ∃ (a : ImplicitInterp), v.Alternates (Voice.leaveImplicit ArgumentFrame.np 0 (some a)))) English.Verbs.verbs) = ["write"]

A verb that leaves the object of its transitive frame implicit does not leave the second object of its double object construction implicit, except write, whose She wrote me the paper's fn. 7 suggests is a prepositional frame with a silent preposition.

theorem Bruening2021.melt_build (v : English.Verbs.Verb) : v ∈ [English.Verbs.melt, English.Verbs.build] → (∃ (a : ImplicitInterp), v.Alternates (Voice.leaveImplicit ArgumentFrame.np 0 (some a))) ∧ ArgumentFrame.np_np ∈ v.valency.frames

melt and build, the base transitives of (7) and (8), leave their object implicit and have a double object construction.

theorem Bruening2021.tyBinary_appl : HeimKratzer.Tree.tyBinary (Montague.Ty.eet ⇒ Montague.Ty.e ⇒ Montague.Ty.e ⇒ Montague.Ty.et) Montague.Ty.eet = some (Montague.Ty.e ⇒ Montague.Ty.e ⇒ Montague.Ty.et) ∧ HeimKratzer.Tree.tyBinary (Montague.Ty.eet ⇒ Montague.Ty.e ⇒ Montague.Ty.e ⇒ Montague.Ty.et) Montague.Ty.et = none

Appl takes a verb with an open individual argument, of type ⟨e,⟨s,t⟩⟩, then the theme, the recipient and the event, so a verb whose object ∃ has closed off, of type ⟨s,t⟩, cannot combine with it: a simple transitive's implicit object is not available in the double object construction.

theorem Bruening2021.dropsInBothFrames : List.map (fun (x : English.Verbs.Verb) => x.form) (List.filter (fun (v : English.Verbs.Verb) => decide ((∃ (a : ImplicitInterp), v.Alternates (Argument.secondObject.leaveImplicit a)) ∧ ∃ (a : ImplicitInterp), v.Alternates (Argument.directObject.leaveImplicit a))) English.Verbs.verbs) = ["write"]

No verb but write leaves its direct object implicit both in the double object and in the prepositional frame.

theorem Bruening2021.implicit_rows (v : English.Verbs.Verb) : v ∈ English.Verbs.verbs → ArgumentFrame.np_np ∈ v.valency.frames → ∀ row ∈ Examples.all, row.feature? "verb" = some v.form → ∀ (x : Argument), (row.feature? "implicit").bind Argument.ofString? = some x → (row.judgment = Judgment.acceptable ↔ ∃ (a : ImplicitInterp), v.Alternates (x.leaveImplicit a))

In (63)–(65) a double object verb leaves its direct object implicit beside a first object or beside a PP exactly as the example is acceptable. The fragment has no double object frame for ask, email, text or telegraph.