Staps & Rooryck (2024): Formalizing Spatial-Causal Polysemy of Agent Prepositions

@cite{staps-rooryck-2024}

Semantics and Pragmatics 17, Article 4, pp. 1–47.

Core Claims

1. Agent prepositions (by, French par/de) are not semantically vacuous case markers. They have non-trivial semantic content derived from their spatial meanings via principled polysemy (@cite{tyler-evans-2003}).

2. The general denotation is polymorphically typed: ⟨η, ⟨θ, t⟩⟩, where η (Figure) and θ (Ground) are instantiated by the syntactic/semantic context. Spatial: ⟨e, ⟨e, t⟩⟩. Agentive: ⟨e, ⟨s, t⟩⟩.

3. French par ('through, via') presupposes high proto-agentivity; de ('from, of') presupposes low proto-agentivity. The relevant factors are: bringing about a change (§3.1), contextually inferred change (§3.2), volitionality (§3.3), and telicity (§3.4).

4. The same polymorphic mechanism extends to causal adjuncts (§2.3): de marks causes-as-situations (type ⟨s, ⟨s, t⟩⟩), par marks causes-as-forces (type ⟨f, ⟨s, t⟩⟩), following @cite{copley-harley-2022}.

Formalization Strategy

Proto-agentivity is formalized via EntailmentProfile.pAgentScore and the specific entailments {volition, causation, movement}. The prediction is: par requires the subject to have at least one of these "active" entailments; de is the default for low-agentivity subjects.

We derive the par/de preference from the verb's stored EntailmentProfile and VendlerClass, connecting to the affectedness hierarchy (@cite{beavers-2010}) and aspectual classification (@cite{vendler-1957}).

Integration with linglib

• Subject profiles reuse canonical @cite{dowty-1991} profiles (kickSubjectProfile, seeSubjectProfile, runSubjectProfile) rather than duplicating them, making the connection structural.
• Passive voice connects to @cite{collins-2005}'s voicePassive — Case-checking by Voice is the syntactic correlate of the preposition's semantic contribution.
• Object affectedness derives from @cite{beavers-2010}'s profileToDegree.

inductive StapsRooryck2024.SemDomain : Type

Semantic domain types for preposition Figure/Ground arguments. The paper's ⟨η, ⟨θ, t⟩⟩ polymorphism: η and θ range over these domain types, constrained by the syntactic/semantic context.

• e : SemDomain
• s : SemDomain
• f : SemDomain

@[implicit_reducible]

instance StapsRooryck2024.instDecidableEqSemDomain : DecidableEq SemDomain

Equations

• StapsRooryck2024.instDecidableEqSemDomain x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance StapsRooryck2024.instReprSemDomain : Repr SemDomain

Equations

• StapsRooryck2024.instReprSemDomain = { reprPrec := StapsRooryck2024.instReprSemDomain.repr }

def StapsRooryck2024.instReprSemDomain.repr : SemDomain → ℕ → Std.Format

Equations

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

structure StapsRooryck2024.PrepType : Type

A polymorphic preposition type: ⟨η, ⟨θ, t⟩⟩. The Figure (η) is the first argument; the Ground (θ) is the second.

• figure : SemDomain
• ground : SemDomain

def StapsRooryck2024.instDecidableEqPrepType.decEq (x✝ x✝¹ : PrepType) : Decidable (x✝ = x✝¹)

Equations

