Cacchioli (2026): The Syntax of Clausal Prefixes in 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

• VerbClass, selects — the verb classes and the clause-typers each admits
• ClauseKind, HasPolP — the clause types and which of them carry the polarity projection

Main results

• kemzi_or_ki, kemzi_of_ilu, kemzi_and_ki_iff — the shape of the selection table: every class takes one of the two prefixes, ʔɨlu occurs only where kɛmzɨ- does, and the two prefixes overlap on the fiction and perception verbs alone
• selects_covers_data, each_typer_attested — the table admits every attested pairing, and each typer is attested
• suffix_iff_polP, polP_clauses_attested — the suffix of the Tigrinya fragment's circumfix, read off each example's negative word, appears exactly in the clauses carrying the polarity projection, and every such clause type is attested with it
• variants_ungrammatical — the starred variants are those that break the generalization

References

• [Cac26]
• [Cac23]

Selection

inductive Cacchioli2026.VerbClass : Type

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

• factive : VerbClass
• cognitiveNonFactive : VerbClass
• fiction : VerbClass
• utterance : VerbClass
• perception : VerbClass
• directive : VerbClass
• desire : VerbClass
• modal : VerbClass
• emotiveFactive : VerbClass
• control : VerbClass
• ecm : VerbClass

@[instance_reducible]

instance Cacchioli2026.instDecidableEqVerbClass : DecidableEq VerbClass

Equations

• Cacchioli2026.instDecidableEqVerbClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cacchioli2026.instFintypeVerbClass : Fintype VerbClass

Equations

• One or more equations did not get rendered due to their size.

def Cacchioli2026.instReprVerbClass.repr : VerbClass → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Cacchioli2026.instReprVerbClass : Repr VerbClass

Equations

• Cacchioli2026.instReprVerbClass = { reprPrec := Cacchioli2026.instReprVerbClass.repr }

def Cacchioli2026.selects : VerbClass → List Complementizer

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

Equations

• Cacchioli2026.selects Cacchioli2026.VerbClass.factive = [Tigrinya.Complementizers.kemzi]
• Cacchioli2026.selects Cacchioli2026.VerbClass.cognitiveNonFactive = [Tigrinya.Complementizers.kemzi, Tigrinya.Complementizers.ilu]
• Cacchioli2026.selects Cacchioli2026.VerbClass.utterance = [Tigrinya.Complementizers.kemzi, Tigrinya.Complementizers.ilu]
• Cacchioli2026.selects Cacchioli2026.VerbClass.fiction = [Tigrinya.Complementizers.kemzi, Tigrinya.Complementizers.ki, Tigrinya.Complementizers.ilu]
• Cacchioli2026.selects Cacchioli2026.VerbClass.perception = [Tigrinya.Complementizers.kemzi, Tigrinya.Complementizers.ki]
• Cacchioli2026.selects Cacchioli2026.VerbClass.directive = [Tigrinya.Complementizers.ki]
• Cacchioli2026.selects Cacchioli2026.VerbClass.desire = [Tigrinya.Complementizers.ki]
• Cacchioli2026.selects Cacchioli2026.VerbClass.modal = [Tigrinya.Complementizers.ki]
• Cacchioli2026.selects Cacchioli2026.VerbClass.emotiveFactive = [Tigrinya.Complementizers.ki]
• Cacchioli2026.selects Cacchioli2026.VerbClass.control = [Tigrinya.Complementizers.ki]
• Cacchioli2026.selects Cacchioli2026.VerbClass.ecm = [Tigrinya.Complementizers.ki]

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.

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.

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.

def Cacchioli2026.parseVerbClass : String → Option VerbClass

The thesis's verb-class labels.

Equations

• Cacchioli2026.parseVerbClass "factive" = some Cacchioli2026.VerbClass.factive
• Cacchioli2026.parseVerbClass "cognitive_non_factive" = some Cacchioli2026.VerbClass.cognitiveNonFactive
• Cacchioli2026.parseVerbClass "fiction" = some Cacchioli2026.VerbClass.fiction
• Cacchioli2026.parseVerbClass "utterance" = some Cacchioli2026.VerbClass.utterance
• Cacchioli2026.parseVerbClass "perception" = some Cacchioli2026.VerbClass.perception
• Cacchioli2026.parseVerbClass "directive" = some Cacchioli2026.VerbClass.directive
• Cacchioli2026.parseVerbClass "desire" = some Cacchioli2026.VerbClass.desire
• Cacchioli2026.parseVerbClass "modal" = some Cacchioli2026.VerbClass.modal
• Cacchioli2026.parseVerbClass "emotive_factive" = some Cacchioli2026.VerbClass.emotiveFactive
• Cacchioli2026.parseVerbClass "control" = some Cacchioli2026.VerbClass.control
• Cacchioli2026.parseVerbClass "ecm" = some Cacchioli2026.VerbClass.ecm
• Cacchioli2026.parseVerbClass x✝ = none

