Be/Have Auxiliary Selection in European Perfects

@cite{burzio-1986} @cite{sorace-2000}

Many European languages select between be and have as the perfect auxiliary based on the transitivity/unaccusativity of the lexical verb. The canonical "Auxiliary Selection Hierarchy":

• Unaccusative verbs → be (Italian è arrivato, French est arrivé)
• Unergative/transitive verbs → have (Italian ha mangiato, French a mangé)

English has collapsed this distinction: all verbs take have.

Bridge to Aspect

Vendler's achievement class (telic, punctual) correlates with unaccusativity: canonical achievements (arrive, die, fall) are unaccusative and select be in split-auxiliary languages.

Types

inductive Phenomena.AuxiliaryVerbs.Selection.PerfectAux : Type

Perfect auxiliary choice.

• be : PerfectAux
• have : PerfectAux

instance Phenomena.AuxiliaryVerbs.Selection.instDecidableEqPerfectAux : DecidableEq PerfectAux

Equations

• Phenomena.AuxiliaryVerbs.Selection.instDecidableEqPerfectAux x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.AuxiliaryVerbs.Selection.instReprPerfectAux.repr : PerfectAux → Nat → Std.Format

Equations

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

instance Phenomena.AuxiliaryVerbs.Selection.instReprPerfectAux : Repr PerfectAux

Equations

• Phenomena.AuxiliaryVerbs.Selection.instReprPerfectAux = { reprPrec := Phenomena.AuxiliaryVerbs.Selection.instReprPerfectAux.repr }

instance Phenomena.AuxiliaryVerbs.Selection.instBEqPerfectAux : BEq PerfectAux

Equations

• Phenomena.AuxiliaryVerbs.Selection.instBEqPerfectAux = { beq := Phenomena.AuxiliaryVerbs.Selection.instBEqPerfectAux.beq }

def Phenomena.AuxiliaryVerbs.Selection.instBEqPerfectAux.beq : PerfectAux → PerfectAux → Bool

Equations

• Phenomena.AuxiliaryVerbs.Selection.instBEqPerfectAux.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive Phenomena.AuxiliaryVerbs.Selection.TransitivityClass : Type

Transitivity class relevant to auxiliary selection.

• unaccusative : TransitivityClass
• unergative : TransitivityClass
• transitive : TransitivityClass
• reflexive : TransitivityClass

instance Phenomena.AuxiliaryVerbs.Selection.instDecidableEqTransitivityClass : DecidableEq TransitivityClass

Equations

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

instance Phenomena.AuxiliaryVerbs.Selection.instReprTransitivityClass : Repr TransitivityClass

Equations

• Phenomena.AuxiliaryVerbs.Selection.instReprTransitivityClass = { reprPrec := Phenomena.AuxiliaryVerbs.Selection.instReprTransitivityClass.repr }

def Phenomena.AuxiliaryVerbs.Selection.instReprTransitivityClass.repr : TransitivityClass → Nat → Std.Format

Equations

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

instance Phenomena.AuxiliaryVerbs.Selection.instBEqTransitivityClass : BEq TransitivityClass

Equations

• Phenomena.AuxiliaryVerbs.Selection.instBEqTransitivityClass = { beq := Phenomena.AuxiliaryVerbs.Selection.instBEqTransitivityClass.beq }

def Phenomena.AuxiliaryVerbs.Selection.instBEqTransitivityClass.beq : TransitivityClass → TransitivityClass → Bool

Equations

• Phenomena.AuxiliaryVerbs.Selection.instBEqTransitivityClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive Phenomena.AuxiliaryVerbs.Selection.SelectionRule : Type

Language-level auxiliary selection rule.

• split : SelectionRule
• haveOnly : SelectionRule
• beOnly : SelectionRule
• mixed : SelectionRule

instance Phenomena.AuxiliaryVerbs.Selection.instDecidableEqSelectionRule : DecidableEq SelectionRule

Equations

• Phenomena.AuxiliaryVerbs.Selection.instDecidableEqSelectionRule x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.AuxiliaryVerbs.Selection.instReprSelectionRule.repr : SelectionRule → Nat → Std.Format

