Documentation

Linglib.Phenomena.Polarity.Studies.MaticNikolaeva2018

Matić & Nikolaeva (2018) @cite{matic-nikolaeva-2018} #

From polarity focus to salient polarity: From things to processes. In @cite{dimroth-sudhoff-2018}, pp. 9–53. DOI 10.1075/la.249.01mat.

The chapter argues that "polarity focus" is not a fixed form-meaning association of the kind a Lean enum can encode, and proposes the term salient polarity for the inferentially-derived interpretation that the literature has tried to denotationally pin down.

Salient polarity does not correspond to anything resembling the traditional linguistic category if the latter is understood as a pairing between a linguistic form and a denotation, but is rather to be conceived of as a fuzzy set of family resemblances unified by shared communicative intentions. — @cite{matic-nikolaeva-2018}, p. 12

This file does not formalize "salient polarity" as a predicate or function. Doing so would be the very stipulation move M&N reject — a form-class encoding masquerading as theory-neutral. Instead, the file records (a) the cross-linguistically attested list of structures ascribed to salient polarity in the literature (M&N examples 2–4, abridged), (b) the cardinality mismatch between this list and the substrate's Strategy enum, and (c) the load-bearing non-isomorphism claim that the substrate's encoding cannot capture M&N's interpretational notion.

Why this is not a "bridge file" #

Per CLAUDE.md anchoring discipline, the file is anchored on a single paper (@cite{matic-nikolaeva-2018}); the cross-framework critique is M&N's own claim, not a synthesis the formaliser invented. It lives in Studies/ exactly like every other Studies/AuthorYear.lean. The contradiction with the substrate is recorded at the substrate's def-site (Features/InformationStructure.lean::Strategy docstring) with a back-pointer here.

Cross-references #

§1 Attested salient-polarity structures (M&N examples 2–4) #

Per @cite{matic-nikolaeva-2018} pp. 13–14, the literature has ascribed salient polarity to a heterogeneous set of structures across German, English, and Serbian. The list below abridges the chapter's enumeration (M&N's own (2), (3), (4)). M&N flag this list as open-ended ("the list seems to be open" — p. 15); the constructors below are a finite proxy for argumentative purposes only.

source
inductive Phenomena.Polarity.Studies.MaticNikolaeva2018.MNAttestedStructure :
Type
  • germanAccentOnAuxiliary : MNAttestedStructure

    German: accent on auxiliary, modal, or complementizer (M&N 2a; cf. @cite{hohle-1992}, Lohnstein 2016)

  • germanAccentOnLexicalVerb : MNAttestedStructure

    German: accent on lexical finite verb (M&N 2b)

  • germanEmphaticTun : MNAttestedStructure

    German: emphatic tun periphrasis "Bücher lesen tut er" (M&N 2c)

  • germanVPFronting : MNAttestedStructure

    German: VP fronting "Bücher gelesen hat er" (M&N 2d)

  • germanAccentedDiscourseParticles : MNAttestedStructure

    German: accented discourse particles doch / schon / wohl / ja "Er ist DOCH gekommen" (M&N 2e)

  • germanDiscourseMarkers : MNAttestedStructure

    German: discourse markers ich schwöre / ehrlich / ungelogen (M&N 2f)

  • germanTruthAdverbs : MNAttestedStructure

    German: adverbs tatsächlich / wahrhaftig (M&N 2g)

  • englishAccentedAuxiliary : MNAttestedStructure

    English: accented auxiliary or modal "He WILL be on time" (M&N 3a)

  • englishAccentedLexicalVerb : MNAttestedStructure

    English: accented lexical verb "He READ it yesterday" (M&N 3b)

  • englishEmphaticDo : MNAttestedStructure

    English: emphatic do-support "She did open the door" (M&N 3c)

  • englishVPFronting : MNAttestedStructure

    English: VP fronting "He went there to learn, and learn he did" (M&N 3d)

  • englishAdverbs : MNAttestedStructure

    English: adverbs really / definitely (M&N 3e)

  • englishParticles : MNAttestedStructure

    English: particles so / too / indeed (M&N 3f)

  • englishSoInversion : MNAttestedStructure

    English: so-inversion "and so do I" (M&N 3g)

  • serbianAccentedFiniteVerb : MNAttestedStructure

    Serbian: accented finite verb "Ona PIŠE romane" (M&N 4a)

  • serbianAccentedAuxiliary : MNAttestedStructure

    Serbian: accent on auxiliary/modal "On JESTE napisao tu knjigu" (M&N 4b)

  • serbianAccentedVerbPostposedSubject : MNAttestedStructure

    Serbian: accented verb + postposed subject (M&N 4c)

  • serbianParticles : MNAttestedStructure

    Serbian: particles and adverbs stvarno / baš (M&N 4d)

