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 @cite{lakoff-1970}, 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 Fragments.Italian.Tense.passatoProssimo : Semantics.Tense.Evidential.TAMEEntry

Italian passato prossimo (present perfect): ho mangiato 'I have eaten'. @cite{lakoff-1970} EP downstream (T ≤ A), UP past (T < S).

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

All Italian tense paradigm entries.

Equations

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

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

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

• label : String
• ep : EPCondition
• up : UPCondition
• mood : Option Core.Discourse.GramMood
• mirative : Option Core.Evidence.MirativityValue
• gramTense : Core.Tense.GramTense

  The grammatical tense this form realizes

• formType : Core.Morphology.Tense.TenseFormType

  Synthetic (inflectional) or periphrastic (auxiliary-based)

def Fragments.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 == Core.Morphology.Tense.TenseFormType.synthetic)

def Fragments.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 Fragments.Italian.Tense.passatoRemotoPerspective : TensePerspectiveEntry

Passato remoto: past, synthetic.

Equations

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

def Fragments.Italian.Tense.imperfettoPerspective : TensePerspectiveEntry

Imperfetto: past, synthetic.

Equations

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

def Fragments.Italian.Tense.presentePerspective : TensePerspectiveEntry

Presente: present, synthetic.

Equations

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

def Fragments.Italian.Tense.futuroSemplicePerspective : TensePerspectiveEntry

Futuro semplice: future, synthetic.

Equations

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

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

Synthetic forms allow false tense.

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

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

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

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

Periphrastic forms block false tense.

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

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

def Fragments.Italian.Tense.kratzerPassatoProssimo : Semantics.Tense.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

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

theorem Fragments.Italian.Tense.kratzerPassatoProssimo_deictic : kratzerPassatoProssimo.canBeDeictic = true

Italian passato prossimo can be deictic (from decomposition).

theorem Fragments.Italian.Tense.kratzerPassatoProssimo_underlyingPresent : kratzerPassatoProssimo.tensePronoun.constraint = Core.Tense.GramTense.present

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

theorem Fragments.Italian.Tense.italian_passatoProssimo_is_pres_perf : kratzerPassatoProssimo.tensePronoun = Semantics.Tense.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.