Olivier (2026): Agree in Restructuring

This file formalizes the account of auxiliary switch in [Oli26]. Auxiliary switch, BE in place of HAVE on a modal in a compound tense whose infinitive is unaccusative or reflexive — is ordinary auxiliary selection across a transparent restructuring domain. Auxiliary selection itself is not driven by argument structure: a person value carries the referential identity of its bearer, Voice's valued φ-set is redistributed by head splitting onto vAux[uPers] and VoicePrt[uGen, uNum], and the Vocabulary Items insert BE when [vAux + T] carry the same identity, HAVE elsewhere — so unaccusatives and bound reflexives take BE and transitives HAVE. In a restructuring clause the auxiliary belongs to the modal, and whether Voice(*) KEEPs its φ-features or SHAREs them with vMOD decides clitic climbing and the switch at once: KEEP leaves vAux featureless, HAVE; SHARE brings the bound reflexive's identity — the subject's — to vAux, BE. Prepositional clitics (y/ci, en/ne, lui/gli) climb without a switch since they introduce no coreferential person value, and a vAux that also probes the internal argument gives the Italian and Sardinian speakers' BE. Out of scope: conditions 1–2, which the restructuring structure presupposes; gender and number on the participle; impersonal si; the corpus counts. The simple compound tense is compound and the restructuring one Restructuring.matrixAux.

References

• [Oli26]
• [Oli25] — person-identity auxiliary selection (§6.2)
• [Oua08] — the KEEP and SHARE transfers

Person values with identity

structure Olivier2026.IndexedPerson : Type

[Person: X [ID: α]] (54): a person value with the referential index of its bearer; two values match for the Vocabulary Items (55) when their indices agree.

• person : Person
• id : ℕ

def Olivier2026.instDecidableEqIndexedPerson.decEq (x✝ x✝¹ : IndexedPerson) : Decidable (x✝ = x✝¹)

Equations

