Močnik and Abramovitz (2019): a variable-force variable-flavor attitude verb in Koryak

Močnik and Abramovitz document the Koryak attitude verb ivək, translated 'say' out of context, which also means 'think' and 'allow for the possibility that'. It varies in force and in flavor, against Nauze's universal that a modal varies on one axis only.

Their entry (15) quantifies universally over the worlds a subset selection function picks from a domain, after Rullmann, Matthewson and Davis, and closes the function existentially over a cover that the context resolves either to the identity, the default, or to all nonempty selections (Cover). The identity cover gives the box over the domain and the full cover the diamond (Frame.ivek_identity_iff, Frame.ivek_all_iff), so the force varies with the cover. A modal-base-like variable sets the domain to the holder's belief worlds or to the worlds compatible with what the holder says (Flavor), so the flavor varies with it. The two are independent parameters, and the entry's force-flavor pairs are the product of two forces and two flavors (meaning_eq), varying on both axes (not_singleAxis_meaning). The pairs the paper attests vary on both axes too (not_singleAxis_attested).

The cover accounts for the conjunctions of §2. ivək of two incompatible complements is contradictory on the identity cover (Frame.not_ivek_identity_and) and consistent on the full cover (Frame.ivek_all_and_iff), the contrast between the necessity and possibility readings of (6) and (8a). The felicitous reading of (8b) is the negated box, and its full-cover reading is the one on which the ball is neither white nor black (Frame.ex8b_all_iff), false in the context of (8) (Frame.ex8b_all_false). The flavor accounts for §3: the two ivəks of (14), set apart by an adverb, are consistent on different flavors (ex14_consistent), while one ivək over clauses that contradict each other, (20), is false on every reading (Frame.not_ivek_and_not). On the doxastic flavor and the identity cover ivək is the non-veridical believe of Hintikka (Frame.ivek_doxastic_identity_iff_holdsAt).

Implementation notes

• The entry's domain is a set of worlds; here it is the set accessible from the evaluation world by the holder's belief or sayings relation.
• (13) writes the second colour of (8b) as the negation of the first, which makes its full-cover reading contradictory in every context. The prose reading, that the ball is half white and half black, needs the two colours as separate predicates, and so they are here.
• attested leaves out the existential 'say' of footnote 10, which the paper could not confirm and the entry predicts (attested_ssubset_meaning).

TODO

• §4: the bouletic readings, split at LF into the doxastic ivək and an item in the embedded clause, the counterfactual mood (23) and the covert des (26), over the information-state index of [Yal07].

References

• [MA19]
• [Nau08]
• [RMD08]
• [Hin62]
• [Yal07]

Force: a universal over a selected subset

inductive MocnikAbramovitz2019.Cover : Type

The cover C of (11) resolves to the identity on the domain, the default, or all subset selection functions, which pick a nonempty subset of it.

• identity : Cover
• all : Cover

@[instance_reducible]

instance MocnikAbramovitz2019.instDecidableEqCover : DecidableEq Cover

Equations

• MocnikAbramovitz2019.instDecidableEqCover x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance MocnikAbramovitz2019.instFintypeCover : Fintype Cover

Equations

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

def MocnikAbramovitz2019.Cover.funs {W : Type u_1} : Cover → Set W → Set (Set W → Set W)

The selection functions a resolution admits over the domain D.

Equations

• MocnikAbramovitz2019.Cover.identity.funs x✝ = {f : Set W → Set W | f x✝ = x✝}
• MocnikAbramovitz2019.Cover.all.funs x✝ = {f : Set W → Set W | f x✝ ⊆ x✝ ∧ (f x✝).Nonempty}

def MocnikAbramovitz2019.Cover.force : Cover → Modality.ModalForce

The force of a resolution, by holds_identity_iff and holds_all_iff.

Equations

• MocnikAbramovitz2019.Cover.identity.force = Modality.ModalForce.necessity
• MocnikAbramovitz2019.Cover.all.force = Modality.ModalForce.possibility

def MocnikAbramovitz2019.Holds {W : Type u_1} (c : Cover) (D : Set W) (p : W → Prop) : Prop

The quantification of (11) over a domain D holds when some admitted selection function maps D into p.

Equations

• MocnikAbramovitz2019.Holds c D p = ∃ f ∈ c.funs D, ∀ v ∈ f D, p v

theorem MocnikAbramovitz2019.holds_identity_iff {W : Type u_1} {D : Set W} {p : W → Prop} : Holds Cover.identity D p ↔ ∀ v ∈ D, p v