• StapsRooryck2024.instDecidableEqPrepType.decEq { figure := a, ground := a_1 } { figure := b, ground := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance StapsRooryck2024.instDecidableEqPrepType : DecidableEq PrepType

Equations

• StapsRooryck2024.instDecidableEqPrepType = StapsRooryck2024.instDecidableEqPrepType.decEq

@[implicit_reducible]

instance StapsRooryck2024.instReprPrepType : Repr PrepType

Equations

• StapsRooryck2024.instReprPrepType = { reprPrec := StapsRooryck2024.instReprPrepType.repr }

def StapsRooryck2024.instReprPrepType.repr : PrepType → ℕ → Std.Format

Equations

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

def StapsRooryck2024.spatialType : PrepType

Spatial instantiation: ⟨e, ⟨e, t⟩⟩. "The house by the lake" — two entities in close proximity.

Equations

• StapsRooryck2024.spatialType = { figure := StapsRooryck2024.SemDomain.e, ground := StapsRooryck2024.SemDomain.e }

def StapsRooryck2024.agentiveType : PrepType

Agentive instantiation: ⟨e, ⟨s, t⟩⟩. "Written by John" — entity in close proximity to event. Interpretation: Initiator(x, e).

Equations

• StapsRooryck2024.agentiveType = { figure := StapsRooryck2024.SemDomain.e, ground := StapsRooryck2024.SemDomain.s }

def StapsRooryck2024.causalForceType : PrepType

Causal adjunct (force-based): ⟨f, ⟨s, t⟩⟩. French par un tremblement de terre — force in close proximity to situation. Used by par in causal adjuncts.

Equations

• StapsRooryck2024.causalForceType = { figure := StapsRooryck2024.SemDomain.f, ground := StapsRooryck2024.SemDomain.s }

def StapsRooryck2024.causalSituationType : PrepType

Causal adjunct (situation-based): ⟨s, ⟨s, t⟩⟩. French de faim — situation in close proximity to situation. Used by de in causal adjuncts.

Equations

• StapsRooryck2024.causalSituationType = { figure := StapsRooryck2024.SemDomain.s, ground := StapsRooryck2024.SemDomain.s }

theorem StapsRooryck2024.agentive_not_spatial : agentiveType ≠ spatialType

theorem StapsRooryck2024.causal_force_not_situation : causalForceType ≠ causalSituationType

def StapsRooryck2024.hasActiveAgentEntailment (p : Semantics.ArgumentStructure.EntailmentProfile.EntailmentProfile) : Bool

The "active" P-Agent entailments that drive par selection. §3.5 (34): change/causation, volitionality, and kinesis/movement are the three entailments that distinguish par-requiring from de-allowing contexts. These are a strict subset of @cite{dowty-1991}'s five P-Agent entailments — sentience and independent existence do NOT contribute to par selection (experiencers allow de).

Note: the paper's (34) establishes a hierarchy among these factors: (34a) change is primary — if change is possible, par presupposes it; (34b) volitionality and telicity are secondary — relevant only when change is excluded. Our disjunction correctly predicts the binary par-required/de-available outcome for all attested verbs.

Equations

• StapsRooryck2024.hasActiveAgentEntailment p = (p.volition || p.causation || p.movement)

def StapsRooryck2024.predictsParRequired (p : Semantics.ArgumentStructure.EntailmentProfile.EntailmentProfile) : Bool

par is required when the subject has active agent entailments. This is a necessary condition: de is RULED OUT for high-agentivity contexts, while par as the modern French default can appear even with low-agentivity Agents.

Equations

• StapsRooryck2024.predictsParRequired p = StapsRooryck2024.hasActiveAgentEntailment p

def StapsRooryck2024.predictsDeAvailable (p : Semantics.ArgumentStructure.EntailmentProfile.EntailmentProfile) : Bool

de is available when active agent entailments are absent.

Equations

• StapsRooryck2024.predictsDeAvailable p = !StapsRooryck2024.hasActiveAgentEntailment p

theorem StapsRooryck2024.par_de_complementary (p : Semantics.ArgumentStructure.EntailmentProfile.EntailmentProfile) : predictsParRequired p = !predictsDeAvailable p

§3.5 (34): par and de are in complementary distribution w.r.t. proto-agentivity. Par implies change; de presupposes its absence. This is the paper's primary empirical generalization.

theorem StapsRooryck2024.canonical_agent_requires_par : predictsParRequired Fragments.French.Predicates.protoTransSubjectProfile = true

Canonical agents (laver, écrire, construire, tuer, abandonner, délaisser) have V+S+C+M+IE → par required. This is kickSubjectProfile from @cite{dowty-1991}.

theorem StapsRooryck2024.experiencer_allows_de : predictsDeAvailable Fragments.French.Predicates.experiencerSubjectProfile = true

Experiencer subjects (aimer, adorer, respecter) have S+IE only → de available. This is seeSubjectProfile from @cite{dowty-1991}.

theorem StapsRooryck2024.stative_positional_allows_de : predictsDeAvailable Fragments.French.Predicates.stativePositionalSubjectProfile = true

Stative positional subjects (précéder, stative suivre) have IE only → de available.

theorem StapsRooryck2024.dynamic_motion_requires_par : predictsParRequired Fragments.French.Predicates.dynamicFollowSubjectProfile = true

Dynamic motion subjects (dynamic suivre) have V+S+M+IE → par required. This is runSubjectProfile from @cite{dowty-1991}.

theorem StapsRooryck2024.accompany_requires_par : predictsParRequired Fragments.French.Predicates.accompanySubjectProfile = true

Accompany subjects have S+M+IE → par required (movement suffices).

def StapsRooryck2024.telicityFavorsPar (vc : Features.VendlerClass) : Bool

§3.4: Telicity influences par/de selection. Telic events imply a bounded change, which increases proto-agentivity.

Equations

• StapsRooryck2024.telicityFavorsPar vc = (vc.telicity == Features.Telicity.telic)

theorem StapsRooryck2024.accomplishment_favors_par : telicityFavorsPar Features.VendlerClass.accomplishment = true

theorem StapsRooryck2024.achievement_favors_par : telicityFavorsPar Features.VendlerClass.achievement = true

theorem StapsRooryck2024.activity_no_telic_par : telicityFavorsPar Features.VendlerClass.activity = false

theorem StapsRooryck2024.state_no_telic_par : telicityFavorsPar Features.VendlerClass.state = false

def StapsRooryck2024.objectChangeFavorsPar (objProfile : Semantics.ArgumentStructure.EntailmentProfile.EntailmentProfile) : Bool

§3.1: Object affectedness also matters. Verbs with quantized or nonquantized affectedness entail a Patient change → forces par. Connects to @cite{beavers-2010}'s affectedness hierarchy.

Equations

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

theorem StapsRooryck2024.laver_object_favors_par : objectChangeFavorsPar Fragments.French.Predicates.protoTransObjectProfile = true

theorem StapsRooryck2024.ecrire_object_favors_par : objectChangeFavorsPar (have __src := Fragments.French.Predicates.protoTransObjectProfile; { volition := __src.volition, sentience := __src.sentience, causation := __src.causation, movement := __src.movement, independentExistence := __src.independentExistence, changeOfState := __src.changeOfState, incrementalTheme := true, causallyAffected := __src.causallyAffected, stationary := __src.stationary, dependentExistence := true }) = true

theorem StapsRooryck2024.stimulus_no_object_par : objectChangeFavorsPar Fragments.French.Predicates.minimalParticipantProfile = false

def StapsRooryck2024.predictsPar (v : Fragments.French.Predicates.FrenchVerbEntry) : Bool

Full prediction combining subject proto-agentivity, object affectedness, and telicity. Any one factor suffices for par.

Equations

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

theorem StapsRooryck2024.par_verbs : predictsPar Fragments.French.Predicates.laver = true ∧ predictsPar Fragments.French.Predicates.ecrire = true ∧ predictsPar Fragments.French.Predicates.construire = true ∧ predictsPar Fragments.French.Predicates.tuer = true ∧ predictsPar Fragments.French.Predicates.abandonner = true ∧ predictsPar Fragments.French.Predicates.delaisser = true ∧ predictsPar Fragments.French.Predicates.suivreDyn = true ∧ predictsPar Fragments.French.Predicates.accompagner = true

Par-required verbs: all have active agent entailments, affected objects, and/or telic aspect.

theorem StapsRooryck2024.de_available_verbs : predictsPar Fragments.French.Predicates.aimer = false ∧ predictsPar Fragments.French.Predicates.adorer = false ∧ predictsPar Fragments.French.Predicates.respecter = false ∧ predictsPar Fragments.French.Predicates.preceder = false ∧ predictsPar Fragments.French.Predicates.suivreStat = false

Par/de verbs: experiencer and stative subjects lack active agent entailments, unaffected objects, and atelic aspect.

structure StapsRooryck2024.SurveyJudgment : Type

Survey judgment: verb form, context agentivity level, and mean acceptability for de and par on [-1, 1] scale.

• verb : String
• context : String
• deMean : ℤ
• parMean : ℤ

def StapsRooryck2024.instReprSurveyJudgment.repr : SurveyJudgment → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance StapsRooryck2024.instReprSurveyJudgment : Repr SurveyJudgment

Equations

• StapsRooryck2024.instReprSurveyJudgment = { reprPrec := StapsRooryck2024.instReprSurveyJudgment.repr }

def StapsRooryck2024.surveyData : List SurveyJudgment

Survey data from @cite{staps-rooryck-2024} Table 2. Means are ×100 (e.g., 0.87 → 87, -0.96 → -96).

Equations

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

theorem StapsRooryck2024.change_verbs_reject_de : ((List.filter (fun (j : SurveyJudgment) => j.verb == "lavé" || j.verb == "maintenu" || j.verb == "traversé" || j.verb == "suivie" && j.context == "high") surveyData).all fun (j : SurveyJudgment) => decide (j.deMean < 0)) = true

§3.1 Change-entailing verbs reject de (all deMean < 0). Filter restricts to the §3.1 items (high proto-agentivity context) to exclude §3.3 volitionality items with the same verb form.

theorem StapsRooryck2024.suivi_high_prefers_par : ((List.filter (fun (j : SurveyJudgment) => j.verb == "suivi" && j.context == "high") surveyData).all fun (j : SurveyJudgment) => decide (j.parMean > j.deMean)) = true

High-agentivity suivi prefers par (parMean > deMean).

theorem StapsRooryck2024.suivi_low_prefers_de : ((List.filter (fun (j : SurveyJudgment) => j.verb == "suivi" && j.context == "low") surveyData).all fun (j : SurveyJudgment) => decide (j.deMean > j.parMean)) = true

Low-agentivity suivi prefers de (deMean > parMean).

inductive StapsRooryck2024.FrenchAgentPrep : Type

The by-phrase is an argument of v, not an adjunct. In the passive, Voice checks Case but does not assign θ — the θ-role comes from v. The par/de preposition is the morphological spell-out of this Case-checking relationship, with the semantic contribution being Initiator(x,e) plus the proto-agentivity presupposition.

This connects @cite{staps-rooryck-2024}'s §2.2 to @cite{collins-2005}'s passive structure: Voice_PASS checks Case while v assigns the external θ-role.

• par : FrenchAgentPrep
• de : FrenchAgentPrep

@[implicit_reducible]

instance StapsRooryck2024.instDecidableEqFrenchAgentPrep : DecidableEq FrenchAgentPrep

Equations

• StapsRooryck2024.instDecidableEqFrenchAgentPrep x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def StapsRooryck2024.instReprFrenchAgentPrep.repr : FrenchAgentPrep → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance StapsRooryck2024.instReprFrenchAgentPrep : Repr FrenchAgentPrep

Equations

• StapsRooryck2024.instReprFrenchAgentPrep = { reprPrec := StapsRooryck2024.instReprFrenchAgentPrep.repr }

def StapsRooryck2024.FrenchAgentPrep.passiveType : FrenchAgentPrep → PrepType

Both par and de in passives have agentive type ⟨e, ⟨s, t⟩⟩. They differ only in presupposition, not at-issue type.

Equations

• StapsRooryck2024.FrenchAgentPrep.par.passiveType = StapsRooryck2024.agentiveType
• StapsRooryck2024.FrenchAgentPrep.de.passiveType = StapsRooryck2024.agentiveType

def StapsRooryck2024.FrenchAgentPrep.causalType : FrenchAgentPrep → PrepType

In causal adjuncts, par and de diverge in type: par: ⟨f, ⟨s, t⟩⟩ (forces), de: ⟨s, ⟨s, t⟩⟩ (situations).

Equations

• StapsRooryck2024.FrenchAgentPrep.par.causalType = StapsRooryck2024.causalForceType
• StapsRooryck2024.FrenchAgentPrep.de.causalType = StapsRooryck2024.causalSituationType

theorem StapsRooryck2024.par_de_same_passive_type : FrenchAgentPrep.par.passiveType = FrenchAgentPrep.de.passiveType

theorem StapsRooryck2024.par_de_different_causal_type : FrenchAgentPrep.par.causalType ≠ FrenchAgentPrep.de.causalType

theorem StapsRooryck2024.passive_provides_case_position : Minimalist.voicePassive.ChecksCase ∧ ¬Minimalist.voicePassive.AssignsTheta

The syntactic precondition for par/de: passive Voice checks Case (feature dissociation per @cite{collins-2005}), providing the structural position for the preposition. The par/de choice is then determined by proto-agentivity.

inductive StapsRooryck2024.CausalChainPosition : Type

Position in the causal chain relative to the Patient. @cite{croft-2012}: par 'through' = perlative (path position), de 'from' = ablative (source position). Closer to Patient → more proto-agentive.

• source : CausalChainPosition
• path : CausalChainPosition
• goal : CausalChainPosition

@[implicit_reducible]

instance StapsRooryck2024.instDecidableEqCausalChainPosition : DecidableEq CausalChainPosition

Equations

• StapsRooryck2024.instDecidableEqCausalChainPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def StapsRooryck2024.instReprCausalChainPosition.repr : CausalChainPosition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance StapsRooryck2024.instReprCausalChainPosition : Repr CausalChainPosition

Equations

• StapsRooryck2024.instReprCausalChainPosition = { reprPrec := StapsRooryck2024.instReprCausalChainPosition.repr }

def StapsRooryck2024.CausalChainPosition.distance : CausalChainPosition → ℕ

Distance from Patient: source > path > goal.

Equations

• StapsRooryck2024.CausalChainPosition.source.distance = 2
• StapsRooryck2024.CausalChainPosition.path.distance = 1
• StapsRooryck2024.CausalChainPosition.goal.distance = 0

def StapsRooryck2024.FrenchAgentPrep.causalPosition : FrenchAgentPrep → CausalChainPosition

Equations

• StapsRooryck2024.FrenchAgentPrep.par.causalPosition = StapsRooryck2024.CausalChainPosition.path
• StapsRooryck2024.FrenchAgentPrep.de.causalPosition = StapsRooryck2024.CausalChainPosition.source

theorem StapsRooryck2024.par_closer_than_de : FrenchAgentPrep.par.causalPosition.distance < FrenchAgentPrep.de.causalPosition.distance

Par has smaller causal distance → higher proto-agentivity.

theorem StapsRooryck2024.quantized_object_implies_par (obj : Semantics.ArgumentStructure.EntailmentProfile.EntailmentProfile) (h : Semantics.ArgumentStructure.Affectedness.Profile.profileToDegree obj = Semantics.ArgumentStructure.Affectedness.Hierarchy.AffectednessDegree.quantized) : objectChangeFavorsPar obj = true

Verbs with quantized object affectedness always require par. Quantized affectedness implies the subject causes a definite change (@cite{beavers-2010}).

theorem StapsRooryck2024.dynamic_vendler_implies_dynamicity (vc : Features.VendlerClass) (h : vc.dynamicity = Features.Dynamicity.dynamic) : vc = Features.VendlerClass.activity ∨ vc = Features.VendlerClass.achievement ∨ vc = Features.VendlerClass.accomplishment ∨ vc = Features.VendlerClass.semelfactive

Dynamic VendlerClasses (activity, achievement, accomplishment) correlate with higher proto-agentivity than states — the stative/dynamic contrast driving suivre's polysemy (§3.3).

theorem StapsRooryck2024.adorer_lexical_not_par : predictsPar Fragments.French.Predicates.adorer = false

§3.2 contextual enrichment gap: adorer's lexical profile predicts de-availability, but high-agentivity contexts license par (survey data shows parMean > 0 in high context). EntailmentProfile alone cannot capture this — it requires pragmatic enrichment.

theorem StapsRooryck2024.adorer_contextual_par_ok : ((List.filter (fun (j : SurveyJudgment) => j.verb == "adorée" && j.context == "high") surveyData).all fun (j : SurveyJudgment) => decide (j.parMean > 0)) = true

theorem StapsRooryck2024.stativePositional_is_minimal : Fragments.French.Predicates.stativePositionalSubjectProfile = Fragments.French.Predicates.minimalParticipantProfile

stativePositionalSubjectProfile is definitionally equal to minimalParticipantProfile — this is structural (via abbrev), not a coincidence. Both roles represent participants with only independent existence.

theorem StapsRooryck2024.active_implies_pAgent_ge_1 (p : Semantics.ArgumentStructure.EntailmentProfile.EntailmentProfile) (h : hasActiveAgentEntailment p = true) : p.pAgentScore ≥ 1

The "active" agent entailments (V, C, M) are a strict subset of @cite{dowty-1991}'s full P-Agent set (V, S, C, M, IE). Profiles with active entailments always have pAgentScore ≥ 1, but the converse fails: experiencer profiles have pAgentScore = 2 (S+IE) yet no active entailments — which is exactly why they allow de.

theorem StapsRooryck2024.experiencer_high_pAgent_but_no_active : Fragments.French.Predicates.experiencerSubjectProfile.pAgentScore ≥ 1 ∧ hasActiveAgentEntailment Fragments.French.Predicates.experiencerSubjectProfile = false

Converse fails: experiencer profiles have pAgentScore ≥ 1 but no active agent entailments. This is the theoretical crux — @cite{staps-rooryck-2024}'s par/de distinction is sensitive to a narrower notion of agentivity than @cite{dowty-1991}'s full count.

theorem StapsRooryck2024.canonical_agent_full_agreement : hasActiveAgentEntailment Fragments.French.Predicates.protoTransSubjectProfile = true ∧ Fragments.French.Predicates.protoTransSubjectProfile.pAgentScore = 5

Canonical agents have all three active entailments and the maximum pAgentScore of 5. This is the canonical case where @cite{staps-rooryck-2024}'s active-agent test and @cite{dowty-1991}'s full P-Agent count agree.

Proto-agentivity level

Binary classification grounding the par/de presupposition contrast. Derived from hasActiveAgentEntailment — not independently stipulated.

inductive StapsRooryck2024.ProtoAgentivityLevel : Type

Binary proto-agentivity level for par/de presuppositions. HIGH = at least one of {V, C, M}; LOW = none.

• high : ProtoAgentivityLevel
• low : ProtoAgentivityLevel

@[implicit_reducible]

instance StapsRooryck2024.instDecidableEqProtoAgentivityLevel : DecidableEq ProtoAgentivityLevel

Equations

• StapsRooryck2024.instDecidableEqProtoAgentivityLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance StapsRooryck2024.instReprProtoAgentivityLevel : Repr ProtoAgentivityLevel

Equations

• StapsRooryck2024.instReprProtoAgentivityLevel = { reprPrec := StapsRooryck2024.instReprProtoAgentivityLevel.repr }

def StapsRooryck2024.instReprProtoAgentivityLevel.repr : ProtoAgentivityLevel → ℕ → Std.Format

Equations

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

def StapsRooryck2024.profileToAgentivityLevel (p : Semantics.ArgumentStructure.EntailmentProfile.EntailmentProfile) : ProtoAgentivityLevel

Bridge from EntailmentProfile to binary agentivity level. Derived from hasActiveAgentEntailment (§2).

Equations

• StapsRooryck2024.profileToAgentivityLevel p = if StapsRooryck2024.hasActiveAgentEntailment p = true then StapsRooryck2024.ProtoAgentivityLevel.high else StapsRooryck2024.ProtoAgentivityLevel.low

theorem StapsRooryck2024.canonical_agent_high : profileToAgentivityLevel Fragments.French.Predicates.protoTransSubjectProfile = ProtoAgentivityLevel.high

theorem StapsRooryck2024.experiencer_low : profileToAgentivityLevel Fragments.French.Predicates.experiencerSubjectProfile = ProtoAgentivityLevel.low

theorem StapsRooryck2024.stative_positional_low : profileToAgentivityLevel Fragments.French.Predicates.stativePositionalSubjectProfile = ProtoAgentivityLevel.low

theorem StapsRooryck2024.dynamic_follow_high : profileToAgentivityLevel Fragments.French.Predicates.dynamicFollowSubjectProfile = ProtoAgentivityLevel.high

Agentive denotations (35a/35b)

The paper's key semantic contribution: par and de share at-issue content (Initiator(x,e)) but carry complementary presuppositions about proto-agentivity. Formalized using PrProp W from Core.Semantics.Presupposition.

structure StapsRooryck2024.AgentivePrepParams (Entity Event W : Type) : Type

Parameters for agentive preposition denotations (35a/35b). Bundled so the denotation is parametric over the event/entity model.

• initiator : Entity → Event → W → Prop

  The at-issue relation: Initiator(x, e).

• highProtoAgentivity : Entity → W → Prop

  Proto-agentivity predicate over entities (in context).

def StapsRooryck2024.parAgentiveDenot {Entity Event W : Type} (params : AgentivePrepParams Entity Event W) (x : Entity) (e : Event) : Core.Presupposition.PrProp W

⟦par⟧_agentive (35a): λx.λe. Initiator(x,e); presup: HIGH proto-agentivity(x).

Equations

• StapsRooryck2024.parAgentiveDenot params x e = { presup := params.highProtoAgentivity x, assertion := params.initiator x e }

def StapsRooryck2024.deAgentiveDenot {Entity Event W : Type} (params : AgentivePrepParams Entity Event W) (x : Entity) (e : Event) : Core.Presupposition.PrProp W

⟦de⟧_agentive (35b): λx.λe. Initiator(x,e); presup: LOW proto-agentivity(x).

Equations

• StapsRooryck2024.deAgentiveDenot params x e = { presup := fun (w : W) => ¬params.highProtoAgentivity x w, assertion := params.initiator x e }

theorem StapsRooryck2024.par_de_same_assertion {Entity Event W : Type} (params : AgentivePrepParams Entity Event W) (x : Entity) (e : Event) : (parAgentiveDenot params x e).assertion = (deAgentiveDenot params x e).assertion

Par and de share at-issue content — same assertion (Initiator(x,e)). This is structural: both pass params.initiator x e as the assertion.

theorem StapsRooryck2024.par_de_presup_complementary {Entity Event W : Type} (params : AgentivePrepParams Entity Event W) [(x : Entity) → (w : W) → Decidable (params.highProtoAgentivity x w)] (x : Entity) (w : W) : params.highProtoAgentivity x w ↔ ¬¬params.highProtoAgentivity x w

Par and de presuppositions are complementary: exactly one is satisfied at every world (classical).

Grounding: presuppositions derive from hasActiveAgentEntailment

The presupposition infrastructure connects back to the per-profile prediction machinery from §2. The proto-agentivity predicate in AgentivePrepParams grounds out in hasActiveAgentEntailment — by construction, not by bridge theorem.

def StapsRooryck2024.lexicalAgentivityParams {Entity Event W : Type} (subjectProfile : Entity → Semantics.ArgumentStructure.EntailmentProfile.EntailmentProfile) (initiator : Entity → Event → W → Prop) : AgentivePrepParams Entity Event W

Construct AgentivePrepParams from EntailmentProfile-based predictions. The proto-agentivity predicate grounds out in hasActiveAgentEntailment, connecting the formal denotation to the existing per-profile predictions.

Equations

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

theorem StapsRooryck2024.presup_agrees_with_prediction {Entity Event W : Type} (subjectProfile : Entity → Semantics.ArgumentStructure.EntailmentProfile.EntailmentProfile) (initiator : Entity → Event → W → Prop) (x : Entity) (e : Event) (w : W) : (parAgentiveDenot (lexicalAgentivityParams subjectProfile initiator) x e).presup w ↔ predictsParRequired (subjectProfile x) = true

The presupposition of ⟦par⟧_agentive agrees with predictsParRequired. This closes the loop: the formal denotation's presupposition IS the existing prediction, not a separate claim that happens to match.

Causal denotations (14b/15b)

The causal uses of par and de differ in type — forces vs situations — already captured by causalForceType/causalSituationType (§1). The denotations are thin wrappers over the causal relations.

def StapsRooryck2024.parCausalDenot (Force Event W : Type) (forces : Force → Event → W → Bool) (f : Force) (e : Event) (w : W) : Bool

⟦par⟧_causal (14b): λf.λe. f FORCES e. Force-based causation — par marks the cause as a force (@cite{copley-harley-2022}).

Equations

• StapsRooryck2024.parCausalDenot Force Event W forces f e w = forces f e w

def StapsRooryck2024.deCausalDenot (Situation Event W : Type) (cause : Situation → Event → W → Bool) (s' : Situation) (e : Event) (w : W) : Bool

⟦de⟧_causal (15b): λs'.λe. s' CAUSE e. Situation-based causation — de marks the cause as a situation (@cite{copley-harley-2022}).

Equations

• StapsRooryck2024.deCausalDenot Situation Event W cause s' e w = cause s' e w

Unified dispatch

def StapsRooryck2024.FrenchAgentPrep.agentiveDenot {Entity Event W : Type} (prep : FrenchAgentPrep) (params : AgentivePrepParams Entity Event W) (x : Entity) (e : Event) : Core.Presupposition.PrProp W

Full denotation dispatch for agentive uses. Wraps the par/de choice into a single function matching on FrenchAgentPrep.

Equations

• StapsRooryck2024.FrenchAgentPrep.par.agentiveDenot params x e = StapsRooryck2024.parAgentiveDenot params x e
• StapsRooryck2024.FrenchAgentPrep.de.agentiveDenot params x e = StapsRooryck2024.deAgentiveDenot params x e