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
    @[implicit_reducible]
    instance Semantics.Negation.CzechNegation.instDecidableEqNegPosition :
    DecidableEq NegPosition
    Equations
    source
    def Semantics.Negation.CzechNegation.instReprNegPosition.repr :
    NegPosition → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance Semantics.Negation.CzechNegation.instReprNegPosition :
      Repr NegPosition
      Equations
      source
      def Semantics.Negation.CzechNegation.NegPosition.toNat :
      NegPosition → ℕ

      Numeric embedding: inner ↦ 0, medial ↦ 1, outer ↦ 2 (by scope width).

      Equations
      Instances For
        source
        @[implicit_reducible]
        instance Semantics.Negation.CzechNegation.instLinearOrderNegPosition :
        LinearOrder NegPosition
        Equations
        • One or more equations did not get rendered due to their size.
        source
        def Semantics.Negation.CzechNegation.NegPosition.equivFin :
        NegPosition ≃ Fin 3

        NegPosition ≃ Fin 3.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[implicit_reducible]
          instance Semantics.Negation.CzechNegation.instFintypeNegPosition :
          Fintype 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
            @[implicit_reducible]
            instance Semantics.Negation.CzechNegation.instDecidableEqDiagnostic :
            DecidableEq Diagnostic
            Equations
            source
            @[implicit_reducible]
            instance Semantics.Negation.CzechNegation.instReprDiagnostic :
            Repr Diagnostic
            Equations
            source
            def Semantics.Negation.CzechNegation.instReprDiagnostic.repr :
            Diagnostic → ℕ → Std.Format
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Semantics.Negation.CzechNegation.Diagnostic.equivFin :
              Diagnostic ≃ Fin 5

              Diagnostic ≃ Fin 5.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[implicit_reducible]
                instance Semantics.Negation.CzechNegation.instFintypeDiagnostic :
                Fintype 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
                  source
                  theorem Semantics.Negation.CzechNegation.licenses_injective :
                  Function.Injective fun (pos : NegPosition) (d : Diagnostic) => licenses pos d

                  Each NegPosition has a unique 5-bit diagnostic signature. This is the formal statement that the diagnostic table (Table 1) distinguishes all three negation readings.

                  source
                  theorem Semantics.Negation.CzechNegation.inner_lt_medial :
                  NegPosition.inner < NegPosition.medial

                  Scope ordering: inner < medial < outer.

                  source
                  theorem Semantics.Negation.CzechNegation.medial_lt_outer :
                  NegPosition.medial < NegPosition.outer
                  source
                  theorem Semantics.Negation.CzechNegation.inner_lt_outer :
                  NegPosition.inner < NegPosition.outer