Deal (2011): Modals without scales

This file formalizes [Dea11]'s account of the Nez Perce modal o'qa, used where English uses a possibility modal and where it uses a necessity modal in upward-entailing contexts, but only where it uses a possibility modal elsewhere. O'qa is a possibility modal without a Horn scale: two modals form a scale only when they quantify over the same domain, sharing a type of modality, and no stronger Nez Perce modal shares o'qa's (§2). A possibility claim without a scalar implicature holds whenever there are accessible worlds of the prejacent, even when all accessible worlds are, so in an upward-entailing context o'qa serves for both forces (§1). Under negation the necessity claim is the weaker one, and o'qa serves only where a possibility modal of English does (§3).

The claims are [Kra81b]'s simple possibility and necessity, and negation acts on them by complement, the negative Polarity. A modal is appropriate where its claim holds and, if it has a scalemate, the scalemate's claim fails when it is the stronger one there (Appropriate). The contexts a modal serves for are then fixed by whether it has a scalemate and which claim is stronger (servesFor_iff), and Table 1 follows (flexible_iff): a modal with a scale is inflexible, a scale-free possibility modal is flexible only in upward-entailing contexts, and a scale-free necessity modal only in downward-entailing ones.

Implementation notes

• Forces are compared on the classical scale, weak necessity counting as necessity; the claims are simple possibility and necessity over a consistent modal base, with no ordering source.
• Negation stands in for the downward-entailing contexts of §3, the restrictions of universals and conditional antecedents, whose rows the environment feature marks; the paper treats conditional antecedents as not upward-entailing, leaving their monotonicity open (fn. 12).
• The rows are o'qa's judgments by the force of the English modal of the context or translation. (11) and (12), where speakers find o'qa too weak a translation of a necessity claim, bear on the preference for possibility translations, which the paper attributes to o'qa's being a possibility modal; they are not rows.

References

• [Dea11]
• [Kra81b]

Claims

def Deal2011.claim {W : Type u_1} (f : Modality.Background W) (p : W → Prop) : Modality.ModalForce → Set W

The claim a modal of force fo makes about p over the base f: simple possibility, or simple necessity for the universal forces.

Equations

• Deal2011.claim f p Modality.ModalForce.possibility = {w : W | Modality.simplePossibility f p w}
• Deal2011.claim f p Modality.ModalForce.weakNecessity = {w : W | Modality.simpleNecessity f p w}
• Deal2011.claim f p Modality.ModalForce.necessity = {w : W | Modality.simpleNecessity f p w}

def Deal2011.StrongerIn : Polarity → Modality.ModalForce → Modality.ModalForce → Prop

In a context of polarity π, the claim of force g is stronger than that of fo: necessity is the stronger claim in an upward-entailing context, possibility under negation.

Equations

• Deal2011.StrongerIn Polarity.positive x✝¹ x✝ = (x✝.classical < x✝¹.classical)
• Deal2011.StrongerIn Polarity.negative x✝¹ x✝ = (x✝¹.classical < x✝.classical)

@[instance_reducible]

instance Deal2011.instDecidableStrongerIn (π : Polarity) (g fo : Modality.ModalForce) : Decidable (StrongerIn π g fo)

Equations

• Deal2011.instDecidableStrongerIn Polarity.positive x✝¹ x✝ = { decide := x✝.classical.rank.succ.ble x✝¹.classical.rank, reflects_decide := ⋯ }
• Deal2011.instDecidableStrongerIn Polarity.negative x✝¹ x✝ = { decide := x✝¹.classical.rank.succ.ble x✝.classical.rank, reflects_decide := ⋯ }

theorem Deal2011.smul_claim_subset {W : Type u_1} {f : Modality.Background W} {p : W → Prop} (hf : ModalLogic.IsSerial f.accessible) {π : Polarity} {g fo : Modality.ModalForce} (h : StrongerIn π g fo) : π • claim f p g ⊆ π • claim f p fo

