Krifka (2015): Bias in Commitment Space Semantics

Krifka models a conversation as a commitment space, the current commitment state with the continuations it projects, all of them coherent. An assertion keeps the states that carry the speaker's commitment. A question keeps the root and proposes continuations: a monopolar question the addressee's assertion of φ, a bipolar question that assertion or the one of ¬φ, a question with high negation the addressee's refusal to commit to φ; a question with low negation is a monopolar question about ¬φ. An answer is performed in the space the question left, so it lands on a state that also carries what the question proposed, and an answer that no such state carries needs a prior rejection, which returns to the space before the question. This is the bias of a question. A matching question tag conjoins an assertion with the monopolar question of the same content, and a reverse tag disjoins it with the monopolar question of the negation.

Main statements

• not_admits_monopolarQuestion_no, admits_bipolarQuestion_no: no needs a prior rejection after a monopolar question and none after a bipolar one.
• root_highNegationQuestion_update_no, not_admits_highNegationQuestion_yes: after a question with high negation no is admitted and keeps the refusal, while yes needs a rejection.
• root_reject_matchingTag_no, commit_speaker_mem_root_assert_assert: rejecting an assertion with a matching tag removes the speaker's commitment, which a plain assertion keeps when the addressee contradicts it.
• root_reverseTag_update_yes: after a reverse tag, the addressee's commitment to φ brings the speaker's with it.

Implementation notes

• Coherence is the paper's ban on blatant inconsistency: nobody is committed to a proposition while committed to its negation or refusing to commit to it. The initial space has every coherent state.
• Developments record the spaces passed through and not who acted, since no statement here depends on the actor of a stage.
• The licensing conditions behind the table of acceptable uses are stated on the evidence and are not derived from the spaces. Contextual evidence is the set of worlds it leaves open: the proposition, everything, or its complement.

TODO

• The second update of an assertion, by the proposition itself, is not modelled, so contradicting a plain assertion needs no rejection here; in the paper the rejection undoes only that update, and the speaker's commitment stays, as here.
• The reaction I don't know is left out: its clash with either answer is a fact about knowledge that coherence does not see.
• The paper prints the addressee's commitment to φ in the last stage of (28b); since no asserts the negation, it is the commitment to ¬φ here.

References

• M. Krifka, Bias in Commitment Space Semantics: Declarative Questions, Negated Questions, and Question Tags (2015)
• D. F. Farkas and K. B. Bruce, On Reacting to Assertions and Polar Questions (2010)
• D. Büring and C. Gunlogson, Aren't Positive and Negative Polar Questions the Same? (2000)

Questions as meta-speech acts

def Krifka2015.question {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) (P : Set (Commitment.State A W)) : Commitment.Space (Commitment.State A W)

A question keeps the root and proposes the continuations that carry one of the acts in P.

Equations

• Krifka2015.question C P = C.restrict ↑(upperClosure P)

theorem Krifka2015.mem_question {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) {P : Set (Commitment.State A W)} {d : Commitment.State A W} : d ∈ question C P ↔ d = C.root ∨ d ∈ C ∧ ∃ p ∈ P, p ⊆ d

theorem Krifka2015.question_singleton {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) (p : Commitment.State A W) : question C {p} = C.restrict ↑(C.update p)

A question proposing one act is the root together with the update by that act (27).

theorem Krifka2015.coe_question_union {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) (P Q : Set (Commitment.State A W)) : ↑(question C (P ∪ Q)) = ↑(question C P) ∪ ↑(question C Q)

A question is the disjunction of the questions proposing its acts (31), (34).

def Krifka2015.monopolarQuestion {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) (a : A) (φ : Set W) : Commitment.Space (Commitment.State A W)

A monopolar question proposes a's assertion of φ (27).

Equations

• Krifka2015.monopolarQuestion C a φ = Krifka2015.question C {{Commitment.commit a φ}}

def Krifka2015.bipolarQuestion {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) (a : A) (φ : Set W) : Commitment.Space (Commitment.State A W)

