Maier (2015): Parasitic Attitudes

This file formalizes Maier's solution to Karttunen's attitude-projection puzzle, Bill believed Fred had been beating his wife and he hoped Fred would stop, which does not presuppose for the speaker that Fred was beating his wife. An agent's mental state is one discourse representation, a belief layer with labelled non-doxastic compartments embedded in it (MentalState, MentalState.flatten), so a referent introduced in the belief layer is accessible from every compartment while a compartment's referents are visible nowhere else (accessible_belief_of_compartment, not_accessible_of_belief): the non-doxastic attitudes are parasitic on belief. A sequence of ascriptions to one agent merges into one description (MentalState.merge), after which a presupposition triggered in a desire compartment binds, in the manner of van der Sandt, to the believed event rather than projecting (MentalState.bind, presup_binds_after_merge, presup_resolved_after_binding), whereas one triggered in the belief layer after a desire finds no antecedent there and projects. That asymmetry is the paper's data: in the sequences of Data/Examples/Maier2015 the presupposition is filtered exactly when the doxastic ascription comes first (filtering_iff_doxastic_first).

Implementation notes

The compartment labels are structural, not intensional operators, so parasitism is the standard accessibility of the DRS core in Semantics/Dynamic/DRS, a compartment being a subordinate box; the core's negation is the subordination device, its truth conditions playing no role. The general accessibility lemmas assume the belief layer and the compartments hold atomic conditions, as every description in the paper does.

References

• [Mai15]
• [Kar73]
• [vdS92]

The DRS language of the Karttunen example (§5.3)

inductive Maier2015.MaierRel : ℕ → Type

The example's relations are sue and jane, husband(h, j), the event cheat(e, j, h), and stop(j, e').

• 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.

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 ℕ

def Maier2015.MCond.IsAtomic : MCond → Prop

A condition introducing no box.

Equations

• Maier2015.MCond.IsAtomic (DRT.Condition.atom a) = True
• Maier2015.MCond.IsAtomic (DRT.Condition.eq u v) = True
• x✝.IsAtomic = False

@[instance_reducible]

instance Maier2015.instDecidablePredMCondIsAtomic : DecidablePred MCond.IsAtomic

Equations

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

Mental-state descriptions (§3.1)

inductive Maier2015.AttMode : Type

The attitude modes of the non-doxastic compartments, desire, imagination and intention.

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

@[instance_reducible]

instance Maier2015.instDecidableEqAttMode : DecidableEq AttMode

Equations

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

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✝

@[instance_reducible]

instance Maier2015.instReprAttMode : Repr AttMode

Equations

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

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

Equations

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

@[instance_reducible]

instance Maier2015.instBEqAttMode : BEq AttMode

Equations

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

structure Maier2015.Compartment : Type

A non-doxastic compartment has its own referents and conditions under an attitude mode.

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

structure Maier2015.MentalState : Type

A mental-state description (32) is a belief layer with embedded compartments.

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

def Maier2015.Compartment.box (c : Compartment) : MCond

A compartment as a subordinate box.

Equations

• c.box = DRT.Condition.neg { referents := c.drefs.toFinset, conditions := c.conds }

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

A description flattens to the belief box with each compartment a subordinate box, so that accessibility runs from a compartment up to the belief layer and not back.

Equations

• K.flatten = { referents := K.beliefDrefs.toFinset, conditions := K.beliefConds ++ List.map Maier2015.Compartment.box K.compartments }

Parasitism as accessibility

theorem Maier2015.not_accessible_of_belief (K : MentalState) (hb : ∀ c ∈ K.beliefConds, c.IsAtomic) (hcs : ∀ c ∈ K.compartments, ∀ cd ∈ c.conds, cd.IsAtomic) {x y : ℕ} (hxc : ∀ c ∈ K.compartments, x ∉ c.drefs) (hy : y ∉ K.beliefDrefs) : ¬K.flatten.Accessible x y

The belief layer does not see a compartment. Where a belief referent is declared only belief referents are accessible, if no compartment declares it again.

theorem Maier2015.accessible_belief_of_compartment (K : MentalState) {x y : ℕ} (hx : x ∈ K.beliefDrefs) (hyc : ∃ c ∈ K.compartments, y ∈ c.drefs) : K.flatten.Accessible y x

A compartment sees the belief layer. Where a compartment declares a referent every belief referent is accessible, parasitism in the paper's sense (§3.1).

Attitude merge (58) and presupposition binding

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

Append one compartment's content to 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.

Equations

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

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

Attitude merge (58) makes two partial descriptions of one agent's state one, merging the belief layers and combining like-mode compartments.

Equations

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

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

K.bind presup antecedent resolves a presupposition by binding its referent to an accessible antecedent in the manner of [vdS92], dropping the presupposed referent and renaming it throughout.

Equations

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

Karttunen's puzzle (§5.3)

Sue thinks that Jane has been cheating on her husband. She hopes that Jane will stop cheating on him. Referents: Sue 10, Jane 11, the husband 12, the believed cheating event 20, and the cheating event 21 presupposed by stop.

def Maier2015.sueBelief : MentalState

After the first sentence Sue believes there is a cheating event (59).

Equations

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

def Maier2015.sueHope : MentalState

The second sentence on its own gives a desire compartment with stop and the presupposed event, with no antecedent in its belief layer.

Equations

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

def Maier2015.sueMerged : MentalState

The two ascriptions merged (59).

Equations

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

def Maier2015.sueBound : MentalState

The merged description after binding the presupposed event to the believed one (60).

Equations

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

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

Before the merge the believed event does not occur in the hope description, so the presupposition of stop has no antecedent and could only be accommodated.

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

After the merge the believed event is accessible from the presupposed one, so binding, the filtering, is licensed.

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

The dependence is asymmetric, since the believed event does not see the desire's referent.

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

After binding the presupposed referent is gone and the believed event remains, so the presupposition is resolved by binding, neither accommodated nor projected (60).

The data

theorem Maier2015.filtering_iff_doxastic_first (e : Datum) : e ∈ Examples.all → (e.judgment = Judgment.acceptable ↔ e.feature? "order" = some "doxasticFirst")

In the attitude sequences of the paper and of [Kar73], the presupposition of the second ascription is filtered, and the discourse felicitous, exactly when the doxastic ascription comes first, since the parasitic attitude sees the belief and not conversely.