Documentation

Linglib.Phenomena.Modality.Studies.LiuRotter2025

Modal Concord Bridge — @cite{rotter-liu-2025} #

@cite{liu-rotter-2025} @cite{rotter-liu-2025}

Connects Liu & Rotter's empirical data to the English modal and adverb fragments, the general concord infrastructure, and @cite{rotter-liu-2025}.

Section A: Semantic overlap via ModalItem #

Each experimental aux-adverb pair shares modal force when projected to the shared ModalItem type. This is the structural precondition for concord.

Section B: Force determines commitment direction #

The paper's FORCE × NUMBER interaction can be predicted from modal force: necessity doubling strengthens, possibility doubling weakens.

Section C: Connection to @cite{rotter-liu-2025} #

Both studies find that MC preserves modal force (single reading, not double).

Section D: Cross-phenomenon concord #

Modal concord is an instance of the general concord pattern. Possibility MC patterns with negative concord (solidarity), necessity MC contrasts (competence).

Section A: Semantic overlap via ModalItem #

Each aux-adverb pair from the stimuli shares concord-compatible force when projected to ModalItem. Both necessity and weak necessity map to the same concord class (necessity-type), so should (weak necessity) concords with definitely (necessity).

source
theorem Phenomena.Modality.ModalConcord.LiuRotter2025.Bridge.must_certainly_share :
Fragments.English.FunctionWords.must.toModalItem.sharesConcordForce Fragments.English.FunctionWords.certainly.toModalItem = true

must + certainly share necessity-type concord force.

source
theorem Phenomena.Modality.ModalConcord.LiuRotter2025.Bridge.should_definitely_share :
Fragments.English.FunctionWords.should.toModalItem.sharesConcordForce Fragments.English.FunctionWords.definitely.toModalItem = true

should + definitely share necessity-type concord force. should is weak necessity, definitely is strong necessity — both are necessity-type for concord purposes.

source
theorem Phenomena.Modality.ModalConcord.LiuRotter2025.Bridge.haveTo_necessarily_share :
Fragments.English.FunctionWords.haveTo.toModalItem.sharesConcordForce Fragments.English.FunctionWords.necessarily.toModalItem = true

have to + necessarily share necessity-type concord force.

source
theorem Phenomena.Modality.ModalConcord.LiuRotter2025.Bridge.may_possibly_share :
Fragments.English.FunctionWords.may.toModalItem.sharesConcordForce Fragments.English.FunctionWords.possibly.toModalItem = true

may + possibly share possibility force.

source
theorem Phenomena.Modality.ModalConcord.LiuRotter2025.Bridge.might_perhaps_share :
Fragments.English.FunctionWords.might.toModalItem.sharesConcordForce Fragments.English.FunctionWords.perhaps.toModalItem = true

might + perhaps share possibility force.

source
theorem Phenomena.Modality.ModalConcord.LiuRotter2025.Bridge.could_potentially_share :
Fragments.English.FunctionWords.could.toModalItem.sharesConcordForce Fragments.English.FunctionWords.potentially.toModalItem = true

could + potentially share possibility force.

source
theorem Phenomena.Modality.ModalConcord.LiuRotter2025.Bridge.all_pairs_share_force :
Fragments.English.FunctionWords.must.toModalItem.sharesConcordForce Fragments.English.FunctionWords.certainly.toModalItem = true ∧ Fragments.English.FunctionWords.should.toModalItem.sharesConcordForce Fragments.English.FunctionWords.definitely.toModalItem = true ∧ Fragments.English.FunctionWords.haveTo.toModalItem.sharesConcordForce Fragments.English.FunctionWords.necessarily.toModalItem = true ∧ Fragments.English.FunctionWords.may.toModalItem.sharesConcordForce Fragments.English.FunctionWords.possibly.toModalItem = true ∧ Fragments.English.FunctionWords.might.toModalItem.sharesConcordForce Fragments.English.FunctionWords.perhaps.toModalItem = true ∧ Fragments.English.FunctionWords.could.toModalItem.sharesConcordForce Fragments.English.FunctionWords.potentially.toModalItem = true

All six stimulus pairs share concord-compatible force.

source
theorem Phenomena.Modality.ModalConcord.LiuRotter2025.Bridge.must_certainly_same_register :
Fragments.English.FunctionWords.must.toModalItem.areRegisterVariants Fragments.English.FunctionWords.certainly.toModalItem = false

must (formal) and certainly (formal) are NOT register variants — they share the same register level. Concord here is not register mixing but force agreement between syntactically distinct categories.

source
theorem Phenomena.Modality.ModalConcord.LiuRotter2025.Bridge.may_possibly_same_register :
Fragments.English.FunctionWords.may.toModalItem.areRegisterVariants Fragments.English.FunctionWords.possibly.toModalItem = false

may (neutral) and possibly (neutral) are also not register variants.

Section B: Force determines commitment direction #

The paper's central finding — that necessity MC strengthens while possibility MC weakens — can be encoded as a function from modal force to predicted direction.

