Trinh & Haida 2015: Constraining the Derivation of Alternatives

@cite{trinh-haida-2015}

Trinh, T. & Haida, A. (2015). Constraining the derivation of alternatives. Natural Language Semantics, 23(4), 249–270.

Core Contribution

The Atomicity constraint (def 32): expressions in the substitution source are syntactically atomic — their internal structure is inaccessible to structural operations. This refines @cite{fox-katzir-2011} / @cite{katzir-2007} to correctly distinguish:

• Symmetry-breaking cases (§3.2.2): "Bill ran and didn't smoke. John ran." → John smoked. Atomicity blocks "ran ∧ smoked" from F(S), so A = {run, run ∧ ¬smoke} satisfies Conditions on A (27), and EXH derives ¬(run ∧ ¬smoke).

• Symmetry-preserving cases (§3.2.3): "Bill ate exactly three. John ate three." → ✗John ate exactly three. Atomicity is vacuous; Conditions on A (27c) force "four" into A, creating symmetry.

Key Definitions

• inBooleanClosure: p is determined by a set of propositions (27c)
• isValidDomain: Conditions on A (27) for EXH domains
• ATree / ATStructOp: parse trees with AT-marking; structural operations that cannot enter AT-marked nodes
• structuralAlternativesAT: F_AT(S) ⊆ F(S)

Relation to the Excluder.preFilter combinator

Atomicity is a restriction on the formal-alternative source F, the @cite{fox-katzir-2011} F (not C) side of the asymmetry. Theories/Semantics/Exhaustification/Combinators.lean packages F-side restrictions as the abstract combinator Excluder.preFilter, with the algebraic non-monotonicity theorem preFilter_can_create_implicature. The Trinh–Haida construction is a linguistically-motivated two-layer F-side restriction (Atomicity + Conditions on A), so it doesn't reduce to a single preFilter call: innocent.exh on full F_AT(run) remains vacuous; the strengthening to ran ∧ smoked requires the further domain-choice step A = {ran, ranNotSmoked}. The Symmetric/Atomic formalization here is therefore complementary to (not subsumed by) the abstract combinator: Combinators.lean proves the asymmetry exists in the algebra; this file shows the linguistic substance the asymmetry licenses.

def Alternatives.AtomicConstraint.inBooleanClosure {W : Type} (domain : List W) (alts : List (W → Bool)) (p : W → Bool) : Bool

A proposition p is in the Boolean closure of alts: p is determined by the truth values of elements of alts. Whenever two worlds agree on all elements of alts, they agree on p. Used in Condition (27c).

Equations

• Alternatives.AtomicConstraint.inBooleanClosure domain alts p = domain.all fun (w₁ : W) => domain.all fun (w₂ : W) => (!alts.all fun (a : W → Bool) => a w₁ == a w₂) || p w₁ == p w₂

def Alternatives.AtomicConstraint.propEqOn {W : Type} (domain : List W) (p q : W → Bool) : Bool

Extensional equality on a finite domain.

Equations

• Alternatives.AtomicConstraint.propEqOn domain p q = domain.all fun (w : W) => p w == q w

def Alternatives.AtomicConstraint.propMemOn {W : Type} (domain : List W) (p : W → Bool) (alts : List (W → Bool)) : Bool

Extensional membership via propEqOn.

Equations

• Alternatives.AtomicConstraint.propMemOn domain p alts = alts.any fun (a : W → Bool) => Alternatives.AtomicConstraint.propEqOn domain p a

def Alternatives.AtomicConstraint.isValidDomain {W : Type} (domain : List W) (formalAlts : List (W → Bool)) (prejacent : W → Bool) (domainOfEXH : List (W → Bool)) : Bool

Conditions on A (27): A is a valid domain of EXH for prejacent S given formal alternatives formalAlts = F(S).

(27a) A ⊆ F(S) (27b) S ∈ A (27c) No S' in F(S) \ A is in the Boolean closure of A

Equations

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

inductive Alternatives.AtomicConstraint.ATree (W : Type) : Type

Parse tree with optional AT-marking. AT-marked nodes (atNode) preserve content for semantic interpretation but are inaccessible to structural operations — implementing the Atomicity constraint (def 32): "Expressions in the substitution source are syntactically atomic."

• leaf {W : Type} (cat : Core.Tree.Cat) (word : W) : ATree W
• node {W : Type} (cat : Core.Tree.Cat) (children : List (ATree W)) : ATree W
• atNode {W : Type} (cat : Core.Tree.Cat) (content : Core.Tree.Tree Core.Tree.Cat W) : ATree W

