Against wide scope free choice ([CG26])

The free-choice reading of "you may A or you may B" does not arise from the wide-scope LF ◇A ∨ ◇B, but from the narrow-scope LF ◇(A ∨ B). For disjunction the two LFs are truth-conditionally equivalent (scope_equivalence), so the scope distinction is invisible to truth conditions; it matters only compositionally, because only ◇(A ∨ B) feeds the exhaustification that derives ◇A ∧ ◇B. The wide-scope LF instead yields an ignorance reading and does not, on its own, entail free choice (wideScope_underdetermines_fc). (For conjunction the two LFs are not equivalent; see §8.)

The narrow-scope LF is derived by modal concord [Zei07]: modal auxiliaries carry uninterpretable features [u∃/∀-MOD]; a single silent interpretable operator c-commanding the coordination checks both, so only it is interpreted, yielding Δ(A ∘ B) rather than ΔA ∘ ΔB.

MOD A COORD MOD B is scope-ambiguous across the board:

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)

The modal operators diamond/box are Core.Logic.Modal.poss/nec (the flat S5 modals shared with the whole free-choice stack), so the scope theorems consume the substrate's distribution lemmas directly.

Main declarations

• scope_equivalence — the two disjunction LFs are truth-conditionally equal.
• disjunctive_obligation_narrow_weaker / _not_wide — must-or-must: under necessity the narrow LF □(A ∪ B) is strictly weaker than the wide □A ∨ □B.
• ConcordDerivation — two [u-MOD] auxiliaries checked by one silent operator.
• narrowScope_yields_fc / wideScope_underdetermines_fc — free choice from the narrow LF; non-entailment of free choice from the wide LF.
• reductionist_thesis — the two packaged together.
• negation_concord_pattern — cross-negation concord succeeds iff forces are duals.

Truth-conditional equivalence

For disjunction the two LFs collapse: ◇(A ∨ B) ↔ ◇A ∨ ◇B in standard modal logic. This is the point of [CG26] — the scope distinction is invisible to truth conditions, and matters only for compositional derivation and pragmatic enrichment. (For conjunction the LFs are not equivalent; see §8.)

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

The two disjunction LFs are truth-conditionally equivalent: ◇(A ∨ B) ↔ ◇A ∨ ◇B. A thin alias for Exhaustification.FreeChoice.diamond_distributes_iff, recording its role as the central observation of [CG26].

Must-or-must: disjunctive obligation (§2)

Under necessity, the scope distinction is not truth-conditionally vacuous. diamond/box here are Core.Logic.Modal.poss/nec, so these theorems consume the substrate's flat distribution directly. For disjunction the narrow LF □(A ∪ B) is strictly weaker than the wide LF □A ∨ □B — exactly C&G's must-or-must contrast: "(either) you must A or you must B" on its salient reading is a single disjunctive obligation □(A ∨ B), not two obligations.

theorem CiardelliGuerrini2026.disjunctive_obligation_narrow_weaker {World : Type u_1} (A B : Set World) : Exhaustification.FreeChoice.box A ∨ Exhaustification.FreeChoice.box B → Exhaustification.FreeChoice.box (A ∪ B)

Wide ⟹ narrow: □A ∨ □B → □(A ∪ B). The narrow disjunctive-obligation LF is the weaker reading (monotonicity of Core.Logic.Modal.nec).

theorem CiardelliGuerrini2026.disjunctive_obligation_not_wide : ∃ (A : Set Bool) (B : Set Bool), Exhaustification.FreeChoice.box (A ∪ B) ∧ ¬(Exhaustification.FreeChoice.box A ∨ Exhaustification.FreeChoice.box B)

…but not conversely: □(A ∪ B) does not entail □A ∨ □B. A disjunctive obligation leaves which disjunct is met open, so neither □A nor □B follows. This is why must-or-must has a genuine narrow reading the wide LF lacks.

Scope-ambiguity data (§2)

MOD A COORD MOD B sentences are scope-ambiguous. The illustrative sentences record the modal force, which §10 cross-checks against the Fragment; narrow-scope availability is witnessed structurally by the concord derivations of §3 (mayMayConcord, mustMustConcord), whose mere existence as well-typed terms is the proof that the two auxiliaries can undergo concord.

structure CiardelliGuerrini2026.ScopeAmbiguityDatum : Type

