Documentation

Studies.QingEtAl2025

Qing et al. (2025): When Can Non-Veridical Preferential Attitude Predicates Take Questions? #

Qing, Özyıldız, Roelofsen, Romero and Uegaki classify non-veridical preferential predicates by clausal distributivity and evaluative valence. Uegaki and Sudo derive the anti-rogativity of hope from two assumptions, that the predicate is clausally distributive and that it presupposes Threshold Significance. Neither holds in general: worry and Mandarin qidai relate the agent to the question rather than to an answer, and negative predicates such as fear lack the presupposition. Composition with a question is therefore trivial, and the predicate anti-rogative, exactly for the distributive positive class. Apparent uses of hope with a polar question are non-canonical, and the asymmetry between hoping for the radical and for its negation follows from the goals of a hopeful wondering.

Main statements #

Implementation notes #

Triviality quantifies over the degree function and threshold, the non-logical constants of Gajewski's analyticity, with the question as its own comparison class, and the concrete models measure preference in the reals. A relational predicate is a parameter relating the agent to the question, since the paper characterizes the class only as a relation to the question not reducible to one to any answer. The class of a predicate is read off the valence and distributivity its lexical entry records. The paper contrasts positive with negative predicates; a neutral one is taken to lack threshold significance, as a negative one does. The pragmatic derivation compares coming to believe the radical or not by Kratzer's ordering with the event's goals as ordering source; the event summation of the adjunction analysis is not formalized. The Spanish predicates without a Fragment entry, temer and preocupar, are classified here. Rows carry the paper's truth values where it gives them and its felicity judgments otherwise; the attested hope whether examples are recorded as marginal, and temer with a polar question and haipa with a constituent question are recorded but not predicted.

References #

The two escapes from triviality (§3) #

The concrete models measure preference in the reals.

source
theorem QingEtAl2025.relational_not_isDistributive {W : Type u_1} {E : Type u_2} (R : E → Set (Set W) → W → Prop) {x : E} {Q : Set (Set W)} {w : W} (hR : R x Q w) (h : ∀ p ∈ Q, ¬R x {p} w) :
¬Distributivity.IsDistributive R

A predicate that relates an agent to a question without relating her to any of its answers, anxious uncertainty for worry (§3.1.2) or anticipation of resolution for Mandarin qidai (§3.1.1), is not clausally distributive. This is the diagnostic of (23) to (25).

source
def QingEtAl2025.Trivial {W : Type u_1} {E : Type u_2} (V : (E → W → Set W → ℝ) → (Set (Set W) → ℝ) → Set (Set W) → E → Set (Set W) → W → Prop) (π : (E → W → Set W → ℝ) → (Set (Set W) → ℝ) → E → Set (Set W) → W → Prop) :
Prop

Composition of a predicate family with a question is trivial under a presupposition when in every model the presupposition entails the assertion, the question serving as its own comparison class as in Uegaki and Sudo's account. The composition is then true whenever defined, which is Gajewski's analyticity with the degree function and threshold as the non-logical constants.

Equations
  • QingEtAl2025.Trivial V π = ∀ (μ : E → W → Set W → ℝ) (θ : Set (Set W) → ℝ) (x : E) (Q : Set (Set W)) (w : W), π μ θ x Q w → V μ θ Q x Q w
