@cite{ciardelli-guerrini-2026} — Against Wide Scope Free Choice

@cite{ciardelli-guerrini-2026} @cite{zeijlstra-2007}

Semantics and Pragmatics 19(4). 2026.

The Reductionist Thesis

The free-choice reading of sentences like "You may A or you may B" does NOT arise from the wide-scope LF ◇A ∨ ◇B. It arises from the narrow-scope LF ◇(A ∨ B). There is no separate problem of "wide-scope free choice."

The two LFs are truth-conditionally equivalent in standard modal logic (diamond_distributes_iff). The difference is compositional: only ◇(A ∨ B) feeds into pragmatic enrichment mechanisms (exhaustification, RSA, BSML) that derive the conjunctive free-choice inference ◇A ∧ ◇B.

Evidence (§2)

"MOD A COORD MOD B" sentences are systematically scope-ambiguous:

Surface form	Wide-scope LF	Narrow-scope LF
may A or may B	◇A ∨ ◇B	◇(A ∨ B)
must A or must B	□A ∨ □B	□(A ∨ B)
may A and may B	◇A ∧ ◇B	◇(A ∧ B)

• Must-or-must: "You must write an essay or you must give a presentation" naturally receives the narrow-scope reading □(essay ∨ presentation) — a disjunctive obligation, not uncertainty between two obligations.

• May-and-may: "You may go to Bob's party and you may go to Charlie's party" naturally receives the narrow-scope reading ◇(Bob ∧ Charlie) — permission to attend BOTH, not two separate permissions.

Compositional Mechanism (§3)

The narrow-scope LF arises via modal concord (@cite{zeijlstra-2007}). Modal auxiliaries carry uninterpretable features [u∃/∀-MOD]. When two auxiliaries with the same feature appear in a coordination, a single silent operator [i∃/∀-MOD] c-commands the coordination and checks both features. The silent operator is semantically interpreted; the auxiliaries are vacuous. This yields Δ(A ∘ B), not ΔA ∘ ΔB.

Key Predictions (§4)

1. Auxiliary vs non-auxiliary: Non-auxiliary modal constructions ("it's ok that", "be allowed to") carry interpretable features and cannot participate in concord → no FC reading in coordination.

2. Either position: Initial "either" does not block narrow-scope readings, contra @cite{meyer-sauerland-2017}, because the silent operator can check features from above "either."

3. Negation flips force for concord: derived from ModalForce.dual — ALLOWi∃ is well-formed because ¬∀ = ∃ = dual(∀).

The Two LFs are Truth-Conditionally Equivalent

In standard modal logic, ◇(A ∨ B) ↔ ◇A ∨ ◇B. The forward direction is diamond_distributes (from Exhaustification/FreeChoice.lean). The reverse is trivially provable. This equivalence is the point of C&G: the scope distinction cannot be detected truth-conditionally — it matters only for compositional derivation and pragmatic enrichment.

inductive CiardelliGuerrini2026.ModalCoordScope : Type

Scope availability for "MOD A COORD MOD B" sentences.

• wideOnly : ModalCoordScope
• narrowOnly : ModalCoordScope
• ambiguous : ModalCoordScope

@[implicit_reducible]

instance CiardelliGuerrini2026.instDecidableEqModalCoordScope : DecidableEq ModalCoordScope

Equations

• CiardelliGuerrini2026.instDecidableEqModalCoordScope x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance CiardelliGuerrini2026.instReprModalCoordScope : Repr ModalCoordScope

Equations

• CiardelliGuerrini2026.instReprModalCoordScope = { reprPrec := CiardelliGuerrini2026.instReprModalCoordScope.repr }

def CiardelliGuerrini2026.instReprModalCoordScope.repr : ModalCoordScope → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CiardelliGuerrini2026.instBEqModalCoordScope : BEq ModalCoordScope

Equations

