Glass (2025): Attested versus unattested contrafactive belief verbs

Glass reframes Holton's contrafactive gap. The factive presupposition of know requires its complement to be Common Ground (EntailsP), and a contrafactive can negate that requirement in two places: with narrow scope, requiring that not-p be Common Ground (EntailsNot), or with wide scope, requiring only that the Common Ground be compatible with not-p (CompatibleNot). The stronger requirement is unattested; the weaker is the postsupposition Glass gives Mandarin yǐwéi in earlier work (yiweiDefined). Table 1, the states of the Common Ground each profile admits, is derived from the requirements (Profile.condition_iff). The profiles of know and think come from the factivity of their fragment entries, whose factive presupposition in the doxastic substrate is the requirement of the factive profile (subset_support_sentence_iff, rows_admits).

Implementation notes

• Context sets are the substrate's Set W; Table 1 depicts the Common Ground after the report is accepted, so the profiles' conditions take the updated context, the intersection with the report's at-issue content, as their argument.
• The attestation facts, no strong contrafactive and yǐwéi a weak one, are the empirical premise of the reframed question (Profile.Attested), which Roberts and Özyıldız derive causally.
• Verbs' profiles come from their fragment entries' factivity except yǐwéi's, the paper's own analysis, since the fragment records only that it is non-factive.

References

• [Gla25]
• [Gla23a]
• [Hol17]
• [RO25]
• [Bra09]
• [Sta78]

Two ways to negate the factive presupposition

def Glass2025.EntailsP {W : Type u_1} (c : Set W) (p : W → Prop) : Prop

Condition (10) is that p is Common Ground, true throughout the context set.

Equations

• Glass2025.EntailsP c p = ∀ w ∈ c, p w

def Glass2025.EntailsNot {W : Type u_1} (c : Set W) (p : W → Prop) : Prop

Condition (11) is that not-p is Common Ground.

Equations

• Glass2025.EntailsNot c p = ∀ w ∈ c, ¬p w

def Glass2025.CompatibleNot {W : Type u_1} (c : Set W) (p : W → Prop) : Prop

Condition (12) is that the Common Ground is compatible with not-p.

Equations

• Glass2025.CompatibleNot c p = ∃ w ∈ c, ¬p w

theorem Glass2025.entailsNot_iff {W : Type u_1} {c : Set W} {p : W → Prop} : EntailsNot c p ↔ ¬∃ w ∈ c, p w

(11) is the narrow-scope negation, saying that it is not possible that p.

theorem Glass2025.compatibleNot_iff {W : Type u_1} {c : Set W} {p : W → Prop} : CompatibleNot c p ↔ ¬EntailsP c p

(12) is the wide-scope negation, saying that p is not Common Ground.

theorem Glass2025.compatibleNot_of_entailsNot {W : Type u_1} {c : Set W} {p : W → Prop} (hc : c.Nonempty) (h : EntailsNot c p) : CompatibleNot c p

The stronger requirement entails the weaker on a nonempty Common Ground.

theorem Glass2025.not_entailsNot_of_compatibleNot : ∃ (c : Set Bool) (p : Bool → Prop), CompatibleNot c p ∧ ¬EntailsNot c p

The weaker requirement does not entail the stronger.

theorem Glass2025.not_entailsP_and_entailsNot {W : Type u_1} {c : Set W} {p : W → Prop} (hc : c.Nonempty) : ¬(EntailsP c p ∧ EntailsNot c p)

know and contra are complementary on a nonempty Common Ground.

theorem Glass2025.know_contra_gap : ∃ (c : Set Bool) (p : Bool → Prop), ¬EntailsP c p ∧ ¬EntailsNot c p

A Common Ground on which p is unsettled satisfies neither the know nor the contra requirement, the gap between them.

theorem Glass2025.not_entailsP_and_compatibleNot {W : Type u_1} {c : Set W} {p : W → Prop} : ¬(EntailsP c p ∧ CompatibleNot c p)

know and yǐwéi are complementary.

