Rotter and Liu (2025): A Register Approach to Modal (Non-)Concord in English

This file formalizes the second experiment of the paper, which adds a context factor, a close or a distant interlocutor, to the modal concord design of [LR25]: modal concord doubles a modal verb with a modal adverb of the same force, must certainly and may possibly, against the single modal. The concord analysis of [Zei07] predicts no effect of doubling on speaker commitment for either force, the modal-spread analysis of [GM18] a strengthening for universal modals and no effect for existential ones (spreadPred), so the two differ only on necessity (analyses_diverge_only_on_necessity). The cell means of the paper's tables are rows, and the shifts from the single modal to concord carry the signs of the first experiment in both contexts: strengthening for necessity, which adjudicates for spread (necessity_adjudicates), and weakening for possibility, which neither analysis predicts (possibility_residual), with confidence tracking commitment and a force-blind penalty on grammaticality, appropriateness, warmth, friendliness, and education. The paper's register question is answered by the absence of any number-by-context interaction: the sign of each concord shift is the same for the close and the distant interlocutor (context_invariant), as an additive context effect must leave it (not_registerSensitive_of_main_effect).

Implementation notes

The analyses and the observed effects are signs, as in the first experiment's study, whose ShiftObservation and rival accounts are reused. Cell means are rows of Data/Examples/RotterLiu2025.json, hundredths of the 1–7 scale read structurally, so the observed signs are decided in the kernel; regression estimates are not formal commitments. Register sensitivity is a difference in sign between the two contexts, and the context main effect is modelled as one additive shift on both cells of a pair.

References

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

The two analyses

@[reducible, inline]

abbrev RotterLiu2025.concordPred : Modality.ModalForce → SignType

The concord analysis: doubling has no commitment effect for any force.

Equations

• RotterLiu2025.concordPred = LiuRotter2025.vacuityEffect

def RotterLiu2025.spreadPred : Modality.ModalForce → SignType

The modal-spread analysis as the paper states it: doubling strengthens commitment for universal modals and maintains the default for existential ones.

Equations

• RotterLiu2025.spreadPred Modality.ModalForce.necessity = 1
• RotterLiu2025.spreadPred Modality.ModalForce.weakNecessity = 1
• RotterLiu2025.spreadPred Modality.ModalForce.possibility = 0

theorem RotterLiu2025.analyses_diverge_only_on_necessity : concordPred Modality.ModalForce.possibility = spreadPred Modality.ModalForce.possibility ∧ concordPred Modality.ModalForce.necessity ≠ spreadPred Modality.ModalForce.necessity

The analyses agree on existential modals and differ on universal ones, the one place the data can adjudicate.

theorem RotterLiu2025.necessity_adjudicates (o : LiuRotter2025.ShiftObservation) (hf : o.force = Modality.ModalForce.necessity) (h : o.smMean < o.mcMean) : o.observedSign = spreadPred o.force ∧ o.observedSign ≠ concordPred o.force

The necessity strengthening carries the sign the spread analysis predicts and the concord analysis does not.

theorem RotterLiu2025.possibility_residual (o : LiuRotter2025.ShiftObservation) (hf : o.force = Modality.ModalForce.possibility) (h : o.mcMean < o.smMean) : o.observedSign ≠ spreadPred o.force ∧ o.observedSign ≠ concordPred o.force

The possibility weakening carries a sign neither analysis predicts, both predicting maintenance.

Register sensitivity

def RotterLiu2025.RegisterSensitive (close distant : LiuRotter2025.ShiftObservation) : Prop

A concord effect is register-sensitive when its shift differs in sign between the close and the distant context.

Equations

• RotterLiu2025.RegisterSensitive close distant = (close.observedSign ≠ distant.observedSign)

theorem RotterLiu2025.context_main_effect_preserves_sign (o : LiuRotter2025.ShiftObservation) (c : ℕ) : { force := o.force, mcMean := o.mcMean + c, smMean := o.smMean + c }.observedSign = o.observedSign

A context main effect, the same additive shift on the concord and the single-modal cell, leaves the sign of the concord shift unchanged.

theorem RotterLiu2025.not_registerSensitive_of_main_effect (o : LiuRotter2025.ShiftObservation) (c : ℕ) : ¬RegisterSensitive o { force := o.force, mcMean := o.mcMean + c, smMean := o.smMean + c }

Contexts that differ by a main effect alone are not register-sensitive: no number-by-context interaction arises.

The cell means

def RotterLiu2025.findCell (context force number : String) : Option Datum

The cell of a context, force, and number.

Equations

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

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

The observed shift from the single modal to concord on a measure, in a context and under a force.

Equations

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

def RotterLiu2025.observedSign (measure context : String) (force : Modality.ModalForce) : Option SignType

The sign of the observed shift.

Equations

• RotterLiu2025.observedSign measure context force = Option.map LiuRotter2025.ShiftObservation.observedSign (RotterLiu2025.observedShift measure context force)

theorem RotterLiu2025.crossover (measure : String) : measure ∈ ["commitment", "confidence"] → ∀ context ∈ ["close", "distant"], observedSign measure context Modality.ModalForce.necessity = some 1 ∧ observedSign measure context Modality.ModalForce.possibility = some (-1)

The crossover of the first experiment replicates in both contexts: doubling strengthens commitment and confidence for necessity and weakens them for possibility.

theorem RotterLiu2025.penalty (measure : String) : measure ∈ ["grammaticality", "appropriateness", "warmth", "friendliness", "education"] → ∀ context ∈ ["close", "distant"], ∀ force ∈ [Modality.ModalForce.necessity, Modality.ModalForce.possibility], observedSign measure context force = some (-1)

The force-blind penalty: concord is rated lower than the single modal on grammaticality, appropriateness, warmth, friendliness, and education in every cell.

theorem RotterLiu2025.context_invariant (measure : String) : measure ∈ ["commitment", "confidence", "grammaticality", "appropriateness", "warmth", "friendliness", "education"] → ∀ force ∈ [Modality.ModalForce.necessity, Modality.ModalForce.possibility], observedSign measure "close" force = observedSign measure "distant" force

No number-by-context interaction: on every measure with a concord effect the shift has the same sign for the close and the distant interlocutor.

The first experiment

theorem RotterLiu2025.necessity_matches_experiment1 : spreadPred Modality.ModalForce.necessity = LiuRotter2025.spreadEffect Modality.ModalForce.necessity

On necessity the strengthening matches the spread prediction and the sign the first experiment reports.

theorem RotterLiu2025.possibility_observed_vs_predicted : LiuRotter2025.spreadEffect Modality.ModalForce.possibility ≠ spreadPred Modality.ModalForce.possibility

On possibility the first experiment's observed weakening diverges from the spread analysis's prediction: the gap is the residual.