• CiardelliGuerrini2026.instBEqModalCoordScope = { beq := CiardelliGuerrini2026.instBEqModalCoordScope.beq }

def CiardelliGuerrini2026.instBEqModalCoordScope.beq : ModalCoordScope → ModalCoordScope → Bool

Equations

• CiardelliGuerrini2026.instBEqModalCoordScope.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure CiardelliGuerrini2026.ScopeAmbiguityDatum : Type

A scope ambiguity datum for "MOD A COORD MOD B" sentences.

• sentence : String
• coord : String
• modalForce : Core.Modality.ModalForce
• dominantReading : String

  Which reading is dominant in context?

• scopeAvailability : ModalCoordScope

  Is the sentence scope-ambiguous?

def CiardelliGuerrini2026.instReprScopeAmbiguityDatum.repr : ScopeAmbiguityDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CiardelliGuerrini2026.instReprScopeAmbiguityDatum : Repr ScopeAmbiguityDatum

Equations

• CiardelliGuerrini2026.instReprScopeAmbiguityDatum = { reprPrec := CiardelliGuerrini2026.instReprScopeAmbiguityDatum.repr }

def CiardelliGuerrini2026.mayOrMay : ScopeAmbiguityDatum

(2) "You may do A or you may do B" — FC reading from narrow-scope.

Equations

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

def CiardelliGuerrini2026.mustOrMust : ScopeAmbiguityDatum

(5) "You must write an essay or you must give a presentation."

Equations

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

def CiardelliGuerrini2026.mayAndMay : ScopeAmbiguityDatum

(7) "You may go to Bob's party and you may go to Charlie's party."

Equations

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

def CiardelliGuerrini2026.scopeData : List ScopeAmbiguityDatum

Equations

• CiardelliGuerrini2026.scopeData = [CiardelliGuerrini2026.mayOrMay, CiardelliGuerrini2026.mustOrMust, CiardelliGuerrini2026.mayAndMay]

theorem CiardelliGuerrini2026.all_ambiguous : (scopeData.all fun (x : ScopeAmbiguityDatum) => x.scopeAvailability == ModalCoordScope.ambiguous) = true

All MOD-COORD-MOD sentences are scope-ambiguous (central claim).

Deriving Narrow-Scope LF via Modal Concord

@cite{zeijlstra-2007}'s feature system explains how the narrow-scope LF ◇(A ∨ B) arises compositionally for "may A or may B":

1. Each "may" carries [u∃-MOD] (uninterpretable existential feature)
2. A silent ◇ operator [i∃-MOD] is projected above the coordination
3. The silent operator checks both [u∃-MOD] features in the conjuncts
4. Only the silent operator is semantically interpreted → ◇(A ∨ B)

def CiardelliGuerrini2026.mayFeature : Core.Modality.ModalFeature

The modal feature carried by English "may" — fully derived from the Fragment entry's force AND interpretability.

Equations

• CiardelliGuerrini2026.mayFeature = Fragments.English.Auxiliaries.may.toModalFeature.get!

def CiardelliGuerrini2026.mustFeature : Core.Modality.ModalFeature

The modal feature carried by English "must" — fully derived from Fragment.

Equations

• CiardelliGuerrini2026.mustFeature = Fragments.English.Auxiliaries.must.toModalFeature.get!

theorem CiardelliGuerrini2026.may_feature_eq : Fragments.English.Auxiliaries.may.toModalFeature = some { force := Core.Modality.ModalForce.possibility, interp := Core.Modality.ModalInterpretability.uninterpretable }

"May" carries [u∃-MOD]: possibility force, uninterpretable.

theorem CiardelliGuerrini2026.must_feature_eq : Fragments.English.Auxiliaries.must.toModalFeature = some { force := Core.Modality.ModalForce.necessity, interp := Core.Modality.ModalInterpretability.uninterpretable }

"Must" carries [u∀-MOD]: necessity force, uninterpretable.

