Seeliger & Repp (2018): Biased declarative questions in Swedish and German

[SR18] distinguish two kinds of question with declarative syntax. A declarative question such as Peter is coming? requires contextual evidence for the proposition the declarative denotes and a speaker who had not assumed it; a rejecting question such as Surely Peter is coming?, German Peter kommt doch wohl?, Swedish Men Peter kommer väl?, requires evidence against it and a speaker who had assumed it. The profiles are stated in the two-dimensional bias scheme of [Sud13], evidential and epistemic, which the paper extends with 'minus' values for epistemic bias (Section 2): the substrate's Question.BiasValue, a set of states of evidence or belief, [+s] being plus s and [−s] its complement minus s.

Table 1's four types follow from the polarity of the declarative (table1): a declarative question of polarity s has evidential bias [+s] and epistemic bias [−s] (dqProfile), and the preliminary REJECTQ operator (17), λq: [¬q]^evid & [q]^epist. {q, ¬q}, gives a rejecting question [+(¬s)] and [+s] (rejectQ). A rejecting question is therefore used in a proper subset of the situations of the declarative question of the opposite polarity, the observation of p. 138 (felicity_rejectQ_ssubset). The revised operator (40), with the illocutionary modifier VERUM or FALSUM, derives the positive rejecting question (rejectQWith_verum) but not the negative one: FALSUM requires only that the evidence not support ¬p and that the speaker not have been committed to p, which admits neutral evidence and no prior assumption, situations Table 1 excludes (felicity_rejectQ_ssubset_rejectQWith_falsum).

Swedish marks a rejecting question with at least one morpho-syntactic cue (p. 157): a negative one with fronted negation or väl, a positive one with men 'but' and väl, or with clause-initial visst or nog when the evidence is direct. SwedishCues.MarksRQ states the generalization and marking_iff checks it against the examples of Sections 3 and 5.3.

Implementation notes

• The question REJECTQ forms from a declarative of polarity s with prejacent p is the polar question on s • p, which is the polar question on p (Question.polar_smul). The commitment-modified propositions IM(q) of (40) are not modelled, only the presuppositions.
• The declarative polarity is Table 1's simplified 'Declarative denotes' column: the paper argues in Section 6.1 that the negation of a negative rejecting question is FALSUM, not propositional negation.

TODO

• The acceptability experiment of Section 5.4 (Table 2), the German rejections of Section 4.2 that show doch wohl to be non-compositional, and the polarity-item diagnostics of Section 6.1 are not yet encoded.
• The comparison with the monopolar declarative questions of [Kri15a] (footnote 17), which predict the rows of declarative but not of rejecting questions.

References

• [SR18]
• [Sud13]
• [Kri15a]

Declarative and rejecting questions (Sections 2, 3 and 4.3)

def SeeligerRepp2018.dqProfile (s : Polarity) : Question.BiasProfile

A declarative question of polarity s: evidence for the proposition the declarative denotes, and a speaker who had not assumed it (Section 2).

Equations

• SeeligerRepp2018.dqProfile s = { evidential := Question.BiasValue.plus s, epistemic := Question.BiasValue.minus s }

def SeeligerRepp2018.rejectQ (s : Polarity) : Question.BiasProfile

The preliminary REJECTQ (17), λq: [¬q]^evid & [q]^epist. {q, ¬q}, on the proposition of a declarative of polarity s: evidence for the opposite proposition, and a speaker who had assumed it.

Equations

• SeeligerRepp2018.rejectQ s = { evidential := Question.BiasValue.plus (Polarity.negative * s), epistemic := Question.BiasValue.plus s }

theorem SeeligerRepp2018.felicity_rejectQ_ssubset (s : Polarity) : (rejectQ s).felicity ⊂ (dqProfile (Polarity.negative * s)).felicity

A rejecting question is used in a proper subset of the situations of the declarative question of the opposite polarity (p. 138): the negative one within the positive declarative question's, the positive one within the negative declarative question's.

The illocutionary modifiers (Section 6.2)

inductive SeeligerRepp2018.Modifier : Type

The illocutionary modifiers of (40): VERUM, a high degree of commitment, and FALSUM, a zero degree.

