Givenness — cognitive status of discourse referents

Substrate for the givenness axis of information structure (one of [Kri08]'s four IS notions). Two types, for the scalar and the categorical view of givenness.

• GivennessStatus — the [GHZ93] (GHZ) six-tier Givenness Hierarchy inFocus > activated > familiar > uniquelyIdentifiable > referential > typeIdentifiable, with a rank giving GHZ's implicational status order (each status entails all lower; not a claim about the many-to-many status-to-form mapping). Promoted from Studies/Ariel2001.lean so it can be shared.
• BinaryGivenness — given | new, the GHZ coarsening (GivennessStatus.toBinary) at the identifiable/indefinite boundary ([Lam94] identifiability). Not [Pri92]'s hearer-old/new binary (which cross-cuts identifiability), nor [Sch99] entailment-givenness (isGiven in Studies/KratzerSelkirk2020.lean); a consumer meaning another axis (e.g. discourse-status) should say so.

Sibling GHZ-6 coarsenings/scales: Ariel's 18-tier Features.AccessibilityLevel (toAccessibility) and Centering's [SH99] StrubeHahnInfoStatus.ofGivenness (its mediated tier drawn from uniquelyIdentifiable/referential). [Ari01] argues AccessibilityLevel is better grounded — the lower GHZ tiers lack independent scalar support — but GHZ-6 is retained as the literature's canonical scalar scale and is small enough for decide. See also [Pri81], [Cha76], [Cha87].

inductive Features.GivennessStatus : Type

[GHZ93] six-tier Givenness Hierarchy (inFocus > … > typeIdentifiable), each status entailing all lower.

• inFocus : GivennessStatus

  In focus: unstressed pronoun — referent currently in attention.

• activated : GivennessStatus

  Activated: that/this/this-N — referent in working memory.

• familiar : GivennessStatus

  Familiar: that-N — referent in long-term memory.

• uniquelyIdentifiable : GivennessStatus

  Uniquely identifiable: the-N — hearer can construct the referent from the description alone.

• referential : GivennessStatus

  Referential: indefinite this-N — speaker has a particular referent in mind, hearer doesn't yet.

• typeIdentifiable : GivennessStatus

  Type identifiable: a-N — hearer can construct a representation of the type of object described.

@[implicit_reducible]

instance Features.instDecidableEqGivennessStatus : DecidableEq GivennessStatus

Equations

• Features.instDecidableEqGivennessStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Features.instReprGivennessStatus : Repr GivennessStatus

Equations

• Features.instReprGivennessStatus = { reprPrec := Features.instReprGivennessStatus.repr }

def Features.instReprGivennessStatus.repr : GivennessStatus → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.instFintypeGivennessStatus : Fintype GivennessStatus

Equations

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

@[implicit_reducible]

instance Features.instInhabitedGivennessStatus : Inhabited GivennessStatus

Equations

• Features.instInhabitedGivennessStatus = { default := Features.instInhabitedGivennessStatus.default }

def Features.GivennessStatus.rank : GivennessStatus → ℕ

Numeric rank: inFocus = 5 (highest), typeIdentifiable = 0 (lowest). Higher rank = more cognitively accessible.

Equations

• Features.GivennessStatus.inFocus.rank = 5
• Features.GivennessStatus.activated.rank = 4
• Features.GivennessStatus.familiar.rank = 3
• Features.GivennessStatus.uniquelyIdentifiable.rank = 2
• Features.GivennessStatus.referential.rank = 1
• Features.GivennessStatus.typeIdentifiable.rank = 0

inductive Features.BinaryGivenness : Type

given | new: the GHZ identifiability coarsening (GivennessStatus.toBinary); see the module docstring for what it is not.

• given : BinaryGivenness

  Given: hearer can identify the referent (GHZ inFocus..uniquelyIdentifiable).

• new : BinaryGivenness

  New: indefinite, not yet identifiable (GHZ referential, typeIdentifiable).

@[implicit_reducible]

instance Features.instDecidableEqBinaryGivenness : DecidableEq BinaryGivenness

Equations

• Features.instDecidableEqBinaryGivenness x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Features.instReprBinaryGivenness : Repr BinaryGivenness

Equations

• Features.instReprBinaryGivenness = { reprPrec := Features.instReprBinaryGivenness.repr }

def Features.instReprBinaryGivenness.repr : BinaryGivenness → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.instFintypeBinaryGivenness : Fintype BinaryGivenness

Equations

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

@[implicit_reducible]

instance Features.instInhabitedBinaryGivenness : Inhabited BinaryGivenness

Equations

• Features.instInhabitedBinaryGivenness = { default := Features.instInhabitedBinaryGivenness.default }

def Features.BinaryGivenness.rank : BinaryGivenness → ℕ

Numeric rank: given = 1, new = 0. Higher rank = more given.

Equations

• Features.BinaryGivenness.given.rank = 1
• Features.BinaryGivenness.new.rank = 0

def Features.GivennessStatus.toBinary : GivennessStatus → BinaryGivenness

GHZ-6 given–new coarsening: identifiable tiers ↦ given, indefinite tiers ↦ new. Makes the module docstring's cut true by construction.

Equations

• Features.GivennessStatus.inFocus.toBinary = Features.BinaryGivenness.given
• Features.GivennessStatus.activated.toBinary = Features.BinaryGivenness.given
• Features.GivennessStatus.familiar.toBinary = Features.BinaryGivenness.given
• Features.GivennessStatus.uniquelyIdentifiable.toBinary = Features.BinaryGivenness.given
• Features.GivennessStatus.referential.toBinary = Features.BinaryGivenness.new
• Features.GivennessStatus.typeIdentifiable.toBinary = Features.BinaryGivenness.new

theorem Features.GivennessStatus.toBinary_monotone (a b : GivennessStatus) : a.rank ≤ b.rank → a.toBinary.rank ≤ b.toBinary.rank

The coarsening is rank-monotone: more accessible GHZ tiers map to given.