On the identity cover the quantification is universal over the domain.

theorem MocnikAbramovitz2019.holds_all_iff {W : Type u_1} {D : Set W} {p : W → Prop} : Holds Cover.all D p ↔ ∃ v ∈ D, p v

On the full cover it is existential, a selection function picking out a single witness.

Flavor: the domain of quantification

inductive MocnikAbramovitz2019.Flavor : Type

The flavors of ivək, the values its modal-base-like variable takes in (15): the holder's belief worlds or the worlds compatible with what the holder says.

• doxastic : Flavor
• assertive : Flavor

@[instance_reducible]

instance MocnikAbramovitz2019.instDecidableEqFlavor : DecidableEq Flavor

Equations

• MocnikAbramovitz2019.instDecidableEqFlavor x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance MocnikAbramovitz2019.instFintypeFlavor : Fintype Flavor

Equations

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

structure MocnikAbramovitz2019.Frame (W : Type u_3) (E : Type u_4) : Type (max u_3 u_4)

For a holder at a world, the worlds compatible with what the holder believes and with what the holder says.

• belief : E → SetRel W W
• sayings : E → SetRel W W

def MocnikAbramovitz2019.Frame.access {W : Type u_1} {E : Type u_2} (F : Frame W E) : Flavor → E → SetRel W W

The accessibility relation a flavor selects.

Equations

• F.access MocnikAbramovitz2019.Flavor.doxastic = F.belief
• F.access MocnikAbramovitz2019.Flavor.assertive = F.sayings

def MocnikAbramovitz2019.Frame.ivek {W : Type u_1} {E : Type u_2} (F : Frame W E) (φ : Flavor) (c : Cover) (p : W → Prop) (x : E) (w : W) : Prop

By the entry (15), ivək on a flavor and a cover holds when some admitted selection from the holder's domain maps it into the complement.

Equations

• F.ivek φ c p x w = MocnikAbramovitz2019.Holds c {v : W | (w, v) ∈ F.access φ x} p

theorem MocnikAbramovitz2019.Frame.ivek_identity_iff {W : Type u_1} {E : Type u_2} {p : W → Prop} {F : Frame W E} {φ : Flavor} {x : E} {w : W} : F.ivek φ Cover.identity p x w ↔ ModalLogic.Box (F.access φ x) p w

On the identity cover ivək is the box over the flavor's accessibility relation.

theorem MocnikAbramovitz2019.Frame.ivek_all_iff {W : Type u_1} {E : Type u_2} {p : W → Prop} {F : Frame W E} {φ : Flavor} {x : E} {w : W} : F.ivek φ Cover.all p x w ↔ ModalLogic.Diamond (F.access φ x) p w

On the full cover ivək is the diamond.

theorem MocnikAbramovitz2019.Frame.ivek_doxastic_identity_iff_holdsAt {W : Type u_1} {E : Type u_2} {p : W → Prop} {F : Frame W E} {x : E} {w : W} : F.ivek Flavor.doxastic Cover.identity p x w ↔ { access := F.belief, veridicality := Doxastic.Veridicality.nonVeridical }.HoldsAt x p w

On the doxastic flavor and the identity cover ivək is the non-veridical believe of [Hin62].

Conjunction and negation, §2

theorem MocnikAbramovitz2019.Frame.not_ivek_identity_and {W : Type u_1} {E : Type u_2} {p q : W → Prop} {F : Frame W E} {φ : Flavor} {x : E} {w : W} (h : ∃ (v : W), (w, v) ∈ F.access φ x) (hpq : ∀ (v : W), (w, v) ∈ F.access φ x → p v → ¬q v) : ¬(F.ivek φ Cover.identity p x w ∧ F.ivek φ Cover.identity q x w)

On the identity cover ivək of two complements that are incompatible over a nonempty domain is contradictory: Option 1 of (12) for (6), and the necessity reading of (8a).

theorem MocnikAbramovitz2019.Frame.ivek_all_and_iff {W : Type u_1} {E : Type u_2} {p q : W → Prop} {F : Frame W E} {φ : Flavor} {x : E} {w : W} : F.ivek φ Cover.all p x w ∧ F.ivek φ Cover.all q x w ↔ (∃ (v : W), (w, v) ∈ F.access φ x ∧ p v) ∧ ∃ (v : W), (w, v) ∈ F.access φ x ∧ q v

On the full cover the two hold together when the domain leaves both complements open: Option 2 of (12) for (6), and the possibility reading of (8a).

