Pronounceability of expressions

A predicate pronounceable : S → Prop separating expressions whose phonological form is realizable in a given language from those that are not. Most expressions in linglib are uniformly pronounceable, but several pragmatic accounts require referring to silent competitors:

• @cite{jeretic-bassi-gonzalez-yatsushiro-meyer-sauerland-2025} — the dual-marked structure tous les NP.dual is generated by the grammar of French but blocked from pronunciation by Avoid Ambiguity; the indirect alternative les deux NP competes with it.
• @cite{sauerland-alexiadou-2020} — Meaning First posits thought-level alternatives that need not be articulated.
• Trace theory, ellipsis, sluicing — silent material more generally.

This module supplies the typeclass and a default instance making Tree C W uniformly pronounceable, plus a lexicon-relativized pronounceability predicate that flags trees containing core-concept leaves not realized in the lexicon.

Pragmatic operators (e.g. Indirect.indirectFrom) require this predicate to define alternatives that pass through unpronounceable witnesses.

structure Alternatives.Pronounceability (S : Type u) : Type u

A pronounceability predicate on expressions.

Most pragmatic accounts assume all expressions are pronounceable, in which case clients should pass (fun _ => True); non-trivial instances arise when expressions can contain silent material that the language fails to realize (e.g. tous les NP.dual in @cite{jeretic-bassi-gonzalez-yatsushiro-meyer-sauerland-2025}).

We keep this as a structure rather than a typeclass: there is no canonical pronounceability per type — it depends on the lexicon, the phenomenon (traces vs ellipsis vs core-concept silent realization), and the analysis. Constants are exposed via the pron/unpron API on Pronounceability.

• pron : S → Prop

  The pronounceability predicate.

def Alternatives.Pronounceability.trivial {S : Type u} : Pronounceability S

The everything-pronounceable instance.

Equations

• Alternatives.Pronounceability.trivial = { pron := fun (x : S) => True }

def Alternatives.Pronounceability.unpron {S : Type u} (P : Pronounceability S) (s : S) : Prop

An expression is unpronounceable.

Equations

• P.unpron s = ¬P.pron s