A bipolar question proposes a's assertion of φ or of ¬φ (23).

Equations

• Krifka2015.bipolarQuestion C a φ = Krifka2015.question C {{Commitment.commit a φ}, {Commitment.commit a φᶜ}}

def Krifka2015.highNegationQuestion {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) (a : A) (φ : Set W) : Commitment.Space (Commitment.State A W)

A question with high negation proposes a's refusal ¬S⊢φ (39).

Equations

• Krifka2015.highNegationQuestion C a φ = Krifka2015.question C {{Commitment.refuse a φ}}

theorem Krifka2015.mem_monopolarQuestion {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) (a : A) (φ : Set W) {d : Commitment.State A W} : d ∈ monopolarQuestion C a φ ↔ d = C.root ∨ d ∈ C ∧ Commitment.commit a φ ∈ d

theorem Krifka2015.coe_bipolarQuestion {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) (a : A) (φ : Set W) : ↑(bipolarQuestion C a φ) = ↑(monopolarQuestion C a φ) ∪ ↑(monopolarQuestion C a φᶜ)

A bipolar question is the disjunction of the two monopolar questions (31).

Answers

theorem Krifka2015.question_update_of_mem {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) {P : Set (Commitment.State A W)} {p : Commitment.State A W} (hp : p ∈ P) : (question C P).update p = C.update p

A proposed act is performed as it would have been before the question (24), (28).

theorem Krifka2015.question_update_of_forall {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) {P : Set (Commitment.State A W)} {k p : Commitment.State A W} (hk : ¬k ⊆ C.root) (hp : p ∈ P) (h : ∀ q ∈ P, q ≠ p → ∀ d ∈ C, ¬k ∪ q ⊆ d) : (question C P).update k = C.update (k ∪ p)

An act that moves the root and that, among the proposals, only p can accompany in a state of C is performed together with p.

def Krifka2015.Admits {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) (k : Commitment.State A W) : Prop

A space admits an act when the states that carry it have a least member, so that the update is again a commitment space (2), (3). An act the space does not admit needs a prior rejection.

Equations

• Krifka2015.Admits C k = ((C.update k).root ∈ C)

theorem Krifka2015.admits_question_iff_of_mem {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) {P : Set (Commitment.State A W)} {p : Commitment.State A W} (hp : p ∈ P) : Admits (question C P) p ↔ Admits C p

A proposed answer is admitted after the question iff it was admitted before.

theorem Krifka2015.admits_question_iff_of_forall {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) {P : Set (Commitment.State A W)} {k p : Commitment.State A W} (hk : ¬k ⊆ C.root) (hp : p ∈ P) (h : ∀ q ∈ P, q ≠ p → ∀ d ∈ C, ¬k ∪ q ⊆ d) : Admits (question C P) k ↔ Admits C (k ∪ p)

An act that only the proposal p can accompany is admitted after the question iff the space before it admits the two together.

theorem Krifka2015.question_singleton_update {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) {k : Commitment.State A W} (hk : ¬k ⊆ C.root) (p : Commitment.State A W) : (question C {p}).update k = C.update (k ∪ p)

After a question proposing only p, an act that moves the root is performed together with p.

theorem Krifka2015.admits_question_singleton_iff {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) {k : Commitment.State A W} (hk : ¬k ⊆ C.root) (p : Commitment.State A W) : Admits (question C {p}) k ↔ Admits C (k ∪ p)

After a question proposing only p, an act that moves the root is admitted iff the space before it admits the act together with p.

theorem Krifka2015.admits_update_iff {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) {k l : Commitment.State A W} (h : Admits C k) : Admits (C.update k) l ↔ Admits C (l ∪ k)

After an admitted act, a further act is admitted iff the space admits the two together.

Coherent states

def Krifka2015.Coherent {A : Type u_1} {W : Type u_2} (c : Commitment.State A W) : Prop

