def Semantics.Attitudes.Parasitic.isParasiticOn {W : Type u_1} {E : Type u_2} (nonDoxAccess : E → W → W → Bool) (doxAccess : Doxastic.AccessRel W E) : Prop

A non-doxastic attitude is parasitic on a doxastic one when its presupposition computation uses the doxastic accessibility relation rather than its own.

Formally: for presupposition filtering under the non-doxastic attitude, we check whether the presupposition holds at all worlds accessible via the doxastic relation.

Equations

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

def Semantics.Attitudes.Parasitic.PreferentialParasiticOn {W : Type u_1} {E : Type u_2} (_pref : Preferential.PreferentialPredicate W E) (dox : Doxastic.DoxasticPredicate W E) : Prop

A preferential predicate is parasitic on a doxastic predicate when the preferential predicate's presupposition filtering defers to the doxastic accessibility relation.

Equations

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

inductive Semantics.Attitudes.Parasitic.ParasiticAttitude : Type

The list of attitude verbs that are parasitic on belief.

These are non-doxastic attitudes whose presupposition filtering uses the belief accessibility relation.

• hope : ParasiticAttitude
• fear : ParasiticAttitude
• imagine : ParasiticAttitude
• dream : ParasiticAttitude
• wish : ParasiticAttitude
• expect : ParasiticAttitude

@[implicit_reducible]

instance Semantics.Attitudes.Parasitic.instDecidableEqParasiticAttitude : DecidableEq ParasiticAttitude

Equations

• Semantics.Attitudes.Parasitic.instDecidableEqParasiticAttitude x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Attitudes.Parasitic.instReprParasiticAttitude.repr : ParasiticAttitude → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Attitudes.Parasitic.instReprParasiticAttitude : Repr ParasiticAttitude

Equations

• Semantics.Attitudes.Parasitic.instReprParasiticAttitude = { reprPrec := Semantics.Attitudes.Parasitic.instReprParasiticAttitude.repr }

def Semantics.Attitudes.Parasitic.hopeParasiticOnBelief : ParasiticAttitude

Hope is parasitic on belief.

When "X believes P and hopes Q", the presuppositions of Q are filtered using X's belief state, not X's hope state.

Equations

• Semantics.Attitudes.Parasitic.hopeParasiticOnBelief = Semantics.Attitudes.Parasitic.ParasiticAttitude.hope

def Semantics.Attitudes.Parasitic.imagineParasiticOnBelief : ParasiticAttitude

Imagine is parasitic on belief.

When "X believes P and imagines Q", the presuppositions of Q are filtered using X's belief state.

Equations

• Semantics.Attitudes.Parasitic.imagineParasiticOnBelief = Semantics.Attitudes.Parasitic.ParasiticAttitude.imagine

def Semantics.Attitudes.Parasitic.dreamParasiticOnBelief : ParasiticAttitude

Dream is parasitic on belief.

When "X believes P and dreams Q", the presuppositions of Q are filtered using X's belief state.

Equations

• Semantics.Attitudes.Parasitic.dreamParasiticOnBelief = Semantics.Attitudes.Parasitic.ParasiticAttitude.dream

structure Semantics.Attitudes.Parasitic.ParasiticAsymmetry {W : Type u_1} {E : Type u_2} (dox : Doxastic.DoxasticPredicate W E) (nonDox : Preferential.PreferentialPredicate W E) : Prop

The parasitic dependency is asymmetric.

Non-doxastic attitudes depend on doxastic ones for presupposition filtering, but NOT vice versa.

This explains Karttunen's observation:

• believe → hope: hope uses belief's accessibility → filtering works
• hope → believe: belief uses its own accessibility → no filtering

• forward : PreferentialParasiticOn nonDox dox

  Non-doxastic is parasitic on doxastic

• backward : ¬∀ (_agent : E) (_p : Core.Presupposition.PrProp W) (_w : W) (_worlds : List W), True → True

  Doxastic is NOT parasitic on non-doxastic

inductive Semantics.Attitudes.Parasitic.FilteringDirection : Type

The filtering direction determines which sequences work.

Filtering can occur in "believe P and hope Q" but not "hope P and believe Q".

• doxasticFirst : FilteringDirection
• parasiticFirst : FilteringDirection

@[implicit_reducible]

instance Semantics.Attitudes.Parasitic.instDecidableEqFilteringDirection : DecidableEq FilteringDirection

Equations

