Negation in Czech polar questions (Staňková & Šimík 2025)

This file formalizes [stankova-2025], a naturalness-rating study of negation in Czech polar questions. Verb position proxies the negation reading — V1 forces FALSUM, nonV1 defaults to inner negation — with the (11)-(12) reading inventory derived from c-command height and the §5.2 predictions derived from clash counting, checked against the typed stimuli in Data.Examples.StankovaSimik2025. The subexperiments make náhodou an overt FALSUM indicator (§6.1) and copak sensitive to contextual evidence (§6.2). Lexical entries live in Czech.Particles and Czech.Determiners; the three-way negation system and its Table 1 diagnostics are [stankova-2026]'s and live in Stankova2026.

References

• [stankova-2025], [stankova-2023], [simik-2024], [nekula-1996].

The main experiment (§5)

A 2×2×2 naturalness-rating design (75 participants, Likert 1-7, CLMM; item (13)) crossing verb position, indefinite (NCI žádný vs PPI nějaký), and context (negative vs neutral). PPIs are more natural in V1 PQs (z = −15.674, p < .001) and NCIs in nonV1 (z = 6.208, p < 0.01); context matters only in nonV1 (z = 8.674, p < 0.01; V1 n.s., z = −1.374, p = 0.169; interaction z = 2.933, p < 0.01). In positive-evidence contexts ((14), §5.3) V1 PQs stay natural (median 6, vs 5 neutral).

inductive StankovaSimik2025.VerbPosition : Type

Verb position in a Czech PQ — V1 (interrogative word order) or nonV1 (declarative). Since ne- is inseparable from the finite verb, verb position fixes the syntactic position of negation (§2).

• 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 ⋯

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

Equations

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

@[instance_reducible]

instance StankovaSimik2025.instReprVerbPosition : Repr VerbPosition

Equations

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

def StankovaSimik2025.VerbPosition.verbHeight : VerbPosition → ℕ

Height of the negated verb in Position.toNat coordinates; the V1 verb raises into the outer (PolP) region, the nonV1 verb stays in TP ((11)-(12)).

Equations

• StankovaSimik2025.VerbPosition.v1.verbHeight = Czech.Negation.Position.outer.toNat
• StankovaSimik2025.VerbPosition.nonV1.verbHeight = Czech.Negation.Position.inner.toNat

def StankovaSimik2025.VerbPosition.availableReadings : VerbPosition → List Czech.Negation.Position

Negation readings available per verb position ((11)-(12)) — V1 only outer; nonV1 also inner (outer there needs a contrastive topic and a focused verb, ex. 18). The substrate's medial reading, [stankova-2026]'s refinement, patterns with inner.

Equations

• StankovaSimik2025.VerbPosition.v1.availableReadings = [Czech.Negation.Position.outer]
• StankovaSimik2025.VerbPosition.nonV1.availableReadings = [Czech.Negation.Position.inner, Czech.Negation.Position.medial, Czech.Negation.Position.outer]

theorem StankovaSimik2025.mem_availableReadings_iff (wp : VerbPosition) (pos : Czech.Negation.Position) : pos ∈ wp.availableReadings ↔ wp.verbHeight ≤ pos.toNat

A reading is available at a verb position iff its operator sits at or above the negated verb — the c-command condition behind (11)-(12).

def StankovaSimik2025.VerbPosition.defaultReading : VerbPosition → Czech.Negation.Position

The default (unmarked) negation reading per verb position.

Equations

• StankovaSimik2025.VerbPosition.v1.defaultReading = Czech.Negation.Position.outer
• StankovaSimik2025.VerbPosition.nonV1.defaultReading = Czech.Negation.Position.inner

theorem StankovaSimik2025.defaultReading_eq_min (wp : VerbPosition) : wp.availableReadings.min? = some wp.defaultReading

The default reading is the narrowest-scope available one — canonical inner negation wherever the verb position allows it.

def StankovaSimik2025.VerbPosition.requiresContextualEvidence (wp : VerbPosition) : Bool

Whether a verb position's default reading requires contextual evidence (§5). Context sensitivity tracks the reading, not the word order; V1's FALSUM default is natural under any evidential bias, nonV1's inner default needs negative evidence.

Equations

• wp.requiresContextualEvidence = (wp.defaultReading.biasStrength == Question.EvidentialBiasStrength.strong)

theorem StankovaSimik2025.nci_diagnoses_nonV1 (wp : VerbPosition) : Czech.Negation.licenses wp.defaultReading Czech.Negation.Diagnostic.nciLicensed = true → wp = VerbPosition.nonV1

An NCI-tolerant default reading identifies declarative word order; the NCI advantage in nonV1 PQs diagnoses inner negation.

theorem StankovaSimik2025.ppi_diagnoses_v1 (wp : VerbPosition) : Czech.Negation.licenses wp.defaultReading Czech.Negation.Diagnostic.ppiOutscoping = true → wp = VerbPosition.v1

