Documentation

Studies.JinKoenig2021

Jin and Koenig (2021): A Cross-Linguistic Study of Expletive Negation #

Jin and Koenig give a typology of expletive negation, a negator in the dependent of a lexical item, triggered by the item's meaning, that contributes no negation to the dependent's proposition. English, French, Januubi, Mandarin and Zarma-Sonrai share its trigger classes (ENTriggerClass). A trigger's meaning activates both its argument and the argument's negation, at distinct worlds, times or entities or within the meaning itself, (13); the substrate's operators deliver this dual inference for before, impossible and comparatives (before_dual, impossible_dual, comparative_dual), and the verbal triggers are the negative-valence attitudes and the verbs whose affirmation implies the negation of their complement (english_triggers). The paper's examples are rows whose negators are the markers of the languages' fragments, the negators the paper calls standard being the fragments' standard negators (kind_eq_standard_iff), and they carry its negator facts (mandarin_negators, french_ne_of_entrenched, januubi_maa).

Implementation notes #

References #

The dual inference (Section 5.5) #

source
def JinKoenig2021.DualInference {X : Type u_1} (p : X → Prop) :
Prop

In (13), a trigger's meaning activates its argument and the argument's negation at distinct points of a domain, worlds, times or entities.

Equations
Instances For

    Temporal operators (Section 6.2) #

    source
    theorem JinKoenig2021.before_dual {T : Type u_1} [LinearOrder T] {A B : Set (NonemptyInterval T)} (h : Tense.beforeEver A B) (hB : (Tense.timeTrace B).Nonempty) :
    DualInference fun (x : T) => x ∈ Tense.timeTrace B

    q before p says that p holds at some time and fails at the time of q, which precedes every time of p, (13b).

    Logical operators (Section 6.3) #

    source
    theorem JinKoenig2021.impossible_dual {W : Type u_1} (f g : Modality.Background W) (p : W → Prop) (w : W) (h : Modality.necessity f g (fun (w' : W) => ¬p w') w) (hb : (Modality.bestWorlds f g w).Nonempty) (hp : ∃ (x : W), p x) :
    DualInference p

    impossible p is the necessity of ¬p, so p fails at the best worlds and, if it holds anywhere, the meaning activates both, (13c).

    source
    theorem JinKoenig2021.possibility_of_not_impossible {W : Type u_1} (f g : Modality.Background W) (p : W → Prop) (w : W) (h : ¬Modality.necessity f g (fun (w' : W) => ¬p w') w) :
    Modality.possibility f g p w

    The negation of impossible p is the possibility of p.

    source
    def JinKoenig2021.withoutSem {W : Type u_1} (q p : Set W) :
    Set W

    q without p is q ∧ ¬p, the negation in the meaning, (13c).

    Equations
    Instances For
      source
      theorem JinKoenig2021.withoutSem_subset_compl {W : Type u_1} (q p : Set W) :
      withoutSem q p ⊆ pᶜ
      source
      def JinKoenig2021.unlessSem {W : Type u_1} (q p : Set W) :
      Set W

      q unless p says that if not p then q, so ¬p holds in the suppositive worlds, (13c).

      Equations
      Instances For
        source
        theorem JinKoenig2021.mem_of_mem_unlessSem {W : Type u_1} {q p : Set W} {w : W} (h : w ∈ unlessSem q p) (hp : w ∉ p) :
        w ∈ q

        Comparatives (Section 6.4) #

        source
        theorem JinKoenig2021.comparative_dual {Entity : Type u_1} {α : Type u_2} [LinearOrder α] (μ : Entity → α) (y z : Entity) (h : μ z < μ y) :
        DualInference fun (e : Entity) => μ y ≤ μ e

        Y is more Q than Z says that Y has Q to its own degree and Z does not, the two predications of (13d) over distinct entities.

        Verbal triggers #

        source
        def JinKoenig2021.IsExpletiveNegationTrigger (v : Verb) :
        Prop

        A verb triggers expletive negation (§5.5) when it is a negative-valence preferential attitude (fear) or its affirmation implies the negation of its complement (forget, prevent).

        Equations
        Instances For
          source
          @[instance_reducible]
          instance JinKoenig2021.instDecidablePredVerbIsExpletiveNegationTrigger :
          DecidablePred IsExpletiveNegationTrigger
          Equations
          • One or more equations did not get rendered due to their size.
          source
          theorem JinKoenig2021.english_triggers :
          IsExpletiveNegationTrigger English.Verbs.fear.toVerb ∧ IsExpletiveNegationTrigger English.Verbs.dread.toVerb ∧ IsExpletiveNegationTrigger English.Verbs.worry.toVerb ∧ IsExpletiveNegationTrigger English.Verbs.forget.toVerb ∧ IsExpletiveNegationTrigger English.Verbs.prevent.toVerb

          The English fragment's fear, dread, worry, forget and prevent are triggers.

          Trigger classes (Tables 5 and 6) #

          source
          inductive JinKoenig2021.ENTriggerClass :
          Type

          The trigger classes of Table 5, each named by a representative concept.

          Instances For
            source
            @[instance_reducible]
            instance JinKoenig2021.instDecidableEqENTriggerClass :
            DecidableEq ENTriggerClass
            Equations
            source
            @[instance_reducible]
            instance JinKoenig2021.instReprENTriggerClass :
            Repr ENTriggerClass
            Equations
            source
            def JinKoenig2021.instReprENTriggerClass.repr :
            ENTriggerClass → ℕ → Std.Format
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[instance_reducible]
              instance JinKoenig2021.instFintypeENTriggerClass :
              Fintype ENTriggerClass
              Equations
              • One or more equations did not get rendered due to their size.
              source
              inductive JinKoenig2021.ENConcept :
              Type

              The trigger concepts of Table 6, one representative per subclass.

              Instances For
                source
                @[instance_reducible]
                instance JinKoenig2021.instDecidableEqENConcept :
                DecidableEq ENConcept
                Equations
                source
                def JinKoenig2021.instReprENConcept.repr :
                ENConcept → ℕ → Std.Format
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[instance_reducible]
                  instance JinKoenig2021.instReprENConcept :
                  Repr ENConcept
                  Equations
                  source
                  @[instance_reducible]
                  instance JinKoenig2021.instFintypeENConcept :
                  Fintype ENConcept
                  Equations
                  • One or more equations did not get rendered due to their size.
                  source
                  def JinKoenig2021.ENConcept.cls :
                  ENConcept → ENTriggerClass

                  The class of a concept.

                  Equations
                  Instances For

                    The examples #

                    source
                    inductive JinKoenig2021.Language :
                    Type

                    The five languages of Section 4.

                    Instances For
                      source
                      @[instance_reducible]
                      instance JinKoenig2021.instDecidableEqLanguage :
                      DecidableEq Language
                      Equations
                      source
                      @[instance_reducible]
                      instance JinKoenig2021.instReprLanguage :
                      Repr Language
                      Equations
                      source
                      def JinKoenig2021.instReprLanguage.repr :
                      Language → ℕ → Std.Format
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        def JinKoenig2021.Language.standard :
                        Language → List Negation.Marker

                        The standard negators of a language, from its fragment.

                        Equations
                        Instances For
                          source
                          def JinKoenig2021.Language.negators :
                          Language → List (String × Negation.Marker)

                          The negators of a language's fragment, under the forms the rows cite them by.

                          Equations
                          Instances For
                            source
                            inductive JinKoenig2021.NegatorKind :
                            Type

                            An example uses the standard negator, a dedicated expletive negator (French ne alone), an imperative negator (Mandarin bié), a deontic one (Mandarin bùgāi) or a copular one (Zarma-Sonrai sinda).

                            Instances For
                              source
                              @[instance_reducible]
                              instance JinKoenig2021.instDecidableEqNegatorKind :
                              DecidableEq NegatorKind
                              Equations
                              source
                              def JinKoenig2021.instReprNegatorKind.repr :
                              NegatorKind → ℕ → Std.Format
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                @[instance_reducible]
                                instance JinKoenig2021.instReprNegatorKind :
                                Repr NegatorKind
                                Equations
                                source
                                structure JinKoenig2021.Row :
                                Type

                                A row records the language, the trigger concept, the negator, its kind, and for French whether the paper reports the use as entrenched.

                                Instances For
                                  source
                                  @[instance_reducible]
                                  instance JinKoenig2021.instDecidableEqRow :
                                  DecidableEq Row
                                  Equations
                                  source
                                  def JinKoenig2021.instDecidableEqRow.decEq (x✝ x✝¹ : Row) :
                                  Decidable (x✝ = x✝¹)
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    source
                                    def JinKoenig2021.languageOf :
                                    String → Option Language
                                    Equations
                                    Instances For
                                      source
                                      def JinKoenig2021.conceptOf :
                                      String → Option ENConcept
                                      Equations
                                      Instances For
                                        source
                                        def JinKoenig2021.kindOf :
                                        String → Option NegatorKind
                                        Equations
                                        Instances For
                                          source
                                          def JinKoenig2021.Row.ofDatum (e : Datum) :
                                          Option Row

                                          A row from the paper's features.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            source
                                            def JinKoenig2021.rows :
                                            List Row

                                            The examples of Sections 1, 2 and 6.

                                            Equations
                                            Instances For
                                              source
                                              theorem JinKoenig2021.isSome_ofDatum (e : Datum) :
                                              e ∈ Examples.all → (e.feature? "negator").isSome = true → (Row.ofDatum e).isSome = true

                                              Every example citing a negator is a row: its negator is one of its language's fragment.

                                              source
                                              theorem JinKoenig2021.kind_eq_standard_iff (r : Row) :
                                              r ∈ rows → (r.kind = NegatorKind.standard ↔ r.negator ∈ r.language.standard)

                                              The negators the paper calls standard are the standard negators of the fragments.

                                              source
                                              theorem JinKoenig2021.mandarin_negators (r : Row) :
                                              r ∈ rows → r.language = Language.mandarin → (r.kind = NegatorKind.imperative ↔ r.concept = ENConcept.fear) ∧ (r.kind = NegatorKind.deontic ↔ r.concept.cls = ENTriggerClass.regret)

                                              Mandarin's negator tracks the trigger, Sections 6.1.1 and 6.1.2. The imperative negator appears exactly under fear and the deontic negator exactly under the regret class.

                                              source
                                              theorem JinKoenig2021.french_ne_of_entrenched (r : Row) :
                                              r ∈ rows → r.language = Language.french → r.entrenched = some true → r.negator = French.Negation.ne

                                              French marks its entrenched uses with ne alone, Section 5.5.

                                              source
                                              theorem JinKoenig2021.januubi_maa (r : Row) :
                                              r ∈ rows → r.language = Language.januubi → r.negator = Januubi.Negation.maa

                                              Januubi's exemplified triggers, barely and before, take its standard negator maa.

                                              Blocked classes (Sections 6.4 and 7) #

                                              source
                                              inductive JinKoenig2021.ENBlockingReason :
                                              Type

                                              Why a trigger class fails to license expletive negation in a language, Section 7.

                                              • modalRestriction : ENBlockingReason

                                                The language disprefers modal operators in complement clauses.

                                              • npOnlyComplement : ENBlockingReason

                                                Comparative complements admit only noun phrases.

                                              • analyticNegation : ENBlockingReason

                                                The concept is expressed analytically with a necessary negation.

                                              Instances For
                                                source
                                                @[instance_reducible]
                                                instance JinKoenig2021.instDecidableEqENBlockingReason :
                                                DecidableEq ENBlockingReason
                                                Equations
                                                source
                                                def JinKoenig2021.instReprENBlockingReason.repr :
                                                ENBlockingReason → ℕ → Std.Format
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  source
                                                  @[instance_reducible]
                                                  instance JinKoenig2021.instReprENBlockingReason :
                                                  Repr ENBlockingReason
                                                  Equations
                                                  source
                                                  def JinKoenig2021.blocking :
                                                  Language → ENConcept → Option ENBlockingReason

                                                  A concept can fail to trigger expletive negation in a language for three reasons. Januubi admits only noun phrases as complements of comparatives and disprefers the modal that the regret class needs; Januubi, Mandarin and Zarma-Sonrai express too … to as 'too … so that … not'; and Mandarin and Zarma-Sonrai express without as 'q not p', where the negation is part of the meaning.

                                                  Equations
                                                  Instances For
                                                    source
                                                    theorem JinKoenig2021.blocking_eq_none_of_mem (r : Row) :
                                                    r ∈ rows → blocking r.language r.concept = none

                                                    No row exemplifies a class the paper reports as blocked.