def Alternatives.AtomicConstraint.ATree.cat {W : Type} : ATree W → Core.Tree.Cat

Equations

• (Alternatives.AtomicConstraint.ATree.leaf c word).cat = c
• (Alternatives.AtomicConstraint.ATree.node c children).cat = c
• (Alternatives.AtomicConstraint.ATree.atNode c content).cat = c

def Alternatives.AtomicConstraint.ATree.expand {W : Type} : ATree W → Core.Tree.Tree Core.Tree.Cat W

Expand to Tree Cat by unsealing AT-marked nodes.

Equations

• (Alternatives.AtomicConstraint.ATree.leaf c word).expand = Core.Tree.Tree.terminal c word
• (Alternatives.AtomicConstraint.ATree.node c children).expand = Core.Tree.Tree.node c (Alternatives.AtomicConstraint.ATree.expand.expandList children)
• (Alternatives.AtomicConstraint.ATree.atNode c content).expand = content

def Alternatives.AtomicConstraint.ATree.expand.expandList {W : Type} : List (ATree W) → List (Core.Tree.Tree Core.Tree.Cat W)

Equations

• Alternatives.AtomicConstraint.ATree.expand.expandList [] = []
• Alternatives.AtomicConstraint.ATree.expand.expandList (t :: ts) = t.expand :: Alternatives.AtomicConstraint.ATree.expand.expandList ts

def Alternatives.AtomicConstraint.ATree.lift {W : Type} : Core.Tree.Tree Core.Tree.Cat W → ATree W

Lift a Tree Cat to ATree (no AT-marking). Traces and binders are wrapped as opaque AT-marked nodes, since they are LF-specific structure inaccessible to PF-level operations.

Equations

• Alternatives.AtomicConstraint.ATree.lift (Core.Tree.Tree.terminal c w) = Alternatives.AtomicConstraint.ATree.leaf c w
• Alternatives.AtomicConstraint.ATree.lift (Core.Tree.Tree.node c cs) = Alternatives.AtomicConstraint.ATree.node c (Alternatives.AtomicConstraint.ATree.lift.liftList cs)
• Alternatives.AtomicConstraint.ATree.lift (Core.Tree.Tree.trace n c) = Alternatives.AtomicConstraint.ATree.atNode c (Core.Tree.Tree.trace n c)
• Alternatives.AtomicConstraint.ATree.lift (Core.Tree.Tree.bind n c body) = Alternatives.AtomicConstraint.ATree.atNode c (Core.Tree.Tree.bind n c body)

def Alternatives.AtomicConstraint.ATree.lift.liftList {W : Type} : List (Core.Tree.Tree Core.Tree.Cat W) → List (ATree W)

Equations

• Alternatives.AtomicConstraint.ATree.lift.liftList [] = []
• Alternatives.AtomicConstraint.ATree.lift.liftList (t :: ts) = Alternatives.AtomicConstraint.ATree.lift t :: Alternatives.AtomicConstraint.ATree.lift.liftList ts

inductive Alternatives.AtomicConstraint.ATStructOp {W : Type} (source : List (ATree W)) : ATree W → ATree W → Prop

Structural operation respecting Atomicity. Like StructOp but inChild can only descend into .node, NOT .atNode. AT-marked material is opaque to further syntactic manipulation.

• subst {W : Type} {source : List (ATree W)} {φ ψ : ATree W} (h_cat : ψ.cat = φ.cat) (h_src : ψ ∈ source) : ATStructOp source φ ψ
• delete {W : Type} {source : List (ATree W)} {cat : Core.Tree.Cat} {cs : List (ATree W)} (i : Fin cs.length) : ATStructOp source (ATree.node cat cs) (ATree.node cat (cs.eraseIdx ↑i))
• contract {W : Type} {source : List (ATree W)} {cat : Core.Tree.Cat} {cs : List (ATree W)} {child : ATree W} (h_mem : child ∈ cs) (h_cat : child.cat = cat) : ATStructOp source (ATree.node cat cs) child
• inChild {W : Type} {source : List (ATree W)} {cat : Core.Tree.Cat} {cs : List (ATree W)} (i : Fin cs.length) {ψ_child : ATree W} (h_step : ATStructOp source (cs.get i) ψ_child) : ATStructOp source (ATree.node cat cs) (ATree.node cat (cs.set (↑i) ψ_child))

def Alternatives.AtomicConstraint.atReachable {W : Type} (source : List (ATree W)) (ψ φ : ATree W) : Prop

AT-constrained reachability (reflexive-transitive closure).

