Documentation

Linglib.Studies.DegenTonhauser2022

[DT22]: Are There Factive Predicates? #

Six experiments testing whether the twenty clause-embedding predicates of [DT21] contain a coherent class of factive predicates under either standard definition: the clausal complement's content (CC) is presupposed (3a, [KK70]), or presupposed and entailed (3b). The paper's traditional four-way classification (13) is traditionalClass. Definition 3a expects the certainty ratings of canonically factive predicates to be categorically higher than those of all other predicates — Separates, which over a finite domain holds iff some threshold puts exactly the factive class on top (separates_iff_exists_threshold).

The data refute that expectation in both response tasks: the optionally factive inform outrates the canonically factive reveal (0.81 vs 0.70 in experiment 1a, 0.90 vs 0.69 in 1b), so the ratings do not separate the class and no nonarbitrary line can be drawn (certainty1a_not_separated, certainty1a_no_threshold; likewise for 1b). The entailment experiments undermine definition 3b: in experiment 2a only be right and prove rated with the entailed controls, yet both project below every canonically factive predicate (entailment_projection_dissociation); experiment 2b adds know, see, discover, and confirm — a heterogeneous class — and the contradictoriness experiments 3a/3b identify no entailed CCs at all. The paper concludes that no coherent class of factive predicates is supported, while cautioning (objection 3) that gradient ratings alone cannot rule out a binary category plus lexical ambiguity. The results bear on projection analyses ([Hei83], [vdS92]) whose explanandum is delimited by exactly this class.

Per-predicate mean ratings (certainty1a, certainty1b, inference2a) are stored as ℚ, so comparisons close by norm_num; the traditional classification agrees with the Fragment's factivity flags (traditionalClass_consistent_with_fragment).

The traditional classification #

inductive DegenTonhauser2022.TraditionalClass :

The traditional four-way classification of the twenty clause-embedding predicates ((13) of [DT22]), by whether the complement content is taken to be presupposed and entailed.

factive : TraditionalClass
CC presupposed (and, on definition 3b, entailed): know, discover, ...
nonveridicalNonfactive : TraditionalClass
CC neither presupposed nor entailed: think, say, ...
veridicalNonfactive : TraditionalClass
CC entailed but not presupposed: be right, demonstrate.
optionallyFactive : TraditionalClass
CC only sometimes presupposed: acknowledge, admit, ...

Instances For

@[instance_reducible]

instance DegenTonhauser2022.instDecidableEqTraditionalClass :

DecidableEq TraditionalClass

Equations

DegenTonhauser2022.instDecidableEqTraditionalClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DegenTonhauser2022.instReprTraditionalClass :

Repr TraditionalClass

Equations

DegenTonhauser2022.instReprTraditionalClass = { reprPrec := DegenTonhauser2022.instReprTraditionalClass.repr }

def DegenTonhauser2022.instReprTraditionalClass.repr :

TraditionalClass → ℕ → Std.Format

Equations

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

Instances For

def DegenTonhauser2022.traditionalClass :

DegenTonhauser2021.Predicate → TraditionalClass

The classification in (13).

Equations

Instances For

Categorical distinction as separation #

def DegenTonhauser2022.Separates {α : Type u_1} {β : Type u_2} [LinearOrder β] (cls : α → Prop) (rating : α → β) :

Every in-class element outrates every out-of-class element.

Equations

DegenTonhauser2022.Separates cls rating = ∀ ⦃p q : α⦄, cls p → ¬cls q → rating q < rating p

Instances For

theorem DegenTonhauser2022.not_separates {α : Type u_1} {β : Type u_2} [LinearOrder β] {cls : α → Prop} {rating : α → β} {p q : α} (hp : cls p) (hq : ¬cls q) (hpq : rating p ≤ rating q) :

¬Separates cls rating

An out-of-class element rating at least as high as an in-class one defeats separation.

theorem DegenTonhauser2022.separates_iff_exists_threshold {α : Type u_1} {β : Type u_2} [LinearOrder β] {cls : α → Prop} {rating : α → β} [Fintype α] [DecidablePred cls] (h : ∃ (q : α), ¬cls q) :

Separates cls rating ↔ ∃ (t : β), ∀ (p : α), cls p ↔ t < rating p

A class is separated by a rating iff some threshold puts exactly the class above it; the separating threshold is the top out-of-class rating.

Data: certainty and inference ratings #

