Glass (2025): Attested versus unattested contrafactive belief verbs

[Gla25] [Gla23a] [RO25]

Semantics and Pragmatics 18, Article 8: 1-17.

Key Claims

1. Two ways to negate the factive presupposition: A contrafactive could require ¬p (all CommonGround worlds are ¬p worlds) or require compatibility with ¬p (some CommonGround world is a ¬p world).

2. Strong contrafactives are unattested: No verb presupposes ¬p (requiring CommonGround ⊨ ¬p). This follows from the Predicate Lexicalization Constraint ([RO25]): ¬p cannot causally support B(x)(p).

3. Weak contrafactives exist: Mandarin yǐwéi ([Gla23a]) has a postsupposition ◇¬p — after utterance, the CommonGround must be compatible with ¬p. This is a definedness condition on the output context, not a presupposition on the input context.

4. Revised question: "Why are there belief verbs like know (CommonGround ⊨ p) and yǐwéi (CommonGround ◇ ¬p), but none like contra (CommonGround ⊨ ¬p)?"

Formalization Strategy

Belief verb denotations are PartialProp W values produced by DoxasticPredicate.toPartialProp. The presup field captures the factive presupposition (or lack thereof). yǐwéi's postsupposition is a Postsupposition value (§2 below). The PresupClass typology and the attestation classifier presupClassIsValid are defined here; their causal derivation via the Predicate Lexicalization Constraint is [RO25]'s account, prosecuted in Studies/RobertsOzyildiz2025.lean.

The presuppositional classes

The typology of belief verbs by presuppositional profile: factive (know — CommonGround must entail p), nonfactive (think — no requirement), contrafactive (hypothetical contra — CommonGround must entail ¬p; UNATTESTED), with yǐwéi's ◇¬p requirement a postsupposition (§2), not a presupposition. The class of a verb is derived from its veridicality, and presupClassIsValid records the attestation facts — valid iff not contrafactive.

inductive Glass2025.PresupClass : Type

Presuppositional profile of a doxastic verb.

• factive : PresupClass

  Presupposes p (know).

• contrafactive : PresupClass

  Would presuppose ¬p (hypothetical contra; unattested).

• nonfactive : PresupClass

  No presupposition (believe, think).

• other : PresupClass

  None of the above.

@[instance_reducible]

instance Glass2025.instDecidableEqPresupClass : DecidableEq PresupClass

Equations

• Glass2025.instDecidableEqPresupClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Glass2025.instReprPresupClass.repr : PresupClass → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Glass2025.instReprPresupClass : Repr PresupClass

Equations

• Glass2025.instReprPresupClass = { reprPrec := Glass2025.instReprPresupClass.repr }

def Glass2025.classifyVeridicality : Features.Veridicality → PresupClass

Classify a doxastic verb by its veridicality.

Equations

• Glass2025.classifyVeridicality Features.Veridicality.veridical = Glass2025.PresupClass.factive
• Glass2025.classifyVeridicality Features.Veridicality.nonVeridical = Glass2025.PresupClass.nonfactive

def Glass2025.presupClassIsValid : PresupClass → Bool

The attestation facts: every profile is attested except the contrafactive. The causal derivation of this table is RobertsOzyildiz2025.presupClassIsValid_eq_via_plc.

Equations

• Glass2025.presupClassIsValid Glass2025.PresupClass.factive = true
• Glass2025.presupClassIsValid Glass2025.PresupClass.nonfactive = true
• Glass2025.presupClassIsValid Glass2025.PresupClass.contrafactive = false
• Glass2025.presupClassIsValid Glass2025.PresupClass.other = true

theorem Glass2025.factive_presup_valid : presupClassIsValid PresupClass.factive = true

Factive presuppositions are attested.

theorem Glass2025.contrafactive_presup_invalid : presupClassIsValid PresupClass.contrafactive = false

Contrafactive presuppositions are unattested.