• Semantics.Attitudes.Parasitic.instDecidableEqFilteringDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Attitudes.Parasitic.instReprFilteringDirection : Repr FilteringDirection

Equations

• Semantics.Attitudes.Parasitic.instReprFilteringDirection = { reprPrec := Semantics.Attitudes.Parasitic.instReprFilteringDirection.repr }

def Semantics.Attitudes.Parasitic.instReprFilteringDirection.repr : FilteringDirection → ℕ → Std.Format

Equations

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

def Semantics.Attitudes.Parasitic.canFilter : FilteringDirection → Bool

Can filtering occur given the attitude order?

Equations

• Semantics.Attitudes.Parasitic.canFilter Semantics.Attitudes.Parasitic.FilteringDirection.doxasticFirst = true
• Semantics.Attitudes.Parasitic.canFilter Semantics.Attitudes.Parasitic.FilteringDirection.parasiticFirst = false

theorem Semantics.Attitudes.Parasitic.doxastic_first_can_filter : canFilter FilteringDirection.doxasticFirst = true

theorem Semantics.Attitudes.Parasitic.parasitic_first_cannot_filter : canFilter FilteringDirection.parasiticFirst = false

inductive Semantics.Attitudes.Parasitic.BeatingWorld : Type

World type for the Bill/Fred example.

• fredWasBeating_fredStopped : BeatingWorld
• fredWasBeating_fredContinues : BeatingWorld
• fredNeverBeat : BeatingWorld

@[implicit_reducible]

instance Semantics.Attitudes.Parasitic.instDecidableEqBeatingWorld : DecidableEq BeatingWorld

Equations

• Semantics.Attitudes.Parasitic.instDecidableEqBeatingWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Attitudes.Parasitic.instReprBeatingWorld : Repr BeatingWorld

Equations

• Semantics.Attitudes.Parasitic.instReprBeatingWorld = { reprPrec := Semantics.Attitudes.Parasitic.instReprBeatingWorld.repr }

def Semantics.Attitudes.Parasitic.instReprBeatingWorld.repr : BeatingWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Attitudes.Parasitic.instInhabitedBeatingWorld : Inhabited BeatingWorld

Equations

• Semantics.Attitudes.Parasitic.instInhabitedBeatingWorld = { default := Semantics.Attitudes.Parasitic.instInhabitedBeatingWorld.default }

def Semantics.Attitudes.Parasitic.instInhabitedBeatingWorld.default : BeatingWorld

Equations

• Semantics.Attitudes.Parasitic.instInhabitedBeatingWorld.default = Semantics.Attitudes.Parasitic.BeatingWorld.fredWasBeating_fredStopped

def Semantics.Attitudes.Parasitic.billBeliefAccess : Doxastic.AccessRel BeatingWorld Unit

Bill's belief accessibility relation.

In some worlds, Bill believes Fred was beating his wife.

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Attitudes.Parasitic.billBeliefAccess PUnit.unit Semantics.Attitudes.Parasitic.BeatingWorld.fredNeverBeat Semantics.Attitudes.Parasitic.BeatingWorld.fredNeverBeat = True
• Semantics.Attitudes.Parasitic.billBeliefAccess PUnit.unit Semantics.Attitudes.Parasitic.BeatingWorld.fredNeverBeat x✝ = False

@[implicit_reducible]

instance Semantics.Attitudes.Parasitic.instDecidableBillBeliefAccess (a : Unit) (w w' : BeatingWorld) : Decidable (billBeliefAccess a w w')

Equations

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

def Semantics.Attitudes.Parasitic.billBelieve : Doxastic.DoxasticPredicate BeatingWorld Unit

Bill's belief predicate.

Equations

• Semantics.Attitudes.Parasitic.billBelieve = Semantics.Attitudes.Doxastic.believeTemplate Semantics.Attitudes.Parasitic.billBeliefAccess

def Semantics.Attitudes.Parasitic.fredWasBeatingPresup : BeatingWorld → Prop

The presupposition of "Fred stopped": Fred was beating.

Equations

• Semantics.Attitudes.Parasitic.fredWasBeatingPresup Semantics.Attitudes.Parasitic.BeatingWorld.fredWasBeating_fredStopped = True
• Semantics.Attitudes.Parasitic.fredWasBeatingPresup Semantics.Attitudes.Parasitic.BeatingWorld.fredWasBeating_fredContinues = True
• Semantics.Attitudes.Parasitic.fredWasBeatingPresup Semantics.Attitudes.Parasitic.BeatingWorld.fredNeverBeat = False

