Turkish Negation Fragment

@cite{miestamo-2005} @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 : String

The Turkish negative verbal suffix (underlying form). Surfaces as -ma- or -me- by vowel harmony.

Equations

• Fragments.Turkish.Negation.negSuffix = "-mA-"

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)?

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

Equations

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

instance Fragments.Turkish.Negation.instReprNegParadigmEntry : Repr NegParadigmEntry

Equations

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

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

instance Fragments.Turkish.Negation.instBEqNegParadigmEntry : BEq NegParadigmEntry

Equations

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

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.negSuffix_is_mA : negSuffix = "-mA-"

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).