theorem Glass2025.nonfactive_presup_valid : presupClassIsValid PresupClass.nonfactive = true

Nonfactive profiles are attested (no presupposition to check).

Minimal 2-world model for exercising Table 1.

• w0: p is true
• w1: p is false

@[instance_reducible]

instance Glass2025.instDecidableEqMiniWorld : DecidableEq Glass2025.MiniWorld✝

Equations

• Glass2025.instDecidableEqMiniWorld x✝ y✝ = if h : Glass2025.MiniWorld.ctorIdx✝ x✝ = Glass2025.MiniWorld.ctorIdx✝ y✝ then isTrue ⋯ else isFalse ⋯

def Glass2025.instReprMiniWorld.repr : Glass2025.MiniWorld✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Glass2025.instReprMiniWorld : Repr Glass2025.MiniWorld✝

Equations

• Glass2025.instReprMiniWorld = { reprPrec := Glass2025.instReprMiniWorld.repr }

@[instance_reducible]

instance Glass2025.instInhabitedMiniWorld : Inhabited Glass2025.MiniWorld✝

Equations

• Glass2025.instInhabitedMiniWorld = { default := Glass2025.instInhabitedMiniWorld.default }

Output-context constraints ([Bra13]): conditions on the Common Ground after an utterance updates it, as opposed to presuppositions, which constrain the input context. [Gla25] argues Mandarin yǐwéi carries the postsupposition ◇¬p: after accepting "x yǐwéi p", the CommonGround must be compatible with ¬p — a condition not derivable from veridicality alone.

structure Glass2025.Postsupposition (W : Type u_1) : Type u_1

A postsupposition: a constraint on the output context after a discourse update, taking the context set (as List W) and the embedded proposition.

• condition : List W → (W → Prop) → Prop

def Glass2025.Postsupposition.none {W : Type u_1} : Postsupposition W

No postsupposition (trivially satisfied).

Equations

• Glass2025.Postsupposition.none = { condition := fun (x : List W) (x_1 : W → Prop) => True }

def Glass2025.Postsupposition.weakContrafactive {W : Type u_1} : Postsupposition W

Weak contrafactive: the output context is compatible with ¬p — some world in the output context falsifies p. This is yǐwéi's ◇¬p ([Gla25], [Gla23a]).

Equations

• Glass2025.Postsupposition.weakContrafactive = { condition := fun (cs : List W) (p : W → Prop) => ∃ w ∈ cs, ¬p w }

def Glass2025.Postsupposition.strongContrafactive {W : Type u_1} : Postsupposition W

Strong contrafactive: the output context entails ¬p — every world in the output context falsifies p. The hypothetical contra verb's requirement — UNATTESTED.

Equations

• Glass2025.Postsupposition.strongContrafactive = { condition := fun (cs : List W) (p : W → Prop) => ∀ w ∈ cs, ¬p w }

theorem Glass2025.Postsupposition.none_condition {W : Type u_1} (cs : List W) (p : W → Prop) : Postsupposition.none.condition cs p

The trivial postsupposition is always satisfied.

theorem Glass2025.Postsupposition.strong_entails_weak {W : Type u_1} {cs : List W} {p : W → Prop} (hne : cs ≠ []) (h : strongContrafactive.condition cs p) : weakContrafactive.condition cs p

Strong contrafactivity entails weak (nonempty contexts): CommonGround ⊨ ¬p forces CommonGround ◇ ¬p — [Gla25]'s observation that yǐwéi's requirement is strictly weaker than contra's.

theorem Glass2025.Postsupposition.weak_not_entails_strong : ∃ (cs : List Bool) (p : Bool → Prop), weakContrafactive.condition cs p ∧ ¬strongContrafactive.condition cs p

Weak contrafactivity does not entail strong: a context can be compatible with ¬p without entailing ¬p.

