Documentation

Linglib.Theories.Semantics.Negation.CzechNegation

Czech Three-Way Negation: Core Types #

@cite{stankova-2025} @cite{zeijlstra-2004}

Pure type definitions for the three-way negation distinction in Czech polar questions (Staňková 2026). Extracted from Phenomena.Negation.CzechThreeWayNeg so that Fragment files can reference these types without importing empirical data.

source
inductive Semantics.Negation.CzechNegation.NegPosition :
Type

The three LF positions for negation in Czech PQs (Staňková 2026 §3, ex. 16).

[CP... [PolP ne- [ModP ne- [TP ne-]]]] OUTER MEDIAL INNER

  • inner : NegPosition

    Inner negation: in TP, propositional ¬p. Narrow scope. Licenses NCIs by Agree, licenses NPIs. Standard sentential negation.

  • medial : NegPosition

    Medial negation: in ModP, scopes over □_ev. Wide scope but syntactically low. Non-propositional: part of evidential bias presupposition.

  • outer : NegPosition

    Outer negation: in PolP, FALSUM operator. Widest scope. Maps to high negation (VSO word order). Obligatorily focused.

Instances For
    source
    instance Semantics.Negation.CzechNegation.instDecidableEqNegPosition :
    DecidableEq NegPosition
    Equations
    source
    instance Semantics.Negation.CzechNegation.instBEqNegPosition :
    BEq NegPosition
    Equations
    source
    def Semantics.Negation.CzechNegation.instBEqNegPosition.beq :
    NegPosition → NegPosition → Bool
    Equations
    Instances For
      source
      def Semantics.Negation.CzechNegation.instReprNegPosition.repr :
      NegPosition → Nat → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        instance Semantics.Negation.CzechNegation.instReprNegPosition :
        Repr NegPosition
        Equations
        source
        inductive Semantics.Negation.CzechNegation.Diagnostic :
        Type

        Diagnostics that distinguish the three negation readings (Table 1).

        • ppiOutscoping : Diagnostic

          ne- outscopes a PPI like nějaký 'some.DET.PPI'

        • nciLicensed : Diagnostic

          Negative concord item like žádný 'no.DET.NCI' is licensed

        • nahodou : Diagnostic

          Particle náhodou 'by chance' is compatible

        • jeste : Diagnostic

          Particle ještě 'yet/still' is compatible (with telic predicates + neg)

        • fakt : Diagnostic

          Particle fakt 'really' is compatible

        Instances For
          source
          instance Semantics.Negation.CzechNegation.instDecidableEqDiagnostic :
          DecidableEq Diagnostic
          Equations
          source
          instance Semantics.Negation.CzechNegation.instBEqDiagnostic :
          BEq Diagnostic
          Equations
          source
          def Semantics.Negation.CzechNegation.instBEqDiagnostic.beq :
          Diagnostic → Diagnostic → Bool
          Equations
          Instances For
            source
            def Semantics.Negation.CzechNegation.instReprDiagnostic.repr :
            Diagnostic → Nat → Std.Format
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              instance Semantics.Negation.CzechNegation.instReprDiagnostic :
              Repr Diagnostic
              Equations
              source
              def Semantics.Negation.CzechNegation.licenses :
              NegPosition → Diagnostic → Bool

              Table 1 from Staňková (2026 §3): compatibility of each negation reading with polarity items and particles.

              This is the core empirical fingerprint: each negation position has a unique Boolean signature across the five diagnostics.

              Equations
              Instances For