Documentation

Linglib.Semantics.Questions.Highlighting

Highlighting #

Besides the proposition it expresses, a sentence highlights some possibilities, making them salient as antecedents for anaphora such as polarity particles, and each highlighted possibility is negative when the sentence introducing it is negative. Roelofsen and Farkas compute the highlights of a formula compositionally beside its inquisitive proposition, so that ?p and ?¬p express the same issue but highlight p positively and its complement negatively. This file develops basic results about highlighting, including that every formula expresses the proposition of the InqB formula it abbreviates, while its highlights are a function neither of that proposition nor of that InqB formula.

Main definitions #

Implementation notes #

The projections ! and ? are primitive, since !p and ¬¬p highlight differently, although in InqB they abbreviate ¬¬φ and φ \\/ ¬φ; conjunction and implication are omitted, as in Roelofsen and Farkas.

References #

source
def Highlighting.neg {W : Type u_1} (H : Set (Polarity × Set W)) :
Set (Polarity × Set W)

The negation of a formula highlights, negatively, the complement of everything the formula highlights.

Equations
Instances For
    source
    noncomputable def Highlighting.project {W : Type u_1} (H : Set (Polarity × Set W)) :
    Set (Polarity × Set W)

    A projection of a formula keeps a single negative possibility and otherwise highlights, positively, the union of what the formula highlights.

    Equations
    Instances For
      source
      @[simp]
      theorem Highlighting.neg_singleton {W : Type u_1} (s : Polarity) (α : Set W) :
      neg {(s, α)} = {(Polarity.negative, αᶜ)}

      The negation of a formula highlighting a single possibility highlights its complement.

      source
      @[simp]
      theorem Highlighting.project_singleton_negative {W : Type u_1} (α : Set W) :
      project {(Polarity.negative, α)} = {(Polarity.negative, α)}

      Projection keeps a single negative possibility.

      source
      @[simp]
      theorem Highlighting.project_singleton_positive {W : Type u_1} (α : Set W) :
      project {(Polarity.positive, α)} = {(Polarity.positive, α)}

      Projection keeps a single positive possibility.

      source
      @[simp]
      theorem Highlighting.project_singleton {W : Type u_1} (x : Polarity × Set W) :
      project {x} = {x}

      Projection keeps a single possibility, whatever its polarity.

      source
      inductive Highlighting.Formula (A : Type u_2) :
      Type u_2

      A formula is built from atoms by negation, inquisitive disjunction, and the non-inquisitive and non-informative projections ! and ? ([RF15]).

      Instances For
        source
        @[instance_reducible]
        instance Highlighting.instDecidableEqFormula {A✝ : Type u_2} [DecidableEq A✝] :
        DecidableEq (Formula A✝)
        Equations
        source
        def Highlighting.instDecidableEqFormula.decEq {A✝ : Type u_2} [DecidableEq A✝] (x✝ x✝¹ : Formula A✝) :
        Decidable (x✝ = x✝¹)
        Equations
        Instances For
          source
          def Highlighting.instReprFormula.repr {A✝ : Type u_2} [Repr A✝] :
          Formula A✝ → ℕ → Std.Format
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[instance_reducible]
            instance Highlighting.instReprFormula {A✝ : Type u_2} [Repr A✝] :
            Repr (Formula A✝)
            Equations
            source
            def Highlighting.Formula.proposition {W : Type u_1} {A : Type u_2} (v : A → Set W) :
            Formula A → Question W

            The proposition a formula expresses under the valuation v of its atoms (26).

            Equations
            Instances For
              source
              noncomputable def Highlighting.Formula.highlights {W : Type u_1} {A : Type u_2} (v : A → Set W) :
              Formula A → Set (Polarity × Set W)

              The possibilities a formula highlights, each with its polarity (60).

              Equations
              Instances For
                source
                def Highlighting.Formula.ofPolarity {A : Type u_2} :
                Polarity → A → Formula A

                The basic formula of polarity s on the atom a is a or ¬a.

                Equations
                Instances For
                  source
                  @[simp]
                  theorem Highlighting.Formula.proposition_ofPolarity {W : Type u_1} {A : Type u_2} (v : A → Set W) (s : Polarity) (a : A) :
                  proposition v (ofPolarity s a) = Question.ofSet (s • v a)

                  A basic formula of polarity s on a expresses the proposition s • v a.

                  source
                  @[simp]
                  theorem Highlighting.Formula.highlights_ofPolarity {W : Type u_1} {A : Type u_2} (v : A → Set W) (s : Polarity) (a : A) :
                  highlights v (ofPolarity s a) = {s • (Polarity.positive, v a)}

                  A basic formula of polarity s on a highlights the image of (positive, v a) under s, the negative polarity complementing the possibility and reversing its polarity.

                  source
                  theorem Highlighting.Formula.proposition_query_ofPolarity {W : Type u_1} {A : Type u_2} (v : A → Set W) (s : Polarity) (a : A) :
                  proposition v (ofPolarity s a).query = Question.polar (v a)

                  The polar interrogatives on a and on ¬a express the same issue.

                  source
                  theorem Highlighting.Formula.not_exists_highlights_eq_comp_proposition {W : Type u_1} {A : Type u_2} (v : A → Set W) [Nonempty A] :
                  ¬∃ (f : Question W → Set (Polarity × Set W)), ∀ (φ : Formula A), highlights v φ = f (proposition v φ)

                  The highlights of a formula are not a function of its proposition, since ?a and ?¬a express the same issue but highlight different possibilities.

                  source
                  def Highlighting.Formula.toInquisitive {A : Type u_2} :
                  Formula A → Inquisitive.Formula A

                  The InqB formula a formula abbreviates, with !φ as ¬¬φ and ?φ as φ \\/ ¬φ.

                  Equations
                  Instances For
                    source
                    theorem Highlighting.Formula.isModalFree_toInquisitive {A : Type u_2} (φ : Formula A) :
                    φ.toInquisitive.IsModalFree
                    source
                    theorem Highlighting.Formula.proposition_toInquisitive {W : Type u_1} {A : Type u_2} [Fintype W] [DecidableEq W] (M : Inquisitive.Model W A) (φ : Formula A) :
                    Inquisitive.proposition M φ.toInquisitive = proposition (fun (a : A) => {w : W | M.val a w}) φ

                    A formula expresses the proposition of the InqB formula it abbreviates, under the valuation of the atoms by their truth sets in M.

                    source
                    theorem Highlighting.Formula.not_exists_highlights_eq_comp_toInquisitive {W : Type u_1} {A : Type u_2} (v : A → Set W) [Nonempty A] :
                    ¬∃ (f : Inquisitive.Formula A → Set (Polarity × Set W)), ∀ (φ : Formula A), highlights v φ = f φ.toInquisitive

                    The highlights of a formula are not a function of the InqB formula it abbreviates, since !a and ¬¬a abbreviate the same formula but highlight a with opposite polarities.