Equations

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

instance Phenomena.AuxiliaryVerbs.Selection.instReprSelectionRule : Repr SelectionRule

Equations

• Phenomena.AuxiliaryVerbs.Selection.instReprSelectionRule = { reprPrec := Phenomena.AuxiliaryVerbs.Selection.instReprSelectionRule.repr }

instance Phenomena.AuxiliaryVerbs.Selection.instBEqSelectionRule : BEq SelectionRule

Equations

• Phenomena.AuxiliaryVerbs.Selection.instBEqSelectionRule = { beq := Phenomena.AuxiliaryVerbs.Selection.instBEqSelectionRule.beq }

def Phenomena.AuxiliaryVerbs.Selection.instBEqSelectionRule.beq : SelectionRule → SelectionRule → Bool

Equations

• Phenomena.AuxiliaryVerbs.Selection.instBEqSelectionRule.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Functions

def Phenomena.AuxiliaryVerbs.Selection.canonicalSelection : TransitivityClass → PerfectAux

Canonical auxiliary selection (Burzio's generalization, Romance pattern): unaccusatives and reflexives → be, everything else → have.

NB: This models the Romance pattern (Italian, French). German differs: reflexives take haben (e.g., hat sich gewaschen 'has REFL washed'), not sein. For German-specific selection, see germanSelection.

Equations

• Phenomena.AuxiliaryVerbs.Selection.canonicalSelection Phenomena.AuxiliaryVerbs.Selection.TransitivityClass.unaccusative = Phenomena.AuxiliaryVerbs.Selection.PerfectAux.be
• Phenomena.AuxiliaryVerbs.Selection.canonicalSelection Phenomena.AuxiliaryVerbs.Selection.TransitivityClass.unergative = Phenomena.AuxiliaryVerbs.Selection.PerfectAux.have
• Phenomena.AuxiliaryVerbs.Selection.canonicalSelection Phenomena.AuxiliaryVerbs.Selection.TransitivityClass.transitive = Phenomena.AuxiliaryVerbs.Selection.PerfectAux.have
• Phenomena.AuxiliaryVerbs.Selection.canonicalSelection Phenomena.AuxiliaryVerbs.Selection.TransitivityClass.reflexive = Phenomena.AuxiliaryVerbs.Selection.PerfectAux.be

def Phenomena.AuxiliaryVerbs.Selection.germanSelection : TransitivityClass → PerfectAux

German auxiliary selection: differs from Romance in that reflexives take haben, not sein (@cite{burzio-1986}).

Equations

• Phenomena.AuxiliaryVerbs.Selection.germanSelection Phenomena.AuxiliaryVerbs.Selection.TransitivityClass.unaccusative = Phenomena.AuxiliaryVerbs.Selection.PerfectAux.be
• Phenomena.AuxiliaryVerbs.Selection.germanSelection Phenomena.AuxiliaryVerbs.Selection.TransitivityClass.reflexive = Phenomena.AuxiliaryVerbs.Selection.PerfectAux.have
• Phenomena.AuxiliaryVerbs.Selection.germanSelection x✝ = Phenomena.AuxiliaryVerbs.Selection.PerfectAux.have

def Phenomena.AuxiliaryVerbs.Selection.selectsBe : TransitivityClass → Bool

Does this transitivity class canonically select be?

Equations

• Phenomena.AuxiliaryVerbs.Selection.selectsBe Phenomena.AuxiliaryVerbs.Selection.TransitivityClass.unaccusative = true
• Phenomena.AuxiliaryVerbs.Selection.selectsBe Phenomena.AuxiliaryVerbs.Selection.TransitivityClass.reflexive = true
• Phenomena.AuxiliaryVerbs.Selection.selectsBe x✝ = false

Data

structure Phenomena.AuxiliaryVerbs.Selection.AuxSelectionDatum : Type

A cross-linguistic auxiliary selection datum.

• language : String
• selectionRule : SelectionRule
• exampleVerb : String
• transitivityClass : TransitivityClass
• selectedAux : PerfectAux
• gloss : String

def Phenomena.AuxiliaryVerbs.Selection.instReprAuxSelectionDatum.repr : AuxSelectionDatum → Nat → Std.Format

Equations

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

instance Phenomena.AuxiliaryVerbs.Selection.instReprAuxSelectionDatum : Repr AuxSelectionDatum

Equations

• Phenomena.AuxiliaryVerbs.Selection.instReprAuxSelectionDatum = { reprPrec := Phenomena.AuxiliaryVerbs.Selection.instReprAuxSelectionDatum.repr }

def Phenomena.AuxiliaryVerbs.Selection.instBEqAuxSelectionDatum.beq : AuxSelectionDatum → AuxSelectionDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.AuxiliaryVerbs.Selection.instBEqAuxSelectionDatum.beq x✝¹ x✝ = false

instance Phenomena.AuxiliaryVerbs.Selection.instBEqAuxSelectionDatum : BEq AuxSelectionDatum

Equations

• Phenomena.AuxiliaryVerbs.Selection.instBEqAuxSelectionDatum = { beq := Phenomena.AuxiliaryVerbs.Selection.instBEqAuxSelectionDatum.beq }

def Phenomena.AuxiliaryVerbs.Selection.italianArrivare : AuxSelectionDatum

Italian arrivare (arrive) — unaccusative, selects essere (@cite{burzio-1986}).

Equations

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

def Phenomena.AuxiliaryVerbs.Selection.italianMangiare : AuxSelectionDatum

Italian mangiare (eat) — transitive, selects avere (@cite{burzio-1986}).

Equations

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

def Phenomena.AuxiliaryVerbs.Selection.frenchArriver : AuxSelectionDatum

French arriver (arrive) — unaccusative, selects être (@cite{burzio-1986}).

Equations

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

def Phenomena.AuxiliaryVerbs.Selection.germanAnkommen : AuxSelectionDatum

German ankommen (arrive) — unaccusative, selects sein (@cite{burzio-1986}).

Equations

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

def Phenomena.AuxiliaryVerbs.Selection.dutchAankomen : AuxSelectionDatum

Dutch aankomen (arrive) — unaccusative, selects zijn (@cite{sorace-2000}).

Equations

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

def Phenomena.AuxiliaryVerbs.Selection.englishArrive : AuxSelectionDatum

English arrive — have-only system, canonical split is collapsed.

Equations

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

def Phenomena.AuxiliaryVerbs.Selection.allData : List AuxSelectionDatum

Equations

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

Theorems

theorem Phenomena.AuxiliaryVerbs.Selection.unaccusative_selects_be : canonicalSelection TransitivityClass.unaccusative = PerfectAux.be

Unaccusatives canonically select be.

theorem Phenomena.AuxiliaryVerbs.Selection.transitive_selects_have : canonicalSelection TransitivityClass.transitive = PerfectAux.have

Transitives canonically select have.

theorem Phenomena.AuxiliaryVerbs.Selection.italian_arrivare_matches_canonical : canonicalSelection italianArrivare.transitivityClass = italianArrivare.selectedAux

Italian arrivare matches the canonical pattern.

theorem Phenomena.AuxiliaryVerbs.Selection.english_breaks_canonical : canonicalSelection englishArrive.transitivityClass ≠ englishArrive.selectedAux

English arrive breaks the canonical pattern (have-only system).

theorem Phenomena.AuxiliaryVerbs.Selection.german_reflexive_takes_have : germanSelection TransitivityClass.reflexive = PerfectAux.have

German reflexives take haben, not sein — unlike Romance.

theorem Phenomena.AuxiliaryVerbs.Selection.romance_reflexive_takes_be : canonicalSelection TransitivityClass.reflexive = PerfectAux.be

Romance reflexives take be (canonical pattern).

theorem Phenomena.AuxiliaryVerbs.Selection.german_romance_agree_on_unaccusative : germanSelection TransitivityClass.unaccusative = canonicalSelection TransitivityClass.unaccusative

German and Romance agree on unaccusatives (both select be).