Wechsler & Zlatić 2000: Agreement via the Declension–Concord–Index–Semantics chain

[WZ00] [Cor91] [Cor98] [PS94] [DK00]

A noun carries two feature bundles — CONCORD (case, number, gender), read by NP-internal targets, and the referential INDEX (person, number, gender), read by pronouns and finite verbs — correlated with declension class and semantics by a chain of binary constraints (their ex. 4):

declension ⇔ concord ⇔ index ⇔ semantics

Regular nouns satisfy every link; hybrid nouns break one (or, braća, two). The theory predicts exactly the three contiguous break patterns of the seven a-priori possibilities, all attested (their §9, n. 3).

Main declarations

• Noun, DecCon/ConInd/IndSem — the lexical entry and the three chain constraints (their exs. 15, 17, 18+22)
• brokenLinks, seven_logical_patterns/three_contiguous_predicted — the mismatch pattern of a noun, and the 7-logical/3-contiguous count
• concordAgrees/indexAgrees — target checking through the HasX.Compatible mixins, with the deca paradigm (exs. 41–42)
• no_single_phi_bundle_for_deca — the §3.3 single-bundle "illusion" as a refutation against Word.Agree
• indexReaders_lowerSet — the Agreement Hierarchy skeleton over Agreement.AgreementTarget, robust to the open predicate position

Coordinate resolution (their fn. 18) is handled in Studies/DalrympleKaplan2000.lean, to which the paper defers; the HPSG spell-out function φ (Appendix) is out of scope.

TODO

• Concord-ending syncretism (Table 2) and the participle indeterminacy it causes (§7.3, left open in the paper).
• The sudija/mušterija disjunctive sex specification (exs. 20, 31–32), here flattened to resolved variants.
• Pragmatic agreement: masculine-plural pronouns for mixed groups (§3.1).

Feature bundles (§3.3)

CONCORD comprises case, number, and gender; INDEX comprises person, number, and gender. Case is contextual (valued in syntax), so the lexical CONCORD carries number and gender; a realized NP-internal target adds the case value.

inductive WechslerZlatic2000.Declension : Type

Serbo-Croatian declension classes (their Table 1). The singular citation-form classes are I/II/III; pluralia tantum sit outside this classification (their Table 3 lists their declension as a distinct value "pl", §6), so they get their own constructor rather than being forced into a numbered class.

• I : Declension
• II : Declension
• III : Declension
• pluralia : Declension

@[implicit_reducible]

instance WechslerZlatic2000.instDecidableEqDeclension : DecidableEq Declension

Equations

• WechslerZlatic2000.instDecidableEqDeclension x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def WechslerZlatic2000.instReprDeclension.repr : Declension → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance WechslerZlatic2000.instReprDeclension : Repr Declension

Equations

• WechslerZlatic2000.instReprDeclension = { reprPrec := WechslerZlatic2000.instReprDeclension.repr }

structure WechslerZlatic2000.ConcordF : Type

Lexical CONCORD features: number and gender (case is contextual).

• number : Number
• gender : Gender

@[implicit_reducible]

instance WechslerZlatic2000.instDecidableEqConcordF : DecidableEq ConcordF

Equations

• WechslerZlatic2000.instDecidableEqConcordF = WechslerZlatic2000.instDecidableEqConcordF.decEq

def WechslerZlatic2000.instDecidableEqConcordF.decEq (x✝ x✝¹ : ConcordF) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance WechslerZlatic2000.instReprConcordF : Repr ConcordF

Equations

• WechslerZlatic2000.instReprConcordF = { reprPrec := WechslerZlatic2000.instReprConcordF.repr }

def WechslerZlatic2000.instReprConcordF.repr : ConcordF → ℕ → Std.Format

Equations

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

structure WechslerZlatic2000.IndexF : Type

INDEX features: person, number, gender (their ex. 8).

• person : Person
• number : Number
• gender : Gender

@[implicit_reducible]

instance WechslerZlatic2000.instDecidableEqIndexF : DecidableEq IndexF

Equations

• WechslerZlatic2000.instDecidableEqIndexF = WechslerZlatic2000.instDecidableEqIndexF.decEq

