Documentation

Linglib.Semantics.Polarity.CzechNegation

Czech Three-Way Negation: Core Types #

The three-way negation distinction in Czech polar questions ([stankova-2026]): the LF positions, the Table 1 diagnostics that fingerprint them, and their evidential bias strengths. Kept free of lexical entries so that Fragment files can reference these types without importing them. NCI licensing by Agree follows [zeijlstra-2004].

source
inductive Czech.Negation.Position :
Type

The three LF positions for negation in Czech PQs ([stankova-2026], her (16)).

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

  • inner : Position

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

  • medial : Position

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

  • outer : Position

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

Instances For
    source
    @[instance_reducible]
    instance Czech.Negation.instDecidableEqPosition :
    DecidableEq Position
    Equations
    source
    def Czech.Negation.instReprPosition.repr :
    Position → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance Czech.Negation.instReprPosition :
      Repr Position
      Equations
      source
      @[instance_reducible]
      instance Czech.Negation.instFintypePosition :
      Fintype Position
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Czech.Negation.Position.toNat :
      Position → ℕ

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

      Equations
      Instances For
        source
        @[instance_reducible]
        instance Czech.Negation.instLinearOrderPosition :
        LinearOrder Position
        Equations
        source
        inductive Czech.Negation.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_reducible]
          instance Czech.Negation.instDecidableEqDiagnostic :
          DecidableEq Diagnostic
          Equations
          source
          @[instance_reducible]
          instance Czech.Negation.instReprDiagnostic :
          Repr Diagnostic
          Equations
          source
          def Czech.Negation.instReprDiagnostic.repr :
          Diagnostic → ℕ → Std.Format
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[instance_reducible]
            instance Czech.Negation.instFintypeDiagnostic :
            Fintype Diagnostic
            Equations
            • One or more equations did not get rendered due to their size.
            source
            def Czech.Negation.licenses :
            Position → Diagnostic → Bool

            [stankova-2026]'s Table 1: 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 Czech.Negation.licenses_injective :
              Function.Injective fun (pos : Position) (d : Diagnostic) => licenses pos d

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

              source
              def Czech.Negation.Position.biasStrength :
              Position → Question.EvidentialBiasStrength

              Evidential bias strength of a negation position — inner strong, medial weak, outer none, FALSUM being epistemic-bias-based ([stankova-2026] §3.1).

              Equations
              Instances For
                source
                theorem Czech.Negation.inner_lt_medial :
                Position.inner < Position.medial

                Scope ordering: inner < medial < outer.

                source
                theorem Czech.Negation.medial_lt_outer :
                Position.medial < Position.outer
                source
                theorem Czech.Negation.inner_lt_outer :
                Position.inner < Position.outer