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

@[implicit_reducible]

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 → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.AuxiliaryVerbs.Selection.instReprPerfectAux : Repr PerfectAux

Equations

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

inductive Phenomena.AuxiliaryVerbs.Selection.TransitivityClass : Type

Transitivity class relevant to auxiliary selection.

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

@[implicit_reducible]

instance Phenomena.AuxiliaryVerbs.Selection.instDecidableEqTransitivityClass : DecidableEq TransitivityClass

Equations

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

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

Equations

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

@[implicit_reducible]

instance Phenomena.AuxiliaryVerbs.Selection.instReprTransitivityClass : Repr TransitivityClass

Equations

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

inductive Phenomena.AuxiliaryVerbs.Selection.SelectionRule : Type

Language-level auxiliary selection rule.

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

@[implicit_reducible]

instance Phenomena.AuxiliaryVerbs.Selection.instDecidableEqSelectionRule : DecidableEq SelectionRule

Equations

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

@[implicit_reducible]

instance Phenomena.AuxiliaryVerbs.Selection.instReprSelectionRule : Repr SelectionRule

Equations

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

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

Equations

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

Functions

def Phenomena.AuxiliaryVerbs.Selection.selection (reflexIsBe : Bool) : TransitivityClass → PerfectAux

Auxiliary selection driven by a single binary parameter: does the language treat reflexives as BE-selecting (Romance pattern) or HAVE-selecting (German pattern)? Unaccusatives always select BE, unergatives and transitives always select HAVE; the only point of cross-linguistic variation in this small typology is the reflexive row (@cite{burzio-1986}, @cite{sorace-2000}).

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.AuxiliaryVerbs.Selection.selection reflexIsBe Phenomena.AuxiliaryVerbs.Selection.TransitivityClass.unaccusative = Phenomena.AuxiliaryVerbs.Selection.PerfectAux.be
• Phenomena.AuxiliaryVerbs.Selection.selection reflexIsBe Phenomena.AuxiliaryVerbs.Selection.TransitivityClass.unergative = Phenomena.AuxiliaryVerbs.Selection.PerfectAux.have
• Phenomena.AuxiliaryVerbs.Selection.selection reflexIsBe Phenomena.AuxiliaryVerbs.Selection.TransitivityClass.transitive = Phenomena.AuxiliaryVerbs.Selection.PerfectAux.have

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

Canonical (Romance) auxiliary selection: reflexives → be.

Equations

• Phenomena.AuxiliaryVerbs.Selection.canonicalSelection = Phenomena.AuxiliaryVerbs.Selection.selection true

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

German auxiliary selection: reflexives → haben, not sein (@cite{burzio-1986}).

Equations

• Phenomena.AuxiliaryVerbs.Selection.germanSelection = Phenomena.AuxiliaryVerbs.Selection.selection false

def Phenomena.AuxiliaryVerbs.Selection.SelectsBe (c : TransitivityClass) : Prop

Does this transitivity class canonically select be? Defined off canonicalSelection so the equivalence is true by construction.

Equations

• Phenomena.AuxiliaryVerbs.Selection.SelectsBe c = (Phenomena.AuxiliaryVerbs.Selection.canonicalSelection c = Phenomena.AuxiliaryVerbs.Selection.PerfectAux.be)

@[implicit_reducible]

instance Phenomena.AuxiliaryVerbs.Selection.instDecidablePredTransitivityClassSelectsBe : DecidablePred SelectsBe

Equations

• Phenomena.AuxiliaryVerbs.Selection.instDecidablePredTransitivityClassSelectsBe c = id inferInstance

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

@[implicit_reducible]

instance Phenomena.AuxiliaryVerbs.Selection.instReprAuxSelectionDatum : Repr AuxSelectionDatum

Equations

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

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

Equations

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

@[implicit_reducible]

instance Phenomena.AuxiliaryVerbs.Selection.instBEqAuxSelectionDatum : BEq AuxSelectionDatum

Equations

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

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

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.english_breaks_canonical : canonicalSelection englishArrive.transitivityClass ≠ englishArrive.selectedAux

English arrive breaks the canonical pattern: the verb is unaccusative yet the language has a have-only perfect system, so the canonical Romance prediction (.be) and the actually-selected auxiliary (.have) disagree. This is the data point worth stating as a theorem; the other previously-listed equalities all reduce to rfl over the selection lookup table and have been removed.