Grubic (2015): Focus and Alternative Sensitivity in Ngamo

Grubic analyses the Ngamo alternative-sensitive particles of chapter 7 against the data of chapter 6, the rows of Data.Examples.Grubic2015, in a question-under-discussion framework. The exclusive yak('i) has Coppock and Beaver's entry for exclusives, the substrate's Focus.Particles.only: it presupposes that some alternative at least as strong as the prejacent on a salient scale is true and asserts that no true alternative is stronger. The additive ke('e) has no truth-conditional content and presupposes a salient antecedent about a different topic situation, and the scalar har('i) asserts its prejacent and presupposes that a contextual implication of it ranks highest among its alternatives.

Main results

• prejacent_projects: on an entailment scale, the complement-exclusion reading, the presupposition of yak('i) entails the prejacent, which therefore projects through negation.
• posExt_only_conjunctions: over the conjunctions of independent atomic answers yak('i) is defined and true exactly where the prejacent holds and every other atom fails.
• ke_eq_zero_of_anaphoric: parallel background-marked antecedents, being anaphoric, cannot supply the antecedent of ke('e).

Implementation notes

The scale is a relation S q p read as q at least as strong as p, the entailment scale being (· ⊆ ·); the VP and NP variants (5) and (6), which reach the propositional entry by the Geach rule, are not repeated. Topic situations are abstracted to a map from answers to a type of situations, so that the non-overlap of (45) is distinctness. The association facts of section 6.2, on which yak('i) alone associates with focus conventionally, are data rows and not theorems.

References

• [Gru15]
• [CB14]
• [BC08]

The exclusive yak('i), section 7.1

theorem Grubic2015.prejacent_projects {W : Type u_1} (C : Set (Set W)) (p : Set W) {w : W} (h : -Focus.Particles.only (fun (x1 x2 : Set W) => x1 ⊆ x2) C p w ≠ 0) : w ∈ p

Negation leaves the presupposition in place, so not only Dimza built a house still has Dimza building a house (29); on a rank-order scale, where alternatives need not entail the prejacent, nothing of the kind follows.

def Grubic2015.conjunctions {W : Type u_1} (atoms : Set (Set W)) : Set (Set W)

The answers of (11) are the nonempty conjunctions of a set of atomic answers.

Equations

• Grubic2015.conjunctions atoms = {q : Set W | ∃ A ⊆ atoms, A.Nonempty ∧ q = ⋂₀ A}

theorem Grubic2015.posExt_only_conjunctions {W : Type u_1} (p : Set W) {atoms : Set (Set W)} (hp : p ∈ atoms) : Trivalent.posExt (Focus.Particles.only (fun (x1 x2 : Set W) => x1 ⊆ x2) (conjunctions atoms) p) = Exhaustification.exh atoms p

Over the conjunctions of atomic answers, the truth set of yak('i) on the entailment scale is the prejacent with no other atom true, the exhaustification Exhaustification.exh over the atoms ((166) and (25)).

The additive ke('e), section 7.3

noncomputable def Grubic2015.ke {W : Type u_1} {T : Type u_2} (p : Set W) (salient : Set (Set W)) (topic : Set W → T) : W → SignType

ke('e) 'also' (45) makes no truth-conditional contribution and presupposes a salient antecedent about a different topic situation, one that need not itself be true (46).

Equations

• Grubic2015.ke p salient topic = {_w : W | ∃ q ∈ salient, topic q ≠ topic p}.indicator fun (w : W) => SignType.ofProp (w ∈ p)

theorem Grubic2015.ke_eq_zero_of_anaphoric {W : Type u_1} {T : Type u_2} (p : Set W) {salient : Set (Set W)} {topic : Set W → T} (h : ∀ q ∈ salient, topic q = topic p) (w : W) : ke p salient topic w = 0

When every salient antecedent is anaphoric to the host's topic situation, as parallel background-marked antecedents are by default, ke('e) is undefined ((44) and (49)).

The scalar har('i), section 7.2

def Grubic2015.CImpl {W : Type u_1} (p CG q : Set W) : Prop

A contextual implication (18) is entailed by the common ground updated with the prejacent but not by the common ground alone.

Equations

• Grubic2015.CImpl p CG q = (¬CG ⊆ q ∧ CG ∩ p ⊆ q)

noncomputable def Grubic2015.har {W : Type u_1} (S : Set W → Set W → Prop) (p CG : Set W) (alt : Set W → Set (Set W)) : W → SignType

har('i) 'even' (17) asserts the prejacent and presupposes that some contextual implication of it ranks highest among its alternatives on the salient scale.

Equations

• Grubic2015.har S p CG alt = {w : W | ∃ (q : Set W), Grubic2015.CImpl p CG q ∧ ∀ q' ∈ alt q, w ∈ q' → S q q'}.indicator fun (w : W) => SignType.ofProp (w ∈ p)

theorem Grubic2015.har_impl_holds {W : Type u_1} (S : Set W → Set W → Prop) (p : Set W) {CG : Set W} {alt : Set W → Set (Set W)} {w : W} (hw : w ∈ CG) (hp : w ∈ p) (h : har S p CG alt w ≠ 0) : ∃ (q : Set W), CImpl p CG q ∧ w ∈ q

At a world of the common ground where the prejacent holds, the implication har('i) presupposes holds as well, so the scale is anchored by a true alternative.