Ferreira (2023): A square of necessities

[Fer23]

A square of necessities: X-marking weak and strong necessity modals. Semantics and Pragmatics 16, Article 8: 1–54.

Core Contributions

1. Portuguese has a tripartite modal system (poder < dever < ter que) where weak necessity is lexicalized as a distinct root, unlike Spanish (deber = strong necessity) or English (ought = ambiguous).

2. Both weak and strong necessity modals can be X-marked via past imperfect morphology (devia, tinha que), but X-marking does NOT weaken modal force — it shifts modal parameters (modal base or ordering source).

3. Two independent X-marking operations generate a 2×2 square of necessities: Xf (modal base revision) and Xg (ordering source revision). Portuguese instantiates all four vertices.

4. WN ≡ SN_Xg: weak necessity is strong necessity with X-marked ordering source — the secondary ordering favors the prejacent among best worlds.

Square Instantiation & Entailment Diamond

    tem que ──Xf──→ tinha que
       │                │
       Xg               Xg
       │                │
     deve ────Xf──→ devia

Entailment flows downward through both paths (SN → SN_Xf → SN_Xfg and SN → SN_Xg → SN_Xfg), forming a diamond. No reverse entailments hold.

X-marking substrate

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

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

Property: f' is a ∗-revision of f for p ([Fer23]). 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' ∈ Semantics.Modality.Kratzer.accessibleWorlds f w → w' ∈ Semantics.Modality.Kratzer.accessibleWorlds f' w
• new_satisfy_p (w w' : W) : w' ∈ Semantics.Modality.Kratzer.accessibleWorlds f' w → w' ∉ Semantics.Modality.Kratzer.accessibleWorlds f w → p w'

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

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

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

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

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

Equations

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

The four vertices of the square

@[reducible, inline]

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

Equations

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

@[reducible]

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

Equations

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

@[reducible]

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

Equations

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

@[reducible]

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

Equations

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

Key equation: WN ≡ SN_Xg

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

Entailment: SN → SN_Xg (must → ought)

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

theorem Ferreira2023.snXg_not_entails_sn : ¬∀ (W : Type) (f : Semantics.Modality.Kratzer.ModalBase W) (g : Semantics.Modality.Kratzer.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 Ferreira2023.sn_entails_snXf {W : Type u_1} (f f' : Semantics.Modality.Kratzer.ModalBase W) (g : Semantics.Modality.Kratzer.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 Ferreira2023.snXg_entails_snXfg {W : Type u_1} (f f' : Semantics.Modality.Kratzer.ModalBase W) (g : Semantics.Modality.Kratzer.OrderingSource W) (p : W → Prop) (w : W) (hRev : IsStarRevision f f' p) (h : snXg f g p w) : snXfg f' g p w

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

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

Non-entailment: reverse arrows fail

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

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

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

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

@[reducible, inline]

abbrev Ferreira2023.World : Type

Equations

• Ferreira2023.World = Fin 4

Portuguese modal typology

inductive Ferreira2023.PortugueseModal : Type

The six Portuguese modal forms: three roots × two tense markings.

• poder : PortugueseModal
• dever : PortugueseModal
• terQue : PortugueseModal
• podia : PortugueseModal
• devia : PortugueseModal
• tinhaQue : PortugueseModal

@[implicit_reducible]

instance Ferreira2023.instDecidableEqPortugueseModal : DecidableEq PortugueseModal

Equations

• Ferreira2023.instDecidableEqPortugueseModal x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Ferreira2023.instReprPortugueseModal.repr : PortugueseModal → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Ferreira2023.instReprPortugueseModal : Repr PortugueseModal

Equations

• Ferreira2023.instReprPortugueseModal = { reprPrec := Ferreira2023.instReprPortugueseModal.repr }

def Ferreira2023.PortugueseModal.force : PortugueseModal → Semantics.Modality.ModalForce

Modal force of each form.

Equations

• Ferreira2023.PortugueseModal.poder.force = Semantics.Modality.ModalForce.possibility
• Ferreira2023.PortugueseModal.podia.force = Semantics.Modality.ModalForce.possibility
• Ferreira2023.PortugueseModal.dever.force = Semantics.Modality.ModalForce.weakNecessity
• Ferreira2023.PortugueseModal.devia.force = Semantics.Modality.ModalForce.weakNecessity
• Ferreira2023.PortugueseModal.terQue.force = Semantics.Modality.ModalForce.necessity
• Ferreira2023.PortugueseModal.tinhaQue.force = Semantics.Modality.ModalForce.necessity

def Ferreira2023.PortugueseModal.isXMarked : PortugueseModal → Bool

Whether a form is X-marked (past imperfect morphology).

Equations

• Ferreira2023.PortugueseModal.podia.isXMarked = true
• Ferreira2023.PortugueseModal.devia.isXMarked = true
• Ferreira2023.PortugueseModal.tinhaQue.isXMarked = true
• Ferreira2023.PortugueseModal.poder.isXMarked = false
• Ferreira2023.PortugueseModal.dever.isXMarked = false
• Ferreira2023.PortugueseModal.terQue.isXMarked = false

def Ferreira2023.PortugueseModal.unmarked : PortugueseModal → PortugueseModal

The unmarked counterpart of each form.

Equations

• Ferreira2023.PortugueseModal.podia.unmarked = Ferreira2023.PortugueseModal.poder
• Ferreira2023.PortugueseModal.devia.unmarked = Ferreira2023.PortugueseModal.dever
• Ferreira2023.PortugueseModal.tinhaQue.unmarked = Ferreira2023.PortugueseModal.terQue
• x✝.unmarked = x✝

Ascending scale of modal force (§2)

theorem Ferreira2023.ascending_force : Semantics.Modality.ModalForce.necessity.atLeastAsStrong Semantics.Modality.ModalForce.weakNecessity = true ∧ Semantics.Modality.ModalForce.weakNecessity.atLeastAsStrong Semantics.Modality.ModalForce.possibility = true ∧ Semantics.Modality.ModalForce.possibility.atLeastAsStrong Semantics.Modality.ModalForce.weakNecessity = false

poder p < dever p < ter que p

X-marking preserves force (§3)

theorem Ferreira2023.xMarking_preserves_force (m : PortugueseModal) : m.force = m.unmarked.force

X-marking does not change modal force: each pair shares force.

Entailment judgments (§2)

theorem Ferreira2023.terQue_entails_dever (f : Semantics.Modality.Kratzer.ModalBase World) (g : Semantics.Modality.Kratzer.OrderingSource World) (p : World → Prop) (w : World) (h : sn f g p w) : snXg f g p w

ter que p ⊨ dever p: strong necessity entails weak. Follows from Directive.strong_entails_weak — the Xg-refined best worlds are a subset of the unrefined best worlds.

theorem Ferreira2023.dever_not_entails_terQue : ¬∀ (f : Semantics.Modality.Kratzer.ModalBase World) (g : Semantics.Modality.Kratzer.OrderingSource World) (p : World → Prop) (w : World), snXg f g p w → sn f g p w

dever p ⊭ ter que p: weak necessity does not entail strong.

theorem Ferreira2023.dever_entails_poder (f : Semantics.Modality.Kratzer.ModalBase World) (g : Semantics.Modality.Kratzer.OrderingSource World) (p : World → Prop) (w : World) (hSerial : (Semantics.Modality.Kratzer.bestWorlds f (xMarkOrdering g p) w).Nonempty) (h : snXg f g p w) : Semantics.Modality.Kratzer.possibility f (xMarkOrdering g p) p w

dever p ⊨ poder p: weak necessity entails possibility, completing the ascending scale poder p < dever p < ter que p. Requires seriality (nonempty best worlds) — the D axiom.

Consistency judgments (§2)

theorem Ferreira2023.dever_consistent_with_not_p : ∃ (f : Semantics.Modality.Kratzer.ModalBase World) (g : Semantics.Modality.Kratzer.OrderingSource World) (p : World → Prop) (w : World), snXg f g p w ∧ ¬p w

dever p ∧ ¬p is consistent: weak necessity is compatible with the prejacent being false ("Este homem deve ter sido assassinado, mas ele pode não ter sido").

theorem Ferreira2023.terQue_inconsistent_with_not_p_realistic (f : Semantics.Modality.Kratzer.ModalBase World) (g : Semantics.Modality.Kratzer.OrderingSource World) (p : World → Prop) (w : World) (hReal : ∀ (w : World), Semantics.Modality.Kratzer.accessibleWorlds f w = {w}) (hSN : sn f g p w) : p w

ter que p ∧ ¬p is contradictory when the base is realistic: if w ∈ ∩f(w) and all best worlds satisfy p, then w satisfies p (by the T axiom).

Non-entailment between present and past forms (§3)

theorem Ferreira2023.devia_not_entails_deve : ¬∀ (f f' : Semantics.Modality.Kratzer.ModalBase World) (g : Semantics.Modality.Kratzer.OrderingSource World) (p : World → Prop) (w : World), IsStarRevision f f' p → snXfg f' g p w → snXg f g p w

devia p ⊬ deve p: X-marking the modal base (via Xf) widens the domain, and the new p-worlds can change the best set under the refined ordering.

Note: the reverse direction (deve p ⊨ devia p) DOES hold — see PortugueseSquare.deve_entails_devia. This follows from sn_entails_snXf applied to the refined ordering: ∗-revision only adds p-worlds, which cannot worsen the truth of the prejacent among best worlds.

Square instantiation: Portuguese occupies all four vertices

structure Ferreira2023.PortugueseSquare : Type

The square of necessities applied to Portuguese modal verbs.

Each field maps to a vertex of the square:

• sn = tem que (strong necessity, unmarked)
• snXf = tinha que (strong necessity, X-marked modal base)
• snXg = deve (= weak necessity, X-marked ordering source)
• snXfg = devia (weak necessity, X-marked modal base)

• f : Semantics.Modality.Kratzer.ModalBase World

  Modal base (epistemic/circumstantial)

• fStar : Semantics.Modality.Kratzer.ModalBase World

  ∗-revised modal base

• g : Semantics.Modality.Kratzer.OrderingSource World

  Ordering source

• p : World → Prop

  Prejacent

• hRev : IsStarRevision self.f self.fStar self.p

  fStar is a valid ∗-revision of f for p

def Ferreira2023.PortugueseSquare.temQue (sq : PortugueseSquare) (w : World) : Prop

tem que: top-left vertex (SN).

Equations

• sq.temQue w = Ferreira2023.sn sq.f sq.g sq.p w

def Ferreira2023.PortugueseSquare.deve (sq : PortugueseSquare) (w : World) : Prop

deve: bottom-left vertex (SN_Xg = WN).

Equations

• sq.deve w = Ferreira2023.snXg sq.f sq.g sq.p w

def Ferreira2023.PortugueseSquare.tinhaQue (sq : PortugueseSquare) (w : World) : Prop

tinha que: top-right vertex (SN_Xf).

Equations

• sq.tinhaQue w = Ferreira2023.snXf sq.fStar sq.g sq.p w

def Ferreira2023.PortugueseSquare.devia (sq : PortugueseSquare) (w : World) : Prop

devia: bottom-right vertex (SN_{Xf,g}).

Equations

• sq.devia w = Ferreira2023.snXfg sq.fStar sq.g sq.p w

theorem Ferreira2023.PortugueseSquare.temQue_entails_deve (sq : PortugueseSquare) (w : World) (h : sq.temQue w) : sq.deve w

tem que ⊨ deve: top-left entails bottom-left (SN → SN_Xg).

Forward entailment under star-revision (§3)

theorem Ferreira2023.PortugueseSquare.temQue_entails_tinhaQue (sq : PortugueseSquare) (w : World) (h : sq.temQue w) : sq.tinhaQue w

tem que ⊨ tinha que: SN entails SN_Xf under ∗-revision. Follows from sn_entails_snXf: best worlds in the wider domain either (a) were already best in the narrower domain, or (b) are new p-worlds.

theorem Ferreira2023.PortugueseSquare.deve_entails_devia (sq : PortugueseSquare) (w : World) (h : sq.deve w) : sq.devia w

deve ⊨ devia: SN_Xg entails SN_{Xf,g} under ∗-revision (bottom-left → bottom-right). Follows from snXg_entails_snXfg.

theorem Ferreira2023.PortugueseSquare.tinhaQue_entails_devia (sq : PortugueseSquare) (w : World) (h : sq.tinhaQue w) : sq.devia w

tinha que ⊨ devia: SN_Xf entails SN_{Xf,g} (top-right → bottom-right). Follows from snXf_entails_snXfg.

Entailment diamond

The four vertices form a Hasse diagram — entailment flows from SN downward to SN_Xfg through both intermediate vertices:

       tem que (SN)
        ╱        ╲
  tinha que     deve
    (SN_Xf)    (SN_Xg)
        ╲        ╱
       devia (SN_Xfg)

English ambiguity (§3)

theorem Ferreira2023.english_ought_ambiguous_between_vertices : PortugueseModal.dever.force = PortugueseModal.devia.force ∧ PortugueseModal.dever.isXMarked = false ∧ PortugueseModal.devia.isXMarked = true

English ought/should is ambiguous between two square vertices: non-X-marked WN (SN_Xg) and X-marked WN (SN_{Xf,g}).

Portuguese disambiguates overtly: deve vs devia. English collapses them into one form.

English fragment bridge (§3)

English should and ought (from FunctionWords) are both classified as .weakNecessity — the SN_Xg vertex of the square. But unlike Portuguese, English lacks overt X-marking morphology (deve vs devia), so the SN_Xfg reading (counterfactual should) is available but not distinguished.

Note: should carries tense := .Past (morphological past = X-marking), while ought carries no tense marking. Both are semantically present-tense weak necessity in their default readings.

theorem Ferreira2023.english_portuguese_weakNecessity_correspondence : (English.Auxiliaries.should.modalMeaning.all fun (x : Semantics.Modality.ForceFlavor) => x.force == Semantics.Modality.ModalForce.weakNecessity) = true ∧ (English.Auxiliaries.ought.modalMeaning.all fun (x : Semantics.Modality.ForceFlavor) => x.force == Semantics.Modality.ModalForce.weakNecessity) = true ∧ PortugueseModal.dever.force = Semantics.Modality.ModalForce.weakNecessity

English should and ought share Portuguese dever's modal force (.weakNecessity), placing them at the SN_Xg vertex.

theorem Ferreira2023.english_should_has_xmarking_morphology : English.Auxiliaries.should.tense = some UD.Tense.Past ∧ English.Auxiliaries.ought.tense = none

English should has morphological past tense (X-marking), but ought does not. This reflects Iatridou's generalization: X-marking in English is realized as past morphology. Portuguese makes this overt: deve (unmarked) vs devia (past imperfect = X-marked).