[Cac25] — Empirical Data [Cac25]

Pure empirical data from [Cac25] "The Syntax of Clausal Prefixes in Tigrinya." No theory imports — this file contains only observed patterns, grammaticality judgments, and co-occurrence restrictions.

Key observations

1. Four prefixes: zɨ-, kɨ-, kəmzi-, ʔay-...-n
2. Complementary distribution: No two prefixes co-occur
3. Verb class selection: The matrix verb determines which prefix appears
4. Fixed linear order: Prefix always precedes the verbal complex
5. Agreement asymmetry: kɨ- and ʔay-...-n take agreement; zɨ- and kəmzi- don't

inductive Cacchioli2025.TigrinyaPrefix : Type

The four clausal prefixes attested in Tigrinya.

• zi : TigrinyaPrefix
• ki : TigrinyaPrefix
• kemzi : TigrinyaPrefix
• ay_n : TigrinyaPrefix

@[implicit_reducible]

instance Cacchioli2025.instDecidableEqTigrinyaPrefix : DecidableEq TigrinyaPrefix

Equations

• Cacchioli2025.instDecidableEqTigrinyaPrefix x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Cacchioli2025.instReprTigrinyaPrefix : Repr TigrinyaPrefix

Equations

• Cacchioli2025.instReprTigrinyaPrefix = { reprPrec := Cacchioli2025.instReprTigrinyaPrefix.repr }

def Cacchioli2025.instReprTigrinyaPrefix.repr : TigrinyaPrefix → ℕ → Std.Format

Equations

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

structure Cacchioli2025.CooccurrenceJudgment : Type

A grammaticality judgment for a prefix combination. true = grammatical, false = ungrammatical.

• prefix1 : TigrinyaPrefix
• prefix2 : TigrinyaPrefix
• grammatical : Bool
• example_ : String

@[implicit_reducible]

instance Cacchioli2025.instReprCooccurrenceJudgment : Repr CooccurrenceJudgment

Equations

• Cacchioli2025.instReprCooccurrenceJudgment = { reprPrec := Cacchioli2025.instReprCooccurrenceJudgment.repr }

def Cacchioli2025.instReprCooccurrenceJudgment.repr : CooccurrenceJudgment → ℕ → Std.Format

Equations

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

def Cacchioli2025.instBEqCooccurrenceJudgment.beq : CooccurrenceJudgment → CooccurrenceJudgment → Bool

Equations

• One or more equations did not get rendered due to their size.
• Cacchioli2025.instBEqCooccurrenceJudgment.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Cacchioli2025.instBEqCooccurrenceJudgment : BEq CooccurrenceJudgment

Equations

• Cacchioli2025.instBEqCooccurrenceJudgment = { beq := Cacchioli2025.instBEqCooccurrenceJudgment.beq }

def Cacchioli2025.cooccurrenceData : List CooccurrenceJudgment

No two prefixes can co-occur (complementary distribution).

Equations

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

theorem Cacchioli2025.all_cooccurrences_ungrammatical : (cooccurrenceData.all fun (x : CooccurrenceJudgment) => x.grammatical == false) = true

All prefix combinations are ungrammatical (complementary distribution).

structure Cacchioli2025.SelectionDatum : Type

A selection datum: a matrix verb selects a particular prefix.

• verb : String
• verbGloss : String
• verbClass : String
• selectedPrefix : TigrinyaPrefix
• example_ : String
• grammatical : Bool

@[implicit_reducible]

instance Cacchioli2025.instReprSelectionDatum : Repr SelectionDatum

Equations

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

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

Equations

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

def Cacchioli2025.instBEqSelectionDatum.beq : SelectionDatum → SelectionDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Cacchioli2025.instBEqSelectionDatum.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Cacchioli2025.instBEqSelectionDatum : BEq SelectionDatum

Equations

• Cacchioli2025.instBEqSelectionDatum = { beq := Cacchioli2025.instBEqSelectionDatum.beq }

def Cacchioli2025.selectionData : List SelectionDatum

Verb class selection data from [Cac25].

Equations

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

structure Cacchioli2025.AgreementDatum : Type

Agreement data: which prefixes take agreement suffixes.

• prefix_ : TigrinyaPrefix
• takesAgreement : Bool

@[implicit_reducible]

instance Cacchioli2025.instReprAgreementDatum : Repr AgreementDatum

Equations

• Cacchioli2025.instReprAgreementDatum = { reprPrec := Cacchioli2025.instReprAgreementDatum.repr }

def Cacchioli2025.instReprAgreementDatum.repr : AgreementDatum → ℕ → Std.Format

Equations

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

def Cacchioli2025.instBEqAgreementDatum.beq : AgreementDatum → AgreementDatum → Bool

Equations

• Cacchioli2025.instBEqAgreementDatum.beq { prefix_ := a, takesAgreement := a_1 } { prefix_ := b, takesAgreement := b_1 } = (a == b && a_1 == b_1)
• Cacchioli2025.instBEqAgreementDatum.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Cacchioli2025.instBEqAgreementDatum : BEq AgreementDatum

Equations