Over a consistent base, a stronger claim entails a weaker one.

def Deal2011.Appropriate {W : Type u_1} (f : Modality.Background W) (p : W → Prop) (π : Polarity) (fo : Modality.ModalForce) (s : Prop) : Set W

A modal of force fo, with a scalemate when s, is appropriate in a context of polarity π where its claim holds and, if it has a scalemate whose claim is the stronger there, that claim fails: the scalar implicature.

Equations

• Deal2011.Appropriate f p π fo s = π • Deal2011.claim f p fo ∩ {w : W | s → Deal2011.StrongerIn π fo.dual fo → w ∉ π • Deal2011.claim f p fo.dual}

Flexibility (§1, §3, Table 1)

def Deal2011.ServesFor (π : Polarity) (fo : Modality.ModalForce) (s : Prop) (g : Modality.ModalForce) : Prop

A modal of force fo, with a scalemate when s, serves in a context of polarity π for the force g when, in every consistent model, it is appropriate wherever a modal of force g with a scale, as in English, is.

Equations

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

def Deal2011.Usable (π : Polarity) (fo : Modality.ModalForce) (s : Prop) (g : Modality.ModalForce) : Prop

A modal serves for its own force, and without a scalemate for any force whose claim is stronger than its own.

Equations

• Deal2011.Usable π fo s g = (fo.classical = g.classical ∨ ¬s ∧ Deal2011.StrongerIn π g fo)

@[instance_reducible]

instance Deal2011.instDecidableUsable (π : Polarity) (fo : Modality.ModalForce) (s : Prop) [Decidable s] (g : Modality.ModalForce) : Decidable (Usable π fo s g)

Equations

• Deal2011.instDecidableUsable π fo s g = { decide := decide (fo.classical = g.classical) || decide (¬s ∧ Deal2011.StrongerIn π g fo), reflects_decide := ⋯ }

theorem Deal2011.appropriate_classical {W : Type u_1} {f : Modality.Background W} {p : W → Prop} (π : Polarity) (fo : Modality.ModalForce) (s : Prop) : Appropriate f p π fo.classical s = Appropriate f p π fo s

theorem Deal2011.servesFor_iff {π : Polarity} {fo g : Modality.ModalForce} {s : Prop} : ServesFor π fo s g ↔ Usable π fo s g

The forces a modal serves for are its own and, if it has no scalemate, those whose claim is stronger than its own.

theorem Deal2011.flexible_iff {π : Polarity} {fo : Modality.ModalForce} {s : Prop} : (∀ (g : Modality.ModalForce), ServesFor π fo s g) ↔ ¬s ∧ StrongerIn π fo.dual fo

Table 1: a modal is flexible in a context of polarity π, serving for every force, exactly when it has no scalemate and its own claim is the weaker there. A modal with a scale is never flexible, a scale-free possibility modal is flexible in upward-entailing contexts only, and a scale-free necessity modal in downward-entailing ones only.

Scales (§2)

def Deal2011.Scalemates (lex : Modality.ModalItem → Modality.ModalForce) (m m' : Modality.ModalItem) : Prop

Two modals are scalemates, forming a Horn scale, when their lexical forces differ and they share a flavour: only quantifiers over the same domain form a scale (§2.1).

Equations

• Deal2011.Scalemates lex m m' = ((lex m).classical ≠ (lex m').classical ∧ ∃ fl ∈ m.flavors, fl ∈ m'.flavors)

def Deal2011.HasScalemate (lex : Modality.ModalItem → Modality.ModalForce) (L : List Modality.ModalItem) (m : Modality.ModalItem) : Prop

A modal has a scalemate in an inventory.

Equations

• Deal2011.HasScalemate lex L m = ∃ m' ∈ L, Deal2011.Scalemates lex m m'

@[instance_reducible]

