Gunlogson (2001): True to Form: Rising and Falling Declaratives as Questions in English

This file formalizes chapters 3 and 4 of [Gun01], the context-update semantics of rising and falling declaratives and the account of when a declarative can be a polar question. A context is a pair of commitment sets, and a locution, a sentence type with its intonation (73), updates one of them: a declarative narrows the targeted set to its content (74), an interrogative leaves it alone (87), and the rise or fall selects the addressee's or the speaker's set (75), (76), Locution.update. The statuses of a proposition in a context, commitment, joint commitment, resolution, controversy, bias, and neutrality (63) to (68), are those of Discourse/Commitment/Declarative.lean; this file adds the reduction-set characterization of bias (69) to (71), IsBiasedR. Chapter 3 classifies locutions by their effect: the theorems that no declarative is neutral and no interrogative biasing (91), (92), Locution.not_isNeutralIn_of_decl, the expression of commitment (93), and entailment, informativeness, and vacuousness (94) to (101), which separate a locution entailed by a context from one uninformative in it. Chapter 4 defines a polar question as a locution uninformative with respect to the addressee's commitment set (104), (132), Locution.IsPolarQuestion, which for a declarative is the Contextual Bias Condition (105), makes every rising declarative question reiterative (134) and without effect (133), and makes the falling declarative the only resolving question (135). The dissertation's locution triples are the rows of Data.Examples.Gunlogson2001.

Implementation notes

Presuppositional admittance, (83) and (84), is not modelled, so consistency (86) is the nonemptiness of the updated commitment sets, and the second clause of the final definition of polar question (136), which is not a condition on commitment sets, is left out. Theorem (91) does not hold as stated: a resolved proposition is controversial for no one under (66), so a resolved context is neutral under (68), and a declarative whose content the addressee already holds makes it a joint commitment and so is neutral, Locution.isNeutralIn_fallingDecl. The theorem holds when the content stays unresolved, which is the form given here, and (93) correspondingly fails for declaratives as literally defined. The reduction-set definition of bias (71), which the paper says is equivalent to (67), agrees with it exactly on unresolved propositions, isBiasedR_iff_isBiased_of_not_isResolved and isBiasedR_of_isJoint.

References

• [Gun01]

Contextual bias through the reduction set, section 3.1

