Maier (2015), Parasitic Attitudes

[Mai15]'s solution to the [Kar73] attitude-projection puzzle, formalized as Maier actually states it: a DRT mechanism, not a world-accessibility abstraction — now over the faithful model-theoretic DRS core (Semantics/Dynamic/DRS/).

The puzzle

[Kar73] (ex. 42) observed that

"Bill believed Fred had been beating his wife and he hoped Fred would stop"

does not presuppose, for the speaker, that Fred was beating his wife — the presupposition of stop is filtered by the preceding belief. The asymmetry is sharpest with the additive trigger too (Maier's (7a)/(7b)): belief-then-hope filters, hope-then-belief does not.

Maier's mechanism (what this file models)

Maier represents an agent's mental state as a single DRS: a global belief layer K_BEL with labeled non-doxastic compartments (DES, IMG, INT) embedded inside it (his (26), (32)). By the standard DRT accessibility (subordination) relation, discourse referents introduced in the belief layer are accessible from an embedded desire compartment, but referents introduced inside the desire compartment are not accessible to the belief layer. That is the parasitism — realized purely structurally (the labels are not intensional operators; Maier fn. 11). Karttunen's puzzle is then solved by two operations (his §5): a sequence of same-agent attitude ascriptions is merged into one mental-state description (his (58)), after which the presupposition triggered in the desire compartment binds ([vdS92] presupposition-as-anaphora) to the now-accessible believed event (his (59)→(60)), rather than projecting.

Main declarations

• MentalState, MentalState.flatten — a belief layer with embedded labeled compartments, flattened to a DRS maierLang ℕ.
• parasitic_asymmetry / presup_binds_after_merge — the core's decidable DRS.Accessible gives Maier's accessibility asymmetry; the believed event becomes an accessible antecedent for the desire-compartment presupposition only after merge.
• MentalState.merge — Maier's attitude-merge (his (58)).
• MentalState.bind — presupposition resolution by renaming to an accessible antecedent (via the core's functorial Condition.map).
• presup_resolved_after_binding — the worked Karttunen derivation ((53)→(60)) resolves the cheating presupposition by binding (filtered, not projected).

Substrate fit (what the faithful core does and does not provide)

• Accessibility / occurrence. DRS.Accessible/DRS.accessibleFrom and DRS.occ (DRS/Basic.lean) are decidable, host-relative, and reproduce Maier's parasitic asymmetry — the four theorems below are decided against them. (DRS.Accessible is the fixed notion: an earlier host-free ∃-over- superordinates formulation was vacuous.)
• Gap 1 — labeled attitude compartment. Standard DRT (the core) has no labeled / operator-free embedded-box condition (Maier fn. 11: DES is a label, not an operator). Modeled paper-locally via MentalState/Compartment; flatten uses neg purely as a subordination device — accScope descends into any complex condition identically, so the accessibility geometry the theorems test is exactly Maier's, while neg's truth-semantics is immaterial (Maier gives the labels no extensional truth-conditions; gap 4).
• Gap 2 — attitude-merge. The core merge/toRel_merge is flat conjunction; Maier's belief-and-like-mode-compartment merge (his (58)) is MentalState.merge.
• Gap 3 — presupposition binding. Renaming is the core's Condition.map (capture-free since the DRSs are proper — no bespoke capture-aware rename, the mathlib relabel/subst discipline). The van der Sandt bind-vs-accommodate choice remains paper-local (bind-only, antecedent supplied by hand).
• Gap 4 — intensional model semantics. The core is extensional first-order DRT; Maier's contexts (Lewisian de se triples), Dox/Bul*, indexical anchors and capture conditions (his (33)/(36)/(37)) are documented, not built. The structural mechanism is modeled.

Empirical projection facts

structure Maier2015.AttitudeSequenceJudgment : Type

A recorded judgment about an attitude-sequence sentence: whether the embedded presupposition projects to the speaker, whether it is attributed to the attitude holder, and whether the sentence is acceptable.

• sentence : String

  The sentence being judged.

• presupProjectsToSpeaker : Bool

  Does the presupposition project to the speaker?

• presupProjectsToHolder : Bool

  Is the presupposition attributed to the attitude holder?

• acceptable : Bool

  Is the sentence acceptable?

def Maier2015.instReprAttitudeSequenceJudgment.repr : AttitudeSequenceJudgment → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Maier2015.instReprAttitudeSequenceJudgment : Repr AttitudeSequenceJudgment

Equations

• Maier2015.instReprAttitudeSequenceJudgment = { reprPrec := Maier2015.instReprAttitudeSequenceJudgment.repr }

def Maier2015.believeHopeFiltering : AttitudeSequenceJudgment

Karttunen's puzzle (ex. 42): a believe-then-hope sequence filters the presupposition of stop, which therefore does not project to the speaker.

Equations

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

def Maier2015.believeHopeTooFiltering : AttitudeSequenceJudgment

Maier's (7a): belief-then-hope filters the too-presupposition, so the discourse is felicitous.

Equations

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

def Maier2015.hopeBelieveNoFiltering : AttitudeSequenceJudgment

Maier's (7b): hope-then-belief does not filter the too-presupposition, which projects and renders the discourse infelicitous. The contrast with (7a) is the asymmetry the parasitic account explains.

Equations

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

def Maier2015.believeImagineFiltering : AttitudeSequenceJudgment

Maier's (22a): the asymmetry extends to purely representational attitudes (imagine/dream) lacking a preference component — belief-then-imagine filters.

Equations

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

def Maier2015.imagineBelieveNoFiltering : AttitudeSequenceJudgment

Maier's (22b): the reverse order (imagine-then-believe) does not filter.

Equations

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

def Maier2015.allJudgments : List AttitudeSequenceJudgment

All empirical judgments collected in this module.

Equations

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

def Maier2015.filteringCases : List AttitudeSequenceJudgment

The filtering cases: a doxastic attitude precedes a parasitic one.

Equations

• Maier2015.filteringCases = [Maier2015.believeHopeFiltering, Maier2015.believeHopeTooFiltering, Maier2015.believeImagineFiltering]

def Maier2015.nonFilteringCases : List AttitudeSequenceJudgment

The non-filtering cases: a parasitic attitude precedes a doxastic one.

Equations

• Maier2015.nonFilteringCases = [Maier2015.hopeBelieveNoFiltering, Maier2015.imagineBelieveNoFiltering]

theorem Maier2015.projection_asymmetry_data : (filteringCases.all fun (x : AttitudeSequenceJudgment) => x.presupProjectsToSpeaker == false) = true ∧ (nonFilteringCases.all fun (x : AttitudeSequenceJudgment) => x.presupProjectsToSpeaker == true) = true

In every filtering case the presupposition stays off the speaker; in every non-filtering case it projects. This is the asymmetry the mechanism below derives.

The DRS language of the Karttunen example (Maier §5.3)

inductive Maier2015.MaierRel : ℕ → Type

Relations of the Karttunen example: sue/jane (1-ary), husband (2-ary, husband(h, j)), event-style cheat(e, j, h) (3-ary, event + cheater + victim), stop(j, e') (2-ary, agent + event).

• sue : MaierRel 1
• jane : MaierRel 1
• husband : MaierRel 2
• cheat : MaierRel 3
• stop : MaierRel 2

def Maier2015.maierLang : FirstOrder.Language

The first-order language of the example (no functions).

Equations

• Maier2015.maierLang = { Functions := fun (x : ℕ) => Empty, Relations := Maier2015.MaierRel }

@[reducible, inline]

abbrev Maier2015.MCond : Type

Conditions over maierLang with ℕ discourse referents.

Equations

• Maier2015.MCond = DRT.Condition Maier2015.maierLang ℕ

Mental-state descriptions (Maier §3.1)

inductive Maier2015.AttMode : Type

Attitude-mode labels for non-doxastic compartments. Per Maier (fn. 11) these are labels, not intensional operators — they do not affect DRT accessibility, only which compartment an ascription contributes to under merge.

• des : AttMode
• imgn : AttMode
• int : AttMode

@[implicit_reducible]

instance Maier2015.instDecidableEqAttMode : DecidableEq AttMode

Equations

• Maier2015.instDecidableEqAttMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Maier2015.instReprAttMode : Repr AttMode

Equations

• Maier2015.instReprAttMode = { reprPrec := Maier2015.instReprAttMode.repr }

def Maier2015.instReprAttMode.repr : AttMode → ℕ → Std.Format

Equations

• Maier2015.instReprAttMode.repr Maier2015.AttMode.des prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Maier2015.AttMode.des")).group prec✝
• Maier2015.instReprAttMode.repr Maier2015.AttMode.imgn prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Maier2015.AttMode.imgn")).group prec✝
• Maier2015.instReprAttMode.repr Maier2015.AttMode.int prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Maier2015.AttMode.int")).group prec✝

def Maier2015.instBEqAttMode.beq : AttMode → AttMode → Bool

Equations

• Maier2015.instBEqAttMode.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Maier2015.instBEqAttMode : BEq AttMode

Equations

• Maier2015.instBEqAttMode = { beq := Maier2015.instBEqAttMode.beq }

structure Maier2015.Compartment : Type

A labeled non-doxastic compartment: an embedded sub-DRS (its own discourse referents and conditions) under an attitude-mode label.

• mode : AttMode
• drefs : List ℕ
• conds : List MCond

structure Maier2015.MentalState : Type

Maier's mental-state description: a global belief layer (discourse referents

• conditions) with embedded labeled compartments. Mirrors his (32) K = K_BEL with DES-K_DES embedded.

• beliefDrefs : List ℕ
• beliefConds : List MCond
• compartments : List Compartment

def Maier2015.MentalState.flatten (K : MentalState) : DRT.DRS maierLang ℕ

Flatten a mental state to a single DRS maierLang ℕ: the belief box containing the belief conditions plus, for each compartment, a subordinate sub-box. Because each compartment is embedded inside the belief box, the core's accessibleFrom makes belief referents accessible from a compartment but not conversely — Maier's parasitism, for free.

Standard DRT (the core) has no labeled / operator-free embedded-box condition (Maier fn. 11), so neg stands in purely as the subordination device: accScope descends into any complex condition identically, so the accessibility geometry the theorems test is exactly Maier's; neg's truth-semantics is immaterial here.

Equations

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

Attitude merge (Maier §5.2, (58))

def Maier2015.Compartment.append (c c' : Compartment) : Compartment

Append one compartment's content into another of the same mode.

Equations

• c.append c' = { mode := c.mode, drefs := c.drefs ++ c'.drefs, conds := c.conds ++ c'.conds }

def Maier2015.mergeCompartments (cs cs' : List Compartment) : List Compartment

Merge two compartment lists by attitude mode: like-mode compartments are combined, others carried over.

Equations

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

def Maier2015.MentalState.merge (K K' : MentalState) : MentalState

Maier's attitude-merge (his (58)): combine two partial descriptions of one agent's mental state by merging the belief layers and merging like-mode compartments. The core's merge is flat concatenation (gap 2); this respects the belief/compartment structure.

Equations

• K.merge K' = { beliefDrefs := K.beliefDrefs ++ K'.beliefDrefs, beliefConds := K.beliefConds ++ K'.beliefConds, compartments := Maier2015.mergeCompartments K.compartments K'.compartments }

Presupposition binding (Maier §4.2, van der Sandt)

def Maier2015.MentalState.bind (presup antecedent : ℕ) (K : MentalState) : MentalState

Resolve a presupposition by binding its referent presup to an accessible antecedent: drop presup from the universes and rename it to antecedent throughout, via the core's functorial Condition.map (capture-free since the DRS is proper). Licensed only when antecedent is accessible from presup (checked separately via DRS.Accessible).

Equations

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

Solving Karttunen's puzzle (Maier §5.3, (53)–(60))

"Sue thinks that Jane has been cheating on her husband. She hopes that Jane will stop cheating on him." Referents: s = 10, j = 11, h = 12, e = 20 (the believed cheating event), e' = 21 (the cheating event presupposed by stop).

def Maier2015.sueBelief : MentalState

After sentence 1: Sue believes there is a cheating event e (Maier (59), belief layer).

Equations

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

def Maier2015.sueHope : MentalState

After sentence 2 (in isolation): Sue's desire compartment contains stop(j, e') and the presupposed cheating event e', with no belief-layer antecedent of its own.

Equations

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

def Maier2015.sueMerged : MentalState

The two ascriptions merged into one mental-state description (Maier (59)).

Equations

• Maier2015.sueMerged = Maier2015.sueBelief.merge Maier2015.sueHope

def Maier2015.sueBound : MentalState

The merged description after binding the presupposed event e' to the believed event e (Maier (60)).

Equations

• Maier2015.sueBound = Maier2015.MentalState.bind 21 20 Maier2015.sueMerged

theorem Maier2015.believed_event_absent_before_merge : 20 ∉ sueHope.flatten.occ

Before merge, the believed cheating event does not even occur in the lone hope description, so the stop presupposition has no antecedent to bind to — only (dispreferred) accommodation is available.

theorem Maier2015.presup_binds_after_merge : sueMerged.flatten.Accessible 21 20

After merge, the believed cheating event e (20) is accessible from the desire-compartment presupposition e' (21): binding e' = e is licensed. This is the filtering, reusing the core's DRS.Accessible unchanged.

theorem Maier2015.parasitic_asymmetry : ¬sueMerged.flatten.Accessible 20 21

The dependence is asymmetric (Maier §3.1, fn. 11): the believed event in the belief layer does not see the desire-compartment referent. Belief can filter desire's presupposition, not conversely.

theorem Maier2015.presup_resolved_after_binding : 21 ∉ sueBound.flatten.occ ∧ 20 ∈ sueBound.flatten.occ

After binding, the presupposed cheating referent e' (21) no longer occurs: it has been identified with the believed event e (20), so the presupposition is resolved by binding (filtered), not accommodated or projected (Maier's (60)).