Construct presuppositional denotations for four verb types directly from veridicality, matching [Gla25] Table 1.

We define the presup fields directly (rather than instantiating full DoxasticPredicates) to keep the model minimal. The connection to DoxasticPredicate.toPartialProp is established by the classification theorems in §4.

Table 1 from [Gla25]: possible states of the Common Ground after updating with each utterance.

Utterance	Projective content	p	◇p ∧ ◇¬p	not-p
x knows p	requires p	✓	✗	✗
x thinks p	(none)	✓	✓	✓
x yǐwéi p	requires ◇(¬p)	✗	✓	✓
x contra p	requires ¬p	✗	✗	✓

We verify this by checking the presup field against each context type.

theorem Glass2025.know_satisfied_factive (w : Glass2025.MiniWorld✝) : w ∈ Glass2025.factiveCtx✝ → Glass2025.knowPresup✝.presup w

theorem Glass2025.know_fails_neutral : ¬∀ w ∈ Glass2025.neutralCtx✝, Glass2025.knowPresup✝.presup w

theorem Glass2025.know_fails_contrafactive : ¬∀ w ∈ Glass2025.contrafactiveCtx✝, Glass2025.knowPresup✝.presup w

theorem Glass2025.think_satisfied_factive (w : Glass2025.MiniWorld✝) : w ∈ Glass2025.factiveCtx✝ → Glass2025.thinkPresup✝.presup w

theorem Glass2025.think_satisfied_neutral (w : Glass2025.MiniWorld✝) : w ∈ Glass2025.neutralCtx✝ → Glass2025.thinkPresup✝.presup w

theorem Glass2025.think_satisfied_contrafactive (w : Glass2025.MiniWorld✝) : w ∈ Glass2025.contrafactiveCtx✝ → Glass2025.thinkPresup✝.presup w

theorem Glass2025.yiwei_presup_satisfied_factive (w : Glass2025.MiniWorld✝) : w ∈ Glass2025.factiveCtx✝ → Glass2025.yiweiPresup✝.presup w

theorem Glass2025.yiwei_presup_satisfied_neutral (w : Glass2025.MiniWorld✝) : w ∈ Glass2025.neutralCtx✝ → Glass2025.yiweiPresup✝.presup w

theorem Glass2025.yiwei_postsup_fails_factive : ¬Glass2025.yiweiPostsup✝.condition Glass2025.factiveCtx✝ fun (x : Glass2025.MiniWorld✝) => Glass2025.prop✝ x = true

theorem Glass2025.yiwei_postsup_satisfied_neutral : Glass2025.yiweiPostsup✝.condition Glass2025.neutralCtx✝ fun (x : Glass2025.MiniWorld✝) => Glass2025.prop✝ x = true

theorem Glass2025.yiwei_postsup_satisfied_contrafactive : Glass2025.yiweiPostsup✝.condition Glass2025.contrafactiveCtx✝ fun (x : Glass2025.MiniWorld✝) => Glass2025.prop✝ x = true

theorem Glass2025.contra_fails_factive : ¬∀ w ∈ Glass2025.factiveCtx✝, Glass2025.contraPresup✝.presup w

theorem Glass2025.contra_fails_neutral : ¬∀ w ∈ Glass2025.neutralCtx✝, Glass2025.contraPresup✝.presup w

theorem Glass2025.contra_satisfied_contrafactive (w : Glass2025.MiniWorld✝) : w ∈ Glass2025.contrafactiveCtx✝ → Glass2025.contraPresup✝.presup w

Each English/Mandarin attitude verb's PresupClass is DERIVED from its veridicality in the Fragment entry. These theorems will BREAK if:

1. A verb's attitude changes
2. The classifyVeridicality function changes
3. The veridicality derivation from Attitude changes

theorem Glass2025.know_is_factive : Option.map classifyVeridicality English.Predicates.Verbal.know.veridicality = some PresupClass.factive

