Matthewson (2013): Gitksan Modals

This file formalizes the description of the Gitksan modal system in [Mat13]. Gitksan is a mixed system (Fig. 1): every modal is specified for modality type, epistemic or circumstantial, and modal strength is encoded among the circumstantial modals, da'aḵhlxw and anooḵ for possibility against sgi for (weak) necessity, but not among the epistemic clitics ima('a) and g̱at, which are compatible with necessity and possibility contexts alike ([Pet10]). With the paper's lexical forces, existential for all but sgi, [Dea11]'s account of modals without scales predicts every modal's uses: the epistemics share a force and so form no scale, and are used for both, while sgi is the scalemate of da'aḵhlxw and anooḵ, and each circumstantial modal is used for its own force. The system fills the empty diagonal of the classification of modal systems by selectivity for type and for strength (Fig. 2), whose other cells English, St'át'imcets and Javanese occupy in the fragments.

Each modal's force and flavours predict its judgments in the paper's contexts, with one exception: sgi is rejected in the sneeze case, pure circumstantial strong necessity, though volunteered for we must all die, of the same force and flavour. No set of force-flavour pairs predicts the gap, so it is not one of modal strength, and the paper suggests sgi needs a non-empty ordering source.

Gitksan modals are not inherently future-oriented, against the English analysis of [Con02]: the prospective dim is present exactly when the prejacent is future-oriented, and it is obligatory with the circumstantial modals because they are future-oriented. Every cell of Fig. 4, perspective by orientation, is attested. The circumstantial possibility modal has no actuality entailment, its obligatory dim keeping it out of the perfective configuration of [Hac06].

Implementation notes

• The paper is agnostic between [Pet10]'s analysis of ima('a) as a possibility modal strengthened by an ordering source and a possibility modal without a scale, as [Dea11] analyses Nez Perce o'qa, the negation diagnostic (30) not separating them, and adopts what the two share, an existential quantifier over worlds. The prediction of the modals' uses follows [Dea11]'s mechanism, which the paper raises for the circumstantial modals (§5.1); forces are compared on Fig. 1's two columns, weak necessity counting as necessity.
• The rows record the paper's flavour labels; its pure circumstantial and teleological readings are the library's circumstantial flavour. A row's force is recorded only where the paper labels the context's strength.
• The primed rows are the dim-less variants that the paper's #(dim) marks as infelicitous.
• Fig. 2's Javanese cell is checked on the Paciran Javanese inventory of [VK13a]. Fig. 3 summarizes an earlier description by Vander Klok, whose possibility modals ento and mungkin are not in that inventory.

References

• [Mat13]
• [Pet10]
• [Dea11]
• [Con02]
• [Hac06]
• [RMD08]
• [VK13a]

The modal system (Fig. 1)

def Matthewson2013.lexicalForce (m : Modality.ModalItem) : Modality.ModalForce