def Cacchioli2026.parseTyper : String → Option Complementizer

The thesis's clause-typer labels.

Equations

• Cacchioli2026.parseTyper "kemzi" = some Tigrinya.Complementizers.kemzi
• Cacchioli2026.parseTyper "ki" = some Tigrinya.Complementizers.ki
• Cacchioli2026.parseTyper "ilu" = some Tigrinya.Complementizers.ilu
• Cacchioli2026.parseTyper x✝ = none

structure Cacchioli2026.SelectionDatum : Type

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

• verbClass : VerbClass
• typer : Complementizer

def Cacchioli2026.instDecidableEqSelectionDatum.decEq (x✝ x✝¹ : SelectionDatum) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Cacchioli2026.instDecidableEqSelectionDatum : DecidableEq SelectionDatum

Equations

• Cacchioli2026.instDecidableEqSelectionDatum = Cacchioli2026.instDecidableEqSelectionDatum.decEq

@[instance_reducible]

instance Cacchioli2026.instReprSelectionDatum : Repr SelectionDatum

Equations

• Cacchioli2026.instReprSelectionDatum = { reprPrec := Cacchioli2026.instReprSelectionDatum.repr }

def Cacchioli2026.instReprSelectionDatum.repr : SelectionDatum → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Cacchioli2026.selectionDatum (e : Datum) : Option SelectionDatum

The selection pairing an example records, where it records one.

Equations

• One or more equations did not get rendered due to their size.

def Cacchioli2026.selectionData : List SelectionDatum

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

Equations

• Cacchioli2026.selectionData = List.filterMap Cacchioli2026.selectionDatum Cacchioli2026.Examples.all

theorem Cacchioli2026.selects_covers_data (d : SelectionDatum) : d ∈ selectionData → d.typer ∈ selects d.verbClass

The selection table admits every attested pairing.

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

inductive Cacchioli2026.ClauseKind : Type

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

• root : ClauseKind
• ilu : ClauseKind
• future : ClauseKind
• relative : ClauseKind
• seem : ClauseKind
• conditional : ClauseKind
• complement : ClauseKind
• subjunctive : ClauseKind
• purpose : ClauseKind

@[instance_reducible]

instance Cacchioli2026.instDecidableEqClauseKind : DecidableEq ClauseKind

Equations

• Cacchioli2026.instDecidableEqClauseKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cacchioli2026.instReprClauseKind : Repr ClauseKind

Equations

• Cacchioli2026.instReprClauseKind = { reprPrec := Cacchioli2026.instReprClauseKind.repr }

def Cacchioli2026.instReprClauseKind.repr : ClauseKind → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Cacchioli2026.HasPolP : ClauseKind → Prop

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

Equations

• Cacchioli2026.HasPolP Cacchioli2026.ClauseKind.root = True
• Cacchioli2026.HasPolP Cacchioli2026.ClauseKind.ilu = True
• Cacchioli2026.HasPolP Cacchioli2026.ClauseKind.future = True
• Cacchioli2026.HasPolP x✝ = False

@[instance_reducible]

instance Cacchioli2026.instDecidablePredClauseKindHasPolP : DecidablePred HasPolP

Equations

• Cacchioli2026.instDecidablePredClauseKindHasPolP Cacchioli2026.ClauseKind.root = isTrue trivial
• Cacchioli2026.instDecidablePredClauseKindHasPolP Cacchioli2026.ClauseKind.ilu = isTrue trivial
• Cacchioli2026.instDecidablePredClauseKindHasPolP Cacchioli2026.ClauseKind.future = isTrue trivial
• Cacchioli2026.instDecidablePredClauseKindHasPolP Cacchioli2026.ClauseKind.relative = isFalse Cacchioli2026.instDecidablePredClauseKindHasPolP._proof_1
• Cacchioli2026.instDecidablePredClauseKindHasPolP Cacchioli2026.ClauseKind.seem = isFalse Cacchioli2026.instDecidablePredClauseKindHasPolP._proof_2
• Cacchioli2026.instDecidablePredClauseKindHasPolP Cacchioli2026.ClauseKind.conditional = isFalse Cacchioli2026.instDecidablePredClauseKindHasPolP._proof_3
• Cacchioli2026.instDecidablePredClauseKindHasPolP Cacchioli2026.ClauseKind.complement = isFalse Cacchioli2026.instDecidablePredClauseKindHasPolP._proof_4
• Cacchioli2026.instDecidablePredClauseKindHasPolP Cacchioli2026.ClauseKind.subjunctive = isFalse Cacchioli2026.instDecidablePredClauseKindHasPolP._proof_5
• Cacchioli2026.instDecidablePredClauseKindHasPolP Cacchioli2026.ClauseKind.purpose = isFalse Cacchioli2026.instDecidablePredClauseKindHasPolP._proof_6