def CiardelliGuerrini2026.silentChecker (f : Core.Modality.ModalFeature) : Core.Modality.ModalFeature

The silent operator that checks a given u-feature: same force, but interpretable. This is the operator C&G posit above the coordination.

Equations

• CiardelliGuerrini2026.silentChecker f = { force := f.force, interp := Core.Modality.ModalInterpretability.interpretable }

theorem CiardelliGuerrini2026.silent_checker_works (f : Core.Modality.ModalFeature) (h : f.interp = Core.Modality.ModalInterpretability.uninterpretable) : (silentChecker f).checks f = true

Core derivation: for any u-feature, the matching silent operator checks it. This is the general form of C&G's concord mechanism — not just "may" or "must", but ANY auxiliary carrying a u-feature.

ConcordDerivation: packaging the full derivation chain

structure CiardelliGuerrini2026.ConcordDerivation : Type

A concord derivation witnesses that two modal features can be checked by a single silent operator. This is the formal content of @cite{ciardelli-guerrini-2026}'s compositional mechanism.

A ConcordDerivation exists iff:

1. Both features are uninterpretable (u-MOD)
2. They belong to the same concord class (both ∃-type or both ∀-type)

The silent operator, checking proofs, and resulting narrow-scope interpretation are all derived automatically from these two conditions.

• f₁ : Core.Modality.ModalFeature

  The feature of the first modal auxiliary

• f₂ : Core.Modality.ModalFeature

  The feature of the second modal auxiliary

• uInterp₁ : self.f₁.interp = Core.Modality.ModalInterpretability.uninterpretable

  Both are uninterpretable

• uInterp₂ : self.f₂.interp = Core.Modality.ModalInterpretability.uninterpretable
• sameClass : Core.Modality.ConcordType.fromModalForce self.f₁.force = Core.Modality.ConcordType.fromModalForce self.f₂.force

  Same concord class

def CiardelliGuerrini2026.ConcordDerivation.checker (cd : ConcordDerivation) : Core.Modality.ModalFeature

The silent interpretable operator — derived, not stipulated.

Equations

• cd.checker = CiardelliGuerrini2026.silentChecker cd.f₁

theorem CiardelliGuerrini2026.ConcordDerivation.checker_interpretable (cd : ConcordDerivation) : cd.checker.interp = Core.Modality.ModalInterpretability.interpretable

The checker is interpretable (semantically active).

theorem CiardelliGuerrini2026.ConcordDerivation.checks_first (cd : ConcordDerivation) : cd.checker.checks cd.f₁ = true

The checker checks the first feature.

theorem CiardelliGuerrini2026.ConcordDerivation.checks_second (cd : ConcordDerivation) : cd.checker.checks cd.f₂ = true

The checker checks the second feature.

def CiardelliGuerrini2026.ConcordDerivation.fromAux (a₁ a₂ : Fragments.English.Auxiliaries.AuxEntry) {f₁ f₂ : Core.Modality.ModalFeature} (_h₁ : a₁.toModalFeature = some f₁) (_h₂ : a₂.toModalFeature = some f₂) (hI₁ : f₁.interp = Core.Modality.ModalInterpretability.uninterpretable) (hI₂ : f₂.interp = Core.Modality.ModalInterpretability.uninterpretable) (hF : Core.Modality.ConcordType.fromModalForce f₁.force = Core.Modality.ConcordType.fromModalForce f₂.force) : ConcordDerivation

Construct a ConcordDerivation from two AuxEntrys. The derivation is built entirely from Fragment data — no stipulation.

Equations

• CiardelliGuerrini2026.ConcordDerivation.fromAux a₁ a₂ _h₁ _h₂ hI₁ hI₂ hF = { f₁ := f₁, f₂ := f₂, uInterp₁ := hI₁, uInterp₂ := hI₂, sameClass := hF }

Universal modal properties

