Documentation

Linglib.Theories.Semantics.Attitudes.RationalAttitude

Rational Attitude Semantics @cite{fusco-sgrizzi-2026} #

@cite{dowty-1979}

Unified semantics for attitude verbs that support both belief and intention readings. The key insight: these are not two separate verb types but a single verb whose interpretation is determined by complement structure.

Core Idea #

A rational attitude is a mental state that can be either:

The difference is determined by complement size:

Denotation (@cite{fusco-sgrizzi-2026}, ex. 24) #

⟦convincere⟧ = λP.λx.λy.λe. ∃e'. Convince(e) ∧ Agent(e,y) ∧ Patient(e,x) ∧ CAUSE(e,e') ∧ RATIONAL-ATTITUDE(e') ∧ Experiencer(x,e') ∧ P(e')

The parameter P is determined by complement size:

The two readings of a rational attitude verb, determined by complement size.

  • belief: complement is propositional (existentially closed by CLOSURE); evaluated via CONTENT modal base (doxastic alternatives)
  • intention: complement is sub-propositional (event variable open); evaluated via INERTIA modal base (normal continuation)
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      Map complement size to rational attitude reading.

      CP-sized complements (fLevel ≥ 6) trigger CLOSURE, yielding a propositional content suitable for belief evaluation. Sub-CP complements leave the event variable unsaturated, producing an intention reading via INERTIA.

      Equations
      Instances For

        Complement size determines reading: CP boundary is the threshold. This formalizes Fusco & Sgrizzi's structural size hypothesis.

        @[reducible, inline]
        abbrev Semantics.Attitudes.RationalAttitude.closure {W : Type u_1} {Time : Type u_2} [LE Time] (P : Events.EvPredW W Time) :
        WProp

        CLOSURE: existential closure of the event variable at the CP level.

        For CP complements, CLOSURE converts an event predicate P(e) into a proposition ∃e. P(e), yielding a belief-compatible propositional content.

        This is existsClosureW from event semantics, re-exported under the name used in @cite{fusco-sgrizzi-2026}.

        Equations
        Instances For
          structure Semantics.Attitudes.RationalAttitude.CausativeAttitude (E : Type u_1) (Time : Type u_2) [LE Time] :
          Type (max u_1 u_2)

          A causative attitude verb: Agent causes Experiencer to enter a rational attitude state whose content is determined by complement P.

          ⟦convincere⟧ = λP.λx.λy.λe. ∃e'. VerbPred(e) ∧ Agent(e,y) ∧ Patient(e,x) ∧ CAUSE(e,e') ∧ RATIONAL-ATTITUDE(e') ∧ Experiencer(x,e') ∧ P(e')

          The parameter P is supplied by the complement:

          • CP (di): CLOSURE applied → P is propositional (belief)
          • Sub-CP (a): P is an event predicate (intention)
          • verbPred : Events.Ev TimeProp

            The verb's descriptive predicate (e.g., Convince)

          • agent : E

            The agent of the matrix event

          • experiencer : E

            The patient/experiencer who enters the attitude

          • isAgent : Events.Ev TimeEProp

            Agent thematic role

          • isPatient : Events.Ev TimeEProp

            Patient thematic role

          • isExperiencer : Events.Ev TimeEProp

            Experiencer thematic role (on the attitude event)

          • cause : Events.Ev TimeEvents.Ev TimeProp

            CAUSE(e, e'): the matrix event e causally brings about the attitude state e'. Abstract relation; instantiated per verb/scenario.

          Instances For
            def Semantics.Attitudes.RationalAttitude.CausativeAttitude.denote {E : Type u_1} {Time : Type u_2} [LE Time] (v : CausativeAttitude E Time) (P : Events.Ev TimeProp) :

            Semantics of a causative attitude verb applied to complement P.

            Returns a proposition existentially closed over both the matrix event and the resulting attitude event.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              def Semantics.Attitudes.RationalAttitude.CausativeAttitude.beliefReading {E : Type u_1} {Time : Type u_2} [LE Time] (v : CausativeAttitude E Time) (embeddedVP : Events.Ev TimeProp) :

              Belief reading: CLOSURE applies to the embedded VP, yielding a proposition. The attitude is evaluated via CONTENT (doxastic alternatives).

              Equations
              Instances For
                def Semantics.Attitudes.RationalAttitude.CausativeAttitude.intentionReading {E : Type u_1} {Time : Type u_2} [LE Time] (v : CausativeAttitude E Time) (embeddedVP : Events.Ev TimeProp) :

                Intention reading: no CLOSURE — the embedded VP is applied directly as an event predicate. The attitude is evaluated via INERTIA.

                Equations
                Instances For
                  theorem Semantics.Attitudes.RationalAttitude.CausativeAttitude.readings_from_single_denote {E : Type u_1} {Time : Type u_2} [LE Time] (v : CausativeAttitude E Time) (VP : Events.Ev TimeProp) :
                  (v.beliefReading VP = v.denote fun (x : Events.Ev Time) => ∃ (e : Events.Ev Time), VP e) v.intentionReading VP = v.denote VP

                  Both readings are instances of the same denote applied to different P. This is the paper's central formal claim (ex. 24): convincere has ONE denotation; the belief/intention split is compositional, arising from complement size (CP triggers CLOSURE, sub-CP does not).

                  @[reducible, inline]
                  abbrev Semantics.Attitudes.RationalAttitude.CauseStar (W : Type u_1) (Time : Type u_2) [LE Time] :
                  Type (max u_1 u_2)

                  CAUSE*(s, e, w): causal self-reference relation (@cite{grano-2024}, (79); @cite{searle-1983}).

                  The attitude state s causally brings about event e in world w "in the right way." Distinguished from plain CAUSE by requiring that the causation proceed via the agent's intention-in-action, not via a deviant causal chain (Harman 1976; Chisholm 1966).

                  Example (Harman): Betty aims her gun intending to kill the target. Her intention makes her nervous; nervousness causes her to pull the trigger; the target is killed. The outcome was caused by the intention, but not "in the right way" — the causal chain was deviant. CAUSE* would not hold, correctly predicting that Betty did not carry out her intention.

                  Equations
                  Instances For
                    def Semantics.Attitudes.RationalAttitude.intentionHolds {E : Type u_1} {W : Type u_2} {Time : Type u_3} [LE Time] (isIntention : Events.Ev TimeWProp) (holder : EEvents.Ev TimeWProp) (content : Events.Ev TimeSet (W × E)) (causeStar : CauseStar W Time) (agent : E) (P : EWEvents.Ev TimeProp) (w : W) :

                    Semantics for intention reports with causal self-reference (@cite{grano-2024}, version 4, (79)).

                    ⟦Kim intends to leave⟧ᵂ·ᵗ = ∃s. INTENTION(s,w) ∧ HOLDER(k,s,w) ∧ ∀⟨w',x⟩ ∈ CONTENT(s): ∃e. CAUSE*(s,e,w') ∧ P(x,w',e)

                    The complement P has type (E → W → Ev Time → Prop) — an event predicate with an open eventuality argument. This is the formal correlate of @cite{grano-2024}'s Premise 3: IND would existentially close the event argument, yielding (E → W → Prop), which is type-incompatible with CAUSE*. The type system enforces that intention reports require eventuality abstraction.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      def Semantics.Attitudes.RationalAttitude.beliefHolds {E : Type u_1} {W : Type u_2} (dox : EWSet W) (agent : E) (P : WProp) (w : W) :

                      Plain belief reports do NOT require CAUSE*: the complement is a proposition (event argument already closed by IND), so there is no event for CAUSE* to bind.

                      ⟦Kim believes that Sandy left⟧ᵂ = ∀w' ∈ DOX(k,w): P(w')

                      The contrast in complement type — (W → Prop) for belief vs (E → W → Ev Time → Prop) for intention — is what makes 'believe' indicative-selecting and 'intend' subjunctive-selecting.

                      Equations
                      Instances For

                        Premise 3: Type-Level Enforcement (@cite{grano-2024}, §4.3) #

                        Intention reports require eventuality abstraction: intentionHolds demands a complement with an open event argument (P : E → W → Ev Time → Prop), while beliefHolds takes a closed proposition (P : W → Prop).

                        Indicative mood existentially closes the event argument ((87)), yielding W → Prop, which is type-incompatible with intentionHolds. Only subjunctive/nonfinite clauses leave the event argument open, enabling the E → W → Ev Time → Prop type that CAUSE* requires.

                        The distinction is enforced by construction — no theorem is needed because you literally cannot pass a W → Prop where E → W → Ev Time → Prop is expected. The Lean type checker is the proof.

                        Modal auxiliaries can appear in CP complements (belief) but not in sub-CP complements (intention). The CP provides the structural space to host modal heads (Mod, F-level 2).

                        Equations
                        Instances For

                          Intention readings are obligatorily future-oriented: the intended event is projected into inertia worlds (future continuation). Belief readings have no temporal constraint (they can be about past, present, or future).

                          Equations
                          Instances For

                            Object control is obligatory for intention readings: the experiencer must be the agent of the intended event. Belief readings allow both subject and object control configurations.

                            Equations
                            Instances For

                              Map rational attitude readings to @cite{searle-1983}'s direction of fit.

                              Belief readings have mind-to-world fit: the propositional content must match independently existing reality. Intention readings have world-to-mind fit: reality must be changed to match the content.

                              Equations
                              Instances For

                                Map rational attitude readings to @cite{searle-1983}'s psychological mode.

                                This connects @cite{fusco-sgrizzi-2026}'s complement-size analysis to Searle's theory of Intentional states: the same verb produces different psychological modes depending on syntactic complement structure.

                                Equations
                                Instances For

                                  The direction of fit derived from the reading matches the direction derived from the corresponding psychological mode.

                                  Belief readings are not causally self-referential; intention readings are. This is the formal correlate of @cite{fusco-sgrizzi-2026}'s CONTENT vs INERTIA modal base distinction: INERTIA worlds are those where the agent's intentions cause the events to come about.