Documentation

Studies.TrinhHaida2015

Trinh and Haida (2015): Constraining the Derivation of Alternatives #

This file formalizes Trinh and Haida's Atomicity constraint and the argument from symmetry that motivates it. Exhaustification EXH(A)(S) negates the innocently excludable members of a domain A of alternatives, (1), the substrate's exhIE, and on Fox and Katzir's theory A is the set of relevant members of the formal alternatives F(S), which, relevance being closed under negation and conjunction, amounts to the conditions (27): A ⊆ F(S), S ∈ A, and no member of F(S) outside A lies in the Boolean closure of A, IsDomain. Two symmetric alternatives, partitioning the prejacent, are then kept or dropped together whenever both are formal alternatives, IsDomain.mem_of_isSymmetric, so a domain holding one without the other does not exist, not_isDomain_pair_of_isSymmetric, and no inference against either arises. The puzzle, (20) against (21), is that Bill went for a run and didn't smoke; John only went for a run does license the inference that John smoked, although run and smoked is a formal alternative symmetric to the contextual run and didn't smoke, while Bill ate exactly three cookies; John only ate three licenses no inference against exactly three. Atomicity, (32), resolves it: expressions in the substitution source are syntactically atomic, so once a contextual constituent has been substituted in, its parts cannot be replaced, (33), and run and smoked is not derivable, Subst and atoms_mem_source. With it gone, {run, run ∧ ¬smoke} satisfies (27) whenever running and smoking are independent among non-runners, run_smoke_isDomain, and exhaustification yields run and smoked, exhIE_run_smoke; with four derived by lexical replacement and equal to three without exactly three, {three, exactly three} fails (27), the symmetric case.

Implementation notes #

Sentences are propositions Set W and the Boolean closure is mathlib's BooleanSubalgebra.closure; membership in it respects any agreement between worlds on the generators, mem_iff_of_mem_closure, which is how (27c) is refuted or established. The derivation of alternatives is by substitution alone, as the paper takes Fox and Katzir's to be, of a same-category source expression for a non-atomic constituent, and every substituted expression enters marked atomic, so an alternative differs from the prejacent by whole source expressions only; the substitution source, the sets F(S) of (35) and (42), and the independence of the predicates are taken from the paper rather than computed from a lexicon. The constraints (60b) and (60c) for the switching problem, bottom-up and non-weakening replacement, and the indirect implicature of (54) are described by the rows. The examples are the rows of Data.Examples.TrinhHaida2015.

References #

Conditions on the domain of exhaustification (27) #

source
structure TrinhHaida2015.IsDomain {W : Type u_1} (F : Set (Set W)) (S : Set W) (A : Set (Set W)) :
Prop