@[implicit_reducible]

instance Semantics.Attitudes.Parasitic.instDecidablePredBeatingWorldFredWasBeatingPresup : DecidablePred fredWasBeatingPresup

Equations

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

theorem Semantics.Attitudes.Parasitic.belief_satisfies_hope_presup (w : BeatingWorld) : w = BeatingWorld.fredWasBeating_fredStopped ∨ w = BeatingWorld.fredWasBeating_fredContinues → ∀ (w' : BeatingWorld), billBeliefAccess () w w' → fredWasBeatingPresup w'

When Bill believes Fred was beating, hope's presupposition is satisfied.

At worlds where Bill believes Fred was beating, ALL his belief-accessible worlds satisfy the presupposition of "stop".

theorem Semantics.Attitudes.Parasitic.no_belief_no_filter (w' : BeatingWorld) : billBeliefAccess () BeatingWorld.fredNeverBeat w' → ¬fredWasBeatingPresup w'

At worlds where Bill doesn't believe Fred was beating, the presupposition of "stop" fails in Bill's belief worlds.

def Semantics.Attitudes.Parasitic.parasiticLocalContext {W : Type u_1} {E : Type u_2} (dox : Doxastic.DoxasticPredicate W E) (agent : E) (w : W) (globalCtx : W → Prop) : W → Prop

The local context for a parasitic attitude embedded under belief.

When we have "X believes P and hopes Q", the local context for Q is computed from X's belief state (not a separate hope accessibility).

Equations

• Semantics.Attitudes.Parasitic.parasiticLocalContext dox agent w globalCtx w' = (globalCtx w ∧ dox.access agent w w')

def Semantics.Attitudes.Parasitic.presupFilteredInParasitic {W : Type u_1} {E : Type u_2} (dox : Doxastic.DoxasticPredicate W E) (agent : E) (w : W) (presup : W → Prop) (worlds : List W) : Prop

A presupposition is filtered in the parasitic local context iff it holds at all doxastically accessible worlds.

Equations

• Semantics.Attitudes.Parasitic.presupFilteredInParasitic dox agent w presup worlds = ∀ w' ∈ worlds, dox.access agent w w' → presup w'

def Semantics.Attitudes.Parasitic.toBeliefLocalCtx {W : Type u_1} {E : Type u_2} (dox : Presupposition.BeliefEmbedding.DoxasticAccessibility W E) (globalCtx : W → Prop) (agent : E) : Presupposition.BeliefEmbedding.BeliefLocalCtx W E

Convert a parasitic attitude context to a BeliefLocalCtx.

This shows that parasitic attitudes use the same local context machinery as belief embedding itself.

Equations

• Semantics.Attitudes.Parasitic.toBeliefLocalCtx dox globalCtx agent = { globalCtx := globalCtx, dox := dox, agent := agent }

theorem Semantics.Attitudes.Parasitic.parasitic_uses_belief_local_context {W : Type u_1} {E : Type u_2} (dox : Presupposition.BeliefEmbedding.DoxasticAccessibility W E) (globalCtx : W → Prop) (agent : E) (p : Core.Presupposition.PrProp W) : have blc := toBeliefLocalCtx dox globalCtx agent; Presupposition.BeliefEmbedding.presupAttributedToHolder blc p ↔ ∀ (w_star : W), globalCtx w_star → ∀ (w' : W), dox agent w_star w' → p.presup w'

The key insight: parasitic attitudes compute presupposition filtering using presupAttributedToHolder from BeliefEmbedding.

This unifies the treatment: both "X believes P" and "X hopes P" (when hope is parasitic on belief) use the same local context machinery.

structure Semantics.Attitudes.Parasitic.ParasiticAnalysis {W : Type u_1} {E : Type u_2} : Type (max u_1 u_2)

Summary structure capturing the parasitic attitude analysis.

• doxasticHost : Doxastic.DoxasticPredicate W E

  The doxastic predicate that hosts parasitic attitudes

• parasiticAttitudes : List ParasiticAttitude

  List of parasitic attitudes

• useDoxasticAccessibility : Bool

  The key property: parasitic attitudes use doxastic accessibility

def Semantics.Attitudes.Parasitic.standardAnalysis {W : Type u_1} {E : Type u_2} (believe : Doxastic.DoxasticPredicate W E) : ParasiticAnalysis

Standard analysis with belief as host.

Equations

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