Indirect alternatives

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

A novel notion of pragmatic alternative introduced by Jeretič, Bassi, Gonzalez, Yatsushiro, Meyer & Sauerland (2025) to account for the anti-duality of French tous.

Definition (paper eq 43)

A pronounceable parse tree I is an indirect alternative of S iff there exists an unpronounceable alternative Sₓ of S (drawn from some base alternative source — typically Katzir's structural alternatives) such that ⟦I⟧ = ⟦Sₓ⟧ and size I ≤ size S.

Application to French tous

The dual structure tous les NP.dual is generated by the grammar (Katzir-substituting pl → dual in the number-feature slot of les NP), but blocked from pronunciation by Avoid Ambiguity (Theories/Pragmatics/AvoidAmbiguity.lean) because its phonological realization coincides with the plural-marked tous les NP. The pronounceable expression les deux NP ('the two NP') is semantically equivalent to tous les NP.dual and at-most-as-complex (Katzir node count). It is therefore an indirect alternative — and triggers Maximize Presupposition, deriving anti-duality of tous.

The infrastructure is generic over the base alternative source, the pronounceability predicate, and the meaning function. It composes with violatesMP from Alternatives.Structural: pass indirectFrom base P meaning size instead of the bare base source to obtain an MP rule that competes with unpronounceable witnesses.

See Phenomena/Presupposition/Studies/JereticEtAl2025.lean for the empirical applications.

def Alternatives.Indirect.indirectFrom {S : Type u} {M : Type v} (base : AlternativeSource S) (P : Pronounceability S) (meaning : S → M) (size : S → ℕ) : AlternativeSource S

The indirect-alternative source (paper eq 43).

indirectFrom base P meaning size s is the set of pronounceable expressions s' such that size s' ≤ size s and there is some unpronounceable sₓ ∈ base s with meaning s' = meaning sₓ.

Parameters:

• base: the underlying alternative source (typically Katzir).
• P: the pronounceability predicate; unpron P sₓ ≡ ¬ P.pron sₓ.
• meaning: the semantic interpretation function.
• size: complexity measure (e.g. Tree.size).

Note: the surrogate s' is not required to be pronounceable here — that is enforced separately by the consumer (typically MP, which only asserts the implicated presupposition for pronounceable competitors).

Equations

• Alternatives.Indirect.indirectFrom base P meaning size s = {s' : S | size s' ≤ size s ∧ ∃ sₓ ∈ base s, P.unpron sₓ ∧ meaning s' = meaning sₓ}

theorem Alternatives.Indirect.size_le_of_mem {S : Type u} {M : Type v} {base : AlternativeSource S} {P : Pronounceability S} {meaning : S → M} {size : S → ℕ} {s' s : S} (h : s' ∈ indirectFrom base P meaning size s) : size s' ≤ size s

Indirect alternatives are at most as complex as the original.

theorem Alternatives.Indirect.empty_when_all_pronounceable {S : Type u} {M : Type v} {base : AlternativeSource S} {P : Pronounceability S} {meaning : S → M} {size : S → ℕ} {s' s : S} (h : s' ∈ indirectFrom base P meaning size s) (allPron : ∀ x ∈ base s, P.pron x) : False

The indirect-alternative set is empty when the base source contains no unpronounceable witnesses — the genuine refinement: an indirect alternative requires a silent witness in the base.