Documentation

Studies.CiardelliGuerrini2026

Ciardelli and Guerrini (2026): Against wide scope free choice #

This file formalizes the reductionist thesis of [CG26]: the free-choice reading of you may A or you may B arises from the narrow-scope LF ◇(A ∨ B), the reading of the wide-scope ◇A ∨ ◇B being the ignorance one ([Fus19]). Possibility distributes over disjunction, so the two LFs coincide in truth conditions there, and the ambiguity shows where they differ: you must A or you must B has a reading as one disjunctive obligation □(A ∨ B), strictly weaker than □A ∨ □B, and you may A and you may B one as a conjunctive permission ◇(A ∧ B), strictly stronger than ◇A ∧ ◇B. The narrow LF arises by modal concord ([Zei07]): a modal auxiliary carries an uninterpretable modal feature, and one silent interpretable operator above the coordination checks both auxiliaries' features when they fall in one concord class. Non-auxiliary modals carry interpretable features and cannot be checked, which is why it's ok for John to sing or it's ok for John to dance has no free choice ([MS17]), while may and can share their feature and mix ([AO06]). Across negation concord needs dual forces ([Gro10], [AB10]), negation flipping the force of the feature it scopes over, so I need not cook and I need not clean conveys a permission to do neither and not an obligation. The modal features come from the English auxiliary Fragment, and the paper's coordination and concord examples are rows.

Implementation notes #

The argument against across-the-board movement from everyone sang or everyone danced ([Sim05]) has no movement substrate here, and the cases the paper leaves open, it is possible that A or it is possible that B and conjoined be allowed, are not rows.

References #

Scope and truth conditions (§2) #

source
@[reducible, inline]
abbrev CiardelliGuerrini2026.universalAccess :
SetRel Bool Bool

Universal accessibility on two worlds, the countermodels' frame.

