[LR25]: Linguistic and Social Meaning Match — modal concord

Modal concord (MC) doubles two modal elements of the same force and flavor (may possibly, must certainly). The semantic-vacuity account ([Zei07]) treats one element as uninterpretable, so MC and the single modal (SM) should be truth-conditionally identical. [LR25] tests this in one 2×2 (FORCE × NUMBER) Latin-square experiment (93 of 104 US-English participants, Prolific) and finds MC is not vacuous: doubling strengthens speaker commitment for necessity but weakens it for possibility — a FORCE × NUMBER crossover (interaction β̂ = −1.85, χ²(1) = 41.51, p < .001; necessity sub-effect β̂ = +1.50, possibility β̂ = −0.35). The concord effect is thus a sign indexed by force, supporting the modal-spread analysis ([GM18]).

This file formalizes that structure, not the regression tables: the effect of concord as a force-indexed SignType, the crossover as the property that distinguishes the spread account from vacuity, and the data as a sign-prediction target.

Main definitions

• spreadEffect — [GM18]'s account: the force-indexed sign of the concord effect on commitment (+ for necessity, − for possibility).
• vacuityEffect — [Zei07]'s rival: the null effect, force-blind.
• warmthEffect — the force-blind MC warmth penalty (a second, distinct profile).
• ShiftObservation, accountErrs — score an account against the observed MC − SM shift in Data.Examples.LiuRotter2025.

Main results

• spread_crossover — the FORCE × NUMBER interaction as a sign reversal.
• spread_nonvacuous, spread_refutes_vacuity — MC is non-vacuous; a sign that reverses with force cannot be the agreement account's force-blind null.
• warmth_ne_spread — the warmth penalty is constant across force, so it is a NUMBER main effect, not the commitment crossover.
• vacuity_errs_on_shift — vacuity errs on every cell with a real shift.

Implementation notes

The effect of concord is a SignType (the magnitude is a model estimate, not a formal commitment); the rival accounts are ModalForce → SignType. Cell means live in Data.Examples.LiuRotter2025 (×100, on the 1–7 scale); they do not reduce in the kernel (string-keyed paperFeatures, ℚ comparison), so concrete shifts are computed via #eval while the kernel-checkable content is each account's systematic error.

The concord effect as a force-indexed sign

def LiuRotter2025.spreadEffect : Semantics.Modality.ModalForce → SignType

The modal-spread account ([GM18]): the modal adverb in an MC construction is not vacuous; doubling reinforces the force, raising speaker commitment for necessity (∀) and lowering it for possibility (∃).

Equations

• LiuRotter2025.spreadEffect Semantics.Modality.ModalForce.necessity = 1
• LiuRotter2025.spreadEffect Semantics.Modality.ModalForce.weakNecessity = 1
• LiuRotter2025.spreadEffect Semantics.Modality.ModalForce.possibility = -1

def LiuRotter2025.vacuityEffect : Semantics.Modality.ModalForce → SignType

The semantic-vacuity / syntactic-agreement account ([Zei07]): one modal carries an uninterpretable feature and contributes no operator at LF, so MC and SM are truth-conditionally identical — concord has no commitment effect, whatever the force.

Equations

• LiuRotter2025.vacuityEffect x✝ = 0

@[simp]

theorem LiuRotter2025.spreadEffect_necessity : spreadEffect Semantics.Modality.ModalForce.necessity = 1

@[simp]

theorem LiuRotter2025.spreadEffect_possibility : spreadEffect Semantics.Modality.ModalForce.possibility = -1

@[simp]

theorem LiuRotter2025.vacuityEffect_apply (f : Semantics.Modality.ModalForce) : vacuityEffect f = 0

theorem LiuRotter2025.spread_crossover : spreadEffect Semantics.Modality.ModalForce.necessity ≠ spreadEffect Semantics.Modality.ModalForce.possibility

The FORCE × NUMBER interaction: the concord effect reverses sign with force.

theorem LiuRotter2025.spread_nonvacuous : spreadEffect Semantics.Modality.ModalForce.necessity ≠ 0 ∧ spreadEffect Semantics.Modality.ModalForce.possibility ≠ 0

MC is semantically non-vacuous: concord shifts commitment under both forces.

theorem LiuRotter2025.vacuity_no_interaction (f g : Semantics.Modality.ModalForce) : vacuityEffect f = vacuityEffect g

Vacuity predicts no interaction: the (null) effect is the same for every force.

theorem LiuRotter2025.spread_refutes_vacuity : spreadEffect ≠ vacuityEffect

The crossover refutes vacuity: the spread effect disagrees with the agreement account's force-blind null already at necessity (+1 vs 0).

A second profile: the warmth penalty

Beyond commitment, the social-meaning measures split in two ([LR25] Table 5). Confidence — and, for necessity, formality — tracks commitment, showing the same force-indexed crossover (the "match" of the title: meaning strength and social perception move together). Friendliness, warmth, and coolness instead show a force-blind main effect of NUMBER: MC is rated lower than SM regardless of force, a uniform social cost of doubling.

