Alternative-sensitive particles in Ngamo

Formalises [grubic-2015] Ch. 6–7: the Ngamo particles yak('i) 'only', ke('e) 'also', and har('i) 'even' in a Beaver & Clark-style QUD account. yak(p) presupposes at least p and asserts at most p over entailment-ranked alternatives (the Coppock & Beaver decomposition); ke(p) presupposes a given alternative about a different topic situation; har(p) presupposes a contextual implication of p ranked high on a salient scale (kept as prose).

yak_eq_prejacent_inter_onlyVia reconciles the scalar and identity formulations of exclusivity: over the conjunction-closure of the atomic alternatives, yak's total content (presupposition plus assertion) coincides with the prejacent exhaustified by the strong-theory onlyVia over the atoms — the Kiss-style identificational meaning derived from the scalar decomposition.

Distribution (her (10)–(12)): yak cannot associate with preverbal subjects but is fine in any focus construction; ke/har associate with preverbal subjects but are marginal with =i/ye-marked focus under parallel backgrounds — data recorded in distribution.

The Coppock & Beaver decomposition (Ch. 7)

def Grubic2015.atLeast {W : Type u_1} (C : Set (Set W)) (p : Set W) : Set W

At least p: some alternative at least as strong as the prejacent holds — yak's presupposition.

Equations

• Grubic2015.atLeast C p = {w : W | ∃ q ∈ C, q ⊆ p ∧ w ∈ q}

def Grubic2015.atMost {W : Type u_1} (C : Set (Set W)) (p : Set W) : Set W

At most p: no alternative strictly stronger than the prejacent holds — yak's assertion.

Equations

• Grubic2015.atMost C p = {w : W | ∀ q ∈ C, w ∈ q → ¬q ⊂ p}

def Grubic2015.yak {W : Type u_1} (C : Set (Set W)) (p : Set W) : Pragmatics.Expressives.TwoDimProp W

yak('i) 'only': presupposes at least p, asserts at most p (her Ch. 7, following Coppock & Beaver's only).

Equations

• Grubic2015.yak C p = Pragmatics.Expressives.TwoDimProp.withCI (fun (x : W) => x ∈ Grubic2015.atMost C p) fun (x : W) => x ∈ Grubic2015.atLeast C p

def Grubic2015.ke {W : Type u_1} (given : Set (Set W)) (p : Set W) : Pragmatics.Expressives.TwoDimProp W

ke('e) 'also': presupposes that a distinct alternative is given (her Ch. 7; the different-topic-situation refinement is prose).

Equations

• Grubic2015.ke given p = Pragmatics.Expressives.TwoDimProp.withCI (fun (x : W) => x ∈ p) fun (w : W) => ∃ q ∈ given, q ≠ p ∧ w ∈ q

def Grubic2015.total {W : Type u_1} (m : Pragmatics.Expressives.TwoDimProp W) : Set W

The total content of a two-dimensional meaning: at-issue plus presupposed.

Equations

• Grubic2015.total m = {w : W | m.atIssue w ∧ m.ci w}

Reconciling the scalar and identity formulations

On the building scenario (her (10)–(11)): worlds track which of the house and the granary Kule built.

structure Grubic2015.BuildWorld : Type

Who-built-what worlds.

• house : Bool
• granary : Bool

def Grubic2015.instDecidableEqBuildWorld.decEq (x✝ x✝¹ : BuildWorld) : Decidable (x✝ = x✝¹)

Equations

• Grubic2015.instDecidableEqBuildWorld.decEq { house := a, granary := a_1 } { house := b, granary := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance Grubic2015.instDecidableEqBuildWorld : DecidableEq BuildWorld

Equations

• Grubic2015.instDecidableEqBuildWorld = Grubic2015.instDecidableEqBuildWorld.decEq

def Grubic2015.instReprBuildWorld.repr : BuildWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Grubic2015.instReprBuildWorld : Repr BuildWorld

Equations

• Grubic2015.instReprBuildWorld = { reprPrec := Grubic2015.instReprBuildWorld.repr }

def Grubic2015.builtHouse : Set BuildWorld

Equations

• Grubic2015.builtHouse = {w : Grubic2015.BuildWorld | w.house = true}

def Grubic2015.builtGranary : Set BuildWorld

Equations

• Grubic2015.builtGranary = {w : Grubic2015.BuildWorld | w.granary = true}

def Grubic2015.builtBoth : Set BuildWorld

Equations

• Grubic2015.builtBoth = Grubic2015.builtHouse ∩ Grubic2015.builtGranary

def Grubic2015.atoms : Set (Set BuildWorld)

The atomic alternatives.

Equations

• Grubic2015.atoms = {Grubic2015.builtHouse, Grubic2015.builtGranary}

def Grubic2015.answers : Set (Set BuildWorld)

The QUD's answer space: the atoms and their conjunction.

Equations

• Grubic2015.answers = {Grubic2015.builtHouse, Grubic2015.builtGranary, Grubic2015.builtBoth}

theorem Grubic2015.yak_eq_prejacent_inter_onlyVia : total (yak answers builtHouse) = builtHouse ∩ Semantics.Focus.onlyVia atoms builtHouse

The scalar and identity formulations coincide: yak's total content over the conjunction-closed answer space equals the prejacent exhaustified by onlyVia over the atoms — the Kiss-style identificational meaning ('built the house and nothing else') derived from the at-least/at-most decomposition.

theorem Grubic2015.ke_needs_distinct_antecedent (w : BuildWorld) : ¬(ke {builtHouse} builtHouse).ci w

ke's additive presupposition needs a distinct given alternative: with only the prejacent given, the presupposition fails everywhere — the anaphoricity behind her (12) parallel-background facts.

Distribution (her (10)–(12))

inductive Grubic2015.Particle : Type

The particles.

• yak : Particle
• ke : Particle
• har : Particle

@[implicit_reducible]

instance Grubic2015.instDecidableEqParticle : DecidableEq Particle

Equations

• Grubic2015.instDecidableEqParticle x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Grubic2015.instReprParticle : Repr Particle

Equations

• Grubic2015.instReprParticle = { reprPrec := Grubic2015.instReprParticle.repr }

def Grubic2015.instReprParticle.repr : Particle → ℕ → Std.Format

Equations

• Grubic2015.instReprParticle.repr Grubic2015.Particle.yak prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Grubic2015.Particle.yak")).group prec✝
• Grubic2015.instReprParticle.repr Grubic2015.Particle.ke prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Grubic2015.Particle.ke")).group prec✝
• Grubic2015.instReprParticle.repr Grubic2015.Particle.har prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Grubic2015.Particle.har")).group prec✝

inductive Grubic2015.Host : Type

The association configurations tested.

• preverbalSubject : Host
• bmMarkedFocus : Host
• plainFocus : Host

@[implicit_reducible]

instance Grubic2015.instDecidableEqHost : DecidableEq Host

Equations

• Grubic2015.instDecidableEqHost x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Grubic2015.instReprHost : Repr Host

Equations

• Grubic2015.instReprHost = { reprPrec := Grubic2015.instReprHost.repr }

def Grubic2015.instReprHost.repr : Host → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Grubic2015.instReprHost.repr Grubic2015.Host.plainFocus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Grubic2015.Host.plainFocus")).group prec✝

def Grubic2015.acceptable : Particle → Host → Bool

Her (10)–(11) acceptability table: yak cannot associate with preverbal subjects; ke/har are marginal with =i/ye-marked focus (under parallel backgrounds — the (12) exception is prose).

Equations

• Grubic2015.acceptable Grubic2015.Particle.yak Grubic2015.Host.preverbalSubject = false
• Grubic2015.acceptable Grubic2015.Particle.yak x✝ = true
• Grubic2015.acceptable x✝ Grubic2015.Host.bmMarkedFocus = false
• Grubic2015.acceptable x✝¹ x✝ = true

theorem Grubic2015.association_crosscuts : acceptable Particle.yak Host.bmMarkedFocus ≠ acceptable Particle.ke Host.bmMarkedFocus ∧ acceptable Particle.yak Host.preverbalSubject ≠ acceptable Particle.ke Host.preverbalSubject

No particle-host uniformity: the two asymmetries cross-cut — association possibilities do not follow from the particle or the host alone.