Documentation

Linglib.Studies.BuringGunlogson2000

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 [ladd-1981] — 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 the substrate's PQForm: PosQ is the paper's PPQ, LoNQ its inner-negation NPQ, HiNQ its outer-negation NPQ.

Main definitions #

E, Felicitous — the proto-condition and the felicity condition of each question type
Determiner, PolarityItem, Question — the morphosyntactic probes and a probed question

Main results #

posQ_condition, hiNQ_condition, loNQ_condition — the three evidence conditions
felicitous_iff_evidenceBiasOK — the derived conditions are the substrate's bias table
felicity_separates_forms — no two question types share a felicity profile
outer_is_interrogative_only — only inner-negation determiners occur in declaratives
wellFormed_iff_determiner_form — the determiner and the polarity item classify a question alike

References #

[BG00]
[ladd-1981]
[hamblin-1973b]

Compelling contextual evidence #

def BuringGunlogson2000.negate :

Question.ContextualEvidence → Question.ContextualEvidence

The contextual evidence of a situation, read relative to ¬p rather than p: evidence for p is evidence against ¬p.

Equations

Instances For

@[simp]

theorem BuringGunlogson2000.negate_negate (ev : Question.ContextualEvidence) :

negate (negate ev) = ev

def BuringGunlogson2000.CompellingFor (ev : Question.ContextualEvidence) :

Compelling evidence for p: evidence that would on its own justify the inference that p.

Equations

BuringGunlogson2000.CompellingFor ev = (ev = Question.ContextualEvidence.forP)

Instances For

def BuringGunlogson2000.CompellingAgainst (ev : Question.ContextualEvidence) :

Compelling evidence against p: compelling evidence for ¬p.

Equations

BuringGunlogson2000.CompellingAgainst ev = BuringGunlogson2000.CompellingFor (BuringGunlogson2000.negate ev)

Instances For

@[instance_reducible]

instance BuringGunlogson2000.instDecidableCompellingFor (ev : Question.ContextualEvidence) :

Decidable (CompellingFor ev)

Equations

BuringGunlogson2000.instDecidableCompellingFor ev = BuringGunlogson2000.instDecidableCompellingFor._aux_1 ev

@[instance_reducible]

instance BuringGunlogson2000.instDecidableCompellingAgainst (ev : Question.ContextualEvidence) :

Decidable (CompellingAgainst ev)

Equations

BuringGunlogson2000.instDecidableCompellingAgainst ev = BuringGunlogson2000.instDecidableCompellingAgainst._aux_1 ev

The evidence conditions #

def BuringGunlogson2000.E (ev : Question.ContextualEvidence) :

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

Equations

BuringGunlogson2000.E ev = ¬BuringGunlogson2000.CompellingAgainst ev

Instances For

@[instance_reducible]

instance BuringGunlogson2000.instDecidableE (ev : Question.ContextualEvidence) :

Decidable (E ev)

Equations

BuringGunlogson2000.instDecidableE ev = BuringGunlogson2000.instDecidableE._aux_1 ev

def BuringGunlogson2000.Felicitous :

Question.PQForm → Question.ContextualEvidence → 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 Question.PQForm.PosQ x✝ = BuringGunlogson2000.E x✝
BuringGunlogson2000.Felicitous Question.PQForm.LoNQ x✝ = ¬BuringGunlogson2000.E x✝
BuringGunlogson2000.Felicitous Question.PQForm.HiNQ x✝ = BuringGunlogson2000.E (BuringGunlogson2000.negate x✝)

Instances For

@[instance_reducible]

instance BuringGunlogson2000.instDecidableFelicitous (f : Question.PQForm) (ev : Question.ContextualEvidence) :

Decidable (Felicitous f ev)

Equations

theorem BuringGunlogson2000.posQ_condition (ev : Question.ContextualEvidence) :

Felicitous Question.PQForm.PosQ ev ↔ ¬CompellingAgainst ev

A positive question requires no compelling evidence against p.

theorem BuringGunlogson2000.hiNQ_condition (ev : Question.ContextualEvidence) :

Felicitous Question.PQForm.HiNQ ev ↔ ¬CompellingFor ev

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

theorem BuringGunlogson2000.loNQ_condition (ev : Question.ContextualEvidence) :

Felicitous Question.PQForm.LoNQ ev ↔ CompellingAgainst ev

An inner-negation question requires compelling evidence against p.

theorem BuringGunlogson2000.felicitous_iff_evidenceBiasOK (f : Question.PQForm) (ev : Question.ContextualEvidence) :

Felicitous f ev ↔ Question.evidenceBiasOK f ev = true

The derived conditions are exactly the substrate's contextual-evidence bias table, so the three rows of that table follow from the single proto-condition instead of being stipulated.

theorem BuringGunlogson2000.posQ_infelicitous_against :

¬Felicitous Question.PQForm.PosQ Question.ContextualEvidence.againstP

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

