Büring and Gunlogson 2000: aren't positive and negative polar questions the same?

This file formalizes the felicity conditions of [BG00]. Standard question semantics gives Is she left-handed?, Isn't she left-handed? and Is she right-handed? one and the same denotation, yet the three types are felicitous in different contexts: a positive question is barred by compelling contextual evidence against its proposition, an inner-negation question requires such evidence, and an outer-negation question is barred by evidence for it. The paper's appendix derives all three from one proto-condition applied to the question's proposition, to its negation, or negated in turn, and the morphosyntactic probes of [Lad81] — kein vs nicht ein, no vs not some, and the polarity items they admit — classify a question independently of those judgements.

The three question types are readings, Option Polarity: none is the paper's PPQ, and a negative question is an inner-negation NPQ, some .negative, when the negation sits inside the questioned proposition, and an outer-negation NPQ, some .positive, when it sits outside. The contextual evidence of a situation is the sign of p it supports, and reading it relative to ¬p negates it.

Main definitions

• E, Felicitous — the proto-condition and the felicity condition of each question type
• Determiner, Question — the morphosyntactic probes and a probed question; the polarity items are the fragments' either, too and brauchen

Main results

• felicitous_none_iff, felicitous_some_positive_iff, felicitous_some_negative_iff — the three evidence conditions
• felicity_separates_readings — no two question types share a felicity profile
• outer_is_interrogative_only — only inner-negation determiners occur in declaratives
• polarity_eq_negative_of_isNPI, polarity_eq_positive_of_isPPI — a polarity item forces the reading the determiner gives

References

• [BG00]
• [Lad81]
• [Ham73]

Compelling contextual evidence

def BuringGunlogson2000.CompellingFor (ev : SignType) : Prop

Evidence is compelling for p when it would on its own justify the inference that p.

Equations

• BuringGunlogson2000.CompellingFor ev = (ev = 1)

def BuringGunlogson2000.CompellingAgainst (ev : SignType) : Prop

Evidence is compelling against p when it is compelling for ¬p, the evidence read relative to ¬p.

Equations

• BuringGunlogson2000.CompellingAgainst ev = BuringGunlogson2000.CompellingFor (-ev)

@[instance_reducible]

instance BuringGunlogson2000.instDecidableCompellingFor (ev : SignType) : Decidable (CompellingFor ev)

Equations

• BuringGunlogson2000.instDecidableCompellingFor ev = BuringGunlogson2000.instDecidableCompellingFor._aux_1 ev

@[instance_reducible]

instance BuringGunlogson2000.instDecidableCompellingAgainst (ev : SignType) : Decidable (CompellingAgainst ev)

Equations

• BuringGunlogson2000.instDecidableCompellingAgainst ev = BuringGunlogson2000.instDecidableCompellingAgainst._aux_1 ev

The evidence conditions

def BuringGunlogson2000.E (ev : SignType) : Prop

The proto-condition: there is no compelling contextual evidence against p.

Equations

• BuringGunlogson2000.E ev = ¬BuringGunlogson2000.CompellingAgainst ev

@[instance_reducible]

instance BuringGunlogson2000.instDecidableE (ev : SignType) : Decidable (E ev)

Equations

• BuringGunlogson2000.instDecidableE ev = { decide := !decide (BuringGunlogson2000.CompellingAgainst ev), reflects_decide := ⋯ }

def BuringGunlogson2000.Felicitous : Option Polarity → SignType → Prop

The felicity condition of each question type, as one proto-condition applied three ways: a positive question imposes it on its own proposition, an outer-negation question on the negation, and an inner-negation question imposes its negation.

Equations

• BuringGunlogson2000.Felicitous none x✝ = BuringGunlogson2000.E x✝
• BuringGunlogson2000.Felicitous (some Polarity.negative) x✝ = ¬BuringGunlogson2000.E x✝
• BuringGunlogson2000.Felicitous (some Polarity.positive) x✝ = BuringGunlogson2000.E (-x✝)

@[instance_reducible]