theorem MocnikAbramovitz2019.Frame.ex8b_identity_iff {W : Type u_1} {E : Type u_2} {F : Frame W E} {φ : Flavor} {x : E} {w : W} {white black : W → Prop} : ¬F.ivek φ Cover.identity white x w ∧ ¬F.ivek φ Cover.identity black x w ↔ (∃ (v : W), (w, v) ∈ F.access φ x ∧ ¬white v) ∧ ∃ (v : W), (w, v) ∈ F.access φ x ∧ ¬black v

On the identity cover (8b) is the felicitous Option 1 of (13), on which the holder's beliefs leave open that the ball is not white and that it is not black.

theorem MocnikAbramovitz2019.Frame.ex8b_all_iff {W : Type u_1} {E : Type u_2} {F : Frame W E} {φ : Flavor} {x : E} {w : W} {white black : W → Prop} : ¬F.ivek φ Cover.all white x w ∧ ¬F.ivek φ Cover.all black x w ↔ ModalLogic.Box (F.access φ x) (fun (v : W) => ¬white v ∧ ¬black v) w

(8b) on the full cover is the reading on which the ball is neither white nor black, which the paper glosses as half white and half black.

theorem MocnikAbramovitz2019.Frame.ex8b_all_false {W : Type u_1} {E : Type u_2} {F : Frame W E} {φ : Flavor} {x : E} {w : W} {white black : W → Prop} (h : ∃ (v : W), (w, v) ∈ F.access φ x) (hctx : ∀ (v : W), (w, v) ∈ F.access φ x → white v ∨ black v) : ¬(¬F.ivek φ Cover.all white x w ∧ ¬F.ivek φ Cover.all black x w)

In the context of (8), where the ball is white or black in every world the domain admits, the full-cover reading of (8b) is false: the infelicitous Option 2 of (13).

One flavor for each ivək, §3

theorem MocnikAbramovitz2019.Frame.not_ivek_and_not {W : Type u_1} {E : Type u_2} {p : W → Prop} {F : Frame W E} {φ : Flavor} {x : E} {w : W} (h : ∃ (v : W), (w, v) ∈ F.access φ x) (c : Cover) : ¬F.ivek φ c (fun (v : W) => p v ∧ ¬p v) x w

One ivək over two clauses that contradict each other, as in (20), is false on every reading over a nonempty domain, the one flavor holding of both.

theorem MocnikAbramovitz2019.ex14_consistent : ∃ (F : Frame Bool Unit) (p : Bool → Prop), (∃ (v : Bool), (true, v) ∈ F.sayings ()) ∧ (∃ (v : Bool), (true, v) ∈ F.belief ()) ∧ F.ivek Flavor.assertive Cover.identity p () true ∧ F.ivek Flavor.doxastic Cover.identity (fun (v : Bool) => ¬p v) () true

In (14) the two ivəks of a discourse, set to the assertive and the doxastic flavor, say that the students study well and think that they study badly, on nonempty domains.

The force-flavor pairs

def MocnikAbramovitz2019.meaning : Finset (Modality.ModalForce × Flavor)

The force-flavor pairs ivək expresses on the entry, one for each resolution of the cover and each flavor.

Equations

• MocnikAbramovitz2019.meaning = Finset.image (fun (r : MocnikAbramovitz2019.Cover × MocnikAbramovitz2019.Flavor) => (r.1.force, r.2)) Finset.univ

theorem MocnikAbramovitz2019.meaning_eq : meaning = {Modality.ModalForce.necessity, Modality.ModalForce.possibility} ×ˢ Finset.univ

The cover and the flavor are independent parameters, so the pairs are the product of two forces and the two flavors.

theorem MocnikAbramovitz2019.not_singleAxis_meaning : ¬Modality.SingleAxis meaning

ivək varies in force and in flavor, against the universal (1) of [Nau08].

def MocnikAbramovitz2019.attested : Finset (Modality.ModalForce × Flavor)

The paper attests the pairs 'think' (2), 'allow for the possibility' (4), (6), (8a), and 'say' (2), (7). Footnote 10 could not confirm an existential 'say'.

Equations

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

theorem MocnikAbramovitz2019.attested_ssubset_meaning : attested ⊂ meaning ∧ (Modality.ModalForce.possibility, Flavor.assertive) ∈ meaning \ attested

The entry predicts the existential 'say' that the paper could not confirm.

theorem MocnikAbramovitz2019.not_singleAxis_attested : ¬Modality.SingleAxis attested

The attested pairs alone vary on both axes.