Documentation

Studies.DegenTonhauser2022

Degen and Tonhauser (2022): Are there factive predicates? An empirical investigation #

A clause-embedding predicate is factive, on Kiparsky and Kiparsky's definition, when the content of its complement is presupposed, and on Gazdar's when that content is presupposed and entailed. Degen and Tonhauser test both definitions on twenty English predicates, diagnosing presupposition by projection and entailment by inference and by contradictoriness, each under a gradient and a categorical response task. On the first definition the canonically factive predicates should project categorically more than the rest, and they do not: the optionally factive acknowledge, hear and inform project at least as much as reveal. On the second, every complement projects, so the factive predicates are those with entailed complements, and under every diagnostic and task these are none, or not categorically more projective than the rest.

Main statements #

not_exists_threshold: no threshold on the certainty ratings picks out the canonically factive predicates, under either task.
factive_eq_empty_or_not_separates: the predicates whose complement is both projective and entailed are none, or not categorically more projective than the rest.
isFactive_iff: the predicates the English lexicon marks factive are the canonically factive ones.

Implementation notes #

A class is categorically more projective when every member's mean certainty rating exceeds every non-member's, Separates; over finitely many predicates this is a threshold on the ratings.
Projective and entailed are the paper's verdicts from its regressions: a complement projects when its ratings are distinguished from the main-clause controls', and is entailed when they are not distinguished from those of the controls with entailed content.

References #

The predicates in the lexicon #

def DegenTonhauser2022.entry :

Predicate → Verb

The English lexical entry of a predicate.

Equations

Instances For

def DegenTonhauser2022.Category.predicates (c : Category) :

The predicates of a category of the paper's classification.

Equations

c.predicates = {p : DegenTonhauser2022.Predicate | p ∈ (DegenTonhauser2022.classification c).predicates}

Instances For

@[instance_reducible]

instance DegenTonhauser2022.instDecidablePredPredicateMemSetPredicates (c : Category) :

DecidablePred fun (x : Predicate) => x ∈ c.predicates

Equations

DegenTonhauser2022.instDecidablePredPredicateMemSetPredicates c p = { decide := decide (List.elem p (DegenTonhauser2022.classification c).predicates = true), reflects_decide := ⋯ }

theorem DegenTonhauser2022.isFactive_iff {p : Predicate} :

(entry p).IsFactive ↔ p ∈ Category.canonicallyFactive.predicates

The English lexicon marks factive exactly the canonically factive predicates.

theorem DegenTonhauser2022.isTrigger_iff {p : Predicate} :

(entry p).IsTrigger ↔ (entry p).IsFactive

The lexicon's presupposition triggers among the twenty are its factive predicates.

Categorical distinctions #

def DegenTonhauser2022.Separates {α : Type u_1} {β : Type u_2} [LinearOrder β] (s : Set α) (f : α → β) :

A rating separates a class when it rates every member above every non-member.

Equations

DegenTonhauser2022.Separates s f = ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∉ s → f b < f a

Instances For

theorem DegenTonhauser2022.not_separates_of_le {α : Type u_1} {β : Type u_2} [LinearOrder β] {s : Set α} {f : α → β} {a b : α} (ha : a ∈ s) (hb : b ∉ s) (h : f a ≤ f b) :

¬Separates s f

theorem DegenTonhauser2022.separates_iff_exists_threshold {α : Type u_1} {β : Type u_2} [LinearOrder β] {s : Set α} {f : α → β} [Finite α] (h : sᶜ.Nonempty) :

Separates s f ↔ ∃ (t : β), s = f ⁻¹' Set.Ioi t

Over finitely many items, a rating separates a class with a non-member iff the class is everything the rating puts above some threshold.

Factive as presupposed #

def DegenTonhauser2022.certaintyMean (t : Task) (p : Predicate) :

ℚ

The mean certainty rating of a predicate's complement under a task.

Equations

DegenTonhauser2022.certaintyMean t p = (DegenTonhauser2022.certainty t p).mean.toRat