Computed from the authors' data at github.com/judith-tonhauser/projective-probability, rounded to two decimals and listed in descending order as in the paper's figures.

def DegenTonhauser2022.certainty1a :

DegenTonhauser2021.Predicate → ℚ

Mean certainty rating, experiment 1a ('certain that', gradient slider; Figure 2). From results/5-projectivity-no-fact (n = 266; main-clause control mean 0.11).

Equations

Instances For

def DegenTonhauser2022.certainty1b :

DegenTonhauser2021.Predicate → ℚ

Proportion of 'yes' responses, experiment 1b ('certain that', forced choice; Figure 4). From results/8-projectivity-no-fact-binary (n = 436; main-clause control mean 0.00).

Equations

Instances For

def DegenTonhauser2022.inference2a :

DegenTonhauser2021.Predicate → ℚ

Mean inference rating, experiment 2a ('does it follow', gradient slider; Figure 9). From results/4-veridicality3 (n = 259; entailing control mean 0.96, non-entailing 0.03).

Equations

Instances For

No categorical projection distinction (definition 3a) #

theorem DegenTonhauser2022.certainty1a_not_separated :

¬Separates (fun (x : DegenTonhauser2021.Predicate) => traditionalClass x = TraditionalClass.factive) certainty1a

The exp 1a certainty ratings do not separate the canonically factive class: the optionally factive inform (0.81) outrates the factive reveal (0.70).

theorem DegenTonhauser2022.certainty1a_no_threshold :

¬∃ (t : ℚ), ∀ (p : DegenTonhauser2021.Predicate), traditionalClass p = TraditionalClass.factive ↔ t < certainty1a p

No threshold recovers the classification from the exp 1a ratings — the paper's "nonarbitrary line" argument.

theorem DegenTonhauser2022.certainty1b_not_separated :

¬Separates (fun (x : DegenTonhauser2021.Predicate) => traditionalClass x = TraditionalClass.factive) certainty1b

The forced-choice replication (exp 1b) does not separate the class either: inform at 0.90 vs reveal at 0.69.

theorem DegenTonhauser2022.certainty1b_no_threshold :

¬∃ (t : ℚ), ∀ (p : DegenTonhauser2021.Predicate), traditionalClass p = TraditionalClass.factive ↔ t < certainty1b p

No threshold recovers the classification from the exp 1b ratings.

Entailment vs projection (definition 3b) #

Definition 3b's best contenders are the least projective: be right and prove carry the top exp 2a inference ratings yet project below every canonically factive predicate.

Fragment bridge #

theorem DegenTonhauser2022.factive_entries_have_factivePresup :

English.Predicates.Verbal.know.factivePresup = true ∧ English.Predicates.Verbal.discover.factivePresup = true ∧ English.Predicates.Verbal.see.factivePresup = true ∧ English.Predicates.Verbal.reveal.factivePresup = true

Canonically factive verbs have factivePresup = true in the Fragment, matching (13); the copular "be annoyed" is covered by copular_presup_matches_classification.

theorem DegenTonhauser2022.nonfactive_entries_lack_factivePresup :

English.Predicates.Verbal.pretend.factivePresup = false ∧ English.Predicates.Verbal.suggest.factivePresup = false ∧ English.Predicates.Verbal.say.factivePresup = false ∧ English.Predicates.Verbal.think.factivePresup = false

Nonveridical nonfactive verbs have factivePresup = false in the Fragment.

theorem DegenTonhauser2022.traditionalClass_consistent_with_fragment (p : DegenTonhauser2021.Predicate) (v : English.Predicates.Verbal.VerbEntry) (h : DegenTonhauser2021.toVerbEntry p = some v) :

(traditionalClass p = TraditionalClass.factive → v.factivePresup = true) ∧ (traditionalClass p = TraditionalClass.nonveridicalNonfactive → v.factivePresup = false)

The traditional classification matches Fragment factivity: factive verbs have factivePresup = true, nonveridical nonfactives false.

theorem DegenTonhauser2022.copular_presup_matches_classification :

(DegenTonhauser2021.toPredicateCore DegenTonhauser2021.Predicate.beAnnoyed).isPresupTrigger = true ∧ (DegenTonhauser2021.toPredicateCore DegenTonhauser2021.Predicate.beRight).isPresupTrigger = false

"be annoyed" is a presupposition trigger while "be right" is not, matching (13).