The taxonomy of projective content

[TBRS13]'s classification of projective contents by two diagnostics: Strong Contextual Felicity (does the trigger require its projective content to be established in the utterance context?) and Obligatory Local Effect (when embedded under a belief predicate, must the content be part of the attitude holder's beliefs?). The two binary diagnostics yield four classes A–D.

Consumed as classification vocabulary by the projective-content study files ([TBRS13], [SB24], [RS24b], and the Nez Perce study of attitude embedding).

Main declarations

• StrongContextualFelicity, ObligatoryLocalEffect — the two diagnostics.
• ProjectiveClass — classes A–D, with scf/ole projections and the classFromProperties reconstruction (class_properties_roundtrip).
• ProjectiveTrigger — the framework's per-trigger table, with toClass. The occasion_verb case follows [SB24].

inductive Semantics.Presupposition.ProjectiveContent.StrongContextualFelicity : Type

Strong Contextual Felicity (SCF): whether a trigger requires its projective content to be established in the utterance context prior to use. Pronouns, demonstratives, and salience-too require it; expressives, appositives, and factives can be informative.

• requires : StrongContextualFelicity

  SCF = yes: requires prior establishment.

• noRequires : StrongContextualFelicity

  SCF = no: the content can be informative.

@[implicit_reducible]

instance Semantics.Presupposition.ProjectiveContent.instDecidableEqStrongContextualFelicity : DecidableEq StrongContextualFelicity

Equations

• Semantics.Presupposition.ProjectiveContent.instDecidableEqStrongContextualFelicity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Presupposition.ProjectiveContent.instReprStrongContextualFelicity.repr : StrongContextualFelicity → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Presupposition.ProjectiveContent.instReprStrongContextualFelicity : Repr StrongContextualFelicity

Equations

• Semantics.Presupposition.ProjectiveContent.instReprStrongContextualFelicity = { reprPrec := Semantics.Presupposition.ProjectiveContent.instReprStrongContextualFelicity.repr }

inductive Semantics.Presupposition.ProjectiveContent.ObligatoryLocalEffect : Type

Obligatory Local Effect (OLE): whether, under a belief predicate, the projective content must be part of the attitude holder's beliefs. Stop and know contents are attributed to the attitude holder; appositive and expressive contents remain speaker commitments.

• obligatory : ObligatoryLocalEffect

  OLE = yes: attributed to the attitude holder.

• notObligatory : ObligatoryLocalEffect

  OLE = no: attributed to the speaker.

@[implicit_reducible]

instance Semantics.Presupposition.ProjectiveContent.instDecidableEqObligatoryLocalEffect : DecidableEq ObligatoryLocalEffect

Equations

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

def Semantics.Presupposition.ProjectiveContent.instReprObligatoryLocalEffect.repr : ObligatoryLocalEffect → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Presupposition.ProjectiveContent.instReprObligatoryLocalEffect : Repr ObligatoryLocalEffect

Equations

• Semantics.Presupposition.ProjectiveContent.instReprObligatoryLocalEffect = { reprPrec := Semantics.Presupposition.ProjectiveContent.instReprObligatoryLocalEffect.repr }

inductive Semantics.Presupposition.ProjectiveContent.ProjectiveClass : Type

The four classes of projective content, each a combination of SCF and OLE values.

• classA : ProjectiveClass

  Class A (SCF=yes, OLE=yes): pronouns (existence), too (existence).

• classB : ProjectiveClass

  Class B (SCF=no, OLE=no): expressives, appositives, NRRCs, possessive NPs.

• classC : ProjectiveClass

  Class C (SCF=no, OLE=yes): stop, know, only, almost.

• classD : ProjectiveClass

  Class D (SCF=yes, OLE=no): too (salience), demonstratives, focus (salience).

@[implicit_reducible]

instance Semantics.Presupposition.ProjectiveContent.instDecidableEqProjectiveClass : DecidableEq ProjectiveClass

