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_2 u_1)

    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 Hamblin Semantics #

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

        Questions are alternative sets. Our QuestionDen W is the extensional representation of Semantics.Questions.Hamblin.QuestionDen W.

        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 question 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:

        Convert our extensional question representation to Hamblin's intensional one.

        toHamblin [p₁, p₂, p₃] = λ p. p ∈ {p₁, p₂, p₃}

        Note: Equality of propositions is checked extensionally over a finite world list.

        Equations
        Instances For

          Convert Hamblin's intensional representation to our extensional one.

          Given a Hamblin question and a list of candidate propositions, returns those propositions that are answers to the question.

          Equations
          Instances For

            Representation Equivalence #

            For finite world sets, our List (BProp W) representation is equivalent to Hamblin's (W → Bool) → Bool. This theorem documents the isomorphism, enabling future extension to full intensional semantics if needed.

            The Equivalence #

            Given a finite set of worlds W and a finite set of propositions P:

            Why List is Sufficient for NVPs #

            For NVP semantics, we only need:

            1. Existential quantification over answers: ∃p ∈ Q. φ(p)
            2. Subset relations: Q ⊆ C
            3. TSP satisfaction: ∃p ∈ C. μ(x,p) > θ

            All of these work identically on List and Hamblin representations for finite cases.

            theorem Semantics.Attitudes.Preferential.roundtrip_preserves_membership {W : Type u_1} [BEq W] [DecidableEq (WBool)] (Q : QuestionDen W) (worlds : List W) (p : BProp W) (hp : p Q) :
            p fromHamblin (toHamblin Q worlds) Q

            Answerhood is preserved by round-trip conversion (List → Hamblin → List).

            For any proposition p in the original list Q, if we convert Q to Hamblin and back (using Q as candidates), p remains an answer.

            This shows the List representation loses no information for finite questions.

            theorem Semantics.Attitudes.Preferential.exists_equiv_any {W : Type u_1} (Q : QuestionDen W) (φ : BProp WBool) :
            (∃ 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 : QuestionDen W) (φ : BProp WBool) (h_subset : questionSubset Q C) (h_exists_Q : List.any Q φ = true) :

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

              Evaluative valence of a preferential predicate.

              • Positive: Expresses desire for the proposition (hope, wish, expect)
              • Negative: Expresses aversion to the proposition (fear, worry, dread)

              This distinction is crucial for:

              1. TSP distribution (positive have TSP, negative don't)
              2. Interpretive asymmetry in "V whether" constructions
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  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
                    Equations
                    • One or more equations did not get rendered due to their size.
                    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 : QuestionDen W) :

                        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.

                            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 is C-distributive (PROVED from its semantics)

                                      Fear is C-distributive (PROVED from its semantics)

                                      Expect is C-distributive

                                      Wish is C-distributive

                                      Dread is C-distributive

                                      def Semantics.Attitudes.Preferential.worry {W : Type u_1} {E : Type u_2} (μ : PreferenceFunction W E) (θ : ThresholdFunction W) (isUncertain : EQuestionDen 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 : EQuestionDen WBool) (x : E) (Q C : QuestionDen 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 : EQuestionDen 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
                                            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 : QuestionDen 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 : QuestionDen 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 : QuestionDen W) (h_subset : pC, p Q) (h_tsp : tspSatisfied μ θ x 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 : QuestionDen 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

                                                  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 : QuestionDen 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 : QuestionDen 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 : QuestionDen 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 : QuestionDen 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 : QuestionDen 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 : QuestionDen 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

                                                                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 : BProp W) (C : QuestionDen W) :

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

                                                                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 : QuestionDen W) (h_subset : pQ, p C) (h_assert : hopeHighlightSemantics μ θ ClauseType.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".