inductive Phenomena.ParasiticAttitudes.Karttunen1973.BeatingWorld : Type

World type for Bill/Fred wife-beating scenario.

Models three possible states:

• Fred was beating and stopped (presupposition satisfied, assertion true)
• Fred was beating and continues (presupposition satisfied, assertion false)
• Fred never beat (presupposition fails)

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

instance Phenomena.ParasiticAttitudes.Karttunen1973.instDecidableEqBeatingWorld : DecidableEq BeatingWorld

Equations

• Phenomena.ParasiticAttitudes.Karttunen1973.instDecidableEqBeatingWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.ParasiticAttitudes.Karttunen1973.instReprBeatingWorld.repr : BeatingWorld → ℕ → Std.Format

Equations

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

instance Phenomena.ParasiticAttitudes.Karttunen1973.instReprBeatingWorld : Repr BeatingWorld

Equations

• Phenomena.ParasiticAttitudes.Karttunen1973.instReprBeatingWorld = { reprPrec := Phenomena.ParasiticAttitudes.Karttunen1973.instReprBeatingWorld.repr }

instance Phenomena.ParasiticAttitudes.Karttunen1973.instInhabitedBeatingWorld : Inhabited BeatingWorld

Equations

• Phenomena.ParasiticAttitudes.Karttunen1973.instInhabitedBeatingWorld = { default := Phenomena.ParasiticAttitudes.Karttunen1973.instInhabitedBeatingWorld.default }

def Phenomena.ParasiticAttitudes.Karttunen1973.instInhabitedBeatingWorld.default : BeatingWorld

Equations

• Phenomena.ParasiticAttitudes.Karttunen1973.instInhabitedBeatingWorld.default = Phenomena.ParasiticAttitudes.Karttunen1973.BeatingWorld.fredWasBeating_fredStopped

structure Phenomena.ParasiticAttitudes.Karttunen1973.AttitudeSequenceJudgment : Type

Empirical judgment about attitude sequence and presupposition projection.

Records:

• The sentence
• Whether the presupposition projects to the speaker
• Whether the presupposition is attributed to the attitude holder
• 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?

instance Phenomena.ParasiticAttitudes.Karttunen1973.instReprAttitudeSequenceJudgment : Repr AttitudeSequenceJudgment

Equations

• Phenomena.ParasiticAttitudes.Karttunen1973.instReprAttitudeSequenceJudgment = { reprPrec := Phenomena.ParasiticAttitudes.Karttunen1973.instReprAttitudeSequenceJudgment.repr }

def Phenomena.ParasiticAttitudes.Karttunen1973.instReprAttitudeSequenceJudgment.repr : AttitudeSequenceJudgment → ℕ → Std.Format

Equations

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

def Phenomena.ParasiticAttitudes.Karttunen1973.believeHopeFiltering : AttitudeSequenceJudgment

Believe-hope sequences filter presuppositions.

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

The presupposition of "stop" (that Fred was beating) is filtered by the preceding belief ascription -- it does not project to the speaker.

Equations

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

def Phenomena.ParasiticAttitudes.Karttunen1973.hopeBelieverNoFiltering : AttitudeSequenceJudgment

Hope-believe does not filter.

"*John hopes Mary will come. He believes Sue will come too."

The "too" presupposition (someone salient will come) is not filtered by the preceding hope -- it projects to the speaker, causing infelicity if no one is salient. This asymmetry shows the dependency is one-directional: believe → hope.

Equations

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

theorem Phenomena.ParasiticAttitudes.Karttunen1973.asymmetry_data : believeHopeFiltering.presupProjectsToSpeaker = false ∧ hopeBelieverNoFiltering.presupProjectsToSpeaker = true

Belief can satisfy hope's presuppositions, but hope cannot satisfy belief's presuppositions.

def Phenomena.ParasiticAttitudes.Karttunen1973.believeImagineFiltering : AttitudeSequenceJudgment

Believe-imagine also filters (imagination is parasitic on belief).

"John believed there was a monster and imagined it was chasing him" → No presupposition to speaker about monster existence

Equations

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

def Phenomena.ParasiticAttitudes.Karttunen1973.believeDreamFiltering : AttitudeSequenceJudgment

Believe-dream also filters (dreams are parasitic on beliefs).

"John believed the king existed and dreamed the king was bald" → No presupposition to speaker about king existence

Equations

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

def Phenomena.ParasiticAttitudes.Karttunen1973.imagineBelieverNoFiltering : AttitudeSequenceJudgment

Imagine-believe does not filter (belief is not parasitic on imagination).

"?John imagined there was a monster. He believed it was dangerous." → Awkward: "it" presupposes established referent not from imagination

Equations

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

def Phenomena.ParasiticAttitudes.Karttunen1973.fredStopped : Core.Presupposition.PrProp BeatingWorld

"Fred stopped beating his wife" as a presuppositional proposition.