• verum : Modifier
• falsum : Modifier

@[instance_reducible]

instance SeeligerRepp2018.instDecidableEqModifier : DecidableEq Modifier

Equations

• SeeligerRepp2018.instDecidableEqModifier x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def SeeligerRepp2018.instReprModifier.repr : Modifier → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance SeeligerRepp2018.instReprModifier : Repr Modifier

Equations

• SeeligerRepp2018.instReprModifier = { reprPrec := SeeligerRepp2018.instReprModifier.repr }

def SeeligerRepp2018.Modifier.bias : Modifier → Polarity → Question.BiasValue

The contexts in which a basis gives the modifier's degree of commitment to the s proposition: VERUM needs the basis to support it, FALSUM that it not support it.

Equations

• SeeligerRepp2018.Modifier.verum.bias x✝ = Question.BiasValue.plus x✝
• SeeligerRepp2018.Modifier.falsum.bias x✝ = Question.BiasValue.minus x✝

def SeeligerRepp2018.rejectQWith (m : Modifier) : Question.BiasProfile

The revised REJECTQ (40), λqλIM: [IM(¬q)]^evid & [IM(q)]^epist. {IM(q), ¬IM(q)}, with q the non-negative proposition, as in (41): the positive rejecting question has VERUM, the negative one FALSUM.

Equations

• SeeligerRepp2018.rejectQWith m = { evidential := m.bias Polarity.negative, epistemic := m.bias Polarity.positive }

theorem SeeligerRepp2018.rejectQWith_verum : rejectQWith Modifier.verum = rejectQ Polarity.positive

With VERUM, (40) agrees with (17) on the positive rejecting question.

theorem SeeligerRepp2018.felicity_rejectQ_ssubset_rejectQWith_falsum : (rejectQ Polarity.negative).felicity ⊂ (rejectQWith Modifier.falsum).felicity ∧ (0, 0) ∈ (rejectQWith Modifier.falsum).felicity

With FALSUM, (40) is strictly weaker than (17) and Table 1 on the negative rejecting question: it admits neutral evidence without a prior assumption.

Table 1

inductive SeeligerRepp2018.Kind : Type

The two kinds of question with declarative syntax.

• declarative : Kind
• rejecting : Kind

@[instance_reducible]

instance SeeligerRepp2018.instDecidableEqKind : DecidableEq Kind

Equations

• SeeligerRepp2018.instDecidableEqKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def SeeligerRepp2018.instReprKind.repr : Kind → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance SeeligerRepp2018.instReprKind : Repr Kind

Equations

• SeeligerRepp2018.instReprKind = { reprPrec := SeeligerRepp2018.instReprKind.repr }

def SeeligerRepp2018.Kind.profile : Kind → Polarity → Question.BiasProfile

The profile of a question of the given kind and polarity.

Equations

• SeeligerRepp2018.Kind.declarative.profile = SeeligerRepp2018.dqProfile
• SeeligerRepp2018.Kind.rejecting.profile = SeeligerRepp2018.rejectQ

def SeeligerRepp2018.typeTable : List (String × Kind × Polarity)

The four types of Table 1, with their kind and the polarity of the declarative.

Equations

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

def SeeligerRepp2018.biasTable : List (String × Question.BiasValue)

The bias values of the annotation.

Equations

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

structure SeeligerRepp2018.Row : Type

An example of Table 1: the kind and polarity of the question, and the profile the example records.

• kind : Kind

  Declarative or rejecting.

• polarity : Polarity

  The polarity of the declarative.

• profile : Question.BiasProfile

  The recorded bias profile.

@[instance_reducible]

instance SeeligerRepp2018.instDecidableEqRow : DecidableEq Row

Equations

• SeeligerRepp2018.instDecidableEqRow = SeeligerRepp2018.instDecidableEqRow.decEq

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

Equations

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

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

The row of an example annotated with a type and a bias profile.

Equations

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

def SeeligerRepp2018.rows : List Row

The examples (5) to (8) of Table 1.

Equations

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

theorem SeeligerRepp2018.rows_length : rows.length = 13