Dually, a PPI-outscoping default identifies interrogative word order; the PPI advantage in V1 PQs diagnoses outer negation (FALSUM).

inductive StankovaSimik2025.Indefinite : Type

The manipulated indefinite (§5.1), a proxy for the negation reading — the NCI žádný for inner, the PPI nějaký for outer.

• 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 ⋯

@[instance_reducible]

instance StankovaSimik2025.instReprIndefinite : Repr Indefinite

Equations

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

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

Equations

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

def StankovaSimik2025.Indefinite.entry : Indefinite → Czech.Determiners.DetEntry

The determiner entry realizing each indefinite.

Equations

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

def StankovaSimik2025.Indefinite.diagnostic : Indefinite → Czech.Negation.Diagnostic

The Table 1 diagnostic each indefinite tests.

Equations

• StankovaSimik2025.Indefinite.nci.diagnostic = Czech.Negation.Diagnostic.nciLicensed
• StankovaSimik2025.Indefinite.ppi.diagnostic = Czech.Negation.Diagnostic.ppiOutscoping

def StankovaSimik2025.Indefinite.reading : Indefinite → Czech.Negation.Position

The negation reading each indefinite proxies for (§5.1).

Equations

• StankovaSimik2025.Indefinite.nci.reading = Czech.Negation.Position.inner
• StankovaSimik2025.Indefinite.ppi.reading = Czech.Negation.Position.outer

theorem StankovaSimik2025.indefinite_diagnostic_matches_lexicon (ind : Indefinite) : ind.entry.diagnostic = some ind.diagnostic

Each indefinite tests exactly the diagnostic its determiner entry carries.

The §5.2 predictions

A condition is penalized once per clash — indefinite against default reading, indefinite against context, verb position against context.

def StankovaSimik2025.clashCount (wp : VerbPosition) (ind : Indefinite) (ctx : Question.ContextualEvidence) : ℕ

The number of clashes in a condition of the §5.1 design.

Equations

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

def StankovaSimik2025.predictedJudgment : ℕ → Features.Judgment

The judgment tier predicted from the clash count.

Equations

• StankovaSimik2025.predictedJudgment 0 = Features.Judgment.acceptable
• StankovaSimik2025.predictedJudgment 1 = Features.Judgment.marginal
• StankovaSimik2025.predictedJudgment x✝ = Features.Judgment.unacceptable

theorem StankovaSimik2025.v1_ppi_preferred (ctx : Question.ContextualEvidence) : clashCount VerbPosition.v1 Indefinite.ppi ctx < clashCount VerbPosition.v1 Indefinite.nci ctx

In V1 PQs the PPI variant incurs fewer clashes than the NCI variant in every context (the main effect of INDEFINITE).

theorem StankovaSimik2025.v1_ppi_context_invariant : clashCount VerbPosition.v1 Indefinite.ppi Question.ContextualEvidence.againstP = clashCount VerbPosition.v1 Indefinite.ppi Question.ContextualEvidence.neutral

V1 PQs with the matching PPI are equally natural in negative and neutral contexts (the null effect of CONTEXT in V1).

theorem StankovaSimik2025.v1_indefinite_context_interaction : clashCount VerbPosition.v1 Indefinite.nci Question.ContextualEvidence.againstP - clashCount VerbPosition.v1 Indefinite.ppi Question.ContextualEvidence.againstP < clashCount VerbPosition.v1 Indefinite.nci Question.ContextualEvidence.neutral - clashCount VerbPosition.v1 Indefinite.ppi Question.ContextualEvidence.neutral

The INDEFINITE effect in V1 is larger in neutral contexts, where the NCI also clashes with the context (the CONTEXT × INDEFINITE interaction).

theorem StankovaSimik2025.nonV1_negative_context_preferred (ind : Indefinite) : clashCount VerbPosition.nonV1 ind Question.ContextualEvidence.againstP < clashCount VerbPosition.nonV1 ind Question.ContextualEvidence.neutral

nonV1 PQs incur fewer clashes in negative than in neutral contexts for either indefinite (the main effect of CONTEXT).

theorem StankovaSimik2025.nonV1_nci_preferred : clashCount VerbPosition.nonV1 Indefinite.nci Question.ContextualEvidence.againstP < clashCount VerbPosition.nonV1 Indefinite.ppi Question.ContextualEvidence.againstP

In negative contexts the nonV1 NCI variant incurs fewer clashes than the PPI variant (the main effect of INDEFINITE).

def StankovaSimik2025.analyzedStimuli : List (Data.Examples.LinguisticExample × VerbPosition × Indefinite × Question.ContextualEvidence)

The (13) stimulus quadruple with each variant's verb position, indefinite, and context.

Equations

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