def WechslerZlatic2000.instDecidableEqIndexF.decEq (x✝ x✝¹ : IndexF) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance WechslerZlatic2000.instReprIndexF : Repr IndexF

Equations

• WechslerZlatic2000.instReprIndexF = { reprPrec := WechslerZlatic2000.instReprIndexF.repr }

def WechslerZlatic2000.instReprIndexF.repr : IndexF → ℕ → Std.Format

Equations

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

inductive WechslerZlatic2000.SexRestriction : Type

Semantic sex restriction on the noun's referent (their exs. 18–20). sudija 'judge'-type nouns are treated via their resolved variants, following the paper's exs. 31–32.

• female : SexRestriction
• male : SexRestriction
• unrestricted : SexRestriction

@[implicit_reducible]

instance WechslerZlatic2000.instDecidableEqSexRestriction : DecidableEq SexRestriction

Equations

• WechslerZlatic2000.instDecidableEqSexRestriction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def WechslerZlatic2000.instReprSexRestriction.repr : SexRestriction → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance WechslerZlatic2000.instReprSexRestriction : Repr SexRestriction

Equations

• WechslerZlatic2000.instReprSexRestriction = { reprPrec := WechslerZlatic2000.instReprSexRestriction.repr }

inductive WechslerZlatic2000.Count : Type

The COUNT feature (their ex. 22): count nouns carry one or aggregate; noncount nouns lack COUNT (none at the entry).

• one : Count
• aggregate : Count

@[implicit_reducible]

instance WechslerZlatic2000.instDecidableEqCount : DecidableEq Count

Equations

• WechslerZlatic2000.instDecidableEqCount x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def WechslerZlatic2000.instReprCount.repr : Count → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance WechslerZlatic2000.instReprCount : Repr Count

Equations

• WechslerZlatic2000.instReprCount = { reprPrec := WechslerZlatic2000.instReprCount.repr }

structure WechslerZlatic2000.Noun : Type

A noun's agreement-relevant lexical entry: the four chain positions.

• lemma_ : String
• decl : Declension
• concord : ConcordF
• index : IndexF
• sex : SexRestriction
• count : Option Count

@[implicit_reducible]

instance WechslerZlatic2000.instDecidableEqNoun : DecidableEq Noun

Equations

• WechslerZlatic2000.instDecidableEqNoun = WechslerZlatic2000.instDecidableEqNoun.decEq

def WechslerZlatic2000.instDecidableEqNoun.decEq (x✝ x✝¹ : Noun) : Decidable (x✝ = x✝¹)

Equations

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

def WechslerZlatic2000.instReprNoun.repr : Noun → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance WechslerZlatic2000.instReprNoun : Repr Noun

Equations

• WechslerZlatic2000.instReprNoun = { reprPrec := WechslerZlatic2000.instReprNoun.repr }

The three chain constraints (their exs. 15, 17, 18, 22)

def WechslerZlatic2000.DecCon (n : Noun) : Prop

DecCon (ex. 15): class I nouns have masculine or neuter concord gender; class II/III nouns have feminine concord gender. Pluralia tantum lie outside the singular declension classification (their §6), so the constraint is vacuous for them — their break, when any, is at a later link.

Equations

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

def WechslerZlatic2000.ConInd (n : Noun) : Prop

ConInd (ex. 17): the noun's CONCORD and INDEX share number and gender (structure sharing in the original).

Equations

• WechslerZlatic2000.ConInd n = (n.concord.number = n.index.number ∧ n.concord.gender = n.index.gender)

def WechslerZlatic2000.IndSemGen (n : Noun) : Prop

IndSem, gender half (ex. 18): a female-restricted noun has feminine index, a male-restricted noun masculine index; vacuous otherwise.

Equations

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

def WechslerZlatic2000.IndSemNum (n : Noun) : Prop

IndSem, number half (ex. 22): aggregate reference gives plural index; nonaggregate and noncount give singular.

Equations

• WechslerZlatic2000.IndSemNum n = match n.count with | some WechslerZlatic2000.Count.aggregate => n.index.number = Number.plural | x => n.index.number = Number.singular

def WechslerZlatic2000.IndSem (n : Noun) : Prop

The index–semantics link: both halves.

Equations