• Cacchioli2025.instBEqAgreementDatum = { beq := Cacchioli2025.instBEqAgreementDatum.beq }

def Cacchioli2025.agreementData : List AgreementDatum

Equations

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

def Cacchioli2025.ctpToFiniteness : CTPClass → Option Bool

Map CTP reality status to [±finite] selection.

Realis CTPs (utterance, knowledge, commentative,...) select [+finite] complements — indicative/realis clauses whose Fin head bears [+finite].

Irrealis CTPs (desiderative, manipulative, modal,...) select [-finite] complements — subjunctive/irrealis clauses whose Fin head bears [-finite].

Some classes are variable (perception can take both finite and non-finite complements), so they return none.

Equations

• Cacchioli2025.ctpToFiniteness CTPClass.utterance = some true
• Cacchioli2025.ctpToFiniteness CTPClass.knowledge = some true
• Cacchioli2025.ctpToFiniteness CTPClass.commentative = some true
• Cacchioli2025.ctpToFiniteness CTPClass.propAttitude = some true
• Cacchioli2025.ctpToFiniteness CTPClass.desiderative = some false
• Cacchioli2025.ctpToFiniteness CTPClass.manipulative = some false
• Cacchioli2025.ctpToFiniteness CTPClass.modal = some false
• Cacchioli2025.ctpToFiniteness CTPClass.phasal = some false
• Cacchioli2025.ctpToFiniteness CTPClass.achievement = some false
• Cacchioli2025.ctpToFiniteness CTPClass.negative = some false
• Cacchioli2025.ctpToFiniteness CTPClass.perception = none
• Cacchioli2025.ctpToFiniteness CTPClass.pretence = none

def Cacchioli2025.ctpToFactivity : CTPClass → Option Bool

Map CTP class to [±factive] selection.

Factive CTPs presuppose the truth of their complement; their Force/C head bears [+factive]. Non-factive CTPs don't, bearing [-factive].

Equations

• Cacchioli2025.ctpToFactivity CTPClass.knowledge = some true
• Cacchioli2025.ctpToFactivity CTPClass.commentative = some true
• Cacchioli2025.ctpToFactivity CTPClass.perception = some true
• Cacchioli2025.ctpToFactivity CTPClass.utterance = some false
• Cacchioli2025.ctpToFactivity CTPClass.propAttitude = some false
• Cacchioli2025.ctpToFactivity CTPClass.desiderative = some false
• Cacchioli2025.ctpToFactivity x✝ = none

theorem Cacchioli2025.knowledge_selects_finite : ctpToFiniteness CTPClass.knowledge = some true

Knowledge verbs select [+finite] (indicative) complements.

theorem Cacchioli2025.desiderative_selects_nonfinite : ctpToFiniteness CTPClass.desiderative = some false

Desiderative verbs select [-finite] (subjunctive/irrealis) complements.

theorem Cacchioli2025.knowledge_is_factive : ctpToFactivity CTPClass.knowledge = some true

Knowledge verbs select [+factive] complements.

theorem Cacchioli2025.utterance_not_factive : ctpToFactivity CTPClass.utterance = some false

Utterance verbs select [-factive] complements.

theorem Cacchioli2025.realis_implies_finite : ctpToFiniteness CTPClass.utterance = some true ∧ ctpToFiniteness CTPClass.knowledge = some true ∧ ctpToFiniteness CTPClass.commentative = some true ∧ ctpToFiniteness CTPClass.propAttitude = some true

Realis CTP classes map to [+finite].

theorem Cacchioli2025.irrealis_implies_nonfinite : ctpToFiniteness CTPClass.desiderative = some false ∧ ctpToFiniteness CTPClass.manipulative = some false ∧ ctpToFiniteness CTPClass.modal = some false ∧ ctpToFiniteness CTPClass.phasal = some false

Irrealis CTP classes map to [-finite].

theorem Cacchioli2025.irrealis_always_nonfinite (c : CTPClass) (b : Bool) (h : ctpToFiniteness c = some b) (hr : ctpRealityStatus c = RealityStatus.irrealis) : b = false

Irrealis CTP classes always map to [-finite] when they have a value. The converse (realis → [+finite]) does not hold universally: phasal verbs are realis but take non-finite complements.

theorem Cacchioli2025.phasal_violates_realis_finite_correspondence : ctpRealityStatus CTPClass.phasal = RealityStatus.realis ∧ ctpToFiniteness CTPClass.phasal = some false

Cross-paper divergence theorem: phasal CTPs witness the failure of the realis ↔ finite correspondence. [Noo07] §3.1.1 puts phasal complements in DTR, but the substrate's ctpRealityStatus classifies them as realis (event is asserted as actual). Cacchioli's feature-based analysis classifies the same complements as [-finite] (reduced). The contradiction makes visible a real Noonan- internal tension between the realis-as-asserted-fact criterion and the DTR → irrealis groupings of Table 2.3.

The witness: phasal is realis AND takes non-finite (irrealis-aligned) complements. Any unification forcing realis ↔ +finite would have to reclassify either Noonan's reality status of phasal or Cacchioli's finiteness assignment.

def Cacchioli2025.headCat (e : Tigrinya.ClausePrefixes.ClausePrefixEntry) : Minimalist.Cat

