Ferreira (2023): A square of necessities

This file formalizes [Fer23]'s square of necessities. Portuguese has a weak necessity modal dever between poder and ter que ((28)–(29), by the test of [Rub21] in (27)), and both necessity modals take past imperfect morphology (devia, tinha que) without a change of force. That morphology is [vFI23]'s X-marking, read after [Sta75] as the suspension of a presupposition: the modal base is replaced by its ∗-revision for the prejacent, which adds the prejacent-worlds most similar to the accessible ones ((79), after [GPB22]). The weak/strong contrast is X-marking of the other parameter: the ∗∗-revision of an ordering source for a proposition makes every best world satisfying it better than every best world failing it (131), and strong necessity under the revised ordering is [vFI08]'s weak necessity, the best of the best worlds under [Kra12b]'s ordering ((129), (133)). The two shifters generate the square (134), which Portuguese fills with tem que, tinha que, deve, devia (135).

Main definitions

• revise, starstar: the ∗-revision of a modal base and the ∗∗-revision of a betterness relation, the two X-marking shifters.
• Vertex, Vertex.necessity: the square (134), a vertex recording which parameters are X-marked, and the necessity operator at a vertex.
• interpret: a modal force read as a Kratzer operator, weak necessity through the ∗∗-revision.
• Pattern.Contradictory, Pattern.Consistent, Profile: the conjunctions of §2 and the four bits of a model that decide them.

Main results

• snXg_iff_weakNecessity: (133), weak necessity is strong necessity with an X-marked ordering source.
• domainIndependent_starstar_iff, not_exists_starstar_orderingSource: the ∗∗-revision is domain-independent exactly when bestness is stable under widening, which a three-world frame refutes, so (131) has no solution among ordering sources.
• Vertex.entails_iff: the entailment order of the square (134). Strong necessity entails every vertex, tinha que entails devia, and nothing else entails anything, which confirms (29) and (82a) and refutes the first half of (82b).
• scale, rubinstein: the scale (28)–(29) and Rubinstein's test (27), decided.
• necessity_iff_interpret: (135), the fragment's force at a vertex is the operator the vertex computes.
• Pattern.contradictory_iff, rows_unacceptable_iff: a conjunction of §2 is contradictory exactly when no valid profile satisfies both conjuncts, and the paper's # judgments ((16)–(25), (30), (32)) are exactly the contradictory ones.
• devia_81, not_devia_80, revise_workday_80, dialogues_predicted: the dialogues (80)–(81) and footnote 18 in a four-world model.

Implementation notes

• The similarity ordering of (41) is a totally realistic ordering source, and (41b)(i) is read with the best worlds drawn from the domain. The ∗-revision is the modal base whose single premise is the widened domain of (79).
• (131) presupposes that a best world stays best when the domain widens, which fails (domainIndependent_starstar_iff), so starstar takes the domain as an argument and a vertex quantifies over the minimal elements of the revised relation (bestOf).
• The ordering revision's target is a contextual parameter different from the prejacent, the asymmetry §4 leaves open, and one target is shared by both conjuncts of a pattern, which is what makes (24) contradictory. Contradictoriness quantifies over models with nonempty best worlds, the deliberative reading of (27ii).
• The dialogues' modal bases are what A says; devia is weak necessity with the workday as the revision's target over a normality ordering.

TODO

• (82b) claims that tem que p does not entail tinha que p. Under (79) and (132a) it does (Vertex.entails_iff): a best world of the widened domain is best in the original domain or an added prejacent-world. The paper's argument, that the best worlds of the two domains need not overlap, does not bear on this. (82a) and the second half of (82b) hold as stated.

References

• [Fer23]
• [vFI08]
• [vFI23]
• [Rub21]
• [Sta75]
• [GPB22]
• [Kra12b]

∗-revision of a modal base (79)

def Ferreira2023.revise {W : Type u_1} (sim f : Modality.Background W) (p : W → Prop) : Modality.Background W

The ∗-revision (79) of f for p under the similarity ordering sim, the modal base whose domain at w is the domain of f together with the p-worlds most similar to some world of it.

Equations

