Turkish Tense-Aspect-Modality System

@cite{goksel-kerslake-2005}

The TAM system is the core of the Turkish verbal paradigm (@cite{goksel-kerslake-2005} Ch 21, Appendix 2). There are five basic TAM categories and three modal categories, occupying a single paradigmatic slot.

Key properties

1. Evidential -mIş is a TAM marker, not a separate evidential morpheme. It fills the same paradigmatic slot as -DI (past definite) and cannot co-occur with it.

2. Aorist negation is asymmetric: affirmative -(I)r becomes negative -mAz rather than the expected *-mA-(I)r. All other categories use regular -mA- negation (see also Fragments.Turkish.Negation).

3. Compound tenses are formed by adding a copular suffix (-DI, -mIş, -(y)sA) to the basic form: geliyordu (progressive + past copula).

Suffix notation

Capital letters indicate vowel harmony alternation (see Fragments.Turkish.VowelHarmony):

• A = a/e (twofold), I = ı/i/u/ü (fourfold)
• D = d/t (voicing assimilation)

inductive Fragments.Turkish.TAM.TAMCategory : Type

The eight TAM categories of Turkish.

• pastDef : TAMCategory
• evidential : TAMCategory
• aorist : TAMCategory
• progressive : TAMCategory
• future : TAMCategory
• conditional : TAMCategory
• optative : TAMCategory
• necessitative : TAMCategory

@[implicit_reducible]

instance Fragments.Turkish.TAM.instDecidableEqTAMCategory : DecidableEq TAMCategory

Equations

• Fragments.Turkish.TAM.instDecidableEqTAMCategory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.Turkish.TAM.instReprTAMCategory : Repr TAMCategory

Equations

• Fragments.Turkish.TAM.instReprTAMCategory = { reprPrec := Fragments.Turkish.TAM.instReprTAMCategory.repr }

def Fragments.Turkish.TAM.instReprTAMCategory.repr : TAMCategory → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Turkish.TAM.instInhabitedTAMCategory : Inhabited TAMCategory

Equations

• Fragments.Turkish.TAM.instInhabitedTAMCategory = { default := Fragments.Turkish.TAM.instInhabitedTAMCategory.default }

def Fragments.Turkish.TAM.instInhabitedTAMCategory.default : TAMCategory

Equations

• Fragments.Turkish.TAM.instInhabitedTAMCategory.default = Fragments.Turkish.TAM.TAMCategory.pastDef

structure Fragments.Turkish.TAM.TAMEntry : Type

TAM suffix entry with positive and negative forms.

• category : TAMCategory
• affSuffix : String
• negSuffix : String
• isNegSymmetric : Bool

  Is negation symmetric (neg = stem + -mA- + TAM)?

def Fragments.Turkish.TAM.instReprTAMEntry.repr : TAMEntry → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Turkish.TAM.instReprTAMEntry : Repr TAMEntry

Equations

• Fragments.Turkish.TAM.instReprTAMEntry = { reprPrec := Fragments.Turkish.TAM.instReprTAMEntry.repr }

@[implicit_reducible]

instance Fragments.Turkish.TAM.instBEqTAMEntry : BEq TAMEntry

Equations

• Fragments.Turkish.TAM.instBEqTAMEntry = { beq := Fragments.Turkish.TAM.instBEqTAMEntry.beq }

def Fragments.Turkish.TAM.instBEqTAMEntry.beq : TAMEntry → TAMEntry → Bool

Equations

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

@[implicit_reducible]

instance Fragments.Turkish.TAM.instInhabitedTAMEntry : Inhabited TAMEntry

Equations

• Fragments.Turkish.TAM.instInhabitedTAMEntry = { default := Fragments.Turkish.TAM.instInhabitedTAMEntry.default }

def Fragments.Turkish.TAM.instInhabitedTAMEntry.default : TAMEntry

Equations

• Fragments.Turkish.TAM.instInhabitedTAMEntry.default = { category := default, affSuffix := default, negSuffix := default, isNegSymmetric := default }

def Fragments.Turkish.TAM.entries : List TAMEntry

Equations

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

inductive Fragments.Turkish.TAM.CopulaSuffix : Type

Copular suffixes that combine with basic TAM for compound tenses.

• pastCop : CopulaSuffix
• evidentialCop : CopulaSuffix
• conditionalCop : CopulaSuffix

@[implicit_reducible]

instance Fragments.Turkish.TAM.instDecidableEqCopulaSuffix : DecidableEq CopulaSuffix

Equations

• Fragments.Turkish.TAM.instDecidableEqCopulaSuffix x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.Turkish.TAM.instReprCopulaSuffix : Repr CopulaSuffix

Equations

• Fragments.Turkish.TAM.instReprCopulaSuffix = { reprPrec := Fragments.Turkish.TAM.instReprCopulaSuffix.repr }

def Fragments.Turkish.TAM.instReprCopulaSuffix.repr : CopulaSuffix → Nat → Std.Format

Equations

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

theorem Fragments.Turkish.TAM.entry_count : entries.length = 8

theorem Fragments.Turkish.TAM.one_asymmetric : (List.filter (fun (x : TAMEntry) => !x.isNegSymmetric) entries).length = 1

Exactly one TAM category has asymmetric negation.

theorem Fragments.Turkish.TAM.asymmetric_is_aorist : ((List.filter (fun (x : TAMEntry) => !x.isNegSymmetric) entries).head!.category == TAMCategory.aorist) = true

The asymmetric category is the aorist.

theorem Fragments.Turkish.TAM.non_aorist_symmetric : ((List.filter (fun (e : TAMEntry) => e.category != TAMCategory.aorist) entries).all fun (x : TAMEntry) => x.isNegSymmetric) = true

All non-aorist categories use regular -mA- negation.

theorem Fragments.Turkish.TAM.tam_negation_aorist_agreement : ((List.filter (fun (x : TAMEntry) => !x.isNegSymmetric) entries).head!.category == TAMCategory.aorist) = true ∧ (List.filter (fun (e : Negation.NegParadigmEntry) => !e.symmetric) Negation.gelParadigm).head!.formLabel = "aorist"

Cross-file bridge: TAM and Negation agree that the aorist is asymmetric. TAM: asymmetric_is_aorist, Negation: aorist_asymmetric.