Martin, Schäfer and Kastner (2025): The Lexical Pragmatics of Reflexive Marking

This file formalizes the pragmatic account of French anticausative marking of Martin, Schäfer and Kastner. Anticausatives marked with se and unmarked ones do not differ in meaning; the se form is ambiguous between anticausative and reflexive voice while the bare form is not (Form.voiceOptions, se_ambiguous), and cooperative speakers manage that ambiguity under the Manner supermaxim. With a human argument the reflexive parse is salient, by the bias to read humans as agents; for a limited-control verb, rougir 'blush', the parse misleads, so the unmarked form is preferred, the unmarked limited-control preference (4), and for an in-control verb, (se) plier 'bend', the bare form's inference that no agentive construal was intended misleads instead, so the marked form is preferred, the marked in-control preference (5). With a nonhuman argument no parse is salient and no preference arises, unless the speaker means to present the nonhuman as responsible, when the marked form is preferred since the reflexive parse is the only way to assign it agency, the marked responsibility preference (preference, generalizations). The control level is not read off the entailment profile, limited-control and in-control property-change verbs sharing one (control_level_not_from_entailments), and the opposite preferences of the two classes falsify any uniform semantic difference between the two forms (opposite_preferences_falsify_uniform_semantics). Preferences arise only for verbs with both forms (SeMarking.HasChoice).

Implementation notes

The voice flavours are the non-thematic and reflexive Voice heads of Syntax/Minimalist/Verbal/Voice.lean after Schäfer (2008), and the entailments of an anticausative's sole argument are those of the French fragment's entries; the account presupposes the reflexive–anticausative syncretism of Koontz-Garboden. The experiments' rating means are described in the paper and not represented.

References

• [MSK25]
• [Sch08a]
• [KG09]

The classes

inductive MartinSchaeferKastner2025.SeMarking : Type

The morphological class of an anticausative is whether it has the bare form only, as changer de position, the se form only, as s'affaiblir, or both, as casser, plier and rougir.

• minusSe : SeMarking
• plusSe : SeMarking
• plusMinusSe : SeMarking

@[instance_reducible]

instance MartinSchaeferKastner2025.instDecidableEqSeMarking : DecidableEq SeMarking

Equations

• MartinSchaeferKastner2025.instDecidableEqSeMarking x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def MartinSchaeferKastner2025.SeMarking.HasChoice : SeMarking → Prop

The speaker has a choice of form only for a verb with both forms.

Equations

• MartinSchaeferKastner2025.SeMarking.plusMinusSe.HasChoice = True
• x✝.HasChoice = False

@[instance_reducible]

instance MartinSchaeferKastner2025.instDecidablePredSeMarkingHasChoice : DecidablePred SeMarking.HasChoice

Equations

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

inductive MartinSchaeferKastner2025.ControlLevel : Type

Whether the change a verb names is typically under its human undergoer's control (§1.1): rougir 'blush' and pâlir 'get pale' are limited-control, plier 'bend' and s'approcher 'get close' in-control. The distinction is world knowledge, not entailment.

• limitedControl : ControlLevel
• inControl : ControlLevel

@[instance_reducible]

instance MartinSchaeferKastner2025.instDecidableEqControlLevel : DecidableEq ControlLevel

Equations

• MartinSchaeferKastner2025.instDecidableEqControlLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive MartinSchaeferKastner2025.ResponsibilityGoal : Type

Whether the speaker means to present the entity as responsible for the change.

• neutral : ResponsibilityGoal
• conveyResponsibility : ResponsibilityGoal

@[instance_reducible]

instance MartinSchaeferKastner2025.instDecidableEqResponsibilityGoal : DecidableEq ResponsibilityGoal

Equations

• MartinSchaeferKastner2025.instDecidableEqResponsibilityGoal x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

theorem MartinSchaeferKastner2025.control_level_not_from_entailments : French.Verbs.rougir.subjectEntailments = French.Verbs.refroidir.subjectEntailments

The control level is not derivable from the entailment profile, since the limited-control rougir and the in-control refroidir share one.

theorem MartinSchaeferKastner2025.movement_sufficient_not_necessary : French.Verbs.approcher.subjectEntailments = some French.Verbs.movingUndergoer ∧ French.Verbs.refroidir.subjectEntailments = some French.Verbs.undergoer ∧ ArgumentStructure.ProtoRoleFeature.movement ∈ French.Verbs.movingUndergoer ∧ ArgumentStructure.ProtoRoleFeature.movement ∉ French.Verbs.undergoer

Movement entailments suffice for in-control status, approcher, but are not necessary, refroidir being in-control without them.

The voice ambiguity of se

inductive MartinSchaeferKastner2025.Form : Type

The two forms of a verb with a choice.

• bare : Form
• se : Form

@[instance_reducible]

instance MartinSchaeferKastner2025.instDecidableEqForm : DecidableEq Form

Equations

• MartinSchaeferKastner2025.instDecidableEqForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive MartinSchaeferKastner2025.Flavor : Type

The paper's two flavours of Voice for a French anticausative are the non-thematic Voice of the marked anticausative, Minimalist.Voice.anticausative, and the reflexive Voice, Minimalist.Voice.reflexive.

• nonThematic : Flavor
• reflexive : Flavor

@[instance_reducible]

instance MartinSchaeferKastner2025.instDecidableEqFlavor : DecidableEq Flavor

Equations

