Pragmatic competition

An expression is blocked when one of its alternatives is strictly better along a preorder, and it survives competition at a point where its content holds and no alternative whose content also holds there is strictly stronger. Blocked is the first relation, for any alternative source S → Set S and any map into a preorder, and unblocked the set of points of the second, for a content function S → Set W; sameAssertion keeps the alternatives with the same at-issue content. Ordered by entailment, blocking compares contents; ordered by harmony it is the blocking of bidirectional optimality theory (BidirectionalOT.blocks_iff_blocked).

Along at-issue content over the weakly assertable alternatives, blocking is Katzir's neo-Gricean principle, and along conventional-implicature content it is Lo Guercio's Maximize Conventional Implicatures. Along presuppositional content over sameAssertion it is Heim's Maximize Presupposition, and its condition at a context, as Schlenker states it, is unblocked: the presupposition less the presuppositions of the strictly stronger alternatives, whose removal is Percus's anti-presupposition and Sauerland's implicated presupposition. The relations carry no theory of why competition obtains, so pragmatic and grammatical accounts of each principle state their disagreement over one definition.

Main definitions

• Competition.Blocked: some alternative is strictly better along a preorder.
• Competition.unblocked: the points where no alternative whose content holds is strictly stronger.
• Competition.sameAssertion: the alternatives with the same at-issue content.

Main results

• Competition.not_blocked_iff_minimalFor: an expression is unblocked when it is minimal among itself and its alternatives.
• Competition.mem_unblocked_iff_minimalFor: an expression is unblocked where it is a most specific competitor whose content holds.
• Competition.disjoint_unblocked: competitors with strictly nested contents are never unblocked at the same point.
• Competition.unblocked_anti: more alternatives, fewer unblocked points.

References

• [Kat07]
• [LG25]
• [Hei91]
• [Sch12b]
• [Per06]
• [Sau08a]

def Competition.Blocked {S : Type u_1} {β : Type u_3} [Preorder β] (alts : S → Set S) (f : S → β) (φ : S) : Prop

φ is blocked when some alternative in alts φ is strictly better under f.

Equations

• Competition.Blocked alts f φ = ∃ φ' ∈ alts φ, f φ' < f φ

theorem Competition.Blocked.mono {S : Type u_1} {β : Type u_3} {alts alts' : S → Set S} {φ : S} [Preorder β] {f : S → β} (h : alts ≤ alts') (hb : Blocked alts f φ) : Blocked alts' f φ

Blocking is monotone in the alternative source.

theorem Competition.not_blocked_of_forall_le {S : Type u_1} {β : Type u_3} {alts : S → Set S} {φ : S} [Preorder β] {f : S → β} (h : ∀ φ' ∈ alts φ, f φ ≤ f φ') : ¬Blocked alts f φ

An expression at least as good as each of its alternatives is not blocked.

theorem Competition.not_blocked_iff_minimalFor {S : Type u_1} {β : Type u_3} {alts : S → Set S} {φ : S} [Preorder β] {f : S → β} : ¬Blocked alts f φ ↔ MinimalFor (fun (x : S) => x ∈ insert φ (alts φ)) f φ

An expression is unblocked exactly when it is minimal under f among itself and its alternatives.

def Competition.sameAssertion {S : Type u_1} {W : Type u_2} (alts : S → Set S) (assertion : S → Set W) (φ : S) : Set S

The alternatives of φ with the same at-issue content, the competitors Maximize Presupposition compares.

Equations

