@cite{dowty-1991} Proto-Roles: Theory Bridges and Canonical Profiles

@cite{levin-2022}

Pure theory file connecting the entailment profile theory (EntailmentProfile.lean) to other semantic modules: @cite{cruse-1973} agentivity, @cite{krifka-1998} SINC, change-of-state, causation, and @cite{levin-1993} meaning components.

Verb-specific entailment profiles (canonical instances of EntailmentProfile) are defined here as theory-level constants. Bridge theorems connecting these profiles to English Fragment entries live in study files under Phenomena/.

theorem Semantics.Events.ProtoRoles.kick_subject_outranks : outranksForSubject kickSubjectProfile kickObjectProfile = true

Kick: subject outranks object (lattice: {V,S,C,M,IE} ⊃ {}).

theorem Semantics.Events.ProtoRoles.build_subject_outranks : outranksForSubject buildSubjectProfile buildObjectProfile = true

Build: subject outranks object.

theorem Semantics.Events.ProtoRoles.eat_subject_outranks : outranksForSubject eatSubjectProfile eatObjectProfile = true

Eat: subject outranks object.

theorem Semantics.Events.ProtoRoles.buy_sell_alternation : allowsAlternation buySubjectProfile sellSubjectProfile = true

Buy/sell subjects have identical profiles → alternation.

theorem Semantics.Events.ProtoRoles.die_unaccusative : predictsUnaccusative dieSubjectProfile = true

die: no volition, no causation, 3 P-Pat → unaccusative.

theorem Semantics.Events.ProtoRoles.arrive_unaccusative : predictsUnaccusative arriveSubjectProfile = true

arrive: no volition, no causation, 1 P-Pat → unaccusative. This FIXES the anomaly in @cite{dowty-1991}'s flat counting, which predicted unergative because pAgentScore (2) > pPatientScore (1).

theorem Semantics.Events.ProtoRoles.run_unergative : predictsUnergative runSubjectProfile = true

run: has volition, 0 P-Pat → unergative.

theorem Semantics.Events.ProtoRoles.run_not_unaccusative : predictsUnaccusative runSubjectProfile = false

theorem Semantics.Events.ProtoRoles.kick_subject_passes_doTest : passesDoTestFromProfile kickSubjectProfile = true

Kick subject passes the do-test (has volition + causation + movement).

theorem Semantics.Events.ProtoRoles.die_subject_fails_doTest : passesDoTestFromProfile dieSubjectProfile = false

Die subject does NOT pass the do-test (no volition, causation, or movement).

theorem Semantics.Events.ProtoRoles.arrive_subject_passes_doTest : passesDoTestFromProfile arriveSubjectProfile = true

Arrive subject passes the do-test (has movement).

theorem Semantics.Events.ProtoRoles.buildObject_is_incrementalTheme : buildObjectProfile.incrementalTheme = true

theorem Semantics.Events.ProtoRoles.eatObject_is_incrementalTheme : eatObjectProfile.incrementalTheme = true

theorem Semantics.Events.ProtoRoles.kickObject_not_incrementalTheme : kickObjectProfile.incrementalTheme = false

theorem Semantics.Events.ProtoRoles.kickObject_changeOfState : kickObjectProfile.changeOfState = true

theorem Semantics.Events.ProtoRoles.buildObject_changeOfState : buildObjectProfile.changeOfState = true

theorem Semantics.Events.ProtoRoles.dieSubject_changeOfState : dieSubjectProfile.changeOfState = true

theorem Semantics.Events.ProtoRoles.arriveSubject_changeOfState : arriveSubjectProfile.changeOfState = true

theorem Semantics.Events.ProtoRoles.causation_entailment_implies_pAgent_ge_one (p : EntailmentProfile) (h : p.causation = true) : p.pAgentScore ≥ 1

theorem Semantics.Events.ProtoRoles.kickSubject_has_causation : kickSubjectProfile.causation = true

theorem Semantics.Events.ProtoRoles.buildSubject_has_causation : buildSubjectProfile.causation = true

theorem Semantics.Events.ProtoRoles.sweep_instr_more_agentive : sweepBroomSubjectProfile.pAgentScore > sweepBasicSubjectProfile.pAgentScore

