Staňková (2026): A Three-Way Distinction of Negation Interpretation in Czech

Staňková proposes that negation in Czech polar questions occupies one of three LF positions, outer (PolP), medial (ModP) or inner (TP), and that the polarity items and the particles náhodou, ještě and fakt fingerprint them (her Table 1, licensed). The positions refine Šimík's two readings of negation (Position.ofReading): medial negation is the paper's addition, low like inner negation but non-propositional like FALSUM.

Main results

• licensed_injective, particle_signatures_distinct: Table 1 fingerprints the three positions, and its three particle columns alone do.
• licenses_nciLicensed_iff_licensedAt, licenses_ppiOutscoping_iff_licensedAt: the polarity columns agree with Staňková and Šimík's licensing of the indefinites.
• czech_refines_nonPreposed: Czech splits Romero's low negation form into inner and medial.
• examples_match_table1: the paper's examples check against Table 1.

References

• [Sta26]
• [SS25]
• [Sta23]
• [Zei04]
• [Rom24]
• [Sim24]
• [GG17]

The three positions

inductive Stankova2026.Position : Type

Negation in a Czech polar question takes one of three LF positions, listed by scope width. Inner negation in TP is propositional negation, medial negation in ModP scopes over the evidential modal, and outer negation in PolP is the commitment operator FALSUM (the paper's (16)).

• inner : Position

  Inner negation is propositional ¬p in TP, which licenses negative concord items by Agree ([Zei04]).

• medial : Position

  Medial negation scopes over the evidential modal in ModP, in the bias presupposition.

• outer : Position

  Outer negation is FALSUM in PolP, high negation with obligatory focus.

@[instance_reducible]

instance Stankova2026.instDecidableEqPosition : DecidableEq Position

Equations

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

@[instance_reducible]

instance Stankova2026.instReprPosition : Repr Position

Equations

• Stankova2026.instReprPosition = { reprPrec := Stankova2026.instReprPosition.repr }

def Stankova2026.instReprPosition.repr : Position → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Stankova2026.instFintypePosition : Fintype Position

Equations

• Stankova2026.instFintypePosition = { elems := { val := ↑Stankova2026.Position.enumList, nodup := Stankova2026.Position.enumList_nodup }, complete := Stankova2026.instFintypePosition._proof_1 }

def Stankova2026.Position.ofReading : Polarity → Position

Each reading of [Sim24] is a position. The inner reading, double-checking the negation of the prejacent (.negative), is inner negation, and the outer reading, double-checking the prejacent (.positive), is outer negation.

Equations

• Stankova2026.Position.ofReading Polarity.negative = Stankova2026.Position.inner
• Stankova2026.Position.ofReading Polarity.positive = Stankova2026.Position.outer

inductive Stankova2026.BiasStrength : Type

The evidential bias strength of a negation position (the paper's §3.1): inner negation presupposes evidence for ¬p, medial negation only the absence of evidence for p, and FALSUM conveys epistemic rather than evidential bias.

• strong : BiasStrength
• weak : BiasStrength
• none_ : BiasStrength

@[instance_reducible]

instance Stankova2026.instDecidableEqBiasStrength : DecidableEq BiasStrength

Equations

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

def Stankova2026.instReprBiasStrength.repr : BiasStrength → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Stankova2026.instReprBiasStrength : Repr BiasStrength

Equations

• Stankova2026.instReprBiasStrength = { reprPrec := Stankova2026.instReprBiasStrength.repr }

def Stankova2026.Position.biasStrength : Position → BiasStrength

The evidential bias strength of each position.

Equations

• Stankova2026.Position.inner.biasStrength = Stankova2026.BiasStrength.strong
• Stankova2026.Position.medial.biasStrength = Stankova2026.BiasStrength.weak
• Stankova2026.Position.outer.biasStrength = Stankova2026.BiasStrength.none_

Table 1

inductive Stankova2026.Diagnostic : Type

The Table 1 diagnostics of a negation position.

• ppiOutscoping : Diagnostic

  The negation admits a positive polarity item like nějaký 'some' in its scope.

• nciLicensed : Diagnostic

  The negation licenses a negative concord item like žádný 'no'.

• nahodou : Diagnostic

  The particle náhodou 'by chance' is compatible.

• jeste : Diagnostic

  The particle ještě 'yet, still' is compatible.

• fakt : Diagnostic

  The particle fakt 'really' is compatible.

@[instance_reducible]

instance Stankova2026.instDecidableEqDiagnostic : DecidableEq Diagnostic

Equations

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

def Stankova2026.instReprDiagnostic.repr : Diagnostic → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Stankova2026.instReprDiagnostic : Repr Diagnostic

Equations

• Stankova2026.instReprDiagnostic = { reprPrec := Stankova2026.instReprDiagnostic.repr }

@[instance_reducible]

instance Stankova2026.instFintypeDiagnostic : Fintype Diagnostic

Equations

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

def Stankova2026.licensed : Position → Finset Diagnostic

Table 1: the diagnostics each negation position licenses.

Equations

• Stankova2026.licensed Stankova2026.Position.inner = {Stankova2026.Diagnostic.nciLicensed, Stankova2026.Diagnostic.jeste, Stankova2026.Diagnostic.fakt}
• Stankova2026.licensed Stankova2026.Position.medial = {Stankova2026.Diagnostic.ppiOutscoping, Stankova2026.Diagnostic.fakt}
• Stankova2026.licensed Stankova2026.Position.outer = {Stankova2026.Diagnostic.ppiOutscoping, Stankova2026.Diagnostic.nahodou}

@[reducible, inline]

abbrev Stankova2026.Licenses (pos : Position) (d : Diagnostic) : Prop

A cell of Table 1: the position licenses the diagnostic.

Equations

• Stankova2026.Licenses pos d = (d ∈ Stankova2026.licensed pos)

theorem Stankova2026.licensed_injective : Function.Injective licensed

Table 1 fingerprints the positions: no two license the same diagnostics.

theorem Stankova2026.licenses_nciLicensed_iff {pos : Position} : Licenses pos Diagnostic.nciLicensed ↔ pos = Position.inner

Only propositional negation licenses a concord item, by Agree with the operator.

theorem Stankova2026.licenses_ppiOutscoping_iff {pos : Position} : Licenses pos Diagnostic.ppiOutscoping ↔ pos ≠ Position.inner

Every non-propositional negation admits a positive polarity item.

theorem Stankova2026.licenses_nahodou_iff {pos : Position} : Licenses pos Diagnostic.nahodou ↔ pos = Position.outer

Náhodou singles out FALSUM.

theorem Stankova2026.licenses_jeste_iff {pos : Position} : Licenses pos Diagnostic.jeste ↔ pos = Position.inner

Ještě singles out propositional negation.

theorem Stankova2026.licenses_fakt_iff {pos : Position} : Licenses pos Diagnostic.fakt ↔ pos ≠ Position.outer

Fakt is repelled by FALSUM alone.

theorem Stankova2026.licenses_nciLicensed_iff_licensedAt (n : Polarity) : Licenses (Position.ofReading n) Diagnostic.nciLicensed ↔ StankovaSimik2025.LicensedAt StankovaSimik2025.Indefinite.nci.entry n

On the two readings of [Sim24], the concord column of Table 1 is [SS25]'s licensing of žádný.

theorem Stankova2026.licenses_ppiOutscoping_iff_licensedAt (n : Polarity) : Licenses (Position.ofReading n) Diagnostic.ppiOutscoping ↔ StankovaSimik2025.LicensedAt StankovaSimik2025.Indefinite.ppi.entry n

On the two readings of [Sim24], the polarity column of Table 1 is [SS25]'s licensing of nějaký.

The diagnostic particles ([Sta26] §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.table1 : List (Particle × Diagnostic)

[Sta26]'s Table 1: which diagnostic each particle realizes.

Equations

• Stankova2026.table1 = [(Czech.Particles.nahodou, Stankova2026.Diagnostic.nahodou), (Czech.Particles.jeste, Stankova2026.Diagnostic.jeste), (Czech.Particles.fakt, Stankova2026.Diagnostic.fakt)]

def Stankova2026.diagnostic? (p : Particle) : Option Diagnostic

The Table 1 diagnostic realized by p, if any.

Equations

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

def Stankova2026.Compatible (p : Particle) (pos : Position) : Prop

A particle is compatible with a negation position when the position licenses the particle's Table 1 diagnostic, vacuously for a particle outside the table.

Equations

• Stankova2026.Compatible p pos = ∀ d ∈ Stankova2026.diagnostic? p, Stankova2026.Licenses pos d

@[instance_reducible]

instance Stankova2026.instDecidableCompatible (p : Particle) (pos : Position) : Decidable (Compatible p pos)

Equations

• Stankova2026.instDecidableCompatible p pos = id inferInstance

theorem Stankova2026.nahodou_identifies_outer (pos : Position) : Compatible Czech.Particles.nahodou pos → pos = Position.outer

náhodou uniquely identifies outer negation.

theorem Stankova2026.jeste_identifies_inner (pos : Position) : Compatible Czech.Particles.jeste pos → pos = Position.inner

ještě uniquely identifies inner negation.

theorem Stankova2026.fakt_plus_no_jeste_identifies_medial (pos : Position) : Compatible Czech.Particles.fakt pos ∧ ¬Compatible Czech.Particles.jeste pos → pos = Position.medial

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

theorem Stankova2026.particle_signatures_distinct (pos pos' : Position) (h : ∀ p ∈ [Czech.Particles.nahodou, Czech.Particles.jeste, Czech.Particles.fakt], Compatible p pos ↔ Compatible 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 ([SS25] 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 ([SS25] §2, [Sta26] §1). The VerbPosition API lives with the experiment that established it, in StankovaSimik2025. Crossing word order with polarity gives [Sim24]'s 2×2 grid of PQ forms (Simik2024.CzechPQForm), which maps onto [Rom24]'s PosQ/LoNQ/HiNQ typology.

def Stankova2026.Position.negationPosition : Position → NegationPosition

Outer negation preposes the negated verb, giving the high negation form (HiNQ) of [Rom24], and inner and medial negation leave it in situ, giving the low negation form (LoNQ).

Equations

• Stankova2026.Position.inner.negationPosition = NegationPosition.nonPreposed
• Stankova2026.Position.medial.negationPosition = NegationPosition.nonPreposed
• Stankova2026.Position.outer.negationPosition = NegationPosition.preposed

def Stankova2026.Position.RequiresFocus : Position → Prop

Only outer negation (FALSUM) is obligatorily focused ([Sta26] §3.2).

Equations

• Stankova2026.Position.outer.RequiresFocus = True
• Stankova2026.Position.medial.RequiresFocus = False
• Stankova2026.Position.inner.RequiresFocus = False

@[instance_reducible]

instance Stankova2026.instDecidablePredPositionRequiresFocus : DecidablePred Position.RequiresFocus

Equations

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

def Stankova2026.Position.toVerbPosition : Position → StankovaSimik2025.VerbPosition

Outer negation has the verb clause-initial, inner and medial negation in situ.

Equations

• Stankova2026.Position.inner.toVerbPosition = StankovaSimik2025.VerbPosition.nonV1
• Stankova2026.Position.medial.toVerbPosition = StankovaSimik2025.VerbPosition.nonV1
• Stankova2026.Position.outer.toVerbPosition = StankovaSimik2025.VerbPosition.v1

def Stankova2026.Position.toCzechPQForm : Position → Simik2024.CzechPQForm

In the grid of [Sim24], outer negation gives an interrogative negative question (InterNPQ), and inner and medial negation a declarative one (DeclNPQ).

Equations

• Stankova2026.Position.inner.toCzechPQForm = Simik2024.CzechPQForm.declNPQ
• Stankova2026.Position.medial.toCzechPQForm = Simik2024.CzechPQForm.declNPQ
• Stankova2026.Position.outer.toCzechPQForm = Simik2024.CzechPQForm.interNPQ

theorem Stankova2026.czechPQForm_negation (pos : Position) : pos.toCzechPQForm.negation = some pos.negationPosition

The two form typologies agree: [Sim24]'s grid refines [Rom24]'s.

theorem Stankova2026.czech_refines_nonPreposed : Position.inner.negationPosition = Position.medial.negationPosition ∧ Position.inner.biasStrength ≠ Position.medial.biasStrength ∧ licensed Position.inner ≠ licensed Position.medial

Czech refines [Rom24]'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 : Position) : p.RequiresFocus → p = Position.outer

Obligatory focus singles out outer negation ([Sta26] §3.2).

Verb position and context sensitivity

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

theorem Stankova2026.context_tracks_bias_strength : (Position.ofReading StankovaSimik2025.VerbPosition.v1.defaultReading).biasStrength = BiasStrength.none_ ∧ (Position.ofReading StankovaSimik2025.VerbPosition.nonV1.defaultReading).biasStrength = BiasStrength.strong

Context sensitivity tracks evidential bias strength, none for a clause-initial verb and outer negation and strong for a verb in situ and inner negation.

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 (Datum × Position × 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.

theorem Stankova2026.examples_match_table1 (x : Datum × Position × Diagnostic) : x ∈ analyzedExamples → (x.1.judgment = Judgment.acceptable ↔ Licenses x.2.1 x.2.2)

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 (Datum × SignType × SignType × Simik2024.CzechPQForm)

The positive-evidence stimulus of [SS25], their (14), a negative question with a clause-initial verb after evidence for p, with the bias-profile cell it occupies.

Equations

• Stankova2026.biasCheckedExamples = [(StankovaSimik2025.Examples.ex14, 1, 0, Simik2024.CzechPQForm.interNPQ)]

theorem Stankova2026.bias_examples_match_profile (x : Datum × SignType × SignType × Simik2024.CzechPQForm) : x ∈ biasCheckedExamples → (x.1.judgment = Judgment.acceptable ↔ x.2.2.2 ∈ Simik2024.czechBiasProfile x.2.1 x.2.2.1)

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