Farkas and Roelofsen (2017): Division of Labor in Declaratives and Interrogatives

This file formalizes [FR17]'s account of falling and rising declaratives, polar interrogatives and tag interrogatives: their inquisitive semantics, the single basic convention of use that replaces the Fregean force operators, and the special discourse effects of the marked forms. A sentence form is a clause-type marker with an intonation, or a declarative anchor with a tag (Form, §4.1); the markers are interpreted by the projection operators of inquisitive semantics (31), (34), (36): dec is the non-inquisitive projection, the double complement Pᶜᶜ, int the non-informative projection Question.query applied only to a non-inquisitive argument, falling intonation is vacuous and rising intonation is Question.query again. Form.interpret composes them as in (37)–(40): a falling declarative expresses !P and every other form ?!P, so that with a non-inquisitive radical the rising declarative, the polar interrogatives and the tag interrogatives express one and the same inquisitive proposition (interpret_declarative_falling, interpret_marked, interpret_interrogative_ofSet, isInquisitive_interpret_ofSet; (41) and (43)). Among the forms for that content the polar interrogatives are optimal and the rest marked (Form.IsMarked, (47)).

A discourse context is a stack of propositions, a commitment state, and for each participant the possibilities she has signalled evidence for with a credence interval (the paper's (22) and §3.2; Context, Context.cs, Context.cg, Context.CommonlyDecided). The basic convention of use Context.basic puts the proposition on the table and commits the speaker to its informative content (48); a falling declarative thereby commits her to the radical and the inquisitive forms commit her to nothing (cs_basic_declarative_falling, cs_basic_of_isInquisitive; their (49) and (50)). The special effects of the marked forms add the highlighted alternative to the speaker's evidence with the credence interval of (52), (56) and (58), [zero, low] for the rising declarative, [moderate, high] for the rising tag and [high] for the falling tag (Form.specialEffect); Context.utter is the full conventional effect, and utter_eq_basic_of_not_isMarked is the division of labor principle (21): the discourse effects of the unmarked forms are the basic convention alone. §6 tests the account in contexts that fix the speaker's evidence and credence; Felicitous renders the reasoning of that section on a Situation, and rows_felicitous checks it against all sixty judgments of (53)–(77).

Implementation notes

• The felicity conditions of §6 are the paper's prose reasoning made explicit: a commitment to the radical needs high credence to be possible in the context; an inquisitive proposition on the table needs an addressee who is not neutral (61); an unmarked inquisitive form presents the speaker as neutral, which needs low credence to be possible (the paper's (63) against (65) and (67)); a marked form needs evidence for the highlighted alternative and a credence the context allows within the form's interval.
• The paper's ⟨?⟩ is a classical case split on inquisitiveness, so Form.interpret is noncomputable. Highlighting is the radical's own alternative, which the operators leave in place, so the forms take the radical's proposition ofSet α and α is the highlighted alternative by construction.
• The common ground is derived from the commitment sets as the paper derives it, not stored.

References

• [FR17]
• [FB10]
• [CGR18]
• [RF15]
• [Gun01]
• [MS15a]

Sentence forms and their semantics

inductive FarkasRoelofsen2017.Intonation : Type

Rising or falling intonation, the markers open and closed of (26b).

• falling : Intonation
• rising : Intonation

@[instance_reducible]

instance FarkasRoelofsen2017.instDecidableEqIntonation : DecidableEq Intonation

Equations

• FarkasRoelofsen2017.instDecidableEqIntonation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance FarkasRoelofsen2017.instReprIntonation : Repr Intonation

Equations

• FarkasRoelofsen2017.instReprIntonation = { reprPrec := FarkasRoelofsen2017.instReprIntonation.repr }

def FarkasRoelofsen2017.instReprIntonation.repr : Intonation → ℕ → Std.Format

Equations

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

inductive FarkasRoelofsen2017.Form : Type

The six sentence forms of (3)–(8) are a declarative or interrogative clause with its intonation, or a falling declarative anchor with a reverse-polarity tag carrying the intonation.

• declarative (i : Intonation) : Form
• interrogative (i : Intonation) : Form
• tag (i : Intonation) : Form

def FarkasRoelofsen2017.instDecidableEqForm.decEq (x✝ x✝¹ : Form) : Decidable (x✝ = x✝¹)

Equations

