Linglib.Phenomena.Presupposition.ProjectiveContent

"John believes Mary stopped smoking" → John believes Mary used to smoke (obligatory local reading)
"John believes it's raining" (from "John knows...") → The embedded proposition is part of John's beliefs

Examples without OLE:

"John believes Lance, an Ohioan, will win" → Speaker (not John) commits to Lance being Ohioan
"John believes that damn cat is outside" → Speaker (not John) is annoyed at the cat

obligatory : ObligatoryLocalEffect
notObligatory : ObligatoryLocalEffect

Instances For

source

instance Phenomena.Presupposition.ProjectiveContent.instDecidableEqObligatoryLocalEffect :

DecidableEq ObligatoryLocalEffect

Equations

Phenomena.Presupposition.ProjectiveContent.instDecidableEqObligatoryLocalEffect x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

def Phenomena.Presupposition.ProjectiveContent.instReprObligatoryLocalEffect.repr :

ObligatoryLocalEffect → ℕ → Std.Format

Equations

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

Instances For

source

instance Phenomena.Presupposition.ProjectiveContent.instReprObligatoryLocalEffect :

Repr ObligatoryLocalEffect

Equations

Phenomena.Presupposition.ProjectiveContent.instReprObligatoryLocalEffect = { reprPrec := Phenomena.Presupposition.ProjectiveContent.instReprObligatoryLocalEffect.repr }

source

inductive Phenomena.Presupposition.ProjectiveContent.ProjectiveClass :

Type

The four classes of projective content from @cite{tonhauser-beaver-roberts-simons-2013}.

Each class is defined by a combination of SCF and OLE values.

classA : ProjectiveClass
Class A: SCF=yes, OLE=yes Examples: pronouns (existence), too (existence)
classB : ProjectiveClass
Class B: SCF=no, OLE=no Examples: expressives, appositives, NRRCs, possessive NPs
classC : ProjectiveClass
Class C: SCF=no, OLE=yes Examples: stop, know, only, almost
classD : ProjectiveClass
Class D: SCF=yes, OLE=no Examples: too (salience), demonstratives, focus (salience)

Instances For

source

instance Phenomena.Presupposition.ProjectiveContent.instDecidableEqProjectiveClass :

DecidableEq ProjectiveClass

Equations

Phenomena.Presupposition.ProjectiveContent.instDecidableEqProjectiveClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

def Phenomena.Presupposition.ProjectiveContent.instReprProjectiveClass.repr :

ProjectiveClass → ℕ → Std.Format

Equations

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

Instances For

source

instance Phenomena.Presupposition.ProjectiveContent.instReprProjectiveClass :

Repr ProjectiveClass

Equations

Phenomena.Presupposition.ProjectiveContent.instReprProjectiveClass = { reprPrec := Phenomena.Presupposition.ProjectiveContent.instReprProjectiveClass.repr }

source

def Phenomena.Presupposition.ProjectiveContent.classFromProperties :

StrongContextualFelicity → ObligatoryLocalEffect → ProjectiveClass

Reconstruct the class from SCF and OLE values.

Equations

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

Instances For

source

theorem Phenomena.Presupposition.ProjectiveContent.class_properties_roundtrip (c : ProjectiveClass) :

classFromProperties c.scf c.ole = c

The class reconstruction is correct.

source

inductive Phenomena.Presupposition.ProjectiveContent.ProjectiveTrigger :

Type

Types of projective content triggers, following @cite{tonhauser-beaver-roberts-simons-2013}.

Each trigger type is associated with a projective class and a description of the content it triggers.

pronoun_existence : ProjectiveTrigger
Personal pronouns: existence of referent
too_existence : ProjectiveTrigger
"too": existence of alternative satisfying predicate
expressive : ProjectiveTrigger
Expressives like "damn": speaker attitude
appositive : ProjectiveTrigger
Appositives: supplementary content
nrrc : ProjectiveTrigger
Non-restrictive relative clauses
possessive_np : ProjectiveTrigger
Possessive NPs: existence of possessor
stop_prestate : ProjectiveTrigger
Change-of-state predicates: prior state
know_complement : ProjectiveTrigger
Factive verbs: complement truth
only_prejacent : ProjectiveTrigger
Focus-sensitive "only": prejacent
almost_polar : ProjectiveTrigger
"almost": polar content
definite_description : ProjectiveTrigger
Definite descriptions: existence and uniqueness
occasion_verb : ProjectiveTrigger
Occasion verbs: prior occasioning eventuality (@cite{solstad-bott-2024}, S&P 17:11). "Punish" presupposes a prior offense; "manage" presupposes a prior difficulty. SCF=no (can be informative), OLE=yes (attributed to attitude holder).
too_salience : ProjectiveTrigger
"too": salience of alternative
demonstrative_indication : ProjectiveTrigger
Demonstratives: indication established
focus_salience : ProjectiveTrigger
Focus: salience of alternatives