theorem Glass2025.know_yiwei_exhaustive {W : Type u_1} {c : Set W} {p : W → Prop} : EntailsP c p ∨ CompatibleNot c p

know and yǐwéi exhaust the space, since p is Common Ground or it is not.

yǐwéi's postsupposition

def Glass2025.yiweiDefined {W : Type u_1} (c belief : Set W) (p : W → Prop) : Prop

By (14), x yǐwéi p updates the Common Ground with x's belief that p, and is defined only if the result is compatible with not-p, a postsupposition in the sense of [Bra09].

Equations

• Glass2025.yiweiDefined c belief p = Glass2025.CompatibleNot (c ∩ belief) p

theorem Glass2025.entailsNot_of_opinionated {W : Type u_1} {c : Set W} {p : W → Prop} (h : EntailsP c p ∨ EntailsNot c p) (hy : CompatibleNot c p) : EntailsNot c p

A speaker with an opinion about p, whose Common Ground entails it or its negation, and who signals that the Common Ground is compatible with not-p, holds that not-p, which is why x yǐwéi p usually conveys that p is false.

Table 1

inductive Glass2025.Profile : Type

The projective profiles of belief verbs require p (know), nothing (think), compatibility with not-p (yǐwéi), or not-p (the hypothetical contra).

• factive : Profile
• nonfactive : Profile
• weakContrafactive : Profile
• strongContrafactive : Profile

@[instance_reducible]

instance Glass2025.instDecidableEqProfile : DecidableEq Profile

Equations

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

@[instance_reducible]

instance Glass2025.instReprProfile : Repr Profile

Equations

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

def Glass2025.instReprProfile.repr : Profile → ℕ → Std.Format

Equations

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

def Glass2025.Profile.condition {W : Type u_1} : Profile → Set W → (W → Prop) → Prop

The requirement a profile places on the Common Ground after the report is accepted.

Equations

• Glass2025.Profile.factive.condition x✝¹ x✝ = Glass2025.EntailsP x✝¹ x✝
• Glass2025.Profile.nonfactive.condition x✝¹ x✝ = True
• Glass2025.Profile.weakContrafactive.condition x✝¹ x✝ = Glass2025.CompatibleNot x✝¹ x✝
• Glass2025.Profile.strongContrafactive.condition x✝¹ x✝ = Glass2025.EntailsNot x✝¹ x✝

inductive Glass2025.State : Type

The states of the Common Ground regarding p distinguished in Table 1.

• p : State
• unsettled : State
• notP : State

@[instance_reducible]

instance Glass2025.instDecidableEqState : DecidableEq State

Equations

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

@[instance_reducible]

instance Glass2025.instReprState : Repr State

Equations

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

def Glass2025.instReprState.repr : State → ℕ → Std.Format

Equations

• Glass2025.instReprState.repr Glass2025.State.p prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Glass2025.State.p")).group prec✝
• Glass2025.instReprState.repr Glass2025.State.unsettled prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Glass2025.State.unsettled")).group prec✝
• Glass2025.instReprState.repr Glass2025.State.notP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Glass2025.State.notP")).group prec✝

noncomputable def Glass2025.state {W : Type u_1} (c : Set W) (p : W → Prop) : State

The state of a Common Ground regarding p.

Equations

• Glass2025.state c p = if Glass2025.EntailsP c p then Glass2025.State.p else if Glass2025.EntailsNot c p then Glass2025.State.notP else Glass2025.State.unsettled

def Glass2025.Profile.Admits : Profile → State → Prop

The states each profile admits, the rows of Table 1.

Equations

• Glass2025.Profile.factive.Admits x✝ = (x✝ = Glass2025.State.p)
• Glass2025.Profile.nonfactive.Admits x✝ = True
• Glass2025.Profile.weakContrafactive.Admits x✝ = (x✝ ≠ Glass2025.State.p)
• Glass2025.Profile.strongContrafactive.Admits x✝ = (x✝ = Glass2025.State.notP)

@[instance_reducible]

