Glass (2025): Attested versus unattested contrafactive belief verbs #
Semantics and Pragmatics 18, Article 8: 1-17.
Key Claims #
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).
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).
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.
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 separate
Semantics.Dynamic.Postsupposition value. The PresupClass classification and PLC
validation from Doxastic.lean derive the contrafactive gap.
Minimal 2-world model for exercising Table 1.
w0: p is truew1: p is false
Equations
- Glass2025.instDecidableEqMiniWorld x✝ y✝ = if h : Glass2025.MiniWorld.ctorIdx✝ x✝ = Glass2025.MiniWorld.ctorIdx✝ y✝ then isTrue ⋯ else isFalse ⋯
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Glass2025.instReprMiniWorld = { reprPrec := Glass2025.instReprMiniWorld.repr }
Equations
- Glass2025.instInhabitedMiniWorld = { default := Glass2025.instInhabitedMiniWorld.default }
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.
Each English/Mandarin attitude verb's PresupClass is DERIVED from its
veridicality in the Fragment entry. These theorems will BREAK if:
- A verb's
attitudechanges - The
classifyVeridicalityfunction changes - The
veridicalityderivation fromAttitudechanges
yǐwéi is classified as nonfactive by veridicality (§4), 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.
Postsupposition type: output-context constraint distinct from
presuppositions ([Gla25]). The world-type-independent tag; the
concrete construct is Semantics.Dynamic.Postsupposition.
- weakContrafactive : PostsupType
Output context must be compatible with ¬p: ◇¬p ([Gla25]).
- strongContrafactive : PostsupType
Output context must entail ¬p: ⊨¬p (hypothetical, UNATTESTED).
Instances For
Equations
- Glass2025.instDecidableEqPostsupType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- Glass2025.instReprPostsupType = { reprPrec := Glass2025.instReprPostsupType.repr }
Equations
- One or more equations did not get rendered due to their size.
Instances For
[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.
Instances For
yǐwéi's veridicality gives nonfactive — no presupposition.
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]).
The contrafactive gap: factive and nonfactive are valid; contrafactive is invalid.
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.
End-to-end: "know" is factive, and factive presuppositions are valid.
End-to-end: "believe" is nonfactive, and nonfactive is valid.
End-to-end: know's presupposition is satisfied in a factive context.
End-to-end: know's presupposition fails in a neutral context.
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.
Nonfactive verbs (including yǐwéi) support neg-raising.
Factive verbs do NOT support neg-raising.
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.