Documentation

Linglib.Studies.Cacchioli2026

Cacchioli 2026: the clausal prefixes of Tigrinya #

Tigrinya is head-final and yet marks its subordinate clauses with prefixes. This file formalizes the two descriptive generalizations of a thesis arguing that the position is syntactic rather than a morphological quirk: zɨ- is a reflex of successive-cyclic Ā-movement rather than a complementizer head, kɛmzɨ- is kɛm plus that reflex, so its complement clauses are relative clauses with a null nominal moved, kɨ- is a subjunctive marker heading a projection below tense, and ʔaj-…-(ɨ)n is split negation whose prefix sits below tense and whose suffix heads a polarity projection above it.

The first generalization is which verb classes take which clause-typer, the thesis's own summary table. The second is the distribution of the negative suffix, which appears exactly in the clauses whose structure reaches the polarity projection — root declaratives, ʔɨlu-complements and the negative future — and is missing wherever the clause is reduced. Both are checked against the thesis's own examples, and both are attested on each side, so neither check is vacuous.

Main definitions #

Main results #

References #

Selection #

source
inductive Cacchioli2026.VerbClass :
Type

The verb classes of the thesis's selection table (ch. 6).

Instances For
    source
    @[instance_reducible]
    instance Cacchioli2026.instDecidableEqVerbClass :
    DecidableEq VerbClass
    Equations
    source
    @[instance_reducible]
    instance Cacchioli2026.instFintypeVerbClass :
    Fintype VerbClass
    Equations
    • One or more equations did not get rendered due to their size.
    source
    def Cacchioli2026.instReprVerbClass.repr :
    VerbClass → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance Cacchioli2026.instReprVerbClass :
      Repr VerbClass
      Equations
      source
      def Cacchioli2026.selects :
      VerbClass → List Complementizer

      The clause-typers a class's complement may take.

      Equations
      Instances For
        source
        theorem Cacchioli2026.kemzi_or_ki (c : VerbClass) :
        Tigrinya.Complementizers.kemzi ∈ selects c ∨ Tigrinya.Complementizers.ki ∈ selects c

        Every class takes one of the two prefixal typers.

        source
        theorem Cacchioli2026.kemzi_of_ilu {c : VerbClass} (h : Tigrinya.Complementizers.ilu ∈ selects c) :
        Tigrinya.Complementizers.kemzi ∈ selects c

        ʔɨlu occurs only where kɛmzɨ- does.

        source
        theorem Cacchioli2026.kemzi_and_ki_iff (c : VerbClass) :
        Tigrinya.Complementizers.kemzi ∈ selects c ∧ Tigrinya.Complementizers.ki ∈ selects c ↔ c = VerbClass.fiction ∨ c = VerbClass.perception

        The two prefixes overlap exactly on fiction and perception verbs.

        source
        structure Cacchioli2026.SelectionDatum :
        Type

        A matrix verb of a given class attested with a given clause-typer.

        Instances For
          source
          @[instance_reducible]
          instance Cacchioli2026.instDecidableEqSelectionDatum :
          DecidableEq SelectionDatum
          Equations
          source
          def Cacchioli2026.instDecidableEqSelectionDatum.decEq (x✝ x✝¹ : SelectionDatum) :
          Decidable (x✝ = x✝¹)
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Cacchioli2026.instReprSelectionDatum.repr :
            SelectionDatum → ℕ → Std.Format
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[instance_reducible]
              instance Cacchioli2026.instReprSelectionDatum :
              Repr SelectionDatum
              Equations
              source
              def Cacchioli2026.selectionData :
              List SelectionDatum

              The attested (verb class, typer) pairs of the thesis's examples.

              Equations
              Instances For
                source
                theorem Cacchioli2026.selects_covers_data (d : SelectionDatum) :
                d ∈ selectionData → d.typer ∈ selects d.verbClass

                The selection table admits every attested pairing.

                source
                theorem Cacchioli2026.each_typer_attested :
                (∃ d ∈ selectionData, d.typer = Tigrinya.Complementizers.kemzi) ∧ (∃ d ∈ selectionData, d.typer = Tigrinya.Complementizers.ki) ∧ ∃ d ∈ selectionData, d.typer = Tigrinya.Complementizers.ilu

                All three typers are attested, so the coverage check has something to check.

                Sentential negation #

                source
                inductive Cacchioli2026.ClauseKind :
                Type

                The clause types in which the thesis negates a verb (ch. 5).

                Instances For
                  source
                  @[instance_reducible]
                  instance Cacchioli2026.instDecidableEqClauseKind :
                  DecidableEq ClauseKind
                  Equations
                  source
                  @[instance_reducible]
                  instance Cacchioli2026.instReprClauseKind :
                  Repr ClauseKind
                  Equations
                  source
                  def Cacchioli2026.instReprClauseKind.repr :
                  ClauseKind → ℕ → Std.Format
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Cacchioli2026.HasPolP :
                    ClauseKind → Prop

                    Clauses carrying the PolP layer that hosts -(ɨ)n: root declaratives, ʔɨlu-complements and the negative future.

                    Equations
                    Instances For
                      source
                      @[instance_reducible]
                      instance Cacchioli2026.instDecidablePredClauseKindHasPolP :
                      DecidablePred HasPolP
                      Equations
                      source
                      structure Cacchioli2026.NegationDatum :
                      Type

                      A negated clause: its kind and whether the suffix -(ɨ)n appears.

                      Instances For
                        source
                        def Cacchioli2026.instDecidableEqNegationDatum.decEq (x✝ x✝¹ : NegationDatum) :
                        Decidable (x✝ = x✝¹)
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          @[instance_reducible]
                          instance Cacchioli2026.instDecidableEqNegationDatum :
                          DecidableEq NegationDatum
                          Equations
                          source
                          @[instance_reducible]
                          instance Cacchioli2026.instReprNegationDatum :
                          Repr NegationDatum
                          Equations
                          source
                          def Cacchioli2026.instReprNegationDatum.repr :
                          NegationDatum → ℕ → Std.Format
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            def Cacchioli2026.negationData :
                            List NegationDatum

                            The negated clauses of the thesis's examples.

                            Equations
                            Instances For
                              source
                              theorem Cacchioli2026.suffix_iff_polP (d : NegationDatum) :
                              d ∈ negationData → (d.suffix = true ↔ HasPolP d.clause)

                              The suffix appears exactly in the clauses that carry PolP.

                              source
                              theorem Cacchioli2026.polP_clauses_attested :
                              { clause := ClauseKind.root, suffix := true } ∈ negationData ∧ { clause := ClauseKind.ilu, suffix := true } ∈ negationData ∧ { clause := ClauseKind.future, suffix := true } ∈ negationData

                              Every clause type the analysis gives a polarity projection is attested with the suffix, so the generalization is confirmed on both sides rather than by the absence of counterexamples.