theorem StankovaSimik2025.stimuli_match_default_licensing : (analyzedStimuli.all fun (x : Data.Examples.LinguisticExample × VerbPosition × Indefinite × Question.ContextualEvidence) => match x with | (e, wp, ind, snd) => (e.judgment == Features.Judgment.acceptable) == Czech.Negation.licenses wp.defaultReading ind.diagnostic) = true

Each (13) variant is fully natural iff Table 1 licenses its indefinite's diagnostic at the verb position's default reading.

theorem StankovaSimik2025.stimuli_match_clash_prediction : (analyzedStimuli.all fun (x : Data.Examples.LinguisticExample × VerbPosition × Indefinite × Question.ContextualEvidence) => match x with | (e, wp, ind, ctx) => e.judgment == predictedJudgment (clashCount wp ind ctx)) = true

Clash counting predicts each (13) variant's three-way judgment tier.

theorem StankovaSimik2025.falsum_broader_than_english_hiNQ : Question.evidenceBiasOK Question.PQForm.HiNQ Question.ContextualEvidence.forP = false ∧ Examples.ex14.judgment = Features.Judgment.acceptable

The (14) stimulus is natural under positive evidence, the cell [romero-2024]'s table rules out for English HiNQs (§5.3).

Classification

inductive StankovaSimik2025.ParticleSemantics : Type

Semantic classification of the Czech PQ particles ([stankova-2025] §6 for náhodou/copak; [stankova-2026] §2.2 supplies the rest via Stankova2026.classification).

• orderingSourceModifier : ParticleSemantics

  Modifies the ordering source of an epistemic modal (náhodou; both papers' hypothesis).

• temporalEndpoint : ParticleSemantics

  Temporal-endpoint presupposition; with telic predicates needs propositional negation (ještě).

• veridicalEmphasis : ParticleSemantics

  'Really'-type emphasis (fakt; semantics deferred by [stankova-2026], cf. VERUM).

• npi : ParticleSemantics

  General NPI (vůbec).

• evidentialConflict : ParticleSemantics

  Conflict between prior epistemic state and contextual evidence (copak; cross-Slavic RAZVE family).

@[instance_reducible]

instance StankovaSimik2025.instDecidableEqParticleSemantics : DecidableEq ParticleSemantics

Equations

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

def StankovaSimik2025.instReprParticleSemantics.repr : ParticleSemantics → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance StankovaSimik2025.instReprParticleSemantics : Repr ParticleSemantics

Equations

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

def StankovaSimik2025.classification : List (Particle × ParticleSemantics)

This paper's classification of its two tested particles.

Equations

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

The experimentally separated bias dimensions (§6)

def StankovaSimik2025.requiresEvidentialBias (p : Particle) : Option Bool

Whether a particle requires evidential bias — some true for copak (§6.2), some false for the FALSUM-tied náhodou (§6.1, acceptable in any type of context), none where untested.

Equations

• StankovaSimik2025.requiresEvidentialBias p = if p = Czech.Particles.copak then some true else if p = Czech.Particles.nahodou then some false else none

theorem StankovaSimik2025.nahodou_context_insensitive : requiresEvidentialBias Czech.Particles.nahodou = some false

In the §6.1 subexperiment NCIs degrade náhodou PQs (z = −12.845, p < .001), so náhodou "could be used as an overt indicator of the covert FALSUM operator being present in the structure" — and FALSUM is context-insensitive.

def StankovaSimik2025.nahodouStimuli : List (Data.Examples.LinguisticExample × Czech.Negation.Diagnostic)

The §6.1 stimuli ((17) both variants, plus the nonV1 (18)) with the diagnostic each manipulates.

Equations

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

theorem StankovaSimik2025.nahodou_stimuli_match_falsum : (nahodouStimuli.all fun (x : Data.Examples.LinguisticExample × Czech.Negation.Diagnostic) => match x with | (e, d) => (e.judgment == Features.Judgment.acceptable) == Czech.Negation.licenses Czech.Negation.Position.outer d) = true

náhodou pins the negation to FALSUM, so Table 1's outer row predicts each §6.1 variant's naturalness regardless of verb position; (18) is a nonV1 PQ and still patterns with outer negation.

theorem StankovaSimik2025.copak_context_sensitive : requiresEvidentialBias Czech.Particles.copak = some true

In the §6.2 subexperiment copak PQs are more natural in biased than neutral contexts (z = 9.372, p < .001); copak "strongly indicates a conflict between speaker's prior belief and the currently available evidence" (citing [nekula-1996]), licensed in positive and negative PQs alike (exs. 19a-b). Its cross-Slavic kin are Polish czyby and Russian razve (p. 12).

theorem StankovaSimik2025.nahodou_copak_opposite_context : requiresEvidentialBias Czech.Particles.nahodou ≠ requiresEvidentialBias Czech.Particles.copak

náhodou and copak express opposite bias dimensions — FALSUM-tied and context-insensitive vs evidential-bias-tied and context-sensitive (§6, the two subexperiments).