Factive vs Non-Factive Attitude Verb Semantics

@cite{karttunen-1971} @cite{kiparsky-kiparsky-1970} @cite{scontras-tonhauser-2025}

Generic infrastructure for the factive/non-factive distinction in Boolean world models: world-dimension typeclasses, lexical semantics for know-type (factive) and think-type (non-factive) verbs, entailment properties, QUD projection, and conditional embedding.

These definitions are parametric in the world type W via typeclasses, allowing instantiation for any model with belief and complement dimensions (e.g., @cite{scontras-tonhauser-2025}'s projection model).

World Dimensions

A world type may carry orthogonal Boolean dimensions:

Dimension	Typeclass	Gloss
C	HasComplement	Whether the complement is true
BEL	HasBelief	Whether the agent believes C
A	HasAntecedent	Whether a conditional antecedent holds

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

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

World type has a complement dimension (C: whether the complement is true).

• c : W → Bool

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

World type has a belief dimension (BEL: whether the agent believes C).

• bel : W → Bool

class Semantics.Attitudes.Factivity.HasAntecedent (W : Type u_1) : Type u_1

World type has an antecedent dimension (A: whether the conditional antecedent holds). Used for conditional embedding of attitude reports.

• a : W → Bool

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

Factive positive: "X knows C" = BEL ∧ C (veridical).

Equations

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

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

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

Equations

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

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

Non-factive positive: "X thinks C" = BEL (non-veridical).

Equations

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

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

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

Equations

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

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

Factive positive entails C (the defining property of factivity).

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

Factive positive entails BEL.

theorem Semantics.Attitudes.Factivity.nonFactivePos_not_entails_c {W : Type u_1} [HasBelief W] [HasComplement W] (h : ∃ (w : W), HasBelief.bel w = true ∧ HasComplement.c w = false) : ∃ (w : W), nonFactivePos w = true ∧ HasComplement.c w = false

Non-factive does NOT entail C (given a world where BEL ∧ ¬C is possible).

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

Know entails think (factivity is strictly stronger than belief).

inductive Semantics.Attitudes.Factivity.QUD : Type

QUD for factive/non-factive models: a question about belief or complement truth. These are the two orthogonal dimensions of a world with HasBelief and HasComplement.

• bel : QUD
• c : QUD

instance Semantics.Attitudes.Factivity.instDecidableEqQUD : DecidableEq QUD

Equations

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

instance Semantics.Attitudes.Factivity.instReprQUD : Repr QUD

Equations

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

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

Equations

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

instance Semantics.Attitudes.Factivity.instBEqQUD : BEq QUD

Equations

• Semantics.Attitudes.Factivity.instBEqQUD = { beq := Semantics.Attitudes.Factivity.instBEqQUD.beq }

def Semantics.Attitudes.Factivity.instBEqQUD.beq : QUD → QUD → Bool

Equations

• Semantics.Attitudes.Factivity.instBEqQUD.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Attitudes.Factivity.instInhabitedQUD.default : QUD

Equations

• Semantics.Attitudes.Factivity.instInhabitedQUD.default = Semantics.Attitudes.Factivity.QUD.bel

instance Semantics.Attitudes.Factivity.instInhabitedQUD : Inhabited QUD

Equations

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

def Semantics.Attitudes.Factivity.allQUDs : List QUD

All QUDs.

Equations

• Semantics.Attitudes.Factivity.allQUDs = [Semantics.Attitudes.Factivity.QUD.bel, Semantics.Attitudes.Factivity.QUD.c]

def Semantics.Attitudes.Factivity.qudProject {W : Type u_1} [HasBelief W] [HasComplement W] : QUD → W → W → Bool

QUD equivalence: two worlds agree on the relevant dimension.

Equations

• Semantics.Attitudes.Factivity.qudProject Semantics.Attitudes.Factivity.QUD.bel x✝¹ x✝ = (Semantics.Attitudes.Factivity.HasBelief.bel x✝¹ == Semantics.Attitudes.Factivity.HasBelief.bel x✝)
• Semantics.Attitudes.Factivity.qudProject Semantics.Attitudes.Factivity.QUD.c x✝¹ x✝ = (Semantics.Attitudes.Factivity.HasComplement.c x✝¹ == Semantics.Attitudes.Factivity.HasComplement.c x✝)

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

Whether a belief state (given as membership over worlds) entails C. A speaker "assumes C" iff C holds at every world they consider possible.

Equations

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

def Semantics.Attitudes.Factivity.condOp {W : Type u_1} (antecedent consequent : W → Bool) : W → Bool

Material conditional operator: ⟦if⟧ = λp.λq.λw. ¬p(w) ∨ q(w).

Equations

• Semantics.Attitudes.Factivity.condOp antecedent consequent w = (!antecedent w || consequent w)

def Semantics.Attitudes.Factivity.composeCondFactive {W : Type u_1} [HasAntecedent W] [HasBelief W] [HasComplement W] : W → Bool

Composed "if A, X knows C".

Equations

• Semantics.Attitudes.Factivity.composeCondFactive = Semantics.Attitudes.Factivity.condOp Semantics.Attitudes.Factivity.HasAntecedent.a Semantics.Attitudes.Factivity.factivePos

def Semantics.Attitudes.Factivity.composeCondNonFactive {W : Type u_1} [HasAntecedent W] [HasBelief W] : W → Bool

Composed "if A, X thinks C".

Equations

• Semantics.Attitudes.Factivity.composeCondNonFactive = Semantics.Attitudes.Factivity.condOp Semantics.Attitudes.Factivity.HasAntecedent.a Semantics.Attitudes.Factivity.nonFactivePos

def Semantics.Attitudes.Factivity.composeCondFactiveNeg {W : Type u_1} [HasAntecedent W] [HasBelief W] [HasComplement W] : W → Bool

Composed "if A, X doesn't know C".

Equations

• Semantics.Attitudes.Factivity.composeCondFactiveNeg = Semantics.Attitudes.Factivity.condOp Semantics.Attitudes.Factivity.HasAntecedent.a Semantics.Attitudes.Factivity.factiveNeg

def Semantics.Attitudes.Factivity.composeCondNonFactiveNeg {W : Type u_1} [HasAntecedent W] [HasBelief W] : W → Bool

Composed "if A, X doesn't think C".

Equations

• Semantics.Attitudes.Factivity.composeCondNonFactiveNeg = Semantics.Attitudes.Factivity.condOp Semantics.Attitudes.Factivity.HasAntecedent.a Semantics.Attitudes.Factivity.nonFactiveNeg