def CiardelliGuerrini2026.modalAuxiliaries : List Fragments.English.Auxiliaries.AuxEntry

The modal auxiliaries that participate in concord: all entries in the Fragment with uninterpretable features.

Equations

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

theorem CiardelliGuerrini2026.modal_aux_count : modalAuxiliaries.length = 13

Exactly 13 English modal auxiliaries carry u-features.

def CiardelliGuerrini2026.concordCapableModals : List Fragments.English.Auxiliaries.AuxEntry

Modal auxiliaries with modal meaning (i.e., those that can form ConcordDerivations). Excludes dare which has u-features but no modal meaning specification.

Equations

• CiardelliGuerrini2026.concordCapableModals = List.filter (fun (a : Fragments.English.Auxiliaries.AuxEntry) => a.toModalFeature.isSome) CiardelliGuerrini2026.modalAuxiliaries

theorem CiardelliGuerrini2026.concord_capable_count : concordCapableModals.length = 12

12 of 13 modal auxiliaries have derivable modal features.

theorem CiardelliGuerrini2026.concord_capable_all_uninterpretable : (concordCapableModals.all fun (a : Fragments.English.Auxiliaries.AuxEntry) => decide ((a.interpretability == some Core.Modality.ModalInterpretability.uninterpretable) = true)) = true

Every concord-capable modal's feature is uninterpretable.

theorem CiardelliGuerrini2026.do_no_feature : Fragments.English.Auxiliaries.do_.toModalFeature = none

Non-modal auxiliaries have no modal feature — they cannot participate in concord at all.

theorem CiardelliGuerrini2026.be_no_feature : Fragments.English.Auxiliaries.am.toModalFeature = none

theorem CiardelliGuerrini2026.have_no_feature : Fragments.English.Auxiliaries.have_.toModalFeature = none

Instantiations

def CiardelliGuerrini2026.mayMayConcord : ConcordDerivation

"May A or may B" concord derivation — fully derived from Fragment.

Equations

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

def CiardelliGuerrini2026.mustMustConcord : ConcordDerivation

"Must A or must B" concord derivation — fully derived from Fragment.

Equations

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

theorem CiardelliGuerrini2026.cross_force_blocked : (silentChecker mustFeature).checks mayFeature = false

Cross-force checking fails: silent □ cannot check "may"[u∃].

The Full Pipeline: From Lexical Features to Free Choice

This is the deepest formalization of @cite{ciardelli-guerrini-2026}'s reductionist thesis. The pipeline has three stages:

1. Feature matching → ConcordDerivation (§3 above)
2. Narrow scope → single modal operator over coordination
3. Exhaustification → free choice inference

The key insight: the narrow-scope / wide-scope distinction is truth-conditionally vacuous (scope_equivalence) but pragmatically active — exhaustification produces opposite results:

• Narrow scope: Exh²(◇(A∨B)) → ◇A ∧ ◇B (free choice: both permitted)
• Wide scope: Exh(◇A ∨ ◇B) → ¬(◇A ∧ ◇B) (exclusive: at most one)

theorem CiardelliGuerrini2026.narrowScope_yields_fc {World : Type u_1} (A B : Set World) (hExh : { p := A, q := B }.exh2) : Exhaustification.FreeChoice.diamond A ∧ Exhaustification.FreeChoice.diamond B

The free choice pipeline: narrow-scope ◇(A∨B), when doubly exhaustified, yields free choice ◇A ∧ ◇B.

This IS the reductionist thesis in action: FC arises from the narrow-scope LF (derived via concord) fed to the standard exhaustification mechanism. Uses free_choice_forward from Exhaustification/FreeChoice.lean.

def CiardelliGuerrini2026.wideScopeExh {World : Type u_1} (A B : Set World) : Prop

Wide-scope exhaustification: Exh(◇A ∨ ◇B) asserts the disjunction while negating the conjunction — yielding exclusive disjunction.

