Sorace (2000): Auxiliary Selection × Vendler Aspect Classes

[Sor00]

Connects the auxiliary selection substrate in AuxiliarySelection to Vendler's aspectual classification from Features.Aktionsart.

Known gaps

• [Sor00]'s gradient Auxiliary Selection Hierarchy is not yet formalized — vendlerClassToTypicalTransitivity is a flat lookup, not a derivation from proto-role entailments. A principled version would build the mapping out of Features/EntailmentProfile.lean so that, e.g., the achievement → unaccusative arrow falls out of changeOfState ∧ ¬volition. TODO when EntailmentProfile-based unaccusativity diagnostics are wired up.

def Sorace2000.vendlerClassToTypicalTransitivity : Features.VendlerClass → ArgumentStructure.AuxiliarySelection.TransitivityClass

Vendler's achievement class (telic, punctual) typically corresponds to unaccusativity: canonical achievements are change-of-state verbs whose subject is a theme/patient.

TODO: derive this from proto-role entailments in Features/EntailmentProfile.lean (cf. file docstring). Today this is a stipulated lookup; the rfl-trivial theorems that chained it with canonicalSelection have been dropped because they just unpacked two lookup tables.

Equations

• Sorace2000.vendlerClassToTypicalTransitivity Features.VendlerClass.achievement = ArgumentStructure.AuxiliarySelection.TransitivityClass.unaccusative
• Sorace2000.vendlerClassToTypicalTransitivity Features.VendlerClass.accomplishment = ArgumentStructure.AuxiliarySelection.TransitivityClass.transitive
• Sorace2000.vendlerClassToTypicalTransitivity Features.VendlerClass.activity = ArgumentStructure.AuxiliarySelection.TransitivityClass.unergative
• Sorace2000.vendlerClassToTypicalTransitivity Features.VendlerClass.state = ArgumentStructure.AuxiliarySelection.TransitivityClass.unergative
• Sorace2000.vendlerClassToTypicalTransitivity Features.VendlerClass.semelfactive = ArgumentStructure.AuxiliarySelection.TransitivityClass.unergative

theorem Sorace2000.haveOnly_agrees_with_canonical_iff (c : ArgumentStructure.AuxiliarySelection.TransitivityClass) : ArgumentStructure.AuxiliarySelection.SelectionRule.selects true ArgumentStructure.AuxiliarySelection.SelectionRule.haveOnly c = some (ArgumentStructure.AuxiliarySelection.canonicalSelection c) ↔ ¬ArgumentStructure.AuxiliarySelection.SelectsBe c

A have-only perfect system agrees with the canonical split exactly on the classes that do not select be ([Sor00]): English, with its have-only perfect, diverges from Italian precisely on the BE-selecting classes (has arrived vs è arrivato).