Issue extraction

[CGR18]

The issue-side observable on discourse states: HasIssue extracts the current issue (a Question W) the way CommonGround.HasContextSet extracts the context set. In inquisitive pragmatics the context is an issue and the context set is its informative content ([CGR18]); frameworks tracking both projections relate them per instance (e.g. how much of the context set an issue's informative content retains is a framework fact, not a law — see the Krifka monopolar/bipolar contrast in Discourse/Commitment/Space.lean).

Main definitions

• Discourse.HasIssue — extraction of the current issue from a discourse state.

class Discourse.HasIssue (S : Type u_1) (W : outParam (Type u_2)) : Type (max u_1 u_2)

A discourse state from which the current issue can be extracted.

• toIssue : S → Question W

@[reducible, inline]

abbrev Discourse.HasIssue.settles {S : Type u_1} {W : Type u_2} [HasIssue S W] (i : Set W) (s : S) : Prop

An information state settles a discourse state's issue iff it resolves the extracted Question.

Equations

• Discourse.HasIssue.settles i s = (i ∈ Discourse.HasIssue.toIssue s)

@[implicit_reducible]

instance Discourse.instHasIssueQuestion {W : Type u_1} : HasIssue (Question W) W

The canonical instance: an issue is its own extraction.

Equations

• Discourse.instHasIssueQuestion = { toIssue := id }