theorem Glass2025.realize_is_factive : Option.map classifyVeridicality English.Predicates.Verbal.realize.veridicality = some PresupClass.factive

theorem Glass2025.discover_is_factive : Option.map classifyVeridicality English.Predicates.Verbal.discover.veridicality = some PresupClass.factive

theorem Glass2025.notice_is_factive : Option.map classifyVeridicality English.Predicates.Verbal.notice.veridicality = some PresupClass.factive

theorem Glass2025.believe_is_nonfactive : Option.map classifyVeridicality English.Predicates.Verbal.believe.veridicality = some PresupClass.nonfactive

theorem Glass2025.think_is_nonfactive : Option.map classifyVeridicality English.Predicates.Verbal.think.veridicality = some PresupClass.nonfactive

theorem Glass2025.hope_is_nonfactive : Option.map classifyVeridicality English.Predicates.Verbal.hope.veridicality = some PresupClass.nonfactive

theorem Glass2025.fear_is_nonfactive : Option.map classifyVeridicality English.Predicates.Verbal.fear.veridicality = some PresupClass.nonfactive

theorem Glass2025.yiwei_veridicality_nonfactive : Option.map classifyVeridicality Mandarin.Predicates.yiwei.veridicality = some PresupClass.nonfactive

yǐwéi is classified as nonfactive by veridicality (§5), but it has an additional postsupposition ◇¬p that is NOT derivable from veridicality. Veridicality is a derivable property of the canonical Mandarin entry; the postsupposition is [Gla25]'s paper-specific overlay, recorded here in the study rather than as a field on the Fragment entry.

inductive Glass2025.PostsupType : Type

Postsupposition type: output-context constraint distinct from presuppositions ([Gla25]). The world-type-independent tag; the concrete construct is Postsupposition (§2).

• weakContrafactive : PostsupType

  Output context must be compatible with ¬p: ◇¬p ([Gla25]).

• strongContrafactive : PostsupType

  Output context must entail ¬p: ⊨¬p (hypothetical, UNATTESTED).

@[instance_reducible]

instance Glass2025.instDecidableEqPostsupType : DecidableEq PostsupType

Equations

• Glass2025.instDecidableEqPostsupType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Glass2025.instReprPostsupType.repr : PostsupType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Glass2025.instReprPostsupType : Repr PostsupType

Equations

• Glass2025.instReprPostsupType = { reprPrec := Glass2025.instReprPostsupType.repr }

def Glass2025.yiweiPostsupType : PostsupType

[Gla25] classifies yǐwéi as carrying a weak contrafactive postsupposition. This is the paper's analytical claim about the canonical Mandarin yiwei entry — not a field on that entry.

Equations

• Glass2025.yiweiPostsupType = Glass2025.PostsupType.weakContrafactive

theorem Glass2025.yiwei_derived_nonfactive : Mandarin.Predicates.yiwei.veridicality = some Features.Veridicality.nonVeridical

yǐwéi's veridicality gives nonfactive — no presupposition.

theorem Glass2025.yiwei_postsup_not_from_veridicality : Option.map classifyVeridicality Mandarin.Predicates.yiwei.veridicality = some PresupClass.nonfactive ∧ yiweiPostsupType = PostsupType.weakContrafactive

The postsupposition IS necessary: veridicality alone gives .nonfactive (no presupposition), but yǐwéi actually has a weak contrafactive postsupposition. Pairing the canonical entry's derivable veridicality with Glass's postsupposition classification shows the two diverge — veridicality is blind to the postsupposition.

The contrafactive gap DERIVED from the Predicate Lexicalization Constraint:

• Factive (know): presup = p → PLC satisfied (p → indic(p) → B(a)(p)) ✓
• Nonfactive (think): no presupposition → PLC not applicable ✓
• Contrafactive (contra): presup = ¬p → PLC violated (¬p ↛ B(a)(p)) ✗

