Perfect-auxiliary selection (be/have)

Many Romance and Germanic languages form the perfect with either be or have, and the choice tracks split intransitivity. The binary account, Burzio's for Italian, has unaccusatives and reflexives take be (Italian è arrivato, French est arrivé) and unergatives and transitives have (Italian ha mangiato); German and Dutch reflexives take have (Sorace §1). Sorace refines the intransitives into the Auxiliary Selection Hierarchy, a chain of seven aspectual and thematic verb types along which the preference for be falls: the verbs at the two ends choose their auxiliary categorically and in every language, the verbs between them vary, and each language draws its cutoff between be and have at its own point. The inflectional typology of auxiliary verb constructions lives in Syntax/Category/Auxiliary/Constructions.lean.

Main definitions

• TransitivityClass and its selection, canonicalSelection and SelectsBe: the binary account.
• AuxiliarySelectionHierarchy: the verb types of the Auxiliary Selection Hierarchy, a bounded linear order with the type most consistent in taking be at the bottom.
• AuxiliarySelectionHierarchy.ofVerb: the type of a verb entry, read off its aspect, its direction of motion and its subject's volition.

References

• [Bur86]
• [Sor00]
• [LRH95]

inductive ArgumentStructure.TransitivityClass : Type

Transitivity class relevant to auxiliary selection.

• unaccusative : TransitivityClass

  The subject is the theme, as of arrive, fall and die.

• unergative : TransitivityClass

  The subject is an agent and there is no object, as with run and laugh.

• transitive : TransitivityClass

  The subject is an agent and the object a theme, as with eat and build.

• reflexive : TransitivityClass

  A reflexive clitic, which selects be in Romance and have in German.

@[instance_reducible]

instance ArgumentStructure.instDecidableEqTransitivityClass : DecidableEq TransitivityClass

Equations

• ArgumentStructure.instDecidableEqTransitivityClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ArgumentStructure.instReprTransitivityClass : Repr TransitivityClass

Equations

• ArgumentStructure.instReprTransitivityClass = { reprPrec := ArgumentStructure.instReprTransitivityClass.repr }

def ArgumentStructure.instReprTransitivityClass.repr : TransitivityClass → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ArgumentStructure.instFintypeTransitivityClass : Fintype TransitivityClass

Equations

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

def ArgumentStructure.TransitivityClass.selection (refl : Verb.PerfectAuxiliary) : TransitivityClass → Verb.PerfectAuxiliary

In the binary account of auxiliary selection, given the auxiliary of reflexives, unaccusatives select be, unergatives and transitives have, and reflexives are the locus of variation, be in Romance and have in German ([Bur86] for the Italian generalization).

Equations

• ArgumentStructure.TransitivityClass.selection refl ArgumentStructure.TransitivityClass.unaccusative = Verb.PerfectAuxiliary.be
• ArgumentStructure.TransitivityClass.selection refl ArgumentStructure.TransitivityClass.reflexive = refl
• ArgumentStructure.TransitivityClass.selection refl ArgumentStructure.TransitivityClass.unergative = Verb.PerfectAuxiliary.have
• ArgumentStructure.TransitivityClass.selection refl ArgumentStructure.TransitivityClass.transitive = Verb.PerfectAuxiliary.have

def ArgumentStructure.TransitivityClass.canonicalSelection : TransitivityClass → Verb.PerfectAuxiliary

Canonical (Romance) auxiliary selection gives reflexives be.

Equations

• ArgumentStructure.TransitivityClass.canonicalSelection = ArgumentStructure.TransitivityClass.selection Verb.PerfectAuxiliary.be

def ArgumentStructure.TransitivityClass.SelectsBe (c : TransitivityClass) : Prop

Does this transitivity class canonically select be?

Equations

• c.SelectsBe = (c.canonicalSelection = Verb.PerfectAuxiliary.be)

@[instance_reducible]

instance ArgumentStructure.TransitivityClass.instDecidablePredSelectsBe : DecidablePred SelectsBe

Equations

• c.instDecidablePredSelectsBe = ArgumentStructure.TransitivityClass.instDecidablePredSelectsBe._aux_1 c