theorem BuringGunlogson2000.loNQ_only_against (ev : Question.ContextualEvidence) :

Felicitous Question.PQForm.LoNQ ev ↔ ev = Question.ContextualEvidence.againstP

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

theorem BuringGunlogson2000.hiNQ_neutral_loNQ_not :

Felicitous Question.PQForm.HiNQ Question.ContextualEvidence.neutral ∧ ¬Felicitous Question.PQForm.LoNQ Question.ContextualEvidence.neutral

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

theorem BuringGunlogson2000.felicity_separates_forms (f g : Question.PQForm) (h : ∀ (ev : Question.ContextualEvidence), Felicitous f ev ↔ Felicitous g ev) :

f = g

No two question types share a felicity profile: the predicted synonymies of a Hamblin denotation ([hamblin-1973b]) are not real.

The morphosyntactic probes #

inductive BuringGunlogson2000.Scope :

Where the negation sits relative to the questioned proposition.

inner : Scope
outer : Scope

Instances For

@[instance_reducible]

instance BuringGunlogson2000.instDecidableEqScope :

DecidableEq Scope

Equations

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

inductive BuringGunlogson2000.Determiner :

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

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

Instances For

@[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.scope :

Determiner → Scope

nicht ein and not some leave the negation outside the questioned proposition; kein and no place it inside.

Equations

Instances For

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

Instances For

@[instance_reducible]

instance BuringGunlogson2000.instDecidableDeclarativeOK (d : Determiner) :

Decidable d.declarativeOK

Equations

theorem BuringGunlogson2000.outer_is_interrogative_only (d : Determiner) :

d.scope = Scope.outer ↔ ¬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.

inductive BuringGunlogson2000.Polarity :

A polarity item is negative or positive.

npi : Polarity
ppi : Polarity

Instances For

@[instance_reducible]

instance BuringGunlogson2000.instDecidableEqPolarity :

DecidableEq Polarity

Equations

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

inductive BuringGunlogson2000.PolarityItem :

The polarity items that probe the distinction: English either and too, German brauchen.

either : PolarityItem
too : PolarityItem
brauchen : PolarityItem

Instances For

@[instance_reducible]

instance BuringGunlogson2000.instDecidableEqPolarityItem :

DecidableEq PolarityItem

Equations

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

def BuringGunlogson2000.PolarityItem.polarity :

PolarityItem → Polarity

Equations

Instances For

def BuringGunlogson2000.Polarity.scope :

Polarity → Scope

A negative polarity item must sit under the negation, so it forces the inner construal; a positive polarity item must escape it, so it forces the outer one.

Equations

Instances For

structure BuringGunlogson2000.Question :

A polar question as its two probes: a negative determiner and, optionally, a polarity item.

determiner : Determiner
item : Option PolarityItem

Instances For

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

The probes agree on where the negation sits.

Equations

q.WellFormed = ∀ pi ∈ q.item, pi.polarity.scope = q.determiner.scope

Instances For

@[instance_reducible]

instance BuringGunlogson2000.instDecidableWellFormed (q : Question) :

Decidable q.WellFormed

Equations

BuringGunlogson2000.instDecidableWellFormed { determiner := determiner, item := none } = isTrue ⋯
BuringGunlogson2000.instDecidableWellFormed { determiner := d, item := some pi } = decidable_of_iff (pi.polarity.scope = d.scope) ⋯

def BuringGunlogson2000.Scope.form :

Scope → Question.PQForm

The question type a well-formed question realizes: inner negation is an inner-negation NPQ, outer negation an outer-negation one.

Equations

Instances For

theorem BuringGunlogson2000.no_takes_either_not_too :

{ determiner := Determiner.no, item := some PolarityItem.either }.WellFormed ∧ ¬{ determiner := Determiner.no, item := some PolarityItem.too }.WellFormed

Is there no vegetarian restaurant either/*too?: 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 PolarityItem.too }.WellFormed ∧ ¬{ determiner := Determiner.notSome, item := some PolarityItem.either }.WellFormed

Isn't there some vegetarian restaurant *either/too?: 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 PolarityItem.brauchen }.WellFormed ∧ ¬{ determiner := Determiner.nichtEin, item := some PolarityItem.brauchen }.WellFormed

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

theorem BuringGunlogson2000.wellFormed_iff_determiner_form (d : Determiner) (pi : PolarityItem) :

{ determiner := d, item := some pi }.WellFormed ↔ pi.polarity.scope.form = d.scope.form

In a well-formed question the polarity item classifies the question exactly as the determiner does, so either probe alone settles the reading.

theorem BuringGunlogson2000.probed_felicity (q : Question) (ev : Question.ContextualEvidence) :

Felicitous q.determiner.scope.form ev ↔ Question.evidenceBiasOK q.determiner.scope.form ev = true

The two probes and the evidence conditions are independent diagnostics of the same distinction: the reading a well-formed question's determiner fixes is felicitous exactly where the corresponding evidence condition holds.