Turkish Negation Fragment

@cite{miestamo-2005} @cite{haspelmath-2013} @cite{dryer-haspelmath-2013}

Turkish expresses standard negation with the verbal suffix -mA- (/-ma-/ or /-me-/ depending on vowel harmony). The suffix is inserted between the verb stem and the TAM suffix.

SymAsy: Symmetric and Asymmetric

Most constructions are symmetric: -mA- inserts without further change. But the aorist is asymmetric (A/Cat): the affirmative aorist marker -(I)r is replaced by -z in the negative.

Construction	Affirmative	Negative	Symmetric?
Progressive	gel-iyor	gel-m-iyor	Yes
Past definite	gel-di	gel-me-di	Yes
Future	gel-ecek	gel-me-yecek	Yes
Evidential	gel-miş	gel-me-miş	Yes
Aorist	gel-ir	gel-me-z	No

The aorist asymmetry is a paradigmatic change: a different morphological marker appears, not just insertion of the negative morpheme.

def Fragments.Turkish.Negation.negSuffix : Typology.Negation.NegMarkerEntry

-mA- — Turkish's negative verbal suffix (underlying form). Surfaces as -ma- (back-vowel stems) or -me- (front-vowel stems) by vowel harmony. Inserted between the verb stem and the TAM suffix: gel-iyor → gel-m-iyor (come-NEG-PROG). The form here is the abstract citation form; the harmony-conditioned alternants are captured by the language's morphology layer, not the marker entry.

Equations

• Fragments.Turkish.Negation.negSuffix = { form := "-mA-", morphemeType := Typology.Negation.NegMorphemeType.affix, position := Typology.Negation.NegMarkerPosition.morphological }

def Fragments.Turkish.Negation.negationSystem : Typology.Negation.NegationSystem

The Turkish negation system: a single verbal affix. The Fragment-side joint consumed by Phenomena/Negation/Studies/Dryer2013.lean.

Equations

• Fragments.Turkish.Negation.negationSystem = Typology.Negation.NegationSystem.ofISO "tur" [Fragments.Turkish.Negation.negSuffix]

structure Fragments.Turkish.Negation.NegParadigmEntry : Type

A Turkish negation paradigm entry.

• formLabel : String
• affirmative : String
• negative : String
• glossAff : String
• glossNeg : String
• symmetric : Bool

  Is this construction symmetric (neg = aff + neg marker, no other change)?

@[implicit_reducible]

instance Fragments.Turkish.Negation.instReprNegParadigmEntry : Repr NegParadigmEntry

Equations

• Fragments.Turkish.Negation.instReprNegParadigmEntry = { reprPrec := Fragments.Turkish.Negation.instReprNegParadigmEntry.repr }

def Fragments.Turkish.Negation.instReprNegParadigmEntry.repr : NegParadigmEntry → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Turkish.Negation.instBEqNegParadigmEntry : BEq NegParadigmEntry

Equations

• Fragments.Turkish.Negation.instBEqNegParadigmEntry = { beq := Fragments.Turkish.Negation.instBEqNegParadigmEntry.beq }

def Fragments.Turkish.Negation.instBEqNegParadigmEntry.beq : NegParadigmEntry → NegParadigmEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.Turkish.Negation.instBEqNegParadigmEntry.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Fragments.Turkish.Negation.instInhabitedNegParadigmEntry : Inhabited NegParadigmEntry

Equations

• Fragments.Turkish.Negation.instInhabitedNegParadigmEntry = { default := Fragments.Turkish.Negation.instInhabitedNegParadigmEntry.default }

def Fragments.Turkish.Negation.instInhabitedNegParadigmEntry.default : NegParadigmEntry

Equations

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

def Fragments.Turkish.Negation.gelParadigm : List NegParadigmEntry

Paradigm for gelmek 'come' (3sg forms).

Equations

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

Verification

theorem Fragments.Turkish.Negation.gel_paradigm_size : gelParadigm.length = 5

theorem Fragments.Turkish.Negation.mostly_symmetric : (List.filter (fun (x : NegParadigmEntry) => x.symmetric) gelParadigm).length = 4

Most constructions are symmetric.

theorem Fragments.Turkish.Negation.aorist_asymmetric : (List.filter (fun (e : NegParadigmEntry) => !e.symmetric) gelParadigm).length = 1 ∧ (List.filter (fun (e : NegParadigmEntry) => !e.symmetric) gelParadigm).head!.formLabel = "aorist"

The aorist is the only asymmetric construction.

theorem Fragments.Turkish.Negation.aorist_different_markers : have aor := (List.filter (fun (x : NegParadigmEntry) => x.formLabel == "aorist") gelParadigm).head!; Fragments.Turkish.Negation.hasSubstr✝ aor.affirmative "ir" = true ∧ Fragments.Turkish.Negation.hasSubstr✝ aor.negative "ez" = true

The aorist negative marker -z differs from the affirmative -r: this is paradigmatic asymmetry (A/Cat).

def Fragments.Turkish.Negation.negationProfile : Typology.Negation.NegationProfile

Turkish negation profile (WALS Ch 112-115 + Greco/JinKoenig fields).

Equations

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