inductive ArgumentStructure.AuxiliarySelectionHierarchy : Type

The Auxiliary Selection Hierarchy ([Sor00], Table 1) orders the aspectual and thematic types of monadic intransitive verbs from the type most consistent in taking be to the type most consistent in taking have. The transitions and states come first, by decreasing telicity, then the processes, by increasing control. The two ends are the core types, whose verbs choose their auxiliary categorically.

• changeOfLocation : AuxiliarySelectionHierarchy

  A telic change of location, as arrive, come and fall denote.

• changeOfState : AuxiliarySelectionHierarchy

  A change of state, mostly without a specified endpoint, as rise, rot, become and die denote.

• continuationOfState : AuxiliarySelectionHierarchy

  The continuation of a pre-existing state, as stay, remain, last and survive denote.

• existenceOfState : AuxiliarySelectionHierarchy

  The existence of a state, as be, exist, belong and seem denote.

• uncontrolledProcess : AuxiliarySelectionHierarchy

  A process without volition, as tremble, cough, verbs of emission and weather verbs denote.

• motionalProcess : AuxiliarySelectionHierarchy

  A controlled process of motion, whose agent undergoes an undirected displacement, as run, swim and walk denote.

• nonmotionalProcess : AuxiliarySelectionHierarchy

  A controlled process without motion, which leaves its agent unaffected, as work, play and talk denote.

@[instance_reducible]

instance ArgumentStructure.instDecidableEqAuxiliarySelectionHierarchy : DecidableEq AuxiliarySelectionHierarchy

Equations

• ArgumentStructure.instDecidableEqAuxiliarySelectionHierarchy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ArgumentStructure.instReprAuxiliarySelectionHierarchy.repr : AuxiliarySelectionHierarchy → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ArgumentStructure.instReprAuxiliarySelectionHierarchy : Repr AuxiliarySelectionHierarchy

Equations

• ArgumentStructure.instReprAuxiliarySelectionHierarchy = { reprPrec := ArgumentStructure.instReprAuxiliarySelectionHierarchy.repr }

@[instance_reducible]

instance ArgumentStructure.instFintypeAuxiliarySelectionHierarchy : Fintype AuxiliarySelectionHierarchy

Equations

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

@[instance_reducible]

instance ArgumentStructure.AuxiliarySelectionHierarchy.instLinearOrder : LinearOrder AuxiliarySelectionHierarchy

The types are ordered as they are listed.

Equations

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

@[instance_reducible]

instance ArgumentStructure.AuxiliarySelectionHierarchy.instBoundedOrder : BoundedOrder AuxiliarySelectionHierarchy

Equations

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

The type of a verb entry

def ArgumentStructure.AuxiliarySelectionHierarchy.ofVerb (v : Verb) : Option AuxiliarySelectionHierarchy

The type of a monadic verb, read off its entry ([Sor00] §§3–4). A state is the continuation of a state when the entry is phasal continuation, as remain is, and the existence of one otherwise. A telic verb is a change of location when it lexicalizes a direction of motion and a change of state otherwise. An atelic dynamic verb is a change of state when it measures change along a scale, as rise does; a motional process when it displaces its theme; and otherwise a nonmotional or an uncontrolled process, as its subject is volitional or not. none when the entry lacks the Vendler class, or a process lacks the subject profile.

Equations

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

theorem ArgumentStructure.AuxiliarySelectionHierarchy.ofVerb_withPath_eq_bot {v : Verb} {p : Adposition.SpatialReading} (hv : v.TakesSpatial) (hd : p.direction ≠ Spatial.Path.Direction.place) (hb : p.IsBounded) {c : Aspect.VendlerClass} (hc : v.vendlerClass = some c) (hdyn : c.dynamicity = Aspect.Dynamicity.dynamic) : ofVerb (v.withPath p) = some ⊥

A bounded directional phrase makes a dynamic verb that selects one a change of location, the bottom of the hierarchy: the directed motion use in which verbs of manner of motion take be ([Sor00] §4.3, [LRH95] p. 185).