This is the standard scalar implicature for disjunction: "A or B" implicates "not both."

Equations

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

theorem CiardelliGuerrini2026.wideScope_blocks_fc {World : Type u_1} (A B : Set World) (h : wideScopeExh A B) : ¬(Exhaustification.FreeChoice.diamond A ∧ Exhaustification.FreeChoice.diamond B)

Wide-scope exhaustification is incompatible with free choice. FC = ◇A ∧ ◇B, but wide-scope Exh asserts ¬(◇A ∧ ◇B).

theorem CiardelliGuerrini2026.scope_equivalence {World : Type u_1} (A B : Set World) : Exhaustification.FreeChoice.diamond (A ∪ B) ↔ Exhaustification.FreeChoice.diamond A ∨ Exhaustification.FreeChoice.diamond B

Truth-conditional equivalence: the scope distinction is semantically vacuous. ◇(A∨B) ↔ ◇A∨◇B in standard modal logic.

theorem CiardelliGuerrini2026.reductionist_thesis {World : Type u_1} (A B : Set World) : ({ p := A, q := B }.exh2 → Exhaustification.FreeChoice.diamond A ∧ Exhaustification.FreeChoice.diamond B) ∧ (wideScopeExh A B → ¬(Exhaustification.FreeChoice.diamond A ∧ Exhaustification.FreeChoice.diamond B))

The Reductionist Thesis (@cite{ciardelli-guerrini-2026}, formalized).

Despite truth-conditional equivalence (scope_equivalence), the two LFs diverge under pragmatic enrichment:

1. Narrow scope + Exh² → FC (both permitted)
2. Wide scope + Exh → ¬FC (at most one)

There is no separate problem of "wide-scope free choice" — the FC reading arises exclusively from the narrow-scope LF, which is derived via modal concord (ConcordDerivation).

Prediction: Non-Auxiliary Modals Block FC in Coordination

@cite{meyer-sauerland-2017} observed that (19a-b) lack FC readings:

(19a) It's ok for John to sing or it's ok for John to dance. (*FC) (19b) John is allowed to sing or he is allowed to dance. (*FC)

@cite{ciardelli-guerrini-2026} explain this: "it's ok" and "be allowed" carry interpretable features. They cannot participate in concord with a higher silent operator, so no narrow-scope LF is available.

Modal auxiliaries ("may", "must", "can") carry uninterpretable features and CAN participate in concord → FC available.

The auxiliary status of "may", "must", "can", "need" is derived from Fragments.English.FunctionWords — they are all .modal entries.

theorem CiardelliGuerrini2026.may_is_modal : Fragments.English.Auxiliaries.may.auxType = Fragments.English.Auxiliaries.AuxType.modal

Fragment-derived: all English modals used by C&G are modal auxiliaries with uninterpretable features.

theorem CiardelliGuerrini2026.must_is_modal : Fragments.English.Auxiliaries.must.auxType = Fragments.English.Auxiliaries.AuxType.modal

theorem CiardelliGuerrini2026.can_is_modal : Fragments.English.Auxiliaries.can.auxType = Fragments.English.Auxiliaries.AuxType.modal

theorem CiardelliGuerrini2026.need_is_modal : Fragments.English.Auxiliaries.need.auxType = Fragments.English.Auxiliaries.AuxType.modal

theorem CiardelliGuerrini2026.may_uninterpretable : Fragments.English.Auxiliaries.may.interpretability = some Core.Modality.ModalInterpretability.uninterpretable

All C&G modals carry uninterpretable features in the Fragment.

theorem CiardelliGuerrini2026.must_uninterpretable : Fragments.English.Auxiliaries.must.interpretability = some Core.Modality.ModalInterpretability.uninterpretable

theorem CiardelliGuerrini2026.can_uninterpretable : Fragments.English.Auxiliaries.can.interpretability = some Core.Modality.ModalInterpretability.uninterpretable