def Cacchioli2026.parseClauseKind : String → Option ClauseKind

The thesis's clause-type labels.

Equations

• Cacchioli2026.parseClauseKind "root" = some Cacchioli2026.ClauseKind.root
• Cacchioli2026.parseClauseKind "ilu" = some Cacchioli2026.ClauseKind.ilu
• Cacchioli2026.parseClauseKind "future" = some Cacchioli2026.ClauseKind.future
• Cacchioli2026.parseClauseKind "relative" = some Cacchioli2026.ClauseKind.relative
• Cacchioli2026.parseClauseKind "seem" = some Cacchioli2026.ClauseKind.seem
• Cacchioli2026.parseClauseKind "conditional" = some Cacchioli2026.ClauseKind.conditional
• Cacchioli2026.parseClauseKind "complement" = some Cacchioli2026.ClauseKind.complement
• Cacchioli2026.parseClauseKind "subjunctive" = some Cacchioli2026.ClauseKind.subjunctive
• Cacchioli2026.parseClauseKind "purpose" = some Cacchioli2026.ClauseKind.purpose
• Cacchioli2026.parseClauseKind x✝ = none

structure Cacchioli2026.NegationDatum : Type

A negated clause, with its kind and its negative word as the forms of its morphs.

• clause : ClauseKind
• word : List String

def Cacchioli2026.instDecidableEqNegationDatum.decEq (x✝ x✝¹ : NegationDatum) : Decidable (x✝ = x✝¹)

Equations

• Cacchioli2026.instDecidableEqNegationDatum.decEq { clause := a, word := a_1 } { clause := b, word := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Cacchioli2026.instDecidableEqNegationDatum : DecidableEq NegationDatum

Equations

• Cacchioli2026.instDecidableEqNegationDatum = Cacchioli2026.instDecidableEqNegationDatum.decEq

@[instance_reducible]

instance Cacchioli2026.instReprNegationDatum : Repr NegationDatum

Equations

• Cacchioli2026.instReprNegationDatum = { reprPrec := Cacchioli2026.instReprNegationDatum.repr }

def Cacchioli2026.instReprNegationDatum.repr : NegationDatum → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Cacchioli2026.NegationDatum.HasSuffix (d : NegationDatum) : Prop

The negative word ends in the fragment's suffix -(ɨ)n.

Equations

• d.HasSuffix = (d.word.getLast? = some Tigrinya.Negation.n.form)

@[instance_reducible]

instance Cacchioli2026.instDecidablePredNegationDatumHasSuffix : DecidablePred NegationDatum.HasSuffix

Equations

• Cacchioli2026.instDecidablePredNegationDatumHasSuffix d = Cacchioli2026.instDecidablePredNegationDatumHasSuffix._aux_1 d

def Cacchioli2026.negativeWord (ws : List (List (List Char))) : Option (List String)

The negative word among the words of a sentence is the one bearing the fragment's negative prefix, ʔaj- or its allomorph ɛj-, given as the forms of its morphs.

Equations

• One or more equations did not get rendered due to their size.

def Cacchioli2026.negationDatum (e : Datum) : Option NegationDatum

The negated clause an example records, where it records one.

Equations

• One or more equations did not get rendered due to their size.

def Cacchioli2026.negationData : List NegationDatum

The negated clauses of the thesis's examples.

Equations

• Cacchioli2026.negationData = List.filterMap Cacchioli2026.negationDatum Cacchioli2026.Examples.all

theorem Cacchioli2026.suffix_iff_polP : (∀ e ∈ Examples.all, (List.lookup "clause" e.paperFeatures).isSome = true → (negationDatum e).isSome = true) ∧ ∀ d ∈ negationData, d.HasSuffix ↔ HasPolP d.clause

The suffix appears exactly in the clauses that carry PolP, every example classified by its clause having a negative word, so that none drops out of negationData.

def Cacchioli2026.variantData : List (NegationDatum × Judgment)

The negated variants the thesis judges beside its examples, in the same clause.

Equations

• One or more equations did not get rendered due to their size.

theorem Cacchioli2026.variants_ungrammatical : variantData ≠ [] ∧ ∀ v ∈ variantData, v.2 = Judgment.ungrammatical ∧ (v.1.HasSuffix ↔ ¬HasPolP v.1.clause)

The negated variants the thesis stars are those that break the generalization: in the ʔɨlu-complement of (25) the negative without the suffix, in the relative clause of (12a) the negative with it.

theorem Cacchioli2026.polP_clauses_attested : (∃ d ∈ negationData, d.clause = ClauseKind.root ∧ d.HasSuffix) ∧ (∃ d ∈ negationData, d.clause = ClauseKind.ilu ∧ d.HasSuffix) ∧ (∃ d ∈ negationData, d.clause = ClauseKind.future ∧ d.HasSuffix) ∧ ∃ d ∈ negationData, ¬d.HasSuffix

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