instance Glass2025.instDecidableAdmits (pr : Profile) (s : State) : Decidable (pr.Admits s)

Equations

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

theorem Glass2025.Profile.condition_iff {W : Type u_1} {c : Set W} {p : W → Prop} (hc : c.Nonempty) (pr : Profile) : pr.condition c p ↔ pr.Admits (state c p)

Table 1 as a theorem. On a nonempty Common Ground, a profile's requirement holds exactly when the profile admits the Common Ground's state.

def Glass2025.Profile.Attested : Profile → Prop

Every profile but the strong contrafactive is attested, by know, think and yǐwéi; this is the empirical premise of the reframed question.

Equations

• Glass2025.Profile.strongContrafactive.Attested = False
• x✝.Attested = True

@[instance_reducible]

instance Glass2025.instDecidablePredProfileAttested : DecidablePred Profile.Attested

Equations

• Glass2025.instDecidablePredProfileAttested Glass2025.Profile.strongContrafactive = isFalse Glass2025.instDecidablePredProfileAttested._proof_1
• Glass2025.instDecidablePredProfileAttested Glass2025.Profile.factive = isTrue trivial
• Glass2025.instDecidablePredProfileAttested Glass2025.Profile.nonfactive = isTrue trivial
• Glass2025.instDecidablePredProfileAttested Glass2025.Profile.weakContrafactive = isTrue trivial

The verbs

def Glass2025.Profile.ofFactivity : Option Presupposition.Factivity → Profile

A factivity class determines a profile, requiring the complement of a factive and nothing of a non-factive; postsuppositions are invisible to it.

Equations

• Glass2025.Profile.ofFactivity (some val) = Glass2025.Profile.factive
• Glass2025.Profile.ofFactivity none = Glass2025.Profile.nonfactive

theorem Glass2025.subset_support_sentence_iff {W : Type u_1} {c : Set W} {p : W → Prop} {E : Type u_2} (V : Doxastic.DoxasticPredicate W E) (a : E) : c ⊆ Function.support (V.sentence a p) ↔ (Profile.ofFactivity V.factivity).condition c p

A doxastic predicate's presupposition is admitted exactly when the requirement of the profile its factivity determines holds, for a factive the requirement (10) that the complement be Common Ground.

def Glass2025.yiweiProfile : Profile

yǐwéi's profile on the paper's analysis, beyond the non-factivity its fragment entry records.

Equations

• Glass2025.yiweiProfile = Glass2025.Profile.weakContrafactive

theorem Glass2025.know_profile : Profile.ofFactivity English.Verbs.know.factivity = Profile.factive

theorem Glass2025.think_profile : Profile.ofFactivity English.Verbs.think.factivity = Profile.nonfactive

theorem Glass2025.yiwei_profile_ofFactivity : Profile.ofFactivity Mandarin.yiwei.factivity = Profile.nonfactive

The fragment's factivity alone makes yǐwéi nonfactive.

structure Glass2025.Row : Type

A belief report of the paper records the verb's profile, the state of the Common Ground in the context described, and the reported judgment.

• profile : Profile
• state : State
• judgment : Judgment

def Glass2025.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Glass2025.instDecidableEqRow : DecidableEq Row

Equations

• Glass2025.instDecidableEqRow = Glass2025.instDecidableEqRow.decEq

def Glass2025.verbProfiles : List (String × Profile)

The rows' verbs know, think and rènwéi take their profiles from their fragment entries' factivity, and yǐwéi from the paper's analysis.

Equations

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

def Glass2025.Row.ofDatum (ex : Datum) : Option Row

Equations

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

def Glass2025.rows : List Row

The nine reports of (1), (2), (4), (5) and (7).

Equations

• Glass2025.rows = List.filterMap Glass2025.Row.ofDatum Glass2025.Examples.all

theorem Glass2025.rows_admits (r : Row) : r ∈ rows → (r.judgment = Judgment.acceptable ↔ r.profile.Admits r.state)

The reports are judged acceptable exactly in the states their profiles admit.