Equations

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

def Semantics.Presupposition.ProjectiveContent.instReprProjectiveClass.repr : ProjectiveClass → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Presupposition.ProjectiveContent.instReprProjectiveClass : Repr ProjectiveClass

Equations

• Semantics.Presupposition.ProjectiveContent.instReprProjectiveClass = { reprPrec := Semantics.Presupposition.ProjectiveContent.instReprProjectiveClass.repr }

def Semantics.Presupposition.ProjectiveContent.ProjectiveClass.scf : ProjectiveClass → StrongContextualFelicity

The SCF value of a projective class.

Equations

• Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classA.scf = Semantics.Presupposition.ProjectiveContent.StrongContextualFelicity.requires
• Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classB.scf = Semantics.Presupposition.ProjectiveContent.StrongContextualFelicity.noRequires
• Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classC.scf = Semantics.Presupposition.ProjectiveContent.StrongContextualFelicity.noRequires
• Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classD.scf = Semantics.Presupposition.ProjectiveContent.StrongContextualFelicity.requires

def Semantics.Presupposition.ProjectiveContent.ProjectiveClass.ole : ProjectiveClass → ObligatoryLocalEffect

The OLE value of a projective class.

Equations

• Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classA.ole = Semantics.Presupposition.ProjectiveContent.ObligatoryLocalEffect.obligatory
• Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classB.ole = Semantics.Presupposition.ProjectiveContent.ObligatoryLocalEffect.notObligatory
• Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classC.ole = Semantics.Presupposition.ProjectiveContent.ObligatoryLocalEffect.obligatory
• Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classD.ole = Semantics.Presupposition.ProjectiveContent.ObligatoryLocalEffect.notObligatory

def Semantics.Presupposition.ProjectiveContent.classFromProperties : StrongContextualFelicity → ObligatoryLocalEffect → ProjectiveClass

Reconstruct the class from its SCF and OLE values.

Equations

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

theorem Semantics.Presupposition.ProjectiveContent.class_properties_roundtrip (c : ProjectiveClass) : classFromProperties c.scf c.ole = c

The two diagnostics jointly determine the class.

inductive Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger : Type

Projective-content triggers, following [TBRS13]'s per-trigger table.

• pronoun_existence : ProjectiveTrigger

  Personal pronouns: existence of referent.

• too_existence : ProjectiveTrigger

  too: existence of an alternative satisfying the 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 ([SB24]). 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.

@[implicit_reducible]

instance Semantics.Presupposition.ProjectiveContent.instDecidableEqProjectiveTrigger : DecidableEq ProjectiveTrigger

Equations

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

@[implicit_reducible]

instance Semantics.Presupposition.ProjectiveContent.instReprProjectiveTrigger : Repr ProjectiveTrigger

Equations

• Semantics.Presupposition.ProjectiveContent.instReprProjectiveTrigger = { reprPrec := Semantics.Presupposition.ProjectiveContent.instReprProjectiveTrigger.repr }

def Semantics.Presupposition.ProjectiveContent.instReprProjectiveTrigger.repr : ProjectiveTrigger → Nat → Std.Format

Equations

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

def Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger.toClass : ProjectiveTrigger → ProjectiveClass

The projective class of each trigger.

Equations

• Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger.pronoun_existence.toClass = Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classA
• Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger.too_existence.toClass = Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classA
• Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger.expressive.toClass = Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classB
• Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger.appositive.toClass = Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classB
• Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger.nrrc.toClass = Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classB
• Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger.possessive_np.toClass = Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classB
• Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger.stop_prestate.toClass = Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classC
• Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger.know_complement.toClass = Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classC
• Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger.only_prejacent.toClass = Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classC
• Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger.almost_polar.toClass = Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classC
• Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger.definite_description.toClass = Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classC
• Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger.occasion_verb.toClass = Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classC
• Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger.too_salience.toClass = Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classD
• Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger.demonstrative_indication.toClass = Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classD
• Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger.focus_salience.toClass = Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classD