def Gunlogson2001.Accessible {W : Type u_1} (K K' : Commitment.State Discourse.Role W) : Prop

(69): K' is reductively accessible from K when each commitment set shrinks to a nonempty subset.

Equations

• Gunlogson2001.Accessible K K' = ((∀ (x : Discourse.Role), Commitment.commitmentSet K' x ⊆ Commitment.commitmentSet K x) ∧ ∀ (x : Discourse.Role), (Commitment.commitmentSet K' x).Nonempty)

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

(71): K is biased toward p when some accessible context settles p and none settles pᶜ.

Equations

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

theorem Gunlogson2001.exists_accessible_iff {W : Type u_1} (K : Commitment.State Discourse.Role W) (q : Set W) : (∃ (K' : Commitment.State Discourse.Role W), Accessible K K' ∧ ∀ (x : Discourse.Role), Commitment.commitmentSet K' x ⊆ q) ↔ ∀ (x : Discourse.Role), (Commitment.commitmentSet K x ∩ q).Nonempty

Some accessible context settles q iff q meets every commitment set.

theorem Gunlogson2001.isBiasedR_iff {W : Type u_1} {K : Commitment.State Discourse.Role W} {p : Set W} : IsBiasedR K p ↔ (∀ (x : Discourse.Role), (Commitment.commitmentSet K x ∩ p).Nonempty) ∧ ∃ (x : Discourse.Role), Commitment.commitmentSet K x ⊆ p

The reduction-set bias unfolds to: p meets every commitment set, and some participant is committed to it.

theorem Gunlogson2001.isBiasedR_iff_isBiased_of_not_isResolved {W : Type u_1} {K : Commitment.State Discourse.Role W} {p : Set W} (hu : ¬Commitment.IsResolved K p) : IsBiasedR K p ↔ Commitment.IsBiased K p

(67) and (71) agree on unresolved propositions.

theorem Gunlogson2001.isBiasedR_of_isJoint {W : Type u_1} {K : Commitment.State Discourse.Role W} {p : Set W} (h : Commitment.IsJoint K p) : IsBiasedR K p

(71) holds of a context in which p is a joint commitment, where (67) fails, since a resolved context is neutral under (68): the two definitions of bias part at resolved propositions.

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

Locutions and their context change potentials, sections 3.2 and 3.3

inductive Gunlogson2001.SentenceType : Type

(73d): the sentence types.

• decl : SentenceType
• interr : SentenceType

@[instance_reducible]

instance Gunlogson2001.instDecidableEqSentenceType : DecidableEq SentenceType

Equations

• Gunlogson2001.instDecidableEqSentenceType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Gunlogson2001.SentenceType.update {W : Type u_1} (p : Set W) : SentenceType → Set W → Set W

(74) and (87): a declarative with content p narrows a commitment set to p; an interrogative leaves it alone.

Equations

• Gunlogson2001.SentenceType.update p Gunlogson2001.SentenceType.decl x✝ = p ∩ x✝
• Gunlogson2001.SentenceType.update p Gunlogson2001.SentenceType.interr x✝ = x✝

def Gunlogson2001.SentenceType.Entails {W : Type u_1} (S : SentenceType) (cs p : Set W) : Prop

(95): a commitment set entails a sentence when updating with it has no effect.

Equations

• S.Entails cs p = (Gunlogson2001.SentenceType.update p S cs = cs)

theorem Gunlogson2001.SentenceType.entails_decl_iff {W : Type u_1} {p cs : Set W} : decl.Entails cs p ↔ cs ⊆ p

theorem Gunlogson2001.SentenceType.entails_interr {W : Type u_1} {p cs : Set W} : interr.Entails cs p

inductive Gunlogson2001.Locution : Type

(73e): the locutions, a sentence type with a rise or a fall.

• risingDecl : Locution
• fallingDecl : Locution
• risingInterr : Locution

@[instance_reducible]

instance Gunlogson2001.instDecidableEqLocution : DecidableEq Locution

Equations

• Gunlogson2001.instDecidableEqLocution x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Gunlogson2001.Locution.sentenceType : Locution → SentenceType

The sentence type of a locution.

Equations

• Gunlogson2001.Locution.risingInterr.sentenceType = Gunlogson2001.SentenceType.interr
• x✝.sentenceType = Gunlogson2001.SentenceType.decl

def Gunlogson2001.Locution.target : Locution → Discourse.Role

(75) and (76): the commitment set the intonation targets, the addressee's under a rise and the speaker's under a fall.

Equations

• Gunlogson2001.Locution.fallingDecl.target = Discourse.Role.speaker
• x✝.target = Discourse.Role.addressee

def Gunlogson2001.Locution.update {W : Type u_1} (p : Set W) : Locution → Commitment.State Discourse.Role W → Commitment.State Discourse.Role W

(77), (78), and (88): the context change potential of a locution with descriptive content p.

Equations

• Gunlogson2001.Locution.update p Gunlogson2001.Locution.risingDecl x✝ = Commitment.rising x✝ p
• Gunlogson2001.Locution.update p Gunlogson2001.Locution.fallingDecl x✝ = Commitment.falling x✝ p
• Gunlogson2001.Locution.update p Gunlogson2001.Locution.risingInterr x✝ = x✝

theorem Gunlogson2001.Locution.commitmentSet_update_target {W : Type u_1} {K : Commitment.State Discourse.Role W} {p : Set W} (L : Locution) : Commitment.commitmentSet (update p L K) L.target = SentenceType.update p L.sentenceType (Commitment.commitmentSet K L.target)

(81): the locution applies its sentence meaning to the targeted commitment set.

theorem Gunlogson2001.Locution.commitmentSet_update_of_ne {W : Type u_1} {K : Commitment.State Discourse.Role W} {p : Set W} (L : Locution) {x : Discourse.Role} (h : x ≠ L.target) : Commitment.commitmentSet (update p L K) x = Commitment.commitmentSet K x

(81): the other commitment set is unchanged.

def Gunlogson2001.Locution.Consistent {W : Type u_1} (L : Locution) (K : Commitment.State Discourse.Role W) (p : Set W) : Prop

(86): L with content p is consistent with K when every updated commitment set is nonempty.

Equations

• L.Consistent K p = ∀ (x : Discourse.Role), (Commitment.commitmentSet (Gunlogson2001.Locution.update p L K) x).Nonempty

Locutionary bias and neutrality, section 3.4

def Gunlogson2001.Locution.IsNeutralIn {W : Type u_1} (L : Locution) (K : Commitment.State Discourse.Role W) (p : Set W) : Prop

(89): L is neutral with respect to K when the updated context is neutral.

Equations

• L.IsNeutralIn K p = Commitment.IsNeutral (Gunlogson2001.Locution.update p L K) p

def Gunlogson2001.Locution.IsBiasingIn {W : Type u_1} (L : Locution) (K : Commitment.State Discourse.Role W) (p : Set W) : Prop

(90): L is biasing with respect to K when it takes a neutral context to a biased one.

Equations

• L.IsBiasingIn K p = (Commitment.IsNeutral K p ∧ Commitment.IsBiased (Gunlogson2001.Locution.update p L K) p)

theorem Gunlogson2001.Locution.not_isNeutralIn_of_decl {W : Type u_1} {K : Commitment.State Discourse.Role W} {p : Set W} (L : Locution) (hL : L.sentenceType = SentenceType.decl) (hc : L.Consistent K p) (hu : ¬Commitment.IsResolved (update p L K) p) : ¬L.IsNeutralIn K p

(91): no declarative is neutral with respect to a context it is consistent with, provided its content stays unresolved: the targeted participant is committed to the content afterwards, so its negation is controversial.

theorem Gunlogson2001.Locution.isNeutralIn_fallingDecl {W : Type u_1} {K : Commitment.State Discourse.Role W} {p : Set W} (ha : Commitment.IsCommitmentOf K Discourse.Role.addressee p) (hs : (p ∩ Commitment.commitmentSet K Discourse.Role.speaker).Nonempty) : fallingDecl.IsNeutralIn K p

The proviso cannot be dropped: a falling declarative whose content the addressee already holds makes it a joint commitment, and a resolved context is neutral under (68).

theorem Gunlogson2001.Locution.isBiasingIn_of_decl {W : Type u_1} {K : Commitment.State Discourse.Role W} {p : Set W} (L : Locution) (hL : L.sentenceType = SentenceType.decl) (h : Commitment.IsNeutral K p) (hu : ¬Commitment.IsResolved K p) (hne : ∀ (x : Discourse.Role), (Commitment.commitmentSet K x).Nonempty) : L.IsBiasingIn K p

A declarative in a neutral, unresolved, nonempty context is biasing.

theorem Gunlogson2001.Locution.not_isBiasingIn_risingInterr {W : Type u_1} {K : Commitment.State Discourse.Role W} {p : Set W} : ¬risingInterr.IsBiasingIn K p

(92): no interrogative is biasing: it leaves the context as it is, and a neutral context is not biased.

def Gunlogson2001.Locution.ExpressesCommitment {W : Type u_1} (L : Locution) (p : Set W) : Prop

(93): L expresses commitment to p when no context consistent with it comes out neutral.

Equations

• L.ExpressesCommitment p = ∀ (K : Commitment.State Discourse.Role W), L.Consistent K p → ¬L.IsNeutralIn K p

theorem Gunlogson2001.Locution.not_expressesCommitment_risingInterr {W : Type u_1} {p : Set W} (h₀ : p.Nonempty) (h₁ : pᶜ.Nonempty) : ¬risingInterr.ExpressesCommitment p

An interrogative does not express commitment: the empty context is neutral toward any contingent proposition and stays so.

theorem Gunlogson2001.Locution.not_expressesCommitment_fallingDecl {W : Type u_1} {p : Set W} (h₀ : p.Nonempty) : ¬fallingDecl.ExpressesCommitment p

Nor, as literally defined, does a falling declarative, (93) inheriting the gap in (91): a context in which only the addressee holds p is consistent with it and comes out neutral.

Entailment, informativeness, and vacuousness, section 3.5

def Gunlogson2001.Locution.Entails {W : Type u_1} (L : Locution) (K : Commitment.State Discourse.Role W) (p : Set W) : Prop

(94): a context entails a locution when the update leaves every commitment set as it was.

Equations

• L.Entails K p = ∀ (x : Discourse.Role), Commitment.commitmentSet (Gunlogson2001.Locution.update p L K) x = Commitment.commitmentSet K x

theorem Gunlogson2001.Locution.entails_iff {W : Type u_1} {K : Commitment.State Discourse.Role W} {p : Set W} (L : Locution) : L.Entails K p ↔ L.sentenceType.Entails (Commitment.commitmentSet K L.target) p

A context entails a locution iff the targeted commitment set entails its sentence.

def Gunlogson2001.Locution.Uninformative {W : Type u_1} (L : Locution) (K : Commitment.State Discourse.Role W) (x : Discourse.Role) (p : Set W) : Prop

(97): L is uninformative with respect to x's commitment set when the set entails its sentence.

Equations

• L.Uninformative K x p = L.sentenceType.Entails (Commitment.commitmentSet K x) p

def Gunlogson2001.Locution.UninformativeIn {W : Type u_1} (L : Locution) (K : Commitment.State Discourse.Role W) (p : Set W) : Prop

(99): uninformative with respect to every commitment set.

Equations

• L.UninformativeIn K p = ∀ (x : Discourse.Role), L.Uninformative K x p

def Gunlogson2001.Locution.InformativeIn {W : Type u_1} (L : Locution) (K : Commitment.State Discourse.Role W) (p : Set W) : Prop

(98): informative with respect to some commitment set.

Equations

• L.InformativeIn K p = ∃ (x : Discourse.Role), ¬L.Uninformative K x p

theorem Gunlogson2001.Locution.uninformative_risingInterr {W : Type u_1} {K : Commitment.State Discourse.Role W} {p : Set W} (x : Discourse.Role) : risingInterr.Uninformative K x p

An interrogative is uninformative with respect to every commitment set.

theorem Gunlogson2001.Locution.uninformative_iff_of_decl {W : Type u_1} {K : Commitment.State Discourse.Role W} {p : Set W} (L : Locution) (hL : L.sentenceType = SentenceType.decl) {x : Discourse.Role} : L.Uninformative K x p ↔ Commitment.commitmentSet K x ⊆ p

A declarative is uninformative with respect to a commitment set already within its content.

theorem Gunlogson2001.Locution.entails_and_informativeIn_fallingDecl {W : Type u_1} {K : Commitment.State Discourse.Role W} {p : Set W} (hs : Commitment.commitmentSet K Discourse.Role.speaker ⊆ p) (ha : ¬Commitment.commitmentSet K Discourse.Role.addressee ⊆ p) : fallingDecl.Entails K p ∧ fallingDecl.InformativeIn K p

(100): a falling declarative reiterating the speaker's commitment is entailed by the context yet informative with respect to the addressee.

theorem Gunlogson2001.Locution.uninformative_of_isCommitmentOf {W : Type u_1} {K : Commitment.State Discourse.Role W} {p : Set W} (L : Locution) {x : Discourse.Role} (h : Commitment.IsCommitmentOf K x p) : L.Uninformative K x p

theorem Gunlogson2001.Locution.uninformativeIn_and_entails_of_isJoint {W : Type u_1} {K : Commitment.State Discourse.Role W} {p : Set W} (L : Locution) (h : Commitment.IsJoint K p) : L.UninformativeIn K p ∧ L.Entails K p

(101): a locution whose content is a joint commitment is vacuous; it is then uninformative with respect to the context and entailed by it.

Polar questions, chapter 4

def Gunlogson2001.Locution.IsPolarQuestion {W : Type u_1} (L : Locution) (K : Commitment.State Discourse.Role W) (p : Set W) : Prop

(132), the Uninformativeness Condition (104) taken as necessary and sufficient: an utterance of L is a polar question in K when L is uninformative with respect to the addressee's commitment set.

Equations

• L.IsPolarQuestion K p = L.Uninformative K Discourse.Role.addressee p

theorem Gunlogson2001.Locution.isPolarQuestion_risingInterr {W : Type u_1} {K : Commitment.State Discourse.Role W} {p : Set W} : risingInterr.IsPolarQuestion K p

(131): every rising interrogative is a polar question.

theorem Gunlogson2001.Locution.isPolarQuestion_iff_of_decl {W : Type u_1} {K : Commitment.State Discourse.Role W} {p : Set W} (L : Locution) (hL : L.sentenceType = SentenceType.decl) : L.IsPolarQuestion K p ↔ Commitment.commitmentSet K Discourse.Role.addressee ⊆ p

(105), the Contextual Bias Condition: a declarative is a polar question only where the addressee is already committed to its content.

theorem Gunlogson2001.Locution.entails_of_isPolarQuestion_risingDecl {W : Type u_1} {K : Commitment.State Discourse.Role W} {p : Set W} (h : risingDecl.IsPolarQuestion K p) : risingDecl.Entails K p

(133): a rising declarative that is a polar question has the effect of the interrogative with the same content, none.

def Gunlogson2001.Locution.IsReiterativeQuestion {W : Type u_1} (L : Locution) (K : Commitment.State Discourse.Role W) (p : Set W) : Prop

(134): a reiterative question, a polar question whose content the addressee is committed to.

Equations

• L.IsReiterativeQuestion K p = (L.IsPolarQuestion K p ∧ Commitment.IsCommitmentOf K Discourse.Role.addressee p)

theorem Gunlogson2001.Locution.isReiterativeQuestion_risingDecl {W : Type u_1} {K : Commitment.State Discourse.Role W} {p : Set W} (hne : (Commitment.commitmentSet K Discourse.Role.addressee).Nonempty) (h : risingDecl.IsPolarQuestion K p) : risingDecl.IsReiterativeQuestion K p

Every rising declarative polar question is reiterative, given a nonempty addressee set.

def Gunlogson2001.Locution.IsResolvingQuestion {W : Type u_1} (L : Locution) (K : Commitment.State Discourse.Role W) (p : Set W) : Prop

(135): a resolving question, a reiterative question that takes its unresolved content to a joint commitment.

Equations

• L.IsResolvingQuestion K p = (L.IsReiterativeQuestion K p ∧ ¬Commitment.IsResolved K p ∧ Commitment.IsJoint (Gunlogson2001.Locution.update p L K) p)

theorem Gunlogson2001.Locution.eq_fallingDecl_of_isResolvingQuestion {W : Type u_1} {K : Commitment.State Discourse.Role W} {p : Set W} (L : Locution) (h : L.IsResolvingQuestion K p) : L = fallingDecl

Only a falling declarative can be a resolving question: the others leave the speaker's commitment set alone, so the content was already joint.

theorem Gunlogson2001.Locution.isJoint_of_entails_of_isPolarQuestion_fallingDecl {W : Type u_1} {K : Commitment.State Discourse.Role W} {p : Set W} (hne : ∀ (x : Discourse.Role), (Commitment.commitmentSet K x).Nonempty) (he : fallingDecl.Entails K p) (hq : fallingDecl.IsPolarQuestion K p) : Commitment.IsJoint K p

A falling declarative question has the effect of the interrogative only when it is vacuous: entailed and a polar question, its content is a joint commitment.