Equations
Instances For
    source
    theorem CiardelliGuerrini2026.poss_union_eq {World : Type u_1} (R : SetRel World World) (A B : Set World) :
    R.preimage (A ∪ B) = R.preimage A ∪ R.preimage B

    May-or-may, (2): possibility distributes over disjunction, so this is the one cell of the paradigm where the scope ambiguity is invisible to truth conditions.

    source
    theorem CiardelliGuerrini2026.exists_not_poss_union_subset_inter :
    ∃ (A : Set Bool) (B : Set Bool), ¬universalAccess.preimage A ∪ universalAccess.preimage B ⊆ universalAccess.preimage A ∩ universalAccess.preimage B

    The wide-scope LF does not entail free choice: one possible disjunct suffices for it.

    source
    theorem CiardelliGuerrini2026.nec_union_subset_nec_union {World : Type u_1} (R : SetRel World World) (A B : Set World) :
    R.core A ∪ R.core B ⊆ R.core (A ∪ B)

    Must-or-must, (5): the narrow-scope disjunctive obligation follows from the wide-scope disjunction of obligations.

    source
    theorem CiardelliGuerrini2026.exists_not_nec_union_subset :
    ∃ (A : Set Bool) (B : Set Bool), ¬universalAccess.core (A ∪ B) ⊆ universalAccess.core A ∪ universalAccess.core B

    But not conversely: a disjunctive obligation leaves open which disjunct is met.

    source
    theorem CiardelliGuerrini2026.poss_inter_subset_poss_inter {World : Type u_1} (R : SetRel World World) (A B : Set World) :
    R.preimage (A ∩ B) ⊆ R.preimage A ∩ R.preimage B

    May-and-may, (7): the narrow-scope conjunctive permission entails the wide-scope conjunction of permissions.

    source
    theorem CiardelliGuerrini2026.exists_not_poss_inter_subset :
    ∃ (A : Set Bool) (B : Set Bool), ¬universalAccess.preimage A ∩ universalAccess.preimage B ⊆ universalAccess.preimage (A ∩ B)

    But not conversely, which is what makes (9b), you may come with me and you may stay here, absurd on its conjunctive reading: two permissions need not be jointly satisfiable.

    source
    inductive CiardelliGuerrini2026.ModalInterpretability :
    Type

    A modal feature is interpretable, contributing a modal operator, or uninterpretable, checked by an interpretable feature that c-commands it.

    Instances For
      source
      @[instance_reducible]
      instance CiardelliGuerrini2026.instDecidableEqModalInterpretability :
      DecidableEq ModalInterpretability
      Equations
      source
      structure CiardelliGuerrini2026.ModalFeature :
      Type

      A modal feature pairs a force with its interpretability: the four features [i∀-MOD], [u∀-MOD], [i∃-MOD] and [u∃-MOD].

      Instances For
        source
        def CiardelliGuerrini2026.instDecidableEqModalFeature.decEq (x✝ x✝¹ : ModalFeature) :
        Decidable (x✝ = x✝¹)
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[instance_reducible]
          instance CiardelliGuerrini2026.instDecidableEqModalFeature :
          DecidableEq ModalFeature
          Equations
          source
          def CiardelliGuerrini2026.ModalFeature.Checks (checker checked : ModalFeature) :
          Prop

          An interpretable feature checks an uninterpretable one of the same concord class; one interpretable feature may check several.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[instance_reducible]
            instance CiardelliGuerrini2026.instDecidableRelModalFeatureChecks :
            DecidableRel ModalFeature.Checks
            Equations
            • One or more equations did not get rendered due to their size.
            source
            def CiardelliGuerrini2026.ModalFeature.negated (f : ModalFeature) :
            ModalFeature

            The feature of a negated constituent: negation flips the force of the feature it scopes over, so concord across negation checks the negated feature (§4.2, footnote 7, after [Gro10] and [AB10]).

            Equations
            Instances For
              source
              theorem CiardelliGuerrini2026.ModalFeature.checks_negated_iff {checker checked : ModalFeature} (hi : checker.interp = ModalInterpretability.interpretable) (hu : checked.interp = ModalInterpretability.uninterpretable) :
              checker.Checks checked.negated ↔ ¬(checker.force.IsUniversal ↔ checked.force.IsUniversal)

              Concord across negation succeeds exactly between the two classes: an interpretable feature checks a negated uninterpretable one iff their forces fall in different classes.

              source
              def CiardelliGuerrini2026.auxiliaryFeatures (a : Auxiliary) :
              Finset ModalFeature

              The features of a modal auxiliary of the Fragment: the forces of its meanings, uninterpretable, Zeijlstra's generalization that auxiliaries contribute no operator.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def CiardelliGuerrini2026.Concord (f₁ f₂ : ModalFeature) :
                Prop

                Two modal features stand in concord when both are uninterpretable and fall in one concord class: one silent interpretable operator above the coordination then checks both, (15), so the modal outscopes the coordinator.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[instance_reducible]
                  instance CiardelliGuerrini2026.instDecidableRelModalFeatureConcord :
                  DecidableRel Concord
                  Equations
                  • One or more equations did not get rendered due to their size.
                  source
                  theorem CiardelliGuerrini2026.exists_checks_of_concord {f₁ f₂ : ModalFeature} (h : Concord f₁ f₂) :
                  ∃ (op : ModalFeature), op.interp = ModalInterpretability.interpretable ∧ op.Checks f₁ ∧ op.Checks f₂

                  The silent operator: an interpretable feature of the shared class checks both features.

                  source
                  theorem CiardelliGuerrini2026.concord_of_checks {op f₁ f₂ : ModalFeature} (h₁ : op.Checks f₁) (h₂ : op.Checks f₂) :
                  Concord f₁ f₂

                  Conversely, two features one operator checks are in concord.

                  source
                  theorem CiardelliGuerrini2026.not_checks_of_interpretable (op : ModalFeature) {f : ModalFeature} (h : f.interp = ModalInterpretability.interpretable) :
                  ¬op.Checks f

                  An interpreted feature is never checked, so non-auxiliary modals such as be allowed admit no narrow-scope LF, (19) and (20).

                  source
                  theorem CiardelliGuerrini2026.fragment_concord :
                  (∀ f ∈ auxiliaryFeatures English.Auxiliaries.may, ∀ g ∈ auxiliaryFeatures English.Auxiliaries.may, Concord f g) ∧ (∀ f ∈ auxiliaryFeatures English.Auxiliaries.must, ∀ g ∈ auxiliaryFeatures English.Auxiliaries.must, Concord f g) ∧ (∀ f ∈ auxiliaryFeatures English.Auxiliaries.may, ∀ g ∈ auxiliaryFeatures English.Auxiliaries.can, Concord f g) ∧ ∀ f ∈ auxiliaryFeatures English.Auxiliaries.may, ∀ g ∈ auxiliaryFeatures English.Auxiliaries.must, ¬Concord f g

                  The Fragment's modals pair as the paper needs: may with may, must with must, may with can, [AO06]'s mixed form of footnote 4, and may not with must.

                  Concord across negation (§4.2) #

                  source
                  theorem CiardelliGuerrini2026.need_not (f : ModalFeature) :
                  f ∈ auxiliaryFeatures English.Auxiliaries.need → { force := Modality.ModalForce.possibility, interp := ModalInterpretability.interpretable }.Checks f.negated ∧ ¬{ force := Modality.ModalForce.necessity, interp := ModalInterpretability.interpretable }.Checks f.negated

                  (28), I need not cook and I need not clean: the negated feature of need is checked by a silent possibility operator, (29a), and not by a necessity one, (29c), so the sentence conveys a permission to do neither and not an obligation to do neither.

                  The rows #

                  source
                  def CiardelliGuerrini2026.featuresOf :
                  String → Finset ModalFeature

                  The modal features of a modal named in the rows: the auxiliaries' from the Fragment, and the interpretable feature of the non-auxiliary modals, (20).

                  Equations
                  Instances For
                    source
                    theorem CiardelliGuerrini2026.coordination_rows (e : Datum) :
                    e ∈ Examples.all → ∀ m₁ ∈ e.feature? "modal1", ∀ m₂ ∈ e.feature? "modal2", ∀ f₁ ∈ featuresOf m₁, ∀ f₂ ∈ featuresOf m₂, e.feature? "narrowReading" ≠ none ↔ Concord f₁ f₂

                    A coordination of two modals has a narrow-scope reading exactly when their features are in concord.

                    source
                    theorem CiardelliGuerrini2026.narrow_reading_available (e : Datum) :
                    e ∈ Examples.all → ∀ n ∈ e.feature? "narrowReading", ∃ r ∈ e.readings, r.1 = n ∧ r.2 = Judgment.acceptable

                    The narrow-scope reading a row names is among its available readings.

                    source
                    theorem CiardelliGuerrini2026.concord_rows (e : Datum) :
                    e ∈ Examples.all → ∀ c ∈ e.feature? "checker", ∀ k ∈ e.feature? "checked", ∀ op ∈ featuresOf c, ∀ f ∈ featuresOf k, (∃ r ∈ e.readings, r.1 = "modal concord" ∧ r.2 = Judgment.acceptable) ↔ op.Checks (if e.feature? "negated" = some "true" then f.negated else f)

                    Modal concord between a higher and a lower modal is available exactly when the higher feature checks the lower one, negated when negation intervenes.