Documentation

Linglib.Theories.Semantics.Attitudes.Preferential

@[reducible, inline]

Question denotation: set of possible answers. Re-exported from CDistributivity.

Equations
Instances For
    @[reducible, inline]
    abbrev Semantics.Attitudes.Preferential.PreferenceFunction (W : Type u_1) (E : Type u_2) :
    Type (max u_1 u_2)

    Preference function: μ(agent, prop) → degree. Alias for DegreeFn.

    Equations
    Instances For
      @[reducible, inline]

      Threshold function: θ(comparison_class) → degree. Alias for ThresholdFn.

      Equations
      Instances For

        Grounding in Question Semantics #

        @cite{uegaki-sudo-2019} @cite{villalta-2008} @cite{rooth-1992} @cite{qing-uegaki-2025}

        Questions are alternative sets. Our AlternativeList W is the extensional, list-based representation of question denotations used by the C-distributivity machinery (still Bool-shaped pending a follow-up migration of Semantics.Attitudes.CDistributivity to substrate-aligned Set propositions).

        Why This Matters for TSP #

        @cite{uegaki-sudo-2019} derive TSP from the interaction of:

        1. Degree semantics (μ(x,p) > θ) — from @cite{villalta-2008}
        2. Alternative semantics (questions as Hamblin sets) — from @cite{hamblin-1973b}
        3. Focus-induced presuppositions — from @cite{rooth-1992}

        The key insight: questions introduce alternatives, and combining a degree predicate with alternatives triggers significance presuppositions.

        The Derivation Chain #

        Hamblin alternative set Q = {p₁, p₂,...} [@cite{hamblin-1973b}]
                ↓
        Alternatives trigger focus semantics [@cite{rooth-1992}]
                ↓
        Focus triggers significance presup [@cite{kennedy-2007}]
                ↓
        For positive valence: significance = ∃p ∈ C. μ(x,p) > θ = TSP
        

        Rooth Integration (see Focus/Sensitivity.lean) #

        The compositional chain from focus marking to TSP is now explicit:

        theorem Semantics.Attitudes.Preferential.exists_equiv_any {W : Type u_1} (Q : AlternativeList W) (φ : (WBool)Bool) :
        (∃ pQ, φ p = true) List.any Q φ = true

        Key semantic operations are equivalent across representations.

        The existential quantification ∃p ∈ Q. φ(p) that appears in:

        • C-distributivity: V x Q C ↔ ∃p ∈ Q. V x p C
        • TSP: ∃p ∈ C. μ(x,p) > θ(C)

        works identically on List (via List.any) and Hamblin (via function application to the characteristic function of answers satisfying φ).

        Subset relations are preserved.

        Q ⊆ C (all answers to Q are in comparison class C) is the same whether we use List containment or Hamblin entailment.

        Equations
        Instances For
          theorem Semantics.Attitudes.Preferential.triviality_representation_independent {W : Type u_1} (Q C : AlternativeList W) (φ : (WBool)Bool) (h_subset : questionSubset Q C) (h_exists_Q : List.any Q φ = true) :
          List.any C φ = true

          The triviality condition uses subset + existential, both of which are representation-independent for finite cases.

          Deriving TSP from Degree Semantics #

          Background: Significance in Degree Constructions #

          @cite{kennedy-2007} observes that degree constructions carry significance presuppositions. The positive form of a gradable adjective presupposes the scale is "significant" in context:

          "John is tall" presupposes height is relevant/significant

          Application to Preferential Predicates #

          @cite{villalta-2008} shows preferential predicates ARE gradable predicates with degree semantics:

          ⟦x hopes p⟧ = μ_hope(x, p) > θ(C)

          As degree constructions, they inherit significance presuppositions. But the CONTENT of "significance" differs by valence:

          Positive Valence (hope, wish, expect) #

          For predicates expressing desires/goals:

          Negative Valence (fear, dread) #

          For predicates expressing aversions/threats:

          Why the Asymmetry? #

          The key insight (@cite{uegaki-sudo-2019}): Positive predicates express bouletic goals — states the agent wants to achieve. Goals inherently presuppose there's something desirable.

          Negative predicates express threats — states to avoid. Threats don't require a symmetric positive goal. "I fear the worst" doesn't presuppose "I desire something."

          Consequence for Anti-Rogativity #

          Only TSP (positive significance) creates triviality with questions:

          Negative predicates lack TSP, so no triviality, so they CAN take questions.

          Significance presupposition content varies by valence.

          This captures the insight that ALL degree predicates have significance presuppositions, but the content differs:

          • Positive: presupposes desired alternative exists (= TSP)
          • Negative: presupposes threat identified (weaker, different structure)
          • desiredExists : SignificanceContent

            Positive: ∃p ∈ C. μ(x,p) > θ — "something is desired" (= TSP)

          • threatIdentified : SignificanceContent

            Negative: threat identification — no symmetric existence presupposition

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

              Does this significance content yield TSP?

              TSP = presupposition that ∃p ∈ C. μ(x,p) > θ(C). Only desiredExists has this form.

              Equations
              Instances For

                TSP distribution DERIVED from valence via significance presuppositions.

                This theorem shows TSP is not stipulated — it follows from:

                1. Degree predicates have significance presuppositions (Kennedy)
                2. Significance content depends on valence (bouletic goals vs threats)
                3. Only positive valence yields TSP-type significance
                Equations
                Instances For
                  def Semantics.Attitudes.Preferential.tspSatisfied {W : Type u_1} {E : Type u_2} (μ : PreferenceFunction W E) (θ : ThresholdFunction W) (agent : E) (C : AlternativeList W) :
                  Bool

                  Check if TSP is satisfied for given parameters

                  Equations
                  Instances For

                    The significance presupposition for a degree predicate.

                    For positive valence, this is exactly TSP. For negative valence, this is the weaker threat-identification condition.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      structure Semantics.Attitudes.Preferential.PreferentialPredicate (W : Type u_1) (E : Type u_2) :
                      Type (max u_1 u_2)

                      A preferential attitude predicate with explicit semantics.

                      Each predicate defines:

                      C-distributivity is then a PROVABLE property, not a stipulated field.

                      • name : String

                        Name of the predicate

                      • veridical : Bool

                        Is the predicate veridical? (NVPs are non-veridical by definition)

                      • valence : AttitudeValence

                        Evaluative valence (positive/negative)

                      • Preference function μ

                      • Threshold function θ

                      • propSemantics : E(WBool)AlternativeList WBool

                        Propositional semantics: ⟦x V p⟧(C)

                      • questionSemantics : EAlternativeList WAlternativeList WBool

                        Question semantics: ⟦x V Q⟧(C)

                      Instances For

                        Does the predicate have TSP? Derived from valence.

                        Equations
                        Instances For

                          C-distributivity is a PROPERTY of a predicate's semantics, not a field.

                          A predicate V is C-distributive iff: ∀ x Q C, V.questionSemantics x Q C ↔ ∃p ∈ Q, V.propSemantics x p C

                          This must be PROVED for each predicate from its semantic definition.

                          Equations
                          Instances For

                            Boolean version for computation

                            Equations
                            Instances For

                              Build a degree-comparison predicate.

                              These have semantics:

                              • ⟦x V p⟧(C) = μ(x, p) > θ(C)
                              • ⟦x V Q⟧(C) = ∃p ∈ Q. μ(x, p) > θ(C)

                              C-distributivity follows AUTOMATICALLY from this structure.

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

                                Theorem: Degree-comparison predicates are C-distributive.

                                This is PROVED, not stipulated. The proof follows from the structure of the semantics: questionSemantics IS the existential over propSemantics.

                                Hope (preferential component): degree-comparison, positive valence. This captures the preference ordering from @cite{villalta-2008} — the component shared by all emotive doxastic analyses. For the full emotive doxastic semantics with doxastic + uncertainty + preference components (@cite{anand-hacquard-2013}), see hopeHybrid below.

                                Note: hope is structurally identical to want except for the name — both are positive-valence degree-comparison predicates. What distinguishes hope from want linguistically is the additional doxastic component (uncertainty condition, epistemic licensing) that hopeHybrid captures.

                                Equations
                                Instances For

                                  Hope is C-distributive (PROVED from its semantics)

                                  Fear (preferential component): degree-comparison, negative valence. Captures the preference ordering only. For the full emotive doxastic semantics with uncertainty condition, see fearHybrid below.

                                  Equations
                                  Instances For

                                    Fear is C-distributive (PROVED from its semantics)

                                    Expect is C-distributive

                                    Wish is C-distributive

                                    Dread is C-distributive

                                    Hope and wish have identical preference semantics — they differ only in name. @cite{anand-hacquard-2013}: what distinguishes hope from want/wish is the doxastic component (captured by hopeHybrid), not the preferential semantics.

                                    def Semantics.Attitudes.Preferential.worry {W : Type u_1} {E : Type u_2} (μ : PreferenceFunction W E) (θ : ThresholdFunction W) (isUncertain : EAlternativeList WBool) :

                                    Worry has DIFFERENT question semantics involving global uncertainty.

                                    ⟦x worries about Q⟧ ≠ ∃p ∈ Q. ⟦x worries about p⟧

                                    The question semantics involves uncertainty about WHICH answer is true, not just whether some answer satisfies the predicate.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      theorem Semantics.Attitudes.Preferential.worry_not_cDistributive {W : Type u_1} {E : Type u_2} [Inhabited W] (μ : PreferenceFunction W E) (θ : ThresholdFunction W) (isUncertain : EAlternativeList WBool) (x : E) (Q C : AlternativeList W) (h_uncertain_false : isUncertain x Q = false) (h_exists : pQ, decide (μ x p > θ C) = true) :
                                      ¬(worry μ θ isUncertain).isCDistributive

                                      Worry is NOT C-distributive when there's an uncertainty requirement.

                                      The question semantics requires global uncertainty, which is NOT reducible to existential quantification over propositional semantics.

                                      def Semantics.Attitudes.Preferential.qidai {W : Type u_1} {E : Type u_2} (μ : PreferenceFunction W E) (θ : ThresholdFunction W) (anticipatesResolution : EAlternativeList WBool) :

                                      Mandarin "qidai" (look forward to): positive but non-C-distributive.

                                      Like worry, it involves anticipation of RESOLUTION, not just existential over individual propositions.

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

                                        The three classes of Non-Veridical Preferential predicates.

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

                                            Classify an NVP. Note: this now requires knowing whether the predicate is C-distributive, which must be PROVED separately.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              theorem Semantics.Attitudes.Preferential.degreeComparison_triviality {W : Type u_1} {E : Type u_2} (name : String) (valence : AttitudeValence) (μ : PreferenceFunction W E) (θ : ThresholdFunction W) (x : E) (Q C : AlternativeList W) (h_subset : pQ, p C) (h_assert : (mkDegreeComparisonPredicate name valence μ θ).questionSemantics x Q C = true) :
                                              tspSatisfied μ θ x C = true

                                              Class 3 triviality for degree-comparison predicates specifically.

                                              Class 3 predicates (C-distributive + positive + TSP) yield trivial meanings when combined with questions. When Q ⊆ C:

                                              • Assertion: ∃p ∈ Q. μ(x,p) > θ(C)
                                              • Presupposition (TSP): ∃p ∈ C. μ(x,p) > θ(C)
                                              • Assertion ⊆ Presupposition → trivial!

                                              For predicates built with mkDegreeComparisonPredicate, we can prove that assertion implies presupposition when Q ⊆ C.

                                              theorem Semantics.Attitudes.Preferential.hope_triviality {W : Type u_1} {E : Type u_2} (μ : PreferenceFunction W E) (θ : ThresholdFunction W) (x : E) (Q C : AlternativeList W) (h_subset : pQ, p C) (h_assert : (hope μ θ).questionSemantics x Q C = true) :
                                              tspSatisfied μ θ x C = true

                                              Hope + question yields trivial meaning when Q ⊆ C

                                              theorem Semantics.Attitudes.Preferential.hope_triviality_reverse {W : Type u_1} {E : Type u_2} (μ : PreferenceFunction W E) (θ : ThresholdFunction W) (x : E) (Q C : AlternativeList W) (h_subset : pC, p Q) (h_tsp : tspSatisfied μ θ x C = true) :
                                              (hope μ θ).questionSemantics x Q C = true

                                              Reverse direction: TSP → assertion when C ⊆ Q.

                                              This is the other half of the triviality argument from @cite{uegaki-2022} §6.5.4: TSP says ∃p ∈ C. μ(x,p) > θ(C). When C ⊆ Q, this p is also in Q, so the assertion ∃p ∈ Q. μ(x,p) > θ(C) holds too.

                                              theorem Semantics.Attitudes.Preferential.hope_triviality_identity {W : Type u_1} {E : Type u_2} (μ : PreferenceFunction W E) (θ : ThresholdFunction W) (x : E) (Q : AlternativeList W) :
                                              (hope μ θ).questionSemantics x Q Q = tspSatisfied μ θ x Q

                                              Triviality identity: When C = Q, assertion ↔ TSP.

                                              This is the core of @cite{uegaki-2022} §6.5.4: the assertion of a non-veridical preferential with an interrogative complement is identical to its presupposition (TSP). Whenever TSP is satisfied (defined), the assertion is true; whenever TSP fails, the assertion is false. The meaning is L-analytic — its truth value is determined entirely by the presupposition, leaving no informative content. This is what @cite{gajewski-2002} identifies as the trigger for unacceptability.

                                              Veridical vs Non-Veridical Preferential Predicates #

                                              @cite{uegaki-sudo-2019} established a crucial distinction:

                                              Non-Veridical (hope) - TRIVIAL #

                                              Presup (TSP): ∃p ∈ C. μ(x,p) > θ(C)
                                              Assertion: ∃p ∈ Q. μ(x,p) > θ(C)
                                              When Q ⊆ C: Assertion ⊆ TSP → TRIVIAL
                                              

                                              Veridical (be happy) - NOT TRIVIAL #

                                              Presup: ∃p ∈ Q. p(w) ∧ μ(x,p) > θ(C)
                                              Assertion: ∃p ∈ Q. p(w) ∧ μ(x,p) > θ(C)
                                                                     ^^^^
                                                                     TRUTH REQUIREMENT breaks triviality!
                                              

                                              Even when Q ⊆ C, whether the assertion is true depends on WHICH answer p is TRUE in the actual world w. This is the key insight: veridicality breaks triviality because it adds a world-dependent constraint.

                                              The Deep Theorem (formalized below as veridical_breaks_triviality) #

                                              Triviality requires ALL THREE conditions:

                                              1. C-distributive
                                              2. Positive valence (TSP)
                                              3. Non-veridical

                                              If ANY condition fails, the predicate can embed questions:

                                              Examples #

                                              PredicateVeridicalC-DistValenceTSPTakes Q?Why
                                              hope+C-dist + TSP → trivial
                                              fear-No TSP
                                              worry-Non-C-dist
                                              be happy+Veridical breaks triviality!
                                              be surprised+Veridical breaks triviality!

                                              Build a veridical preferential predicate.

                                              Unlike non-veridical predicates, veridical ones require the complement proposition to be TRUE in the actual world:

                                              ⟦x is happy that p⟧(w, C) = p(w) ∧ μ(x, p) > θ(C) ⟦x is happy about Q⟧(w, C) = ∃p ∈ Q. p(w) ∧ μ(x, p) > θ(C)

                                              The truth requirement p(w) is what breaks triviality: even if TSP holds (some proposition is preferred), the assertion may be false because the TRUE answer in w might not be the preferred one.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                def Semantics.Attitudes.Preferential.PreferentialPredicate.propSemanticsAt {W : Type u_1} {E : Type u_2} (V : PreferentialPredicate W E) (x : E) (p : WBool) (C : AlternativeList W) (w : W) :
                                                Bool

                                                World-sensitive propositional semantics for veridical predicates.

                                                ⟦x V p⟧(w, C) = p(w) ∧ μ(x, p) > θ(C)

                                                The truth requirement p(w) is what distinguishes veridical from non-veridical.

                                                Equations
                                                Instances For

                                                  World-sensitive question semantics for veridical predicates.

                                                  ⟦x V Q⟧(w, C) = ∃p ∈ Q. p(w) ∧ μ(x, p) > θ(C)

                                                  For veridical predicates, the assertion requires some TRUE answer to be preferred.

                                                  Equations
                                                  Instances For
                                                    theorem Semantics.Attitudes.Preferential.nonveridical_worldIndependent {W : Type u_1} {E : Type u_2} (name : String) (valence : AttitudeValence) (μ : PreferenceFunction W E) (θ : ThresholdFunction W) (x : E) (Q C : AlternativeList W) (w₁ w₂ : W) :
                                                    (mkDegreeComparisonPredicate name valence μ θ).questionSemanticsAt x Q C w₁ = (mkDegreeComparisonPredicate name valence μ θ).questionSemanticsAt x Q C w₂

                                                    World-independence contrast: Non-veridical predicates have world-independent semantics (questionSemanticsAt ignores the world), while veridical predicates have world-dependent semantics. This is the structural basis for L-analyticity: for non-veridical predicates, assertion ⊆ presupposition holds at ALL worlds because the world variable doesn't appear.

                                                    "be surprised": veridical, positive valence (expectation-violation). Classified as positive following @cite{uegaki-sudo-2019}: the degree function measures how much the true answer exceeds the subject's expectations, a positive-direction evaluation.

                                                    Equations
                                                    Instances For
                                                      theorem Semantics.Attitudes.Preferential.veridical_breaks_triviality {W : Type u_1} {E : Type u_2} (name : String) (valence : AttitudeValence) (μ : PreferenceFunction W E) (θ : ThresholdFunction W) (x : E) (Q C : AlternativeList W) (w : W) (_h_subset : pQ, p C) (_h_tsp : tspSatisfied μ θ x C = true) (h_no_true_preferred : pQ, p w = truedecide (μ x p > θ C) = false) :
                                                      (mkVeridicalPreferential name valence μ θ).questionSemanticsAt x Q C w = false

                                                      Core Theorem: Veridicality breaks triviality.

                                                      Even when:

                                                      • TSP holds (some proposition is preferred above threshold)
                                                      • Q ⊆ C (question answers are in comparison class)

                                                      The question assertion can still be FALSE for veridical predicates, because no TRUE answer in w may be the preferred one.

                                                      This is the key insight from @cite{uegaki-sudo-2019}: non-veridicality is a NECESSARY condition for the triviality that makes predicates anti-rogative.

                                                      Proof Strategy #

                                                      We show that under the specified conditions:

                                                      1. TSP is satisfied (h_tsp)
                                                      2. But for every answer p in Q, if p is true in w, it's not preferred (h_no_true_preferred)
                                                      3. Therefore the question assertion is false

                                                      This proves that TSP satisfaction does NOT guarantee assertion truth for veridical predicates — the triviality derivation fails!

                                                      theorem Semantics.Attitudes.Preferential.nonveridical_is_trivial {W : Type u_1} {E : Type u_2} (μ : PreferenceFunction W E) (θ : ThresholdFunction W) (x : E) (Q C : AlternativeList W) (h_subset : pQ, p C) (h_assert : (hope μ θ).questionSemantics x Q C = true) :
                                                      tspSatisfied μ θ x C = true

                                                      Contrast Theorem: Non-veridical predicates ARE trivial.

                                                      When TSP holds and Q ⊆ C, the assertion is ALWAYS true for non-veridical C-distributive predicates. This is the triviality that makes them anti-rogative.

                                                      Combined with veridical_breaks_triviality, this shows the asymmetry:

                                                      • Non-veridical + C-dist + positive → trivial → anti-rogative
                                                      • Veridical + C-dist + positive → NOT trivial → responsive
                                                      theorem Semantics.Attitudes.Preferential.veridicalPreferential_isCDistributiveAt {W : Type u_1} {E : Type u_2} (name : String) (valence : AttitudeValence) (μ : PreferenceFunction W E) (θ : ThresholdFunction W) (x : E) (Q C : AlternativeList W) (w : W) :
                                                      (mkVeridicalPreferential name valence μ θ).questionSemanticsAt x Q C w = true pQ, (mkVeridicalPreferential name valence μ θ).propSemanticsAt x p C w = true

                                                      Veridical predicates ARE C-distributive (at a given world).

                                                      The world-sensitive semantics preserves the existential structure: ⟦x V Q⟧(w, C) = ∃p ∈ Q. ⟦x V p⟧(w, C)

                                                      Note: This is C-distributivity for the world-sensitive semantics, which is the relevant notion for veridical predicates.

                                                      theorem Semantics.Attitudes.Preferential.beHappy_isCDistributiveAt {W : Type u_1} {E : Type u_2} (μ : PreferenceFunction W E) (θ : ThresholdFunction W) (x : E) (Q C : AlternativeList W) (w : W) :
                                                      (beHappy μ θ).questionSemanticsAt x Q C w = true pQ, (beHappy μ θ).propSemanticsAt x p C w = true

                                                      beHappy is C-distributive (at a given world)

                                                      theorem Semantics.Attitudes.Preferential.beSurprised_isCDistributiveAt {W : Type u_1} {E : Type u_2} (μ : PreferenceFunction W E) (θ : ThresholdFunction W) (x : E) (Q C : AlternativeList W) (w : W) :
                                                      (beSurprised μ θ).questionSemanticsAt x Q C w = true pQ, (beSurprised μ θ).propSemanticsAt x p C w = true

                                                      beSurprised is C-distributive (at a given world)

                                                      The Triviality Conditions (@cite{uegaki-sudo-2019}) #

                                                      For a preferential predicate to be anti-rogative (unable to embed questions), ALL THREE conditions must hold:

                                                      1. C-distributive: ⟦x V Q⟧ ↔ ∃p ∈ Q. ⟦x V p⟧
                                                      2. Positive valence: Predicate has TSP (threshold significance presupposition)
                                                      3. Non-veridical: Truth of complement is NOT required

                                                      Why Each Condition is Necessary #

                                                      If not C-distributive (worry, qidai):

                                                      If negative valence (fear, dread):

                                                      If veridical (be happy, be surprised):

                                                      The Formalized Results #

                                                      Together, these theorems prove that non-veridicality is NECESSARY for the triviality derivation that creates anti-rogativity.

                                                      Main Results #

                                                      Proved Theorems (no axioms!): #

                                                      1. degreeComparisonPredicate_isCDistributive: Any predicate built with mkDegreeComparisonPredicate is C-distributive. This follows from the semantic structure: questionSemantics = ∃p ∈ Q. propSemantics.

                                                      2. hope_isCDistributive, fear_isCDistributive, expect_isCDistributive, wish_isCDistributive, dread_isCDistributive: C-distributivity for standard degree-comparison predicates (derived from #1).

                                                      3. worry_not_cDistributive: Worry with uncertainty requirement is NOT C-distributive. Proved by contradiction: global uncertainty breaks the equivalence.

                                                      4. degreeComparison_triviality / hope_triviality: Class 3 predicates yield trivial meanings with questions (assertion ⊆ presupposition when Q ⊆ C).

                                                      5. veridical_breaks_triviality (NEW): The core @cite{uegaki-sudo-2019} insight — veridical predicates break triviality because even when TSP holds, the assertion can be false (no TRUE answer is preferred).

                                                      6. veridicalPreferential_isCDistributiveAt: Veridical predicates preserve C-distributivity for their world-sensitive semantics.

                                                      Architecture: #

                                                      This gives genuine explanatory force: "hope" is anti-rogative BECAUSE its degree-comparison semantics makes it C-distributive, and combined with positive valence (TSP) and non-veridicality, this yields triviality.

                                                      "Be happy" takes questions DESPITE being C-distributive and positive BECAUSE it is veridical — the truth requirement breaks the triviality derivation.

                                                      Highlighted Propositions and hope-whether #

                                                      @cite{uegaki-2022} Ch 6 addresses apparent counterexamples to the anti-rogativity of positive NVPs: attested "hope whether" constructions (@cite{white-2021}).

                                                      The solution uses highlighting (@cite{pruitt-roelofsen-2011}): clauses have both an ordinary semantic value and a highlighted value — a subset of propositions with privileged status.

                                                      Key Insight #

                                                      When hope is sensitive to the highlighted value rather than the ordinary semantic value, hope whether p reduces to hope that p — no triviality! The anti-rogativity prediction is preserved for constituent interrogatives (highlighted value = full question = trivial) while allowing polar ones.

                                                      Clause types relevant to highlighting.

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

                                                          Highlighted propositions of a clause (@cite{pruitt-roelofsen-2011}).

                                                          • Polar interrogatives highlight the overtly-realized proposition (singleton)
                                                          • Declaratives highlight the asserted proposition (singleton)
                                                          • Constituent interrogatives highlight all alternatives (= ordinary value)

                                                          The key asymmetry: polar and declarative both yield singletons, while constituent interrogatives yield the full question.

                                                          Equations
                                                          Instances For

                                                            Highlighting-sensitive version of hope's denotation.

                                                            The Dayal-answer preferred by the subject is restricted to be a highlighted proposition of the complement φ, rather than a member of the ordinary semantic value.

                                                            ⟦hope_C φ⟧ = λx: ∃w'[AnsD_w'(⟦φ⟧_H) ∈ C] . ∃d ∈ { Pref_w(x,p) | p ∈ C } [d > θ(C)] . ∃w''[ AnsD_w''(Q) ∈ ⟦φ⟧_H ∧ Pref_w(x, AnsD_w''(Q)) > θ(C) ]

                                                            Equations
                                                            Instances For
                                                              theorem Semantics.Attitudes.Preferential.hope_highlight_declarative_equiv {W : Type u_1} {E : Type u_2} (μ : PreferenceFunction W E) (θ : ThresholdFunction W) (x : E) (p : WBool) (C : AlternativeList W) :
                                                              hopeHighlightSemantics μ θ HighlightingClauseType.declarative x [p] C = decide (μ x p > θ C)

                                                              With a declarative complement, highlighting changes nothing: the highlighted value is {p}, and hopeSemanticsHighlight reduces to whether μ(x, p) > θ(C). Same as standard hope.

                                                              theorem Semantics.Attitudes.Preferential.hope_highlight_polar_equiv {W : Type u_1} {E : Type u_2} (μ : PreferenceFunction W E) (θ : ThresholdFunction W) (x : E) (p neg_p : WBool) (C : AlternativeList W) :
                                                              hopeHighlightSemantics μ θ HighlightingClauseType.polarInterrogative x [p, neg_p] C = decide (μ x p > θ C)

                                                              With a polar interrogative "whether p", highlighting reduces to the singleton {p}. So "hope whether p" ≈ "hope that p" — NOT trivial.

                                                              theorem Semantics.Attitudes.Preferential.hope_highlight_constituent_equiv {W : Type u_1} {E : Type u_2} (μ : PreferenceFunction W E) (θ : ThresholdFunction W) (x : E) (Q C : AlternativeList W) :
                                                              hopeHighlightSemantics μ θ HighlightingClauseType.constituentInterrog x Q C = List.any Q fun (p : WBool) => decide (μ x p > θ C)

                                                              With a constituent interrogative "who V", all alternatives are highlighted. This is identical to the standard (non-highlighting) semantics — still trivial when combined with TSP and Q ⊆ C.

                                                              theorem Semantics.Attitudes.Preferential.hope_highlight_constituent_trivial {W : Type u_1} {E : Type u_2} (μ : PreferenceFunction W E) (θ : ThresholdFunction W) (x : E) (Q C : AlternativeList W) (h_subset : pQ, p C) (h_assert : hopeHighlightSemantics μ θ HighlightingClauseType.constituentInterrog x Q C = true) :
                                                              tspSatisfied μ θ x C = true

                                                              Constituent interrogatives with TSP are still trivial under highlighting. This preserves the anti-rogativity prediction for "*hope who left".

                                                              Emotive Doxastics: Hybrid Representational + Preferential #

                                                              @cite{anand-hacquard-2013} show that hope and fear are not pure preferential predicates (like want). They have three components:

                                                              1. Doxastic assertion: the attitude holder believes φ is possible (∃w' ∈ DOX: φ(w') = 1)
                                                              2. Preference assertion: φ-verifiers are preferred to φ-falsifiers
                                                              3. Uncertainty condition: the attitude holder is uncertain about φ (both φ-verifiers and φ-falsifiers exist in DOX)

                                                              The doxastic component is what licenses embedded epistemic possibility modals. The uncertainty condition is what blocks epistemic necessity: necessity entails certainty, contradicting the uncertainty requirement.

                                                              This hybrid structure distinguishes hope from want:

                                                              Evidence for the doxastic component (@cite{scheffler-2008}) #

                                                              hope can felicitously answer questions (providing doxastic information): A: "Is Peter coming today?" B: "I hope/*want that he is coming today."

                                                              hope is infelicitous with certainty about the complement: "It is raining. #I hope it is raining." (vs. ✓"I want it to be raining.")

                                                              Verifiers and Falsifiers #

                                                              @cite{anand-hacquard-2013} define φ-verifiers in information state S as subsets of S that are certain about φ — where φ's truth value doesn't change with (monotonically) increasing information:

                                                              φ-verifiers in S = {S' ⊂ S | ∀S'' ⊂ S': ∀w' ∈ S'': ⟦φ⟧(w') = 1}

                                                              For unmodalized φ, this simplifies to pow(S ∩ φ). For modalized φ (might p, must p), verifiers are still pow(S ∩ p) — modalized complements raise the same issue as unmodalized ones.

                                                              structure Semantics.Attitudes.Preferential.EmotiveDoxasticPredicate (W : Type u_1) (E : Type u_2) :
                                                              Type (max u_1 u_2)

                                                              An emotive doxastic predicate: hybrid representational + preferential.

                                                              Combines a doxastic accessibility relation (from Doxastic.lean) with a preference function (from Preferential). The accessibility relation provides the information state that epistemics quantify over; the preference function orders verifiers against falsifiers.

                                                              Instances For
                                                                def Semantics.Attitudes.Preferential.EmotiveDoxasticPredicate.doxasticAssertion {W : Type u_1} {E : Type u_2} (V : EmotiveDoxasticPredicate W E) (agent : E) (p : WProp) (w : W) (worlds : List W) :

                                                                The doxastic assertion: ∃w' ∈ DOX(x,w) such that φ(w').

                                                                This is the component that licenses embedded epistemic possibility modals. When the complement is might p, the doxastic assertion reduces to DOX ∩ p ≠ ∅ by vacuous quantification — identical to the unmodalized case.

                                                                Equations
                                                                Instances For
                                                                  def Semantics.Attitudes.Preferential.EmotiveDoxasticPredicate.uncertaintyCondition {W : Type u_1} {E : Type u_2} (V : EmotiveDoxasticPredicate W E) (agent : E) (p : WProp) (w : W) (worlds : List W) :

                                                                  The uncertainty condition: both φ-verifiers and φ-falsifiers exist in DOX. The attitude holder is genuinely uncertain about φ.

                                                                  This is what blocks epistemic necessity: must p under hope would require ∀w' ∈ DOX: p(w'), which combined with the uncertainty condition (∃w' ∈ DOX: ¬p(w')) yields a contradiction.

                                                                  Equations
                                                                  Instances For
                                                                    def Semantics.Attitudes.Preferential.EmotiveDoxasticPredicate.preferenceAssertion {W : Type u_1} {E : Type u_2} (V : EmotiveDoxasticPredicate W E) (agent : E) (p : WProp) [DecidablePred p] (C : AlternativeList W) :

                                                                    The preference assertion: φ-verifying doxastic alternatives are preferred to φ-falsifying ones.

                                                                    For positive valence (hope): μ(x, p) > θ(C) — the agent prefers p. For negative valence (fear): μ(x, p) > θ(C) — where μ measures dispreference.

                                                                    Equations
                                                                    Instances For
                                                                      def Semantics.Attitudes.Preferential.EmotiveDoxasticPredicate.holdsAt {W : Type u_1} {E : Type u_2} (V : EmotiveDoxasticPredicate W E) (agent : E) (p : WProp) [DecidablePred p] (w : W) (worlds : List W) (C : AlternativeList W) :

                                                                      Full semantics for an emotive doxastic: all three components must hold.

                                                                      ⟦a hopes_C that φ⟧ is defined iff: (i) φ-verifiers in S' ≠ ∅ ∧ φ-falsifiers in S' ≠ ∅ (uncertainty) (ii) ∃w' ∈ S': ⟦φ⟧(w') = 1 (doxastic) (iii) φ-verifiers >_DES φ-falsifiers (preference)

                                                                      where S' = DOX(a, w).

                                                                      Note: condition (ii) is entailed by the first conjunct of (i), so it is redundant in the conjunction. We include it explicitly for clarity and because it is the component responsible for epistemic licensing — it provides the information state that embedded epistemics are anaphoric to.

                                                                      Equations
                                                                      Instances For

                                                                        Hope: emotive doxastic with positive valence.

                                                                        Equations
                                                                        Instances For

                                                                          Fear: emotive doxastic with negative valence.

                                                                          Equations
                                                                          Instances For
                                                                            theorem Semantics.Attitudes.Preferential.doxastic_assertion_might_concord {W : Type u_1} {E : Type u_2} (V : EmotiveDoxasticPredicate W E) (agent : E) (p : WProp) (w : W) (worlds : List W) (h : V.doxasticAssertion agent p w worlds) :
                                                                            V.doxasticAssertion agent (fun (x : W) => Doxastic.diaAt V.access agent w worlds p) w worlds

                                                                            Under emotive doxastics, might p contributes the same doxastic assertion as bare p — modal concord.

                                                                            When the complement is might p, the doxastic assertion becomes: ∃w' ∈ DOX: (∃w'' ∈ DOX: p(w'')) By vacuous quantification over the shared information state, this reduces to: ∃w'' ∈ DOX: p(w''). Both yield: DOX ∩ p ≠ ∅.

                                                                            We model this by showing that the doxastic assertion for p and for the function λ w. diaAt R x w worlds p (= "might p" evaluated at the same DOX) are equivalent when the information state is shared.

                                                                            theorem Semantics.Attitudes.Preferential.must_contradicts_uncertainty {W : Type u_1} {E : Type u_2} (V : EmotiveDoxasticPredicate W E) (agent : E) (p : WProp) (w : W) (worlds : List W) (h_must : Doxastic.boxAt V.access agent w worlds p) :
                                                                            ¬V.uncertaintyCondition agent p w worlds

                                                                            Under emotive doxastics, must p contradicts the uncertainty condition. If ∀w' ∈ DOX: p(w'), then there are no falsifiers in DOX, violating the uncertainty condition's requirement that ∃w' ∈ DOX: ¬p(w').