Italian Modal Auxiliaries

@cite{hacquard-2010} @cite{cinque-2004} @cite{hacquard-2006} @cite{rizzi-1978}

Italian modal auxiliaries dovere ('must') and potere ('can'), with their behavior under restructuring. These are the primary empirical evidence for @cite{hacquard-2006}'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 Fragments.Italian.Modals.ItalianModalEntry : Type

An Italian modal auxiliary entry with position-sensitive flavor.

• form : String

  Citation form

• force : Core.Modality.ModalForce

  Modal force (necessity or possibility)

• canRestructure : Bool

  Whether the modal can restructure (appear below AspP)

• highFlavors : List Core.Modality.ModalFlavor

  Flavors available when non-restructured (high position)

• lowFlavors : List Core.Modality.ModalFlavor

  Flavors available when restructured (low position)

instance Fragments.Italian.Modals.instReprItalianModalEntry : Repr ItalianModalEntry

Equations

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

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

Equations

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

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

Equations

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

instance Fragments.Italian.Modals.instBEqItalianModalEntry : BEq ItalianModalEntry

Equations

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

def Fragments.Italian.Modals.potere : ItalianModalEntry

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

@cite{rizzi-1978}; @cite{hacquard-2006}, 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 Fragments.Italian.Modals.dovere : ItalianModalEntry

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

@cite{rizzi-1978}; @cite{hacquard-2006}, 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 Fragments.Italian.Modals.RestructuringDiagnostic : Type

Restructuring diagnostics from @cite{rizzi-1978}.

• 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

instance Fragments.Italian.Modals.instDecidableEqRestructuringDiagnostic : DecidableEq RestructuringDiagnostic

Equations

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

def Fragments.Italian.Modals.instBEqRestructuringDiagnostic.beq : RestructuringDiagnostic → RestructuringDiagnostic → Bool

Equations

• Fragments.Italian.Modals.instBEqRestructuringDiagnostic.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Italian.Modals.instBEqRestructuringDiagnostic : BEq RestructuringDiagnostic

Equations

• Fragments.Italian.Modals.instBEqRestructuringDiagnostic = { beq := Fragments.Italian.Modals.instBEqRestructuringDiagnostic.beq }

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

Equations

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

instance Fragments.Italian.Modals.instReprRestructuringDiagnostic : Repr RestructuringDiagnostic

Equations

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

structure Fragments.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 Core.Modality.ModalFlavor

  The modal reading(s) available

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

Equations

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

instance Fragments.Italian.Modals.instReprRestructuringExample : Repr RestructuringExample

Equations

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

def Fragments.Italian.Modals.potere_high : RestructuringExample

Non-restructured potere — epistemic. "Gianni può essere intelligente" = Gianni may be intelligent. No clitic climbing; epistemic reading available. @cite{hacquard-2006}, Ch. 4.

Equations

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

def Fragments.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. @cite{rizzi-1978}; @cite{hacquard-2006}, Ch. 4.

Equations

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

def Fragments.Italian.Modals.dovere_high : RestructuringExample

Non-restructured dovere — epistemic. "Gianni deve essere a casa" = Gianni must be at home. Epistemic necessity. @cite{hacquard-2006}, Ch. 4.

Equations

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

def Fragments.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). @cite{rizzi-1978}; @cite{hacquard-2006}, Ch. 4.

Equations

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

def Fragments.Italian.Modals.allExamples : List RestructuringExample

Equations

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

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

Non-restructured examples have epistemic as a flavor.

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

Restructured examples lack epistemic as a flavor.

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

The core generalization: restructured ↔ no epistemic.

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

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

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