Documentation

Studies.Simik2024

Šimík (2024): Polar question semantics and bias: Lessons from Slavic/Czech #

This file formalizes Šimík's survey of polar-question bias in Slavic. A question form's bias profile is the set of cells, contextual evidence by prior epistemic bias (after Sudo), in which it is felicitous: Table 2 gives the profile of the four Czech forms, interrogative and declarative crossed with polarity (czechBiasProfile), and Table 1 the profile of the Serbian strategies reported from Todorović (serbianBiasProfile). The Czech cleaning-service scenarios (11)–(18) are typed rows, and the table predicts each judgment (cleaning_examples_match_table2); declaratives need evidence (declarative_requires_evidence) and Czech InterNPQ, unlike English high negation, is felicitous under positive evidence (interNPQ_broader_than_english_outer), while Serbian high negation is narrower than English (serbian_hnpq_narrower_than_english). The quiz scenario (24) diagnoses each of ten languages' default strategy: its positive form is the quiz-felicitous one (default_quiz_felicitous), declaratives never are (declarative_quiz_infelicitous), and negation triggers bias except under Polish czy and Macedonian dali (negationTriggersBias_iff). Serbian je li is neutral in Table 1 yet quiz-infelicitous (jeLi_neutral_yet_quiz_infelicitous), the contrast the chapter attributes to a covert 'wonder' selecting the question (wonderLF), which denotes the unique true answer (trueAnswers_polar_existsUnique). Russian razve resolves a conflict between evidence for the prejacent and a prior against it (razveProfile), invariantly across inner and outer negation (razveProfile_negation_invariant), and is a root phenomenon while li embeds (razve_root_li_embedded). The chapter's Czech FALSUM (falsumCz) presupposes only epistemic possibility of the prejacent, weaker than Repp's operator, the necessity □[epi ○ conv] (p ∉ cg ·) along the knowledge and conversational goals of its bearer (falsumCz_eq_one_of_falsum), and licenses the particle náhodou under outer negation alone (NahodouLicensed, nahodou_examples).

Implementation notes #

Table 2's starred DeclPPQ of the neutral cell, conditioned on a contrastive topic, is admitted by czechFelicitous and read off the row feature contrastiveTopic. The language rows carry the paper's own strategy labels; the derived predicates read the normalized strategy and polarity features. The kin of razve across Slavic are listed (razveKin) without a profile, as the chapter leaves their semantics open.

References #

Bias and the polarity of the prejacent (§3.1) #

def Simik2024.evidence (s : Polarity) :
SignType

The contextual evidence a conflict-resolving question of the given polarity rests on, which is evidence for the prejacent as asked.

