Documentation

Linglib.Fragments.German.Determiners

German determiners #

This file defines the declensions of the German determiners and the German determiner inventory. A determiner declines for the case, number and gender of its noun, and its forms are the main way these categories are shown. A paradigm has sixteen cells, the four cases in each of the three genders of the singular and in the plural, where the genders fall together. Many determiners take one set of endings, the strong endings of dieser 'this'. The indefinite article ein, its negative kein and the possessives take them too, except in the nominative singular masculine and the nominative and accusative singular neuter, where they have none, and ein has no plural. The definite article der has forms of its own. The paradigms are Durrell's.

No paradigm distinguishes all sixteen cells. The definite article keeps the four cases apart in the masculine singular only: the nominative and the accusative fall together in the other genders and in the plural, and the genitive and the dative in the feminine singular. In the singular it keeps the three genders apart in the nominative and the accusative but not in the genitive and the dative, and that is the agreement evidence for the three-gender carrier of German.Gender.

The definite article contracts with some prepositions, im for in dem and zur for zu der. Durrell notes that the full form is used where the article is stressed, refers back to something just mentioned or has the force of a demonstrative, as in Er ging zu der Hütte 'he went to the hut (just mentioned)' against Er ging zur Hütte 'he went to the hut (we all know)'. Schwarz takes the contracted and the full form for a weak article of uniqueness and a strong article of familiarity, and Moroney classes a language by how its articles mark the two.

Main declarations #

References #

source
inductive German.Determiners.GenderNumber :
Type

A determiner agrees with its noun in a gender in the singular, and only in number in the plural, where the genders fall together.

Instances For
    source
    def German.Determiners.instDecidableEqGenderNumber.decEq (x✝ x✝¹ : GenderNumber) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[instance_reducible]
      instance German.Determiners.instDecidableEqGenderNumber :
      DecidableEq GenderNumber
      Equations
      source
      def German.Determiners.instReprGenderNumber.repr :
      GenderNumber → ℕ → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[instance_reducible]
        instance German.Determiners.instReprGenderNumber :
        Repr GenderNumber
        Equations
        source
        @[instance_reducible]
        instance German.Determiners.instFintypeGenderNumber :
        Fintype GenderNumber
        Equations

        Declensions #

        source
        def German.Determiners.strongEnding :
        GenderNumber → Case → String

        strongEnding x c is the strong ending of the cell, the ending dieser takes there.

        Equations
        Instances For
          source
          def German.Determiners.dieser (x : GenderNumber) (c : Case) :
          String

          dieser 'this' declines with the strong endings on the stem dies-, and jener 'that' declines like it.

          Equations
          Instances For
            source
            def German.Determiners.Endingless (x : GenderNumber) (c : Case) :
            Prop

            Endingless x c holds of the nominative singular masculine and the nominative and accusative singular neuter, the cells where ein, kein and the possessives have no ending.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[instance_reducible]
              instance German.Determiners.instDecidableEndingless (x : GenderNumber) (c : Case) :
              Decidable (Endingless x c)
              Equations
              • One or more equations did not get rendered due to their size.
              source
              def German.Determiners.einWord (stem : String) (x : GenderNumber) (c : Case) :
              String

              einWord stem declines an ein-word, such as kein or the possessive mein, on the stem stem, with the strong endings except in the endingless cells, where it has none.

              Equations
              Instances For
                source
                def German.Determiners.kein :
                GenderNumber → Case → String

                kein 'no' is an ein-word.

                Equations
                Instances For
                  source
                  def German.Determiners.ein :
                  GenderNumber → Case → Option String

                  The indefinite article ein is an ein-word in the singular and has no plural.

                  Equations
                  Instances For
                    source
                    def German.Determiners.definite :
                    GenderNumber → Case → String

                    definite x c is the form of the definite article in the cell.

                    Equations
                    Instances For

                      Syncretism #

                      source
                      theorem German.Determiners.injective_definite_sg_masc :
                      Function.Injective (definite (GenderNumber.sg Gender.Value.masc))

                      The masculine singular of the definite article keeps the four cases apart.

                      source
                      theorem German.Determiners.definite_nom_eq_acc_iff (x : GenderNumber) :
                      definite x Case.nom = definite x Case.acc ↔ x ≠ GenderNumber.sg Gender.Value.masc

                      The nominative and the accusative of the definite article fall together everywhere but in the masculine singular.

                      source
                      theorem German.Determiners.definite_gen_eq_dat_iff (x : GenderNumber) :
                      definite x Case.gen = definite x Case.dat ↔ x = GenderNumber.sg Gender.Value.fem

                      The genitive and the dative of the definite article fall together in the feminine singular only.

                      Gender agreement #

                      source
                      theorem German.Determiners.injective_definite_sg_nom :
                      Function.Injective fun (g : Gender.Value) => definite (GenderNumber.sg g) Case.nom

                      The nominative singular of the definite article keeps the three genders apart.

                      source
                      theorem German.Determiners.not_injective_definite_sg_dat :
                      ¬Function.Injective fun (g : Gender.Value) => definite (GenderNumber.sg g) Case.dat

                      The dative singular does not, the masculine and the neuter both being dem.

                      source
                      theorem German.Determiners.faithful :
                      Gender.Faithful fun (g : Gender.Value) => definite (GenderNumber.sg g)

                      The three-gender carrier is faithful to the definite article.

                      The inventory #

                      source
                      def German.Determiners.inventory :
                      Determiner.Inventory

                      The inventory lists the weak definite article, the form contracted with a preposition as in im; the strong definite article, the full form as in in dem; the indefinite article; the demonstrative dieser, which no longer contrasts with jener and is distance-neutral, so it covers every participant set; and the possessive mein.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        theorem German.Determiners.marking :
                        inventory.markingStrategy = Reference.MarkingStrategy.bipartite

                        German derives the .bipartite Moroney cell.