Documentation

Studies.Chierchia1998

Chierchia (1998): Reference to kinds across languages #

Chierchia's Nominal Mapping Parameter sets whether a language's nouns denote kinds, predicates, or either: Chinese and Japanese are [+arg, −pred], the Romance languages [−arg, +pred], and English [+arg, +pred]. In a [+arg, −pred] language every noun denotes a kind, so its extension is mass and a numeral needs a classifier. A language's determiners decide which covert type shifts it blocks, and with the parameter which bare nominals it admits as arguments. A bare plural denotes its kind, whose instances meet the existential of derived kind predication in an episodic sentence and the generic operator in a generic one. A kind sends each situation to a partial individual, ∩ takes the largest member of a property's extension (Reference.iota of IsGreatest) where the result is a kind, and ∪ takes the parts of a kind's value (Set.Iic).

Main definitions #

Main results #

Implementation notes #

Each language's blocking is derived from its fragment's determiner inventory by Determiner.Inventory.Blocks. The generic operator is the conditional over the normal cases of a Genericity.Normality. The set K of kinds is a parameter, primitive as in the paper, and its one stated property, that no kind has a singular instance in every situation, is a hypothesis.

References #

source
inductive Chierchia1998.Language :
Type

The sample covers five of the languages the paper discusses.

