Tonhauser, Beaver and Degen (2018): How Projective Is Projective Content? Gradience in Projectivity and At-Issueness

Tonhauser, Beaver and Degen's Gradient Projection Principle says that content embedded under an entailment-cancelling operator projects to the extent that it is not at-issue. Projectivity and at-issueness are gradient, measured on the unit interval, so the principle is the involution Set.Icc.symm (gppProjection); restricted to binary at-issueness it is the Projection Principle of Simons, Tonhauser, Beaver and Roberts, that content projects iff it is not at-issue (gppProjection_eq_one_iff). The categorical analyses the paper reviews predict projection at the ceiling (ceilingProjection).

Against the observed means of Data.Experiments.TonhauserBeaverDegen2018, the principle is the closer account on every content but the pre-state of stop (gpp_closer_than_ceiling, ceiling_closer_on_stop), the effect it predicts holds in all four experiments (atIssuenessEffect_beta_pos), and the printed Tukey comparisons divide the contents into more than two projectivity classes, cutting across the hard/soft classification (three_classes, soft_not_a_class, hard_soft_indistinguishable).

Implementation notes

• Degrees are Set.Icc (0 : ℚ) 1: the observations are printed decimals, read through Decimal.toRat, and every comparison is exact ℚ arithmetic closed by decide +kernel.
• The paper's own test of the principle is the sign and size of the at-issueness effect in its regressions, kept as data in atIssuenessEffect; the error comparison against the ceiling is the paper's review of categorical analyses at the granularity this file can check. No theorem re-thresholds a printed p-value.
• Distinguished reads the paper's printed Tukey verdicts; what counts as distinguished is the paper's mark, not a recomputed test. The paper leaves open whether at-issueness causes projection.

References

• [TBD18]
• [STBR10]
• [BRST17]
• [Kar73]
• [Gaz79]
• [Hei83]
• [vdS92]
• [Pot05]

The Gradient Projection Principle

def TonhauserBeaverDegen2018.gppProjection : ↑(Set.Icc 0 1) → ↑(Set.Icc 0 1)

By (7), content projects to the extent that it is not at-issue.

Equations

• TonhauserBeaverDegen2018.gppProjection = Set.Icc.symm

theorem TonhauserBeaverDegen2018.gppProjection_antitone : Antitone gppProjection

More not-at-issue content is more projective.

theorem TonhauserBeaverDegen2018.gppProjection_lt_iff {a b : ↑(Set.Icc 0 1)} : gppProjection a < gppProjection b ↔ b < a

The principle's order prediction, strictly.

theorem TonhauserBeaverDegen2018.gppProjection_eq_one_iff {ai : ↑(Set.Icc 0 1)} : gppProjection ai = 1 ↔ ai = 0

Restricted to binary at-issueness, the principle is the Projection Principle: content projects fully iff it is not at-issue at all.

theorem TonhauserBeaverDegen2018.gppProjection_eq_zero_iff {ai : ↑(Set.Icc 0 1)} : gppProjection ai = 0 ↔ ai = 1

Fully at-issue content does not project.

Projection at the ceiling

def TonhauserBeaverDegen2018.ceilingProjection : ↑(Set.Icc 0 1) → ↑(Set.Icc 0 1)

Projection at the ceiling whatever the at-issueness: what [Kar73], [Gaz79] and global accommodation predict for a presupposition not under a plug or a filter, and [Pot05] for a conventional implicature.

Equations

• TonhauserBeaverDegen2018.ceilingProjection x✝ = 1

@[simp]

theorem TonhauserBeaverDegen2018.ceilingProjection_val (ai : ↑(Set.Icc 0 1)) : ↑(ceilingProjection ai) = 1

theorem TonhauserBeaverDegen2018.gppProjection_eq_ceiling_iff {ai : ↑(Set.Icc 0 1)} : gppProjection ai = ceilingProjection ai ↔ ai = 0

The principle and the ceiling agree exactly on fully not-at-issue content.

The observed degrees

The by-expression means are rationals in the unit interval, lifted to Set.Icc (0 : ℚ) 1 once and for all.

theorem TonhauserBeaverDegen2018.heterogeneous_mem (e : Expression) : (heterogeneous e).projectivity.toRat ∈ Set.Icc 0 1 ∧ (heterogeneous e).notAtIssueness.toRat ∈ Set.Icc 0 1

