Italian Tense Fragment

Paradigm entries for Italian tense forms following the TAMEEntry and TensePerspectiveEntry patterns from Fragments/English/Tense.lean.

Italian Tense System

Italian distinguishes five core indicative tenses:

Form	Label	EP	UP	Type
passato prossimo	present perfect	downstream	past	periphrastic
passato remoto	simple past	downstream	past	synthetic
imperfetto	imperfect	downstream	past	synthetic
presente	simple present	downstream	present	synthetic
futuro semplice	simple future	unconstrained	future	synthetic

The passato prossimo / passato remoto distinction is significant: both express past time reference, but they differ in morphological type (periphrastic vs synthetic) and, following [Lak70], in whether they allow false-tense interpretations.

Kratzer Decomposition

The passato prossimo (ho mangiato) parallels English present perfect: PRESENT tense + PERFECT aspect. The auxiliary avere/essere makes the PERF head morphologically transparent.

def Italian.Tense.passatoProssimo : Tense.Evidential.TAMEEntry

Italian passato prossimo (present perfect): ho mangiato 'I have eaten'. [Lak70] EP downstream (T ≤ A), UP past (T < S).

Equations

• Italian.Tense.passatoProssimo = { label := "passato prossimo", ep := Tense.Evidential.EPCondition.downstream, up := Tense.Evidential.UPCondition.past }

def Italian.Tense.passatoRemoto : Tense.Evidential.TAMEEntry

Italian passato remoto (simple past/preterite): mangiai 'I ate'. EP downstream (T ≤ A), UP past (T < S).

Equations

• Italian.Tense.passatoRemoto = { label := "passato remoto", ep := Tense.Evidential.EPCondition.downstream, up := Tense.Evidential.UPCondition.past }

def Italian.Tense.imperfetto : Tense.Evidential.TAMEEntry

Italian imperfetto (imperfect): mangiavo 'I was eating / I used to eat'. EP downstream (T ≤ A), UP past (T < S).

Equations

• Italian.Tense.imperfetto = { label := "imperfetto", ep := Tense.Evidential.EPCondition.downstream, up := Tense.Evidential.UPCondition.past }

def Italian.Tense.presente : Tense.Evidential.TAMEEntry

Italian presente (simple present): mangio 'I eat'. EP downstream (T ≤ A), UP present (T = S).

Equations

• Italian.Tense.presente = { label := "presente", ep := Tense.Evidential.EPCondition.downstream, up := Tense.Evidential.UPCondition.present }

def Italian.Tense.futuroSemplice : Tense.Evidential.TAMEEntry

Italian futuro semplice (simple future): mangerò 'I will eat'. EP unconstrained, UP future (S < T).

Equations

• Italian.Tense.futuroSemplice = { label := "futuro semplice", ep := Tense.Evidential.EPCondition.unconstrained, up := Tense.Evidential.UPCondition.future }

def Italian.Tense.allEntries : List Tense.Evidential.TAMEEntry

All Italian tense paradigm entries.

Equations

• Italian.Tense.allEntries = [Italian.Tense.passatoProssimo, Italian.Tense.passatoRemoto, Italian.Tense.imperfetto, Italian.Tense.presente, Italian.Tense.futuroSemplice]

structure Italian.Tense.TensePerspectiveEntryextends Tense.Evidential.TAMEEntry : Type

A tense paradigm entry enriched with Lakoff's perspective dimensions.

• label : String
• ep : EPCondition
• up : UPCondition
• mood : Option Semantics.Mood.GramMood
• mirative : Option Features.Mirativity.MirativityValue
• gramTense : Finset Ordering

  The grammatical tense this form realizes

• formType : Morphology.Tense.TenseFormType

  Synthetic (inflectional) or periphrastic (auxiliary-based)

def Italian.Tense.TensePerspectiveEntry.allowsFalseTense (e : TensePerspectiveEntry) : Bool

Does this form allow false-tense interpretations? Derived from formType: only synthetic forms can.

Equations

• e.allowsFalseTense = (e.formType == Morphology.Tense.TenseFormType.synthetic)

def Italian.Tense.passatoProssimoPerspective : TensePerspectiveEntry

Passato prossimo: past, periphrastic (avere/essere + past participle).

Equations

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

def Italian.Tense.passatoRemotoPerspective : TensePerspectiveEntry

Passato remoto: past, synthetic.

Equations

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

def Italian.Tense.imperfettoPerspective : TensePerspectiveEntry

Imperfetto: past, synthetic.

Equations

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

def Italian.Tense.presentePerspective : TensePerspectiveEntry

Presente: present, synthetic.

Equations

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

def Italian.Tense.futuroSemplicePerspective : TensePerspectiveEntry

Futuro semplice: future, synthetic.

Equations

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

theorem Italian.Tense.passatoRemoto_allows_false : passatoRemotoPerspective.allowsFalseTense = true

Synthetic forms allow false tense.

theorem Italian.Tense.imperfetto_allows_false : imperfettoPerspective.allowsFalseTense = true

theorem Italian.Tense.presente_allows_false : presentePerspective.allowsFalseTense = true

theorem Italian.Tense.futuro_allows_false : futuroSemplicePerspective.allowsFalseTense = true

theorem Italian.Tense.passatoProssimo_blocks_false : passatoProssimoPerspective.allowsFalseTense = false

Periphrastic forms block false tense.

theorem Italian.Tense.prossimo_remoto_distinction : passatoProssimoPerspective.gramTense = passatoRemotoPerspective.gramTense ∧ passatoProssimoPerspective.formType ≠ passatoRemotoPerspective.formType

Passato prossimo and passato remoto: both past, different formType.

def Italian.Tense.kratzerPassatoProssimo : Tense.SOT.Decomposition.KratzerDecomposition

Italian passato prossimo: Kratzer decomposition. Surface "ho V-to" = PRESENT tense + PERFECT aspect. Parallel to English present perfect — the auxiliary avere/essere makes the PERF head morphologically transparent.

Equations

• Italian.Tense.kratzerPassatoProssimo = { tensePronoun := Tense.SOT.Decomposition.kratzerEnglishPast, hasPerfect := true }

theorem Italian.Tense.kratzerPassatoProssimo_deictic : kratzerPassatoProssimo.canBeDeictic

Italian passato prossimo can be deictic (from decomposition).

theorem Italian.Tense.kratzerPassatoProssimo_underlyingPresent : kratzerPassatoProssimo.tensePronoun.constraint = Tense.present

The underlying tense head is PRESENT, not PAST. Pastness comes from the PERF aspect head.

theorem Italian.Tense.italian_passatoProssimo_is_pres_perf : kratzerPassatoProssimo.tensePronoun = Tense.SOT.Decomposition.kratzerEnglishPast ∧ kratzerPassatoProssimo.hasPerfect = true

Italian passato prossimo shares the same underlying tense pronoun as English present perfect: both use kratzerEnglishPast (PRESENT tense head + indexical mode). The decomposition is PRESENT + PERFECT in both languages.