lexicalForce m is the force the paper assigns to m. ima('a) and g̱at introduce an existential quantifier over worlds (§3.1–3.2), da'aḵhlxw and anooḵ are possibility modals, and sgi is a (weak) necessity modal (§4).

Equations

• Matthewson2013.lexicalForce m = if m = Gitksan.sgi then Modality.ModalForce.necessity else Modality.ModalForce.possibility

theorem Matthewson2013.forces_usable (m : Modality.ModalItem) : m ∈ Gitksan.modals → ∀ (g : Modality.ModalForce), g.classical ∈ m.classical.forces ↔ Deal2011.Usable Polarity.positive (lexicalForce m) (Deal2011.HasScalemate lexicalForce Gitksan.modals m) g

The lexical forces derive Fig. 1. In an upward-entailing context each modal serves, on [Dea11]'s account, for exactly the forces it is used with. The epistemics have no scalemate and serve for both; sgi shares its flavours with da'aḵhlxw and anooḵ, so each of the three serves for its own.

theorem Matthewson2013.hasScalemate_iff (m : Modality.ModalItem) : m ∈ Gitksan.modals → (Deal2011.HasScalemate lexicalForce Gitksan.modals m ↔ m.Circumstantial)

The epistemic clitics are modals without scales, and the circumstantial modals all belong to one.

Rows

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

modalTable keys the fragment's modals by their forms.

Equations

• Matthewson2013.modalTable = List.map (fun (m : Modality.ModalItem) => (m.form, m)) Gitksan.modals

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

forceTable maps a row's force label to the force its context supports.

Equations

• Matthewson2013.forceTable = [("possibility", Modality.ModalForce.possibility), ("weak necessity", Modality.ModalForce.weakNecessity), ("necessity", Modality.ModalForce.necessity)]

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

flavorTable maps a row's flavour label to a flavour, reading the pure circumstantial and teleological labels as circumstantial.

Equations

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

theorem Matthewson2013.rows_resolve (e : Datum) : e ∈ Examples.all → ∀ s ∈ e.feature? "modal", s ≠ "dim" → (e.parse? "modal" modalTable).isSome = true

Every row naming a modal other than the plain future names one of the fragment's.

Force and flavour (§3, §4)

theorem Matthewson2013.rows_meaning (e : Datum) : e ∈ Examples.all → e.feature? "test" ≠ some "sneeze" → ∀ m ∈ e.parse? "modal" modalTable, ∀ fo ∈ e.parse? "force" forceTable, ∀ fl ∈ e.parse? "flavor" flavorTable, e.judgment = Judgment.acceptable ↔ (fo, fl) ∈ m.meaning

Outside the sneeze case, a modal is accepted in a context exactly when it expresses the context's force and flavour. The possibility modals are rejected in necessity contexts, (66) and (80), and anooḵ in a pure circumstantial one, (79).

theorem Matthewson2013.sgi_attested : (∀ fo ∈ Gitksan.sgi.forces, ∃ e ∈ Examples.all, e.parse? "modal" modalTable = some Gitksan.sgi ∧ e.parse? "force" forceTable = some fo ∧ e.judgment = Judgment.acceptable) ∧ ∀ fl ∈ Gitksan.sgi.flavors, ∃ e ∈ Examples.all, e.parse? "modal" modalTable = some Gitksan.sgi ∧ e.parse? "flavor" flavorTable = some fl ∧ e.judgment = Judgment.acceptable

sgi is volunteered in strong necessity contexts, (89), (92) and (100), and accepted in a weak one, (90), with deontic, circumstantial and bouletic readings, so each force and flavour it expresses is attested.

theorem Matthewson2013.sneeze_rows (e : Datum) : e ∈ Examples.all → e.feature? "test" = some "sneeze" → (e.judgment = Judgment.acceptable ↔ e.feature? "modal" ≠ some "sgi")

The sneeze case of (95)–(96), pure circumstantial strong necessity, takes the plain future and not sgi.

theorem Matthewson2013.sneeze_gap : ¬∃ (M : Finset Modality.ForceFlavor), ∀ e ∈ Examples.all, e.parse? "modal" modalTable = some Gitksan.sgi → ∀ fo ∈ e.parse? "force" forceTable, ∀ fl ∈ e.parse? "flavor" flavorTable, e.judgment = Judgment.acceptable ↔ (fo, fl) ∈ M

In (96) and (100), sgi is rejected in the sneeze case and volunteered for we must all die, both pure circumstantial strong necessity, so no set of force-flavour pairs predicts its judgments, and the sneeze gap is not one of modal strength.

Modal systems (Fig. 2)

def Matthewson2013.TypeSelective (L : List Modality.ModalItem) : Prop

An inventory selects modality type when each of its modals is epistemic or circumstantial.

Equations

• Matthewson2013.TypeSelective L = ∀ m ∈ L, m.Epistemic ∨ m.Circumstantial

def Matthewson2013.StrengthSelective (L : List Modality.ModalItem) : Prop

An inventory selects modal strength when none of its modals varies between necessity and possibility, weak necessity counting as necessity.

Equations

• Matthewson2013.StrengthSelective L = ∀ m ∈ L, ¬m.classical.VariesForce

@[instance_reducible]

instance Matthewson2013.instDecidableTypeSelective (L : List Modality.ModalItem) : Decidable (TypeSelective L)

Equations

• Matthewson2013.instDecidableTypeSelective L = Matthewson2013.instDecidableTypeSelective._aux_1 L

@[instance_reducible]

instance Matthewson2013.instDecidableStrengthSelective (L : List Modality.ModalItem) : Decidable (StrengthSelective L)

Equations

• Matthewson2013.instDecidableStrengthSelective L = Matthewson2013.instDecidableStrengthSelective._aux_1 L

def Matthewson2013.Mixed (L : List Modality.ModalItem) : Prop

A mixed system selects type throughout and strength among its circumstantial modals only.

Equations

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

@[instance_reducible]

instance Matthewson2013.instDecidableMixed (L : List Modality.ModalItem) : Decidable (Mixed L)

Equations

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

theorem Matthewson2013.gitksan_mixed : Mixed Gitksan.modals

theorem Matthewson2013.fig2 : (StrengthSelective (List.map Auxiliary.toModalItem English.Auxiliaries.modals) ∧ ¬TypeSelective (List.map Auxiliary.toModalItem English.Auxiliaries.modals)) ∧ (TypeSelective Statimcets.modals ∧ ¬StrengthSelective Statimcets.modals) ∧ TypeSelective Javanese.Paciran.modals ∧ StrengthSelective Javanese.Paciran.modals

The fragments reproduce Fig. 2. English selects strength and not type, St'át'imcets type and not strength, and Javanese both (Fig. 3), a cell that the classification of [RMD08] left open.

Modal–temporal interaction (§3.3, §4, §5.3, Fig. 4)

def Matthewson2013.orientationOf : String → Option Modality.TemporalOrientation

orientationOf reads the orientation a row records.

Equations

• Matthewson2013.orientationOf "past" = some Modality.TemporalOrientation.past
• Matthewson2013.orientationOf "present" = some Modality.TemporalOrientation.present
• Matthewson2013.orientationOf "future" = some Modality.TemporalOrientation.future
• Matthewson2013.orientationOf x✝ = none

def Matthewson2013.perspectiveOf : String → Option Modality.TemporalPerspective

perspectiveOf reads the perspective a row records.

Equations

• Matthewson2013.perspectiveOf "past" = some Modality.TemporalPerspective.past
• Matthewson2013.perspectiveOf "present" = some Modality.TemporalPerspective.present
• Matthewson2013.perspectiveOf x✝ = none

theorem Matthewson2013.dim_rows (e : Datum) : e ∈ Examples.all → ∀ o ∈ (e.feature? "orientation").bind orientationOf, e.judgment = Judgment.acceptable ↔ (e.feature? "prospective" = some "true" ↔ o = Modality.TemporalOrientation.future)

In the paradigms (38)–(48), (53), (56), (73) and (83), the prospective aspect dim is present exactly when the prejacent is future-oriented, with epistemic and circumstantial modals alike.

theorem Matthewson2013.circumstantial_future (e : Datum) : e ∈ Examples.all → ∀ m ∈ e.parse? "modal" modalTable, m.Circumstantial → ∀ o ∈ (e.feature? "orientation").bind orientationOf, o = Modality.TemporalOrientation.future

The circumstantial modals are future-oriented (§4).

theorem Matthewson2013.dim_circumstantial (e : Datum) : e ∈ Examples.all → ∀ m ∈ e.parse? "modal" modalTable, m.Circumstantial → ∀ o ∈ (e.feature? "orientation").bind orientationOf, e.judgment = Judgment.acceptable ↔ e.feature? "prospective" = some "true"

dim is obligatory with the circumstantial modals, as their future orientation needs it.

theorem Matthewson2013.fig4 (p : Modality.TemporalPerspective) (o : Modality.TemporalOrientation) : ∃ e ∈ Examples.all, e.parse? "modal" modalTable = some Gitksan.imaa ∧ (e.feature? "perspective").bind perspectiveOf = some p ∧ (e.feature? "orientation").bind orientationOf = some o ∧ e.judgment = Judgment.acceptable

ima('a) is attested at every temporal perspective and orientation (Fig. 4).

theorem Matthewson2013.unmarked_orientation : Condoravdi2002.Scope.modal.orientation = Modality.TemporalOrientation.future ∧ ∀ e ∈ Examples.all, e.feature? "prospective" = some "false" → e.judgment = Judgment.acceptable → ∀ o ∈ (e.feature? "orientation").bind orientationOf, o ≠ Modality.TemporalOrientation.future

An unmarked English possibility modal is future-oriented on [Con02]'s analysis, as in (35), while no accepted Gitksan modal sentence without dim is, as in (39).

theorem Matthewson2013.no_actuality_entailment (e : Datum) : e ∈ Examples.all → e.feature? "actualityEntailment" = some "false" → e.parse? "modal" modalTable = some Gitksan.daakhlxw ∧ e.feature? "prospective" = some "true" ∧ e.judgment = Judgment.acceptable

da'aḵhlxw with its dim has no actuality entailment in (62), the ability holding while the event fails.