Rising and falling declaratives

[Gun01] represents a two-party context as the pair of the participants' commitment sets, the worlds compatible with each one's public beliefs (60), and reads a declarative's intonation as choosing whose commitment set its content updates: falling for the speaker's, rising for the addressee's (77), (78). Which participant is committed to what defines the statuses of a proposition — a commitment of a participant, a joint commitment, resolved, controversial — and the bias of a context toward it (63)–(68). [Gun08] refines the addressee's commitment under a rising declarative as attributed by the speaker rather than self-generated, the Commitment.Source coordinate.

Main definitions

• Commitment.commitmentSet — cs_X (60).
• Commitment.falling, Commitment.rising — (78), (77).
• Commitment.IsCommitmentOf, IsJoint, IsResolved, IsControversial, IsBiased, IsNeutral — (63)–(68).

Main results

• Commitment.commitmentSet_falling, Commitment.commitmentSet_rising — each intonation narrows exactly one commitment set.
• Commitment.isBiased_falling, Commitment.isBiased_rising — a declarative in a neutral, unresolved context biases it toward its content.
• Commitment.IsResolved.isNeutral — a resolved context is neutral under (68), since (66) makes a resolved proposition controversial for no one.

References

• C. Gunlogson, True to Form: Rising and Falling Declaratives as Questions in English (2001)
• C. Gunlogson, A Question of Commitment (2008)

def Commitment.commitmentSet {W : Type u_1} (K : State Discourse.Role W) (x : Discourse.Role) : Set W

cs_X (60): the worlds compatible with x's public commitments.

Equations

• Commitment.commitmentSet K x = Commitment.contextSet (Commitment.ofCommitter K x)

def Commitment.falling {W : Type u_1} (K : State Discourse.Role W) (p : Set W) : State Discourse.Role W

A falling declarative (78): the speaker commits to p.

Equations

• Commitment.falling K p = insert (Commitment.commit Discourse.Role.speaker p) K

def Commitment.rising {W : Type u_1} (K : State Discourse.Role W) (p : Set W) : State Discourse.Role W

A rising declarative (77): the addressee is committed to p, attributed by the speaker.

Equations

• Commitment.rising K p = insert (Commitment.commit Discourse.Role.addressee p Commitment.Force.doxastic Commitment.Source.otherGenerated) K

def Commitment.IsCommitmentOf {W : Type u_1} (K : State Discourse.Role W) (x : Discourse.Role) (p : Set W) : Prop

(63): p is a commitment of x.

Equations

• Commitment.IsCommitmentOf K x p = ((Commitment.commitmentSet K x).Nonempty ∧ Commitment.commitmentSet K x ⊆ p)

def Commitment.IsJoint {W : Type u_1} (K : State Discourse.Role W) (p : Set W) : Prop

(64): p is a joint commitment.

Equations

• Commitment.IsJoint K p = ∀ (x : Discourse.Role), Commitment.IsCommitmentOf K x p

def Commitment.IsResolved {W : Type u_1} (K : State Discourse.Role W) (p : Set W) : Prop

(65): p is resolved.

Equations

• Commitment.IsResolved K p = (Commitment.IsJoint K p ∨ Commitment.IsJoint K pᶜ)

def Commitment.IsControversial {W : Type u_1} (K : State Discourse.Role W) (p : Set W) : Prop

(66): p is controversial — someone is committed against it, it is unresolved, and no commitment set is empty.

Equations

• Commitment.IsControversial K p = ((∃ (x : Discourse.Role), Commitment.IsCommitmentOf K x pᶜ) ∧ ¬Commitment.IsResolved K p ∧ ∀ (x : Discourse.Role), (Commitment.commitmentSet K x).Nonempty)

def Commitment.IsBiased {W : Type u_1} (K : State Discourse.Role W) (p : Set W) : Prop

(67): the context is biased toward p.

Equations

• Commitment.IsBiased K p = (Commitment.IsControversial K pᶜ ∧ ¬Commitment.IsControversial K p)