Instances For
    source
    @[instance_reducible]
    instance Chierchia1998.instDecidableEqLanguage :
    DecidableEq Language
    Equations
    source
    @[instance_reducible]
    instance Chierchia1998.instFintypeLanguage :
    Fintype Language
    Equations
    • One or more equations did not get rendered due to their size.
    source
    def Chierchia1998.Language.nominalMapping :
    Language → Genericity.NominalMapping

    nominalMapping l is the setting of the Nominal Mapping Parameter in l.

    Equations
    Instances For
      source
      def Chierchia1998.Language.determiners :
      Language → Determiner.Inventory

      determiners l is the determiner inventory of the fragment of l.

      Equations
      Instances For
        source
        def Chierchia1998.Language.HasClassifiers :
        Language → Prop

        The language has numeral classifiers, as its fragment records for Mandarin and Japanese; the Romance languages and English have none.

        Equations
        Instances For
          source
          theorem Chierchia1998.hasClassifiers_iff (l : Language) :
          l.HasClassifiers ↔ l.nominalMapping = Genericity.NominalMapping.argOnly

          A [+arg, −pred] language has a generalized classifier system, and a classifier language must be [+arg, −pred]: the classifier languages of the sample are exactly the [+arg, −pred] ones.

          Kind formation, §2 #

          ∩ takes a property to the individual concept that picks out the largest member of its extension at each situation, where that concept is a kind, (16), and is undefined otherwise. A kind cannot have a singular instance in every situation (p. 351), so ∩ is undefined for a singular property, which is true of atoms only. A plural is true of the pluralities of its singular, (10a), and a mass noun comes out of the lexicon already pluralized, closed under sum (p. 347); where such an extension is finite and has a plurality, its largest member is that plurality or above it, so its concept passes the condition (pp. 351 and 357).

          source
          theorem Chierchia1998.iota_isGreatest_notMem_of_atom {S : Type u_1} {E : Type u_2} {K : Set (S → Option E)} {P : S → Set E} [PartialOrder E] (hK : ∀ k ∈ K, ¬∀ (s : S), ∀ d ∈ k s, Mereology.Atom d) (hP : ∀ (s : S), ∀ x ∈ P s, Mereology.Atom x) :
          (fun (s : S) => Reference.iota (IsGreatest (P s))) ∉ K

          ∩ is undefined for a singular property: its concept is singular in every situation, and no kind is.

          source
          theorem Chierchia1998.not_forall_atom_iota_isGreatest {S : Type u_1} {E : Type u_2} {P : S → Set E} [SemilatticeSup E] {s : S} {x : E} (hfin : (P s).Finite) (hcum : SupClosed (P s)) (hx : x ∈ P s) (hx0 : ¬IsBot x) (hxa : ¬Mereology.Atom x) :
          ¬∀ (s : S), ∀ d ∈ Reference.iota (IsGreatest (P s)), Mereology.Atom d

          The concept of a property closed under sum is not singular in every situation once its extension somewhere is finite and has a plurality.

          Bare arguments and type-shift blocking #

          The determiner inventory of each sampled language decides by the Blocking Principle which covert shifts it blocks, and with the mapping which bare nominals it admits as arguments (NominalMapping.LicensesBare), given whether ∩ is defined for the nominal.

          source
          theorem Chierchia1998.argOnly_blocks_nothing (l : Language) :
          l.nominalMapping = Genericity.NominalMapping.argOnly → ¬l.determiners.Blocks Genericity.CovertShift.iota ∧ ¬l.determiners.Blocks Genericity.CovertShift.exists

          A [+arg, −pred] language has no articles and so blocks neither ι nor ∃, and ∩ is never blocked: all three of Chierchia's shifts are available to Mandarin and Japanese bare nouns.

          source
          theorem Chierchia1998.argOnly_licensesBare (down : Prop) :
          Language.mandarin.nominalMapping.LicensesBare Language.mandarin.determiners down ∧ Language.japanese.nominalMapping.LicensesBare Language.japanese.determiners down

          Mandarin and Japanese admit every bare nominal as an argument.

          source
          theorem Chierchia1998.predOnly_blocks_iota (l : Language) :
          l.nominalMapping = Genericity.NominalMapping.predOnly → l.determiners.Blocks Genericity.CovertShift.iota

          The [−arg, +pred] languages of the sample have a definite article and so block ι.

          source
          theorem Chierchia1998.predOnly_not_licensesBare (down : Prop) :
          ¬Language.french.nominalMapping.LicensesBare Language.french.determiners down ∧ ¬Language.italian.nominalMapping.LicensesBare Language.italian.determiners down

          French and Italian admit no bare nominal as an argument, since their nouns need D.

          source
          theorem Chierchia1998.english_licensesBare_iff (down : Prop) :
          Language.english.nominalMapping.LicensesBare Language.english.determiners down ↔ down

          English, [+arg, +pred] with the and a blocking ι and ∃, admits exactly the bare nominals kind formation is defined for.

          source
          theorem Chierchia1998.english_not_licensesBare_singular {S : Type u_1} {E : Type u_2} [PartialOrder E] {K : Set (S → Option E)} {P : S → Set E} (hK : ∀ k ∈ K, ¬∀ (s : S), ∀ d ∈ k s, Mereology.Atom d) (hP : ∀ (s : S), ∀ x ∈ P s, Mereology.Atom x) :
          ¬Language.english.nominalMapping.LicensesBare Language.english.determiners ((fun (s : S) => Reference.iota (IsGreatest (P s))) ∈ K)

          English admits no bare singular count noun, (24b), since ∩ is undefined for it.

          Bare plurals in generic and episodic sentences, §4.1 #

          source
          def Chierchia1998.dogsBark {S : Type u_1} {E : Type u_2} [PartialOrder E] (N : Genericity.Normality S (E × S)) (dog : S → Set E) (C : Set (E × S)) (bark : E → S → Prop) :
          Set S

          Dogs bark (38b), Gn x, s [∪∩dog(x) ∧ C(x, s)] [bark(x, s)], puts the instances of the kind in the restriction of the generic operator, which binds them with the situations.

          Equations
          Instances For
            source
            def Chierchia1998.computersRoute {S : Type u_1} {E : Type u_2} [PartialOrder E] (N : Genericity.Normality S (E × S)) (computer plane : S → Set E) (C : Set (E × S)) (route : E → E → S → Prop) :
            Set S

            In Computers route modern planes (39b), the object is fronted into the restriction of the generic operator and the subject is reconstructed into its scope, where derived kind predication reads it existentially.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem Chierchia1998.mem_computersRoute {S : Type u_1} {E : Type u_2} [PartialOrder E] {N : Genericity.Normality S (E × S)} {computer plane : S → Set E} {C : Set (E × S)} {route : E → E → S → Prop} {s : S} :
              s ∈ computersRoute N computer plane C route ↔ ∀ p ∈ N.normal s ({p : E × S | p.1 ∈ (Reference.iota (IsGreatest (plane p.2))).elim ∅ Set.Iic} ∩ C), ∃ x ∈ (Reference.iota (IsGreatest (computer p.2))).elim ∅ Set.Iic, route x p.1 p.2

              In (39b) the fronted bare plural is universal over the normal cases of the restriction, and the one in the scope is existential over the instances of its kind at each, as Diesing's generalization predicts (p. 368).

              source
              theorem Chierchia1998.some_up_of_mem_dogsBark {S : Type u_1} {E : Type u_2} [PartialOrder E] {N : Genericity.Normality S (E × S)} {dog : S → Set E} {C : Set (E × S)} {bark : E → S → Prop} {s s' : S} {x : E} (h : s ∈ dogsBark N dog C bark) (hx : (x, s') ∈ N.normal s ({p : E × S | p.1 ∈ (Reference.iota (IsGreatest (dog p.2))).elim ∅ Set.Iic} ∩ C)) :
              Quantifier.GQ.some ((Reference.iota (IsGreatest (dog s'))).elim ∅ Set.Iic) fun (x : E) => bark x s'

              The generic reading of a bare plural, (38b), entails its episodic reading by derived kind predication, (31c), at any situation where the kind has a normal instance: if dogs bark, then some dog barks wherever a normal dog is.