Matthewson (2016): Modality

This file formalizes the typological claims of the handbook chapter [Mat16]. On flavour, [Kra12b] projects a conversational background in a factual mode, over the worlds holding counterparts of some actual situation or body of evidence, or in a content mode, over the worlds compatible with what some source of information says. A factual background is therefore realistic, and realism is exactly the veridicality of necessity, so a factual modal cannot be followed by the denial of its prejacent while a content modal can: the rumor of (23)–(24), and St'át'imcets k'a against lákw7a in (25)–(28). Deniability diagnoses the content mode rather than ruling out a modal analysis of an evidential. With the circumstantial–evidential division, whether a background encodes an information source, the modes give Table 18.3's three classes, which St'át'imcets lexicalizes in full, and Gitksan keeps its epistemic and circumstantial modals apart.

On force, Gitksan ima('a) and g̱at, variable in force, and Nez Perce o'qa, a possibility modal that no necessity modal competes with ([Dea11]), are modals without duals, and o'qa's necessity uses vanish in downward-entailing contexts, as [Dea11]'s account of modals without scales predicts. Nsyilxcen mat is used in possibility and necessity contexts and cmay in possibility contexts only ([Men13]), which raises questions for the view that possibility modals are weak through the scalar implicature a contrasting necessity modal induces: no lexical forces let the scalar account alone predict both. On modal–temporal interaction, epistemic modals take a past temporal perspective in Blackfoot, Ktunaxa, St'át'imcets and Gitksan, and Gitksan marks future orientation with the prospective dim where English marks past orientation with the perfect, a mirror image of [Con02]'s scopings and [Mat13]'s paradigms. On typology, Gitksan and Niuean, the chapter's cases of epistemic modals lacking duals, distinguish force among circumstantial modals and not among epistemic ones: in each, a circumstantial possibility modal and a necessity modal are duals and no epistemic modal has one. [VK13b]'s refinement of [Nau08]'s universal, one axis of variation per modal domain, is strictly stronger than the universal and holds of Gitksan.

Implementation notes

• A factual-mode base is realistic, the actual world holding the situation or evidence whose counterparts it projects, and a content-mode base is unconstrained. Deniability is stated for simple necessity, the force of must in (23)–(24), without the stereotypical ordering source whose wiggle room the chapter allows the factual (23).
• The rows are joined to the fragments through parse? tables, and every row naming a modal resolves (rows_resolve), so no row theorem holds by a failed lookup.
• Duals, force distinctions and [Nau08]'s axes compare necessity with possibility, weak necessity counting as necessity (ModalItem.classical): Table 18.1's sgi is a (weak) necessity modal varying only in flavour. The chapter's weak necessity and graded modality (§18.3.1) are not formalized.
• A dual is a modal of the other force sharing a flavour, the necessity–possibility pairs of §18.3.1 and the same-domain condition on [Dea11]'s scales.
• Table 18.4's hypothetical root system has a teleological flavour, which the library folds into circumstantial; bouletic stands in for it, which keeps the system ambiguous along both axes.
• The English row of Table 18.3 (can, might, must) is not formalized, no fragment recording the source or mode of the English modals.
• §18.3.2 contrasts [Pet10]'s ima('a), a possibility modal strengthened by an ordering source, with [Dea11]'s o'qa; the two part only in downward-entailing contexts, where the chapter finds ima('a) untestable, so Peterson's analysis is not formalized.
• The chapter says only that Nsyilxcen raises questions for the scalar account; nsyilxcen_not_scalar sharpens this to the account without further tampering with the modal's domain, such as [RMD08]'s restriction of a necessity modal.
• (63)'s three contexts are the rows (63a)–(63c), and (42)–(43)'s sentences are rows keyed by the force of their context.

References

• [Mat16]
• [Kra12b]
• [Mat13]
• [RMD08]
• [Pet10]
• [Dea11]
• [Men13]
• [Nau08]
• [VK13b]
• [Con02]

Modes of projection (Table 18.2)

inductive Matthewson2016.ProjectionMode : Type

[Kra12b]'s modes of projecting a conversational background: factual, over the worlds holding counterparts of some actual situation or body of evidence, and content, over the worlds compatible with the propositional content of some source of information.

• factual : ProjectionMode
• content : ProjectionMode

@[instance_reducible]

instance Matthewson2016.instDecidableEqProjectionMode : DecidableEq ProjectionMode

Equations

• Matthewson2016.instDecidableEqProjectionMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Matthewson2016.instReprProjectionMode : Repr ProjectionMode

Equations

• Matthewson2016.instReprProjectionMode = { reprPrec := Matthewson2016.instReprProjectionMode.repr }

def Matthewson2016.instReprProjectionMode.repr : ProjectionMode → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Matthewson2016.instFintypeProjectionMode : Fintype ProjectionMode

Equations

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

def Matthewson2016.ProjectionMode.Admits {W : Type u_1} : ProjectionMode → Modality.Background W → Prop

The modal bases a mode projects. The actual world holds the situation or evidence whose counterparts a factual base projects, so a factual base is realistic; the content of a source may be false, so a content base need not be.

Equations

• Matthewson2016.ProjectionMode.factual.Admits x✝ = x✝.IsRealistic
• Matthewson2016.ProjectionMode.content.Admits x✝ = True

def Matthewson2016.Deniable {W : Type u_1} (f : Modality.Background W) : Prop

A modal base allows must p, but not p when at some world p is necessary and false.

Equations

• Matthewson2016.Deniable f = ∃ (p : W → Prop) (w : W), Modality.simpleNecessity f p w ∧ ¬p w

theorem Matthewson2016.deniable_iff_not_isRealistic {W : Type u_1} {f : Modality.Background W} : Deniable f ↔ ¬f.IsRealistic

A base allows the denial of a necessity claim exactly when it is not realistic.

def Matthewson2016.ProjectionMode.Veridical (μ : ProjectionMode) (W : Type u_2) : Prop

A mode is veridical over a space of worlds when no base it projects there allows the denial of a necessity claim.

Equations

• μ.Veridical W = ∀ (f : Modality.Background W), μ.Admits f → ¬Matthewson2016.Deniable f

theorem Matthewson2016.ProjectionMode.veridical_iff {W : Type u_1} {μ : ProjectionMode} [Nonempty W] : μ.Veridical W ↔ μ = factual

Deniability diagnoses the content mode: over any worlds, a mode is veridical exactly when it is factual, a content base being free to hold what holds nowhere.

@[instance_reducible]

instance Matthewson2016.instDecidableVeridicalOfNonempty {W : Type u_1} {μ : ProjectionMode} [Nonempty W] : Decidable (μ.Veridical W)

Equations

• Matthewson2016.instDecidableVeridicalOfNonempty = decidable_of_iff (μ = Matthewson2016.ProjectionMode.factual) ⋯

theorem Matthewson2016.rumor : ProjectionMode.factual.Admits Kratzer2012.evidence ∧ ¬Deniable Kratzer2012.evidence ∧ Deniable Kratzer2012.content

(23)–(24): the rumor as evidence of things projects factually and rules out given the rumor, Roger must have been elected chief, but he actually wasn't; the rumor's content allows according to the rumor to be denied.

The three-way classification (Table 18.3)

inductive Matthewson2016.BackgroundClass : Type

The chapter's three classes of conversational backgrounds: factual backgrounds without an information source, the traditional circumstantial class, and factual and content backgrounds encoding one, the two epistemic subtypes.

• factualCircumstantial : BackgroundClass
• factualEvidential : BackgroundClass
• contentEvidential : BackgroundClass

@[instance_reducible]

instance Matthewson2016.instDecidableEqBackgroundClass : DecidableEq BackgroundClass

Equations

• Matthewson2016.instDecidableEqBackgroundClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Matthewson2016.instReprBackgroundClass : Repr BackgroundClass

Equations

• Matthewson2016.instReprBackgroundClass = { reprPrec := Matthewson2016.instReprBackgroundClass.repr }

def Matthewson2016.instReprBackgroundClass.repr : BackgroundClass → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Matthewson2016.instFintypeBackgroundClass : Fintype BackgroundClass

Equations

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

def Matthewson2016.BackgroundClass.projectionMode : BackgroundClass → ProjectionMode

The mode in which a class projects.

Equations

• Matthewson2016.BackgroundClass.factualCircumstantial.projectionMode = Matthewson2016.ProjectionMode.factual
• Matthewson2016.BackgroundClass.factualEvidential.projectionMode = Matthewson2016.ProjectionMode.factual
• Matthewson2016.BackgroundClass.contentEvidential.projectionMode = Matthewson2016.ProjectionMode.content

def Matthewson2016.BackgroundClass.traditionalFlavor : BackgroundClass → Modality.ModalFlavor

The traditional epistemic or circumstantial flavour a class refines.

Equations

• Matthewson2016.BackgroundClass.factualCircumstantial.traditionalFlavor = Modality.ModalFlavor.circumstantial
• Matthewson2016.BackgroundClass.factualEvidential.traditionalFlavor = Modality.ModalFlavor.epistemic
• Matthewson2016.BackgroundClass.contentEvidential.traditionalFlavor = Modality.ModalFlavor.epistemic

theorem Matthewson2016.table18_2 : (∀ (c : BackgroundClass), c.traditionalFlavor = Modality.ModalFlavor.circumstantial → c.projectionMode = ProjectionMode.factual) ∧ ∀ (μ : ProjectionMode), ∃ (c : BackgroundClass), c.traditionalFlavor = Modality.ModalFlavor.epistemic ∧ c.projectionMode = μ

Table 18.2: the traditional circumstantial class is factual, and the new classification splits the traditional epistemic class by mode.

theorem Matthewson2016.projectionMode_traditionalFlavor_injective : Function.Injective fun (c : BackgroundClass) => (c.projectionMode, c.traditionalFlavor)

The factual–content and circumstantial–evidential divisions determine the class.

def Matthewson2016.BackgroundClass.ofMode (μ : ProjectionMode) : Option Evidential.EvidenceType → BackgroundClass

The class of a modal from its mode and the information source it encodes, if any.

Equations

• One or more equations did not get rendered due to their size.
• Matthewson2016.BackgroundClass.ofMode μ none = Matthewson2016.BackgroundClass.factualCircumstantial

theorem Matthewson2016.BackgroundClass.traditionalFlavor_ofMode {μ : ProjectionMode} {s : Option Evidential.EvidenceType} : (ofMode μ s).traditionalFlavor = Modality.ModalFlavor.circumstantial ↔ s = none

The circumstantial–evidential division is whether an information source is encoded.

theorem Matthewson2016.BackgroundClass.projectionMode_ofMode {μ : ProjectionMode} {s : Option Evidential.EvidenceType} (h : s = none → μ = ProjectionMode.factual) : (ofMode μ s).projectionMode = μ

The factual–content division is the mode, a background without a source being factual.

Rows

def Matthewson2016.modalTable : List (String × Modality.ModalItem)

The modals the chapter's rows name, keyed by their forms.

Equations

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

theorem Matthewson2016.rows_resolve (e : Datum) : e ∈ Examples.all → (e.feature? "modal").isSome = true → (e.parse? "modal" modalTable).isSome = true

Every row naming a modal names one of the fragments'.

def Matthewson2016.statimcetsMode (m : Modality.ModalItem) : ProjectionMode

The mode in which a St'át'imcets modal projects: lákw7a from the content of its sensory evidence, the other evidentials and the circumstantial modals factually (Table 18.3).

Equations

• Matthewson2016.statimcetsMode m = if m = Statimcets.lakw7a then Matthewson2016.ProjectionMode.content else Matthewson2016.ProjectionMode.factual

def Matthewson2016.statimcetsClass (m : Modality.ModalItem) : BackgroundClass

The class of a St'át'imcets modal.

Equations

• Matthewson2016.statimcetsClass m = Matthewson2016.BackgroundClass.ofMode (Matthewson2016.statimcetsMode m) (Statimcets.source m)

theorem Matthewson2016.table18_3 : statimcetsClass Statimcets.ka = BackgroundClass.factualCircumstantial ∧ statimcetsClass Statimcets.kaCircumfix = BackgroundClass.factualCircumstantial ∧ statimcetsClass Statimcets.kaInfer = BackgroundClass.factualEvidential ∧ statimcetsClass Statimcets.ku7 = BackgroundClass.factualEvidential ∧ statimcetsClass Statimcets.lakw7a = BackgroundClass.contentEvidential

Table 18.3's St'át'imcets row.

theorem Matthewson2016.statimcets_full_split (c : BackgroundClass) : ∃ m ∈ Statimcets.modals, statimcetsClass m = c

St'át'imcets encodes the full three-way split.

theorem Matthewson2016.deniability_rows (W : Type u_2) [Nonempty W] (e : Datum) : e ∈ Examples.all → e.feature? "test" = some "deniability" → ∃ m ∈ e.parse? "modal" modalTable, e.judgment = Judgment.acceptable ↔ ¬(statimcetsMode m).Veridical W

(25)–(28): a modal survives but it was the wind exactly when its mode allows the denial of its prejacent, as the content lákw7a does and the factual k'a does not.

Gitksan: epistemic and circumstantial apart (Table 18.1)

theorem Matthewson2016.gitksan_absolute_split : Matthewson2013.TypeSelective Gitksan.modals

The split between epistemic and circumstantial readings is absolute in Gitksan: each modal selects one type, [Mat13]'s type selectivity.

Modal force: modals without duals (§18.3.2)

A modal without a dual comes in no necessity–possibility pair and is used in contexts supporting either claim: Gitksan ima('a) and g̱at, variable in force, and Nez Perce o'qa, a possibility modal usable in necessity contexts because no necessity modal competes with it to induce a scalar implicature ([Dea11]).

def Matthewson2016.HasDualIn (L : List Modality.ModalItem) (m : Modality.ModalItem) : Prop

A modal has a dual in an inventory when it is fixed for one classical force and another item of the inventory, sharing one of its flavours, is fixed for the dual force.

Equations

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

@[instance_reducible]

instance Matthewson2016.instDecidableHasDualIn (L : List Modality.ModalItem) (m : Modality.ModalItem) : Decidable (HasDualIn L m)

Equations

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

theorem Matthewson2016.not_hasDualIn_of_variesForce {L : List Modality.ModalItem} {m : Modality.ModalItem} (h : m.classical.VariesForce) : ¬HasDualIn L m

A modal varying in force has no dual.

theorem Matthewson2016.no_duals : ¬HasDualIn Gitksan.modals Gitksan.imaa ∧ ¬HasDualIn Gitksan.modals Gitksan.gat ∧ ¬HasDualIn NezPerce.modals NezPerce.oqa

Gitksan ima('a) and g̱at vary in force, and Nez Perce o'qa has no necessity counterpart, so none has a dual in its inventory.

def Matthewson2016.forceTable : List (String × Modality.ModalForce)

The force a reading names.

Equations

• Matthewson2016.forceTable = [("possibility", Modality.ModalForce.possibility), ("necessity", Modality.ModalForce.necessity)]

theorem Matthewson2016.imaa_rows (e : Datum) : e ∈ Examples.all → e.parse? "modal" modalTable = some Gitksan.imaa → ∀ r ∈ e.readings, ∃ fo ∈ List.lookup r.1 forceTable, r.2 = Judgment.acceptable ↔ fo ∈ Gitksan.imaa.forces

(37)–(38): ima('a) is read with each force it expresses, and with possibility where English must would be infelicitous.

def Matthewson2016.polarityTable : List (String × Polarity)

The polarity of a row's context.

Equations

• Matthewson2016.polarityTable = [("false", Polarity.positive), ("true", Polarity.negative)]

theorem Matthewson2016.oqa_rows (e : Datum) : e ∈ Examples.all → e.parse? "modal" modalTable = some NezPerce.oqa → ∀ π ∈ e.parse? "downwardEntailing" polarityTable, ∀ r ∈ e.readings, ∃ fo ∈ List.lookup r.1 forceTable, r.2 = Judgment.acceptable ↔ Deal2011.Usable π (Deal2011.lexicalForce NezPerce.oqa) (Deal2011.HasScalemate Deal2011.lexicalForce NezPerce.modals NezPerce.oqa) fo

(39)–(40): o'qa takes a possibility translation everywhere and a necessity translation only outside a downward-entailing context, as [Dea11]'s account of a possibility modal without a scale predicts.

theorem Matthewson2016.nsyilxcen_rows (e : Datum) : e ∈ Examples.all → ∀ m ∈ e.parse? "modal" modalTable, m ∈ Nsyilxcen.modals → ∀ fo ∈ e.parse? "force" forceTable, e.judgment = Judgment.acceptable ↔ fo ∈ m.forces

(42)–(43): Nsyilxcen mat is accepted in possibility and necessity contexts and cmay in possibility contexts only, as the fragment records.

theorem Matthewson2016.nsyilxcen_not_scalar : ¬∃ (lex : Modality.ModalItem → Modality.ModalForce), ∀ m ∈ Nsyilxcen.modals, ∀ (g : Modality.ModalForce), g.classical ∈ m.classical.forces ↔ Deal2011.Usable Polarity.positive (lex m) (Deal2011.HasScalemate lex Nsyilxcen.modals m) g

(42)–(43) against the scalar account: no lexical forces for mat and cmay let [Dea11]'s account predict their uses. A strict possibility cmay needs a necessity scalemate, and a necessity mat serves only for necessity in an upward-entailing context.

Modal–temporal interaction (§18.4.3)

theorem Matthewson2016.past_perspective_epistemics (e : Datum) : e ∈ Examples.all → e.feature? "perspective" = some "past" → e.judgment = Judgment.acceptable ∧ (e.feature? "flavor" = some "epistemic" ∨ ∃ m ∈ e.parse? "modal" modalTable, m.Epistemic)

(57)–(62): an epistemic modal takes a past temporal perspective in Blackfoot, Ktunaxa, St'át'imcets and Gitksan, every past-perspective row being an accepted epistemic.

theorem Matthewson2016.gitksan_orientation_rows (e : Datum) : e ∈ Examples.all → e.parse? "modal" modalTable = some Gitksan.imaa → ∀ s ∈ e.feature? "orientation", ∃ o ∈ Matthewson2013.orientationOf s, e.judgment = Judgment.acceptable ↔ (e.feature? "prospective" = some "true" ↔ o = Modality.TemporalOrientation.future)

(60)–(63): ima('a) takes every orientation, and dim is present exactly when it is future-oriented, as in [Mat13]'s paradigms.

theorem Matthewson2016.marking_mirror : (∀ (s : Condoravdi2002.Scope), s.orientation = Modality.TemporalOrientation.past ↔ s = Condoravdi2002.Scope.modalPerf) ∧ ∀ e ∈ Matthewson2013.Examples.all, ∀ o ∈ (e.feature? "orientation").bind Matthewson2013.orientationOf, e.judgment = Judgment.acceptable ↔ (e.feature? "prospective" = some "true" ↔ o = Modality.TemporalOrientation.future)

English marks past orientation, by the perfect under the modal among [Con02]'s scopings, and Gitksan future orientation, by dim in [Mat13]'s paradigms: the mirror image of §18.4.3.

Typology (§18.5)

def Matthewson2016.DistinguishesForce (L : List Modality.ModalItem) (D : Modality.ModalItem → Prop) : Prop

An inventory distinguishes force within a domain when two of its modals there express different sets of classical forces.

Equations

• Matthewson2016.DistinguishesForce L D = ∃ m ∈ L, ∃ m' ∈ L, D m ∧ D m' ∧ m.classical.forces ≠ m'.classical.forces

@[instance_reducible]

instance Matthewson2016.instDecidableDistinguishesForceOfDecidablePredModalItem (L : List Modality.ModalItem) (D : Modality.ModalItem → Prop) [DecidablePred D] : Decidable (DistinguishesForce L D)

Equations

• Matthewson2016.instDecidableDistinguishesForceOfDecidablePredModalItem L D = Matthewson2016.instDecidableDistinguishesForceOfDecidablePredModalItem._aux_1 L D

theorem Matthewson2016.force_only_circumstantial : (¬DistinguishesForce Gitksan.modals Modality.ModalItem.Epistemic ∧ DistinguishesForce Gitksan.modals Modality.ModalItem.Circumstantial) ∧ ¬DistinguishesForce Niuean.modals Modality.ModalItem.Epistemic ∧ DistinguishesForce Niuean.modals Modality.ModalItem.Circumstantial

The flavour–force correlation: Gitksan and Niuean distinguish force among their circumstantial modals and not among their epistemic ones.

theorem Matthewson2016.gitksan_duals : HasDualIn Gitksan.modals Gitksan.daakhlxw ∧ HasDualIn Gitksan.modals Gitksan.sgi ∧ ¬HasDualIn Gitksan.modals Gitksan.imaa ∧ ¬HasDualIn Gitksan.modals Gitksan.gat

Gitksan's circumstantial da'aḵhlxw and sgi are duals; its epistemic ima('a) and g̱at have none.

theorem Matthewson2016.niuean_duals : HasDualIn Niuean.modals Niuean.maeke ∧ HasDualIn Niuean.modals Niuean.lata ∧ ¬HasDualIn Niuean.modals Niuean.liga

Niuean's circumstantial maeke and lata are duals; its epistemic liga has none.

def Matthewson2016.strengthTable : List (String × Modality.ModalForce)

The strength a Niuean row records.

Equations

• Matthewson2016.strengthTable = [("weak", Modality.ModalForce.possibility), ("strong", Modality.ModalForce.necessity)]

def Matthewson2016.flavorTable : List (String × Modality.ModalFlavor)

The flavour a Niuean row records, (68)'s obligation reading being deontic.

Equations

• Matthewson2016.flavorTable = [("epistemic", Modality.ModalFlavor.epistemic), ("circumstantial", Modality.ModalFlavor.circumstantial), ("deontic", Modality.ModalFlavor.deontic)]

theorem Matthewson2016.niuean_rows : (∀ e ∈ Examples.all, e.feature? "section" = some "18.5" → (e.feature? "force").isSome = true → ∃ m ∈ e.parse? "modal" modalTable, ∃ fo ∈ e.parse? "force" strengthTable, ∃ fl ∈ e.parse? "flavor" flavorTable, (fo, fl) ∈ m.meaning) ∧ ∀ fo ∈ Niuean.liga.forces, ∃ e ∈ Examples.all, e.parse? "modal" modalTable = some Niuean.liga ∧ e.parse? "force" strengthTable = some fo

(64)–(68): each Niuean example expresses a force and flavour its modal has, and liga is attested with each of its forces.

def Matthewson2016.OneAxisWithin (L : List Modality.ModalItem) (D : Modality.ModalItem → Prop) : Prop

An inventory varies along one axis within a domain when its modals there do not vary in force and in flavour both.

Equations

• Matthewson2016.OneAxisWithin L D = ¬((∃ m ∈ L, D m ∧ m.classical.VariesForce) ∧ ∃ m ∈ L, D m ∧ m.VariesFlavor)

@[instance_reducible]

instance Matthewson2016.instDecidableOneAxisWithinOfDecidablePredModalItem (L : List Modality.ModalItem) (D : Modality.ModalItem → Prop) [DecidablePred D] : Decidable (OneAxisWithin L D)

Equations

• Matthewson2016.instDecidableOneAxisWithinOfDecidablePredModalItem L D = { decide := !decide ((∃ m ∈ L, D m ∧ m.classical.VariesForce) ∧ ∃ m ∈ L, D m ∧ m.VariesFlavor), reflects_decide := ⋯ }

theorem Matthewson2016.OneAxisWithin.singleAxis {L : List Modality.ModalItem} {D : Modality.ModalItem → Prop} (h : OneAxisWithin L D) {m : Modality.ModalItem} (hm : m ∈ L) (hD : D m) : Modality.SingleAxis m.classical.meaning

A modal of a one-axis domain varies on one axis.

def Matthewson2016.VanderKlok (L : List Modality.ModalItem) : Prop

[VK13b]'s refinement of the universal: within each domain, epistemic and non-epistemic, an inventory varies along one axis only.

Equations

• Matthewson2016.VanderKlok L = (Matthewson2016.OneAxisWithin L Modality.ModalItem.Epistemic ∧ Matthewson2016.OneAxisWithin L fun (x : Modality.ModalItem) => ¬x.Epistemic)

@[instance_reducible]

instance Matthewson2016.instDecidableVanderKlok (L : List Modality.ModalItem) : Decidable (VanderKlok L)

Equations

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

theorem Matthewson2016.VanderKlok.singleAxis {L : List Modality.ModalItem} (h : VanderKlok L) {m : Modality.ModalItem} (hm : m ∈ L) : Modality.SingleAxis m.classical.meaning

The refinement entails the universal, each modal lying in one of the two domains.

theorem Matthewson2016.gitksan_vanderKlok : VanderKlok Gitksan.modals

Gitksan satisfies the refinement, its epistemic modals varying in force and its circumstantial modals in flavour.

theorem Matthewson2016.gitksan_nauze (m : Modality.ModalItem) : m ∈ Gitksan.modals → Modality.SingleAxis m.classical.meaning

[Nau08]'s universal holds of Gitksan: every modal varies on one axis, between necessity and possibility or among flavours.

def Matthewson2016.hypotheticalRootSystem : List Modality.ModalItem

Table 18.4's hypothetical root system: a deontic modal x of either force, a necessity modal y over two flavours, and possibility modals w and z for one flavour each.

Equations

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

theorem Matthewson2016.hypotheticalRootSystem_singleAxis_not_vanderKlok : (∀ m ∈ hypotheticalRootSystem, Modality.SingleAxis m.classical.meaning) ∧ ¬VanderKlok hypotheticalRootSystem

The system satisfies the universal and violates the refinement, x varying in force and y in flavour within the root domain, so the refinement is strictly stronger.