Liu and Rotter (2025): Linguistic and Social Meaning Match

This file formalizes the modal concord experiment of [LR25]. Modal concord doubles two modal elements of the same force and flavour, may possibly and must certainly; on the semantic-vacuity account of [Zei07] one element is uninterpretable, so a concord sentence and its single-modal counterpart should be truth-conditionally identical. The paper's 2 × 2 (force × number) Latin-square experiment on US English finds concord non-vacuous, and in opposite directions: doubling strengthens speaker commitment for necessity and weakens it for possibility, a force × number crossover, as the modal-spread account of [GM18] predicts (spreadEffect, spread_crossover, spread_refutes_vacuity). Confidence tracks commitment, the match of the title, while friendliness, warmth, and coolness show a force-blind penalty for doubling (warmthEffect, warmth_ne_spread). The observed shifts between the concord and single-modal cell means carry exactly these signs (commitment_matches_spread, confidence_matches_spread, warmth_matches_penalty).

Implementation notes

The effect of concord is a SignType; the regression estimates are not formal commitments. The cell means of the paper's Table 1 are rows of Data/Examples/LiuRotter2025.json, stored as hundredths of the 1–7 scale and read structurally, so the observed signs are decided in the kernel. The concord precondition, that the doubled elements share a concord class, is read off the English auxiliary fragment.

References

• [LR25]
• [Zei07]
• [GM18]

The concord effect as a force-indexed sign

def LiuRotter2025.spreadEffect : Modality.ModalForce → SignType

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

Equations

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

def LiuRotter2025.vacuityEffect : Modality.ModalForce → SignType

The semantic-vacuity account ([Zei07]): one modal carries an uninterpretable feature and contributes no operator, so concord has no commitment effect under any force.

Equations

• LiuRotter2025.vacuityEffect x✝ = 0

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

Concord is non-vacuous: it shifts commitment under both forces.

theorem LiuRotter2025.vacuity_no_interaction (f g : 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, already at necessity.

A second profile: the warmth penalty

The social-meaning measures split in two (Table 5). Confidence, and for necessity formality, track commitment and show the same crossover; friendliness, warmth, and coolness show a force-blind main effect of number, the concord sentence rated lower than the single modal under both forces.

def LiuRotter2025.warmthEffect : Modality.ModalForce → SignType

The warmth profile: a force-blind penalty for doubling.

Equations

• LiuRotter2025.warmthEffect x✝ = -1

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

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

theorem LiuRotter2025.warmth_ne_spread : warmthEffect ≠ spreadEffect

The warmth penalty is not the commitment crossover: it is constant where spread reverses.

The concord precondition in the fragment

def LiuRotter2025.SharesConcordForce (a b : Modality.ModalItem) : Prop

Two modal items share a concord class when a meaning of each has forces of one class, both universal or both existential.

Equations

• LiuRotter2025.SharesConcordForce a b = ∃ x ∈ a.meaning, ∃ y ∈ b.meaning, x.force.IsUniversal ↔ y.force.IsUniversal

@[instance_reducible]

instance LiuRotter2025.instDecidableRelModalItemSharesConcordForce : DecidableRel SharesConcordForce

Equations

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

theorem LiuRotter2025.must_certainly_share : SharesConcordForce English.Auxiliaries.must.toModalItem English.Adverbs.certainly

must and certainly, the necessity stimulus, share necessity-type force.

theorem LiuRotter2025.may_possibly_share : SharesConcordForce English.Auxiliaries.may.toModalItem English.Adverbs.possibly

may and possibly, the possibility stimulus, share possibility force.

Predicting against the data

The four condition cells carry the Table 1 means of every measure in hundredths of the 1–7 scale. An account predicts the sign of the concord shift, concord minus single modal, 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 concord and single-modal cell means, in hundredths.

• force : Modality.ModalForce
• mcMean : ℕ
• smMean : ℕ

@[instance_reducible]

instance LiuRotter2025.instDecidableEqShiftObservation : DecidableEq ShiftObservation

Equations

• LiuRotter2025.instDecidableEqShiftObservation = LiuRotter2025.instDecidableEqShiftObservation.decEq

def LiuRotter2025.instDecidableEqShiftObservation.decEq (x✝ x✝¹ : ShiftObservation) : Decidable (x✝ = x✝¹)

Equations

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

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

The observed sign of the concord shift.

Equations

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

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

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

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

Predicting a null effect, the vacuity account errs on every cell with a real shift.

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.

def LiuRotter2025.forceKey : Modality.ModalForce → String

The force feature value of a modal force.

Equations

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

def LiuRotter2025.findCell (force number : String) : Option Datum

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

Equations

• LiuRotter2025.findCell force number = List.find? (fun (e : Datum) => e.feature? "force" == some force && e.feature? "number" == some number) LiuRotter2025.Examples.all

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

The observed shift of a measure under a force, joining the concord and single-modal cells.

Equations

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

theorem LiuRotter2025.commitment_matches_spread : Option.map (fun (x : ShiftObservation) => x.observedSign) (observedShift "commitment" Modality.ModalForce.necessity) = some (spreadEffect Modality.ModalForce.necessity) ∧ Option.map (fun (x : ShiftObservation) => x.observedSign) (observedShift "commitment" Modality.ModalForce.possibility) = some (spreadEffect Modality.ModalForce.possibility)

Commitment shifts carry the spread sign: concord strengthens necessity and weakens possibility.

theorem LiuRotter2025.confidence_matches_spread : Option.map (fun (x : ShiftObservation) => x.observedSign) (observedShift "confidence" Modality.ModalForce.necessity) = some (spreadEffect Modality.ModalForce.necessity) ∧ Option.map (fun (x : ShiftObservation) => x.observedSign) (observedShift "confidence" Modality.ModalForce.possibility) = some (spreadEffect Modality.ModalForce.possibility)

Confidence tracks commitment: the match of linguistic and social meaning.

theorem LiuRotter2025.warmth_matches_penalty : Option.map (fun (x : ShiftObservation) => x.observedSign) (observedShift "warmth" Modality.ModalForce.necessity) = some (warmthEffect Modality.ModalForce.necessity) ∧ Option.map (fun (x : ShiftObservation) => x.observedSign) (observedShift "warmth" Modality.ModalForce.possibility) = some (warmthEffect Modality.ModalForce.possibility)

Warmth shifts carry the penalty sign under both forces.