Factive and non-factive attitude semantics

The factive/non-factive distinction of [KK70] and [Kar71] over Boolean world models: a world type carries orthogonal dimensions — HasComplement (is the complement true?) and HasBelief (does the agent believe it?) — and the know-type and think-type verbs differ in whether the complement dimension enters the lexical semantics:

Verb form	Semantics	Factivity
"X knows C"	BEL ∧ C	factive
"X doesn't know"	¬(BEL ∧ C)	factive
"X thinks C"	BEL	non-factive
"X doesn't think"	¬BEL	non-factive

Factivity is veridicality of the positive form (factivePos_entails_c), and know is strictly stronger than think (factive_entails_nonfactive). QUD is the two-question space of the projection experiments (BEL? and C?), and assumesComplement renders "the speaker assumes C" as C holding throughout a belief state.

The semantics is Bool-valued deliberately: these meanings feed the ℚ-valued RSA tables of [ST25] (Studies/ ScontrasTonhauser2025.lean) and [GW25a]-style models (Studies/GroveWhite2025.lean) as literal-listener truth tables; the Prop migration is coupled to the planned RSA measures migration.

class Factivity.HasComplement (W : Type u_1) : Type u_1

The world type carries a complement dimension: is the complement true at w?

• c : W → Bool

class Factivity.HasBelief (W : Type u_1) : Type u_1

The world type carries a belief dimension: does the agent believe the complement at w?

• bel : W → Bool

Lexical semantics

def Factivity.factivePos {W : Type u_1} [HasBelief W] [HasComplement W] (w : W) : Bool

Factive positive: "X knows C" is BEL ∧ C.

Equations

• Factivity.factivePos w = (Factivity.HasBelief.bel w && Factivity.HasComplement.c w)

def Factivity.factiveNeg {W : Type u_1} [HasBelief W] [HasComplement W] (w : W) : Bool

Factive negative: "X doesn't know C" is ¬(BEL ∧ C).

Equations

• Factivity.factiveNeg w = !(Factivity.HasBelief.bel w && Factivity.HasComplement.c w)

def Factivity.nonFactivePos {W : Type u_1} [HasBelief W] (w : W) : Bool

Non-factive positive: "X thinks C" is BEL.

Equations

• Factivity.nonFactivePos w = Factivity.HasBelief.bel w

def Factivity.nonFactiveNeg {W : Type u_1} [HasBelief W] (w : W) : Bool

Non-factive negative: "X doesn't think C" is ¬BEL.

Equations

• Factivity.nonFactiveNeg w = !Factivity.HasBelief.bel w

Entailment

theorem Factivity.factivePos_entails_c {W : Type u_1} [HasBelief W] [HasComplement W] (w : W) (h : factivePos w = true) : HasComplement.c w = true

Factive positive entails the complement — the defining property of factivity.

theorem Factivity.factivePos_entails_bel {W : Type u_1} [HasBelief W] [HasComplement W] (w : W) (h : factivePos w = true) : HasBelief.bel w = true

Factive positive entails belief.

theorem Factivity.factive_entails_nonfactive {W : Type u_1} [HasBelief W] [HasComplement W] (w : W) (h : factivePos w = true) : nonFactivePos w = true

Know entails think: factivity is strictly stronger than belief.

Question under discussion

inductive Factivity.QUD : Type

The two-question space of the projection experiments: BEL? and C? — the orthogonal dimensions of a HasBelief/HasComplement world.

• bel : QUD

  "Does X believe C?"

• c : QUD

  "Is C true?"

@[instance_reducible]

instance Factivity.instDecidableEqQUD : DecidableEq QUD

Equations

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

@[instance_reducible]

instance Factivity.instReprQUD : Repr QUD

Equations

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

def Factivity.instReprQUD.repr : QUD → Nat → Std.Format

Equations

• Factivity.instReprQUD.repr Factivity.QUD.bel prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Factivity.QUD.bel")).group prec✝
• Factivity.instReprQUD.repr Factivity.QUD.c prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Factivity.QUD.c")).group prec✝

@[instance_reducible]

instance Factivity.instInhabitedQUD : Inhabited QUD

Equations

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

def Factivity.assumesComplement {W : Type u_1} [HasComplement W] (membership : W → Bool) (allWorlds : List W) : Bool

The speaker assumes the complement: C holds at every world of the belief state.

Equations

• Factivity.assumesComplement membership allWorlds = allWorlds.all fun (w : W) => !membership w || Factivity.HasComplement.c w