X-Marking on Necessity Modals

@cite{ferreira-2023} @cite{von-fintel-iatridou-2023}

X-marking is a morphological operation (realized as past imperfect in Portuguese, covert ambiguity in English) that shifts the modal parameters of necessity modals without changing their quantificational force (both remain ∀ over best worlds).

Two independent X-marking operations target the two Kratzerian parameters:

• Xf (modal base revision): widens the domain ∩f_w by suspending presupposed evidence against the prejacent, adding p-worlds similar to currently accessible worlds.

• Xg (ordering source revision): refines the ordering by favoring p-worlds among those previously ranked as best.

Applied to strong necessity (SN), these generate the square of necessities:

    SN ────Xf────→ SN_Xf
    │                │
    Xg               Xg
    │                │
    SN_Xg ──Xf────→ SN_{Xf,g}

The central equation: WN ≡ SN_Xg — weak necessity IS strong necessity with X-marked ordering source.

Star-revision: X-marking on modal bases (Xf)

structure Semantics.Modality.Kratzer.XMarking.IsStarRevision {W : Type u_1} (f f' : ModalBase W) (p : W → Prop) : Prop

Property: f' is a ∗-revision of f for p (@cite{ferreira-2023}). UNVERIFIED: §3 reference removed pending check against the JoS pdf.

A ∗-revision widens the modal domain by adding p-worlds: (1) every world accessible under f remains accessible under f', (2) every newly accessible world satisfies p.

• widens (w w' : W) : w' ∈ accessibleWorlds f w → w' ∈ accessibleWorlds f' w
• new_satisfy_p (w w' : W) : w' ∈ accessibleWorlds f' w → w' ∉ accessibleWorlds f w → p w'

theorem Semantics.Modality.Kratzer.XMarking.starRevision_widens {W : Type u_1} {f f' : ModalBase W} {p : W → Prop} (h : IsStarRevision f f' p) (w w' : W) (hw : w' ∈ accessibleWorlds f w) : w' ∈ accessibleWorlds f' w

theorem Semantics.Modality.Kratzer.XMarking.starRevision_new_satisfy_p {W : Type u_1} {f f' : ModalBase W} {p : W → Prop} (h : IsStarRevision f f' p) (w w' : W) (hw' : w' ∈ accessibleWorlds f' w) (hnew : w' ∉ accessibleWorlds f w) : p w'

Double-star-revision: X-marking on ordering sources (Xg)

def Semantics.Modality.Kratzer.XMarking.xMarkOrdering {W : Type u_1} (g : OrderingSource W) (p : W → Prop) : OrderingSource W

Xg: X-marking targeting the ordering source (∗∗-revision). Adds a secondary ordering that favors p-worlds among the best worlds.

Equations

• Semantics.Modality.Kratzer.XMarking.xMarkOrdering g p = Semantics.Modality.Directive.combineOrdering g fun (x : W) => [p]

The four vertices of the square

@[reducible, inline]

abbrev Semantics.Modality.Kratzer.XMarking.sn {W : Type u_1} (f : ModalBase W) (g : OrderingSource W) (p : W → Prop) (w : W) : Prop

Equations

• Semantics.Modality.Kratzer.XMarking.sn f g p w = Semantics.Modality.Kratzer.necessity f g p w

@[reducible]

def Semantics.Modality.Kratzer.XMarking.snXg {W : Type u_1} (f : ModalBase W) (g : OrderingSource W) (p : W → Prop) (w : W) : Prop

Equations

• Semantics.Modality.Kratzer.XMarking.snXg f g p w = Semantics.Modality.Kratzer.necessity f (Semantics.Modality.Kratzer.XMarking.xMarkOrdering g p) p w

@[reducible]

def Semantics.Modality.Kratzer.XMarking.snXf {W : Type u_1} (f' : ModalBase W) (g : OrderingSource W) (p : W → Prop) (w : W) : Prop

Equations

• Semantics.Modality.Kratzer.XMarking.snXf f' g p w = Semantics.Modality.Kratzer.necessity f' g p w

@[reducible]

def Semantics.Modality.Kratzer.XMarking.snXfg {W : Type u_1} (f' : ModalBase W) (g : OrderingSource W) (p : W → Prop) (w : W) : Prop

Equations

• Semantics.Modality.Kratzer.XMarking.snXfg f' g p w = Semantics.Modality.Kratzer.necessity f' (Semantics.Modality.Kratzer.XMarking.xMarkOrdering g p) p w

Key equation: WN ≡ SN_Xg

theorem Semantics.Modality.Kratzer.XMarking.wn_equiv_snXg {W : Type u_1} (f : ModalBase W) (g : OrderingSource W) (p : W → Prop) (w : W) : Directive.weakNecessity f g (fun (x : W) => [p]) p w ↔ snXg f g p w

Entailment: SN → SN_Xg (must → ought)

theorem Semantics.Modality.Kratzer.XMarking.sn_entails_snXg {W : Type u_1} (f : ModalBase W) (g : OrderingSource W) (p : W → Prop) (w : W) (h : sn f g p w) : snXg f g p w

theorem Semantics.Modality.Kratzer.XMarking.snXg_not_entails_sn : ¬∀ (W : Type) (f : ModalBase W) (g : OrderingSource W) (p : W → Prop) (w : W), snXg f g p w → sn f g p w

The converse fails: SN_Xg ⊭ SN.

Counterexample: W = Bool, f = universal access, g = trivial ordering, p = (· = true). Then snXg holds (xMarkOrdering favors true so best = {true}), but sn fails (all accessible worlds best under empty ordering, p false is false).

Forward entailment: SN → SN_Xf under star-revision

theorem Semantics.Modality.Kratzer.XMarking.sn_entails_snXf {W : Type u_1} (f f' : ModalBase W) (g : OrderingSource W) (p : W → Prop) (w : W) (hRev : IsStarRevision f f' p) (hSN : sn f g p w) : snXf f' g p w

Forward entailments along square edges

theorem Semantics.Modality.Kratzer.XMarking.snXg_entails_snXfg {W : Type u_1} (f f' : ModalBase W) (g : OrderingSource W) (p : W → Prop) (w : W) (hRev : IsStarRevision f f' p) (h : snXg f g p w) : snXfg f' g p w

theorem Semantics.Modality.Kratzer.XMarking.snXf_entails_snXfg {W : Type u_1} (f' : ModalBase W) (g : OrderingSource W) (p : W → Prop) (w : W) (h : snXf f' g p w) : snXfg f' g p w

theorem Semantics.Modality.Kratzer.XMarking.xMarking_parameter_independence {W : Type u_1} (f' : ModalBase W) (g : OrderingSource W) (p : W → Prop) (w : W) : snXfg f' g p w = necessity f' (xMarkOrdering g p) p w

Non-entailment: reverse arrows fail

theorem Semantics.Modality.Kratzer.XMarking.xMarked_unmarked_independent : ¬∀ (W : Type) (f f' : ModalBase W) (g : OrderingSource W) (p : W → Prop) (w : W), IsStarRevision f f' p → snXfg f' g p w → snXg f g p w

theorem Semantics.Modality.Kratzer.XMarking.snXfg_not_entails_snXf : ¬∀ (W : Type) (f' : ModalBase W) (g : OrderingSource W) (p : W → Prop) (w : W), snXfg f' g p w → snXf f' g p w

theorem Semantics.Modality.Kratzer.XMarking.xf_is_universal {W : Type u_1} (f' : ModalBase W) (g : OrderingSource W) (p : W → Prop) (w : W) : snXf f' g p w ↔ ∀ w' ∈ bestWorlds f' g w, p w'

Xf preserves the quantifier: SN_Xf is still ∀ over best worlds.