Givenness — Cognitive Status of Discourse Referents

@cite{gundel-hedberg-zacharski-1993} @cite{prince-1981} @cite{chafe-1976} @cite{chafe-1987} @cite{ariel-2001}

Substrate type for the Givenness axis of information structure. @cite{krifka-2008} enumerates four IS notions — focus, givenness, topic, and delimitation (frame-setting). At-issueness (Roberts / Tonhauser-Beaver-Roberts-Simons / Tonhauser-Beaver-Degen) is a separate axis from the QUD tradition that the post-2008 literature treats as orthogonal to Krifka's four. @cite{fery-ishihara-2016} (Oxford Handbook of Information Structure introduction) adopts Krifka's definitions as the unifying baseline. Linglib currently provides substrate for focus, givenness, topic, and at-issueness; delimitation has no substrate yet.

The handbook section on givenness names two interpretive modes:

• Scalar / hierarchical — Prince 1981, Chafe 1976, @cite{gundel-hedberg-zacharski-1993} (GHZ), @cite{lambrecht-1994}. The cognitive status of a referent in the hearer's mind is graded.
• Categorical — Schwarzschild 1999. Binary given vs not given, derived from grammatical antecedent presence.

This file provides the substrate for both:

• GivennessStatus (GHZ-6): inFocus | activated | familiar | uniquelyIdentifiable | referential | typeIdentifiable. The full hierarchy, promoted from Phenomena/Reference/Studies/Ariel2001.lean (where it was originally defined for the GHZ-vs-Ariel comparison) so it can be consumed across Theories/ and Features/.

• BinaryGivenness (Prince 1981 hearer-status): given | new. The simplest categorical distinction; coarsening of GHZ-6 cutting at hearer-knowledge: anything the hearer can identify (inFocus through uniquelyIdentifiable) is given; anything brand-new to the hearer (referential, typeIdentifiable) is new. This is the cut Prince 1981 / Strube-Hahn 1999 use. Chafe's later activation-based view (Chafe 1987, elaborated in Chafe 1994) draws a different cut as a three-way active / semi-active / inactive taxonomy; not provided here as a primitive.

Critique: Ariel 2001 on GHZ

@cite{ariel-2001} (pp. 62-65) raises four substantive critiques of the GHZ-6 hierarchy that consumers should know about:

1. Limited psychological evidence. Ariel argues (p. 64) that psychological evidence supports the scalar relation between inFocus and activated only — the four lower tiers (familiar through typeIdentifiable) lack independent experimental support as a distinct scalar order.
2. Internally disjunctive tiers. uniquelyIdentifiable and referential each cover two cognitively different processes (retrieve vs construct an existing/new representation; Ariel p. 63).
3. Many-many form-function. A given GHZ status maps to many surface forms, and a given form maps to many statuses (Mulkern 1996 on partial vs full proper names; Ariel p. 64).
4. Implicationality counterexample. Ziv 1996 — pronouns (inFocus) are predicted by the implicational hierarchy to also be uniquelyIdentifiable, but Ziv exhibits cases of unidentified inferred role players where this fails.

Ariel's own account uses the 18-tier Features.AccessibilityLevel (see below) which Ariel argues is the better-grounded scale. GHZ-6 is nonetheless retained as substrate because it is what the IS literature widely cites (Krifka 2008 / Féry-Ishihara 2016 list it as the canonical scalar givenness theory), and because Centering's @cite{strube-hahn-1999} information-status taxonomy projects naturally from GHZ-style categories. Discrete enough for decide-based theorems, where AccessibilityLevel's 18 tiers can be unwieldy.

Relation to AccessibilityLevel