theorem TonhauserBeaverDegen2018.predicates_mem (p : Predicate) : (predicates p).projectivity.toRat ∈ Set.Icc 0 1 ∧ (predicates p).notAtIssueness.toRat ∈ Set.Icc 0 1

def TonhauserBeaverDegen2018.Expression.projectivity (e : Expression) : ↑(Set.Icc 0 1)

The observed projectivity of a heterogeneous expression's content, Experiment 1a.

Equations

• e.projectivity = ⟨(TonhauserBeaverDegen2018.heterogeneous e).projectivity.toRat, ⋯⟩

def TonhauserBeaverDegen2018.Expression.notAtIssueness (e : Expression) : ↑(Set.Icc 0 1)

Its observed not-at-issueness.

Equations

• e.notAtIssueness = ⟨(TonhauserBeaverDegen2018.heterogeneous e).notAtIssueness.toRat, ⋯⟩

def TonhauserBeaverDegen2018.Expression.atIssueness (e : Expression) : ↑(Set.Icc 0 1)

Its observed at-issueness: the released data code the asking-whether response so that 1 is not-at-issue.

Equations

• e.atIssueness = Set.Icc.symm e.notAtIssueness

def TonhauserBeaverDegen2018.Predicate.projectivity (p : Predicate) : ↑(Set.Icc 0 1)

The observed projectivity of a predicate's complement, Experiment 1b.

Equations

• p.projectivity = ⟨(TonhauserBeaverDegen2018.predicates p).projectivity.toRat, ⋯⟩

def TonhauserBeaverDegen2018.Predicate.notAtIssueness (p : Predicate) : ↑(Set.Icc 0 1)

Its observed not-at-issueness.

Equations

• p.notAtIssueness = ⟨(TonhauserBeaverDegen2018.predicates p).notAtIssueness.toRat, ⋯⟩

def TonhauserBeaverDegen2018.Predicate.atIssueness (p : Predicate) : ↑(Set.Icc 0 1)

Its observed at-issueness.

Equations

• p.atIssueness = Set.Icc.symm p.notAtIssueness

theorem TonhauserBeaverDegen2018.gppProjection_atIssueness (e : Expression) : gppProjection e.atIssueness = e.notAtIssueness

On observed at-issueness the principle predicts exactly the observed not-at-issueness.

Errors on the observations

def TonhauserBeaverDegen2018.error (f : ↑(Set.Icc 0 1) → ↑(Set.Icc 0 1)) (a p : ↑(Set.Icc 0 1)) : ℚ

The absolute error of an account on content observed at at-issueness a and projectivity p.

Equations

• TonhauserBeaverDegen2018.error f a p = |↑(f a) - ↑p|

theorem TonhauserBeaverDegen2018.gpp_closer_iff (a p : ↑(Set.Icc 0 1)) : error gppProjection a p < error ceilingProjection a p ↔ ↑(Set.Icc.symm a) < 1 ∧ 2 * ↑p < 1 + ↑(Set.Icc.symm a)

The principle beats the ceiling exactly on content observed below the midpoint between its not-at-issueness and the ceiling; on fully not-at-issue content the two coincide.

theorem TonhauserBeaverDegen2018.nrrc_more_projective_than_discover : Expression.nrrc.atIssueness < Expression.discover.atIssueness ∧ gppProjection Expression.discover.atIssueness < gppProjection Expression.nrrc.atIssueness ∧ Expression.discover.projectivity < Expression.nrrc.projectivity

On the paper's worked prediction, the content of an NRRC is more not-at-issue than the complement of discover, so the principle predicts it more projective, and it is.

theorem TonhauserBeaverDegen2018.gpp_closer_than_ceiling (e : Expression) (h : e ≠ Expression.stop) : error gppProjection e.atIssueness e.projectivity < error ceilingProjection e.atIssueness e.projectivity

The principle is the closer account on every Experiment 1a expression but stop.

theorem TonhauserBeaverDegen2018.ceiling_closer_on_stop : error ceilingProjection Expression.stop.atIssueness Expression.stop.projectivity < error gppProjection Expression.stop.atIssueness Expression.stop.projectivity

The pre-state of stop, the least not-at-issue content on the asking-whether diagnostic yet highly projective: its projectivity .87 exceeds the midpoint .855 of gpp_closer_iff, and the ceiling is the closer account.

