Staňková and Šimík (2025): Negation in Czech Polar Questions

Staňková and Šimík analyse negation in Czech polar questions. The negative prefix moves with the finite verb, so verb position fixes the position of negation: a clause-initial verb sits above the canonical negation operator and is licensed only by Repp's commitment operator FALSUM (Simik2024.falsumCz_eq_one_of_falsum), while a verb in situ is licensed by either (mem_availableReadings_iff). Following Zeijlstra, the concord item žádný and the prefix carry an uninterpretable negative feature and contribute no negation of their own, so of the readings the determiner fragment lists for žádný only the indefinite one yields 'no' under the canonical operator (compl_eq_no_iff). The canonical operator licenses concord items and needs negative contextual evidence; FALSUM licenses positive polarity items and is indifferent to evidence; and declarative word order needs evidence. Felicity in a context follows from these three sources (Felicitous), which yields the predictions the paper's naturalness study tests: in interrogative questions the polarity item is felicitous in every context and the concord item in none (v1_ppi_any_context, v1_nci_never), and declarative questions need evidence, the concord item negative evidence (nonV1_nci_iff, nonV1_ppi_iff). The particle náhodou is licensed by FALSUM alone, so it excludes concord items whatever the word order (nahodou_excludes_nci), and copak needs evidence matching the question's polarity, against the speaker's prior belief (copak_requires_bias, copak_prior_ne_evidence).

Implementation notes

The readings of negation are Šimík's inner and outer negation. The main experiment (seventy-five speakers, a fully crossed design of verb position, indefinite and context, cumulative link mixed models) found a main effect of the indefinite in interrogative questions, no effect of context there, a preference for negative contexts and for concord items in declarative questions, high naturalness of interrogative questions under positive evidence, a main effect of the indefinite for náhodou questions, and a main effect of context for copak questions; these results are stated in prose only.

References

• [SS25]
• [Rep13]
• [Zei04]
• [Gun02]
• [Sud13]
• [BG00]
• [Nek96]
• [Sim24]

Verb position and the readings of negation

inductive StankovaSimik2025.VerbPosition : Type

The finite verb of a Czech polar question is clause-initial, in interrogative word order, or in situ, in declarative word order. The negative prefix is inseparable from the finite verb, so verb position fixes the position of negation.

• v1 : VerbPosition
• nonV1 : VerbPosition

@[instance_reducible]

instance StankovaSimik2025.instDecidableEqVerbPosition : DecidableEq VerbPosition

Equations

• StankovaSimik2025.instDecidableEqVerbPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance StankovaSimik2025.instReprVerbPosition : Repr VerbPosition

Equations

• StankovaSimik2025.instReprVerbPosition = { reprPrec := StankovaSimik2025.instReprVerbPosition.repr }

def StankovaSimik2025.instReprVerbPosition.repr : VerbPosition → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance StankovaSimik2025.instFintypeVerbPosition : Fintype VerbPosition

Equations

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

def StankovaSimik2025.VerbPosition.availableReadings : VerbPosition → List Polarity