The rows cover the four types in English, German and Swedish, with (8c′).

theorem SeeligerRepp2018.table1 (r : Row) : r ∈ rows → r.profile = r.kind.profile r.polarity

Table 1: every example has the profile of its kind and polarity.

Marking rejecting questions in Swedish (Sections 3, 5.3 and 6)

structure SeeligerRepp2018.SwedishCues : Type

The morpho-syntactic cues of a Swedish declarative that bear on a rejecting reading, and whether the contextual evidence is direct. Väl is Swedish.Particles.val.

• fronted : Bool

  The negation is fronted.

• val : Bool

  Clause-medial väl.

• men : Bool

  Clause-initial men 'but'.

• initial : Bool

  Clause-initial visst or nog.

• direct : Bool

  The contextual evidence is direct.

@[instance_reducible]

instance SeeligerRepp2018.instDecidableEqSwedishCues : DecidableEq SwedishCues

Equations

• SeeligerRepp2018.instDecidableEqSwedishCues = SeeligerRepp2018.instDecidableEqSwedishCues.decEq

def SeeligerRepp2018.instDecidableEqSwedishCues.decEq (x✝ x✝¹ : SwedishCues) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance SeeligerRepp2018.instReprSwedishCues : Repr SwedishCues

Equations

• SeeligerRepp2018.instReprSwedishCues = { reprPrec := SeeligerRepp2018.instReprSwedishCues.repr }

def SeeligerRepp2018.instReprSwedishCues.repr : SwedishCues → ℕ → Std.Format

Equations

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

def SeeligerRepp2018.SwedishCues.MarksRQ (c : SwedishCues) : Polarity → Prop

The generalization of p. 157: a negative rejecting question needs fronted negation or väl; a positive one men with väl, or clause-initial visst or nog when the evidence is direct.

Equations

• c.MarksRQ Polarity.negative = (c.fronted = true ∨ c.val = true)
• c.MarksRQ Polarity.positive = (c.men = true ∧ c.val = true ∨ c.initial = true ∧ c.direct = true)

@[instance_reducible]

instance SeeligerRepp2018.instDecidableMarksRQ (c : SwedishCues) (s : Polarity) : Decidable (c.MarksRQ s)

Equations

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

structure SeeligerRepp2018.MarkingRow : Type

An example of a Swedish declarative in the context of a rejecting question.

• polarity : Polarity

  The polarity of the rejecting question.

• cues : SwedishCues

  The cues of the declarative.

• judgment : Judgment

  Whether the declarative can be the rejecting question.

@[instance_reducible]

instance SeeligerRepp2018.instDecidableEqMarkingRow : DecidableEq MarkingRow

Equations

• SeeligerRepp2018.instDecidableEqMarkingRow = SeeligerRepp2018.instDecidableEqMarkingRow.decEq

def SeeligerRepp2018.instDecidableEqMarkingRow.decEq (x✝ x✝¹ : MarkingRow) : Decidable (x✝ = x✝¹)

Equations

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

def SeeligerRepp2018.yesNo : List (String × Bool)

Presence of a cue in the annotation.

Equations

• SeeligerRepp2018.yesNo = [("yes", true), ("no", false)]

def SeeligerRepp2018.MarkingRow.ofDatum (ex : Datum) : Option MarkingRow

The marking row of an example annotated with its cues.

Equations

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

def SeeligerRepp2018.markingRows : List MarkingRow

The Swedish examples (7c), (8c), (8c′), (23) and (24).

Equations

• SeeligerRepp2018.markingRows = List.filterMap SeeligerRepp2018.MarkingRow.ofDatum SeeligerRepp2018.Examples.all

theorem SeeligerRepp2018.markingRows_length : markingRows.length = 11

The rows cover the three Swedish rejecting questions of (7) and (8) and the eight of (23) and (24).

theorem SeeligerRepp2018.marking_iff (r : MarkingRow) : r ∈ markingRows → (r.judgment = Judgment.acceptable ↔ r.cues.MarksRQ r.polarity)

The generalization predicts every judgment: an example is acceptable as a rejecting question just when it carries the cues.