def Commitment.IsNeutral {W : Type u_1} (K : State Discourse.Role W) (p : Set W) : Prop

(68): the context is neutral with respect to p.

Equations

• Commitment.IsNeutral K p = (¬Commitment.IsControversial K p ∧ ¬Commitment.IsControversial K pᶜ)

@[simp]

theorem Commitment.commitmentSet_empty {W : Type u_1} (x : Discourse.Role) : commitmentSet ∅ x = Set.univ

theorem Commitment.commitmentSet_falling {W : Type u_1} (K : State Discourse.Role W) (p : Set W) : commitmentSet (falling K p) Discourse.Role.speaker = p ∩ commitmentSet K Discourse.Role.speaker ∧ commitmentSet (falling K p) Discourse.Role.addressee = commitmentSet K Discourse.Role.addressee

A falling declarative narrows the speaker's commitment set by its content and leaves the addressee's alone.

theorem Commitment.commitmentSet_rising {W : Type u_1} (K : State Discourse.Role W) (p : Set W) : commitmentSet (rising K p) Discourse.Role.addressee = p ∩ commitmentSet K Discourse.Role.addressee ∧ commitmentSet (rising K p) Discourse.Role.speaker = commitmentSet K Discourse.Role.speaker

A rising declarative narrows the addressee's commitment set by its content and leaves the speaker's alone.

Statuses

@[simp]

theorem Commitment.isResolved_compl {W : Type u_1} {K : State Discourse.Role W} {p : Set W} : IsResolved K pᶜ ↔ IsResolved K p

theorem Commitment.IsResolved.isNeutral {W : Type u_1} {K : State Discourse.Role W} {p : Set W} (h : IsResolved K p) : IsNeutral K p

A resolved proposition is controversial for no one, so a resolved context is neutral.

theorem Commitment.IsNeutral.not_isBiased {W : Type u_1} {K : State Discourse.Role W} {p : Set W} (h : IsNeutral K p) : ¬IsBiased K p

theorem Commitment.IsNeutral.not_subset {W : Type u_1} {K : State Discourse.Role W} {p : Set W} (h : IsNeutral K p) (hu : ¬IsResolved K p) (hne : ∀ (x : Discourse.Role), (commitmentSet K x).Nonempty) (x : Discourse.Role) : ¬commitmentSet K x ⊆ p ∧ ¬commitmentSet K x ⊆ pᶜ

In a neutral, unresolved, nonempty context no participant is committed either way.

theorem Commitment.isBiased_of_commitmentSet_eq {W : Type u_1} {K : State Discourse.Role W} {p : Set W} {K' : State Discourse.Role W} {y : Discourse.Role} (h : IsNeutral K p) (hu : ¬IsResolved K p) (hne : ∀ (x : Discourse.Role), (commitmentSet K x).Nonempty) (hy : commitmentSet K' y = p ∩ commitmentSet K y) (hx : ∀ (x : Discourse.Role), x ≠ y → commitmentSet K' x = commitmentSet K x) : IsBiased K' p

Narrowing one participant's commitment set to p in a neutral, unresolved, nonempty context biases it toward p.

theorem Commitment.isBiased_falling {W : Type u_1} {K : State Discourse.Role W} {p : Set W} (h : IsNeutral K p) (hu : ¬IsResolved K p) (hne : ∀ (x : Discourse.Role), (commitmentSet K x).Nonempty) : IsBiased (falling K p) p

A falling declarative in a neutral, unresolved, nonempty context biases it toward its content.

theorem Commitment.isBiased_rising {W : Type u_1} {K : State Discourse.Role W} {p : Set W} (h : IsNeutral K p) (hu : ¬IsResolved K p) (hne : ∀ (x : Discourse.Role), (commitmentSet K x).Nonempty) : IsBiased (rising K p) p

A rising declarative in a neutral, unresolved, nonempty context biases it toward its content.