• Ferreira2023.revise sim f p w = {fun (w' : W) => w' ∈ f.accessibleWorlds w ∨ ∃ w'' ∈ f.accessibleWorlds w, w' ∈ (Modality.premisePreorder (sim w'')).minimals {v : W | p v}}

theorem Ferreira2023.accessibleWorlds_revise {W : Type u_1} (sim f : Modality.Background W) (p : W → Prop) (w : W) : (revise sim f p).accessibleWorlds w = f.accessibleWorlds w ∪ {w' : W | ∃ w'' ∈ f.accessibleWorlds w, w' ∈ (Modality.premisePreorder (sim w'')).minimals {v : W | p v}}

theorem Ferreira2023.subset_accessibleWorlds_revise {W : Type u_1} (sim f : Modality.Background W) (p : W → Prop) (w : W) : f.accessibleWorlds w ⊆ (revise sim f p).accessibleWorlds w

The revision widens the domain.

theorem Ferreira2023.prop_of_mem_accessibleWorlds_revise {W : Type u_1} {sim f : Modality.Background W} {p : W → Prop} {w w' : W} (h : w' ∈ (revise sim f p).accessibleWorlds w) (hn : w' ∉ f.accessibleWorlds w) : p w'

Every world the revision adds is a p-world.

theorem Ferreira2023.strongNecessity_revise {W : Type u_1} {f g : Modality.Background W} {q : W → Prop} {w : W} (sim : Modality.Background W) (h : Modality.Directive.strongNecessity f g q w) : Modality.Directive.strongNecessity (revise sim f q) g q w

A best world of a domain is a p-world when nothing adds to it: the ∗-revision for the prejacent preserves strong necessity.

∗∗-revision of an ordering source (130)–(131)

def Ferreira2023.bestOf {W : Type u_1} (R : W → W → Prop) (D : Set W) : Set W

The members of D no member betters under a relation, (41b)(i) for an arbitrary betterness.

Equations

• Ferreira2023.bestOf R D = {u : W | u ∈ D ∧ ∀ v ∈ D, ¬R v u}

theorem Ferreira2023.bestOf_strictlyBetter {W : Type u_1} (A : Set (W → Prop)) (D : Set W) : bestOf (fun (u v : W) => u < v) D = (Modality.premisePreorder A).minimals D

Under the betterness of an ordering source (130), the best worlds are the substrate's.

def Ferreira2023.starstar {W : Type u_1} (g : Modality.Background W) (p : W → Prop) (w : W) (D : Set W) (u v : W) : Prop

The ∗∗-revision (131) of the betterness of g w on D for p, under which in addition every best p-world betters every best non-p-world.

Equations

• Ferreira2023.starstar g p w D u v = (u < v ∨ p u ∧ ¬p v ∧ u ∈ (Modality.premisePreorder (g w)).minimals D ∧ v ∈ (Modality.premisePreorder (g w)).minimals D)

theorem Ferreira2023.bestOf_starstar {W : Type u_1} (g : Modality.Background W) (p : W → Prop) (w : W) (D : Set W) : bestOf (starstar g p w D) D = (Modality.premisePreorder {p}).minimals ((Modality.premisePreorder (g w)).minimals D)

The best worlds under the ∗∗-revision are the p-best of the best, the lexicographic refinement of (129b).

def Ferreira2023.DomainIndependent {W : Type u_1} (F : Set W → W → W → Prop) : Prop

(131) asks for one betterness relation whose restriction to every domain is the ∗∗-revision on that domain.

Equations

• Ferreira2023.DomainIndependent F = ∃ (R : W → W → Prop), ∀ (D : Set W) (u v : W), u ∈ D → v ∈ D → (R u v ↔ F D u v)

theorem Ferreira2023.domainIndependent_starstar_iff {W : Type u_1} (g : Modality.Background W) (p : W → Prop) (w : W) : DomainIndependent (starstar g p w) ↔ ∀ ⦃D D' : Set W⦄, D ⊆ D' → ∀ ⦃u v : W⦄, p u → ¬p v → u ∈ (Modality.premisePreorder (g w)).minimals D → v ∈ (Modality.premisePreorder (g w)).minimals D → u ∈ (Modality.premisePreorder (g w)).minimals D' ∧ v ∈ (Modality.premisePreorder (g w)).minimals D'

The ∗∗-revision is domain-independent exactly when a p-world and a non-p-world that are both best in a domain stay best in every larger domain. Bestness is stable under shrinking a domain (Preorder.mem_minimals_of_subset); (131) presupposes stability under widening.

A three-world frame

Worlds 0 and 1 are incomparable, so both are best among {0, 1}, and 2 betters 1. Widening the domain to the whole frame unseats 1, which is what defeats (131) and, in the countermodels below, the entailment from deve to devia. Three worlds and all three criteria are needed: a p-world and a non-p-world must both be best somewhere, and a third world must better one of them.

@[reducible, inline]

abbrev Ferreira2023.g₃ : Modality.Background (Fin 3)

The ordering source of the three-world frame.

Equations

• Ferreira2023.g₃ x✝ = {fun (x : Fin 3) => x = 0, fun (x : Fin 3) => x = 1 ∨ x = 2, fun (x : Fin 3) => x = 2}

theorem Ferreira2023.minimals_pair_g₃ : (Modality.premisePreorder (g₃ 0)).minimals {0, 1} = {0, 1}

Both worlds of the pair are best in it.

theorem Ferreira2023.minimals_univ_g₃ : (Modality.premisePreorder (g₃ 0)).minimals Set.univ = {0, 2}

Over the whole frame 2 betters 1.

theorem Ferreira2023.not_domainIndependent_starstar : ¬DomainIndependent (starstar g₃ (fun (x : Fin 3) => x = 1) 0)

(131) has no solution on the three-world frame: 1, the p-world, and 0 are both best in the pair, and 1 is not best in the whole frame.

theorem Ferreira2023.not_exists_starstar_orderingSource : ¬∃ (g' : Modality.Background (Fin 3)), ∀ (D : Set (Fin 3)) (u v : Fin 3), u ∈ D → v ∈ D → (u < v ↔ starstar g₃ (fun (x : Fin 3) => x = 1) 0 D u v)

In the paper's terms, no ordering source is a ∗∗-revision of g₃ for (· = 1).

The square of necessities (132)–(134)

def Ferreira2023.snXg {W : Type u_1} (f g : Modality.Background W) (p q : W → Prop) (w : W) : Prop

Strong necessity with the ordering source ∗∗-revised for p (132b).

Equations

• Ferreira2023.snXg f g p q w = ∀ w' ∈ Ferreira2023.bestOf (Ferreira2023.starstar g p w (f.accessibleWorlds w)) (f.accessibleWorlds w), q w'

theorem Ferreira2023.snXg_iff_weakNecessity {W : Type u_1} (f g : Modality.Background W) (p q : W → Prop) (w : W) : snXg f g p q w ↔ Modality.Directive.weakNecessity f g (fun (x : W) => {p}) q w

Weak necessity (133) is strong necessity with an X-marked ordering source, the secondary ordering source of [vFI08] being the revision's target.

structure Ferreira2023.Vertex : Type

A vertex of the square (134) records whether the modal base and the ordering source are X-marked.

• xf : Bool

  The modal base is ∗-revised for the prejacent.

• xg : Bool

  The ordering source is ∗∗-revised.

def Ferreira2023.instDecidableEqVertex.decEq (x✝ x✝¹ : Vertex) : Decidable (x✝ = x✝¹)

Equations

• Ferreira2023.instDecidableEqVertex.decEq { xf := a, xg := a_1 } { xf := b, xg := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Ferreira2023.instDecidableEqVertex : DecidableEq Vertex

Equations

• Ferreira2023.instDecidableEqVertex = Ferreira2023.instDecidableEqVertex.decEq

def Ferreira2023.instReprVertex.repr : Vertex → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Ferreira2023.instReprVertex : Repr Vertex

Equations

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

@[instance_reducible]

instance Ferreira2023.instFintypeVertex : Fintype Vertex

Equations

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

def Ferreira2023.Vertex.base {W : Type u_1} (v : Vertex) (sim f : Modality.Background W) (q : W → Prop) : Modality.Background W

The modal base at a vertex is f or its ∗-revision for the prejacent q (78), (84).

Equations

• v.base sim f q = if v.xf = true then Ferreira2023.revise sim f q else f

def Ferreira2023.Vertex.necessity {W : Type u_1} (v : Vertex) (sim f g : Modality.Background W) (p q : W → Prop) (w : W) : Prop

The necessity at a vertex (134), over the vertex's base and the betterness of g, ∗∗-revised for p when the ordering source is X-marked.

Equations

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

theorem Ferreira2023.Vertex.necessity_xg_false {W : Type u_1} {sim f g : Modality.Background W} {p q : W → Prop} {w : W} (xf : Bool) : { xf := xf, xg := false }.necessity sim f g p q w ↔ Modality.Directive.strongNecessity ({ xf := xf, xg := false }.base sim f q) g q w

Without X-marking of the ordering source, a vertex is strong necessity over its base.

theorem Ferreira2023.Vertex.necessity_xg_true {W : Type u_1} {sim f g : Modality.Background W} {p q : W → Prop} {w : W} (xf : Bool) : { xf := xf, xg := true }.necessity sim f g p q w ↔ Modality.Directive.weakNecessity ({ xf := xf, xg := true }.base sim f q) g (fun (x : W) => {p}) q w

With X-marking of the ordering source, a vertex is weak necessity over its base, the secondary ordering source [p].

The entailment order of the square ((29), (82))

def Ferreira2023.Vertex.Entails (v v' : Vertex) : Prop

Entailment between vertices, over every model whose similarity ordering is totally realistic (41a).

Equations

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

theorem Ferreira2023.Vertex.Entails.refl (v : Vertex) : v.Entails v

theorem Ferreira2023.Vertex.Entails.trans {u v x : Vertex} (h₁ : u.Entails v) (h₂ : v.Entails x) : u.Entails x

theorem Ferreira2023.Vertex.entails_xg (xf : Bool) : { xf := xf, xg := false }.Entails { xf := xf, xg := true }

X-marking the ordering source weakens, at either value of the other parameter (29).

theorem Ferreira2023.Vertex.entails_xf : { xf := false, xg := false }.Entails { xf := true, xg := false }

X-marking the modal base preserves strong necessity.

theorem Ferreira2023.Vertex.entails_of_sn (v : Vertex) : { xf := false, xg := false }.Entails v

Strong necessity entails every vertex.

The first countermodel: nothing excluded, nothing ordered. The Xg vertices hold, since the p-best world is the prejacent-world, and the others fail.

The second countermodel: only the non-prejacent world is accessible, and the ordering prefers the prejacent-world. The revision adds the prejacent-world, which is then best, so the Xf vertices hold and the others fail.

The third countermodel refutes deve q ⊨ devia q on the three-world frame: the base excludes 2, the revision for the prejacent puts it back, and 2 unseats 1, the only p-world. Only deve holds.

theorem Ferreira2023.Vertex.entails_iff (v v' : Vertex) : v.Entails v' ↔ v = v' ∨ v = { xf := false, xg := false } ∨ v = { xf := true, xg := false } ∧ v' = { xf := true, xg := true }

In the entailment order of the square (134), strong necessity entails every vertex, tinha que entails devia, and nothing else entails anything.

theorem Ferreira2023.entails_82 : (¬{ xf := false, xg := true }.Entails { xf := true, xg := true } ∧ ¬{ xf := true, xg := true }.Entails { xf := false, xg := true }) ∧ { xf := false, xg := false }.Entails { xf := true, xg := false } ∧ ¬{ xf := true, xg := false }.Entails { xf := false, xg := false }

In (82), the X-marked weak necessity and its unmarked counterpart are independent, and the X-marked strong necessity does not entail its unmarked counterpart; the unmarked strong necessity does entail the marked one, against the paper's first line of (82b).

Forces as operators

def Ferreira2023.interpret {W : Type u_1} (φ : Modality.ModalForce) (f g : Modality.Background W) (p q : W → Prop) (w : W) : Prop

A force as a Kratzer operator over a modal base and an ordering source, possibility and necessity over the best worlds and weak necessity through the ∗∗-revision for p (132b).

Equations

• Ferreira2023.interpret Modality.ModalForce.possibility f g p q w = Modality.possibility f g q w
• Ferreira2023.interpret Modality.ModalForce.weakNecessity f g p q w = Ferreira2023.snXg f g p q w
• Ferreira2023.interpret Modality.ModalForce.necessity f g p q w = Modality.Directive.strongNecessity f g q w

def Ferreira2023.modalAt : Vertex → Auxiliary

The Portuguese necessity modal at each vertex (135). X-marking the ordering source is lexical, from ter que to dever, and X-marking the modal base is the past imperfect.

Equations

• Ferreira2023.modalAt { xf := false, xg := false } = Portuguese.Modals.terQue
• Ferreira2023.modalAt { xf := false, xg := true } = Portuguese.Modals.dever
• Ferreira2023.modalAt { xf := true, xg := false } = Portuguese.Modals.tinhaQue
• Ferreira2023.modalAt { xf := true, xg := true } = Portuguese.Modals.devia

def Ferreira2023.square (v : Vertex) : Modality.ModalItem

The modal item at a vertex.

Equations

• Ferreira2023.square v = (Ferreira2023.modalAt v).toModalItem

theorem Ferreira2023.tense_square (v : Vertex) : (modalAt v).tense = some UD.Tense.Imp ↔ v.xf = true

The fragment's modal at a vertex is in the past imperfect exactly when the modal base is X-marked (135).

theorem Ferreira2023.forces_square (v : Vertex) : (square v).forces = {if v.xg = true then Modality.ModalForce.weakNecessity else Modality.ModalForce.necessity}

The fragment's force at a vertex is weak necessity exactly when the ordering source is X-marked (83), (135).

theorem Ferreira2023.necessity_iff_interpret {W : Type u_1} {sim f g : Modality.Background W} {p q : W → Prop} {w : W} {φ : Modality.ModalForce} (v : Vertex) (hφ : φ ∈ (square v).forces) : v.necessity sim f g p q w ↔ interpret φ (v.base sim f q) g p q w

Semantically (135), the necessity at a vertex is the operator of the force the fragment gives the vertex's modal, over the vertex's base.

The conjunctions of §2

structure Ferreira2023.Conjunct : Type

A conjunct is a modal of some force over the prejacent or its negation, possibly negated.

• force : Modality.ModalForce

  The force of the modal.

• negModal : Bool

  The modal is negated.

• negPrejacent : Bool

  The prejacent is negated.

def Ferreira2023.instDecidableEqConjunct.decEq (x✝ x✝¹ : Conjunct) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Ferreira2023.instDecidableEqConjunct : DecidableEq Conjunct

Equations

• Ferreira2023.instDecidableEqConjunct = Ferreira2023.instDecidableEqConjunct.decEq

def Ferreira2023.instReprConjunct.repr : Conjunct → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Ferreira2023.instReprConjunct : Repr Conjunct

Equations

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

def Ferreira2023.Conjunct.holds {W : Type u_1} (c : Conjunct) (f g : Modality.Background W) (p q : W → Prop) (w : W) : Prop

The conjunct's truth at w, p the target of weak necessity's ordering revision and q the prejacent.

Equations

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

def Ferreira2023.Conjunct.Entails (c₁ c₂ : Conjunct) : Prop

Entailment between conjuncts over every model with nonempty best worlds, the conclusion of a deliberation (27ii).

Equations

• c₁.Entails c₂ = ∀ (W : Type) (f g : Modality.Background W) (p q : W → Prop) (w : W), (Modality.bestWorlds f g w).Nonempty → c₁.holds f g p q w → c₂.holds f g p q w

structure Ferreira2023.Pattern : Type

A conjunction of two modal claims about one prejacent, with one target for the ordering revision.

• first : Conjunct

  The first conjunct.

• second : Conjunct

  The second conjunct.

@[instance_reducible]

instance Ferreira2023.instDecidableEqPattern : DecidableEq Pattern

Equations

• Ferreira2023.instDecidableEqPattern = Ferreira2023.instDecidableEqPattern.decEq

def Ferreira2023.instDecidableEqPattern.decEq (x✝ x✝¹ : Pattern) : Decidable (x✝ = x✝¹)

Equations

• Ferreira2023.instDecidableEqPattern.decEq { first := a, second := a_1 } { first := b, second := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Ferreira2023.instReprPattern : Repr Pattern

Equations

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

def Ferreira2023.instReprPattern.repr : Pattern → ℕ → Std.Format

Equations

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

def Ferreira2023.Pattern.Contradictory (pat : Pattern) : Prop

The conjunction is contradictory as the conclusion of a deliberation: false in every model with nonempty best worlds.

Equations

• pat.Contradictory = ∀ (W : Type) (f g : Modality.Background W) (p q : W → Prop) (w : W), (Modality.bestWorlds f g w).Nonempty → ¬(pat.first.holds f g p q w ∧ pat.second.holds f g p q w)

def Ferreira2023.Pattern.Consistent (pat : Pattern) : Prop

The conjunction has a model with nonempty best worlds.

Equations

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

Profiles: the four bits of a model that decide the conjunctions

structure Ferreira2023.Profile : Type

Which of the prejacent and its negation hold at some best world, and at some p-best of the best worlds.

• bestQ : Bool

  Some best world is a prejacent-world.

• bestNotQ : Bool

  Some best world is not a prejacent-world.

• topQ : Bool

  Some p-best of the best worlds is a prejacent-world.

• topNotQ : Bool

  Some p-best of the best worlds is not a prejacent-world.

@[instance_reducible]

instance Ferreira2023.instDecidableEqProfile : DecidableEq Profile

Equations

• Ferreira2023.instDecidableEqProfile = Ferreira2023.instDecidableEqProfile.decEq

def Ferreira2023.instDecidableEqProfile.decEq (x✝ x✝¹ : Profile) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Ferreira2023.instReprProfile : Repr Profile

Equations

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

def Ferreira2023.instReprProfile.repr : Profile → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Ferreira2023.instFintypeProfile : Fintype Profile

Equations

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

noncomputable def Ferreira2023.profile {W : Type u_1} (f g : Modality.Background W) (p q : W → Prop) (w : W) : Profile

The profile of a model at w.

Equations

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

def Ferreira2023.Profile.Valid (π : Profile) : Prop

A profile is valid when it is the profile of a model with nonempty best worlds, whose p-best best worlds are nonempty and best.

Equations

• π.Valid = ((π.topQ = true ∨ π.topNotQ = true) ∧ (π.topQ = true → π.bestQ = true) ∧ (π.topNotQ = true → π.bestNotQ = true))

@[instance_reducible]

instance Ferreira2023.instDecidablePredProfileValid : DecidablePred Profile.Valid

Equations

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

theorem Ferreira2023.minimals_singleton_nonempty {W : Type u_1} {S : Set W} (hS : S.Nonempty) (p : W → Prop) : ((Modality.premisePreorder {p}).minimals S).Nonempty

The p-best of a nonempty set are nonempty: a p-member if there is one, else all.

theorem Ferreira2023.profile_valid {W : Type u_1} {f g : Modality.Background W} {p q : W → Prop} {w : W} (hne : (Modality.bestWorlds f g w).Nonempty) : (profile f g p q w).Valid

def Ferreira2023.Conjunct.evalP (π : Profile) (c : Conjunct) : Bool

A conjunct's truth value on a profile.

Equations

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

theorem Ferreira2023.Conjunct.holds_iff_evalP {W : Type u_1} (c : Conjunct) (f g : Modality.Background W) (p q : W → Prop) (w : W) : c.holds f g p q w ↔ evalP (profile f g p q w) c = true

A conjunct's truth depends on the model only through its profile.

theorem Ferreira2023.Profile.Valid.exists_model {π : Profile} (hπ : π.Valid) : ∃ (f : Modality.Background Bool) (g : Modality.Background Bool) (p : Bool → Prop) (q : Bool → Prop), (Modality.bestWorlds f g true).Nonempty ∧ profile f g p q true = π

Every valid profile is the profile of a two-world model.

theorem Ferreira2023.Pattern.contradictory_iff (pat : Pattern) : pat.Contradictory ↔ ∀ (π : Profile), π.Valid → ¬(Conjunct.evalP π pat.first = true ∧ Conjunct.evalP π pat.second = true)

A conjunction is contradictory exactly when no valid profile satisfies both conjuncts.

theorem Ferreira2023.Pattern.consistent_iff (pat : Pattern) : pat.Consistent ↔ ∃ (π : Profile), π.Valid ∧ Conjunct.evalP π pat.first = true ∧ Conjunct.evalP π pat.second = true

A conjunction is consistent exactly when some valid profile satisfies both conjuncts.

theorem Ferreira2023.Conjunct.entails_iff (c₁ c₂ : Conjunct) : c₁.Entails c₂ ↔ ∀ (π : Profile), π.Valid → evalP π c₁ = true → evalP π c₂ = true

A conjunct entails another exactly when it does on every valid profile.

@[instance_reducible]

instance Ferreira2023.instDecidablePredPatternContradictory : DecidablePred Pattern.Contradictory

Equations

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

@[instance_reducible]

instance Ferreira2023.instDecidablePredPatternConsistent : DecidablePred Pattern.Consistent

Equations

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

@[instance_reducible]

instance Ferreira2023.instDecidableRelConjunctEntails : DecidableRel Conjunct.Entails

Equations

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

theorem Ferreira2023.Pattern.consistent_iff_not_contradictory (pat : Pattern) : pat.Consistent ↔ ¬pat.Contradictory

theorem Ferreira2023.scale (φ ψ : Modality.ModalForce) (n : Bool) : φ ≤ ψ ↔ { force := ψ, negModal := false, negPrejacent := n }.Entails { force := φ, negModal := false, negPrejacent := n }

The scale of forces (28)–(29) is the entailment order, the prejacent held fixed, and no entailment runs up the scale.

theorem Ferreira2023.rubinstein : ({ force := Modality.ModalForce.necessity, negModal := false, negPrejacent := false }.Entails { force := Modality.ModalForce.weakNecessity, negModal := false, negPrejacent := false } ∧ ¬{ force := Modality.ModalForce.weakNecessity, negModal := false, negPrejacent := false }.Entails { force := Modality.ModalForce.necessity, negModal := false, negPrejacent := false }) ∧ { first := { force := Modality.ModalForce.weakNecessity, negModal := false, negPrejacent := false }, second := { force := Modality.ModalForce.weakNecessity, negModal := false, negPrejacent := true } }.Contradictory

Dever passes Rubinstein's test for weak necessity (27). It is entailed by ter que and not conversely, and dever p and dever ¬p are contradictory.

The paradigm ((16)–(25), (30), (32))

def Ferreira2023.conjunctTable : List (String × Conjunct)

The conjuncts of the paper's examples, keyed as in Data/Examples/Ferreira2023.json.

Equations

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

structure Ferreira2023.Row : Type

A row pairs a conjunction with the paper's judgment.

• pattern : Pattern

  The conjunction.

• judgment : Judgment

  The paper's judgment.

def Ferreira2023.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

• Ferreira2023.instDecidableEqRow.decEq { pattern := a, judgment := a_1 } { pattern := b, judgment := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Ferreira2023.instDecidableEqRow : DecidableEq Row

Equations

• Ferreira2023.instDecidableEqRow = Ferreira2023.instDecidableEqRow.decEq

@[instance_reducible]

instance Ferreira2023.instReprRow : Repr Row

Equations

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

def Ferreira2023.instReprRow.repr : Row → ℕ → Std.Format

Equations

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

def Ferreira2023.Row.ofDatum (ex : Datum) : Option Row

The row of an example tagged with two conjuncts.

Equations

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

theorem Ferreira2023.row_ofDatum_isSome (ex : Datum) : ex ∈ Examples.all → (ex.feature? "first").isSome = true → (Row.ofDatum ex).isSome = true

Every example tagged with a first conjunct parses.

def Ferreira2023.rows : List Row

The conjunctions of §2.

Equations

• Ferreira2023.rows = List.filterMap Ferreira2023.Row.ofDatum Ferreira2023.Examples.all

theorem Ferreira2023.rows_unacceptable_iff (r : Row) : r ∈ rows → (r.judgment = Judgment.unacceptable ↔ r.pattern.Contradictory)

A conjunction of (16)–(25), (30) or (32) is judged # exactly when it is contradictory.

(80)–(81): suspending the knowledge that Peter is not in his office

structure Ferreira2023.Day : Type

A world of the dialogues records whether Peter is in his office and whether the day is a holiday.

• office : Bool

  Peter is in his office.

• holiday : Bool

  The day is a holiday.

theorem Ferreira2023.Day.ext {x y : Day} (office : x.office = y.office) (holiday : x.holiday = y.holiday) : x = y

theorem Ferreira2023.Day.ext_iff {x y : Day} : x = y ↔ x.office = y.office ∧ x.holiday = y.holiday

@[instance_reducible]

instance Ferreira2023.instDecidableEqDay : DecidableEq Day

Equations

• Ferreira2023.instDecidableEqDay = Ferreira2023.instDecidableEqDay.decEq

def Ferreira2023.instDecidableEqDay.decEq (x✝ x✝¹ : Day) : Decidable (x✝ = x✝¹)

Equations

• Ferreira2023.instDecidableEqDay.decEq { office := a, holiday := a_1 } { office := b, holiday := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Ferreira2023.instReprDay.repr : Day → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Ferreira2023.instReprDay : Repr Day

Equations

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

@[instance_reducible]

instance Ferreira2023.instFintypeDay : Fintype Day

Equations

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

def Ferreira2023.Day.sim : Modality.Background Day

Similarity by agreement on each coordinate, a totally realistic ordering source (41a).

Equations

• w.sim = {fun (v : Ferreira2023.Day) => v.office = w.office, fun (v : Ferreira2023.Day) => v.holiday = w.holiday}

theorem Ferreira2023.Day.sim_isTotallyRealistic : sim.IsTotallyRealistic

def Ferreira2023.Day.normal : Modality.Background Day

Normally people are in the office on workdays and not on holidays.

Equations

• x✝.normal = {fun (v : Ferreira2023.Day) => v.holiday = true → v.office = false, fun (v : Ferreira2023.Day) => v.holiday = false → v.office = true}

def Ferreira2023.Day.atOffice (v : Day) : Prop

The prejacent, that Peter is in his office.

Equations

• v.atOffice = (v.office = true)

def Ferreira2023.Day.workday (v : Day) : Prop

The target of the ordering revision, that the day is a workday.

Equations

• v.workday = (v.holiday = false)

def Ferreira2023.Day.checked : Modality.Background Day

A has checked, and Peter is not in his office (81).

Equations

• x✝.checked = {fun (v : Ferreira2023.Day) => v.office = false}

def Ferreira2023.Day.holidayInfo : Modality.Background Day

A has said that the day is a holiday (80).

Equations

• x✝.holidayInfo = {fun (v : Ferreira2023.Day) => v.holiday = true}

theorem Ferreira2023.Day.deve_guess (w : Day) : { xf := false, xg := true }.necessity sim ⊥ normal workday atOffice w

B guesses that, with nothing known, normality on a workday puts Peter in his office.

theorem Ferreira2023.Day.devia_81 (w : Day) : ¬{ xf := false, xg := true }.necessity sim checked normal workday atOffice w ∧ { xf := true, xg := true }.necessity sim checked normal workday atOffice w

After A has checked (81), deve is false and devia is true. Suspending the knowledge that Peter is not in his office reinstates the bias towards his being there.

theorem Ferreira2023.Day.not_devia_80 (w : Day) : ¬{ xf := true, xg := true }.necessity sim holidayInfo normal workday atOffice w

On a holiday (80) the suspension adds only holiday worlds, and devia is false.

theorem Ferreira2023.Day.revise_workday_80 (w : Day) : { xf := false, xg := true }.necessity sim (revise sim holidayInfo workday) normal workday atOffice w

Revising the base of (80) for the salient proposition, the workday, instead of the prejacent would wrongly make devia true (footnote 18).

def Ferreira2023.Day.baseTable : List (String × Modality.Background Day)

The modal base of each dialogue, keyed as in the JSON, is what A has said.

Equations

• Ferreira2023.Day.baseTable = [("checked", Ferreira2023.Day.checked), ("holiday", Ferreira2023.Day.holidayInfo)]

theorem Ferreira2023.Day.dialogues_predicted (ex : Datum) : ex ∈ [Examples.ex_80, Examples.ex_81] → ∃ b ∈ ex.parse? "base" baseTable, ex.judgment = Judgment.acceptable ↔ ∀ (w : Day), { xf := true, xg := true }.necessity sim b normal workday atOffice w

In (80)–(81), devia is judged true exactly when the X-marked weak necessity holds over what A has said.