• Competition.sameAssertion alts assertion φ = {φ' : S | φ' ∈ alts φ ∧ assertion φ' = assertion φ}

@[simp]

theorem Competition.mem_sameAssertion {S : Type u_1} {W : Type u_2} {alts : S → Set S} {assertion : S → Set W} {φ φ' : S} : φ' ∈ sameAssertion alts assertion φ ↔ φ' ∈ alts φ ∧ assertion φ' = assertion φ

theorem Competition.sameAssertion_le {S : Type u_1} {W : Type u_2} (alts : S → Set S) (assertion : S → Set W) : sameAssertion alts assertion ≤ alts

Unblocked points

def Competition.unblocked {S : Type u_1} {W : Type u_2} (alts : S → Set S) (content : S → Set W) (φ : S) : Set W

φ is unblocked at the points where its content holds and no alternative whose content also holds there is strictly stronger: its content less the contents of the strictly stronger alternatives.

Equations

• Competition.unblocked alts content φ = content φ \ ⋃₀ (content '' alts φ ∩ Set.Iio (content φ))

theorem Competition.mem_unblocked_iff {S : Type u_1} {W : Type u_2} {alts : S → Set S} {content : S → Set W} {φ : S} {w : W} : w ∈ unblocked alts content φ ↔ w ∈ content φ ∧ ∀ ψ ∈ alts φ, w ∈ content ψ → ¬content ψ ⊂ content φ

theorem Competition.unblocked_subset {S : Type u_1} {W : Type u_2} (alts : S → Set S) (content : S → Set W) (φ : S) : unblocked alts content φ ⊆ content φ

theorem Competition.mem_unblocked_iff_minimalFor {S : Type u_1} {W : Type u_2} {alts : S → Set S} {content : S → Set W} {φ : S} {w : W} : w ∈ unblocked alts content φ ↔ MinimalFor (fun (ψ : S) => ψ ∈ insert φ (alts φ) ∧ w ∈ content ψ) content φ

φ is unblocked at w exactly when it is a most specific competitor whose content holds at w, among itself and its alternatives.

theorem Competition.unblocked_eq_self {S : Type u_1} {W : Type u_2} {alts : S → Set S} {content : S → Set W} {φ : S} (h : ¬Blocked alts content φ) : unblocked alts content φ = content φ

An expression blocked by no alternative is unblocked wherever its content holds.

theorem Competition.unblocked_eq_sdiff {S : Type u_1} {W : Type u_2} {alts : S → Set S} {content : S → Set W} {φ ψ : S} (hψ : ψ ∈ alts φ) (hss : content ψ ⊂ content φ) (hother : ∀ χ ∈ alts φ, content χ ⊂ content φ → content χ ⊆ content ψ) : unblocked alts content φ = content φ \ content ψ

With one strictly stronger alternative containing the others, φ is unblocked on its content less that alternative's.

theorem Competition.disjoint_unblocked_of_ssubset {S : Type u_1} {W : Type u_2} {alts : S → Set S} {content : S → Set W} {φ ψ : S} (hψ : ψ ∈ alts φ) (h : content ψ ⊂ content φ) : Disjoint (content ψ) (unblocked alts content φ)

Where φ is unblocked, no strictly stronger alternative's content holds.

theorem Competition.disjoint_unblocked {S : Type u_1} {W : Type u_2} {alts : S → Set S} {content : S → Set W} {φ ψ : S} (hψ : ψ ∈ alts φ) (h : content ψ ⊂ content φ) : Disjoint (unblocked alts content ψ) (unblocked alts content φ)

Two competitors with strictly nested contents are never unblocked at the same point.

theorem Competition.unblocked_ssubset_iff {S : Type u_1} {W : Type u_2} {alts : S → Set S} {content : S → Set W} {φ : S} : unblocked alts content φ ⊂ content φ ↔ ∃ ψ ∈ alts φ, content ψ ⊂ content φ ∧ (content ψ).Nonempty

An expression is unblocked at fewer points than its content holds exactly when some alternative with satisfiable content is strictly stronger.

theorem Competition.unblocked_anti {S : Type u_1} {W : Type u_2} {alts alts' : S → Set S} {content : S → Set W} {φ : S} (h : alts ≤ alts') : unblocked alts' content φ ⊆ unblocked alts content φ

Enlarging the alternatives shrinks the unblocked points, so an expression blocked by an independent factor widens the use of its competitors.