def LiuRotter2025.warmthEffect : Semantics.Modality.ModalForce → SignType

The warmth profile: a force-blind penalty. MC is perceived as less warm (friendly, warm, cool) than SM under both forces — a NUMBER main effect with no interaction, distinct from the commitment crossover.

Equations

• LiuRotter2025.warmthEffect x✝ = -1

theorem LiuRotter2025.warmth_no_interaction (f g : Semantics.Modality.ModalForce) : warmthEffect f = warmthEffect g

theorem LiuRotter2025.warmth_real_cost (f : Semantics.Modality.ModalForce) : warmthEffect f ≠ 0

theorem LiuRotter2025.warmth_ne_spread : warmthEffect ≠ spreadEffect

The warmth penalty is not the commitment crossover: it disagrees with the spread effect at necessity (−1 vs +1), being constant where spread reverses.

The concord precondition in the fragment

Both MC stimulus pairs share concord-compatible force — the structural precondition for concord ([Zei07]). The auxiliaries carry uninterpretable features in the fragment, so the agreement account's vacuous element is must/may; the crossover overturns its prediction that this element contributes nothing.

theorem LiuRotter2025.must_certainly_share : English.Auxiliaries.must.toModalItem.sharesConcordForce English.Auxiliaries.certainly.toModalItem = true

must + certainly (the necessity MC stimulus) share necessity-type force.

theorem LiuRotter2025.may_possibly_share : English.Auxiliaries.may.toModalItem.sharesConcordForce English.Auxiliaries.possibly.toModalItem = true

may + possibly (the possibility MC stimulus) share possibility force.

theorem LiuRotter2025.stimulus_auxiliaries_uninterpretable : English.Auxiliaries.must.interpretability = some Semantics.Modality.ModalInterpretability.uninterpretable ∧ English.Auxiliaries.may.interpretability = some Semantics.Modality.ModalInterpretability.uninterpretable

Zeijlstra's vacuous element: the modal auxiliaries are uninterpretable in the fragment, so under the agreement account they contribute no operator.

Predicting against the data

The four condition cells (Data.Examples.LiuRotter2025) carry the Table 1 means (×100, on the 1–7 Likert scale) for every measure. An account predicts the sign of the concord shift MC − SM per force; the observed sign is read off the cell means.

structure LiuRotter2025.ShiftObservation : Type

An observed concord shift for one measure under one force: the MC and SM cell means.

• force : Semantics.Modality.ModalForce
• mcMean : ℚ
• smMean : ℚ

def LiuRotter2025.ShiftObservation.observedSign (o : ShiftObservation) : SignType

The observed sign of the concord shift (MC − SM).

Equations

• o.observedSign = SignType.sign (o.mcMean - o.smMean)

def LiuRotter2025.accountErrs (acc : Semantics.Modality.ModalForce → SignType) (o : ShiftObservation) : Prop

An account errs on an observation when its predicted sign disagrees with the observed shift sign.

Equations

• LiuRotter2025.accountErrs acc o = (acc o.force ≠ o.observedSign)

theorem LiuRotter2025.vacuity_errs_on_shift (o : ShiftObservation) (h : o.mcMean ≠ o.smMean) : accountErrs vacuityEffect o

The agreement account errs on every cell with a real shift: predicting a null effect, it cannot match any nonzero MC − SM difference.

theorem LiuRotter2025.spread_correct_of_match (o : ShiftObservation) (h : o.observedSign = spreadEffect o.force) : ¬accountErrs spreadEffect o

When the observed shift carries the sign the spread account predicts, the account does not err — the content the agreement account cannot deliver.

The observed shifts

forceKey/findCell/observedShift join the MC and SM cells of Examples.all to read the observed sign for any measure. The #evals exhibit the paper's findings: the spread sign predicts both commitment and confidence (the crossover, ±1 by force), while warmth is a uniform penalty (−1 under both forces). Means do not reduce in the kernel, so these are computed, not proved.

def LiuRotter2025.forceKey : Semantics.Modality.ModalForce → String

The paperFeatures force value for a modal force.

Equations

• LiuRotter2025.forceKey Semantics.Modality.ModalForce.necessity = "necessity"
• LiuRotter2025.forceKey Semantics.Modality.ModalForce.weakNecessity = "necessity"
• LiuRotter2025.forceKey Semantics.Modality.ModalForce.possibility = "possibility"

def LiuRotter2025.findCell (force number : String) : Option Data.Examples.LinguisticExample

The cell with the given force and number ("MC"/"SM") values.

Equations

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

def LiuRotter2025.cellMean (measure : String) (e : Data.Examples.LinguisticExample) : Option ℚ

Read a Likert mean (stored ×100) for measure from a cell's features.

Equations

• LiuRotter2025.cellMean measure e = (List.lookup measure e.paperFeatures).bind fun (s : String) => Option.map (fun (n : ℚ) => n / 100) do let a ← s.toNat? pure ↑a

def LiuRotter2025.observedShift (measure : String) (force : Semantics.Modality.ModalForce) : Option ShiftObservation

The observed MC − SM shift for measure under force, joining the cells.

Equations

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