theorem CiardelliGuerrini2026.need_uninterpretable : Fragments.English.Auxiliaries.need.interpretability = some Core.Modality.ModalInterpretability.uninterpretable

structure CiardelliGuerrini2026.NonAuxModalDatum : Type

Non-auxiliary modal constructions — these have no Fragment entry because they are multi-word periphrastic constructions, not single-word auxiliaries in Zwicky & Pullum's sense. Their absence from the auxiliary lexicon IS the prediction: no AuxEntry → no uninterpretable feature → no concord → no narrow-scope LF.

• form : String
• fcInCoordination : Bool

def CiardelliGuerrini2026.instReprNonAuxModalDatum.repr : NonAuxModalDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CiardelliGuerrini2026.instReprNonAuxModalDatum : Repr NonAuxModalDatum

Equations

• CiardelliGuerrini2026.instReprNonAuxModalDatum = { reprPrec := CiardelliGuerrini2026.instReprNonAuxModalDatum.repr }

def CiardelliGuerrini2026.nonAuxData : List NonAuxModalDatum

Equations

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

theorem CiardelliGuerrini2026.nonAux_no_fc : (nonAuxData.all fun (x : NonAuxModalDatum) => x.fcInCoordination == false) = true

No non-auxiliary modal construction permits FC in coordination.

Against ATB Movement (§1, ex. 3)

@cite{simons-2005} proposed that the narrow-scope LF ◇(A ∨ B) arises from across-the-board (ATB) movement of the modal at LF. C&G note there is evidence AGAINST this: ATB movement is independently blocked for nominal quantifiers:

(3a) Everyone sang or everyone danced. (3b) Everyone sang or danced.

(3a) CANNOT be interpreted as (3b). If ATB movement of "everyone" were possible at LF, (3a) should receive the (3b) reading — but it doesn't. This undermines ATB as the mechanism for deriving narrow-scope modal LFs.

C&G's modal concord account avoids this problem: the narrow-scope LF is derived via feature checking (specific to modals), not movement (which would overgeneralize to quantifiers).

structure CiardelliGuerrini2026.ATBCounterexample : Type

ATB counterexample data.

• surface : String
• atbReading : String
• atbReadingAvailable : Bool

def CiardelliGuerrini2026.instReprATBCounterexample.repr : ATBCounterexample → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CiardelliGuerrini2026.instReprATBCounterexample : Repr ATBCounterexample

Equations

• CiardelliGuerrini2026.instReprATBCounterexample = { reprPrec := CiardelliGuerrini2026.instReprATBCounterexample.repr }

def CiardelliGuerrini2026.everyoneATB : ATBCounterexample

(3) "Everyone sang or everyone danced" ≠ "Everyone sang or danced."

Equations

• CiardelliGuerrini2026.everyoneATB = { surface := "Everyone sang or everyone danced", atbReading := "Everyone sang or danced", atbReadingAvailable := false }

Concord Across Negation (§4.2)

Modal concord across negation requires opposite forces. The checking uses ModalForce.dual — negation over a modal operator yields its dual:

(24) The countess allowed that I needn't do it again. ALLOWi∃ ✓ — dual(∀) = ∃, matches checker

(26) *The countess firmly demanded that I needn't do it again. *DEMANDi∀ ✗ — dual(∀) = ∃ ≠ ∀

(25) A restraining order demands that Roiland may not harass the plaintiff. DEMANDi∀ ✓ — dual(∃) = ∀, matches checker

(27) *A special permit allows that Roiland may not recycle. *ALLOWi∃ ✗ — dual(∃) = ∀ ≠ ∃

The pattern: checking across negation succeeds iff the checker's force equals the dual of the checked item's force. This follows from ModalFeature.checksAcrossNegation, which uses ModalForce.dual.