Variable agentivity = the broom sense has strictly more P-Agent entailments than the basic sense.

theorem Semantics.Events.ProtoRoles.sweep_passes_doTest : passesDoTestFromProfile sweepBasicSubjectProfile = true

theorem Semantics.Events.ProtoRoles.sweep_instr_passes_doTest : passesDoTestFromProfile sweepBroomSubjectProfile = true

theorem Semantics.Events.ProtoRoles.wind_is_effector : isEffector sweepBasicSubjectProfile = true

Wind as effector: movement + independent existence.

theorem Semantics.Events.ProtoRoles.kickObject_is_forceRecipient : isForceRecipient kickObjectProfile = true

Kick object is a force recipient (causally affected + stationary).

@cite{levin-1993}'s meaning components are a coarse-grained projection of Dowty's entailment profiles. Three of the four components correspond to specific Dowty entailments:

| Levin component | Dowty entailment | Argument |
|---|---|---|
| `causation` | P-Agent (c) `causation` | Subject |
| `changeOfState` | P-Patient (a) `changeOfState` | Object / unacc. subject |
| `motion` | P-Agent (d) `movement` | Subject |
| `contact` | — (no direct Dowty counterpart) | — |

The key divergence: Levin's `causation` is *narrow* — it diagnoses
specifically causation of a change of state (via the causative/inchoative
alternation). Dowty's `causation` is *broad* — any event where one
participant causes something in another. 

def Semantics.Events.ProtoRoles.levinSubjectPrediction (mc : MeaningComponents) : Bool × Bool

Equations

• Semantics.Events.ProtoRoles.levinSubjectPrediction mc = (mc.causation, mc.motion)

def Semantics.Events.ProtoRoles.levinPatientPrediction (mc : MeaningComponents) : Bool × Bool

Equations

• Semantics.Events.ProtoRoles.levinPatientPrediction mc = (mc.changeOfState, mc.causation)

theorem Semantics.Events.ProtoRoles.break_class_subject_causation : (levinSubjectPrediction LevinClass.break_.meaningComponents).1 = true

theorem Semantics.Events.ProtoRoles.break_class_patient_cos : (levinPatientPrediction LevinClass.break_.meaningComponents).1 = true

theorem Semantics.Events.ProtoRoles.hit_class_no_levin_causation : (levinSubjectPrediction LevinClass.hit.meaningComponents).1 = false

theorem Semantics.Events.ProtoRoles.hit_class_patient_no_cos : (levinPatientPrediction LevinClass.hit.meaningComponents).1 = false

theorem Semantics.Events.ProtoRoles.kick_dowty_vs_levin_causation : kickSubjectProfile.causation = true ∧ LevinClass.hit.meaningComponents.causation = false

theorem Semantics.Events.ProtoRoles.motion_class_subject_movement : (levinSubjectPrediction LevinClass.mannerOfMotion.meaningComponents).2 = true ∧ (levinSubjectPrediction LevinClass.inherentlyDirectedMotion.meaningComponents).2 = true

theorem Semantics.Events.ProtoRoles.stative_class_no_dynamics : levinSubjectPrediction LevinClass.exist.meaningComponents = (false, false) ∧ levinSubjectPrediction LevinClass.admire.meaningComponents = (false, false)

theorem Semantics.Events.ProtoRoles.levin_causation_subsumes (mc : MeaningComponents) : mc.causation = true → (levinSubjectPrediction mc).1 = true

theorem Semantics.Events.ProtoRoles.dowty_causation_not_subsumes : kickSubjectProfile.causation = true ∧ LevinClass.hit.meaningComponents.causation = false

theorem Semantics.Events.ProtoRoles.levin_causation_implies_both (mc : MeaningComponents) (h : mc.causation = true) : (levinSubjectPrediction mc).1 = true ∧ (levinPatientPrediction mc).2 = true

theorem Semantics.Events.ProtoRoles.kick_wellformed : kickSubjectProfile.wellFormedInternal = true

All canonical verb profiles satisfy the internal well-formedness constraint (volition → sentience).

theorem Semantics.Events.ProtoRoles.die_wellformed : dieSubjectProfile.wellFormedInternal = true