instance BuringGunlogson2000.instDecidableFelicitous (r : Option Polarity) (ev : SignType) : Decidable (Felicitous r ev)

Equations

• BuringGunlogson2000.instDecidableFelicitous none x✝ = { decide := !decide (BuringGunlogson2000.CompellingAgainst x✝), reflects_decide := ⋯ }
• BuringGunlogson2000.instDecidableFelicitous (some Polarity.negative) x✝ = { decide := !decide (BuringGunlogson2000.E x✝), reflects_decide := ⋯ }
• BuringGunlogson2000.instDecidableFelicitous (some Polarity.positive) x✝ = { decide := !decide (BuringGunlogson2000.CompellingAgainst (-x✝)), reflects_decide := ⋯ }

theorem BuringGunlogson2000.felicitous_none_iff (ev : SignType) : Felicitous none ev ↔ ¬CompellingAgainst ev

A positive question requires no compelling evidence against p.

theorem BuringGunlogson2000.felicitous_some_positive_iff (ev : SignType) : Felicitous (some Polarity.positive) ev ↔ ¬CompellingFor ev

An outer-negation question requires no compelling evidence for p.

theorem BuringGunlogson2000.felicitous_some_negative_iff (ev : SignType) : Felicitous (some Polarity.negative) ev ↔ CompellingAgainst ev

An inner-negation question requires compelling evidence against p.

theorem BuringGunlogson2000.not_felicitous_none_neg_one : ¬Felicitous none (-1)

A positive question is barred by compelling evidence against p — Is it sunny? asked of someone in a dripping raincoat.

theorem BuringGunlogson2000.felicitous_some_negative_iff_eq (ev : SignType) : Felicitous (some Polarity.negative) ev ↔ ev = -1

An inner-negation question is felicitous only against p, the neutral context included in the exclusion.

theorem BuringGunlogson2000.felicitous_some_positive_zero_not_negative : Felicitous (some Polarity.positive) 0 ∧ ¬Felicitous (some Polarity.negative) 0

An outer-negation question tolerates a neutral context, unlike an inner-negation one.

theorem BuringGunlogson2000.felicity_separates_readings (r s : Option Polarity) (h : ∀ (ev : SignType), Felicitous r ev ↔ Felicitous s ev) : r = s

No two question types share a felicity profile, so the predicted synonymies of a Hamblin denotation ([Ham73]) are not real.

The morphosyntactic probes

inductive BuringGunlogson2000.Determiner : Type

The negative determiners that probe the distinction are German kein and nicht ein and English no and not some.

• kein : Determiner
• nichtEin : Determiner
• no : Determiner
• notSome : Determiner

@[instance_reducible]

instance BuringGunlogson2000.instDecidableEqDeterminer : DecidableEq Determiner

Equations

• BuringGunlogson2000.instDecidableEqDeterminer x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def BuringGunlogson2000.Determiner.polarity : Determiner → Polarity

The polarity of the proposition a question with the determiner double-checks: nicht ein and not some leave the negation outside it, so it is positive; kein and no place it inside.

Equations

• BuringGunlogson2000.Determiner.kein.polarity = Polarity.negative
• BuringGunlogson2000.Determiner.no.polarity = Polarity.negative
• BuringGunlogson2000.Determiner.nichtEin.polarity = Polarity.positive
• BuringGunlogson2000.Determiner.notSome.polarity = Polarity.positive

def BuringGunlogson2000.Determiner.declarativeOK : Determiner → Prop

Whether the determiner also occurs in a declarative. The non-amalgamated forms do not, even under rising intonation.

Equations

• BuringGunlogson2000.Determiner.kein.declarativeOK = True
• BuringGunlogson2000.Determiner.no.declarativeOK = True
• BuringGunlogson2000.Determiner.nichtEin.declarativeOK = False
• BuringGunlogson2000.Determiner.notSome.declarativeOK = False

@[instance_reducible]

instance BuringGunlogson2000.instDecidableDeclarativeOK (d : Determiner) : Decidable d.declarativeOK

Equations