theorem CiardelliGuerrini2026.allow_neg_need_ok : { force := Core.Modality.ModalForce.possibility, interp := Core.Modality.ModalInterpretability.interpretable }.checksAcrossNegation { force := Core.Modality.ModalForce.necessity, interp := Core.Modality.ModalInterpretability.uninterpretable } = true

(24) ALLOW[i∃] checks ¬NEED[u∀]: well-formed (dual(∀) = ∃).

theorem CiardelliGuerrini2026.demand_neg_need_bad : { force := Core.Modality.ModalForce.necessity, interp := Core.Modality.ModalInterpretability.interpretable }.checksAcrossNegation { force := Core.Modality.ModalForce.necessity, interp := Core.Modality.ModalInterpretability.uninterpretable } = false

(26) *DEMAND[i∀] checks ¬NEED[u∀]: ill-formed (dual(∀) = ∃ ≠ ∀).

theorem CiardelliGuerrini2026.demand_neg_may_ok : { force := Core.Modality.ModalForce.necessity, interp := Core.Modality.ModalInterpretability.interpretable }.checksAcrossNegation { force := Core.Modality.ModalForce.possibility, interp := Core.Modality.ModalInterpretability.uninterpretable } = true

(25) DEMAND[i∀] checks ¬MAY[u∃]: well-formed (dual(∃) = ∀).

theorem CiardelliGuerrini2026.allow_neg_may_bad : { force := Core.Modality.ModalForce.possibility, interp := Core.Modality.ModalInterpretability.interpretable }.checksAcrossNegation { force := Core.Modality.ModalForce.possibility, interp := Core.Modality.ModalInterpretability.uninterpretable } = false

(27) *ALLOW[i∃] checks ¬MAY[u∃]: ill-formed (dual(∃) = ∀ ≠ ∃).

theorem CiardelliGuerrini2026.negation_concord_pattern (checkerForce checkedForce : Core.Modality.ModalForce) (hNec : checkerForce = Core.Modality.ModalForce.necessity ∨ checkerForce = Core.Modality.ModalForce.possibility) (hChk : checkedForce = Core.Modality.ModalForce.necessity ∨ checkedForce = Core.Modality.ModalForce.possibility) : { force := checkerForce, interp := Core.Modality.ModalInterpretability.interpretable }.checksAcrossNegation { force := checkedForce, interp := Core.Modality.ModalInterpretability.uninterpretable } = true ↔ checkerForce = checkedForce.dual

General pattern: cross-negation concord succeeds ↔ forces are duals. This is the content of the negation-concord generalization from @cite{grosz-2010} and @cite{anand-brasoveanu-2010}, formalized as a consequence of checksAcrossNegation using ModalForce.dual.

Concord + Negation + Coordination (§4.2, ex. 28-29)

"I need not cook and I need not clean" can convey ◇(¬Cook ∧ ¬Clean) — permission to do neither — but NOT □(¬Cook ∧ ¬Clean) — obligation to do neither. This follows from the concord-across-negation generalization.

The "need" u-feature force comes from the Fragment: necessity.

theorem CiardelliGuerrini2026.need_feature_eq : Fragments.English.Auxiliaries.need.toModalFeature = some { force := Core.Modality.ModalForce.necessity, interp := Core.Modality.ModalInterpretability.uninterpretable }

"Need" carries [u∀-MOD] in the Fragment.

theorem CiardelliGuerrini2026.need_not_existential_ok : { force := Core.Modality.ModalForce.possibility, interp := Core.Modality.ModalInterpretability.interpretable }.checksAcrossNegation Fragments.English.Auxiliaries.need.toModalFeature.get! = true

The existential reading is available: ◇[i∃] checks ¬NEED[u∀].

theorem CiardelliGuerrini2026.need_not_universal_blocked : { force := Core.Modality.ModalForce.necessity, interp := Core.Modality.ModalInterpretability.interpretable }.checksAcrossNegation Fragments.English.Auxiliaries.need.toModalFeature.get! = false