• WechslerZlatic2000.IndSem n = (WechslerZlatic2000.IndSemGen n ∧ WechslerZlatic2000.IndSemNum n)

@[implicit_reducible]

instance WechslerZlatic2000.instDecidableDecCon (n : Noun) : Decidable (DecCon n)

Equations

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

@[implicit_reducible]

instance WechslerZlatic2000.instDecidableConInd (n : Noun) : Decidable (ConInd n)

Equations

• WechslerZlatic2000.instDecidableConInd n = id inferInstance

@[implicit_reducible]

instance WechslerZlatic2000.instDecidableIndSemGen (n : Noun) : Decidable (IndSemGen n)

Equations

• WechslerZlatic2000.instDecidableIndSemGen n = id inferInstance

@[implicit_reducible]

instance WechslerZlatic2000.instDecidableIndSemNum (n : Noun) : Decidable (IndSemNum n)

Equations

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

@[implicit_reducible]

instance WechslerZlatic2000.instDecidableIndSem (n : Noun) : Decidable (IndSem n)

Equations

• WechslerZlatic2000.instDecidableIndSem n = WechslerZlatic2000.instDecidableIndSem._aux_1 n

Mismatch patterns

inductive WechslerZlatic2000.ChainLink : Type

The three links of the chain (their ex. 4, read left to right).

• decCon : ChainLink
• conInd : ChainLink
• indSem : ChainLink

@[implicit_reducible]

instance WechslerZlatic2000.instDecidableEqChainLink : DecidableEq ChainLink

Equations

• WechslerZlatic2000.instDecidableEqChainLink x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def WechslerZlatic2000.instReprChainLink.repr : ChainLink → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance WechslerZlatic2000.instReprChainLink : Repr ChainLink

Equations

• WechslerZlatic2000.instReprChainLink = { reprPrec := WechslerZlatic2000.instReprChainLink.repr }

@[implicit_reducible]

instance WechslerZlatic2000.instFintypeChainLink : Fintype ChainLink

Equations

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

def WechslerZlatic2000.linkHolds (n : Noun) : ChainLink → Prop

Does a given link hold for a noun?

Equations

• WechslerZlatic2000.linkHolds n WechslerZlatic2000.ChainLink.decCon = WechslerZlatic2000.DecCon n
• WechslerZlatic2000.linkHolds n WechslerZlatic2000.ChainLink.conInd = WechslerZlatic2000.ConInd n
• WechslerZlatic2000.linkHolds n WechslerZlatic2000.ChainLink.indSem = WechslerZlatic2000.IndSem n

@[implicit_reducible]

instance WechslerZlatic2000.instDecidableLinkHolds (n : Noun) (l : ChainLink) : Decidable (linkHolds n l)

Equations

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

def WechslerZlatic2000.brokenLinks (n : Noun) : Finset ChainLink

A noun's mismatch pattern: the set of broken links (their ex. 5, the double bars).

Equations

• WechslerZlatic2000.brokenLinks n = {l : WechslerZlatic2000.ChainLink | ¬WechslerZlatic2000.linkHolds n l}

def WechslerZlatic2000.Regular (n : Noun) : Prop

A noun is regular iff every link holds.

Equations

• WechslerZlatic2000.Regular n = ∀ (l : WechslerZlatic2000.ChainLink), WechslerZlatic2000.linkHolds n l

@[implicit_reducible]

instance WechslerZlatic2000.instDecidableRegular (n : Noun) : Decidable (Regular n)

Equations

• WechslerZlatic2000.instDecidableRegular n = WechslerZlatic2000.instDecidableRegular._aux_1 n

The Serbo-Croatian lexicon (their Table 3, exs. 14, 16, 20, 29,

35, 39, 45)

Number values at the entry are those of the singular citation form for ordinary count nouns; collectives and pluralia tantum carry their lexically fixed values.

def WechslerZlatic2000.knjiga : Noun

knjiga 'book': perfectly regular class II feminine (ex. 14).

Equations

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

def WechslerZlatic2000.žena : Noun

žena 'woman': regular, female-denoting (their §1).

Equations

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

def WechslerZlatic2000.muž : Noun

muž 'husband': regular class I masculine (their §4.3).

Equations

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

def WechslerZlatic2000.steva : Noun

