Documentation

Linglib.Theories.Syntax.Minimalism.Polarity

Syntactic Polarity: PolP and [±Pol] #

@cite{holmberg-2016} @cite{laka-1990}

Syntactic polarity as a formal feature on the PolP functional head, connecting @cite{laka-1990}'s ΣP and @cite{holmberg-2016}'s analysis of yes/no answers.

Key Claims #

  1. Every finite clause has a polarity head (Pol⁰) projecting PolP in the IP domain
  2. In declaratives, [±Pol] is valued: [+Pol] for affirmative, [-Pol] for negative
  3. In polar questions, [±Pol] is unvalued — the answer values it
  4. "Yes"/"No" are focus-movement remnants of PolP ellipsis under identity

Connection to Core.Polarity #

Core.Polarity provides the semantic type (.positive / .negative). This file provides the syntactic feature [±Pol] that participates in Agree and maps to Core.Polarity at LF.

Connection to Cat.Pol #

Minimalism.Cat.Pol is the categorial label for the polarity head. This file adds the feature infrastructure for what that head carries.

source
inductive Minimalism.Polarity.PolFeature :
Type

The polarity feature on Pol⁰, which may be valued or unvalued.

In declaratives: valued [+Pol] or [-Pol] In polar questions: unvalued [uPol] — waiting for an answer to value it

  • valued : Core.Polarity → PolFeature

    Valued polarity: [+Pol] (affirmative) or [-Pol] (negative)

  • unvalued : PolFeature

    Unvalued polarity: the feature in polar questions that the answer resolves

Instances For
    source
    def Minimalism.Polarity.instDecidableEqPolFeature.decEq (x✝ x✝¹ : PolFeature) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      instance Minimalism.Polarity.instDecidableEqPolFeature :
      DecidableEq PolFeature
      Equations
      source
      instance Minimalism.Polarity.instReprPolFeature :
      Repr PolFeature
      Equations
      source
      def Minimalism.Polarity.instReprPolFeature.repr :
      PolFeature → ℕ → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        instance Minimalism.Polarity.instBEqPolFeature :
        BEq PolFeature
        Equations
        source
        def Minimalism.Polarity.instBEqPolFeature.beq :
        PolFeature → PolFeature → Bool
        Equations
        Instances For
          source
          def Minimalism.Polarity.PolFeature.toFeatureVal :
          PolFeature → GramFeature

          Convert a PolFeature to a FeatureVal for use in the Agree system. [+Pol] maps to .pol true, [-Pol] maps to .pol false.

          Equations
          Instances For
            source
            def Minimalism.Polarity.PolFeature.toPolarity :
            PolFeature → Option Core.Polarity

            Recover Core.Polarity from a valued syntactic [±Pol] feature.

            Equations
            Instances For
              source
              structure Minimalism.Polarity.PolHead :
              Type

              A Pol⁰ head: the functional head projecting PolP.

              In @cite{holmberg-2016}'s analysis, every finite clause has a Pol⁰ bearing a [±Pol] feature. The head's category is Cat.Pol.

              • feature : PolFeature

                The polarity feature on this head

              • inQuestion : Bool

                Is this in a question context (unvalued [±Pol])?

              Instances For
                source
                def Minimalism.Polarity.instReprPolHead.repr :
                PolHead → ℕ → Std.Format
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  instance Minimalism.Polarity.instReprPolHead :
                  Repr PolHead
                  Equations
                  source
                  def Minimalism.Polarity.PolHead.affirmative :
                  PolHead

                  An affirmative declarative Pol⁰: [+Pol]

                  Equations
                  Instances For
                    source
                    def Minimalism.Polarity.PolHead.negative :
                    PolHead

                    A negative declarative Pol⁰: [-Pol]

                    Equations
                    Instances For
                      source
                      def Minimalism.Polarity.PolHead.question :
                      PolHead

                      A polar question Pol⁰: [uPol]

                      Equations
                      Instances For
                        source
                        def Minimalism.Polarity.PolFeature.value (f : PolFeature) (p : Core.Polarity) :
                        Option PolFeature

                        Value an unvalued [±Pol] feature — the core operation in answering a polar question. The answer provides a Core.Polarity that values the feature.

                        Returns none if the feature is already valued (nothing to do).

                        Equations
                        Instances For
                          source
                          theorem Minimalism.Polarity.value_unvalued (p : Core.Polarity) :
                          PolFeature.unvalued.value p = some (PolFeature.valued p)

                          Valuing an unvalued feature always succeeds.

                          source
                          theorem Minimalism.Polarity.value_valued (p q : Core.Polarity) :
                          (PolFeature.valued p).value q = none

                          Valuing a valued feature always fails.

                          source
                          theorem Minimalism.Polarity.value_then_toPolarity (p : Core.Polarity) :
                          (PolFeature.unvalued.value p).bind PolFeature.toPolarity = some p

                          Round-trip: valuing then extracting polarity recovers the answer.

                          source
                          theorem Minimalism.Polarity.pol_feature_matches :
                          (FeatureVal.pol true).sameType (FeatureVal.pol false) = true

                          The [±Pol] feature matches itself in the Agree system.

                          source
                          theorem Minimalism.Polarity.pol_ne_neg :
                          (FeatureVal.pol true).sameType (FeatureVal.neg true) = false

                          [±Pol] is distinct from [±neg]: polarity and negation are separate features on separate heads (PolP vs NegP).