Equations
Instances For
    def Simik2024.prior (s : Polarity) :
    SignType

    The prior epistemic bias a conflict-resolving question of the given polarity double-checks, which is against the prejacent as asked.

    Equations
    Instances For

      The polarity of a question with the given reading of negation, which is positive without negation and negative with either reading of it.

      Equations
      Instances For

        The Czech forms and their bias profile (§3.2, Table 2) #

        The chapter's grid of Czech polar-question forms, which crosses interrogative (verb-initial) or declarative word order with polarity.

        Instances For
          @[instance_reducible]
          Equations
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            The position of the negation of each grid cell, in [Rom24]'s forms. The verb-initial InterNPQ preposes its negated verb, a high negation question, and DeclNPQ does not, a low one.

            Equations
            Instances For
              @[instance_reducible]
              Equations
              • One or more equations did not get rendered due to their size.
              def Simik2024.czechBiasProfile :
              SignType → SignType → Finset CzechPQForm

              The forms natural in each cell of contextual evidence by prior epistemic bias (Table 2), with the starred DeclPPQ of the neutral cell left to czechFelicitous.

              Equations
              Instances For
                def Simik2024.czechFelicitous (ev ob : SignType) (ct : Bool) :

                The forms felicitous in a cell, admitting the unbiased declarative of (18) when a contrastive topic claims the initial position.

                Equations
                Instances For
                  theorem Simik2024.interPPQ_mem_iff (ev ob : SignType) :
                  CzechPQForm.interPPQ ∈ czechBiasProfile ev ob ↔ ev = 0 ∧ ob ≠ -1

                  The default form is natural exactly without evidence and without a prior against the prejacent.

                  theorem Simik2024.declPPQ_mem_iff (ev ob : SignType) :
                  CzechPQForm.declPPQ ∈ czechBiasProfile ev ob ↔ ev = 1 ∧ ob ≠ 1

                  DeclPPQ needs positive evidence and no prior for the prejacent.

                  theorem Simik2024.declNPQ_mem_iff (ev ob : SignType) :
                  CzechPQForm.declNPQ ∈ czechBiasProfile ev ob ↔ ev = -1 ∧ ob ≠ -1

                  DeclNPQ needs negative evidence and no prior against the prejacent.

                  theorem Simik2024.interNPQ_mem_iff (ev ob : SignType) :
                  CzechPQForm.interNPQ ∈ czechBiasProfile ev ob ↔ ob = 1 ∧ ev ≠ 1 ∨ ev = 1 ∧ ob = 0

                  InterNPQ conveys a prior for the prejacent, with neutral or conflicting evidence, or else positive evidence without a prior (the explanation-seeking (17)).

                  theorem Simik2024.declarative_requires_evidence (ev ob : SignType) (f : CzechPQForm) (hf : f.Declarative) (h : f ∈ czechBiasProfile ev ob) :
                  ev ≠ 0

                  Declarative questions are specialized for evidential bias ([Gun02]).

                  Czech high negation is broader than English, being felicitous under positive evidence, which the evidence condition of [BG00] on outer negation excludes.

                  The cleaning scenarios (11)–(18) #

                  The grid form a row instantiates.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    def Simik2024.evidence? (e : Datum) :
                    Option SignType

                    The contextual evidence of a row's scenario.

                    Equations
                    Instances For
                      def Simik2024.epistemic? (e : Datum) :
                      Option SignType

                      The speaker's prior epistemic bias in a row's scenario.

                      Equations
                      Instances For

                        Whether a row's scenario places a contrastive topic clause-initially.

                        Equations
                        Instances For
                          theorem Simik2024.cleaning_examples_match_table2 (e : Datum) :
                          e ∈ Examples.all → ∀ f ∈ form? e, ∀ ev ∈ evidence? e, ∀ ob ∈ epistemic? e, e.judgment = Judgment.unacceptable ↔ f ∉ czechFelicitous ev ob (contrastiveTopic e)

                          Table 2 predicts the scenarios. A form is judged infelicitous exactly when its cell excludes it, the degraded InterPPQ of (18) counting as admitted.

                          Default strategies under the quiz scenario (§4.1) #

                          The ten surveyed languages.

                          Instances For
                            @[instance_reducible]
                            Equations
                            def Simik2024.instReprLanguage.repr :
                            Language → ℕ → Std.Format
                            Equations
                            Instances For
                              @[instance_reducible]
                              Equations

                              The formal means of marking a polar question.

                              Instances For
                                @[instance_reducible]
                                Equations
                                def Simik2024.instReprStrategy.repr :
                                Strategy → ℕ → Std.Format
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[instance_reducible]
                                  Equations

                                  The strategy a quiz row instantiates.

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

                                    The polarity of a quiz row.

                                    Equations
                                    Instances For

                                      The quiz rows (25)–(34) of a language.

                                      Equations
                                      Instances For

                                        Every language's default strategy is quiz-felicitous in its positive form.

                                        Declarative polar questions convey evidential bias and are quiz-infelicitous in every language.

                                        Negation triggers bias in a language when no negated interrogative form is quiz-felicitous.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          @[instance_reducible]
                                          Equations

                                          Every language's quiz rows include a negated interrogative form.

                                          Negation triggers bias everywhere except under Polish czy (30b) and Macedonian dali (32a).

                                          theorem Simik2024.quiz_particles_in_fragment (l : Language) (e : Datum) :
                                          e ∈ quizRows l → ∀ f ∈ e.feature? "particle", f ∈ List.map (fun (x : Particle) => x.form) l.particles

                                          The particle of every quiz row is an entry of the language's fragment.

                                          Every fragment particle is recorded in matrix polar questions.

                                          The Serbian strategies and Todorović's bias profile (§4.2.2, Table 1) #

                                          The Serbian strategies of (31) and Table 1, which are the two positive particle strategies, high negation (nije li), and low negation (je l' … nije).

                                          Instances For
                                            @[instance_reducible]
                                            Equations
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              @[instance_reducible]
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              def Simik2024.serbianBiasProfile :
                                              SignType → SignType → Finset SerbianPQForm

                                              The Serbian strategies natural in each cell (Table 1), after [Tod23].

                                              Equations
                                              Instances For
                                                theorem Simik2024.daLiPPQ_mem_iff (ev ob : SignType) :
                                                SerbianPQForm.daLiPPQ ∈ serbianBiasProfile ev ob ↔ ev = 0 ∧ ob = 0

                                                da li questions are limited to neutral contexts.

                                                je li questions have the broader distribution.

                                                theorem Simik2024.ppq_no_negative_bias (ev ob : SignType) (f : SerbianPQForm) (hf : f.negation = none) (h : f ∈ serbianBiasProfile ev ob) :
                                                ev ≠ -1 ∧ ob ≠ -1

                                                Positive questions are incompatible with negative biases.

                                                theorem Simik2024.hnpq_mem_iff (ev ob : SignType) :
                                                SerbianPQForm.hnpq ∈ serbianBiasProfile ev ob ↔ ev = -1 ∧ ob = 1

                                                High negation resolves a conflict between a prior for the prejacent and evidence against it, and nothing else.

                                                Low negation has the broader distribution among negative questions.

                                                Serbian high negation is narrower than English, since neutral evidence, which the evidence condition of [BG00] on outer negation admits, admits no Serbian HNPQ.

                                                The quiz rows of (31) carry the markers of the Table 1 strategies.

                                                In the quiz-versus-information-seeking contrast, je li is natural in the neutral cell of Table 1 yet infelicitous in the quiz (31b), where da li is felicitous (31a).

                                                Information-seeking questions (§2, §4.2.1) #

                                                The chapter hypothesizes that the strategies that are neutral yet quiz-infelicitous (Serbian je li, Slovenian a, possibly Russian intonation questions) embed the Hamblin question under a covert 'wonder', modelled as 'want to know' applied to the true answer ([Kar77b], [Day96]); a quiz master knows the answer and so cannot want to know it.

                                                theorem Simik2024.trueAnswers_polar_existsUnique {W : Type u_1} (p : Set W) (w : W) :
                                                ∃! q : Set W, q ∈ Question.trueAnswers {p, pᶜ} w

                                                A polar question has exactly one true answer at each world.

                                                def Simik2024.wonderLF {W : Type u_1} (p : Set W) {E : Type u_2} (wantToKnow : E → Set W → Set W) (x : E) :
                                                Set W

                                                The speaker wants to know the true answer to the polar question over p (the chapter's (36)); the embedded (10b) is the same form with the attitude holder in place of the speaker.

                                                Equations
                                                Instances For

                                                  Russian razve and its kin (§4.2.4) #

                                                  def Simik2024.razveProfile (r : Option Polarity) :
                                                  SignType × SignType

                                                  The bias profile of a razve question on each reading, which pairs evidence for the prejacent as asked with a prior for its negation (the conflict-resolving profile of §3.1).

                                                  Equations
                                                  Instances For

                                                    The profile of razve negative questions is the same under inner negation (VERUM) and outer negation (FALSUM), with negative evidence and a positive prior.

                                                    def Simik2024.razveNegations :
                                                    Finset (Option Polarity)

                                                    Razve is compatible with both negations ([RG22]'s LFs (40), diagnosed by the polarity items in (41)), neuželi with inner negation only. The two readings double-check the negation of the prejacent, some .negative, and the prejacent itself, some .positive.

                                                    Equations
                                                    Instances For

                                                      Neuželi lexicalizes VERUM and so tolerates inner negation only.

                                                      Equations
                                                      Instances For

                                                        The kin of razve the chapter lists across Slavic, whose semantics it leaves open.

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

                                                          FALSUM and the Czech outer negation (§3.3.2, §5) #

                                                          noncomputable def Simik2024.falsumCz {W : Type u_1} (epi : SetRel W W) (cg : W → Filter W) (p : Set W) :
                                                          W → SignType

                                                          The chapter's Czech FALSUM (44) is defined when the attitude holder considers the prejacent possible, and true when it is not in the common ground.

                                                          Equations
                                                          Instances For
                                                            def Simik2024.falsumCzQuestion {W : Type u_1} (cg : W → Filter W) (p : Set W) :

                                                            The question (45) over the Czech FALSUM asks whether the prejacent is outside the common ground.

                                                            Equations
                                                            Instances For
                                                              theorem Simik2024.falsumCz_eq_zero_iff {W : Type u_1} (epi : SetRel W W) (cg : W → Filter W) (p : Set W) (w : W) :
                                                              falsumCz epi cg p w = 0 ↔ ModalLogic.Box epi (fun (x : W) => x ∉ p) w

                                                              The commitment of the Czech operator is weak, since its presupposition is epistemic possibility, the dual of necessity, and fails only where the prejacent is necessarily false.

                                                              theorem Simik2024.falsumCz_eq_one_of_falsum {W : Type u_1} (epi conv : SetRel W W) (cg : W → Filter W) (p : Set W) [(epi.comp conv).IsRefl] {w : W} (h : ModalLogic.Box (epi.comp conv) (fun (x : W) => p ∉ cg x) w) (hw : falsumCz epi cg p w ≠ 0) :
                                                              falsumCz epi cg p w = 1

                                                              [Rep13]'s FALSUM (22b), □[epi ○ conv] (p ∉ cg ·), makes the Czech operator true wherever it is defined when the bearer's knowledge-then-goals relation is reflexive, as it is for reflexive epi and conv; reflexive conv, every world satisfying the bearer's conversational goals, is an idealization.

                                                              Náhodou is licensed by outer negation and by nothing else (43). The two readings of negation in a polar question (the chapter's (14), after [Lad81] and [Rep13]) are polarities of the proposition the question double-checks. Inner negation, the classical propositional operator diagnosed by negative polarity items, double-checks the negation of the prejacent, .negative; outer negation, the non-propositional FALSUM diagnosed by positive polarity items, the prejacent itself, .positive.

                                                              Equations
                                                              Instances For
                                                                @[instance_reducible]
                                                                Equations

                                                                Náhodou needs outer negation (43d).

                                                                The reading of negation an indefinite diagnoses, the polarity item diagnosing the outer one and the concord item the inner one.

                                                                Equations
                                                                Instances For
                                                                  theorem Simik2024.nahodou_examples (e : Datum) :
                                                                  e ∈ Examples.all → e.feature? "nahodou" = some "true" → ∀ pol ∈ polarity? e, ∀ r ∈ indefiniteReading? e, e.judgment = Judgment.acceptable ↔ NahodouLicensed pol r

                                                                  The (43) rows with náhodou are acceptable exactly when the particle is licensed by the polarity and the reading the indefinite diagnoses.