Equations

• Alternatives.AtomicConstraint.atReachable source ψ φ = Relation.ReflTransGen (Alternatives.AtomicConstraint.ATStructOp source) φ ψ

def Alternatives.AtomicConstraint.atomicSubstitutionSource {W : Type} (lexicon : List (Core.Tree.Tree Core.Tree.Cat W)) (φ : Core.Tree.Tree Core.Tree.Cat W) (context : List (Core.Tree.Tree Core.Tree.Cat W)) : List (ATree W)

The substitution source with Atomicity: lexical items + subtrees of S are lifted (transparent); contextual constituents are wrapped in atNode (opaque).

Equations

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

def Alternatives.AtomicConstraint.structuralAlternativesAT {W : Type} (lex : List (Core.Tree.Tree Core.Tree.Cat W)) (φ : Core.Tree.Tree Core.Tree.Cat W) (context : List (Core.Tree.Tree Core.Tree.Cat W)) : Set (Core.Tree.Tree Core.Tree.Cat W)

F_AT(S): formal alternatives derivable under Atomicity. S' ∈ F_AT(S) iff ∃ ATree t reachable from lift(S) via AT-constrained operations with t.expand = S'.

Equations

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

Symmetry Breaking

(34) Bill went for a run and didn't smoke. John (only) went for a run. Inference: ¬[John went for a run and didn't smoke] → John smoked.

Atomicity blocks "ran ∧ smoked" from F(S) because deriving it requires modifying the interior of the AT-marked contextual constituent "ran ∧ ¬smoked" (removing the NegP). This leaves A = {run, run ∧ ¬smoke} as a valid domain satisfying (27c), and EXH(A)(run) = run ∧ smoke.

inductive Alternatives.AtomicConstraint.AW : Type

Four activity worlds (run and smoke are independent).

• rs : AW
• rns : AW
• s : AW
• ns : AW

@[implicit_reducible]

instance Alternatives.AtomicConstraint.instDecidableEqAW : DecidableEq AW

Equations

• Alternatives.AtomicConstraint.instDecidableEqAW x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Alternatives.AtomicConstraint.instReprAW.repr : AW → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Alternatives.AtomicConstraint.instReprAW : Repr AW

Equations

• Alternatives.AtomicConstraint.instReprAW = { reprPrec := Alternatives.AtomicConstraint.instReprAW.repr }

@[implicit_reducible]

instance Alternatives.AtomicConstraint.instFintypeAW : Fintype AW

Equations

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

theorem Alternatives.AtomicConstraint.run_valid_domain : isValidDomain Alternatives.AtomicConstraint.awDomain✝ Alternatives.AtomicConstraint.fATrun✝ Alternatives.AtomicConstraint.ran✝ Alternatives.AtomicConstraint.domainA✝ = true

A satisfies all three Conditions on A (27). Crucially, (27c) holds: neither "smoke" nor "¬smoke" is in BC({run, run ∧ ¬smoke}) because the 4-world domain distinguishes them from all Boolean combinations.

theorem Alternatives.AtomicConstraint.run_exh_correct : Exhaustification.innocent.exh (Exhaustification.altsFromPreds Alternatives.AtomicConstraint.domainA✝) (Exhaustification.predToFinset Alternatives.AtomicConstraint.ran✝) = Exhaustification.predToFinset fun (w : AW) => Alternatives.AtomicConstraint.ran✝ w && Alternatives.AtomicConstraint.smoked✝ w

EXH(A)(run) = run ∧ smoke: the correct empirical inference. exhIE negates "run ∧ ¬smoke" (the only non-weaker alternative in A), deriving that John smoked.

theorem Alternatives.AtomicConstraint.without_atomicity_vacuous : Exhaustification.innocent.exh (Exhaustification.altsFromPreds [Alternatives.AtomicConstraint.ran✝, Alternatives.AtomicConstraint.smoked✝, Alternatives.AtomicConstraint.didntSmoke✝, Alternatives.AtomicConstraint.ranNotSmoked✝, Alternatives.AtomicConstraint.ranAndSmoked✝]) (Exhaustification.predToFinset Alternatives.AtomicConstraint.ran✝) = Exhaustification.predToFinset Alternatives.AtomicConstraint.ran✝

Symmetry Preserving

(41) Bill ate exactly three cookies. John (only) ate three cookies. *Inference: ¬[John ate exactly three cookies]

Atomicity is vacuous here (alternatives are derived by simple lexical substitution). The non-attested inference is blocked by Conditions on A (27c): "four" ∈ BC({three, exactly_three}), so excluding "four" from A is impossible, but including it creates symmetry.

