Avoid Ambiguity

@cite{jeretic-bassi-gonzalez-yatsushiro-meyer-sauerland-2025}

The pragmatic principle Jeretič, Bassi, Gonzalez, Yatsushiro, Meyer & Sauerland (2025) introduce as eq (37):

If a string S is ambiguous between two parses P1 and P2, and there is a string S' with a parse P1' whose meaning is semantically equivalent to P1, but no parse P2' equivalent to P2, and S' is structurally at most as complex as S, then string S cannot realize parse P1.

In words: do not realize a parse P1 of an ambiguous string S when a no-more-complex unambiguous expression S' is available with the same meaning. Surface ambiguity is acceptable; redundant ambiguity (where the clearer alternative exists at no extra cost) is not.

Why this is its own principle

AvoidAmbiguity differs from Maximize Presupposition (cf. Theories.Semantics.Alternatives.Structural.violatesMP) along three axes:

1. Trigger: MP's competitor wins by stronger presupposition; AA's competitor wins by less ambiguity.
2. Domain: MP compares meanings (one parse per expression); AA compares parse-sets per expression.
3. Output: MP adds an implicated presupposition; AA blocks a parse from being realized at all.

Both share the "competitor at-most-as-complex" cost ceiling, but the asymmetry in trigger/output prevents collapsing them under one rule.

Application to French tous

In Jeretič et al. 2025, AA blocks the parse [tous les NP.dual] (generated by the grammar via the dual core concept) because its phonological realization tous les NP is also ambiguous with [tous les NP.pl], and the unambiguous expression les deux NP (no more complex by node count) realizes the dual meaning. The blocked dual parse persists as an unpronounceable alternative, feeding indirect competition (Theories.Semantics.Alternatives.Indirect).

Generic shape

The principle is parametric in:

• parses : S → List P — each surface string maps to its set of parses.
• meaning : P → M — semantic interpretation of a parse.
• size : S → Nat — complexity measure.

It is therefore reusable for any Avoid-Ambiguity-style competition: lexical blocking, syncretism, Aronoff-style word formation, etc.

def Pragmatics.AvoidAmbiguity.IsAmbiguous {S P M : Type u} [DecidableEq M] (parses : S → List P) (meaning : P → M) (s : S) : Prop

A string S is ambiguous if it has at least two parses with distinct meanings. Singletons and meaning-equivalent multi-parses do not count as ambiguous.

Equations

• Pragmatics.AvoidAmbiguity.IsAmbiguous parses meaning s = ∃ (p₁ : P), p₁ ∈ parses s ∧ ∃ (p₂ : P), p₂ ∈ parses s ∧ meaning p₁ ≠ meaning p₂

def Pragmatics.AvoidAmbiguity.UnambiguouslyRealizes {S P M : Type u} [DecidableEq M] (parses : S → List P) (meaning : P → M) (s' s : S) (p : P) : Prop

A string S' is unambiguously equivalent to a parse p of S iff some parse of S' realizes the same meaning as p, and no parse of S' realizes any meaning that some other parse of S realizes distinctly from p.

In the paper's wording: S' has a parse P1' equivalent to P1, but no parse P2' equivalent to P2 (for any other parse P2 of S).

Equations

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

def Pragmatics.AvoidAmbiguity.Blocked {S P M : Type u} [DecidableEq M] (parses : S → List P) (meaning : P → M) (size : S → ℕ) (s : S) (p : P) : Prop

The Avoid Ambiguity blocking relation (paper eq 37).

Blocked parses meaning size s p holds iff there is an alternative string s' of complexity at most size s that unambiguously realizes the meaning of p. Then s is forbidden from realizing parse p.

Equations

• Pragmatics.AvoidAmbiguity.Blocked parses meaning size s p = ∃ (s' : S), size s' ≤ size s ∧ Pragmatics.AvoidAmbiguity.UnambiguouslyRealizes parses meaning s' s p

theorem Pragmatics.AvoidAmbiguity.self_witness_only_unambiguous {S P M : Type u} [DecidableEq M] [DecidableEq P] (parses : S → List P) (meaning : P → M) (s : S) (p : P) (hWit : UnambiguouslyRealizes parses meaning s s p) (p₂ : P) : p₂ ∈ parses s → meaning p₂ = meaning p

A parse p of an unambiguous string s is never blocked by s itself: s cannot serve as its own clearer competitor (it has only one meaning, but the existential requires another string to bear witness — and even if s = s', the clause is vacuous when s is unambiguous). This expresses that AA does not block parses of unambiguous strings via self-competition.

Concretely: if s is unambiguous and s itself is the witness s', then the second clause of UnambiguouslyRealizes (no s'-parse equiv to a different parse p₂ of s) requires that for every p₂ ≠ p of s, no s-parse equates p₂ — but p₂ itself is such a parse, contradiction.

theorem Pragmatics.AvoidAmbiguity.blocking_requires_atMostAsComplex {S P M : Type u} [DecidableEq M] {parses : S → List P} {meaning : P → M} {size : S → ℕ} {s : S} {p : P} (h : Blocked parses meaning size s p) : ∃ (s' : S), size s' ≤ size s

Avoid Ambiguity does not block via more-complex witnesses.

Decidability

IsAmbiguous and UnambiguouslyRealizes are decidable from [DecidableEq M] alone, since they only quantify over the finite list parses s. Blocked requires an additional witness set: we expose blockedOver, the list-relativized version, which checks the existential against an explicitly-supplied candidate list rather than imposing a Fintype S constraint globally.

@[implicit_reducible]

instance Pragmatics.AvoidAmbiguity.instDecidableIsAmbiguous {S P M : Type u} [DecidableEq M] (parses : S → List P) (meaning : P → M) (s : S) : Decidable (IsAmbiguous parses meaning s)

Equations

• Pragmatics.AvoidAmbiguity.instDecidableIsAmbiguous parses meaning s = id inferInstance

@[implicit_reducible]

instance Pragmatics.AvoidAmbiguity.instDecidableUnambiguouslyRealizes {S P M : Type u} [DecidableEq M] (parses : S → List P) (meaning : P → M) (s' s : S) (p : P) : Decidable (UnambiguouslyRealizes parses meaning s' s p)

Equations

• Pragmatics.AvoidAmbiguity.instDecidableUnambiguouslyRealizes parses meaning s' s p = id inferInstance

def Pragmatics.AvoidAmbiguity.blockedOver {S P M : Type u} [DecidableEq M] (parses : S → List P) (meaning : P → M) (size : S → ℕ) (candidates : List S) (s : S) (p : P) : Bool

Decision procedure for Blocked against a specific list of candidate strings. Returns true iff some candidate s' ∈ candidates of size ≤ size s unambiguously realizes p.

Equations

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

theorem Pragmatics.AvoidAmbiguity.blocked_of_blockedOver {S P M : Type u} [DecidableEq M] (parses : S → List P) (meaning : P → M) (size : S → ℕ) (candidates : List S) (s : S) (p : P) (h : blockedOver parses meaning size candidates s p = true) : Blocked parses meaning size s p

blockedOver soundly witnesses Blocked.