theorem TonhauserBeaverDegen2018.gpp_closer_than_ceiling_predicates (p : Predicate) : error gppProjection p.atIssueness p.projectivity < error ceilingProjection p.atIssueness p.projectivity

On the twelve predicates of Experiment 1b the principle is closer throughout.

theorem TonhauserBeaverDegen2018.atIssuenessEffect_beta_pos (x : Experiment) : 0 < (atIssuenessEffect x).beta.toRat

The at-issueness coefficient is positive in all four experiments, the direction the principle predicts; the paper reports it significant in all but Experiment 2b.

Projectivity classes from the printed comparisons

def TonhauserBeaverDegen2018.Expression.Distinguished (a b : Expression) : Prop

Two Experiment 1a contents' projectivity means are distinguished by the printed Tukey comparison.

Equations

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

@[instance_reducible]

instance TonhauserBeaverDegen2018.instDecidableRelExpressionDistinguished : DecidableRel Expression.Distinguished

Equations

• TonhauserBeaverDegen2018.instDecidableRelExpressionDistinguished x✝¹ x✝ = TonhauserBeaverDegen2018.instDecidableRelExpressionDistinguished._aux_1 x✝¹ x✝

def TonhauserBeaverDegen2018.Predicate.Distinguished (a b : Predicate) : Prop

Two Experiment 1b complements' projectivity means are distinguished.

Equations

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

@[instance_reducible]

instance TonhauserBeaverDegen2018.instDecidableRelPredicateDistinguished : DecidableRel Predicate.Distinguished

Equations

• TonhauserBeaverDegen2018.instDecidableRelPredicateDistinguished x✝¹ x✝ = TonhauserBeaverDegen2018.instDecidableRelPredicateDistinguished._aux_1 x✝¹ x✝

theorem TonhauserBeaverDegen2018.three_classes : Expression.nrrc.Distinguished Expression.stop ∧ Expression.stop.Distinguished Expression.only ∧ Expression.nrrc.Distinguished Expression.only

The projective contents fall into more than two projectivity classes: the content of NRRCs, the pre-state of stop and the prejacent of only are pairwise distinguished.

theorem TonhauserBeaverDegen2018.know_indistinguishable_from_annoyed : ¬Expression.know.Distinguished Expression.annoyed

The complement of know is statistically indistinguishable in projectivity from that of the hard-triggering factive be annoyed.

def TonhauserBeaverDegen2018.Expression.hardness? : Expression → Option Presupposition.Hardness

The hard/soft classification the paper checks its ranking against, as it cites it for the Experiment 1a contents: be annoyed is a hard trigger, and discover, stop and only are soft triggers.

Equations

• TonhauserBeaverDegen2018.Expression.annoyed.hardness? = some Presupposition.Hardness.hard
• TonhauserBeaverDegen2018.Expression.discover.hardness? = some Presupposition.Hardness.soft
• TonhauserBeaverDegen2018.Expression.stop.hardness? = some Presupposition.Hardness.soft
• TonhauserBeaverDegen2018.Expression.only.hardness? = some Presupposition.Hardness.soft
• x✝.hardness? = none

theorem TonhauserBeaverDegen2018.some_differences_align : Expression.discover.Distinguished Expression.annoyed ∧ Expression.stop.Distinguished Expression.annoyed

Some observed differences align with the classification: discover and stop are each less projective than the hard-triggering be annoyed.

theorem TonhauserBeaverDegen2018.soft_not_a_class : ∃ (a : Expression) (b : Expression), a.hardness? = some Presupposition.Hardness.soft ∧ b.hardness? = some Presupposition.Hardness.soft ∧ a.Distinguished b

The soft triggers are not a projectivity class: the prejacent of only is distinguished from the pre-state of stop.

theorem TonhauserBeaverDegen2018.hard_soft_indistinguishable (h : Predicate) : h ∈ [Predicate.annoyed, Predicate.amused] → ∀ s ∈ [Predicate.notice, Predicate.aware, Predicate.realize, Predicate.see, Predicate.findOut, Predicate.learn], ¬h.Distinguished s

Nor are the hard triggers a class apart in Experiment 1b: the hard-triggering emotive factives are indistinguishable from the soft-triggering semi-factives.

theorem TonhauserBeaverDegen2018.establish_least_projective (p : Predicate) (h : p ≠ Predicate.establish) : Predicate.establish.Distinguished p

The complement of establish is the least projective content, distinguished from every other Experiment 1b complement.