Instances For

source

instance Phenomena.Presupposition.ProjectiveContent.instDecidableEqProjectiveTrigger :

DecidableEq ProjectiveTrigger

Equations

Phenomena.Presupposition.ProjectiveContent.instDecidableEqProjectiveTrigger x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

def Phenomena.Presupposition.ProjectiveContent.instReprProjectiveTrigger.repr :

ProjectiveTrigger → ℕ → Std.Format

Equations

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

Instances For

source

instance Phenomena.Presupposition.ProjectiveContent.instReprProjectiveTrigger :

Repr ProjectiveTrigger

Equations

Phenomena.Presupposition.ProjectiveContent.instReprProjectiveTrigger = { reprPrec := Phenomena.Presupposition.ProjectiveContent.instReprProjectiveTrigger.repr }

source

def Phenomena.Presupposition.ProjectiveContent.ProjectiveTrigger.toClass :

ProjectiveTrigger → ProjectiveClass

The projective class for each trigger type.

Equations

Instances For

source

structure Phenomena.Presupposition.ProjectiveContent.ProjectiveItem (W : Type u_1) :

Type u_1

A projective content item, combining a trigger with its content.

This extends the basic PrProp to track what kind of projective content is involved.

trigger : ProjectiveTrigger
The trigger type
content : W → Bool
The projective content as a proposition
atIssue : W → Bool
The at-issue content (if any)
projectivityDegree : Option ℚ
Gradient projectivity degree (TBD2018), if empirically measured
atIssuenessDegree : Option ℚ
Gradient at-issueness degree (TBD2018), if empirically measured

Instances For

source

def Phenomena.Presupposition.ProjectiveContent.ProjectiveItem.toPrProp {W : Type u_1} (pc : ProjectiveItem W) :

Core.Presupposition.PrProp W

Convert a ProjectiveItem to a PrProp.

The projective content becomes the presupposition, and the at-issue content becomes the assertion.

Equations

pc.toPrProp = { presup := pc.content, assertion := pc.atIssue }

Instances For

source

def Phenomena.Presupposition.ProjectiveContent.ProjectiveItem.projectiveClass {W : Type u_1} (pc : ProjectiveItem W) :

ProjectiveClass

Get the projective class for this item.

Equations

pc.projectiveClass = pc.trigger.toClass

Instances For

source

structure Phenomena.Presupposition.ProjectiveContent.ProjectionBehavior :

Type

Projection behavior describes how content behaves under embedding.

All projective contents share the core property that they can project past certain operators, but they differ in their default behavior.

projectsPastNegation : Bool
Projects past negation by default
projectsPastQuestions : Bool
Projects past questions by default
projectsPastModals : Bool
Projects past modals by default
projectsPastConditionals : Bool
Projects past conditionals (from antecedent)

Instances For

source

instance Phenomena.Presupposition.ProjectiveContent.instReprProjectionBehavior :

Repr ProjectionBehavior

Equations

Phenomena.Presupposition.ProjectiveContent.instReprProjectionBehavior = { reprPrec := Phenomena.Presupposition.ProjectiveContent.instReprProjectionBehavior.repr }

source

def Phenomena.Presupposition.ProjectiveContent.instReprProjectionBehavior.repr :

ProjectionBehavior → ℕ → Std.Format

Equations

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

Instances For

source

def Phenomena.Presupposition.ProjectiveContent.defaultProjection :

ProjectionBehavior

Default projection behavior: all projective contents project by default.

Tonhauser et al. argue that projection is the default for all projective contents. The differences are in SCF and OLE, not in whether they project.

Equations

Phenomena.Presupposition.ProjectiveContent.defaultProjection = { projectsPastNegation := true, projectsPastQuestions := true, projectsPastModals := true, projectsPastConditionals := true }

Instances For

source

inductive Phenomena.Presupposition.ProjectiveContent.AtIssueness :

Type

At-issueness status of content (binary classification).

Following @cite{roberts-2012}, at-issue content addresses the Question Under Discussion (QUD), while not-at-issue content is backgrounded.

Note: @cite{tonhauser-beaver-degen-2018} show that at-issueness is gradient, not binary. For the gradient version, see Core.Discourse.AtIssueness.AtIssuenessDegree. This binary enum is recoverable from a degree + threshold via AtIssueness.ofDegree.

atIssue : AtIssueness
Content that addresses the QUD
notAtIssue : AtIssueness
Backgrounded content

Instances For

source

instance Phenomena.Presupposition.ProjectiveContent.instDecidableEqAtIssueness :