• BuringGunlogson2000.instDecidableDeclarativeOK BuringGunlogson2000.Determiner.kein = { decide := true, reflects_decide := BuringGunlogson2000.instDecidableDeclarativeOK._proof_1 }
• BuringGunlogson2000.instDecidableDeclarativeOK BuringGunlogson2000.Determiner.no = { decide := true, reflects_decide := BuringGunlogson2000.instDecidableDeclarativeOK._proof_2 }
• BuringGunlogson2000.instDecidableDeclarativeOK BuringGunlogson2000.Determiner.nichtEin = { decide := false, reflects_decide := BuringGunlogson2000.instDecidableDeclarativeOK._proof_3 }
• BuringGunlogson2000.instDecidableDeclarativeOK BuringGunlogson2000.Determiner.notSome = { decide := false, reflects_decide := BuringGunlogson2000.instDecidableDeclarativeOK._proof_4 }

theorem BuringGunlogson2000.outer_is_interrogative_only (d : Determiner) : d.polarity = Polarity.positive ↔ ¬d.declarativeOK

An outer-negation construal is confined to the syntactic category of interrogative: exactly the determiners that fail in declaratives are the outer-negation ones.

structure BuringGunlogson2000.Question : Type

A polar question as its two probes: a negative determiner and, optionally, a polarity item, English either or too or German brauchen.

• determiner : Determiner
• item : Option PolarityItem

def BuringGunlogson2000.Question.WellFormed (q : Question) : Prop

The probes agree on where the negation sits: a negative polarity item must sit under it, so it requires the inner construal, and a positive polarity item must escape it, so it requires the outer one.

Equations

• q.WellFormed = ∀ e ∈ q.item, (e.IsNPI → q.determiner.polarity = Polarity.negative) ∧ (e.IsPPI → q.determiner.polarity = Polarity.positive)

@[instance_reducible]

instance BuringGunlogson2000.instDecidableWellFormed (q : Question) : Decidable q.WellFormed

Equations

• BuringGunlogson2000.instDecidableWellFormed { determiner := determiner, item := none } = isTrue ⋯
• BuringGunlogson2000.instDecidableWellFormed { determiner := d, item := some e } = decidable_of_iff ((e.IsNPI → d.polarity = Polarity.negative) ∧ (e.IsPPI → d.polarity = Polarity.positive)) ⋯

theorem BuringGunlogson2000.no_takes_either_not_too : { determiner := Determiner.no, item := some English.PolarityItems.either }.WellFormed ∧ ¬{ determiner := Determiner.no, item := some English.PolarityItems.too }.WellFormed

Is there no vegetarian restaurant either/*too? (14a): the inner-negation determiner takes the negative polarity item and refuses the positive one.

theorem BuringGunlogson2000.notSome_takes_too_not_either : { determiner := Determiner.notSome, item := some English.PolarityItems.too }.WellFormed ∧ ¬{ determiner := Determiner.notSome, item := some English.PolarityItems.either }.WellFormed

Isn't there some vegetarian restaurant *either/too? (14b): the outer-negation determiner takes the positive polarity item and refuses the negative one.

theorem BuringGunlogson2000.brauchen_takes_kein_not_nichtEin : { determiner := Determiner.kein, item := some German.PolarityItems.brauchen }.WellFormed ∧ ¬{ determiner := Determiner.nichtEin, item := some German.PolarityItems.brauchen }.WellFormed

Brauchst du keine/*nicht eine Entschuldigung mitzubringen? (16): the German NPI likewise goes with the amalgamated determiner only.

theorem BuringGunlogson2000.polarity_eq_negative_of_isNPI {d : Determiner} {e : PolarityItem} (he : e.IsNPI) (h : { determiner := d, item := some e }.WellFormed) : d.polarity = Polarity.negative

A negative polarity item forces the inner-negation reading (13a).

theorem BuringGunlogson2000.polarity_eq_positive_of_isPPI {d : Determiner} {e : PolarityItem} (he : e.IsPPI) (h : { determiner := d, item := some e }.WellFormed) : d.polarity = Polarity.positive

A positive polarity item forces the outer-negation reading (13b).