Topic — Aboutness and Contrastive Topics

@cite{reinhart-1981} @cite{buring-2003} @cite{krifka-2008}

Substrate type for the Topic axis of information structure, one of the four IS notions Krifka 2008 enumerates (focus, givenness, topic, delimitation; see Features/Givenness.lean for the broader discussion of how at-issueness sits orthogonally to Krifka's four). @cite{fery-ishihara-2016} (Oxford Handbook of Information Structure) follows Krifka in treating topic as a primitive notion, defined per @cite{krifka-2008}:

The topic constituent identifies the entity or set of entities under which the information expressed in the comment constituent should be stored in the CG content.

Following @cite{reinhart-1981}'s file-card metaphor: the CG is organized like a subject-oriented library catalogue indexed by topics; each new proposition is filed under the topic it is about.

What's here

• TopicMark — binary aboutness marking. Whether a constituent is the (Reinhart) aboutness topic or not. Substrate hook for studies that need to annotate constituents as topical.
• ContrastiveTopic α — placeholder structure for Büring-style contrastive topic, mirroring Features.InformationStructure.Focus shape (a marked element with a list of alternatives). Not enough yet to formalize Büring 2003's full [T,F]-marking calculus, but enough to type lexical entries that bear contrastive-topic marking.

What's not here

This file deliberately does NOT formalize:

• Büring 2003's full [T,F]-marking + question hierarchy / D-tree semantics. That belongs in a future Theories/Semantics/Focus/Buring2003.lean study or similar.
• Krifka 2008's frame-setting topics (§5.1.4) and delimitation topics — distinct concepts to add when consumers demand them.
• @cite{fery-ishihara-2016} Ch 4 (Büring) argues for eliminating non-contrastive topics as a coherent linguistic category; this remains a live debate. The substrate keeps both TopicMark (aboutness) and ContrastiveTopic available rather than picking a side.

Layer position

Features/. Sibling of Features/Givenness.lean, Features/Accessibility.lean, and Features/InformationStructure.lean. Importable from any consumer that needs to type a constituent as topical or contrastive-topic. Currently Phenomena/Generics/BarePlurals.lean has a local TopicFocusDatum that could migrate here in a follow-up.

inductive Features.TopicMark : Type

@cite{reinhart-1981} aboutness topic: whether a constituent is the entity under which the proposition is filed in the CG. Binary by design — degree-of-topicality theories belong in their own files.

• aboutness : TopicMark

  Aboutness topic: the constituent the proposition is about.

• nonTopic : TopicMark

  Non-topical constituent.

@[implicit_reducible]

instance Features.instDecidableEqTopicMark : DecidableEq TopicMark

Equations

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

@[implicit_reducible]

instance Features.instReprTopicMark : Repr TopicMark

Equations

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

def Features.instReprTopicMark.repr : TopicMark → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.instFintypeTopicMark : Fintype TopicMark

Equations

• Features.instFintypeTopicMark = { elems := { val := ↑Features.TopicMark.enumList, nodup := Features.TopicMark.enumList_nodup }, complete := Features.instFintypeTopicMark._proof_1 }

def Features.instInhabitedTopicMark.default : TopicMark

Equations

• Features.instInhabitedTopicMark.default = Features.TopicMark.aboutness

@[implicit_reducible]

instance Features.instInhabitedTopicMark : Inhabited TopicMark

Equations

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

structure Features.ContrastiveTopic (α : Type) : Type

@cite{buring-2003} contrastive topic: a topic constituent paired with a set of alternative topics that could have been chosen. Mirrors Features.InformationStructure.Focus shape — both Roothian-flavored alternative-set primitives.

The placeholder structure carries the topic and its alternatives; Büring's full [T,F]-marking calculus (where the alternatives index a discourse-tree of subquestions) belongs in a later study file.

• topic : α

  The topical element.

• alternatives : List α

  Alternative topics that could have been picked instead.

@[implicit_reducible]

instance Features.instReprContrastiveTopic {α✝ : Type} [Repr α✝] : Repr (ContrastiveTopic α✝)

Equations

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

def Features.instReprContrastiveTopic.repr {α✝ : Type} [Repr α✝] : ContrastiveTopic α✝ → ℕ → Std.Format

Equations

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