Ferreira (2023): A square of necessities

@cite{ferreira-2023}

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.

@[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 → Core.Modality.ModalForce

Modal force of each form.

Equations

• Ferreira2023.PortugueseModal.poder.force = Core.Modality.ModalForce.possibility
• Ferreira2023.PortugueseModal.podia.force = Core.Modality.ModalForce.possibility
• Ferreira2023.PortugueseModal.dever.force = Core.Modality.ModalForce.weakNecessity
• Ferreira2023.PortugueseModal.devia.force = Core.Modality.ModalForce.weakNecessity
• Ferreira2023.PortugueseModal.terQue.force = Core.Modality.ModalForce.necessity
• Ferreira2023.PortugueseModal.tinhaQue.force = Core.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 : Core.Modality.ModalForce.necessity.atLeastAsStrong Core.Modality.ModalForce.weakNecessity = true ∧ Core.Modality.ModalForce.weakNecessity.atLeastAsStrong Core.Modality.ModalForce.possibility = true ∧ Core.Modality.ModalForce.possibility.atLeastAsStrong Core.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 : Core.Logic.Intensional.ModalBase World) (g : Core.Logic.Intensional.OrderingSource World) (p : World → Prop) (w : World) (h : Semantics.Modality.Kratzer.XMarking.sn f g p w) : Semantics.Modality.Kratzer.XMarking.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 : Core.Logic.Intensional.ModalBase World) (g : Core.Logic.Intensional.OrderingSource World) (p : World → Prop) (w : World), Semantics.Modality.Kratzer.XMarking.snXg f g p w → Semantics.Modality.Kratzer.XMarking.sn f g p w

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

theorem Ferreira2023.dever_entails_poder (f : Core.Logic.Intensional.ModalBase World) (g : Core.Logic.Intensional.OrderingSource World) (p : World → Prop) (w : World) (hSerial : (Semantics.Modality.Kratzer.bestWorlds f (Semantics.Modality.Kratzer.XMarking.xMarkOrdering g p) w).Nonempty) (h : Semantics.Modality.Kratzer.XMarking.snXg f g p w) : Semantics.Modality.Kratzer.possibility f (Semantics.Modality.Kratzer.XMarking.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 : Core.Logic.Intensional.ModalBase World) (g : Core.Logic.Intensional.OrderingSource World) (p : World → Prop) (w : World), Semantics.Modality.Kratzer.XMarking.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 : Core.Logic.Intensional.ModalBase World) (g : Core.Logic.Intensional.OrderingSource World) (p : World → Prop) (w : World) (hReal : ∀ (w : World), Semantics.Modality.Kratzer.accessibleWorlds f w = {w}) (hSN : Semantics.Modality.Kratzer.XMarking.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' : Core.Logic.Intensional.ModalBase World) (g : Core.Logic.Intensional.OrderingSource World) (p : World → Prop) (w : World), Semantics.Modality.Kratzer.XMarking.IsStarRevision f f' p → Semantics.Modality.Kratzer.XMarking.snXfg f' g p w → Semantics.Modality.Kratzer.XMarking.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 : Core.Logic.Intensional.ModalBase World

  Modal base (epistemic/circumstantial)

• fStar : Core.Logic.Intensional.ModalBase World

  ∗-revised modal base

• g : Core.Logic.Intensional.OrderingSource World

  Ordering source

• p : World → Prop

  Prejacent

• hRev : Semantics.Modality.Kratzer.XMarking.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 = Semantics.Modality.Kratzer.XMarking.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 = Semantics.Modality.Kratzer.XMarking.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 = Semantics.Modality.Kratzer.XMarking.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 = Semantics.Modality.Kratzer.XMarking.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 : (Fragments.English.Auxiliaries.should.modalMeaning.all fun (x : Core.Modality.ForceFlavor) => x.force == Core.Modality.ModalForce.weakNecessity) = true ∧ (Fragments.English.Auxiliaries.ought.modalMeaning.all fun (x : Core.Modality.ForceFlavor) => x.force == Core.Modality.ModalForce.weakNecessity) = true ∧ PortugueseModal.dever.force = Core.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 : Fragments.English.Auxiliaries.should.tense = some UD.Tense.Past ∧ Fragments.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).