Features.AccessibilityLevel (@cite{ariel-2001}) is the empirically-better-supported sibling: 18 tiers of NP-form-marking with informativity, rigidity, and attenuation criteria. Ariel's toAccessibility projection from GHZ-6 to AccessibilityLevel lives in Phenomena/Reference/Studies/Ariel2001.lean (Ariel-specific bridge). Use AccessibilityLevel when finer distinctions matter (proximate vs distal demonstratives; clitic vs unstressed vs zero pronouns); use GivennessStatus when the IS-literature 6-tier shape is the right granularity.

Layer position

Features/. Importable from any Theories/, Phenomena/, or Fragments/ consumer that needs to type a discourse referent's cognitive status. The Centering MEDIATED tier (Theories/Discourse/Centering/Instances/InformationStatus.lean) used to lack a substrate source for the inferable / containing-inferable / anchored-brand-new tier; GHZ-6's familiar and uniquelyIdentifiable now supply it via StrubeHahnInfoStatus.ofGivenness.

inductive Features.GivennessStatus : Type

@cite{gundel-hedberg-zacharski-1993} (GHZ): six cognitive statuses organized as an implicational hierarchy. Each status implies all lower ones (a referent in focus is also activated, familiar, etc.):

in focus > activated > familiar > uniquely identifiable >
referential > type identifiable

The form-mapping documented in the original paper: inFocus = unstressed pronoun activated = that, this, this N familiar = that N uniquelyIdentifiable = the N referential = indefinite this N typeIdentifiable = a N

Promoted from Phenomena/Reference/Studies/Ariel2001.lean where it was originally defined for the GHZ-vs-Ariel-accessibility comparison. The Ariel-specific projection (GivennessStatus.toAccessibility) stays in Ariel2001.lean.

• inFocus : GivennessStatus

  Unstressed pronoun: referent currently in attention. Per @cite{ariel-2001} p. 64 (citing Ziv 1996), the implicational claim that inFocus entities are also uniquelyIdentifiable has counterexamples (unidentified inferred role players); this enum's ordinal placement is the GHZ-claimed order, not a proven cognitive fact.

• 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 ⋯

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

Equations

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

@[implicit_reducible]

instance Features.instReprGivennessStatus : Repr GivennessStatus

Equations

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

@[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.instInhabitedGivennessStatus.default : GivennessStatus

Equations

• Features.instInhabitedGivennessStatus.default = Features.GivennessStatus.inFocus

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

@cite{prince-1981} hearer-status binary: given | new. The simplest categorical givenness distinction. given covers any referent the hearer can identify (regardless of activation state); new covers referents the hearer doesn't yet know about.

This is the cut Prince 1981 / Strube-Hahn 1999 use. Chafe's activation-based view (Chafe 1987) draws a different three-way taxonomy (active / semi-active / inactive); not provided here as a primitive.

• given : BinaryGivenness

  Given: hearer can identify the referent. Covers GHZ's inFocus through uniquelyIdentifiable.

• new : BinaryGivenness

  New: brand-new to the hearer. Covers GHZ's referential and 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.instInhabitedBinaryGivenness.default : BinaryGivenness

Equations

• Features.instInhabitedBinaryGivenness.default = Features.BinaryGivenness.given

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

theorem Features.GivennessStatus.rank_injective : Function.Injective rank

Distinct GHZ-6 statuses have distinct ranks.

theorem Features.BinaryGivenness.rank_injective : Function.Injective rank

Distinct binary-givenness values have distinct ranks.

@[implicit_reducible]

instance Features.instLinearOrderGivennessStatus : LinearOrder GivennessStatus

Total order on GivennessStatus via the rank function.

Equations

• Features.instLinearOrderGivennessStatus = LinearOrder.lift' Features.GivennessStatus.rank Features.GivennessStatus.rank_injective

@[implicit_reducible]

instance Features.instLinearOrderBinaryGivenness : LinearOrder BinaryGivenness

Total order on BinaryGivenness via the rank function.

Equations

• Features.instLinearOrderBinaryGivenness = LinearOrder.lift' Features.BinaryGivenness.rank Features.BinaryGivenness.rank_injective