An illustrative "MOD A COORD MOD B" sentence.

• sentence : String
• coord : String

  The coordinator: "or" or "and".

• modalForce : Semantics.Modality.ModalForce
• dominantReading : String

  The reading dominant in the discussed context.

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" — free choice from the narrow-scope LF.

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]

Modal concord derivation (§3)

[Zei07]'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, giving ◇(A ∨ B).

def CiardelliGuerrini2026.mayFeature : Semantics.Modality.ModalFeature

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

Equations

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

def CiardelliGuerrini2026.mustFeature : Semantics.Modality.ModalFeature

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

Equations

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

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

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

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

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

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

The silent operator that checks a given u-feature: same force, but interpretable. This is the operator [CG26] posit above the coordination.

Equations

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

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

Core derivation: the matching silent operator checks any u-feature. This is the general form of the 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 [CG26]'s compositional mechanism.

A ConcordDerivation exists iff both features are uninterpretable (u-MOD) and belong to the same concord class (both ∃-type or both ∀-type). The silent operator, the checking proofs, and the resulting narrow-scope interpretation are all derived from these two conditions.

• f₁ : Semantics.Modality.ModalFeature

  The feature of the first modal auxiliary.

• f₂ : Semantics.Modality.ModalFeature

  The feature of the second modal auxiliary.

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

  Both are uninterpretable.

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

  Same concord class.

def CiardelliGuerrini2026.ConcordDerivation.checker (cd : ConcordDerivation) : Semantics.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 = Semantics.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₂ : English.Auxiliaries.AuxEntry) {f₁ f₂ : Semantics.Modality.ModalFeature} (_h₁ : a₁.toModalFeature = some f₁) (_h₂ : a₂.toModalFeature = some f₂) (hI₁ : f₁.interp = Semantics.Modality.ModalInterpretability.uninterpretable) (hI₂ : f₂.interp = Semantics.Modality.ModalInterpretability.uninterpretable) (hF : Semantics.Modality.ConcordType.fromModalForce f₁.force = Semantics.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 English.Auxiliaries.AuxEntry

The modal auxiliaries that participate in concord: Fragment entries 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 English.Auxiliaries.AuxEntry

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

Equations

• CiardelliGuerrini2026.concordCapableModals = List.filter (fun (a : 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 : English.Auxiliaries.AuxEntry) => decide ((a.interpretability == some Semantics.Modality.ModalInterpretability.uninterpretable) = true)) = true

Every concord-capable modal's feature is uninterpretable.

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

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

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

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

Instantiations

def CiardelliGuerrini2026.mayMayConcord : ConcordDerivation

"May A or may B" concord derivation — fully derived from the 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 the 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: a silent □ cannot check "may" [u∃].

The FC pipeline: concord → narrow scope → free choice (§3)

The pipeline has three stages:

1. feature matching → ConcordDerivation (above);
2. narrow scope → a single modal operator over the coordination;
3. exhaustification → the free-choice inference.

The key point: the narrow/wide scope distinction is truth-conditionally vacuous for disjunction (scope_equivalence) but pragmatically active. Only the narrow-scope LF, exhaustified, yields free choice; the wide-scope LF underdetermines it (and yields an ignorance reading instead).

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: the narrow-scope ◇(A ∨ B), 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 (free_choice_forward).

theorem CiardelliGuerrini2026.wideScope_underdetermines_fc : ∃ (A : Set Unit) (B : Set Unit), (Exhaustification.FreeChoice.diamond A ∨ Exhaustification.FreeChoice.diamond B) ∧ ¬(Exhaustification.FreeChoice.diamond A ∧ Exhaustification.FreeChoice.diamond B)

The wide-scope LF ◇A ∨ ◇B does not entail free choice ◇A ∧ ◇B: a disjunction of possibilities holds even when only one disjunct is possible. This is why [CG26] locate the free-choice reading exclusively in the narrow-scope LF — the wide-scope LF yields the ignorance reading (the speaker is unsure which disjunct holds), not free choice.

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

The reductionist thesis ([CG26], formalized).

Despite truth-conditional equivalence (scope_equivalence), the FC reading arises only from the narrow-scope LF: (1) the two disjunction LFs are equivalent, and (2) the narrow-scope LF, exhaustified, yields free choice. The wide-scope LF does not (wideScope_underdetermines_fc), so there is no separate problem of "wide-scope free choice".

Auxiliary vs non-auxiliary modals (§4.1)

[MS17] 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)