instance Deal2011.instDecidableScalemates (lex : Modality.ModalItem → Modality.ModalForce) (m m' : Modality.ModalItem) : Decidable (Scalemates lex m m')

Equations

• Deal2011.instDecidableScalemates lex m m' = { decide := decide ((lex m).classical ≠ (lex m').classical) && decide (∃ x ∈ m.flavors, x ∈ m'.flavors), reflects_decide := ⋯ }

@[instance_reducible]

instance Deal2011.instDecidableHasScalemate (lex : Modality.ModalItem → Modality.ModalForce) (L : List Modality.ModalItem) (m : Modality.ModalItem) : Decidable (HasScalemate lex L m)

Equations

• Deal2011.instDecidableHasScalemate lex L m = Deal2011.instDecidableHasScalemate._aux_1 lex L m

def Deal2011.ServesIn (lex : Modality.ModalItem → Modality.ModalForce) (L : List Modality.ModalItem) (π : Polarity) (m : Modality.ModalItem) (g : Modality.ModalForce) : Prop

A modal of the inventory L serves in a context of polarity π for the force g, given its lexical force and whether it has a scalemate in L.

Equations

• Deal2011.ServesIn lex L π m g = Deal2011.ServesFor π (lex m) (Deal2011.HasScalemate lex L m) g

def Deal2011.lexicalForce : Modality.ModalItem → Modality.ModalForce

The Nez Perce modals are possibility modals (§2): o'qa, the participial construction, which appears to express possibility, 'ax̂, which speakers judge equivalent to o'qa, and the epistemic particles 'maybe'.

Equations

• Deal2011.lexicalForce x✝ = Modality.ModalForce.possibility

theorem Deal2011.oqa_scaleFree : ¬HasScalemate lexicalForce NezPerce.modals NezPerce.oqa

O'qa is a quantifier without a scale (§2.6).

theorem Deal2011.oqa_flexible : (∀ (g : Modality.ModalForce), ServesIn lexicalForce NezPerce.modals Polarity.positive NezPerce.oqa g) ∧ ¬∀ (g : Modality.ModalForce), ServesIn lexicalForce NezPerce.modals Polarity.negative NezPerce.oqa g

O'qa is flexible in an upward-entailing context and not under negation.

theorem Deal2011.oqa_forces (g : Modality.ModalForce) : g.classical ∈ NezPerce.oqa.classical.forces ↔ Usable Polarity.positive (lexicalForce NezPerce.oqa) (HasScalemate lexicalForce NezPerce.modals NezPerce.oqa) g

The fragment records o'qa's upward-entailing uses: the forces it serves for.

Rows

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

The modals the rows name, keyed by their forms.

Equations

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

def Deal2011.polarityTable : List (String × Polarity)

The polarity of a row's environment: negation, the restriction of a universal and a conditional antecedent are not upward-entailing.

Equations

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

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

The force of the English modal of a row's context or translation.

Equations

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

theorem Deal2011.rows_resolve (e : Datum) : e ∈ Examples.all → (e.parse? "modal" modalTable).isSome = true ∧ (e.parse? "environment" polarityTable).isSome = true

Every row resolves its modal and environment.

theorem Deal2011.rows (e : Datum) : e ∈ Examples.all → ∀ m ∈ e.parse? "modal" modalTable, ∀ π ∈ e.parse? "environment" polarityTable, (∀ g ∈ e.parse? "force" forceTable, e.judgment = Judgment.acceptable ↔ Usable π (lexicalForce m) (HasScalemate lexicalForce NezPerce.modals m) g) ∧ ∀ r ∈ e.readings, ∃ g ∈ List.lookup r.1 forceTable, r.2 = Judgment.acceptable ↔ Usable π (lexicalForce m) (HasScalemate lexicalForce NezPerce.modals m) g

§1 and §3: o'qa is accepted in a context, or on a translation, exactly when it serves for the force of the English modal there, both forces in upward-entailing environments and possibility alone elsewhere.