Documentation

Linglib.Studies.Stankova2026

Czech three-way negation in polar questions (Staňková 2026) #

[stankova-2026] proposes that negation in Czech polar questions occupies three LF positions (her (16)) — outer (PolP), medial (ModP), inner (TP) — fingerprinted by polarity items and the diagnostic particles náhodou / ještě / fakt (her Table 1, encoded as the substrate's licenses):

Position	ne- > PPI	NCI	náhodou	ještě	fakt
outer	✓	✗	✓	✗	✗
medial	✓	✗	✗	✗	✓
inner	✗	✓	✗	✓	✓

Main results #

signatures_distinct, particle_signatures_distinct — the Table 1 columns jointly fingerprint the three positions.
nahodou_identifies_outer, jeste_identifies_inner, fakt_plus_no_jeste_identifies_medial — per-particle pinning.
instance Distributed Particle Position — Table 1 as a licensing axis alongside clause type and embedding.
czech_refines_loNQ — Czech splits [romero-2024]'s LoNQ into inner and medial.
czechBiasProfile — [simik-2024]'s Table 2 grid of PQ forms by evidential × original bias.
examples_match_table1 — the paper's examples (Data.Examples.Stankova2026) check against Table 1.

References #

[stankova-2026], [stankova-2025], [stankova-2023], [zeijlstra-2004], [romero-2024], [simik-2024], [gartner-gyuris-2017].

Table 1 fingerprints #

def Stankova2026.signature (pos : Czech.Negation.Position) :

List Bool

The Boolean signature of a negation position across the five Table 1 diagnostics.

Equations

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

Instances For

theorem Stankova2026.signatures_distinct :

signature Czech.Negation.Position.outer ≠ signature Czech.Negation.Position.medial ∧ signature Czech.Negation.Position.outer ≠ signature Czech.Negation.Position.inner ∧ signature Czech.Negation.Position.medial ≠ signature Czech.Negation.Position.inner

Each negation position has a unique diagnostic signature — the empirical basis for the three-way distinction.

theorem Stankova2026.only_inner_licenses_nci (p : Czech.Negation.Position) :

Czech.Negation.licenses p Czech.Negation.Diagnostic.nciLicensed = true → p = Czech.Negation.Position.inner

Only inner negation licenses NCIs: the Agree relation with ¬ requires LF c-command, and medial and outer negation are too high ([stankova-2026] (6), (10)).

The diagnostic particles ([stankova-2026] §2.2, Table 1) #

Entries live in Czech.Particles; this paper contributes the §2.2 licensing profiles — ještě felicitous in PQs only under inner negation (§2.2.2, (14); with telic predicates it requires negation, (13)), fakt licensed by inner and medial but repelled by outer on its canonical reading (§2.2.3, (15), fn. 8), vůbec an NPI licensed by inner only ((9)-(10)) — plus the Table 1 assignments and the fingerprint results.

def Stankova2026.classification :

List (Particle × StankovaSimik2025.ParticleSemantics)

This paper's classification of its three particles (the others are classified in StankovaSimik2025.classification). The paper defers fakt's semantics, noting the parallels to English really (Romero & Han's VERUM) and Russian razve.

Equations

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

Instances For

def Stankova2026.table1 :

List (Particle × Czech.Negation.Diagnostic)

[stankova-2026]'s Table 1: which diagnostic each particle realizes.

Equations

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

Instances For

def Stankova2026.diagnostic? (p : Particle) :

Option Czech.Negation.Diagnostic

The Table 1 diagnostic realized by p, if any.

Equations

Stankova2026.diagnostic? p = List.lookup p Stankova2026.table1

Instances For

@[instance_reducible]

instance Stankova2026.instDistributedParticlePosition :

Distributed Particle Czech.Negation.Position

Table 1 as a Distributed axis: negation position is a licensing context like clause type and embedding.

Equations

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

def Stankova2026.compatibleWith? (p : Particle) (pos : Czech.Negation.Position) :

Option Bool

Table 1 compatibility of a particle with a negation position, when the particle carries a diagnostic.

Equations

Stankova2026.compatibleWith? p pos = Option.map (Czech.Negation.licenses pos) (Stankova2026.diagnostic? p)

Instances For

theorem Stankova2026.nahodou_identifies_outer (pos : Czech.Negation.Position) :

compatibleWith? Czech.Particles.nahodou pos = some true → pos = Czech.Negation.Position.outer

náhodou uniquely identifies outer negation.

theorem Stankova2026.jeste_identifies_inner (pos : Czech.Negation.Position) :

compatibleWith? Czech.Particles.jeste pos = some true → pos = Czech.Negation.Position.inner

ještě uniquely identifies inner negation.

theorem Stankova2026.fakt_plus_no_jeste_identifies_medial (pos : Czech.Negation.Position) :

compatibleWith? Czech.Particles.fakt pos = some true ∧ compatibleWith? Czech.Particles.jeste pos = some false → pos = Czech.Negation.Position.medial

fakt accepted while ještě is rejected identifies medial negation.

theorem Stankova2026.particle_signatures_distinct (pos pos' : Czech.Negation.Position) :

(∀ p ∈ [Czech.Particles.nahodou, Czech.Particles.jeste, Czech.Particles.fakt], compatibleWith? p pos = compatibleWith? p pos') → pos = pos'

The three Table 1 particles jointly fingerprint the three negation positions.

theorem Stankova2026.copak_no_diagnostic :

diagnostic? Czech.Particles.copak = none

copak is outside Table 1: it appears in positive and negative PQs alike ([stankova-2025] exs. 19a-b).

Word order and PQ-form typology #

Czech PQs come in V1 (interrogative) and nonV1 (declarative) word orders; since ne- is inseparable from the finite verb, verb position determines the syntactic position of negation ([stankova-2025] §2, [stankova-2026] §1). The VerbPosition API lives with the experiment that established it, in StankovaSimik2025. Crossing word order with polarity gives [simik-2024]'s 2×2 grid of PQ forms, which maps onto [romero-2024]'s PosQ/LoNQ/HiNQ typology.

inductive Stankova2026.CzechPQForm :

[simik-2024]'s 2×2 grid of Czech PQ forms ([simik-2024] §3.2, exx. 11-17): word order (interrogative vs declarative) × polarity.

interPPQ : CzechPQForm
Interrogative (V1), positive: the default unbiased PQ.
interNPQ : CzechPQForm
Interrogative (V1), negative: outer negation, positive epistemic bias; broader distribution than English HiNQ ([simik-2024] §5).
declPPQ : CzechPQForm
Declarative (nonV1), positive: positive evidential bias.
declNPQ : CzechPQForm
Declarative (nonV1), negative: negative evidential bias.

Instances For

@[instance_reducible]

instance Stankova2026.instDecidableEqCzechPQForm :

DecidableEq CzechPQForm

Equations

Stankova2026.instDecidableEqCzechPQForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Stankova2026.instReprCzechPQForm.repr :

CzechPQForm → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Stankova2026.instReprCzechPQForm :

Repr CzechPQForm

Equations

Stankova2026.instReprCzechPQForm = { reprPrec := Stankova2026.instReprCzechPQForm.repr }

def Czech.Negation.Position.toPQForm :

Position → Question.PQForm

[romero-2024] PQ form of a negation position: outer is high negation (HiNQ), inner and medial are both low (LoNQ).

Equations

Instances For

def Czech.Negation.Position.requiresFocus :

Position → Bool

Only outer negation (FALSUM) is obligatorily focused ([stankova-2026] §3.2).

Equations

Czech.Negation.Position.outer.requiresFocus = true
Czech.Negation.Position.medial.requiresFocus = false
Czech.Negation.Position.inner.requiresFocus = false

Instances For

def Czech.Negation.Position.toVerbPosition :

Position → StankovaSimik2025.VerbPosition

Verb position realizing a negation position: outer is V1, inner and medial are nonV1.

Equations

Instances For

def Czech.Negation.Position.toCzechPQForm :

Position → Stankova2026.CzechPQForm

[simik-2024] PQ form of a negation position: outer is InterNPQ, inner and medial are DeclNPQ.

Equations

Instances For

def Stankova2026.CzechPQForm.toPQForm :

CzechPQForm → Question.PQForm

[romero-2024] PQ form of each [simik-2024] grid cell: InterNPQ is HiNQ, DeclNPQ is LoNQ, positive forms are PosQ.

Equations

Instances For

theorem Stankova2026.czechPQForm_consistent_with_pqForm (pos : Czech.Negation.Position) :

pos.toCzechPQForm.toPQForm = pos.toPQForm

The two form typologies agree: [simik-2024]'s grid refines [romero-2024]'s.

theorem Stankova2026.czech_refines_loNQ :

Czech.Negation.Position.inner.toPQForm = Czech.Negation.Position.medial.toPQForm ∧ Czech.Negation.Position.inner.biasStrength ≠ Czech.Negation.Position.medial.biasStrength ∧ signature Czech.Negation.Position.inner ≠ signature Czech.Negation.Position.medial

Czech refines [romero-2024]'s LoNQ: inner and medial share the LoNQ form but differ in evidential bias strength and in Table 1 signatures.

theorem Stankova2026.only_outer_requires_focus (p : Czech.Negation.Position) :

p.requiresFocus = true → p = Czech.Negation.Position.outer

Obligatory focus singles out outer negation ([stankova-2026] §3.2).

theorem Stankova2026.czech_outer_matches_romero_hiNQ_bias :

Czech.Negation.Position.outer.toPQForm = Question.PQForm.HiNQ ∧ Question.originalBiasOK Question.PQForm.HiNQ Question.OriginalBias.forP = true ∧ Question.originalBiasOK Question.PQForm.HiNQ Question.OriginalBias.neutral = false

Czech outer negation is a HiNQ with mandatory original bias for p, matching [romero-2024]'s Table 1.

theorem Stankova2026.czech_low_neg_matches_romero_loNQ_bias :

Czech.Negation.Position.inner.toPQForm = Question.PQForm.LoNQ ∧ Question.originalBiasOK Question.PQForm.LoNQ Question.OriginalBias.neutral = true

Czech low negation is a LoNQ compatible with neutral original bias, matching [romero-2024]'s Table 1.

theorem Stankova2026.czech_inner_matches_romero_evidence_bias :

Czech.Negation.Position.inner.toPQForm = Question.PQForm.LoNQ ∧ Question.evidenceBiasOK Question.PQForm.LoNQ Question.ContextualEvidence.againstP = true

Czech inner negation requires contextual evidence against p, matching [romero-2024]'s Table 2 for LoNQs.

theorem Stankova2026.czech_outer_matches_romero_evidence :

Czech.Negation.Position.outer.toPQForm = Question.PQForm.HiNQ ∧ Question.evidenceBiasOK Question.PQForm.HiNQ Question.ContextualEvidence.againstP = true

Czech outer negation (HiNQ) is compatible with evidence against p (contradiction scenarios).

Verb position and context sensitivity #

The verb-position API (availableReadings, defaultReading, requiresContextualEvidence) is [stankova-2025]'s and lives in StankovaSimik2025; this paper adds the link to evidential bias strength.

theorem Stankova2026.context_tracks_bias_strength :

StankovaSimik2025.VerbPosition.v1.defaultReading.biasStrength = Question.EvidentialBiasStrength.none_ ∧ StankovaSimik2025.VerbPosition.nonV1.defaultReading.biasStrength = Question.EvidentialBiasStrength.strong

Context sensitivity tracks evidential bias strength: V1/outer none, nonV1/inner strong.

The Czech bias profile ([simik-2024] Table 2) #

def Stankova2026.czechBiasProfile :

Question.ContextualEvidence → Question.OriginalBias → List CzechPQForm

Which Czech PQ forms are felicitous per contextual evidence × original speaker bias cell ([simik-2024] Table 2, based on [stankova-2023]); empty list = no form natural.

Equations

Instances For

theorem Stankova2026.interPPQ_is_default :

(czechBiasProfile Question.ContextualEvidence.neutral Question.OriginalBias.neutral).contains CzechPQForm.interPPQ = true

InterPPQ is the sole form felicitous with no bias at all — the default PQ ([simik-2024] §4.1, ex. 25).

theorem Stankova2026.declPPQ_requires_positive_evidence :

(czechBiasProfile Question.ContextualEvidence.forP Question.OriginalBias.neutral).contains CzechPQForm.declPPQ = true ∧ (czechBiasProfile Question.ContextualEvidence.againstP Question.OriginalBias.neutral).contains CzechPQForm.declPPQ = false

DeclPPQ needs positive contextual evidence ([stankova-2023], [simik-2024] §3.2).

theorem Stankova2026.declNPQ_requires_negative_evidence :

(czechBiasProfile Question.ContextualEvidence.againstP Question.OriginalBias.neutral).contains CzechPQForm.declNPQ = true ∧ (czechBiasProfile Question.ContextualEvidence.forP Question.OriginalBias.neutral).contains CzechPQForm.declNPQ = false

DeclNPQ needs negative contextual evidence ([stankova-2023], [simik-2024] §3.2).

theorem Stankova2026.interNPQ_broad_distribution :

(czechBiasProfile Question.ContextualEvidence.forP Question.OriginalBias.neutral).contains CzechPQForm.interNPQ = true ∧ (czechBiasProfile Question.ContextualEvidence.neutral Question.OriginalBias.forP).contains CzechPQForm.interNPQ = true ∧ (czechBiasProfile Question.ContextualEvidence.againstP Question.OriginalBias.forP).contains CzechPQForm.interNPQ = true

InterNPQ appears in three bias cells — the broadest distribution among negative forms, reflecting Czech outer negation's broader range than English HiNQ ([simik-2024] §5).

The paper's examples #

Typed stimuli live in Data.Examples.Stankova2026; each is paired here with the negation reading and Table 1 diagnostic the paper assigns.

def Stankova2026.analyzedExamples :

List (Data.Examples.LinguisticExample × Czech.Negation.Position × Czech.Negation.Diagnostic)

The paper's polarity/particle examples with their negation reading and tested diagnostic.

Equations

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

Instances For

theorem Stankova2026.examples_match_table1 :

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

Table 1 predicts each example's judgment: the diagnostic is licensed at the example's negation position iff the example is acceptable.

def Stankova2026.biasCheckedExamples :

List (Data.Examples.LinguisticExample × Question.ContextualEvidence × Question.OriginalBias × CzechPQForm)

[stankova-2025]'s positive-evidence stimulus ((14): V1 negative PQ after evidence for p) with the bias-profile cell it occupies.

Equations

Stankova2026.biasCheckedExamples = [(StankovaSimik2025.Examples.ex14, Question.ContextualEvidence.forP, Question.OriginalBias.neutral, Stankova2026.CzechPQForm.interNPQ)]

Instances For

theorem Stankova2026.bias_examples_match_profile :

(biasCheckedExamples.all fun (x : Data.Examples.LinguisticExample × Question.ContextualEvidence × Question.OriginalBias × CzechPQForm) => match x with | (e, ev, ob, f) => (e.judgment == Features.Judgment.acceptable) == (czechBiasProfile ev ob).contains f) = true

The bias profile predicts the positive-evidence stimulus — the form is felicitous iff it appears in its evidence × original-bias cell.