The readings of negation available at a verb position, each given as the polarity of the proposition the question double-checks, .positive for FALSUM, the outer reading, and .negative for the canonical operator, the inner reading. The clause-initial verb raises above the canonical operator and is licensed by FALSUM alone, the verb in situ by FALSUM or by the canonical operator (the paper's (11) and (12)).

Equations

• StankovaSimik2025.VerbPosition.v1.availableReadings = [Polarity.positive]
• StankovaSimik2025.VerbPosition.nonV1.availableReadings = [Polarity.negative, Polarity.positive]

theorem StankovaSimik2025.mem_availableReadings_iff (wp : VerbPosition) (n : Polarity) : n ∈ wp.availableReadings ↔ n = Polarity.positive ∨ wp = VerbPosition.nonV1

A reading is available exactly when its operator c-commands the negated verb, which FALSUM always does and the canonical operator does only over the verb in situ.

def StankovaSimik2025.VerbPosition.defaultReading : VerbPosition → Polarity

The unmarked reading at a verb position is that of the lowest available operator.

Equations

• StankovaSimik2025.VerbPosition.v1.defaultReading = Polarity.positive
• StankovaSimik2025.VerbPosition.nonV1.defaultReading = Polarity.negative

theorem StankovaSimik2025.defaultReading_mem (wp : VerbPosition) : wp.defaultReading ∈ wp.availableReadings

Indefinites as proxies for the readings

inductive StankovaSimik2025.Indefinite : Type

The experiment manipulates the indefinite, the negative concord item žádný as a proxy for inner negation or the positive polarity item nějaký as a proxy for FALSUM.

• nci : Indefinite
• ppi : Indefinite

@[instance_reducible]

instance StankovaSimik2025.instDecidableEqIndefinite : DecidableEq Indefinite

Equations

• StankovaSimik2025.instDecidableEqIndefinite x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def StankovaSimik2025.instReprIndefinite.repr : Indefinite → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance StankovaSimik2025.instReprIndefinite : Repr Indefinite

Equations

• StankovaSimik2025.instReprIndefinite = { reprPrec := StankovaSimik2025.instReprIndefinite.repr }

@[instance_reducible]

instance StankovaSimik2025.instFintypeIndefinite : Fintype Indefinite

Equations

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

def StankovaSimik2025.Indefinite.word : Indefinite → Czech.Determiners.QuantityWord

The determiner realizing each indefinite.

Equations

• StankovaSimik2025.Indefinite.nci.word = Czech.Determiners.QuantityWord.zadny
• StankovaSimik2025.Indefinite.ppi.word = Czech.Determiners.QuantityWord.nejaky

def StankovaSimik2025.Indefinite.entry : Indefinite → PolarityItem

The polarity entry of each indefinite.

Equations

• StankovaSimik2025.Indefinite.nci.entry = Czech.PolarityItems.zadny
• StankovaSimik2025.Indefinite.ppi.entry = Czech.PolarityItems.nejaky

theorem StankovaSimik2025.compl_eq_no_iff {d : Quantifier.GQ.Family} (hd : d ∈ Semantics.Denotes.denote Indefinite.nci.word) : dᶜ = Quantifier.GQ.Family.no ↔ d = Quantifier.GQ.Family.some

The concord item and the prefix carry [uNeg] and so "do not map to negation" (p. 5), the canonical operator being the clause's one negation. Of the readings of žádný, exactly the indefinite one then yields no; the negative-quantifier reading yields double negation.

def StankovaSimik2025.LicensedAt (e : PolarityItem) (n : Polarity) : Prop

A polarity item is licensed at a reading of negation when a positive polarity item falls under FALSUM and a negative one under the canonical operator (the paper's (11) and (12)).

Equations

• StankovaSimik2025.LicensedAt e n = ((e.IsPPI → n = Polarity.positive) ∧ (e.IsNPI → n = Polarity.negative))

@[instance_reducible]

instance StankovaSimik2025.instDecidableLicensedAt (e : PolarityItem) (n : Polarity) : Decidable (LicensedAt e n)

Equations

• StankovaSimik2025.instDecidableLicensedAt e n = id inferInstance

theorem StankovaSimik2025.licensedAt_ppi_iff_not_nci (n : Polarity) : LicensedAt Indefinite.ppi.entry n ↔ ¬LicensedAt Indefinite.nci.entry n

The two indefinites split the readings, the polarity item being licensed exactly where the concord item is not.

Bias and felicity

def StankovaSimik2025.ReadingAdmits : Polarity → SignType → Prop

The canonical operator requires negative contextual evidence, as in the evidentially biased contexts of [Gun02] and [Sud13], while FALSUM, conveying epistemic rather than evidential bias, requires none.

Equations

• StankovaSimik2025.ReadingAdmits Polarity.negative x✝ = (x✝ = -1)
• StankovaSimik2025.ReadingAdmits Polarity.positive x✝ = True

@[instance_reducible]

instance StankovaSimik2025.instDecidableReadingAdmits (n : Polarity) (ctx : SignType) : Decidable (ReadingAdmits n ctx)

Equations

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

def StankovaSimik2025.WordOrderAdmits : VerbPosition → SignType → Prop

Declarative word order requires contextual evidence ([Gun02]); interrogative word order requires none.

Equations

• StankovaSimik2025.WordOrderAdmits StankovaSimik2025.VerbPosition.v1 x✝ = True
• StankovaSimik2025.WordOrderAdmits StankovaSimik2025.VerbPosition.nonV1 x✝ = (x✝ ≠ 0)

@[instance_reducible]

instance StankovaSimik2025.instDecidableWordOrderAdmits (wp : VerbPosition) (ctx : SignType) : Decidable (WordOrderAdmits wp ctx)

Equations

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

def StankovaSimik2025.Felicitous (wp : VerbPosition) (ind : Indefinite) (ctx : SignType) : Prop

A negative polar question with an indefinite is felicitous in a context when some reading available at its verb position licenses the indefinite and admits the context's evidence, and the word order admits the evidence.

Equations

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

@[instance_reducible]

instance StankovaSimik2025.instDecidableFelicitous (wp : VerbPosition) (ind : Indefinite) (ctx : SignType) : Decidable (Felicitous wp ind ctx)

Equations

• StankovaSimik2025.instDecidableFelicitous wp ind ctx = id inferInstance

theorem StankovaSimik2025.v1_ppi_any_context (ctx : SignType) : Felicitous VerbPosition.v1 Indefinite.ppi ctx

In interrogative questions the positive polarity item is felicitous in every context, since FALSUM licenses it and is indifferent to evidence.

theorem StankovaSimik2025.v1_nci_never (ctx : SignType) : ¬Felicitous VerbPosition.v1 Indefinite.nci ctx

In interrogative questions the negative concord item is never felicitous, since the clause-initial verb is out of reach of the canonical operator.

theorem StankovaSimik2025.v1_context_invariant (ind : Indefinite) (ctx ctx' : SignType) : Felicitous VerbPosition.v1 ind ctx ↔ Felicitous VerbPosition.v1 ind ctx'

Interrogative questions are indifferent to the context.

theorem StankovaSimik2025.nonV1_nci_iff (ctx : SignType) : Felicitous VerbPosition.nonV1 Indefinite.nci ctx ↔ ctx = -1

A declarative question with the concord item is felicitous exactly under negative evidence, which inner negation requires.

theorem StankovaSimik2025.nonV1_ppi_iff (ctx : SignType) : Felicitous VerbPosition.nonV1 Indefinite.ppi ctx ↔ ctx ≠ 0

A declarative question with the polarity item is felicitous exactly under some evidence, since FALSUM licenses the verb in situ and the word order needs evidence.

theorem StankovaSimik2025.nonV1_neutral_infelicitous (ind : Indefinite) : ¬Felicitous VerbPosition.nonV1 ind 0

Declarative questions are infelicitous without contextual evidence.

theorem StankovaSimik2025.falsum_broader_than_english_outer : ¬BuringGunlogson2000.Felicitous (some Polarity.positive) 1 ∧ Felicitous VerbPosition.v1 Indefinite.ppi 1

Czech FALSUM is broader than English high negation, since an interrogative question with the polarity item is felicitous under positive evidence (the paper's (14)), which the evidence condition of [BG00] on English outer negation excludes.

The particles

theorem StankovaSimik2025.nahodou_excludes_nci (wp : VerbPosition) : ¬∃ n ∈ wp.availableReadings, LicensedAt Indefinite.nci.entry n ∧ Simik2024.NahodouLicensed Polarity.negative n

Náhodou excludes the concord item at either verb position, since the item needs inner negation and the particle needs FALSUM (the paper's (17) and (18)).

theorem StankovaSimik2025.nahodou_ppi (wp : VerbPosition) : ∃ n ∈ wp.availableReadings, LicensedAt Indefinite.ppi.entry n ∧ Simik2024.NahodouLicensed Polarity.negative n

Náhodou is felicitous with the polarity item at either verb position, the verb in situ being licensed by FALSUM under a contrastive topic.

def StankovaSimik2025.CopakLicensed (pol : Polarity) (ctx : SignType) : Prop

Copak is felicitous exactly when the context's evidence matches the question's polarity.

Equations

• StankovaSimik2025.CopakLicensed pol ctx = (ctx = Simik2024.evidence pol)

@[instance_reducible]

instance StankovaSimik2025.instDecidableCopakLicensed (pol : Polarity) (ctx : SignType) : Decidable (CopakLicensed pol ctx)

Equations

• StankovaSimik2025.instDecidableCopakLicensed pol ctx = id inferInstance

theorem StankovaSimik2025.copak_requires_bias (pol : Polarity) : ¬CopakLicensed pol 0

Copak is infelicitous without contextual evidence.

theorem StankovaSimik2025.copak_prior_ne_evidence (pol : Polarity) : (Simik2024.prior pol = 1 ↔ Simik2024.evidence pol = -1) ∧ (Simik2024.prior pol = -1 ↔ Simik2024.evidence pol = 1)

Copak marks a conflict, the prior belief it conveys opposing the evidence it requires.

theorem StankovaSimik2025.nahodou_copak_opposite (ctx : SignType) : Simik2024.NahodouLicensed Polarity.negative Polarity.positive ∧ (CopakLicensed Polarity.negative ctx → ctx ≠ 0)

The two particles part on context, náhodou being licensed by FALSUM whatever the evidence and copak only under evidence.