Steva: masculine name declining in class II — the declension ∥ concord break (their exs. 28–29). sudija 'judge' applied to males patterns identically (ex. 19a).

Equations

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

def WechslerZlatic2000.deca : Noun

deca 'children': class II collective, feminine singular CONCORD, neuter plural INDEX — the concord ∥ index break (their ex. 45–46).

Equations

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

def WechslerZlatic2000.gospoda : Noun

gospoda 'gentlemen': like deca but male-restricted with masculine plural index (their ex. 40, §7.1).

Equations

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

def WechslerZlatic2000.makazeNonAggregate : Noun

makaze 'scissors' on its nonaggregate reading ('one pair'): plural declension/concord/index against singular reference — the index ∥ semantics break (their exs. 34–35, with naočare 'glasses'). Declension is pluralia (Table 3 value "pl", not a numbered class); the feminine concord gender is supplied (Table 3 leaves makaze's gender unspecified) and is inessential to the break.

Equations

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

def WechslerZlatic2000.devojče : Noun

devojče 'girl': female-denoting diminutive with neuter index — an index ∥ semantics (gender) break (their exs. 11, Table 3).

Equations

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

def WechslerZlatic2000.braća : Noun

braća 'brothers': male-only with feminine singular concord and neuter plural index — the unique double break, concord ∥ index and index ∥ semantics (their ex. 39).

Equations

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

The mismatch typology, derived (their §5–§7)

theorem WechslerZlatic2000.regulars_satisfy_chain : Regular knjiga ∧ Regular žena ∧ Regular muž

Regular nouns satisfy the whole chain.

theorem WechslerZlatic2000.steva_breaks_decCon : brokenLinks steva = {ChainLink.decCon}

Steva breaks exactly declension ∥ concord (their ex. 29).

theorem WechslerZlatic2000.deca_breaks_conInd : brokenLinks deca = {ChainLink.conInd}

deca breaks exactly concord ∥ index (their ex. 46).

theorem WechslerZlatic2000.gospoda_breaks_conInd : brokenLinks gospoda = {ChainLink.conInd}

gospoda breaks exactly concord ∥ index (their §7.1).

theorem WechslerZlatic2000.makaze_breaks_indSem : brokenLinks makazeNonAggregate = {ChainLink.indSem}

makaze (nonaggregate) breaks exactly index ∥ semantics (their ex. 35).

theorem WechslerZlatic2000.devojče_breaks_indSem : brokenLinks devojče = {ChainLink.indSem}

devojče breaks exactly index ∥ semantics (gender half).

theorem WechslerZlatic2000.braća_double_break : brokenLinks braća = {ChainLink.conInd, ChainLink.indSem}

braća breaks both concord ∥ index and index ∥ semantics — the predicted-rare double break (their ex. 39).

Seven logical patterns, three predicted (their §9, n. 3)

A two-type mismatch pattern is a bipartition of the four chain positions; identify it with its cell containing declension (position 0). There are 2³ − 1 = 7 such bipartitions. The theory admits only breaks at chain links, so the cell must be an initial segment of the chain — and there are exactly 3 of those, realized by Steva, deca, and makaze respectively.

def WechslerZlatic2000.bipartitions : Finset (Finset (Fin 4))

Bipartitions of the four chain positions, as proper subsets containing position 0.

Equations

• WechslerZlatic2000.bipartitions = {S : Finset (Fin 4) | 0 ∈ S ∧ S ≠ Finset.univ}

def WechslerZlatic2000.cellOfBreak : ChainLink → Finset (Fin 4)

The cell of position 0 under a single break at link l: an initial segment of the chain.

Equations

• WechslerZlatic2000.cellOfBreak WechslerZlatic2000.ChainLink.decCon = {0}
• WechslerZlatic2000.cellOfBreak WechslerZlatic2000.ChainLink.conInd = {0, 1}
• WechslerZlatic2000.cellOfBreak WechslerZlatic2000.ChainLink.indSem = {0, 1, 2}

theorem WechslerZlatic2000.seven_logical_patterns : bipartitions.card = 7

Seven logically possible two-type mismatch patterns a priori (their §9, n. 3).

theorem WechslerZlatic2000.three_contiguous_predicted : {S ∈ bipartitions | ∃ (l : ChainLink), S = cellOfBreak l}.card = 3

Of the seven, the theory predicts the three contiguous ones — the initial-segment cells realized by Steva, deca, makaze (their §9: "our theory predicts three to be possible").

theorem WechslerZlatic2000.attested_patterns_are_contiguous : brokenLinks steva = {ChainLink.decCon} ∧ brokenLinks deca = {ChainLink.conInd} ∧ brokenLinks makazeNonAggregate = {ChainLink.indSem}

The attested single-break patterns are exactly the three contiguous cells — Steva, deca/gospoda, makaze/devojče (their Table 3: "Only contiguous cells in a row are connected by constraints, so we predict exactly the pattern observed").

Target checking through the carrier mixins (§3.3)

NP-internal targets (determiners, attributive adjectives) check CONCORD: case, number, gender. Pronouns and finite verbs check INDEX: person, number, gender. Both run through the shared HasX.Compatible relations. A target may be underspecified for a feature (none), where the flat-order wildcard semantics of Compatible does real work — see kojih, the concord-underspecified plural relative pronoun (§7.4).

structure WechslerZlatic2000.ConcordTarget : Type

A realized NP-internal target's inflectional features: the noun's lexical concord plus contextual case (their ex. 12). A feature is none when the target is unmarked for it (e.g. kojih, §7.4).

• case : Option Case
• number : Option Number
• gender : Option Gender

def WechslerZlatic2000.instDecidableEqConcordTarget.decEq (x✝ x✝¹ : ConcordTarget) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance WechslerZlatic2000.instDecidableEqConcordTarget : DecidableEq ConcordTarget

Equations

• WechslerZlatic2000.instDecidableEqConcordTarget = WechslerZlatic2000.instDecidableEqConcordTarget.decEq

@[implicit_reducible]

instance WechslerZlatic2000.instReprConcordTarget : Repr ConcordTarget

Equations

• WechslerZlatic2000.instReprConcordTarget = { reprPrec := WechslerZlatic2000.instReprConcordTarget.repr }

def WechslerZlatic2000.instReprConcordTarget.repr : ConcordTarget → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance WechslerZlatic2000.instHasCaseConcordTarget : HasCase ConcordTarget

Equations

• WechslerZlatic2000.instHasCaseConcordTarget = { caseOf := WechslerZlatic2000.ConcordTarget.case }

@[implicit_reducible]

instance WechslerZlatic2000.instHasNumberConcordTarget : HasNumber ConcordTarget

Equations

• WechslerZlatic2000.instHasNumberConcordTarget = { numberOf := WechslerZlatic2000.ConcordTarget.number }

@[implicit_reducible]

instance WechslerZlatic2000.instHasGenderConcordTarget : HasGender ConcordTarget

Equations

• WechslerZlatic2000.instHasGenderConcordTarget = { genderOf := WechslerZlatic2000.ConcordTarget.gender }

def WechslerZlatic2000.Noun.concordAt (n : Noun) (c : Case) : ConcordTarget

The noun's realized concord bundle at a contextual case value (the noun's own concord is always fully specified).

