Documentation

Studies.RomeroHan2004

Romero and Han (2004): On negative yes/no questions #

This file formalizes the paper's derivation of the epistemic bias of yes/no questions with preposed negation from one assumption: preposing negation contributes the conversational epistemic operator VERUM, FOR-SURE-CG (43), true at a world when the proposition is in the common ground at every world satisfying the conversational goals of an individual x at every world conforming to the knowledge of x, x being the addressee, or the addressee and the speaker together. With epi and conv the accessibility relations of x, it is the necessity □[epi ○ conv] (p ∈ cg ·), which ModalLogic.box_comp unfolds into the paper's two quantifiers. A question over VERUM partitions on certainty about adding the proposition to the common ground rather than on the proposition, denotation_eq, a meta-conversational move licit only under a prior bias; the paper's positive and negative readings are the two scopes of negation relative to VERUM, distinguished by which polarity items they license, Licensed. The polarity of the implicature is fixed not by the partition, which the positive reading shares with a really-question, but by the pronounced cell: pronouncing certainty asks for conclusive evidence, so the speaker believes the negation, and pronouncing uncertainty asks for doubts, so the speaker believes the proposition, speakerBelief_eq. The paper's examples are rows: the polarity-item judgments follow licensing, and the bias of every question with preposed negation and of every VERUM form is the one the model implicates, bias_of_form.

Implementation notes #

The common ground at a world is a filter of propositions, so acceptance is closed under entailment and conjunction where the paper speaks of a set of propositions. VERUM is not a named operator of its own: other analyses built on it, [Rep13]'s FALSUM among them, are necessities along the same relation of the common ground's acceptance of a proposition or its failure to. Speaker belief is the epistemic proposition of the states settling a proposition, Set.Iic. A question's form is the position of its negation, Option NegationPosition, what matters being its position relative to the rest of the clause, preposed or not; a bias is the sign of the proposition the speaker's belief supports. The Principle of Economy that makes VERUM questions biased is stated in the paper in prose and is not formalized.

References #

The four VERUM questions #

source
inductive RomeroHan2004.Form :
Type

The yes/no questions containing VERUM: the positive reading of preposed negation, with negation over VERUM (73), the negative reading, with VERUM over negation (68), the really-question (111), and focused NOT (118).

