Documentation

Studies.HarleyRitter2002

Harley and Ritter (2002): Person and number in pronouns #

This file formalizes [HR02]'s feature geometry for the person and number of pronouns: Participant with its dependents Speaker and Addressee, Individuation with Group, Minimal and Minimal's dependent Augmented, and a pronoun's content a subtree containing the root, so that a complex geometry implies its simpler subgeometries. The inventory each of the nine languages activates is read off its pronoun table (active_of_rows); every attested cell is licensed by its language's inventory and distinct cells receive distinct geometries (licenses_rows); and the person-only languages Pirahã, Maxakalí and Kwakiutl realize exactly the geometries their inventories license, at most four first- and second-person pronouns (person_only_exhaust). Pruning a dependent from a licensed geometry leaves a licensed geometry, whence the implicational universals of (18), no dual without plural, no paucal without dual, no inclusive without second person (dual_needs_plural and its siblings), and Greenberg's Universals 37 and 45 on gender; Universal 36, gender implies number, is the dependency of Class on Individuation. Markedness is node count and acquisition builds structure top-down, so third person is least marked, the Fijian first inclusive paucal uses all eight nodes, and first person precedes second and singular plural (20).

Implementation notes #

The pronoun tables (Tables 3–8 and 13–15) are the rows of Data/Examples/HarleyRitter2002.json, read off by the tables' person and number labels; the inventories of (12)–(17), (25) and (27) are stated as Lang.active and then shown to be what the rows determine. The default Speaker and Minimal nodes do not count toward markedness, so the Daga first singular is less marked than the first plural.

References #

Languages and their inventories #

source
inductive HarleyRitter2002.Lang :
Type

The languages of §2.3–2.8 and §4.