Equations

• n.concordAt c = { case := some c, number := some n.concord.number, gender := some n.concord.gender }

structure WechslerZlatic2000.IndexTarget : Type

An index-checking target's features (pronoun, finite verb).

• person : Person
• number : Number
• gender : Gender

@[implicit_reducible]

instance WechslerZlatic2000.instDecidableEqIndexTarget : DecidableEq IndexTarget

Equations

• WechslerZlatic2000.instDecidableEqIndexTarget = WechslerZlatic2000.instDecidableEqIndexTarget.decEq

def WechslerZlatic2000.instDecidableEqIndexTarget.decEq (x✝ x✝¹ : IndexTarget) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance WechslerZlatic2000.instReprIndexTarget : Repr IndexTarget

Equations

• WechslerZlatic2000.instReprIndexTarget = { reprPrec := WechslerZlatic2000.instReprIndexTarget.repr }

def WechslerZlatic2000.instReprIndexTarget.repr : IndexTarget → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance WechslerZlatic2000.instHasPersonIndexTarget : HasPerson IndexTarget

Equations

• WechslerZlatic2000.instHasPersonIndexTarget = { personOf := fun (t : WechslerZlatic2000.IndexTarget) => some t.person }

@[implicit_reducible]

instance WechslerZlatic2000.instHasNumberIndexTarget : HasNumber IndexTarget