Instances For
    source
    def QingEtAl2025.presupposition {W : Type u_1} {E : Type u_2} :
    Degree.EvaluativeValence → (E → W → Set W → ℝ) → (Set (Set W) → ℝ) → E → Set (Set W) → W → Prop

    A positive preferential predicate presupposes threshold significance of a question. A negative one triggers no such presupposition (§3.2) and presupposes only that the question has an answer in the comparison class.

    Equations
    Instances For
      source
      theorem QingEtAl2025.trivial_positive {W : Type u_1} {E : Type u_2} :
      Trivial Preferential.degreeComparison (presupposition Degree.EvaluativeValence.positive)

      A distributive positive predicate composed with a question is trivial, as Uegaki and Sudo show.

      source
      theorem QingEtAl2025.not_trivial_negative {W : Type u_1} {E : Type u_2} [Inhabited E] [Inhabited W] {v : Degree.EvaluativeValence} (hv : v ≠ Degree.EvaluativeValence.positive) :
      ¬Trivial Preferential.degreeComparison (presupposition v)

      Without threshold significance, x fears Q says only that some answer is feared, which a model falsifies.

      source
      theorem QingEtAl2025.not_trivial_relational {W : Type u_1} {E : Type u_2} (v : Degree.EvaluativeValence) (R : E → Set (Set W) → W → Prop) (hR : ∃ (x : E) (Q : Set (Set W)) (w : W), Q.Nonempty ∧ ¬R x Q w) :
      ¬Trivial (fun (x : E → W → Set W → ℝ) (x_1 : Set (Set W) → ℝ) (x_2 : Set (Set W)) => R) (presupposition v)

      A relational predicate is not trivial even under threshold significance, since some agent does not stand in the relation to a question an answer of which clears the threshold.

      The classification (Table 2) #

      source
      inductive QingEtAl2025.PredicateClass :
      Type

      The three classes of non-veridical preferential predicates.

      • nonDistributive : PredicateClass

        Class 1 consists of the predicates that are not clausally distributive, of either valence.

      • distributiveNegative : PredicateClass

        Class 2 consists of the distributive negative predicates.

      • distributivePositive : PredicateClass

        Class 3 consists of the distributive positive predicates, the class Uegaki and Sudo describe.

      Instances For
        source
        @[instance_reducible]
        instance QingEtAl2025.instDecidableEqPredicateClass :
        DecidableEq PredicateClass
        Equations
        source
        @[instance_reducible]
        instance QingEtAl2025.instReprPredicateClass :
        Repr PredicateClass
        Equations
        source
        def QingEtAl2025.instReprPredicateClass.repr :
        PredicateClass → ℕ → Std.Format
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def QingEtAl2025.classOf :
          Attitude → Option PredicateClass

          The class of a predicate, read off the valence and distributivity its lexical entry records. A distributive predicate of neutral valence is outside the classification.

          Equations
          Instances For
            source
            def QingEtAl2025.semantics {W : Type u_1} {E : Type u_2} (R : E → Set (Set W) → W → Prop) :
            Bool → (E → W → Set W → ℝ) → (Set (Set W) → ℝ) → Set (Set W) → E → Set (Set W) → W → Prop

            The interrogative use of a preferential predicate is a degree comparison when it is distributive and a relation R to the question otherwise.

            Equations
            Instances For
              source
              theorem QingEtAl2025.trivial_iff_class {W : Type u_1} {E : Type u_2} [Inhabited E] [Inhabited W] (v : Degree.EvaluativeValence) (d : Bool) (R : E → Set (Set W) → W → Prop) (hR : ∃ (x : E) (Q : Set (Set W)) (w : W), Q.Nonempty ∧ ¬R x Q w) :
              Trivial (semantics R d) (presupposition v) ↔ classOf (Attitude.preferential v d) = some PredicateClass.distributivePositive

              Canonical composition with a question is trivial, hence anti-rogative, exactly for the distributive positive class (Table 2).

              The paper's judgments #

              source
              def QingEtAl2025.attitude? :
              String → Option Attitude

              attitude? s is the attitude that the predicate name s denotes, read off the Fragment entry for English, Mandarin, Japanese, Turkish, and Spanish esperar, and off the paper's classification for the other Spanish predicates.

              Equations
              Instances For
                source
                def QingEtAl2025.class? (r : Datum) :
                Option PredicateClass

                The class of a row's predicate.

                Equations
                Instances For
                  source
                  def QingEtAl2025.valence? (r : Datum) :
                  Option Degree.EvaluativeValence

                  The valence of a row's predicate, or of its manner adverb or veridical preferential where the paper's argument turns on valence alone.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def QingEtAl2025.Holds (r : Datum) :
                    Prop

                    A row holds in its context when it is judged true, where the paper gives a truth value, and when it is not infelicitous otherwise.

                    Equations
                    Instances For
                      source
                      @[instance_reducible]
                      instance QingEtAl2025.instDecidableHolds (r : Datum) :
                      Decidable (Holds r)
                      Equations
                      • One or more equations did not get rendered due to their size.
                      source
                      def QingEtAl2025.Argument (r : Datum) :
                      Prop

                      An interrogative complement composed canonically, as the predicate's argument.

                      Equations
                      Instances For
                        source
                        @[instance_reducible]
                        instance QingEtAl2025.instDecidableArgument (r : Datum) :
                        Decidable (Argument r)
                        Equations
                        source
                        theorem QingEtAl2025.responsive_rows (r : Datum) :
                        r ∈ Examples.all → Argument r → r.judgment = Judgment.acceptable → ∀ c ∈ class? r, c ≠ PredicateClass.distributivePositive

                        Every acceptable interrogative complement is under a class 1 or class 2 predicate.

                        source
                        theorem QingEtAl2025.anti_rogative_rows (r : Datum) :
                        r ∈ Examples.all → Argument r → class? r = some PredicateClass.distributivePositive → r.judgment ≠ Judgment.acceptable

                        Under canonical composition a class 3 predicate takes no question: the paper marks every such example, hope whether and its counterparts in the four other languages.

                        source
                        theorem QingEtAl2025.tsp_rows (r : Datum) :
                        r ∈ Examples.all → r.feature? "polarity" = some "negated" → ∀ v ∈ valence? r, r.judgment = Judgment.acceptable ↔ v = Degree.EvaluativeValence.negative

                        A negated positive preferential is infelicitous where the agent prefers no answer, and a negated negative one is felicitous, so the negative predicates lack threshold significance. The rows are (38) to (41), (44), (49), and (52).

                        source
                        theorem QingEtAl2025.nondistributive_rows (r : Datum) :
                        r ∈ Examples.all → r.feature? "truth" = some "false" → r.feature? "clause" = some "declarative" → class? r = some PredicateClass.nonDistributive ∧ ∃ r' ∈ Examples.all, r'.context = r.context ∧ r'.feature? "predicate" = r.feature? "predicate" ∧ r'.feature? "clause" = some "constituent" ∧ r'.feature? "truth" = some "true"

                        Every declarative the paper judges false is under a class 1 predicate and sits beside a constituent question of the same predicate judged true in the same context. This is the non-distributivity diagnostic of (23) to (36).

                        source
                        theorem QingEtAl2025.diye_rows (r : Datum) :
                        r ∈ Examples.all → r.feature? "embedding" = some "diye" → r.judgment = Judgment.acceptable

                        Turkish diye clauses combine with um- "hope", kork- "fear", and an intransitive verb alike, in (71), (73), (75), and (76), as adjoined reports of wondering rather than arguments.

                        source
                        def QingEtAl2025.turkishVerb? :
                        String → Option Turkish.Verb

                        turkishVerb? s is the Fragment verb that the predicate name s of a Turkish row names.

                        Equations
                        Instances For
                          source
                          def QingEtAl2025.turkishInflections :
                          List (List ((σ : Turkish.Verb.Slot) × Turkish.Verb.Exponent σ))

                          The paper's glosses segment its Turkish finite verbs into four inflections, the imperfective, its negative, its past, and the perfective past, the last two in the first person.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            theorem QingEtAl2025.turkish_forms (r : Datum) :
                            r ∈ Examples.all → r.language = "nucl1301" → ∃ v ∈ (r.feature? "predicate").bind turkishVerb?, ∃ sfx ∈ turkishInflections, Turkish.Verb.Licensed (v.suffixes sfx) ∧ ∃ t ∈ r.glossedTokens, Turkish.Phonology.ofSegmented? t.1 = some (v.inflect sfx)

                            The finite verb of every Turkish row is its predicate's Fragment entry under one of the paper's inflections. The finite-verb template licenses the suffix string, and the Fragment's phonology derives its surface form, korkmuyor and umuyordum among them.

                            source
                            theorem QingEtAl2025.dolan_isIntransitive :
                            Turkish.dolan.IsIntransitive

                            The verb of (73) is intransitive, so its diye clause is no argument.

                            Non-canonical composition (§4) #

                            source
                            theorem QingEtAl2025.highlighted_eq_declarative {W : Type u_1} {E : Type u_2} (μ : E → W → Set W → ℝ) (θ : Set (Set W) → ℝ) (C : Set (Set W)) (x : E) (p : Set W) (w : W) :
                            Preferential.degreeComparison μ θ C x {p} w ↔ p ∈ Preferential.preferred μ θ C x w

                            Composed with the highlighted content of whether p, the singleton of the radical, a degree-comparison predicate means its declarative (70). This first candidate analysis (§4.2) yields the interpretive asymmetry but not the inquisitive implication.

                            source
                            def QingEtAl2025.HopefulGoals {V : Type u_3} (φ Bφ : V → Prop) (G : Set (V → Prop)) :
                            Prop

                            The goals of a hopeful event whose agent hopes φ are φ or the agent's believing φ (89).

                            Equations
                            Instances For
                              source
                              theorem QingEtAl2025.hopes_radical {V : Type u_3} {Bp : V → Prop} {v₁ v₂ : V} (h₁ : Bp v₁) (h₂ : ¬Bp v₂) :
                              v₁ < v₂

                              When the agent hopes for the radical, with the goal of believing p, the outcome in which they come to believe p is strictly better than the one in which they do not, so the wondering meets Tabatowski's convention on asking whether p.

                              source
                              theorem QingEtAl2025.hopes_negation {V : Type u_3} {p Bnp : V → Prop} {v₁ v₂ : V} {G : Set (V → Prop)} (hG : HopefulGoals (fun (v : V) => ¬p v) Bnp G) (hp₁ : p v₁) (hn₁ : ¬Bnp v₁) :
                              ¬v₁ < v₂

                              When the agent hopes for the negation, whichever goal (89) allows, an outcome in which p holds and the agent does not believe ¬p satisfies neither ¬p nor believing ¬p, so coming to believe p is no better than not, and the wondering cannot be hopeful.

                              source
                              theorem QingEtAl2025.fears {V : Type u_3} {Bp Bnp : V → Prop} {v₁ v₂ : V} (h₁ : Bp v₁) (h₂ : ¬Bp v₂) (hn₂ : ¬Bnp v₂) :
                              v₁ < v₂

                              Fear constrains no goal (87). The purely epistemic goal of knowing whether p makes coming to believe p strictly better than remaining undecided, whichever answer is feared.

                              source
                              theorem QingEtAl2025.asymmetry_rows (r : Datum) :
                              r ∈ Examples.all → ∀ t ∈ r.feature? "target", ∀ v ∈ valence? r, (v = Degree.EvaluativeValence.positive → (Holds r ↔ t = "radical")) ∧ (v = Degree.EvaluativeValence.negative → Holds r)

                              In the polar cases a positive predicate or adverb holds exactly when the agent's attitude targets the radical, and a negative one holds either way. The rows are (45), (50), (62), (63), (75), (76), (78), and (79).