Instances For
    source
    @[instance_reducible]
    instance RomeroHan2004.instDecidableEqForm :
    DecidableEq Form
    Equations
    source
    @[instance_reducible]
    instance RomeroHan2004.instFintypeForm :
    Fintype Form
    Equations
    source
    def RomeroHan2004.prejacent {W : Type u_1} (p : Set W) :
    Form → Set W

    The proposition under VERUM: the proposition for the positive reading and really, its negation for the negative reading and focused NOT.

    Equations
    Instances For
      source
      def RomeroHan2004.Form.Doubt :
      Form → Prop

      Whether the form pronounces the doubt cell, the complement of VERUM: only the positive reading, where negation scopes over VERUM, does.

      Equations
      Instances For
        source
        @[instance_reducible]
        instance RomeroHan2004.instDecidablePredFormDoubt :
        DecidablePred Form.Doubt
        Equations
        • One or more equations did not get rendered due to their size.
        source
        def RomeroHan2004.pronounced {W : Type u_1} (epi conv : SetRel W W) (cg : W → Filter W) (p : Set W) (f : Form) :
        Set W

        The cell a form pronounces: VERUM of the prejacent, or its complement.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def RomeroHan2004.denotation {W : Type u_1} (epi conv : SetRel W W) (cg : W → Filter W) (p : Set W) (f : Form) :
          Question W

          The question denoted: the polar question over the pronounced cell.

          Equations
          Instances For
            source
            theorem RomeroHan2004.denotation_eq {W : Type u_1} (epi conv : SetRel W W) (cg : W → Filter W) (p : Set W) (f : Form) :
            denotation epi conv cg p f = Question.polar {w : W | ModalLogic.Box (epi.comp conv) (fun (x : W) => prejacent p f ∈ cg x) w}

            Every VERUM question denotes the partition on certainty about its prejacent (48), (69), (74), whichever cell it pronounces.

            source
            theorem RomeroHan2004.denotation_pi_eq_really {W : Type u_1} (epi conv : SetRel W W) (cg : W → Filter W) (p : Set W) :
            denotation epi conv cg p Form.pi = denotation epi conv cg p Form.really

            The positive reading and the really-question denote the same partition (84), (85).

            The epistemic implicature #

            A question pronouncing certainty about its prejacent asks for conclusive evidence for it, which the addressee can only supply if the prejacent is the addressee's proposition and its negation the speaker's belief; a question pronouncing uncertainty asks for doubts, so the prejacent is the speaker's belief.

            source
            def RomeroHan2004.speakerBelief {W : Type u_1} (p : Set W) (f : Form) :
            Set (Set W)

            The speaker's original belief implicated by a form: the epistemic proposition of the states settling the prejacent's negation, or the prejacent itself for the doubt cell.

            Equations
            Instances For
              source
              def RomeroHan2004.Form.implicature :
              Form → Polarity

              The bias each form implicates: belief in the proposition for the preposed-negation readings (81), (82) and focused NOT (117), belief in its negation for really (110).

              Equations
              Instances For
                source
                theorem RomeroHan2004.speakerBelief_eq {W : Type u_1} (p : Set W) (f : Form) :
                speakerBelief p f = Set.Iic (f.implicature • p)

                The implicated belief settles the proposition under the polarity of the form's implicature; the partition shared by the positive reading and really cannot fix it.

                Polarity items #

                Positive polarity items are licensed under VERUM in a positive clause and negative ones in a negative clause (70), (71), (75), (76); VERUM intervenes between negation and the clause in the positive reading, so the clause is negated only in the negative reading and under focused NOT.

                source
                def RomeroHan2004.Form.Negated :
                Form → Prop

                Whether the clause under VERUM is negated.

                Equations
                Instances For
                  source
                  @[instance_reducible]
                  instance RomeroHan2004.instDecidablePredFormNegated :
                  DecidablePred Form.Negated
                  Equations
                  • One or more equations did not get rendered due to their size.
                  source
                  def RomeroHan2004.Licensed (e : PolarityItem) (f : Form) :
                  Prop

                  A polarity item is licensed in a form iff a positive item finds the clause unnegated and a negative one finds it negated.

                  Equations
                  Instances For
                    source
                    @[instance_reducible]
                    instance RomeroHan2004.instDecidableLicensed (e : PolarityItem) (f : Form) :
                    Decidable (Licensed e f)
                    Equations

                    The paper's examples #

                    source
                    structure RomeroHan2004.Row :
                    Type

                    An example: the position of its negation, if any, its reported bias, its VERUM form and its polarity item, each when the paper gives one, and its judgment.

                    Instances For
                      source
                      def RomeroHan2004.Row.ofDatum (e : Datum) :
                      Row

                      A datum read into its row.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        def RomeroHan2004.data :
                        List Row

                        The paper's examples.

                        Equations
                        Instances For
                          source
                          theorem RomeroHan2004.licensed_iff_acceptable (d : Row) :
                          d ∈ data → ∀ e ∈ d.item.toList, ∀ f ∈ d.form.toList, Licensed e f ↔ d.judgment = Judgment.acceptable

                          Licensing predicts every too and either judgment on (6), (7) and (77) to (80).

                          source
                          theorem RomeroHan2004.bias_of_negation (d : Row) :
                          d ∈ data → ∀ n ∈ d.negation.toList, ∀ b ∈ d.bias.toList, (n = some NegationPosition.preposed → b = 1) ∧ (n = some NegationPosition.nonPreposed → b = 0)

                          Preposed negation carries a positive bias in every language of the survey, (1), (5) and (14) to (18), and non-preposed negation none.

                          source
                          theorem RomeroHan2004.bias_of_form (d : Row) :
                          d ∈ data → ∀ f ∈ d.form.toList, ∀ b ∈ d.bias.toList, b = ↑f.implicature

                          The bias reported for a VERUM form is the belief the model implicates.