Equations

• WechslerZlatic2000.instHasNumberIndexTarget = { numberOf := fun (t : WechslerZlatic2000.IndexTarget) => some t.number }

@[implicit_reducible]

instance WechslerZlatic2000.instHasGenderIndexTarget : HasGender IndexTarget

Equations

• WechslerZlatic2000.instHasGenderIndexTarget = { genderOf := fun (t : WechslerZlatic2000.IndexTarget) => some t.gender }

def WechslerZlatic2000.Noun.indexTarget (n : Noun) : IndexTarget

The noun's index bundle as a checking target.

Equations

• n.indexTarget = { person := n.index.person, number := n.index.number, gender := n.index.gender }

def WechslerZlatic2000.concordAgrees (a : ConcordTarget) (n : Noun) (c : Case) : Prop

Concord agreement: the target's case, number, and gender are each compatible with the noun's realized concord.

Equations

• WechslerZlatic2000.concordAgrees a n c = (HasCase.Compatible a (n.concordAt c) ∧ HasNumber.Compatible a (n.concordAt c) ∧ HasGender.Compatible a (n.concordAt c))

@[implicit_reducible]

instance WechslerZlatic2000.instDecidableConcordAgrees (a : ConcordTarget) (n : Noun) (c : Case) : Decidable (concordAgrees a n c)

Equations

• WechslerZlatic2000.instDecidableConcordAgrees a n c = WechslerZlatic2000.instDecidableConcordAgrees._aux_1 a n c

def WechslerZlatic2000.indexAgrees (p : IndexTarget) (n : Noun) : Prop

Index agreement: the target's person, number, and gender are each compatible with the noun's index.

Equations

• WechslerZlatic2000.indexAgrees p n = (HasPerson.Compatible p n.indexTarget ∧ HasNumber.Compatible p n.indexTarget ∧ HasGender.Compatible p n.indexTarget)

@[implicit_reducible]

instance WechslerZlatic2000.instDecidableIndexAgrees (p : IndexTarget) (n : Noun) : Decidable (indexAgrees p n)

Equations

• WechslerZlatic2000.instDecidableIndexAgrees p n = WechslerZlatic2000.instDecidableIndexAgrees._aux_1 p n

The deca paradigm (their exs. 41–43)

Posmatrali smo ovu dobru decu. Ona su spavala. — feminine singular on the accusative determiner and adjective (CONCORD), neuter plural on the coreferential pronoun (INDEX); the crossed combinations fail.

def WechslerZlatic2000.ovu : ConcordTarget

ovu/dobru: accusative feminine singular modifier (ex. 41).

Equations

• WechslerZlatic2000.ovu = { case := some Case.acc, number := some Number.singular, gender := some Gender.feminine }

def WechslerZlatic2000.ona : IndexTarget

ona: neuter plural pronoun (ex. 41).

Equations

• WechslerZlatic2000.ona = { person := Person.third, number := Number.plural, gender := Gender.neuter }

theorem WechslerZlatic2000.knjiga_regular_targets : concordAgrees { case := some Case.nom, number := some Number.singular, gender := some Gender.feminine } knjiga Case.nom ∧ indexAgrees { person := Person.third, number := Number.singular, gender := Gender.feminine } knjiga

ova stara (nominative feminine singular, ex. 6) agrees with regular knjiga in concord — and je (3sg feminine) in index.

theorem WechslerZlatic2000.deca_mixed_agreement : concordAgrees ovu deca Case.acc ∧ indexAgrees ona deca

Mixed agreement with deca (exs. 41–42): the f.sg modifier checks CONCORD and the nt.pl pronoun checks INDEX — simultaneously.

theorem WechslerZlatic2000.deca_crossed_combinations_fail : ¬concordAgrees { case := some Case.acc, number := some Number.plural, gender := some Gender.neuter } deca Case.acc ∧ ¬indexAgrees { person := Person.third, number := Number.singular, gender := Gender.feminine } deca

