Belief and complement worlds

The world space of the know/think projection experiments: a world records whether the attitude holder believes the complement and whether the complement is true. Know holds at a world when both do and think when the first does, so know entails the complement and entails think, the factive against non-factive contrast of [KK70]. The two questions of the experiments ask for the two coordinates, and a speaker assumes the complement when it is true throughout an information state.

References

• [KK70]
• [ST25]
• [GW25a]

@[reducible, inline]

abbrev Factivity.World : Type

A world of the projection experiments records whether the attitude holder believes the complement and whether it is true, as the pair of the two truth values, so that a prior over worlds can be a product measure.

Equations

• Factivity.World = (Bool × Bool)

@[reducible, inline]

abbrev Factivity.World.believes (w : World) : Bool

The attitude holder believes the complement.

Equations

• w.believes = w.1

@[reducible, inline]

abbrev Factivity.World.complement (w : World) : Bool

The complement is true.

Equations

• w.complement = w.2

def Factivity.World.Knows (w : World) : Prop

X knows C holds when X believes the complement and it is true.

Equations

• w.Knows = (w.believes = true ∧ w.complement = true)

@[instance_reducible]

instance Factivity.instDecidablePredWorldKnows : DecidablePred World.Knows

Equations

• Factivity.instDecidablePredWorldKnows x✝ = { decide := decide (x✝.believes = true) && decide (x✝.complement = true), reflects_decide := ⋯ }

def Factivity.World.Thinks (w : World) : Prop

X thinks C holds when X believes the complement.

Equations

• w.Thinks = (w.believes = true)

@[instance_reducible]

instance Factivity.instDecidablePredWorldThinks : DecidablePred World.Thinks

Equations

• Factivity.instDecidablePredWorldThinks x✝ = Factivity.instDecidablePredWorldThinks._aux_1 x✝

theorem Factivity.World.Knows.complement {w : World} (h : w.Knows) : w.complement = true

Know entails its complement, the defining property of a factive.

theorem Factivity.World.Knows.thinks {w : World} (h : w.Knows) : w.Thinks

Know entails think.

inductive Factivity.Question : Type

The two questions of the experiments, whether X believes the complement and whether it is true.

• belief : Question
• complement : Question

@[instance_reducible]

instance Factivity.instDecidableEqQuestion : DecidableEq Question

Equations

• Factivity.instDecidableEqQuestion x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Factivity.instReprQuestion : Repr Question

Equations

• Factivity.instReprQuestion = { reprPrec := Factivity.instReprQuestion.repr }

def Factivity.instReprQuestion.repr : Question → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Factivity.instReprQuestion.repr Factivity.Question.belief prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Factivity.Question.belief")).group prec✝

@[instance_reducible]

instance Factivity.instInhabitedQuestion : Inhabited Question

Equations

• Factivity.instInhabitedQuestion = { default := Factivity.instInhabitedQuestion.default }

@[instance_reducible]

instance Factivity.instFintypeQuestion : Fintype Question

Equations

• Factivity.instFintypeQuestion = { elems := { val := ↑Factivity.Question.enumList, nodup := Factivity.Question.enumList_nodup }, complete := Factivity.instFintypeQuestion._proof_1 }

def Factivity.Question.answer : Question → World → Bool

The answer a world gives to a question.

Equations

• Factivity.Question.belief.answer x✝ = x✝.believes
• Factivity.Question.complement.answer x✝ = x✝.complement

def Factivity.AssumesComplement (S : Finset World) : Prop

The speaker assumes the complement when it is true throughout the information state.

Equations

• Factivity.AssumesComplement S = ∀ w ∈ S, w.complement = true

@[instance_reducible]

instance Factivity.instDecidablePredFinsetWorldAssumesComplement : DecidablePred AssumesComplement

Equations

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