The universal reading is blocked: □[i∀] cannot check ¬NEED[u∀].

Conjunctive Permission (§2, ex. 7-8)

"You may go to Bob's party and you may go to Charlie's party" has a reading where Alice is allowed to go to BOTH parties: ◇(Bob ∧ Charlie).

This is distinct from ◇Bob ∧ ◇Charlie. Unlike disjunction, ◇(A ∧ B) is strictly STRONGER than ◇A ∧ ◇B — so the scope distinction has truth-conditional consequences for conjunction.

theorem CiardelliGuerrini2026.conjunctive_narrow_stronger {World : Type u_1} (p q : Set World) (h : Exhaustification.FreeChoice.diamond (p ∩ q)) : Exhaustification.FreeChoice.diamond p ∧ Exhaustification.FreeChoice.diamond q

For conjunction, narrow scope is strictly stronger than wide scope: ◇(A ∧ B) → ◇A ∧ ◇B but not conversely.

Connection to Empirical Modal Concord (@cite{rotter-liu-2025})

@cite{rotter-liu-2025} study "must have to VP" stacking, where two necessity modals yield a single-necessity reading (concord). This is the same phenomenon C&G exploit: modal concord — one modal is semantically vacuous.

The ModalFeature.checks infrastructure from §3 models this directly: in "must have to", one auxiliary carries [i∀-MOD] and the other [u∀-MOD]. The i-feature checks the u-feature, leaving only one semantic operator.

The empirical finding that "must have to" preserves single-necessity meaning (meaning_must_close_to_mustHaveTo) is predicted by the concord mechanism.

theorem CiardelliGuerrini2026.must_haveTo_same_feature : Fragments.English.Auxiliaries.must.toModalFeature = Fragments.English.Auxiliaries.haveTo.toModalFeature

"Must" and "have to" have the same modal feature (both [u∀-MOD]). Concord between them is predicted: same-force u-features.

theorem CiardelliGuerrini2026.haveTo_feature_eq : Fragments.English.Auxiliaries.haveTo.toModalFeature = some { force := Core.Modality.ModalForce.necessity, interp := Core.Modality.ModalInterpretability.uninterpretable }

"Have to" carries [u∀-MOD]: necessity force, uninterpretable.

def CiardelliGuerrini2026.mustHaveToConcord : ConcordDerivation

"Must have to" concord as a ConcordDerivation — derived from Fragment. The @cite{rotter-liu-2025} finding that "must have to" yields single necessity (not double necessity) follows: the checker checks both u-features, leaving one semantic operator.

Equations

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

theorem CiardelliGuerrini2026.must_may_no_concord : { force := Fragments.English.Auxiliaries.may.toModalFeature.get!.force, interp := Core.Modality.ModalInterpretability.interpretable }.checks Fragments.English.Auxiliaries.must.toModalFeature.get! = false

Cross-force concord fails: "must"[u∀] cannot be checked by a silent [i∃-MOD] operator. This predicts no concord between necessity and possibility modals.

Verifying Scope Data Against Fragment Entries

The modalForce field in each ScopeAmbiguityDatum is independently verifiable against the Fragment's modal meaning entries.

theorem CiardelliGuerrini2026.mayOrMay_force_verified : mayOrMay.modalForce = Fragments.English.Auxiliaries.may.toModalFeature.get!.force

The force in mayOrMay matches the Fragment entry for "may".

theorem CiardelliGuerrini2026.mustOrMust_force_verified : mustOrMust.modalForce = Fragments.English.Auxiliaries.must.toModalFeature.get!.force

The force in mustOrMust matches the Fragment entry for "must".

theorem CiardelliGuerrini2026.mayAndMay_force_verified : mayAndMay.modalForce = Fragments.English.Auxiliaries.may.toModalFeature.get!.force

The force in mayAndMay matches the Fragment entry for "may".