Instances For
    source
    @[instance_reducible]
    instance HarleyRitter2002.instDecidableEqLang :
    DecidableEq Lang
    Equations
    source
    @[instance_reducible]
    instance HarleyRitter2002.instReprLang :
    Repr Lang
    Equations
    source
    def HarleyRitter2002.instReprLang.repr :
    Lang → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance HarleyRitter2002.instFintypeLang :
      Fintype Lang
      Equations
      source
      def HarleyRitter2002.Lang.ofGlottocode :
      String → Option Lang

      The language of a pool row, by Glottocode.

      Equations
      Instances For
        source
        def HarleyRitter2002.Lang.active :
        Lang → Finset Phi.Geometry.Node

        The nodes each language activates ((12)–(17), (25), (27)): Speaker is contrastive where there is an inclusive, Minimal where there is a dual, Augmented where there is a paucal; the person-only languages activate no Individuation.

        Equations
        Instances For
          source
          theorem HarleyRitter2002.active_isLowerSet (l : Lang) :
          IsLowerSet ↑l.active

          The pronoun tables #

          source
          structure HarleyRitter2002.Row :
          Type

          A pronoun of the tables: its language, cell, and form.

          Instances For
            source
            def HarleyRitter2002.instDecidableEqRow.decEq (x✝ x✝¹ : Row) :
            Decidable (x✝ = x✝¹)
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[instance_reducible]
              instance HarleyRitter2002.instDecidableEqRow :
              DecidableEq Row
              Equations
              source
              def HarleyRitter2002.instReprRow.repr :
              Row → ℕ → Std.Format
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[instance_reducible]
                instance HarleyRitter2002.instReprRow :
                Repr Row
                Equations
                source
                def HarleyRitter2002.personOfLabel :
                String → Option Person

                The person of a pool row, by the tables' labels.

                Equations
                Instances For
                  source
                  def HarleyRitter2002.numberOfLabel :
                  String → Option Number

                  The number of a pool row, by the tables' labels; none is number-neutral.

                  Equations
                  Instances For
                    source
                    def HarleyRitter2002.Row.ofDatum (ex : Datum) :
                    Option Row

                    Read a row off a pool example.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      theorem HarleyRitter2002.row_ofDatum_isSome (ex : Datum) :
                      ex ∈ Examples.all → (Row.ofDatum ex).isSome = true
                      source
                      def HarleyRitter2002.rows :
                      List Row

                      The pronouns of Tables 3–8 and 13–15.

                      Equations
                      Instances For
                        source
                        def HarleyRitter2002.Lang.rows (l : Lang) :
                        List Row

                        A language's pronouns.

                        Equations
                        Instances For
                          source
                          def HarleyRitter2002.Row.cell (r : Row) :
                          Option (Finset Phi.Geometry.Node)

                          The geometry of a row's cell in its language.

                          Equations
                          Instances For
                            source
                            theorem HarleyRitter2002.licenses_rows (r : Row) :
                            r ∈ rows → Phi.Geometry.Licenses r.lang.active r.person r.number

                            Every attested cell is licensed by its language's inventory.

                            source
                            theorem HarleyRitter2002.active_of_rows (l : Lang) :
                            (Phi.Geometry.Node.addressee ∈ l.active ↔ ∃ r ∈ l.rows, r.person = Person.second) ∧ (Phi.Geometry.Node.speaker ∈ l.active ↔ ∃ r ∈ l.rows, r.person = Person.firstInclusive) ∧ (Phi.Geometry.Node.minimal ∈ l.active ↔ ∃ r ∈ l.rows, r.number = Number.dual) ∧ (Phi.Geometry.Node.augmented ∈ l.active ↔ ∃ r ∈ l.rows, r.number = Number.paucal) ∧ (Phi.Geometry.Node.individuation ∈ l.active ↔ ∃ r ∈ l.rows, ∃ s ∈ l.rows, r.person = s.person ∧ r.number ≠ s.number)

                            The inventory is read off the paradigm (§2.4, §3): Addressee is active iff there is a second person, Speaker iff an inclusive, Minimal iff a dual, Augmented iff a paucal, and Individuation iff some person distinguishes numbers — which the person-only languages do not.

                            source
                            theorem HarleyRitter2002.cell_nodup (l : Lang) :
                            (List.map Row.cell l.rows).Nodup

                            Within a language, distinct cells receive distinct geometries.

                            source
                            theorem HarleyRitter2002.person_only_exhaust (l : Lang) :
                            l ∈ [Lang.piraha, Lang.maxakali, Lang.kwakiutl] → (List.filterMap Row.cell l.rows).toFinset = l.active.lowerSubsets.erase ∅

                            The person-only languages realize every nonempty lower subset of their inventory and nothing else (§4, (25), (27)).

                            source
                            theorem HarleyRitter2002.card_participant_geometries :
                            {x ∈ Lang.maxakali.active.lowerSubsets | Phi.Geometry.Node.participant ∈ x}.card = 4

                            A language using only the Participant node has four geometries with it ((26)): no such language has more than four first- and second-person pronouns.

                            Complex geometries imply simpler ones (§2.10, §6.1) #

                            source
                            theorem HarleyRitter2002.cell_plural_eq (A : Finset Phi.Geometry.Node) (p : Person) :
                            Phi.Geometry.cell A p Number.plural = Option.map (fun (x : Finset Phi.Geometry.Node) => {b ∈ x | ¬Phi.Geometry.Node.minimal ≤ b}) (Phi.Geometry.cell A p Number.dual)

                            Plural is dual with Minimal pruned ((32a)).

                            source
                            theorem HarleyRitter2002.cell_singular_eq {A : Finset Phi.Geometry.Node} (h : Phi.Geometry.Node.minimal ∈ A) (p : Person) :
                            Phi.Geometry.cell A p Number.singular = Option.map (fun (x : Finset Phi.Geometry.Node) => {b ∈ x | ¬Phi.Geometry.Node.group ≤ b}) (Phi.Geometry.cell A p Number.dual)

                            Singular is dual with Group pruned, in an inventory with a contrastive Minimal ((32a)).

                            source
                            theorem HarleyRitter2002.cell_dual_eq (A : Finset Phi.Geometry.Node) (p : Person) :
                            Phi.Geometry.cell A p Number.dual = Option.map (fun (x : Finset Phi.Geometry.Node) => {b ∈ x | ¬Phi.Geometry.Node.augmented ≤ b}) (Phi.Geometry.cell A p Number.paucal)

                            Dual is paucal with Augmented pruned.

                            source
                            theorem HarleyRitter2002.cell_second_eq (A : Finset Phi.Geometry.Node) (n : Number) :
                            Phi.Geometry.cell A Person.second n = Option.map (fun (x : Finset Phi.Geometry.Node) => {b ∈ x | ¬Phi.Geometry.Node.speaker ≤ b}) (Phi.Geometry.cell A Person.firstInclusive n) ∧ Phi.Geometry.cell A Person.firstExclusive n = Option.map (fun (x : Finset Phi.Geometry.Node) => {b ∈ x | ¬Phi.Geometry.Node.addressee ≤ b}) (Phi.Geometry.cell A Person.firstInclusive n)

                            Second person is inclusive with Speaker pruned, exclusive inclusive with Addressee pruned ((32b)).

                            source
                            theorem HarleyRitter2002.licenses_of_map_filter {A : Finset Phi.Geometry.Node} {p : Person} {n n' : Number} {p' : Person} {a : Phi.Geometry.Node} (h : Phi.Geometry.cell A p' n' = Option.map (fun (x : Finset Phi.Geometry.Node) => {b ∈ x | ¬a ≤ b}) (Phi.Geometry.cell A p n)) (hl : Phi.Geometry.Licenses A p n) :
                            Phi.Geometry.Licenses A p' n'
                            source
                            theorem HarleyRitter2002.dual_needs_plural {A : Finset Phi.Geometry.Node} {p : Person} (h : Phi.Geometry.Licenses A p Number.dual) :
                            Phi.Geometry.Licenses A p Number.plural

                            (18a) No dual without plural.

                            source
                            theorem HarleyRitter2002.paucal_needs_dual {A : Finset Phi.Geometry.Node} {p : Person} (h : Phi.Geometry.Licenses A p Number.paucal) :
                            Phi.Geometry.Licenses A p Number.dual

                            (18b) No paucal without dual.

                            source
                            theorem HarleyRitter2002.inclusive_needs_second {A : Finset Phi.Geometry.Node} {n : Number} (h : Phi.Geometry.Licenses A Person.firstInclusive n) :
                            Phi.Geometry.Licenses A Person.second n ∧ Phi.Geometry.Licenses A Person.firstExclusive n

                            (18c) No inclusive without second person — nor without exclusive.

                            Gender (§6.3) #

                            source
                            theorem HarleyRitter2002.gender_needs_number {A : Finset Phi.Geometry.Node} (hA : IsLowerSet ↑A) (h : Phi.Geometry.Node.nounClass ∈ A) :
                            Phi.Geometry.Node.individuation ∈ A

                            Universal 36: gender implies number — Class depends on Individuation.

                            source
                            theorem HarleyRitter2002.gendered_plural_needs_gendered_singular {A g : Finset Phi.Geometry.Node} (hg : g ∈ A.lowerSubsets) (hc : Phi.Geometry.Node.nounClass ∈ g) :
                            {b ∈ g | ¬Phi.Geometry.Node.group ≤ b} ∈ A.lowerSubsets ∧ Phi.Geometry.Node.nounClass ∈ {b ∈ g | ¬Phi.Geometry.Node.group ≤ b} ∧ Phi.Geometry.Node.group ∉ {b ∈ g | ¬Phi.Geometry.Node.group ≤ b}

                            Universals 37 and 45: a gendered geometry with Group prunes to a gendered one without, so gender in the plural implies gender in the singular.

                            source
                            theorem HarleyRitter2002.no_gender_only_in_plural {A : Finset Phi.Geometry.Node} (hall : ∀ g ∈ A.lowerSubsets, Phi.Geometry.Node.nounClass ∈ g → Phi.Geometry.Node.group ∈ g) (g : Finset Phi.Geometry.Node) :
                            g ∈ A.lowerSubsets → Phi.Geometry.Node.nounClass ∉ g

                            The system (45) — gender only in nonsingular numbers — is impossible: an inventory whose every gendered geometry has Group has no gendered geometry.

                            Markedness (§1.3, §2.3) #

                            source
                            theorem HarleyRitter2002.third_least_marked {A : Finset Phi.Geometry.Node} {p : Person} {n : Number} {g g' : Finset Phi.Geometry.Node} (h : Phi.Geometry.cell A Person.third n = some g) (h' : Phi.Geometry.cell A p n = some g') :
                            g ⊆ g'

                            Third person is the least marked: its geometry lies within every other person's in the same number.

                            source
                            theorem HarleyRitter2002.daga_first_singular_lt_plural (g : Finset Phi.Geometry.Node) :
                            g ∈ Phi.Geometry.cell Lang.daga.active Person.first Number.singular → ∀ g' ∈ Phi.Geometry.cell Lang.daga.active Person.first Number.plural, g.card < g'.card

                            In Daga, the first singular is less marked than the first plural — the default Speaker and Minimal nodes are not counted (§2.3).

                            source
                            theorem HarleyRitter2002.fijian_inclusive_paucal :
                            Phi.Geometry.cell Lang.fijian.active Person.firstInclusive Number.paucal = some Lang.fijian.active ∧ Lang.fijian.active.card = 8

                            The most marked pronoun, the Fijian first inclusive paucal, uses all eight person–number nodes (§2.8).

                            Acquisition (§3) #

                            source
                            theorem HarleyRitter2002.first_before_second {A : Finset Phi.Geometry.Node} {n : Number} (g : Finset Phi.Geometry.Node) :
                            g ∈ Phi.Geometry.cell A Person.first n → ∀ g' ∈ Phi.Geometry.cell A Person.second n, g ⊂ g'

                            First person is acquired before second: its geometry is a proper part ((20a-ii)).

                            source
                            theorem HarleyRitter2002.singular_before_plural {A : Finset Phi.Geometry.Node} {p : Person} (hm : Phi.Geometry.Node.minimal ∉ A) (hi : Phi.Geometry.Node.individuation ∈ A) (g : Finset Phi.Geometry.Node) :
                            g ∈ Phi.Geometry.cell A p Number.singular → ∀ g' ∈ Phi.Geometry.cell A p Number.plural, g ⊂ g'

                            Singular is acquired before plural where Minimal is a default ((20a-iii)).

                            source
                            theorem HarleyRitter2002.second_third_plural_incomparable (g : Finset Phi.Geometry.Node) :
                            g ∈ Phi.Geometry.cell Lang.daga.active Person.second Number.singular → ∀ g' ∈ Phi.Geometry.cell Lang.daga.active Person.third Number.plural, ¬g ⊆ g' ∧ ¬g' ⊆ g

                            Second person and third plural are incomparable, so their order varies ((20b)).

                            Empty paradigm space (§4.1) #

                            source
                            theorem HarleyRitter2002.maxakali_coopts (g : Finset Phi.Geometry.Node) :
                            g ∈ Phi.Geometry.cell Lang.maxakali.active Person.first Number.singular → ∀ g' ∈ Phi.Geometry.cell Lang.maxakali.active Person.firstExclusive Number.plural, g ≠ g' ∧ Phi.Geometry.fillDefaults g = Phi.Geometry.fillDefaults g'

                            Maxakalí's first singular, the bare Participant node, and its first exclusive plural, Participant with Speaker, fill to the same content by the Speaker default yet are distinct geometries — the exclusive plural co-opts the representation the contrastive Speaker makes available ((27)).