Negative Auxiliaries

@cite{anderson-2006} @cite{miestamo-2005}

Some languages express sentential negation through a negative auxiliary verb that hosts inflection (tense, agreement) while the lexical verb appears in a nonfinite form. This is a special case of the aux-headed AVC pattern.

Cross-linguistic strategies

Strategy	Structure	Example
NegVerb	Inflected neg aux + nonfinite LV	Finnish ei mene 'NEG.3SG go'
NegAffix	Bound negative morpheme	Kwerba or-, Tswana ga/se
NegParticle	Free negative particle	English not, Italian non

The neg-verb strategy is particularly interesting because the negative element is itself an auxiliary verb, creating an AVC with the negative verb as inflectional head.

Types

inductive Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.NegStrategy : Type

Strategy for expressing sentential negation.

• negVerb : NegStrategy

  Negative auxiliary verb that inflects (Finnish ei, Komi oz).

• negAffix : NegStrategy

  Bound negative morpheme (Kwerba or- prefix, Tswana ga/se).

• negParticle : NegStrategy

  Free negative particle (English not).

instance Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.instDecidableEqNegStrategy : DecidableEq NegStrategy

Equations

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

def Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.instReprNegStrategy.repr : NegStrategy → ℕ → Std.Format

Equations

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

instance Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.instReprNegStrategy : Repr NegStrategy

Equations

• Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.instReprNegStrategy = { reprPrec := Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.instReprNegStrategy.repr }

def Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.instBEqNegStrategy.beq : NegStrategy → NegStrategy → Bool

Equations

• Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.instBEqNegStrategy.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.instBEqNegStrategy : BEq NegStrategy

Equations

• Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.instBEqNegStrategy = { beq := Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.instBEqNegStrategy.beq }

Functions

def Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.NegStrategy.expectedInflPattern : NegStrategy → Option Typology.InflPattern

A negative verb creates an AVC and therefore has an expected inflectional pattern: aux-headed (the neg verb hosts inflection). Affixes and particles do not create AVCs.

Equations

• Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.NegStrategy.negVerb.expectedInflPattern = some Phenomena.AuxiliaryVerbs.Typology.InflPattern.auxHeaded
• Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.NegStrategy.negAffix.expectedInflPattern = none
• Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.NegStrategy.negParticle.expectedInflPattern = none

def Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.NegStrategy.isVerbal : NegStrategy → Bool

Is this strategy verbal (i.e., does it create an AVC)?

Equations

• Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.NegStrategy.negVerb.isVerbal = true
• x✝.isVerbal = false

Data

structure Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.NegAuxDatum : Type

A negative auxiliary datum.

• language : String
• strategy : NegStrategy
• form : String
• gloss : String

def Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.instReprNegAuxDatum.repr : NegAuxDatum → ℕ → Std.Format

Equations

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

instance Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.instReprNegAuxDatum : Repr NegAuxDatum

Equations

• Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.instReprNegAuxDatum = { reprPrec := Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.instReprNegAuxDatum.repr }

def Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.instBEqNegAuxDatum.beq : NegAuxDatum → NegAuxDatum → Bool

Equations

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

instance Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.instBEqNegAuxDatum : BEq NegAuxDatum

Equations

• Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.instBEqNegAuxDatum = { beq := Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.instBEqNegAuxDatum.beq }

def Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.finnish : NegAuxDatum

Finnish ei — negative auxiliary verb (inflects for person/number). The 3sg citation form derives from Fragments.Finnish.Negation.negParadigm.

Equations

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

def Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.komi : NegAuxDatum

Komi oz — negative auxiliary verb (@cite{anderson-2006}).

Equations

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

def Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.udihe : NegAuxDatum

Udihe e-si — negative auxiliary verb (past tense on neg aux) (@cite{anderson-2006}).

Equations

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

def Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.kwerba : NegAuxDatum

Kwerba or- — negative affix (prefix on verb) (@cite{anderson-2006}).

Equations

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

def Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.tswana : NegAuxDatum

Tswana ga/se — negative affixes (preverbal bound morphemes in the Bantu verbal complex; ga in indicative, se in subjunctive/hortative).

Equations

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

def Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.englishNot : NegAuxDatum

English not — negative particle (does not create an AVC).

Equations

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

def Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.italianNon : NegAuxDatum

Italian non — preverbal negative particle (symmetric negation). Form derived from Fragments.Italian.Negation.negMarker.

Equations

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

def Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.allData : List NegAuxDatum

Equations

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

Theorems

theorem Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.negVerb_implies_auxHeaded : NegStrategy.negVerb.expectedInflPattern = some Typology.InflPattern.auxHeaded

Negative verbs create aux-headed AVCs.

theorem Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.negAffix_no_avc : NegStrategy.negAffix.expectedInflPattern = none

Negative affixes do not create AVCs.

theorem Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.negParticle_no_avc : NegStrategy.negParticle.expectedInflPattern = none

Negative particles do not create AVCs.

Per-datum verification

theorem Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.finnish_is_negVerb : finnish.strategy = NegStrategy.negVerb

theorem Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.komi_is_negVerb : komi.strategy = NegStrategy.negVerb

theorem Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.udihe_is_negVerb : udihe.strategy = NegStrategy.negVerb

theorem Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.kwerba_is_negAffix : kwerba.strategy = NegStrategy.negAffix

theorem Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.tswana_is_negAffix : tswana.strategy = NegStrategy.negAffix

theorem Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.english_is_negParticle : englishNot.strategy = NegStrategy.negParticle

theorem Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.italian_is_negParticle : italianNon.strategy = NegStrategy.negParticle

Bridge to Finnish Fragment

theorem Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.finnish_form_from_fragment : finnish.form = "ei"

The Finnish negative auxiliary form derives from the Fragment paradigm.

Bridge to Italian Fragment

theorem Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.italian_form_from_fragment : italianNon.form = Fragments.Italian.Negation.negMarker

The Italian negative particle form derives from the Fragment negation marker.

Bridge to Negation Typology (WALS Ch 112)

NegStrategy in this file and NegMorphemeType in Phenomena.Negation.Typology classify the same dimension — the morphological status of the negative marker. This bridge maps between them.

def Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.NegStrategy.toNegMorphemeType : NegStrategy → Negation.Typology.NegMorphemeType

Map from AVC-oriented NegStrategy to WALS-oriented NegMorphemeType.

Equations

• Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.NegStrategy.negVerb.toNegMorphemeType = Phenomena.Negation.Typology.NegMorphemeType.auxVerb
• Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.NegStrategy.negAffix.toNegMorphemeType = Phenomena.Negation.Typology.NegMorphemeType.affix
• Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.NegStrategy.negParticle.toNegMorphemeType = Phenomena.Negation.Typology.NegMorphemeType.particle

theorem Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.negVerb_maps_to_auxVerb : NegStrategy.negVerb.toNegMorphemeType = Negation.Typology.NegMorphemeType.auxVerb

theorem Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.negAffix_maps_to_affix : NegStrategy.negAffix.toNegMorphemeType = Negation.Typology.NegMorphemeType.affix

theorem Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.negParticle_maps_to_particle : NegStrategy.negParticle.toNegMorphemeType = Negation.Typology.NegMorphemeType.particle