Presupposition: Fred was beating his wife Assertion: Fred no longer beats his wife

Equations

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

def Phenomena.ParasiticAttitudes.Karttunen1973.fredWasBeating : Core.Presupposition.PrProp BeatingWorld

"Fred was beating his wife" (the antecedent belief).

No presupposition, just an assertion.

Equations

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

theorem Phenomena.ParasiticAttitudes.Karttunen1973.assertion_entails_presup (w : BeatingWorld) : fredWasBeating.assertion w = true → fredStopped.presup w = true

The assertion of "Fred was beating" entails the presupposition of "Fred stopped beating".

This is what enables filtering in believe-hope sequences.

inductive Phenomena.ParasiticAttitudes.Karttunen1973.AttitudeType : Type

Classification of attitudes by their parasitic status.

• Doxastic: belief, knowledge - these are the "host" attitudes
• Parasitic: hope, fear, imagine, dream - depend on doxastic attitudes

• doxastic : AttitudeType
• parasitic : AttitudeType

instance Phenomena.ParasiticAttitudes.Karttunen1973.instDecidableEqAttitudeType : DecidableEq AttitudeType

Equations

• Phenomena.ParasiticAttitudes.Karttunen1973.instDecidableEqAttitudeType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.ParasiticAttitudes.Karttunen1973.instReprAttitudeType.repr : AttitudeType → ℕ → Std.Format

Equations

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

instance Phenomena.ParasiticAttitudes.Karttunen1973.instReprAttitudeType : Repr AttitudeType

Equations

• Phenomena.ParasiticAttitudes.Karttunen1973.instReprAttitudeType = { reprPrec := Phenomena.ParasiticAttitudes.Karttunen1973.instReprAttitudeType.repr }

def Phenomena.ParasiticAttitudes.Karttunen1973.classifyAttitude : String → AttitudeType

Common attitude verbs and their classification.

Equations

• Phenomena.ParasiticAttitudes.Karttunen1973.classifyAttitude "believe" = Phenomena.ParasiticAttitudes.Karttunen1973.AttitudeType.doxastic
• Phenomena.ParasiticAttitudes.Karttunen1973.classifyAttitude "know" = Phenomena.ParasiticAttitudes.Karttunen1973.AttitudeType.doxastic
• Phenomena.ParasiticAttitudes.Karttunen1973.classifyAttitude "think" = Phenomena.ParasiticAttitudes.Karttunen1973.AttitudeType.doxastic
• Phenomena.ParasiticAttitudes.Karttunen1973.classifyAttitude "hope" = Phenomena.ParasiticAttitudes.Karttunen1973.AttitudeType.parasitic
• Phenomena.ParasiticAttitudes.Karttunen1973.classifyAttitude "fear" = Phenomena.ParasiticAttitudes.Karttunen1973.AttitudeType.parasitic
• Phenomena.ParasiticAttitudes.Karttunen1973.classifyAttitude "imagine" = Phenomena.ParasiticAttitudes.Karttunen1973.AttitudeType.parasitic
• Phenomena.ParasiticAttitudes.Karttunen1973.classifyAttitude "dream" = Phenomena.ParasiticAttitudes.Karttunen1973.AttitudeType.parasitic
• Phenomena.ParasiticAttitudes.Karttunen1973.classifyAttitude "wish" = Phenomena.ParasiticAttitudes.Karttunen1973.AttitudeType.parasitic
• Phenomena.ParasiticAttitudes.Karttunen1973.classifyAttitude "expect" = Phenomena.ParasiticAttitudes.Karttunen1973.AttitudeType.parasitic
• Phenomena.ParasiticAttitudes.Karttunen1973.classifyAttitude x✝ = Phenomena.ParasiticAttitudes.Karttunen1973.AttitudeType.doxastic

def Phenomena.ParasiticAttitudes.Karttunen1973.canFilter (first second : AttitudeType) : Bool

Filtering can only occur when a doxastic attitude precedes a parasitic one.

This captures Maier's asymmetric dependency.

Equations

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

theorem Phenomena.ParasiticAttitudes.Karttunen1973.doxastic_then_parasitic_can_filter : canFilter AttitudeType.doxastic AttitudeType.parasitic = true

theorem Phenomena.ParasiticAttitudes.Karttunen1973.parasitic_then_doxastic_cannot_filter : canFilter AttitudeType.parasitic AttitudeType.doxastic = false

def Phenomena.ParasiticAttitudes.Karttunen1973.allJudgments : List AttitudeSequenceJudgment

All empirical judgments collected in this module.

Equations

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

def Phenomena.ParasiticAttitudes.Karttunen1973.filteringCases : List AttitudeSequenceJudgment

The filtering cases are exactly those where doxastic precedes parasitic.

Equations

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

def Phenomena.ParasiticAttitudes.Karttunen1973.nonFilteringCases : List AttitudeSequenceJudgment

The non-filtering cases are those where parasitic precedes doxastic.

Equations

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