DecidableEq AtIssueness

Equations

Phenomena.Presupposition.ProjectiveContent.instDecidableEqAtIssueness x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

instance Phenomena.Presupposition.ProjectiveContent.instReprAtIssueness :

Repr AtIssueness

Equations

Phenomena.Presupposition.ProjectiveContent.instReprAtIssueness = { reprPrec := Phenomena.Presupposition.ProjectiveContent.instReprAtIssueness.repr }

source

def Phenomena.Presupposition.ProjectiveContent.instReprAtIssueness.repr :

AtIssueness → ℕ → Std.Format

Equations

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

Instances For

source

def Phenomena.Presupposition.ProjectiveContent.AtIssueness.ofDegree (d : Core.Discourse.AtIssueness.AtIssuenessDegree) (θ : Core.Discourse.AtIssueness.AtIssuenessThreshold := Core.Discourse.AtIssueness.defaultThreshold) :

AtIssueness

Recover binary at-issueness from a gradient degree and threshold. With the default threshold of 0.5, content with degree > 0.5 maps to .atIssue, ≤ 0.5 to .notAtIssue.

Equations

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

Instances For

source

inductive Phenomena.Presupposition.ProjectiveContent.Challengeability :

Type

Challengeability with "Hey wait a minute!"

The HWAM test distinguishes at-issue from not-at-issue content:

At-issue content can be challenged with "No, that's not true"
Not-at-issue content can be challenged with "Hey wait a minute!"

directDenial : Challengeability
Can be challenged with "No, that's not true"
hwamChallenge : Challengeability
Can be challenged with "Hey wait a minute!"
notChallengeable : Challengeability
Cannot be directly challenged

Instances For

source

instance Phenomena.Presupposition.ProjectiveContent.instDecidableEqChallengeability :

DecidableEq Challengeability

Equations

Phenomena.Presupposition.ProjectiveContent.instDecidableEqChallengeability x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

def Phenomena.Presupposition.ProjectiveContent.instReprChallengeability.repr :

Challengeability → ℕ → Std.Format

Equations

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

Instances For

source

instance Phenomena.Presupposition.ProjectiveContent.instReprChallengeability :

Repr Challengeability

Equations

Phenomena.Presupposition.ProjectiveContent.instReprChallengeability = { reprPrec := Phenomena.Presupposition.ProjectiveContent.instReprChallengeability.repr }

source

def Phenomena.Presupposition.ProjectiveContent.projectiveContentTypicalStatus :

AtIssueness × Challengeability

Projective content is typically not-at-issue and HWAM-challengeable.

This diagnostic identifies projective content.

Equations

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

Instances For

source

inductive Phenomena.Presupposition.ProjectiveContent.BeliefAttribution :

Type

Attribution of projective content under belief predicates.

When "x believes that S" is uttered, who is committed to the projective content of S?

attitudeHolder : BeliefAttribution
Attributed to attitude holder (x)
speaker : BeliefAttribution
Attributed to speaker
ambiguous : BeliefAttribution
Potentially ambiguous

Instances For

source

instance Phenomena.Presupposition.ProjectiveContent.instDecidableEqBeliefAttribution :

DecidableEq BeliefAttribution

Equations

Phenomena.Presupposition.ProjectiveContent.instDecidableEqBeliefAttribution x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

instance Phenomena.Presupposition.ProjectiveContent.instReprBeliefAttribution :

Repr BeliefAttribution

Equations

Phenomena.Presupposition.ProjectiveContent.instReprBeliefAttribution = { reprPrec := Phenomena.Presupposition.ProjectiveContent.instReprBeliefAttribution.repr }

source

def Phenomena.Presupposition.ProjectiveContent.instReprBeliefAttribution.repr :

BeliefAttribution → ℕ → Std.Format

Equations

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

Instances For

source

def Phenomena.Presupposition.ProjectiveContent.ProjectiveClass.beliefAttribution :

ProjectiveClass → BeliefAttribution

Get the belief attribution for a projective class.

Equations

Instances For

source

inductive Phenomena.Presupposition.ProjectiveContent.TraditionalCategory :

Type

Traditional classification of projective phenomena.

This maps the traditional terminology onto the Tonhauser et al. taxonomy. Note that this is a simplification — the paper argues that traditional categories don't carve at the joints.

presupposition : TraditionalCategory
Traditional "presupposition"
conventionalImplicature : TraditionalCategory
Potts-style "conventional implicature"
supplementary : TraditionalCategory
Supplementary/parenthetical content

Instances For

source

instance Phenomena.Presupposition.ProjectiveContent.instDecidableEqTraditionalCategory :

DecidableEq TraditionalCategory

Equations