Italian Modal Auxiliaries

[Hac10] [Cin04] [Hac06] [Riz78]

Italian modal auxiliaries dovere ('must') and potere ('can'), with their behavior under restructuring. These are the primary empirical evidence for [Hac06]'s event-relative analysis: when Italian modals appear in restructuring configurations (syntactically low, below AspP), they lose epistemic readings.

Italian Restructuring

Italian potere and dovere participate in restructuring. In restructuring contexts, the modal is syntactically low — merged below AspP, with the lower verb's clitic climbing through the modal. Diagnostics:

1. Clitic climbing: lo posso fare ('it I-can do') — clitic lo climbs past the modal (restructuring) vs posso farlo (non-restructuring).
2. Auxiliary selection: è dovuto andare (auxiliary essere with unaccusative andare) — auxiliary matches the lower verb (restructuring) vs ha dovuto andare (non-restructuring, default avere).

When restructured (low): only root readings (circumstantial, deontic). When non-restructured (high): epistemic readings available.

structure Italian.Modals.ItalianModalEntry : Type

An Italian modal auxiliary entry with position-sensitive flavor.

• form : String

  Citation form

• force : Semantics.Modality.ModalForce

  Modal force (necessity or possibility)

• canRestructure : Bool

  Whether the modal can restructure (appear below AspP)

• highFlavors : List Semantics.Modality.ModalFlavor

  Flavors available when non-restructured (high position)

• lowFlavors : List Semantics.Modality.ModalFlavor

  Flavors available when restructured (low position)

def Italian.Modals.instReprItalianModalEntry.repr : ItalianModalEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Italian.Modals.instReprItalianModalEntry : Repr ItalianModalEntry

Equations

• Italian.Modals.instReprItalianModalEntry = { reprPrec := Italian.Modals.instReprItalianModalEntry.repr }

def Italian.Modals.instBEqItalianModalEntry.beq : ItalianModalEntry → ItalianModalEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Italian.Modals.instBEqItalianModalEntry.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Italian.Modals.instBEqItalianModalEntry : BEq ItalianModalEntry

Equations

• Italian.Modals.instBEqItalianModalEntry = { beq := Italian.Modals.instBEqItalianModalEntry.beq }

def Italian.Modals.potere : ItalianModalEntry

Potere ('can'): restructuring modal. High: epistemic, deontic, circumstantial. Low (restructured): deontic, circumstantial only.

[Riz78]; [Hac06], Ch. 4:

• "Gianni può essere intelligente" (epistemic, non-restructured)
• "Gianni lo può fare" (root, restructured — clitic climbing)

Equations

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

def Italian.Modals.dovere : ItalianModalEntry

Dovere ('must'): restructuring modal. High: epistemic, deontic, circumstantial. Low (restructured): deontic, circumstantial only.

[Riz78]; [Hac06], Ch. 4:

• "Gianni deve essere a casa" (epistemic, non-restructured)
• "Gianni deve lavorare" (deontic/circumstantial, restructured)

Equations

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

inductive Italian.Modals.RestructuringDiagnostic : Type

Restructuring diagnostics from [Riz78].

• cliticClimbing : RestructuringDiagnostic

  Clitic climbing: clitic raises past the modal to the higher verb

• auxiliaryChange : RestructuringDiagnostic

  Auxiliary change: auxiliary of the lower verb surfaces on the modal

@[implicit_reducible]

instance Italian.Modals.instDecidableEqRestructuringDiagnostic : DecidableEq RestructuringDiagnostic

Equations

• Italian.Modals.instDecidableEqRestructuringDiagnostic x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Italian.Modals.instReprRestructuringDiagnostic.repr : RestructuringDiagnostic → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Italian.Modals.instReprRestructuringDiagnostic : Repr RestructuringDiagnostic

Equations

• Italian.Modals.instReprRestructuringDiagnostic = { reprPrec := Italian.Modals.instReprRestructuringDiagnostic.repr }

structure Italian.Modals.RestructuringExample : Type

A restructuring example: sentence + diagnostic + reading.

• italian : String

  Italian sentence

• gloss : String

  English gloss

• isRestructured : Bool

  Whether the modal is restructured

• diagnostic : Option RestructuringDiagnostic

  Which diagnostic evidences restructuring

• availableFlavors : List Semantics.Modality.ModalFlavor

  The modal reading(s) available

def Italian.Modals.instReprRestructuringExample.repr : RestructuringExample → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Italian.Modals.instReprRestructuringExample : Repr RestructuringExample

Equations

• Italian.Modals.instReprRestructuringExample = { reprPrec := Italian.Modals.instReprRestructuringExample.repr }

def Italian.Modals.potere_high : RestructuringExample

Non-restructured potere — epistemic. "Gianni può essere intelligente" = Gianni may be intelligent. No clitic climbing; epistemic reading available. [Hac06], Ch. 4.

Equations

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

def Italian.Modals.potere_low_clitic : RestructuringExample

Restructured potere — root only. "Lo posso fare" = I can do it (clitic climbing). Clitic climbing diagnoses low position; epistemic unavailable. [Riz78]; [Hac06], Ch. 4.

Equations

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

def Italian.Modals.dovere_high : RestructuringExample

Non-restructured dovere — epistemic. "Gianni deve essere a casa" = Gianni must be at home. Epistemic necessity. [Hac06], Ch. 4.

Equations

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

def Italian.Modals.dovere_low_aux : RestructuringExample

Restructured dovere — deontic/root only. "È dovuto andare a casa" = He had to go home. Auxiliary change (essere from unaccusative andare). [Riz78]; [Hac06], Ch. 4.

Equations

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

def Italian.Modals.allExamples : List RestructuringExample

Equations

• Italian.Modals.allExamples = [Italian.Modals.potere_high, Italian.Modals.potere_low_clitic, Italian.Modals.dovere_high, Italian.Modals.dovere_low_aux]

theorem Italian.Modals.high_has_epistemic : List.elem Semantics.Modality.ModalFlavor.epistemic potere_high.availableFlavors = true ∧ List.elem Semantics.Modality.ModalFlavor.epistemic dovere_high.availableFlavors = true

Non-restructured examples have epistemic as a flavor.

theorem Italian.Modals.low_lacks_epistemic : List.elem Semantics.Modality.ModalFlavor.epistemic potere_low_clitic.availableFlavors = false ∧ List.elem Semantics.Modality.ModalFlavor.epistemic dovere_low_aux.availableFlavors = false

Restructured examples lack epistemic as a flavor.

theorem Italian.Modals.restructuring_blocks_epistemic : (allExamples.all fun (ex : RestructuringExample) => if ex.isRestructured = true then !List.elem Semantics.Modality.ModalFlavor.epistemic ex.availableFlavors else List.elem Semantics.Modality.ModalFlavor.epistemic ex.availableFlavors) = true

The core generalization: restructured ↔ no epistemic.

theorem Italian.Modals.potere_flavors_match_position : Semantics.Modality.ModalFlavor.epistemic ∈ potere.highFlavors ∧ Semantics.Modality.ModalFlavor.epistemic ∉ potere.lowFlavors

The entry's position-sensitive flavors match EventRelativity's content licensing predictions.

theorem Italian.Modals.dovere_flavors_match_position : Semantics.Modality.ModalFlavor.epistemic ∈ dovere.highFlavors ∧ Semantics.Modality.ModalFlavor.epistemic ∉ dovere.lowFlavors