• Olivier2026.instDecidableEqIndexedPerson.decEq { person := a, id := a_1 } { person := b, id := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Olivier2026.instDecidableEqIndexedPerson : DecidableEq IndexedPerson

Equations

• Olivier2026.instDecidableEqIndexedPerson = Olivier2026.instDecidableEqIndexedPerson.decEq

@[instance_reducible]

instance Olivier2026.instReprIndexedPerson : Repr IndexedPerson

Equations

• Olivier2026.instReprIndexedPerson = { reprPrec := Olivier2026.instReprIndexedPerson.repr }

def Olivier2026.instReprIndexedPerson.repr : IndexedPerson → ℕ → Std.Format

Equations

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

inductive Olivier2026.Clitic : Type

The clitics the paper distinguishes: the reflexive se/si, bound by the external argument through Voice* and so sharing its identity (54b), (60); the accusative le/lo and dative lui/gli, with identities of their own; the locative y/ci and partitive en/ne, which value a P-feature and carry no coreferential person (§7.3); and (65)'s je ne m'aurais pas foutu dehors, a reflexive whose identity is not its binder's (§6.2.3).

• reflexive : Clitic
• detachedReflexive : Clitic
• accusative : Clitic
• dative : Clitic
• locative : Clitic
• partitive : Clitic

@[instance_reducible]

instance Olivier2026.instDecidableEqClitic : DecidableEq Clitic

Equations

• Olivier2026.instDecidableEqClitic x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Olivier2026.instReprClitic : Repr Clitic

Equations

• Olivier2026.instReprClitic = { reprPrec := Olivier2026.instReprClitic.repr }

def Olivier2026.instReprClitic.repr : Clitic → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Olivier2026.instReprClitic.repr Olivier2026.Clitic.dative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Olivier2026.Clitic.dative")).group prec✝

@[instance_reducible]

instance Olivier2026.instFintypeClitic : Fintype Clitic

Equations

• Olivier2026.instFintypeClitic = { elems := { val := ↑Olivier2026.Clitic.enumList, nodup := Olivier2026.Clitic.enumList_nodup }, complete := Olivier2026.instFintypeClitic._proof_1 }

def Olivier2026.Clitic.prepositional : Clitic → Bool

The "prepositional" clitics of §3.2.2 — locative, partitive and non-reflexive dative — which pronominalise PP-constituents and never introduce the subject's identity.

Equations

• Olivier2026.Clitic.locative.prepositional = true
• Olivier2026.Clitic.partitive.prepositional = true
• Olivier2026.Clitic.dative.prepositional = true
• x✝.prepositional = false

structure Olivier2026.Clause : Type

A clause by the class of its verb and its clitic, if any.

• verb : ArgumentStructure.TransitivityClass
• clitic : Option Clitic

@[instance_reducible]

instance Olivier2026.instDecidableEqClause : DecidableEq Clause

Equations

• Olivier2026.instDecidableEqClause = Olivier2026.instDecidableEqClause.decEq

def Olivier2026.instDecidableEqClause.decEq (x✝ x✝¹ : Clause) : Decidable (x✝ = x✝¹)

Equations

• Olivier2026.instDecidableEqClause.decEq { verb := a, clitic := a_1 } { verb := b, clitic := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Olivier2026.instReprClause.repr : Clause → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Olivier2026.instReprClause : Repr Clause

Equations

• Olivier2026.instReprClause = { reprPrec := Olivier2026.instReprClause.repr }

def Olivier2026.externalArg (ea : Person) : IndexedPerson

The external argument's value carries index 0, the internal argument's 1, and any other bearer's — a cognate object (fn. 26), a detached reflexive — 2.

Equations

• Olivier2026.externalArg ea = { person := ea, id := 0 }

def Olivier2026.internalArg (ia : Person) : IndexedPerson

The internal argument's value.

Equations

• Olivier2026.internalArg ia = { person := ia, id := 1 }

def Olivier2026.voicePerson (ea ia : Person) : Clause → IndexedPerson

The person/identity Voice(*) comes to bear after probing (58)–(61): the internal argument's for unaccusatives and transitives (a DP or an accusative clitic), the bound reflexive's — the external argument's identity — for reflexive verbs (60), the identity of its own for a detached reflexive (65), and a default value for the cognate object of unergatives (fn. 26).

Equations

• Olivier2026.voicePerson ea ia { verb := ArgumentStructure.TransitivityClass.unaccusative, clitic := clitic } = Olivier2026.internalArg ia
• Olivier2026.voicePerson ea ia { verb := ArgumentStructure.TransitivityClass.transitive, clitic := clitic } = Olivier2026.internalArg ia
• Olivier2026.voicePerson ea ia { verb := ArgumentStructure.TransitivityClass.reflexive, clitic := some Olivier2026.Clitic.detachedReflexive } = { person := ea, id := 2 }
• Olivier2026.voicePerson ea ia { verb := ArgumentStructure.TransitivityClass.reflexive, clitic := clitic } = Olivier2026.externalArg ea
• Olivier2026.voicePerson ea ia { verb := ArgumentStructure.TransitivityClass.unergative, clitic := clitic } = { person := Person.third, id := 2 }

def Olivier2026.tPerson (ea ia : Person) : ArgumentStructure.TransitivityClass → IndexedPerson

T's person/identity: the external argument's, or the raised internal argument's for unaccusatives (59).

Equations

• Olivier2026.tPerson ea ia ArgumentStructure.TransitivityClass.unaccusative = Olivier2026.internalArg ia
• Olivier2026.tPerson ea ia x✝ = Olivier2026.externalArg ea

def Olivier2026.insert (vAux : Option IndexedPerson) (t : IndexedPerson) : Verb.PerfectAuxiliary

Vocabulary Items (55): BE when vAux and T carry the same identity, HAVE elsewhere — HAVE is the default auxiliary.

Equations

• Olivier2026.insert vAux t = if Option.map (fun (x : Olivier2026.IndexedPerson) => x.id) vAux = some t.id then Verb.PerfectAuxiliary.be else Verb.PerfectAuxiliary.have

Simple compound tenses (§6.2.2)

def Olivier2026.compound (ea ia : Person) (cl : Clause) : Verb.PerfectAuxiliary

The auxiliary of a simple compound tense (58): Voice splits, so vAux carries Voice's person/identity, and T carries the subject's.

Equations

• Olivier2026.compound ea ia cl = Olivier2026.insert (some (Olivier2026.voicePerson ea ia cl)) (Olivier2026.tPerson ea ia cl.verb)

theorem Olivier2026.compound_eq_canonical (ea ia : Person) (c : ArgumentStructure.TransitivityClass) : compound ea ia { verb := c } = c.canonicalSelection

(59)–(61): identity matching yields the canonical distribution — BE with unaccusatives and reflexives, HAVE with transitives and unergatives — for every pair of persons.

Restructuring clauses (§5, §7)

inductive Olivier2026.TransferStyle : Type

The transfer of Voice()'s φ-features to vMOD (45), after [Oua08]: KEEP leaves them on Voice(), SHARE puts them on vMOD as well. Ouali's third operation, DONATE, plays no role in the paper.

• keep : TransferStyle
• share : TransferStyle

@[instance_reducible]

instance Olivier2026.instDecidableEqTransferStyle : DecidableEq TransferStyle

Equations

• Olivier2026.instDecidableEqTransferStyle x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Olivier2026.instReprTransferStyle.repr : TransferStyle → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Olivier2026.instReprTransferStyle : Repr TransferStyle

Equations

• Olivier2026.instReprTransferStyle = { reprPrec := Olivier2026.instReprTransferStyle.repr }

structure Olivier2026.Restructuring : Type

A modal in a compound tense over an infinitive (40): the embedded clause, whether Voice(*) KEEPs its φ-features or SHAREs them with vMOD (45), and whether a vAux that receives a prepositional clitic's P-feature also receives the internal argument's person (§7.3's "rich" vAux).

• embedded : Clause
• transfer : TransferStyle
• richAux : Bool

def Olivier2026.instDecidableEqRestructuring.decEq (x✝ x✝¹ : Restructuring) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Olivier2026.instDecidableEqRestructuring : DecidableEq Restructuring

Equations

• Olivier2026.instDecidableEqRestructuring = Olivier2026.instDecidableEqRestructuring.decEq

@[instance_reducible]

instance Olivier2026.instReprRestructuring : Repr Restructuring

Equations

• Olivier2026.instReprRestructuring = { reprPrec := Olivier2026.instReprRestructuring.repr }

def Olivier2026.instReprRestructuring.repr : Restructuring → ℕ → Std.Format

Equations

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

def Olivier2026.Restructuring.climbs (r : Restructuring) : Prop

A clitic climbs iff its φ-features are shared upwards — it spells out on the head that bears them (45), clitic reduplication showing the copies (41)–(44).

Equations

• r.climbs = (r.embedded.clitic.isSome = true ∧ r.transfer = Olivier2026.TransferStyle.share)

@[instance_reducible]

instance Olivier2026.instDecidableClimbs (r : Restructuring) : Decidable r.climbs

Equations

• Olivier2026.instDecidableClimbs r = { decide := decide (r.embedded.clitic.isSome = true) && decide (r.transfer = Olivier2026.TransferStyle.share), reflects_decide := ⋯ }

def Olivier2026.Restructuring.vAuxPerson (ea ia : Person) (r : Restructuring) : Option IndexedPerson

The person/identity vAux receives after splitting vMOD: nothing under KEEP (69), (74); under SHARE, Voice's — unless a prepositional clitic climbed to a "poor" vAux, which then carries only its P-feature (§7.3).

Equations

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

def Olivier2026.Restructuring.matrixAux (ea ia : Person) (r : Restructuring) : Verb.PerfectAuxiliary

The modal's auxiliary.

Equations

• Olivier2026.Restructuring.matrixAux ea ia r = Olivier2026.insert (Olivier2026.Restructuring.vAuxPerson ea ia r) (Olivier2026.tPerson ea ia r.embedded.verb)

def Olivier2026.Restructuring.Switch (ea ia : Person) (r : Restructuring) : Prop

Auxiliary Switch: the modal surfaces with BE.

Equations

• Olivier2026.Restructuring.Switch ea ia r = (Olivier2026.Restructuring.matrixAux ea ia r = Verb.PerfectAuxiliary.be)

@[instance_reducible]

instance Olivier2026.instDecidableSwitch (ea ia : Person) (r : Restructuring) : Decidable (Restructuring.Switch ea ia r)

Equations

• Olivier2026.instDecidableSwitch ea ia r = Olivier2026.instDecidableSwitch._aux_1 ea ia r

theorem Olivier2026.keep_have (ea ia : Person) (r : Restructuring) (h : r.transfer = TransferStyle.keep) : Restructuring.matrixAux ea ia r = Verb.PerfectAuxiliary.have ∧ ¬r.climbs

(69), (74): under KEEP vAux is featureless, so the modal takes HAVE and no clitic climbs.

theorem Olivier2026.share_switch_iff_selectsBe (ea ia : Person) (c : ArgumentStructure.TransitivityClass) (cl : Option Clitic) (hcl : cl ≠ some Clitic.detachedReflexive) (hp : (Option.map Clitic.prepositional cl).getD false = false) (rich : Bool) : Restructuring.Switch ea ia { embedded := { verb := c, clitic := cl }, transfer := TransferStyle.share, richAux := rich } ↔ c.SelectsBe

Condition 3 derived: under SHARE, with no prepositional clitic, the modal switches to BE exactly when the infinitive is a BE-selecting predicate (71), (76) versus (61) — the identity vAux inherits is T's iff Voice probed the subject's bearer.

theorem Olivier2026.reflexive_switch_iff_climbs (ea ia : Person) (t : TransferStyle) (rich : Bool) : Restructuring.Switch ea ia { embedded := { verb := ArgumentStructure.TransitivityClass.reflexive, clitic := some Clitic.reflexive }, transfer := t, richAux := rich } ↔ { embedded := { verb := ArgumentStructure.TransitivityClass.reflexive, clitic := some Clitic.reflexive }, transfer := t, richAux := rich }.climbs

Condition α and Table 1: with a reflexive infinitive, AS obtains exactly when the reflexive clitic climbs — (19b)/(20a) against (19a)/(20b) — so there is no AS without climbing.

theorem Olivier2026.unaccusative_optional (ea ia : Person) (rich : Bool) : Restructuring.matrixAux ea ia { embedded := { verb := ArgumentStructure.TransitivityClass.unaccusative }, transfer := TransferStyle.share, richAux := rich } = Verb.PerfectAuxiliary.be ∧ Restructuring.matrixAux ea ia { embedded := { verb := ArgumentStructure.TransitivityClass.unaccusative }, transfer := TransferStyle.keep, richAux := rich } = Verb.PerfectAuxiliary.have

§7.2: with an unaccusative infinitive and no clitic nothing but the auxiliary distinguishes SHARE (75)/(76) from KEEP (73)/(74) — AS is optional.

theorem Olivier2026.prepositional_climbing (ea ia : Person) (cl : Clitic) (hcl : cl.prepositional = true) (rich : Bool) : { embedded := { verb := ArgumentStructure.TransitivityClass.unaccusative, clitic := some cl }, transfer := TransferStyle.share, richAux := rich }.climbs ∧ (Restructuring.Switch ea ia { embedded := { verb := ArgumentStructure.TransitivityClass.unaccusative, clitic := some cl }, transfer := TransferStyle.share, richAux := rich } ↔ rich = true)

§7.3: a prepositional clitic climbing out of an unaccusative leaves HAVE when vAux carries only its P-feature ((25)–(27), (36)), BE when vAux also probes the internal argument ((28)–(30), (37a)).

theorem Olivier2026.accusative_climbing (ea ia : Person) (rich : Bool) : { embedded := { verb := ArgumentStructure.TransitivityClass.transitive, clitic := some Clitic.accusative }, transfer := TransferStyle.share, richAux := rich }.climbs ∧ Restructuring.matrixAux ea ia { embedded := { verb := ArgumentStructure.TransitivityClass.transitive, clitic := some Clitic.accusative }, transfer := TransferStyle.share, richAux := rich } = Verb.PerfectAuxiliary.have

(31), [CS04]'s lo sarei voluto andare a trovare aside: an accusative clitic climbs out of a transitive infinitive without AS — its identity is not the subject's.

Varieties (§7.1)

inductive Olivier2026.Variety : Type

The grammars the paper compares by the transfers they admit: Modern French only KEEP, earlier French and Standard Italian both, Sardinian only SHARE.

• modernFrench : Variety
• earlierFrench : Variety
• standardItalian : Variety
• sardinian : Variety

@[instance_reducible]

instance Olivier2026.instDecidableEqVariety : DecidableEq Variety

Equations

• Olivier2026.instDecidableEqVariety x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Olivier2026.instReprVariety.repr : Variety → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Olivier2026.instReprVariety : Repr Variety

Equations

• Olivier2026.instReprVariety = { reprPrec := Olivier2026.instReprVariety.repr }

@[instance_reducible]

instance Olivier2026.instFintypeVariety : Fintype Variety

Equations

• Olivier2026.instFintypeVariety = { elems := { val := ↑Olivier2026.Variety.enumList, nodup := Olivier2026.Variety.enumList_nodup }, complete := Olivier2026.instFintypeVariety._proof_1 }

def Olivier2026.Variety.admits : Variety → TransferStyle → Prop

The transfer operations a variety admits.

Equations

• Olivier2026.Variety.modernFrench.admits x✝ = (x✝ = Olivier2026.TransferStyle.keep)
• Olivier2026.Variety.sardinian.admits x✝ = (x✝ = Olivier2026.TransferStyle.share)
• x✝¹.admits x✝ = (x✝ = Olivier2026.TransferStyle.keep ∨ x✝ = Olivier2026.TransferStyle.share)

@[instance_reducible]

instance Olivier2026.instDecidableAdmits (v : Variety) (t : TransferStyle) : Decidable (v.admits t)

Equations

• One or more equations did not get rendered due to their size.
• Olivier2026.instDecidableAdmits Olivier2026.Variety.modernFrench x✝ = Olivier2026.instDecidableAdmits._aux_1 x✝
• Olivier2026.instDecidableAdmits Olivier2026.Variety.sardinian x✝ = Olivier2026.instDecidableAdmits._aux_3 x✝

theorem Olivier2026.sardinian_reflexive (ea ia : Person) (r : Restructuring) (hv : Variety.sardinian.admits r.transfer) (he : r.embedded = { verb := ArgumentStructure.TransitivityClass.reflexive, clitic := some Clitic.reflexive }) : r.climbs ∧ Restructuring.Switch ea ia r

(38): in Sardinian the reflexive clitic climbs and the modal takes BE, obligatorily.

theorem Olivier2026.modernFrench_no_switch (ea ia : Person) (r : Restructuring) (hv : Variety.modernFrench.admits r.transfer) : ¬r.climbs ∧ ¬Restructuring.Switch ea ia r

Modern French: KEEP alone yields neither climbing nor AS — (2a), (3a); the attested AS of §3.3 is the SHARE derivation (71) surfacing in a grammar that does not usually use it.