[CG26] explain this: "it's ok" and "be allowed" carry interpretable features, so they are already interpreted and cannot be checked by a higher silent operator — no narrow-scope LF, no FC. Modal auxiliaries ("may", "must", "can") carry uninterpretable features and can be checked → FC available. The auxiliary status of "may", "must", "can", "need" is derived from English.FunctionWords — they are all .modal entries.

Caveat: in §4.3 the authors flag (31) "it is possible that A or it is possible that B", a non-auxiliary modal that nevertheless seems to allow FC, as an outstanding problem. The prediction below is therefore about the concord mechanism (interpreted features cannot be checked), not an exceptionless surface generalization.

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

Fragment-derived: the English modals used by [CG26] are modal auxiliaries.

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

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

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

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

All these modals carry uninterpretable features in the Fragment.

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

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

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

theorem CiardelliGuerrini2026.interpreted_unchecked (checker f : Semantics.Modality.ModalFeature) (h : f.interp = Semantics.Modality.ModalInterpretability.interpretable) : checker.checks f = false

The mechanism behind the auxiliary/non-auxiliary contrast: an interpreted feature can never be checked. Non-auxiliary modal constructions ("it's ok that", "be allowed/required to") carry interpretable features, so no silent operator can check them — hence no narrow-scope LF and no FC in coordination. This is derived from ModalFeature.checks (which requires the checked feature to be uninterpretable), not stipulated.

theorem CiardelliGuerrini2026.interpreted_not_concord_checked (cd : ConcordDerivation) : cd.f₂.interp ≠ Semantics.Modality.ModalInterpretability.interpretable

Corollary: an interpreted feature cannot be the checked conjunct of a ConcordDerivation — that would contradict uInterp₂.

Against ATB movement (§1, ex. 3)

[Sim05] proposed that the narrow-scope LF ◇(A ∨ B) arises from across-the-board (ATB) movement of the modal at LF. [CG26] note 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 does not. This undermines ATB as the mechanism for deriving narrow-scope modal LFs. The modal concord account avoids the problem: the narrow-scope LF is derived by feature checking (specific to modals), not movement (which would overgeneralize to quantifiers).

Formalizing the contrast faithfully needs a movement/quantifier substrate this study does not import, so the argument is recorded here as prose.

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) ALLOWi∃ ✓ — dual(∀) = ∃, matches the checker (26) *DEMANDi∀ ✗ — dual(∀) = ∃ ≠ ∀ (25) DEMANDi∀ ✓ — dual(∃) = ∀, matches the checker (27) *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. The generalization is from [Gro10] and [AB10].

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

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

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

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

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

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

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

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

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

General pattern: cross-negation concord succeeds iff the forces are duals. This is the content of the negation-concord generalization from [Gro10] and [AB10], formalized as a consequence of checksAcrossNegation using ModalForce.dual.

"I need not cook and I need not clean" (§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 (necessity) comes from the Fragment.

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

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

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

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

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

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

Conjunctive permission, may-and-may (§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). Unlike disjunction, ◇(A ∧ B) is strictly stronger than ◇A ∧ ◇B, so for conjunction the scope distinction has truth-conditional consequences.

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).

Same-feature concord in the fragment

[CG26]'s mechanism for the narrow-scope LF is that two auxiliaries carrying the same modal feature are checked by a single silent operator (the coordination structure for "you must A or you must B" → □(A ∨ B)), leaving one semantic operator. The fragment exhibits the precondition: must and have to both carry [u∀-MOD], so a single [i∀] operator checks both.

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

must and have to carry the same modal feature (both [u∀-MOD]) — a same-force concord configuration.

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

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

def CiardelliGuerrini2026.mustHaveToConcord : ConcordDerivation

The must/have to concord as a ConcordDerivation, derived from the Fragment: two [u∀] auxiliaries checked by one operator.

Equations

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

theorem CiardelliGuerrini2026.must_may_no_concord : { force := English.Auxiliaries.may.toModalFeature.get!.force, interp := Semantics.Modality.ModalInterpretability.interpretable }.checks 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.

Scope-data verification against the Fragment

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

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

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

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

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

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

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