source
def Phenomena.Modality.ModalConcord.LiuRotter2025.Bridge.concordStrengthens :
Core.Modality.ModalForce → Bool

Predicted commitment effect of concord given modal force. true = strengthening (MC > SM), false = weakening (MC < SM). Both necessity and weak necessity concord strengthen.

Equations
Instances For
    source
    theorem Phenomena.Modality.ModalConcord.LiuRotter2025.Bridge.necessity_matches_prediction :
    concordStrengthens Core.Modality.ModalForce.necessity = true ∧ (commitmentRating necMC).mean > (commitmentRating necSM).mean

    The data matches the force-based prediction for necessity.

    source
    theorem Phenomena.Modality.ModalConcord.LiuRotter2025.Bridge.possibility_matches_prediction :
    concordStrengthens Core.Modality.ModalForce.possibility = false ∧ (commitmentRating posMC).mean < (commitmentRating posSM).mean

    The data matches the force-based prediction for possibility.

    Section C: Connection to @cite{rotter-liu-2025} #

    Both studies agree that MC preserves modal force (single reading).

    source
    theorem Phenomena.Modality.ModalConcord.LiuRotter2025.Bridge.both_studies_single_necessity :
    (meaningRating Condition.must).mean - (meaningRating Condition.mustHaveTo).mean < 1 / 2 ∧ (commitmentRating necMC).mean > 4

    Both studies: necessity MC yields single necessity.

    source
    theorem Phenomena.Modality.ModalConcord.LiuRotter2025.Bridge.complementary_diagnostics :
    (formalityRating Condition.haveTo).mean < (formalityRating Condition.mustHaveTo).mean ∧ (commitmentRating necMC).mean ≠ (commitmentRating necSM).mean

    Register and commitment are complementary diagnostics.

    Section D: Cross-phenomenon concord #

    Modal concord is an instance of the general ConcordType from Core/ModalLogic.lean. The social indexation of MC depends on force: necessity MC → competence, possibility MC → solidarity. This connects to negative concord, which also indexes solidarity.

    The socialIndex mapping is defined here (not in Core) because it encodes an empirical claim from @cite{rotter-liu-2025} §4.

    source
    def Phenomena.Modality.ModalConcord.LiuRotter2025.Bridge.socialIndex :
    Core.Modality.ConcordType → Core.Register.SocialIndex

    Social indexation of each concord type. NC and MC possibility both index solidarity; MC necessity indexes competence (@cite{rotter-liu-2025} §4).

    Equations
    Instances For
      source
      theorem Phenomena.Modality.ModalConcord.LiuRotter2025.Bridge.necessity_mc_competence :
      socialIndex (Core.Modality.ConcordType.fromModalForce Core.Modality.ModalForce.necessity) = Core.Register.SocialIndex.competence

      Necessity MC is a competence-indexing concord phenomenon.

      source
      theorem Phenomena.Modality.ModalConcord.LiuRotter2025.Bridge.possibility_mc_solidarity :
      socialIndex (Core.Modality.ConcordType.fromModalForce Core.Modality.ModalForce.possibility) = Core.Register.SocialIndex.solidarity

      Possibility MC is a solidarity-indexing concord phenomenon.

      source
      theorem Phenomena.Modality.ModalConcord.LiuRotter2025.Bridge.possibility_mc_like_nc :
      socialIndex (Core.Modality.ConcordType.fromModalForce Core.Modality.ModalForce.possibility) = socialIndex Core.Modality.ConcordType.negation

      Possibility MC patterns with negative concord: Both are solidarity-indexing concord phenomena. This is the cross-phenomenon generalization from @cite{rotter-liu-2025} §4.

      source
      theorem Phenomena.Modality.ModalConcord.LiuRotter2025.Bridge.necessity_mc_unlike_nc :
      socialIndex (Core.Modality.ConcordType.fromModalForce Core.Modality.ModalForce.necessity) ≠ socialIndex Core.Modality.ConcordType.negation

      Necessity MC contrasts with negative concord.

      source
      theorem Phenomena.Modality.ModalConcord.LiuRotter2025.Bridge.force_determines_social_index :
      socialIndex Core.Modality.ConcordType.modalNecessity ≠ socialIndex Core.Modality.ConcordType.modalPossibility

      Force determines social meaning: Necessity and possibility modal concord receive opposite social indexation.

      source
      theorem Phenomena.Modality.ModalConcord.LiuRotter2025.Bridge.social_index_aligns_with_commitment :
      socialIndex (Core.Modality.ConcordType.fromModalForce Core.Modality.ModalForce.necessity) = Core.Register.SocialIndex.competence ∧ (commitmentRating necMC).mean > (commitmentRating necSM).mean ∧ socialIndex (Core.Modality.ConcordType.fromModalForce Core.Modality.ModalForce.possibility) = Core.Register.SocialIndex.solidarity ∧ (commitmentRating posMC).mean < (commitmentRating posSM).mean

      Social meaning mirrors commitment direction: The concord type's social index aligns with the commitment data — competence-indexing necessity MC strengthens commitment, solidarity-indexing possibility MC weakens it.