By (27), A is a domain of EXH for the prejacent S with formal alternatives F when it is a subset of F containing S and every member of F in its Boolean closure.

  • subset : A ⊆ F
  • self_mem : S ∈ A
  • closed (S' : Set W) : S' ∈ F → S' ∈ BooleanSubalgebra.closure A → S' ∈ A
Instances For
    source
    theorem TrinhHaida2015.mem_iff_of_mem_closure {W : Type u_1} {A : Set (Set W)} {p : Set W} (hp : p ∈ BooleanSubalgebra.closure A) {w v : W} (h : ∀ a ∈ A, w ∈ a ↔ v ∈ a) :
    w ∈ p ↔ v ∈ p

    A proposition in the Boolean closure of A separates no two worlds that agree on every member of A.

    source
    theorem TrinhHaida2015.notMem_closure_of_separates {W : Type u_1} {A : Set (Set W)} {p : Set W} {w v : W} (h : ∀ a ∈ A, w ∈ a ↔ v ∈ a) (hw : w ∈ p) (hv : v ∉ p) :
    p ∉ BooleanSubalgebra.closure A

    Two worlds agreeing on A but not on p witness that p is outside the closure.

    source
    theorem TrinhHaida2015.isDomain_self {W : Type u_1} {F : Set (Set W)} {S : Set W} (hS : S ∈ F) :
    IsDomain F S F

    The formal alternatives are a domain for any of their members.

    source
    theorem TrinhHaida2015.IsDomain.compl_mem {W : Type u_1} {F A : Set (Set W)} {S S₁ : Set W} (hA : IsDomain F S A) (h₁ : S₁ ∈ A) (h₂ : S₁ᶜ ∈ F) :
    S₁ᶜ ∈ A

    The negation of a member of a domain is in the domain whenever it is a formal alternative.

    source
    theorem TrinhHaida2015.IsDomain.mem_of_isSymmetric {W : Type u_1} {F A : Set (Set W)} {S S₁ S₂ : Set W} (hA : IsDomain F S A) (h : Alternatives.IsSymmetric S S₁ S₂) (h₁ : S₁ ∈ A) (h₂ : S₂ ∈ F) :
    S₂ ∈ A

    The partner of a symmetric alternative in a domain is in the domain's Boolean closure, so the domain contains it too whenever it is a formal alternative.

    source
    theorem TrinhHaida2015.not_isDomain_pair_of_isSymmetric {W : Type u_1} {F : Set (Set W)} {S S₁ S₂ : Set W} (h : Alternatives.IsSymmetric S S₁ S₂) (hne₁ : S₁.Nonempty) (h₂ : S₂ ∈ F) :
    ¬IsDomain F S {S, S₁}

    In (43), (46) and (49), the domain that would license an inference against one of two symmetric formal alternatives, the prejacent with that alternative alone, fails (27).

    source
    theorem TrinhHaida2015.isDomain_pair {W : Type u_1} {F : Set (Set W)} {S S₁ : Set W} (hS : S ∈ F) (h₁ : S₁ ∈ F) (h : ∀ S' ∈ F, S' ∈ BooleanSubalgebra.closure {S, S₁} → S' = S ∨ S' = S₁) :
    IsDomain F S {S, S₁}

    By (36), the prejacent with one alternative is a domain once every other formal alternative lies outside their Boolean closure.

    Symmetry breaking under Atomicity: run and smoke (section 3.2.2) #

    source
    theorem TrinhHaida2015.run_smoke_isDomain {W : Type u_1} {run smoke : Set W} {w v : W} (hw : w ∉ run ∧ w ∈ smoke) (hv : v ∉ run ∧ v ∉ smoke) :
    IsDomain {run, smoke, smokeᶜ, run ∩ smokeᶜ} run {run, run ∩ smokeᶜ}

    In (35)–(36), with run ∧ smoke underivable, {run, run ∧ ¬smoke} is a domain for the formal alternatives {run, smoke, ¬smoke, run ∧ ¬smoke}, provided a non-runner smokes in some world and not in another, since then neither smoke nor ¬smoke is in the closure.

    source
    theorem TrinhHaida2015.exhIE_run_smoke {W : Type u_1} {run smoke : Set W} {u : W} (hu : u ∈ run ∧ u ∈ smoke) :
    Exhaustification.exhIE {run, run ∩ smokeᶜ} run = run ∩ smoke

    The inference of (34) is that exhaustifying run against run ∧ ¬smoke yields run ∧ smoke, given a world in which someone runs and smokes.

    Atomicity (32) #

    source
    inductive TrinhHaida2015.ATree (C V : Type) :
    Type

    A tree in the derivation of alternatives is built from the prejacent's own constituents and the expressions substituted in from the source, which are atomic, their internal structure inaccessible (32). Binder bodies are opaque as well.

    Instances For
      source
      def TrinhHaida2015.ATree.cat {C V : Type} :
      ATree C V → C

      The category of the root.

      Equations
      Instances For
        source
        def TrinhHaida2015.ATree.ofTree {C V : Type} :
        PhraseStructure.Tree C V → ATree C V

        The prejacent enters the derivation with no atomic expression, an adjunction structure as a phrase.

        Equations
        Instances For
          source
          def TrinhHaida2015.ATree.ofTree.ofTreeList {C V : Type} :
          List (PhraseStructure.Tree C V) → List (ATree C V)
          Equations
          Instances For
            source
            def TrinhHaida2015.ATree.expand {C V : Type} :
            ATree C V → PhraseStructure.Tree C V

            The sentence a derivation tree stands for.

            Equations
            Instances For
              source
              def TrinhHaida2015.ATree.expand.expandList {C V : Type} :
              List (ATree C V) → List (PhraseStructure.Tree C V)
              Equations
              Instances For
                source
                def TrinhHaida2015.ATree.atoms {C V : Type} :
                ATree C V → List (PhraseStructure.Tree C V)

                The atomic expressions of a tree.

                Equations
                Instances For
                  source
                  def TrinhHaida2015.ATree.atoms.atomsList {C V : Type} :
                  List (ATree C V) → List (PhraseStructure.Tree C V)
                  Equations
                  Instances For
                    source
                    def TrinhHaida2015.ATree.Replaceable {C V : Type} :
                    ATree C V → Prop

                    By (60a), only a non-atomic expression is replaceable.

                    Equations
                    Instances For
                      source
                      theorem TrinhHaida2015.ATree.atoms_ofTree {C V : Type} (t : PhraseStructure.Tree C V) :
                      (ofTree t).atoms = []
                      source
                      theorem TrinhHaida2015.ATree.atomsList_ofTreeList {C V : Type} (cs : List (PhraseStructure.Tree C V)) :
                      atoms.atomsList (ofTree.ofTreeList cs) = []
                      source
                      theorem TrinhHaida2015.ATree.mem_atomsList_set {C V : Type} (cs : List (ATree C V)) (i : Fin cs.length) (ψ : ATree C V) {a : PhraseStructure.Tree C V} :
                      a ∈ atoms.atomsList (cs.set (↑i) ψ) → a ∈ ψ.atoms ∨ a ∈ atoms.atomsList cs

                      Replacing one child adds only that child's atomic expressions.

                      source
                      theorem TrinhHaida2015.ATree.mem_atomsList_of_getElem {C V : Type} (cs : List (ATree C V)) (i : Fin cs.length) {a : PhraseStructure.Tree C V} :
                      a ∈ cs[i].atoms → a ∈ atoms.atomsList cs

                      A child's atomic expressions are among the tree's.

                      source
                      inductive TrinhHaida2015.Subst {C V : Type} (source : List (PhraseStructure.Tree C V)) :
                      ATree C V → ATree C V → Prop

                      In one substitution, (13a) under (32), a replaceable constituent is replaced by a same-category expression of the source, which enters as atomic. Substitution is the only operation, since [FK11]'s simplification is by substitution alone.

                      Instances For
                        source
                        def TrinhHaida2015.Derivable {C V : Type} (source : List (PhraseStructure.Tree C V)) :
                        ATree C V → ATree C V → Prop

                        Derivability by successive substitution.

                        Equations
                        Instances For
                          source
                          def TrinhHaida2015.formalAlternatives {C V : Type} (source : List (PhraseStructure.Tree C V)) (φ : PhraseStructure.Tree C V) :
                          Set (PhraseStructure.Tree C V)

                          The formal alternatives of a prejacent under Atomicity are the sentences of the trees derivable from it.

                          Equations
                          Instances For
                            source
                            theorem TrinhHaida2015.Subst.atoms_mem_source {C V : Type} {source : List (PhraseStructure.Tree C V)} {φ ψ : ATree C V} (h : Subst source φ ψ) (hφ : ∀ a ∈ φ.atoms, a ∈ source) (a : PhraseStructure.Tree C V) :
                            a ∈ ψ.atoms → a ∈ source

                            A substitution adds one atomic expression, from the source.

                            source
                            theorem TrinhHaida2015.atoms_mem_source {C V : Type} {source : List (PhraseStructure.Tree C V)} {φ : PhraseStructure.Tree C V} {t : ATree C V} (h : Derivable source (ATree.ofTree φ) t) (a : PhraseStructure.Tree C V) :
                            a ∈ t.atoms → a ∈ source

                            Every atomic expression of a derivable tree is a source expression, so an alternative differs from the prejacent by whole source expressions, so the second step of (33), replacing inside one, is impossible.