The crossed combinations fail: a neuter plural modifier does not stand in concord agreement with deca, and a feminine singular pronoun does not stand in index agreement with it (cf. je in their ex. 62).

def WechslerZlatic2000.kojih : ConcordTarget

kojih: the genitive plural relative pronoun, unmarked for CONCORD gender and number (§7.4). Its wildcard concord features make it compatible with deca (and with a feminine-singular noun) — the case where Compatible's flat-order semantics is not mere equality.

Equations

• WechslerZlatic2000.kojih = { case := some Case.gen, number := none, gender := none }

theorem WechslerZlatic2000.kojih_underspecified_agrees : concordAgrees kojih deca Case.gen

kojih agrees in concord with deca despite deca's f.sg concord and kojih's plural index — its underspecified concord is a wildcard. A fully-specified neuter-plural modifier does not (deca_crossed_combinations_fail).

theorem WechslerZlatic2000.regular_nouns_mask_the_split (n : Noun) (hn : ConInd n) (t : IndexTarget) : HasNumber.Compatible t n.indexTarget ↔ HasNumber.Compatible t (n.concordAt Case.nom)

For chain-intact nouns the split is invisible: a target's concord agreement coincides with index agreement on the shared number/gender features (the "illusion … that a single feature bundle on the noun is responsible for all the agreeing items", their §3.3).

theorem WechslerZlatic2000.no_single_phi_bundle_for_deca : ¬{ form := "dobra", cat := UD.UPOS.ADJ, features := { number := some UD.Number.Sing, gender := some UD.Gender.Fem } }.Agree { form := "ona", cat := UD.UPOS.PRON, features := { number := some UD.Number.Plur, gender := some UD.Gender.Neut } }

The single-φ-bundle view (Word.phi/Word.Agree) cannot host deca: its CONCORD-bearing attributive (f.sg) and its INDEX-bearing pronoun (nt.pl) do not Word.Agree, so they cannot both copy one fully-valued source bundle. This is §3.3's "illusion", as a refutation against the library's one-bundle primitive — note a featureless word would tolerate both (wildcards), so the claim is about the two specified surface forms, not about compatibility.

The Agreement Hierarchy, derived (their §8)

Corbett's hierarchy lives as Agreement.AgreementTarget; W&Z's contribution is readsIndex, the bundle-access derivation of it. Attributives lack referential indices (read only CONCORD); pronouns and verbs read INDEX, which alone connects to the semantics. The predicate position is open in the paper (§7.3): secondary predication points to concord (ex. 50), coordination to index (exs. 51–53).

def WechslerZlatic2000.readsIndex (predReadsIndex : Bool) : Agreement.AgreementTarget → Prop

Whether a target reads the INDEX bundle — the precondition for semantic agreement (their §8). predReadsIndex is the open predicate position (§7.3, "left for future research"); the hierarchy's monotonicity (indexReaders_lowerSet) holds for either value.

Equations

• WechslerZlatic2000.readsIndex predReadsIndex Agreement.AgreementTarget.attributive = False
• WechslerZlatic2000.readsIndex predReadsIndex Agreement.AgreementTarget.predicate = (predReadsIndex = true)
• WechslerZlatic2000.readsIndex predReadsIndex Agreement.AgreementTarget.relativePronoun = True
• WechslerZlatic2000.readsIndex predReadsIndex Agreement.AgreementTarget.personalPronoun = True
• WechslerZlatic2000.readsIndex predReadsIndex Agreement.AgreementTarget.verb = True

@[implicit_reducible]

instance WechslerZlatic2000.instDecidablePredAgreementTargetReadsIndex (p : Bool) : DecidablePred (readsIndex p)

Equations

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

theorem WechslerZlatic2000.indexReaders_lowerSet (p : Bool) (t u : Agreement.AgreementTarget) (h : u.rank ≤ t.rank) : readsIndex p t → readsIndex p u

The hierarchy skeleton: the index readers form a lower set in the AgreementTarget rank (higher rank = more syntactic), so semantic agreement can surface only at more-semantic targets — and this holds whichever way the open predicate position resolves. This is the categorical claim W&Z derive (their §8, "concord elements should never show semantic agreement unless the pronouns do"); it explains but does not reproduce Corbett's gradient, corpus-level likelihood law ([Cor98]; their fn. 21).