Turkish Negation Fragment

[Mie05] [Has13b] [DH13a]

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 Turkish.Negation.negSuffix : Syntax.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

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

def Turkish.Negation.negationSystem : Syntax.Negation.NegationSystem

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

Equations

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

structure 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 Turkish.Negation.instReprNegParadigmEntry : Repr NegParadigmEntry

Equations

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

def Turkish.Negation.instReprNegParadigmEntry.repr : NegParadigmEntry → ℕ → Std.Format

Equations

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

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

Equations

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

@[implicit_reducible]

instance Turkish.Negation.instBEqNegParadigmEntry : BEq NegParadigmEntry

Equations

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

@[implicit_reducible]

instance Turkish.Negation.instInhabitedNegParadigmEntry : Inhabited NegParadigmEntry

Equations

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

def 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 Turkish.Negation.gel_paradigm_size : gelParadigm.length = 5

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

Most constructions are symmetric.

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

def Turkish.Negation.negationProfile : Syntax.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.