inductive Alternatives.AtomicConstraint.CW : Type

Three cookie worlds: ate exactly 3, 4, or 5.

• w3 : CW
• w4 : CW
• w5 : CW

@[implicit_reducible]

instance Alternatives.AtomicConstraint.instDecidableEqCW : DecidableEq CW

Equations

• Alternatives.AtomicConstraint.instDecidableEqCW x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Alternatives.AtomicConstraint.instReprCW.repr : CW → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Alternatives.AtomicConstraint.instReprCW : Repr CW

Equations

• Alternatives.AtomicConstraint.instReprCW = { reprPrec := Alternatives.AtomicConstraint.instReprCW.repr }

@[implicit_reducible]

instance Alternatives.AtomicConstraint.instFintypeCW : Fintype CW

Equations

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

theorem Alternatives.AtomicConstraint.four_in_bc : inBooleanClosure Alternatives.AtomicConstraint.cwDomain✝ [Alternatives.AtomicConstraint.three✝, Alternatives.AtomicConstraint.exactlyThree✝] Alternatives.AtomicConstraint.four✝ = true

"four" is in BC({three, exactly_three}): worlds agreeing on both "three" (always true) and "exactly_three" always agree on "four", because four ≡ three ∧ ¬exactly_three on this domain.

theorem Alternatives.AtomicConstraint.restricted_domain_invalid : isValidDomain Alternatives.AtomicConstraint.cwDomain✝ Alternatives.AtomicConstraint.fCookies✝ Alternatives.AtomicConstraint.three✝ [Alternatives.AtomicConstraint.three✝, Alternatives.AtomicConstraint.exactlyThree✝] = false

A = {three, exactly_three} violates (27c): "four" is excluded from A but is in BC(A).

theorem Alternatives.AtomicConstraint.full_domain_valid : isValidDomain Alternatives.AtomicConstraint.cwDomain✝ Alternatives.AtomicConstraint.fCookies✝ Alternatives.AtomicConstraint.three✝ Alternatives.AtomicConstraint.fCookies✝ = true

A = F(S) = {three, exactly_three, four} satisfies (27).

theorem Alternatives.AtomicConstraint.cookies_symmetric : Symmetric.isSymmetric Alternatives.AtomicConstraint.cwDomain✝ Alternatives.AtomicConstraint.three✝ Alternatives.AtomicConstraint.exactlyThree✝ Alternatives.AtomicConstraint.four✝ = true

"exactly_three" and "four" are symmetric alternatives of "three": they partition its denotation.

theorem Alternatives.AtomicConstraint.cookies_exh_vacuous : Exhaustification.innocent.exh (Exhaustification.altsFromPreds Alternatives.AtomicConstraint.fCookies✝) (Exhaustification.predToFinset Alternatives.AtomicConstraint.three✝) = Exhaustification.predToFinset Alternatives.AtomicConstraint.three✝

With A = F(S) (the only valid domain), exhIE is vacuous: the symmetric alternatives make exhaustification identity.

Switching Problem Constraints

For structures where a weak scalar item embeds a strong one (e.g., [some[all]]), Atomicity alone is insufficient. The paper adds three constraints on the derivation of formal alternatives:

(60a) Only non-AT-marked expressions are replaceable. (60b) The most deeply embedded replaceable expression must be replaced first (bottom-up). (60c) No replacement may yield a sentence logically weaker than the prejacent.

These constraints prevent "some" and "all" from switching places under negation while still allowing the correct indirect implicature derivation. (60a) is already captured by ATStructOp (no inChild into atNode). (60b) and (60c) are additional derivation-order and semantic monotonicity constraints:

def Alternatives.AtomicConstraint.bottomUpOrdering (pos maxReplaceable : ℕ) : Prop

(60b) Bottom-up ordering: the replacement position must be at least as deeply embedded as any other replaceable position. Modeled as a property of a derivation step at position pos in a tree of depth maxDepth.

Equations

• Alternatives.AtomicConstraint.bottomUpOrdering pos maxReplaceable = (pos ≥ maxReplaceable)

def Alternatives.AtomicConstraint.nonWeakeningStep {W : Type} (domain : List W) (before after : W → Bool) : Bool

(60c) Semantic monotonicity: the result of a replacement step must not be logically weaker than the input (on the domain).

Equations

• Alternatives.AtomicConstraint.nonWeakeningStep domain before after = ((!domain.any fun (w : W) => before w && !after w) || domain.any fun (w : W) => after w && !before w)