[Cac25]'s cartographic head assignment for the four prefixes ([Riz97] split CP): zɨ- spells out Rel, kɨ- Fin, kəmzi- Force, ʔay- Neg. Paper-specific analysis projected over the framework-neutral fragment entries.

Equations

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

theorem Cacchioli2025.zi_fvalue_topic_field : Minimalist.fValue (headCat Tigrinya.ClausePrefixes.zi) = Minimalist.fValue Minimalist.Cat.Top

zɨ- (Rel) is at the same fValue level as Top (topic field, F5).

theorem Cacchioli2025.ki_fvalue_boundary : Minimalist.fValue (headCat Tigrinya.ClausePrefixes.ki) = 3

kɨ- (Fin) is at the IP/CP boundary (F3).

theorem Cacchioli2025.kemzi_fvalue_clause_typing : Minimalist.fValue (headCat Tigrinya.ClausePrefixes.kemzi) = 6

kəmzi- (Force) is at the clause-typing level (F6).

theorem Cacchioli2025.ay_fvalue_inflectional : Minimalist.fValue (headCat Tigrinya.ClausePrefixes.ay_n) = 2

ʔay-...-n (Neg) is in the inflectional domain (F2).

theorem Cacchioli2025.prefixes_distinct_flevels : Minimalist.fValue (headCat Tigrinya.ClausePrefixes.ay_n) < Minimalist.fValue (headCat Tigrinya.ClausePrefixes.ki) ∧ Minimalist.fValue (headCat Tigrinya.ClausePrefixes.ki) < Minimalist.fValue (headCat Tigrinya.ClausePrefixes.zi) ∧ Minimalist.fValue (headCat Tigrinya.ClausePrefixes.zi) < Minimalist.fValue (headCat Tigrinya.ClausePrefixes.kemzi)

The four prefixes target four distinct F-levels: Neg(2) < Fin(3) < Rel(5) < Force(6).

theorem Cacchioli2025.agreement_matches_data_bridge : Tigrinya.ClausePrefixes.zi.agrees = some false ∧ Tigrinya.ClausePrefixes.ki.agrees = some true ∧ Tigrinya.ClausePrefixes.kemzi.agrees = some false ∧ Tigrinya.ClausePrefixes.ay_n.agrees = some true

Fragment agreement field matches empirical data for each prefix.

theorem Cacchioli2025.only_neg_discontinuous : Tigrinya.ClausePrefixes.zi.position = some Morphology.FormativePosition.praefixed ∧ Tigrinya.ClausePrefixes.ki.position = some Morphology.FormativePosition.praefixed ∧ Tigrinya.ClausePrefixes.kemzi.position = some Morphology.FormativePosition.praefixed ∧ Tigrinya.ClausePrefixes.ay_n.position = some Morphology.FormativePosition.circumfixed

Only ʔay-...-n is discontinuous (circumfixal position).

theorem Cacchioli2025.knowledge_selects_kemzi : ctpToFiniteness CTPClass.knowledge = some true

Knowledge verbs select [+finite] → predicts kəmzi- (factive).

theorem Cacchioli2025.desiderative_selects_ki : ctpToFiniteness CTPClass.desiderative = some false

Desiderative verbs select [-finite] → predicts kɨ- (subjunctive).

theorem Cacchioli2025.commentative_selects_kemzi : ctpToFiniteness CTPClass.commentative = some true

Commentative verbs select [+finite] → predicts kəmzi- (factive).

theorem Cacchioli2025.manipulative_selects_ki : ctpToFiniteness CTPClass.manipulative = some false

Manipulative verbs select [-finite] → predicts kɨ- (subjunctive).

theorem Cacchioli2025.neg_circumfix_realize : (Tigrinya.ClausePrefixes.negCircumfix "mäs'ə").realize = "ʔay-mäs'ə-n"

The negative circumfix surfaces correctly for a sample verb.

theorem Cacchioli2025.neg_circumfix_from_neg : (Tigrinya.ClausePrefixes.negCircumfix "mäs'ə").gloss = Tigrinya.ClausePrefixes.ay_n.gloss

The negative circumfix gloss is derived from the fragment entry.

theorem Cacchioli2025.all_prefixes_verbal : Minimalist.catFamily (headCat Tigrinya.ClausePrefixes.zi) = Minimalist.CatFamily.verbal ∧ Minimalist.catFamily (headCat Tigrinya.ClausePrefixes.ki) = Minimalist.CatFamily.verbal ∧ Minimalist.catFamily (headCat Tigrinya.ClausePrefixes.kemzi) = Minimalist.CatFamily.verbal ∧ Minimalist.catFamily (headCat Tigrinya.ClausePrefixes.ay_n) = Minimalist.CatFamily.verbal

All four prefix heads are in the verbal extended projection.

def Cacchioli2025.tigrinyaAnalysis : Bondarenko2022.ContAnalysis

[Cac25]'s extension of [Bon22]'s Cont-exponence paradigm: kemzi as Tigrinya's overt Cont exponent (the 2025 comparison, so it lives here per the chronology rule).

Equations

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