theorem Semantics.Events.ProtoRoles.arrive_wellformed : arriveSubjectProfile.wellFormedInternal = true

theorem Semantics.Events.ProtoRoles.sweep_basic_wellformed : sweepBasicSubjectProfile.wellFormedInternal = true

theorem Semantics.Events.ProtoRoles.kick_pair_causation_cos : (!kickSubjectProfile.causation || kickObjectProfile.changeOfState) = true ∧ (!kickSubjectProfile.independentExistence || kickObjectProfile.dependentExistence) = false

Kick satisfies the causation↔CoS paired constraint but NOT the IE↔DE constraint (the ball exists independently of the kicking).

theorem Semantics.Events.ProtoRoles.build_pair_partial : (!buildSubjectProfile.causation || buildObjectProfile.changeOfState) = true ∧ (!buildSubjectProfile.independentExistence || buildObjectProfile.dependentExistence) = true ∧ (!buildSubjectProfile.movement || buildObjectProfile.stationary) = false

Build satisfies causation↔CoS and IE↔DE, but NOT movement↔stationary (the thing being built is not stationary relative to the builder).

theorem Semantics.Events.ProtoRoles.eat_pair_partial : (!eatSubjectProfile.causation || eatObjectProfile.changeOfState) = true ∧ (!eatSubjectProfile.movement || eatObjectProfile.stationary) = false ∧ (!eatSubjectProfile.independentExistence || eatObjectProfile.dependentExistence) = false

Eat satisfies causation↔CoS but NOT movement↔stationary or IE↔DE (food exists independently and is not stationary).

@cite{grimm-2011}'s agentivity lattice reformulates proto-role entailments as privative features with lattice structure. This section connects the entailment profiles to Grimm's lattice, combining results from multiple theory bridges (@cite{cruse-1973} agentivity, @cite{krifka-1998} SINC).

theorem Semantics.Events.ProtoRoles.kick_cruse_grimm_consistent : passesDoTestFromProfile kickSubjectProfile = true ∧ AgentivityLattice.AgentivityNode.fromEntailmentProfile kickSubjectProfile = ⊤ ∧ (AgentivityLattice.GrimmNode.fromSubjectProfile kickSubjectProfile).toCaseRegion.toAccusativeCase = Core.Case.nom

Cross-theory: kick subject passes the do-test (@cite{cruse-1973}), has maximal agentivity on @cite{grimm-2011}'s lattice (⊤), and maps to NOM in an accusative system. Three theories converge.

theorem Semantics.Events.ProtoRoles.die_cruse_grimm_consistent : passesDoTestFromProfile dieSubjectProfile = false ∧ AgentivityLattice.AgentivityNode.fromEntailmentProfile dieSubjectProfile = ⊥ ∧ (AgentivityLattice.GrimmNode.fromObjectProfile dieSubjectProfile).toCaseRegion.toErgativeCase = Core.Case.abs

Cross-theory: die subject fails the do-test, has zero agentivity (⊥), and maps to ABS in an ergative system.

theorem Semantics.Events.ProtoRoles.build_krifka_grimm_consistent : buildObjectProfile.incrementalTheme = true ∧ AgentivityLattice.PersistenceLevel.fromPatientProfile buildObjectProfile = AgentivityLattice.PersistenceLevel.exPersEnd ∧ (AgentivityLattice.GrimmNode.fromObjectProfile buildObjectProfile).toCaseRegion ≠ AgentivityLattice.CaseRegion.accAbs

Cross-theory: build object is an incremental theme (@cite{krifka-1998}), maps to exPersEnd on @cite{grimm-2011}'s persistence scale (creation), and falls OUTSIDE the canonical ACC region — creation verb objects are non-prototypically transitive.

theorem Semantics.Events.ProtoRoles.arrive_asp_grimm_consistent : predictsUnaccusative arriveSubjectProfile = true ∧ (AgentivityLattice.GrimmNode.fromSubjectProfile arriveSubjectProfile).toCaseRegion ≠ AgentivityLattice.CaseRegion.nomErg

Cross-theory: arrive subject has movement but not instigation → Grimm's lattice places it outside the NOM/ERG region, consistent with the priority-based ASP predicting unaccusative.