Instances For

def DegenTonhauser2022.Projects (t : Task) (p : Predicate) :

A predicate's complement projects under a task when its certainty ratings are distinguished from the main-clause controls'.

Equations

DegenTonhauser2022.Projects t p = (p ∉ (DegenTonhauser2022.projectionResults t).indistinguishable)

Instances For

@[instance_reducible]

instance DegenTonhauser2022.instDecidablePredPredicateProjects (t : Task) :

DecidablePred (Projects t)

Equations

DegenTonhauser2022.instDecidablePredPredicateProjects t x✝ = { decide := !decide (x✝ ∈ (DegenTonhauser2022.projectionResults t).indistinguishable), reflects_decide := ⋯ }

theorem DegenTonhauser2022.projects (t : Task) (p : Predicate) :

Every complement projects, so the canonically factive class has to be drawn within the ratings.

theorem DegenTonhauser2022.certaintyMean_reveal_le_iff (t : Task) (p : Predicate) :

certaintyMean t Predicate.reveal ≤ certaintyMean t p ↔ p ∈ Category.canonicallyFactive.predicates ∨ p ∈ [Predicate.acknowledge, Predicate.hear, Predicate.inform]

The complements at least as projective as that of reveal are those of the canonically factive predicates and of the optionally factive acknowledge, hear and inform, under either task.

theorem DegenTonhauser2022.certaintyMean_lt_of_mem_of_not_mem {t : Task} {p q : Predicate} (hp : p ∈ Category.canonicallyFactive.predicates) (hq : q ∉ Category.canonicallyFactive.predicates) (hq' : q ∉ [Predicate.acknowledge, Predicate.hear, Predicate.inform]) :

certaintyMean t q < certaintyMean t p

With acknowledge, hear and inform set aside, the canonically factive predicates are categorically more projective than the rest.

theorem DegenTonhauser2022.not_separates_certaintyMean (t : Task) :

¬Separates Category.canonicallyFactive.predicates (certaintyMean t)

theorem DegenTonhauser2022.not_exists_threshold (t : Task) :

¬∃ (θ : ℚ), Category.canonicallyFactive.predicates = certaintyMean t ⁻¹' Set.Ioi θ

No threshold on either task's certainty ratings picks out the canonically factive predicates.

Factive as presupposed and entailed #

def DegenTonhauser2022.Entailed (d : Diagnostic) (t : Task) (p : Predicate) :

A predicate's complement is entailed under a diagnostic and task when its ratings are not distinguished from those of the controls with entailed content.

Equations

DegenTonhauser2022.Entailed d t p = (p ∈ (DegenTonhauser2022.entailmentResults d t).indistinguishable)

Instances For

@[instance_reducible]

instance DegenTonhauser2022.instDecidablePredPredicateEntailed (d : Diagnostic) (t : Task) :

DecidablePred (Entailed d t)

Equations

DegenTonhauser2022.instDecidablePredPredicateEntailed d t x✝ = { decide := decide (List.elem x✝ (DegenTonhauser2022.entailmentResults d t).indistinguishable = true), reflects_decide := ⋯ }

theorem DegenTonhauser2022.factive_eq_empty_or_not_separates (d : Diagnostic) (t t' : Task) :

{p : Predicate | Projects t' p ∧ Entailed d t p} = ∅ ∨ ¬Separates {p : Predicate | Projects t' p ∧ Entailed d t p} (certaintyMean t')

Under either diagnostic and task, no complement is projective and entailed, or the entailed complement of be right projects less than the nonentailed one of say.

theorem DegenTonhauser2022.certaintyMean_lt_of_entailed {t : Task} {p q : Predicate} (hp : Entailed Diagnostic.inference Task.gradient p) (hq : q ∈ Category.canonicallyFactive.predicates) :

certaintyMean t p < certaintyMean t q

The best contenders on the second definition, be right and prove, whose complements alone the gradient inference ratings leave entailed, project less than every canonically factive predicate.