• MartinSchaeferKastner2025.instDecidableEqFlavor x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def MartinSchaeferKastner2025.instReprFlavor.repr : Flavor → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance MartinSchaeferKastner2025.instReprFlavor : Repr Flavor

Equations

• MartinSchaeferKastner2025.instReprFlavor = { reprPrec := MartinSchaeferKastner2025.instReprFlavor.repr }

def MartinSchaeferKastner2025.Flavor.head : Flavor → Minimalist.Voice.Head

The Voice head each flavour is.

Equations

• MartinSchaeferKastner2025.Flavor.nonThematic.head = Minimalist.Voice.anticausative
• MartinSchaeferKastner2025.Flavor.reflexive.head = Minimalist.Voice.reflexive

def MartinSchaeferKastner2025.Form.voiceOptions : Form → List Flavor

The voice flavours a form admits. The bare form admits only the non-thematic anticausative and the se form the reflexive as well, the syncretism of [Sch08a] and [KG09].

Equations

• MartinSchaeferKastner2025.Form.bare.voiceOptions = [MartinSchaeferKastner2025.Flavor.nonThematic]
• MartinSchaeferKastner2025.Form.se.voiceOptions = [MartinSchaeferKastner2025.Flavor.nonThematic, MartinSchaeferKastner2025.Flavor.reflexive]

theorem MartinSchaeferKastner2025.se_ambiguous : (∀ (f : Form), Flavor.nonThematic ∈ f.voiceOptions) ∧ Flavor.reflexive ∈ Form.se.voiceOptions ∧ Flavor.reflexive ∉ Form.bare.voiceOptions

Both forms share the anticausative parse, and only the se form has the reflexive one.

Managing the ambiguity (§2)

def MartinSchaeferKastner2025.ReflexiveSalient (a : Reference.Animacy) : Prop

The agent bias makes the reflexive parse of the se form salient for a human argument.

Equations

• MartinSchaeferKastner2025.ReflexiveSalient a = (a = Reference.Animacy.human)

def MartinSchaeferKastner2025.ReflexiveClashes : ControlLevel → Prop

The reflexive parse clashes with shared assumptions for a limited-control verb, whose change is not under the undergoer's control, and aligns with them for an in-control verb.

Equations

• MartinSchaeferKastner2025.ReflexiveClashes MartinSchaeferKastner2025.ControlLevel.limitedControl = True
• MartinSchaeferKastner2025.ReflexiveClashes MartinSchaeferKastner2025.ControlLevel.inControl = False

@[instance_reducible]

instance MartinSchaeferKastner2025.instDecidablePredAnimacyReflexiveSalient : DecidablePred ReflexiveSalient

Equations

• MartinSchaeferKastner2025.instDecidablePredAnimacyReflexiveSalient a = MartinSchaeferKastner2025.instDecidablePredAnimacyReflexiveSalient._aux_1 a

@[instance_reducible]

instance MartinSchaeferKastner2025.instDecidablePredControlLevelReflexiveClashes : DecidablePred ReflexiveClashes

Equations

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

inductive MartinSchaeferKastner2025.Preference : Type

The preferred form of a verb with a choice.

• unmarked : Preference
• marked : Preference

@[instance_reducible]

instance MartinSchaeferKastner2025.instDecidableEqPreference : DecidableEq Preference

Equations

• MartinSchaeferKastner2025.instDecidableEqPreference x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def MartinSchaeferKastner2025.preference (ctrl : ControlLevel) (anim : Reference.Animacy) (goal : ResponsibilityGoal) : Option Preference

The preference the Manner supermaxim predicts. Where the reflexive parse is salient, the speaker avoids the ambiguous form when that parse misleads and keeps it when the bare form's inference that no agent was intended misleads instead; where no parse is salient, the marked form is preferred only when the speaker means to convey responsibility, the reflexive parse being the only way to assign a nonhuman agency.

Equations

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

theorem MartinSchaeferKastner2025.generalizations (g : ResponsibilityGoal) (c : ControlLevel) {a : Reference.Animacy} (ha : a ≠ Reference.Animacy.human) : preference ControlLevel.limitedControl Reference.Animacy.human g = some Preference.unmarked ∧ preference ControlLevel.inControl Reference.Animacy.human g = some Preference.marked ∧ preference c a ResponsibilityGoal.conveyResponsibility = some Preference.marked ∧ preference c a ResponsibilityGoal.neutral = none

The three generalizations hold. With a human argument the limited-control verbs prefer the unmarked form and the in-control verbs the marked one, with a nonhuman argument the marked form is preferred to convey responsibility, and otherwise a nonhuman argument yields no preference.

theorem MartinSchaeferKastner2025.opposite_preferences_falsify_uniform_semantics (g : ResponsibilityGoal) : preference ControlLevel.limitedControl Reference.Animacy.human g ≠ preference ControlLevel.inControl Reference.Animacy.human g

Against the causation claim of [labelle-1992] and [labelle-doron-2010], the same class of verbs with a choice shows opposite preferences by control level, which no uniform semantic difference between the two forms could produce.

Unaccusativity

theorem MartinSchaeferKastner2025.cos_profiles_unaccusative : ArgumentStructure.PredictsUnaccusative French.Verbs.undergoer ∧ ArgumentStructure.PredictsUnaccusative French.Verbs.movingUndergoer

The entailments of the anticausatives' sole argument predict unaccusativity, since they impose no volition and no causation and include a patient entailment.