Instances For
    source
    @[implicit_reducible]
    instance Phenomena.Polarity.Studies.MaticNikolaeva2018.instDecidableEqMNAttestedStructure :
    DecidableEq MNAttestedStructure
    Equations
    source
    def Phenomena.Polarity.Studies.MaticNikolaeva2018.instReprMNAttestedStructure.repr :
    MNAttestedStructure → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance Phenomena.Polarity.Studies.MaticNikolaeva2018.instReprMNAttestedStructure :
      Repr MNAttestedStructure
      Equations
      source
      def Phenomena.Polarity.Studies.MaticNikolaeva2018.mnAllStructures :
      List MNAttestedStructure
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        §2 The substrate's denotational mapping (Option-valued) #

        The substrate Strategy enum has 5 constructors. Any denotational encoding of salient polarity onto this enum must collapse M&N's 18+ attested structures into 5 buckets — necessarily many-to-one.

        The mapping below is the charitable reading of how a denotational account would assign each M&N structure to a substrate strategy. It is Option-valued: structures for which no substrate strategy gives a defensible fit return none. (.other exists in the substrate as a catch-all but using it would mask the failure; we want the non-fit to be visible at the type level. This realizes the mathlib-audit recommendation to expose the dumping-ground claim structurally rather than via a decide count.)

        source
        def Phenomena.Polarity.Studies.MaticNikolaeva2018.substrateBestEffort :
        MNAttestedStructure → Option Typology.PolarityMarking.Strategy
        Equations
        Instances For

          §2b Fragment routing — the M&N argument on actual lexical data #

          For 4 M&N structures the existing Fragment library already encodes the corresponding lexical entry. The routing below makes the M&N non-isomorphism claims indictments of actual Fragment data, not just of M&N's hand-curated symbol list. The 14 unrouted structures (German tun periphrasis, Serbian particles, English so-inversion, etc.) have no Fragment entries; for those the M&N argument runs against the substrate enum directly, in §2 above.

          source
          def Phenomena.Polarity.Studies.MaticNikolaeva2018.fromFragment :
          MNAttestedStructure → Option Typology.PolarityMarking.Entry
          Equations
          Instances For
            source
            theorem Phenomena.Polarity.Studies.MaticNikolaeva2018.substrateBestEffort_agrees_with_fragments (s : MNAttestedStructure) (e : Typology.PolarityMarking.Entry) :
            fromFragment s = some e → substrateBestEffort s = some e.strategy

            For the 4 Fragment-routable M&N structures, the Fragment's substrate strategy field agrees with substrateBestEffort. This grounds the best-effort mapping in actual data: it isn't an editorial fiction.

            §3 Non-isomorphism: the encoding is many-to-one #

            The substrate's encoding is not injective on M&N's attested-structure list — .verumFocus collects 7 cross-linguistic structures M&N treat as separate phenomena, and none collects 10 more (M&N's claim that "the grammatical category gets a blurry extension and must be continuously expanded", p. 15).

            source
            theorem Phenomena.Polarity.Studies.MaticNikolaeva2018.substrate_cannot_encode_germanEmphaticTun_and_englishVPFronting :
            substrateBestEffort MNAttestedStructure.germanEmphaticTun = none ∧ substrateBestEffort MNAttestedStructure.englishVPFronting = none

            The denotational encoding cannot place two attested structures M&N treat as substantively different (German emphatic tun and English VP fronting). Both fall outside any substrate strategy bucket.

            source
            theorem Phenomena.Polarity.Studies.MaticNikolaeva2018.fragment_data_lumps_emphaticDo_with_verumFocus :
            Fragments.English.PolarityMarking.emphaticDo.strategy = Fragments.German.PolarityMarking.verumFocus.strategy

            The substrate's .verumFocus constructor collects multiple distinct M&N structures. This is now a claim about real Fragment data: the English do-support entry (Fragments.English.PolarityMarking.emphaticDo) and the German verum-focus entry (Fragments.German.PolarityMarking.verumFocus) have the same substrate strategy field, even though M&N argue they have different distributional properties (M&N §2.2.1).

            source
            theorem Phenomena.Polarity.Studies.MaticNikolaeva2018.substrate_cannot_encode_at_least_ten :
            (List.filter (fun (s : MNAttestedStructure) => substrateBestEffort s == none) mnAllStructures).length ≥ 10

            The substrate has no defensible encoding for at least 10 of M&N's 18 attested salient-polarity structures. The substrate's catch-all .other constructor would silently absorb these, but accepting that absorption is exactly what M&N argue against (p. 15: "the grammatical category gets a blurry extension and must be continuously expanded to encompass all structures carrying the desired effect"). The Option-valued mapping makes the failure structural: there is no some _ to assign.

            §4 Open-endedness: the load-bearing claim #

            M&N's deeper argument is not just that the encoding is many-to-one — it is that the list of structures that can convey salient polarity is itself open-ended. The chapter (p. 15) explicitly notes that expressions like on the contrary, just the opposite, and complement clauses introduced with it is true that fit the standard salient- polarity diagnostics but are not in any existing typology, and concludes "the list seems to be open."

            We record M&N's three explicit witnesses as String data outside MNAttestedStructure. The inductive type cannot witness its own incompleteness — adding the three witnesses as constructors would just push the openness one step further out (M&N would point at yet another structure not in the extended type). The witness list plus the non-emptiness theorem is the substantive Lean correlate of M&N's "the list seems to be open" claim.

            source
            def Phenomena.Polarity.Studies.MaticNikolaeva2018.mnOpenEndedWitnesses :
            List String

            Three salient-polarity-conveying structures M&N (p. 15) explicitly cite as missing from existing typologies. They live as String data rather than MNAttestedStructure constructors precisely because M&N's openness argument denies that any finite enumeration closes the category.

            Equations
            Instances For
              source
              theorem Phenomena.Polarity.Studies.MaticNikolaeva2018.mn_attested_list_strictly_grows :
              mnOpenEndedWitnesses ≠ []

              The salient-polarity-conveying list M&N attests is larger than the 18-constructor MNAttestedStructure enum: at minimum, three further witnesses (M&N p. 15) can be exhibited as Strings outside the inductive type. Any finite extension of MNAttestedStructure would face the same problem. This is the operational sense in which M&N's open-endedness claim holds against any closure attempt.

              §5 Garassino & Jacob (2018, fn 13) endorsement #

              The same-volume @cite{garassino-jacob-2018} explicitly adopt M&N's salient-polarity view (their fn 13, p. 236; verbatim quote in Phenomena/Polarity/Studies/GarassinoJacob2018.lean::§4). This is a documented framework alignment within the volume itself, not the formaliser's editorial synthesis — a peer in the same edited volume reaching the same conclusion.

              §6 The argument extends to sibling frameworks #

              M&N §2 explicitly target three sibling frameworks beyond the substrate's form-class encoding. Two of them are formalized in linglib:

              Below we extend the M&N non-fit argument to both. The shared shape — each framework yields an Option-valued partial mapping from MNAttestedStructure, with the none extension counting the framework's encoding failures — could be lifted to a typeclass (FrameworkFit α := MNAttestedStructure → Option α); we keep the mappings as separate defs for now so each framework's coverage profile stays visible at the def-site.

              source
              inductive Phenomena.Polarity.Studies.MaticNikolaeva2018.RHAnalysis :
              Type

              Romero & Han's framework offers exactly one analytic option for salient polarity: the FOR-SURE-CG operator. M&N call this LOT.

              • epistemicVerum : RHAnalysis

                @cite{romero-han-2004}'s forSureCG operator analyzes the structure as expressing speaker certainty about CG-addition.

              Instances For
                source
                @[implicit_reducible]
                instance Phenomena.Polarity.Studies.MaticNikolaeva2018.instDecidableEqRHAnalysis :
                DecidableEq RHAnalysis
                Equations
                source
                @[implicit_reducible]
                instance Phenomena.Polarity.Studies.MaticNikolaeva2018.instReprRHAnalysis :
                Repr RHAnalysis
                Equations
                source
                def Phenomena.Polarity.Studies.MaticNikolaeva2018.instReprRHAnalysis.repr :
                RHAnalysis → ℕ → Std.Format
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Phenomena.Polarity.Studies.MaticNikolaeva2018.romeroHanBestEffort :
                  MNAttestedStructure → Option RHAnalysis

                  R&H's FOR-SURE-CG analysis is canonically motivated by — and arguably restricted to — accent on finite verbs / auxiliaries (the prosodic-on-finite-verb subset). For M&N's other 11 structures (periphrastic tun, VP fronting, discourse particles, inversion constructions, adverbs, …) the R&H framework is silent.

                  Equations
                  Instances For
                    source
                    theorem Phenomena.Polarity.Studies.MaticNikolaeva2018.romeroHan_cannot_encode_at_least_eleven :
                    (List.filter (fun (s : MNAttestedStructure) => romeroHanBestEffort s == none) mnAllStructures).length ≥ 11

                    R&H's FOR-SURE-CG analysis cannot encode at least 11 of M&N's 18 attested salient-polarity structures. The framework's analytic scope is the prosodic-on-finite-verb subset; everything else falls outside.

                    source
                    inductive Phenomena.Polarity.Studies.MaticNikolaeva2018.GutzmannDimension :
                    Type

                    Gutzmann 2015's UCI dimensions (DEONT/EPIS/HKNOW). The 2015 framework is about sentence-mood operators, not polarity-marking devices; M&N's specific Gutzmann target is Gutzmann & Castroviejo Miró 2011 ("a kind of conversational operator"), which is not formalized in linglib.

                    Instances For
                      source
                      @[implicit_reducible]
                      instance Phenomena.Polarity.Studies.MaticNikolaeva2018.instDecidableEqGutzmannDimension :
                      DecidableEq GutzmannDimension
                      Equations
                      source
                      def Phenomena.Polarity.Studies.MaticNikolaeva2018.instReprGutzmannDimension.repr :
                      GutzmannDimension → ℕ → Std.Format
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        @[implicit_reducible]
                        instance Phenomena.Polarity.Studies.MaticNikolaeva2018.instReprGutzmannDimension :
                        Repr GutzmannDimension
                        Equations
                        source
                        def Phenomena.Polarity.Studies.MaticNikolaeva2018.gutzmannBestEffort :
                        MNAttestedStructure → Option GutzmannDimension

                        Gutzmann 2015's sentence-mood UCIs do not analyze polarity-marking structures: the framework's scope is clause-type composition (V2/VL/imperative declaratives, interrogatives), not the prosodic / particle / construction inventory M&N enumerate. The constant-none encoding records that the framework simply does not extend. The shared verum-related Gutzmann critique M&N actually engage (Gutzmann & Castroviejo Miró 2011) is not in linglib's substrate.

                        Equations
                        Instances For
                          source
                          theorem Phenomena.Polarity.Studies.MaticNikolaeva2018.gutzmann_2015_framework_does_not_apply (s : MNAttestedStructure) :
                          gutzmannBestEffort s = none

                          Gutzmann 2015's sentence-mood framework cannot analyze any of M&N's 18 attested salient-polarity structures — the framework scopes over clause types, not polarity-marking devices. Vacuous coverage, recorded structurally.

                          source
                          theorem Phenomena.Polarity.Studies.MaticNikolaeva2018.mn_argument_extends_across_frameworks :
                          (List.filter (fun (s : MNAttestedStructure) => substrateBestEffort s == none) mnAllStructures).length ≥ 10 ∧ (List.filter (fun (s : MNAttestedStructure) => romeroHanBestEffort s == none) mnAllStructures).length ≥ 11 ∧ (List.filter (fun (s : MNAttestedStructure) => gutzmannBestEffort s == none) mnAllStructures).length = 18

                          The M&N argument is universal: at least 10 attested structures fall outside the substrate enum, at least 11 fall outside R&H's FOR-SURE-CG, and all 18 fall outside Gutzmann 2015's sentence-mood UCIs. The structures inside the intersection of all three frameworks — the canonical prosodic verum focus on finite verbs — are exactly the cases all four traditions agree about; the disagreement is entirely about what else counts.