A commitment state is coherent when nobody is committed to a proposition while committed to its negation or refusing to commit to it (pp. 329, 340).

Equations

• Krifka2015.Coherent c = ∀ (a : A) (φ : Set W), Commitment.commit a φ ∈ c → Commitment.commit a φᶜ ∉ c ∧ Commitment.refuse a φ ∉ c

theorem Krifka2015.Coherent.mono {A : Type u_1} {W : Type u_2} {c d : Commitment.State A W} (h : c ⊆ d) (hd : Coherent d) : Coherent c

def Krifka2015.coherent (A : Type u_1) (W : Type u_2) : Commitment.Space (Commitment.State A W)

The space of coherent states, with no commitments at the root.

Equations

• Krifka2015.coherent A W = { carrier := {c : Commitment.State A W | Krifka2015.Coherent c}, root := ∅, isLeast' := ⋯ }

theorem Krifka2015.root_update_coherent {A : Type u_1} {W : Type u_2} {k : Commitment.State A W} (h : Coherent k) : ((coherent A W).update k).root = k

A coherent act is performed as it is.

theorem Krifka2015.admits_coherent_iff {A : Type u_1} {W : Type u_2} {k : Commitment.State A W} : Admits (coherent A W) k ↔ Coherent k

The coherent space admits exactly the coherent acts.

theorem Krifka2015.not_subset_root_coherent {A : Type u_1} {W : Type u_2} (x : Commitment A W) : ¬{x} ⊆ (coherent A W).root

theorem Krifka2015.coherent_commit {A : Type u_1} {W : Type u_2} {a : A} {φ : Set W} [Nonempty W] : Coherent {Commitment.commit a φ}

theorem Krifka2015.coherent_commit_compl_refuse {A : Type u_1} {W : Type u_2} {a : A} {φ : Set W} [Nonempty W] : Coherent {Commitment.commit a φᶜ, Commitment.refuse a φ}

theorem Krifka2015.coherent_commit_commit {A : Type u_1} {W : Type u_2} {a b : A} {φ : Set W} [Nonempty W] : Coherent {Commitment.commit a φ, Commitment.commit b φ}

theorem Krifka2015.coherent_commit_compl_commit {A : Type u_1} {W : Type u_2} {a b : A} {φ : Set W} [Nonempty W] (hab : a ≠ b) : Coherent {Commitment.commit a φᶜ, Commitment.commit b φ}

theorem Krifka2015.contextSet_singleton_commit {A : Type u_1} {W : Type u_2} (a : A) (φ : Set W) : Commitment.contextSet {Commitment.commit a φ} = φ

Which answers a question admits

theorem Krifka2015.monopolarQuestion_update_yes {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) (a : A) (φ : Set W) : (monopolarQuestion C a φ).update {Commitment.commit a φ} = C.assert a φ

Answering yes to a monopolar question is asserting φ (28a).

theorem Krifka2015.admits_monopolarQuestion_yes (A : Type u_1) (W : Type u_2) (a : A) (φ : Set W) [Nonempty W] : Admits (monopolarQuestion (coherent A W) a φ) {Commitment.commit a φ}

Yes to a monopolar question is admitted (28a).

theorem Krifka2015.not_admits_monopolarQuestion_no (A : Type u_1) (W : Type u_2) (a : A) (φ : Set W) : ¬Admits (monopolarQuestion (coherent A W) a φ) {Commitment.commit a φᶜ}

No to a monopolar question is not admitted, so it needs a prior rejection (28b).

theorem Krifka2015.admits_bipolarQuestion_yes (A : Type u_1) (W : Type u_2) (a : A) (φ : Set W) [Nonempty W] : Admits (bipolarQuestion (coherent A W) a φ) {Commitment.commit a φ}

Yes to a bipolar question is admitted (24).

theorem Krifka2015.admits_bipolarQuestion_no (A : Type u_1) (W : Type u_2) (a : A) (φ : Set W) [Nonempty W] : Admits (bipolarQuestion (coherent A W) a φ) {Commitment.commit a φᶜ}

No to a bipolar question is admitted (24).

theorem Krifka2015.highNegationQuestion_update_no (A : Type u_1) (W : Type u_2) (a : A) (φ : Set W) : (highNegationQuestion (coherent A W) a φ).update {Commitment.commit a φᶜ} = (coherent A W).update {Commitment.commit a φᶜ, Commitment.refuse a φ}

Answering no to a question with high negation is committing to ¬φ while refusing to commit to φ (p. 340).

theorem Krifka2015.root_highNegationQuestion_update_no (A : Type u_1) (W : Type u_2) (a : A) (φ : Set W) [Nonempty W] : ((highNegationQuestion (coherent A W) a φ).update {Commitment.commit a φᶜ}).root = {Commitment.commit a φᶜ, Commitment.refuse a φ}

No to a question with high negation lands on the state that keeps the refusal.

theorem Krifka2015.admits_highNegationQuestion_no (A : Type u_1) (W : Type u_2) (a : A) (φ : Set W) [Nonempty W] : Admits (highNegationQuestion (coherent A W) a φ) {Commitment.commit a φᶜ}

No to a question with high negation is admitted (p. 340).

theorem Krifka2015.not_admits_highNegationQuestion_yes (A : Type u_1) (W : Type u_2) (a : A) (φ : Set W) : ¬Admits (highNegationQuestion (coherent A W) a φ) {Commitment.commit a φ}

Yes to a question with high negation needs a prior rejection (p. 340).

Developments and rejection

structure Krifka2015.Development (S : Type u_1) [LE S] : Type u_1

A commitment space development (8) is the current space with the spaces the conversation has passed through, the latest first.

• current : Commitment.Space S
• past : List (Commitment.Space S)

def Krifka2015.Development.perform {S : Type u_1} [LE S] (D : Development S) (act : Commitment.Space S → Commitment.Space S) : Development S

Performing an act extends the development by its result (8).

Equations

• D.perform act = { current := act D.current, past := D.current :: D.past }

def Krifka2015.Development.reject {S : Type u_1} [LE S] (D : Development S) : Development S

Rejecting the last act returns to the space before it and keeps the record (10).

Equations

• D.reject = { current := D.past.headD D.current, past := D.current :: D.past }

@[simp]

theorem Krifka2015.Development.current_perform {S : Type u_1} [LE S] (D : Development S) (act : Commitment.Space S → Commitment.Space S) : (D.perform act).current = act D.current

@[simp]

theorem Krifka2015.Development.current_reject_perform {S : Type u_1} [LE S] (D : Development S) (act : Commitment.Space S → Commitment.Space S) : (D.perform act).reject.current = D.current

Rejecting an act restores the space it was performed on.

def Krifka2015.start (A : Type u_1) (W : Type u_2) : Development (Commitment.State A W)

A conversation starting from the coherent space.

Equations

• Krifka2015.start A W = { current := Krifka2015.coherent A W }

theorem Krifka2015.root_reject_monopolarQuestion_no {A : Type u_1} {W : Type u_2} [Nonempty W] (a : A) (φ : Set W) : (((start A W).perform fun (x : Commitment.Space (Commitment.State A W)) => monopolarQuestion x a φ).reject.perform fun (x : Commitment.Space (Commitment.State A W)) => x.assert a φᶜ).current.root = {Commitment.commit a φᶜ}

Rejecting a monopolar question and answering no leaves the addressee committed to ¬φ and to nothing else (28b).

The issue a space raises

def Krifka2015.continuations {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) : Set (Commitment.State A W)

The continuations of a space are its states other than the root.

Equations

• Krifka2015.continuations C = ↑C \ {C.root}

noncomputable def Krifka2015.toIssue {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) : Question W

The issue a space raises is settled by the information states inside some continuation's context set, or inside the root's when the space has no continuations.

Equations

• Krifka2015.toIssue C = if Krifka2015.continuations C = ∅ then Question.ofSet (Commitment.contextSet C.root) else ⨆ c ∈ Krifka2015.continuations C, Question.ofSet (Commitment.contextSet c)

@[instance_reducible]

noncomputable instance Krifka2015.instHasIssueSpaceState_studies {A : Type u_1} {W : Type u_2} : Discourse.HasIssue (Commitment.Space (Commitment.State A W)) W

Equations

• Krifka2015.instHasIssueSpaceState_studies = { toIssue := Krifka2015.toIssue }

theorem Krifka2015.mem_toIssue_iff {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) {i : Set W} : i ∈ toIssue C ↔ continuations C = ∅ ∧ i ⊆ Commitment.contextSet C.root ∨ ∃ c ∈ continuations C, i ⊆ Commitment.contextSet c

A two-world model

inductive Krifka2015.Weather : Type

In one world it is raining and in the other it is not.

• rain : Weather
• noRain : Weather

@[instance_reducible]

instance Krifka2015.instDecidableEqWeather : DecidableEq Weather

Equations

• Krifka2015.instDecidableEqWeather x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Krifka2015.instNonemptyWeather : Nonempty Weather

def Krifka2015.raining : Set Weather

It is raining.

Equations

• Krifka2015.raining = {Krifka2015.Weather.rain}

def Krifka2015.C₀ : Commitment.Space (Commitment.State Discourse.Role Weather)

The initial commitment space has every coherent state.

Equations

• Krifka2015.C₀ = Krifka2015.coherent Discourse.Role Krifka2015.Weather

theorem Krifka2015.assert_contextSet_vs_farkasBruce_cg : Commitment.contextSet (C₀.assert Discourse.Role.speaker raining).root = raining ∧ (Commitment.Table.empty.assert Discourse.Role.speaker raining).commonGround = ⊤

An assertion narrows the root at once, while the Table of [FB10] leaves the common ground as it was until the proposal is accepted.

theorem Krifka2015.monopolar_continuation_subset {φ : Set Weather} {c : Commitment.State Discourse.Role Weather} (hc : c ∈ continuations (monopolarQuestion C₀ Discourse.Role.addressee φ)) : Commitment.contextSet c ⊆ φ

Every continuation of the monopolar question records the addressee's commitment, so its context set lies inside the proposed proposition.

theorem Krifka2015.singleton_commit_mem_continuations (φ : Set Weather) : {Commitment.commit Discourse.Role.addressee φ} ∈ continuations (monopolarQuestion C₀ Discourse.Role.addressee φ)

theorem Krifka2015.monopolar_not_inquisitive : ¬(toIssue (monopolarQuestion C₀ Discourse.Role.addressee raining)).IsInquisitive

A monopolar question raises no inquisitive issue, so its bias is invisible to the issue observable.

theorem Krifka2015.bipolar_continuation_subset {c : Commitment.State Discourse.Role Weather} (hc : c ∈ continuations (bipolarQuestion C₀ Discourse.Role.addressee raining)) : Commitment.contextSet c ⊆ raining ∨ Commitment.contextSet c ⊆ rainingᶜ

Every continuation of the bipolar question records one of the two answers.

theorem Krifka2015.bipolar_inquisitive : (toIssue (bipolarQuestion C₀ Discourse.Role.addressee raining)).IsInquisitive

A bipolar question raises a genuine issue.

Table 1

def Krifka2015.evidence (φ : Set Weather) : SignType → Set Weather

The contextual evidence of [BG00] leaves open φ, its complement, or every world, according to the sign of φ it supports.

Equations

• Krifka2015.evidence φ SignType.pos = φ
• Krifka2015.evidence φ SignType.neg = φᶜ
• Krifka2015.evidence φ SignType.zero = Set.univ

def Krifka2015.MonopolarLicensed (E φ : Set Weather) : Prop

A monopolar question proposing S₂⊢φ is licensed by evidence for φ.

Equations

• Krifka2015.MonopolarLicensed E φ = (E ⊆ φ)

def Krifka2015.BipolarLicensed (E φ : Set Weather) : Prop

A bipolar question is licensed by neutral evidence.

Equations

• Krifka2015.BipolarLicensed E φ = (¬E ⊆ φ ∧ ¬E ⊆ φᶜ)

def Krifka2015.HighNegationLicensed (E φ : Set Weather) : Prop

The high-negation question, proposing the refusal ¬S₂⊢φ, is licensed wherever the evidence is not for φ.

Equations

• Krifka2015.HighNegationLicensed E φ = ¬E ⊆ φ

def Krifka2015.Licensed (E φ : Set Weather) : Option Polarity → Prop

Each question is licensed on particular readings. The question without negation, none, is licensed on either of its readings; the question with low negation, about ¬φ (some .negative), only on the monopolar reading of ¬φ; the question with high negation, about φ (some .positive), as such.

Equations

• Krifka2015.Licensed E φ none = (Krifka2015.MonopolarLicensed E φ ∨ Krifka2015.BipolarLicensed E φ)
• Krifka2015.Licensed E φ (some Polarity.negative) = Krifka2015.MonopolarLicensed E φᶜ
• Krifka2015.Licensed E φ (some Polarity.positive) = Krifka2015.HighNegationLicensed E φ

theorem Krifka2015.raining_ne_empty : raining ≠ ∅

theorem Krifka2015.raining_ne_univ : raining ≠ Set.univ

theorem Krifka2015.table1 (e : SignType) : (Licensed (evidence raining e) raining none ↔ e ≠ -1) ∧ (Licensed (evidence raining e) raining (some Polarity.negative) ↔ e = -1) ∧ (Licensed (evidence raining e) raining (some Polarity.positive) ↔ e ≠ 1)

Licensing reproduces Table 1. With evidence for φ only the question without negation is licensed, read monopolar; with neutral evidence the question without negation, read bipolar, and the high-negation question; with evidence against φ both negated questions and not the question without negation.

theorem Krifka2015.licensed_iff_felicitous (r : Option Polarity) (e : SignType) : Licensed (evidence raining e) raining r ↔ BuringGunlogson2000.Felicitous r e

The licensing conditions are the evidence conditions of [BG00].

Question tags (44), (45)

def Krifka2015.matchingTag {W : Type u_1} (C : Commitment.Space (Commitment.State Discourse.Role W)) (φ : Set W) : Set (Commitment.State Discourse.Role W)

A matching tag conjoins the assertion with the monopolar question of the same content (44).

Equations

• Krifka2015.matchingTag C φ = ↑(C.assert Discourse.Role.speaker φ) ∩ ↑(Krifka2015.monopolarQuestion C Discourse.Role.addressee φ)

def Krifka2015.reverseTag {W : Type u_1} (C : Commitment.Space (Commitment.State Discourse.Role W)) (φ : Set W) : Set (Commitment.State Discourse.Role W)

A reverse tag disjoins the assertion with the monopolar question of the negation (45).

Equations

• Krifka2015.reverseTag C φ = ↑(C.assert Discourse.Role.speaker φ) ∪ ↑(Krifka2015.monopolarQuestion C Discourse.Role.addressee φᶜ)

theorem Krifka2015.matchingTag_eq {W : Type u_1} (C : Commitment.Space (Commitment.State Discourse.Role W)) (φ : Set W) (hk : Commitment.commit Discourse.Role.speaker φ ∉ C.root) (h : Admits C {Commitment.commit Discourse.Role.addressee φ, Commitment.commit Discourse.Role.speaker φ}) : matchingTag C φ = ↑(C.update {Commitment.commit Discourse.Role.addressee φ, Commitment.commit Discourse.Role.speaker φ})

A matching tag is the single act committing both participants (p. 342).

theorem Krifka2015.reverseTag_eq {W : Type u_1} (C : Commitment.Space (Commitment.State Discourse.Role W)) (φ : Set W) (h : Admits C {Commitment.commit Discourse.Role.speaker φ}) : reverseTag C φ = ↑(question C {{Commitment.commit Discourse.Role.speaker φ}, {Commitment.commit Discourse.Role.addressee φᶜ}})

A reverse tag is the question proposing the speaker's assertion or the addressee's assertion of the negation, when the space admits the former.

theorem Krifka2015.isLeast_reverseTag {W : Type u_1} (C : Commitment.Space (Commitment.State Discourse.Role W)) (φ : Set W) : IsLeast (reverseTag C φ) C.root

A reverse tag keeps the root, the speaker's commitment being only one branch.

theorem Krifka2015.commit_speaker_mem_root_assert_assert {W : Type u_1} (C : Commitment.Space (Commitment.State Discourse.Role W)) (φ ψ : Set W) : Commitment.commit Discourse.Role.speaker φ ∈ ((C.assert Discourse.Role.speaker φ).assert Discourse.Role.addressee ψ).root

When the addressee contradicts a plain assertion, the speaker is still committed (p. 342).

theorem Krifka2015.isLeast_matchingTag (W : Type u_1) (φ : Set W) [Nonempty W] : IsLeast (matchingTag (coherent Discourse.Role W) φ) {Commitment.commit Discourse.Role.addressee φ, Commitment.commit Discourse.Role.speaker φ}

After a matching tag both participants are committed at the root.

theorem Krifka2015.not_admits_matchingTag_no (W : Type u_1) (φ : Set W) [Nonempty W] : ¬Admits ((coherent Discourse.Role W).update {Commitment.commit Discourse.Role.addressee φ, Commitment.commit Discourse.Role.speaker φ}) {Commitment.commit Discourse.Role.addressee φᶜ}

After a matching tag no needs a prior rejection (p. 342).

theorem Krifka2015.root_reject_matchingTag_no (W : Type u_1) (φ : Set W) [Nonempty W] : (((start Discourse.Role W).perform fun (x : Commitment.Space (Commitment.State Discourse.Role W)) => x.update {Commitment.commit Discourse.Role.addressee φ, Commitment.commit Discourse.Role.speaker φ}).reject.perform fun (x : Commitment.Space (Commitment.State Discourse.Role W)) => x.assert Discourse.Role.addressee φᶜ).current.root = {Commitment.commit Discourse.Role.addressee φᶜ}

Rejecting an assertion with a matching tag and answering no leaves only the addressee's commitment, the speaker's being rejected with the tag (p. 342).

theorem Krifka2015.admits_assert_no (W : Type u_1) (φ : Set W) [Nonempty W] : Admits ((coherent Discourse.Role W).assert Discourse.Role.speaker φ) {Commitment.commit Discourse.Role.addressee φᶜ}

A plain assertion admits the addressee's no without a rejection.

theorem Krifka2015.root_reverseTag_update_yes (W : Type u_1) (φ : Set W) [Nonempty W] : ((question (coherent Discourse.Role W) {{Commitment.commit Discourse.Role.speaker φ}, {Commitment.commit Discourse.Role.addressee φᶜ}}).update {Commitment.commit Discourse.Role.addressee φ}).root = {Commitment.commit Discourse.Role.addressee φ, Commitment.commit Discourse.Role.speaker φ}

After a reverse tag, the addressee's commitment to φ brings the speaker's with it (p. 343).

theorem Krifka2015.root_reverseTag_update_no (W : Type u_1) (φ : Set W) [Nonempty W] : ((question (coherent Discourse.Role W) {{Commitment.commit Discourse.Role.speaker φ}, {Commitment.commit Discourse.Role.addressee φᶜ}}).update {Commitment.commit Discourse.Role.addressee φᶜ}).root = {Commitment.commit Discourse.Role.addressee φᶜ}

After a reverse tag, the addressee's no leaves the speaker uncommitted (p. 343).