• FarkasRoelofsen2017.instDecidableEqForm.decEq (FarkasRoelofsen2017.Form.declarative a) (FarkasRoelofsen2017.Form.declarative b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• FarkasRoelofsen2017.instDecidableEqForm.decEq (FarkasRoelofsen2017.Form.declarative i) (FarkasRoelofsen2017.Form.interrogative i_1) = isFalse ⋯
• FarkasRoelofsen2017.instDecidableEqForm.decEq (FarkasRoelofsen2017.Form.declarative i) (FarkasRoelofsen2017.Form.tag i_1) = isFalse ⋯
• FarkasRoelofsen2017.instDecidableEqForm.decEq (FarkasRoelofsen2017.Form.interrogative i) (FarkasRoelofsen2017.Form.declarative i_1) = isFalse ⋯
• FarkasRoelofsen2017.instDecidableEqForm.decEq (FarkasRoelofsen2017.Form.interrogative a) (FarkasRoelofsen2017.Form.interrogative b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• FarkasRoelofsen2017.instDecidableEqForm.decEq (FarkasRoelofsen2017.Form.interrogative i) (FarkasRoelofsen2017.Form.tag i_1) = isFalse ⋯
• FarkasRoelofsen2017.instDecidableEqForm.decEq (FarkasRoelofsen2017.Form.tag i) (FarkasRoelofsen2017.Form.declarative i_1) = isFalse ⋯
• FarkasRoelofsen2017.instDecidableEqForm.decEq (FarkasRoelofsen2017.Form.tag i) (FarkasRoelofsen2017.Form.interrogative i_1) = isFalse ⋯
• FarkasRoelofsen2017.instDecidableEqForm.decEq (FarkasRoelofsen2017.Form.tag a) (FarkasRoelofsen2017.Form.tag b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance FarkasRoelofsen2017.instDecidableEqForm : DecidableEq Form

Equations

• FarkasRoelofsen2017.instDecidableEqForm = FarkasRoelofsen2017.instDecidableEqForm.decEq

@[instance_reducible]

instance FarkasRoelofsen2017.instReprForm : Repr Form

Equations

• FarkasRoelofsen2017.instReprForm = { reprPrec := FarkasRoelofsen2017.instReprForm.repr }

def FarkasRoelofsen2017.instReprForm.repr : Form → ℕ → Std.Format

Equations

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

def FarkasRoelofsen2017.Intonation.interpret {W : Type u_1} : Intonation → Question W → Question W

closed intonation is vacuous and open intonation is the non-informative projection (36).

Equations

• FarkasRoelofsen2017.Intonation.falling.interpret = id
• FarkasRoelofsen2017.Intonation.rising.interpret = Question.query

noncomputable def FarkasRoelofsen2017.Form.interpret {W : Type u_1} : Form → Question W → Question W

dec is !, int is ⟨?⟩, which applies ? only to a non-inquisitive argument, and a tag applies int to the falling declarative anchor, as in (37)–(40).

Equations

• (FarkasRoelofsen2017.Form.declarative i).interpret x✝ = i.interpret x✝ᶜᶜ
• (FarkasRoelofsen2017.Form.interrogative i).interpret x✝ = i.interpret (if x✝.IsInquisitive then x✝ else x✝.query)
• (FarkasRoelofsen2017.Form.tag i).interpret x✝ = i.interpret (if x✝ᶜᶜ.IsInquisitive then x✝ᶜᶜ else x✝ᶜᶜ.query)

def FarkasRoelofsen2017.Form.IsMarked : Form → Prop

Polar interrogatives are the optimal forms for an inquisitive content, and rising declaratives and tag interrogatives are marked (47).

Equations

• (FarkasRoelofsen2017.Form.declarative FarkasRoelofsen2017.Intonation.rising).IsMarked = True
• (FarkasRoelofsen2017.Form.tag i).IsMarked = True
• x✝.IsMarked = False

@[instance_reducible]

instance FarkasRoelofsen2017.Form.instDecidablePredIsMarked : DecidablePred IsMarked

Equations

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

theorem FarkasRoelofsen2017.interpret_declarative_falling {W : Type u_1} (P : Question W) : (Form.declarative Intonation.falling).interpret P = Pᶜᶜ

A falling declarative expresses the non-inquisitive projection of its radical (41a).

theorem FarkasRoelofsen2017.interpret_marked {W : Type u_1} (P : Question W) (i : Intonation) : (Form.declarative Intonation.rising).interpret P = Pᶜᶜ.query ∧ (Form.tag i).interpret P = Pᶜᶜ.query

A rising declarative and a tag interrogative express ?!P, as in (39) and (40).

theorem FarkasRoelofsen2017.interpret_interrogative_ofSet {W : Type u_1} (α : Set W) (i : Intonation) : (Form.interrogative i).interpret (Question.ofSet α) = (Question.ofSet α).query

A polar interrogative with a non-inquisitive radical expresses ?P, whatever its intonation (38).

theorem FarkasRoelofsen2017.interpret_eq_query_ofSet {W : Type u_1} (α : Set W) (f : Form) (h : f ≠ Form.declarative Intonation.falling) : f.interpret (Question.ofSet α) = (Question.ofSet α).query

Every form but the falling declarative expresses the same inquisitive proposition {α, ᾱ} for a radical α (43).

theorem FarkasRoelofsen2017.isInquisitive_interpret_ofSet {W : Type u_1} {α : Set W} (h₁ : α ≠ Set.univ) (h₂ : α ≠ ∅) (f : Form) (h : f ≠ Form.declarative Intonation.falling) : (f.interpret (Question.ofSet α)).IsInquisitive

Those forms raise a genuine issue unless the radical is a tautology or a contradiction (41b).

Credence and discourse contexts

inductive FarkasRoelofsen2017.CredenceLevel : Type

§3.2 distinguishes four credence levels, from zero, when the highlighted alternative is not considered more likely than its complement, to high, when it is much more likely.

• zero : CredenceLevel
• low : CredenceLevel
• moderate : CredenceLevel
• high : CredenceLevel

@[instance_reducible]

instance FarkasRoelofsen2017.instDecidableEqCredenceLevel : DecidableEq CredenceLevel

Equations

• FarkasRoelofsen2017.instDecidableEqCredenceLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def FarkasRoelofsen2017.instReprCredenceLevel.repr : CredenceLevel → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance FarkasRoelofsen2017.instReprCredenceLevel : Repr CredenceLevel

Equations

• FarkasRoelofsen2017.instReprCredenceLevel = { reprPrec := FarkasRoelofsen2017.instReprCredenceLevel.repr }

@[instance_reducible]

instance FarkasRoelofsen2017.instFintypeCredenceLevel : Fintype CredenceLevel

Equations

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

def FarkasRoelofsen2017.CredenceLevel.toNat : CredenceLevel → ℕ

Equations

• FarkasRoelofsen2017.CredenceLevel.zero.toNat = 0
• FarkasRoelofsen2017.CredenceLevel.low.toNat = 1
• FarkasRoelofsen2017.CredenceLevel.moderate.toNat = 2
• FarkasRoelofsen2017.CredenceLevel.high.toNat = 3

@[instance_reducible]

instance FarkasRoelofsen2017.CredenceLevel.instLinearOrder : LinearOrder CredenceLevel

Equations

• FarkasRoelofsen2017.CredenceLevel.instLinearOrder = LinearOrder.lift' FarkasRoelofsen2017.CredenceLevel.toNat FarkasRoelofsen2017.CredenceLevel.instLinearOrder._proof_1

structure FarkasRoelofsen2017.Context (A : Type u_2) (W : Type u_3) : Type (max u_2 u_3)

A discourse context (22), enriched in §3.2, records the propositions proposed so far, the participants' commitments, and for each participant the possibilities they have signalled evidence for, each with a credence interval.

• table : List (Question W)
• commitments : Commitment.State A W
• evidence : A → Set (Set W × Set CredenceLevel)

def FarkasRoelofsen2017.Context.cs {W : Type u_1} {A : Type u_2} (K : Context A W) (x : A) : Set W

cs(x) is the set of worlds compatible with everything x is committed to.

Equations

• K.cs x = Commitment.contextSet (Commitment.ofCommitter K.commitments x)

def FarkasRoelofsen2017.Context.cg {W : Type u_1} {A : Type u_2} (K : Context A W) : Set W

The common ground, the smallest set every participant is committed to the actual world lying in.

Equations

• K.cg = ⋃ (x : A), K.cs x

def FarkasRoelofsen2017.Context.CommonlyDecided {W : Type u_1} {A : Type u_2} (K : Context A W) (P : Question W) : Prop

The participants have commonly decided on P when the common ground complies with it or cannot comply with it.

Equations

• K.CommonlyDecided P = (K.cg ∈ P ∨ ∀ s ∈ P, K.cg ∩ s = ∅)

def FarkasRoelofsen2017.Context.basic {W : Type u_1} {A : Type u_2} (K : Context A W) (x : A) (φ : Question W) : Context A W

The basic convention of use (48) puts the proposition on the table and its informative content into the speaker's commitments.

Equations

• K.basic x φ = { table := φ :: K.table, commitments := insert (Commitment.commit x φ.info) K.commitments, evidence := K.evidence }

def FarkasRoelofsen2017.Context.special {W : Type u_1} {A : Type u_2} (K : Context A W) (x : A) [DecidableEq A] (α : Set W) (I : Set CredenceLevel) : Context A W

A special effect enters the highlighted alternative into the speaker's evidence with a credence interval.

Equations

• K.special x α I = { table := K.table, commitments := K.commitments, evidence := Function.update K.evidence x (insert (α, I) (K.evidence x)) }

def FarkasRoelofsen2017.Form.specialEffect : Form → Option (CredenceLevel × CredenceLevel)

A marked form signals a credence interval for the highlighted alternative, as in (52), (56) and (58).

Equations

• (FarkasRoelofsen2017.Form.declarative FarkasRoelofsen2017.Intonation.rising).specialEffect = some (FarkasRoelofsen2017.CredenceLevel.zero, FarkasRoelofsen2017.CredenceLevel.low)
• (FarkasRoelofsen2017.Form.tag FarkasRoelofsen2017.Intonation.rising).specialEffect = some (FarkasRoelofsen2017.CredenceLevel.moderate, FarkasRoelofsen2017.CredenceLevel.high)
• (FarkasRoelofsen2017.Form.tag FarkasRoelofsen2017.Intonation.falling).specialEffect = some (FarkasRoelofsen2017.CredenceLevel.high, FarkasRoelofsen2017.CredenceLevel.high)
• x✝.specialEffect = none

noncomputable def FarkasRoelofsen2017.Context.utter {W : Type u_1} {A : Type u_2} [DecidableEq A] (K : Context A W) (x : A) (f : Form) (α : Set W) : Context A W

The conventional discourse effect of x uttering the form f with radical α is the basic convention on the proposition the form expresses, followed by the form's special effect if it has one.

Equations

• K.utter x f α = match f.specialEffect with | none => K.basic x (f.interpret (Question.ofSet α)) | some I => (K.basic x (f.interpret (Question.ofSet α))).special x α (Set.Icc I.1 I.2)

theorem FarkasRoelofsen2017.Context.utter_eq_basic_of_not_isMarked {W : Type u_1} {A : Type u_2} [DecidableEq A] (K : Context A W) (x : A) {f : Form} (h : ¬f.IsMarked) (α : Set W) : K.utter x f α = K.basic x (f.interpret (Question.ofSet α))

By the division of labor principle (21a), an unmarked form's discourse effects are the basic convention of use alone.

theorem FarkasRoelofsen2017.Context.table_utter {W : Type u_1} {A : Type u_2} [DecidableEq A] (K : Context A W) (x : A) (f : Form) (α : Set W) : (K.utter x f α).table = f.interpret (Question.ofSet α) :: K.table

A marked form's effects include the basic convention (21b).

theorem FarkasRoelofsen2017.Context.commitments_utter {W : Type u_1} {A : Type u_2} [DecidableEq A] (K : Context A W) (x : A) (f : Form) (α : Set W) : (K.utter x f α).commitments = insert (Commitment.commit x (f.interpret (Question.ofSet α)).info) K.commitments

theorem FarkasRoelofsen2017.Context.cs_basic_declarative_falling {W : Type u_1} {A : Type u_2} (K : Context A W) (x : A) (α : Set W) : (K.basic x ((Form.declarative Intonation.falling).interpret (Question.ofSet α))).cs x = K.cs x ∩ α

A falling declarative commits the speaker to the radical (49).

theorem FarkasRoelofsen2017.Context.cs_basic_of_isInquisitive {W : Type u_1} {A : Type u_2} (K : Context A W) (x : A) {φ : Question W} (h : φ.info = Set.univ) : (K.basic x φ).cs x = K.cs x

An inquisitive proposition commits the speaker only to the trivial possibility, as in (50) and (51).

theorem FarkasRoelofsen2017.Context.mem_evidence_utter {W : Type u_1} {A : Type u_2} [DecidableEq A] (K : Context A W) (x : A) {f : Form} {I : CredenceLevel × CredenceLevel} (h : f.specialEffect = some I) (α : Set W) : (α, Set.Icc I.1 I.2) ∈ (K.utter x f α).evidence x

A marked form registers the highlighted alternative as evidenced with its credence interval, as in (52), (56) and (58).

theorem FarkasRoelofsen2017.Context.evidence_utter_of_not_isMarked {W : Type u_1} {A : Type u_2} [DecidableEq A] (K : Context A W) (x : A) {f : Form} (h : ¬f.IsMarked) (α : Set W) : (K.utter x f α).evidence = K.evidence

An unmarked form registers no evidence.

Testing the account (§6)

structure FarkasRoelofsen2017.Situation : Type

A situation of §6 fixes whether the speaker has evidence for the highlighted alternative, whether the addressee is neutral, and the range of credence the context makes reasonable.

• evidence : Bool
• addresseeNeutral : Bool
• lo : CredenceLevel
• hi : CredenceLevel

def FarkasRoelofsen2017.instDecidableEqSituation.decEq (x✝ x✝¹ : Situation) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance FarkasRoelofsen2017.instDecidableEqSituation : DecidableEq Situation

Equations

• FarkasRoelofsen2017.instDecidableEqSituation = FarkasRoelofsen2017.instDecidableEqSituation.decEq

@[instance_reducible]

instance FarkasRoelofsen2017.instReprSituation : Repr Situation

Equations

• FarkasRoelofsen2017.instReprSituation = { reprPrec := FarkasRoelofsen2017.instReprSituation.repr }

def FarkasRoelofsen2017.instReprSituation.repr : Situation → ℕ → Std.Format

Equations

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

def FarkasRoelofsen2017.Felicitous (f : Form) (s : Situation) : Prop

A form is felicitous in a situation by the reasoning of §6: a commitment to the radical needs high credence to be possible; an issue on the table needs an addressee who is not neutral; the unmarked inquisitive form presents the speaker as neutral, which needs low credence to be possible; a marked form needs evidence and a credence the context allows within its interval.

Equations

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

@[instance_reducible]

instance FarkasRoelofsen2017.instDecidableFelicitous (f : Form) (s : Situation) : Decidable (Felicitous f s)

Equations

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

structure FarkasRoelofsen2017.Row : Type

A judgment of §6 records the form, the situation, and the paper's verdict.

• form : Form
• situation : Situation
• judgment : Judgment

def FarkasRoelofsen2017.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance FarkasRoelofsen2017.instDecidableEqRow : DecidableEq Row

Equations

• FarkasRoelofsen2017.instDecidableEqRow = FarkasRoelofsen2017.instDecidableEqRow.decEq

@[instance_reducible]

instance FarkasRoelofsen2017.instReprRow : Repr Row

Equations

• FarkasRoelofsen2017.instReprRow = { reprPrec := FarkasRoelofsen2017.instReprRow.repr }

def FarkasRoelofsen2017.instReprRow.repr : Row → ℕ → Std.Format

Equations

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

def FarkasRoelofsen2017.formTable : List (String × Form)

Equations

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

def FarkasRoelofsen2017.boolTable : List (String × Bool)

Equations

• FarkasRoelofsen2017.boolTable = [("yes", true), ("no", false)]

def FarkasRoelofsen2017.addresseeTable : List (String × Bool)

Equations

• FarkasRoelofsen2017.addresseeTable = [("neutral", true), ("informed", false)]

def FarkasRoelofsen2017.credenceTable : List (String × CredenceLevel)

Equations

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

def FarkasRoelofsen2017.Row.ofDatum (ex : Datum) : Option Row

Equations

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

theorem FarkasRoelofsen2017.row_ofDatum_isSome (ex : Datum) : ex ∈ Examples.all → (Row.ofDatum ex).isSome = true

def FarkasRoelofsen2017.rows : List Row

Equations

• FarkasRoelofsen2017.rows = List.filterMap FarkasRoelofsen2017.Row.ofDatum FarkasRoelofsen2017.Examples.all

theorem FarkasRoelofsen2017.rows_felicitous (r : Row) : r ∈ rows → (r.judgment = Judgment.acceptable ↔ Felicitous r.form r.situation)

The account reproduces every judgment of §6.