This is not a stipulation — it follows from the causal structure of belief formation ([RO25]).

theorem Glass2025.contrafactive_gap : presupClassIsValid PresupClass.factive = true ∧ presupClassIsValid PresupClass.nonfactive = true ∧ presupClassIsValid PresupClass.contrafactive = false

The contrafactive gap: factive and nonfactive are valid; contrafactive is invalid.

theorem Glass2025.all_english_attitude_verbs_valid : ([English.Predicates.Verbal.know, English.Predicates.Verbal.realize, English.Predicates.Verbal.discover, English.Predicates.Verbal.notice, English.Predicates.Verbal.believe, English.Predicates.Verbal.think, English.Predicates.Verbal.want, English.Predicates.Verbal.hope, English.Predicates.Verbal.expect, English.Predicates.Verbal.wish, English.Predicates.Verbal.fear, English.Predicates.Verbal.dread, English.Predicates.Verbal.worry].all fun (v : English.Predicates.Verbal.VerbEntry) => (Option.map presupClassIsValid (Option.map classifyVeridicality v.veridicality)).getD true) = true

All English attitude verbs have valid presuppositional profiles.

The full derivation chain: Fragment entry → attitude → veridicality → PresupClass → presupClassIsValid → PLC check

This section exercises the complete pipeline for representative verbs.

theorem Glass2025.know_endtoend_valid : Option.map presupClassIsValid (Option.map classifyVeridicality English.Predicates.Verbal.know.veridicality) = some true

End-to-end: "know" is factive, and factive presuppositions are valid.

theorem Glass2025.believe_endtoend_valid : Option.map presupClassIsValid (Option.map classifyVeridicality English.Predicates.Verbal.believe.veridicality) = some true

End-to-end: "believe" is nonfactive, and nonfactive is valid.

theorem Glass2025.know_presup_satisfied_endtoend : Glass2025.factiveCtx✝.all Glass2025.prop✝ = true

End-to-end: know's presupposition is satisfied in a factive context.

theorem Glass2025.know_presup_fails_endtoend : Glass2025.neutralCtx✝.all Glass2025.prop✝ = false

End-to-end: know's presupposition fails in a neutral context.

theorem Glass2025.yiwei_endtoend : (∀ w ∈ Glass2025.neutralCtx✝, Glass2025.yiweiPresup✝.presup w) ∧ Glass2025.yiweiPostsup✝.condition Glass2025.neutralCtx✝ fun (x : Glass2025.MiniWorld✝) => Glass2025.prop✝ x = true

End-to-end: yǐwéi's postsupposition is satisfied in a neutral context (where veridicality-based presupposition is vacuously OK).

[Gla25] §4.2 notes that yǐwéi supports neg-raising, like other nonfactive verbs. This follows from Veridicality: neg-raising is available for non-veridical predicates ([Gaj07], NegRaising.lean).

Since PresupClass.nonfactive verbs are exactly the non-veridical ones, the neg-raising gap aligns with the contrafactive gap.

theorem Glass2025.nonfactive_supports_negRaising : NegRaising.negRaisingAvailable Features.Veridicality.nonVeridical = true

Nonfactive verbs (including yǐwéi) support neg-raising.

theorem Glass2025.factive_blocks_negRaising : NegRaising.negRaisingAvailable Features.Veridicality.veridical = false

Factive verbs do NOT support neg-raising.

theorem Glass2025.veridicality_determines_both : presupClassIsValid PresupClass.factive = true ∧ NegRaising.negRaisingAvailable Features.Veridicality.veridical = false ∧ presupClassIsValid PresupClass.nonfactive = true ∧ NegRaising.negRaisingAvailable Features.Veridicality.nonVeridical = true

The contrafactive gap and the neg-raising gap trace to the same source: veridicality. Factives satisfy PLC but block neg-raising; nonfactives escape PLC (no presupposition) and support neg-raising.