Variation in the lexical semantics of property concept roots

@cite{hanink-koontz-garboden-2025}

Hanink, E.A. & Koontz-Garboden, A. (2025). Variation in the lexical semantics of property concept roots: Evidence from Wá·šiw. Natural Language & Linguistic Theory 43, 2727–2769.

Core contribution

Property concept (PC) roots in Wá·šiw come in two semantic types:

• Individual/state relations (Class 1, Class 3): λx_e λs_v[P(x)(s)] These relate an individual to a state (e.g., √IHUK' 'dry': λx λs[dry(x)(s)]). Type: ⟨e, ⟨v, t⟩⟩ = RootDenotationType.indivStatePred.

• Quality predicates (Class 2): λs_v[P(s)] These are predicates of states with no individual argument (e.g., √I:YEL 'big': λs[big(s)]). Type: ⟨v, t⟩ = RootDenotationType.statePred.

Three morphological classes

Class	ATTR ʔil-	Reduplication	v_HAVE -iʔ	Example
1	*	*	*	yasaŋ 'hot'
2	*	*	✓	i:yel 'big'
3	✓	✓	✓	kaykay 'tall'

Key mechanisms

1. -iʔ as v_have (possessive light verb / categorizer): ⟦-iʔ⟧ = λP_⟨e,t⟩ λx_e ∃y_e[P(y) & π(x, y)] Verbalizes quality-denoting roots (Class 2) by introducing possessive semantics. Also functions as v_have in ordinary possession.

2. ʔil- as ∇ (type-shifter): ⟦ʔil-⟧ = λP_⟨e,⟨v,t⟩⟩ λs_v[∇(λx λs'[P(x)(s')])(s)] Converts individual/state relations (Class 3) to quality-type predicates, which then feed into -iʔ.

3. Type mismatch prediction: v_become requires ⟨e, ⟨v, t⟩⟩ as input. Class 2 roots are ⟨v, t⟩ (hasIndivArg = false), so they CANNOT appear as finals in resultative bipartite verb constructions. Class 1 and 3 roots CAN (hasIndivArg = true).

Connections

• Both -iʔ and ʔil- ADD semantic content (possession, ∇) — monotonic operations consistent with the MH (@cite{koontz-garboden-2009}).
• π is Barker's relationalizer from possessive NP semantics, reused inside the verbal categorizer's denotation.
• Against @cite{menon-pancheva-2014}'s universalist claim: not all PC roots have the same meaning.
• All Wá·šiw PC roots are RootEntailments.propertyConcept (+S −M −R −C) per @cite{beavers-koontz-garboden-2020} — the variation is in semantic type, not in structural entailments.

inductive HaninkKoontzGarboden2025.MorphClass : Type

Morphological class of PC verbs in Wá·šiw (Table 2).

• class1 : MorphClass
• class2 : MorphClass
• class3 : MorphClass

@[implicit_reducible]

instance HaninkKoontzGarboden2025.instDecidableEqMorphClass : DecidableEq MorphClass

Equations

• HaninkKoontzGarboden2025.instDecidableEqMorphClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance HaninkKoontzGarboden2025.instReprMorphClass : Repr MorphClass

Equations

• HaninkKoontzGarboden2025.instReprMorphClass = { reprPrec := HaninkKoontzGarboden2025.instReprMorphClass.repr }

def HaninkKoontzGarboden2025.instReprMorphClass.repr : MorphClass → ℕ → Std.Format

Equations

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

def HaninkKoontzGarboden2025.MorphClass.denotationType : MorphClass → RootDenotationType

The RootDenotationType of roots in each morphological class.

Derived from the paper's analysis (§§4–5):

• Class 1/3: individual/state relations ⟨e, ⟨v, t⟩⟩
• Class 2: quality predicates ⟨v, t⟩

Equations

• HaninkKoontzGarboden2025.MorphClass.class1.denotationType = RootDenotationType.indivStatePred
• HaninkKoontzGarboden2025.MorphClass.class2.denotationType = RootDenotationType.statePred
• HaninkKoontzGarboden2025.MorphClass.class3.denotationType = RootDenotationType.indivStatePred

def HaninkKoontzGarboden2025.MorphClass.canBeResultFinal (mc : MorphClass) : Bool

v_become requires an individual/state relation ⟨e, ⟨v, t⟩⟩. A root can serve as a bipartite verb "final" (result component) iff its denotation type has an individual argument.

This is DERIVED from RootDenotationType.hasIndivArg, not stipulated per morphological class.

Equations

• mc.canBeResultFinal = mc.denotationType.hasIndivArg

theorem HaninkKoontzGarboden2025.class1_can_be_final : MorphClass.class1.canBeResultFinal = true

Class 1 roots can appear as bipartite verb finals (e.g., √IHUK' 'dry' in resultative 'dry by wiping').

theorem HaninkKoontzGarboden2025.class3_can_be_final : MorphClass.class3.canBeResultFinal = true

Class 3 roots can appear as bipartite verb finals (e.g., √ŠI:ŠIP 'straight' in resultative 'straighten by pulling').

theorem HaninkKoontzGarboden2025.class2_cannot_be_final : MorphClass.class2.canBeResultFinal = false

Class 2 roots CANNOT appear as bipartite verb finals — type mismatch with v_become because statePred.hasIndivArg = false. (@cite{hanink-koontz-garboden-2025} §5.1)

theorem HaninkKoontzGarboden2025.bipartite_gap_iff_no_indiv_arg (mc : MorphClass) : mc.canBeResultFinal = false ↔ mc = MorphClass.class2

The bipartite verb gap follows from semantic type: exactly the quality-type roots (those lacking an individual argument) are excluded.

def HaninkKoontzGarboden2025.vHave {Entity State : Type} [BEq Entity] (entities : List Entity) (P : Semantics.ArgumentStructure.Relational.Pred1 Entity State) (R : Semantics.ArgumentStructure.Relational.Pred2 Entity State) (x : Entity) (s : State) : Bool

Denotation of -iʔ as v_have (@cite{hanink-koontz-garboden-2025} (34)): ⟦-iʔ⟧ = λP λx ∃y[P(y) & π(x, y)]

Takes a one-place predicate P (the quality/state) and a possession relation R, returning a predicate of individuals who possess something satisfying P. Quantification over the possessum y is modeled via List.any over a finite entity domain.

Equations

• HaninkKoontzGarboden2025.vHave entities P R x s = entities.any fun (y : Entity) => P y s && R x y s

theorem HaninkKoontzGarboden2025.vHave_is_ex_pi {Entity State : Type} [BEq Entity] (entities : List Entity) (P : Semantics.ArgumentStructure.Relational.Pred1 Entity State) (R : Semantics.ArgumentStructure.Relational.Pred2 Entity State) (x : Entity) (s : State) : vHave entities P R x s = entities.any fun (y : Entity) => Semantics.ArgumentStructure.Relational.π P R x y s

v_have is Barker's π composed with existential closure: vHave entities P R x s = ∃y ∈ entities. (π P R) x y s

def HaninkKoontzGarboden2025.nabla {Entity State : Type} [BEq Entity] (entities : List Entity) (P : Entity → State → Bool) (s : State) : Bool

The ∇ operator (ʔil-): type-shifts an individual/state relation to a quality predicate (@cite{hanink-koontz-garboden-2025} (57)).

⟦ʔil-⟧ = λP_⟨e,⟨v,t⟩⟩ λs_v[∇P(s)]

Takes a relation P between individuals and states, and returns the set of states that underly P's range — i.e., states s such that some individual bears P to s.

Equations

• HaninkKoontzGarboden2025.nabla entities P s = entities.any fun (x : Entity) => P x s

theorem HaninkKoontzGarboden2025.nabla_closes_indiv_arg {Entity State : Type} [BEq Entity] (entities : List Entity) (P : Entity → State → Bool) (s₁ s₂ : State) (h : ∀ (x : Entity), P x s₁ = P x s₂) : nabla entities P s₁ = nabla entities P s₂

∇ produces a quality-type predicate: its output depends only on the state, with the individual argument existentially closed. This matches RootDenotationType.statePred (⟨v,t⟩).

def HaninkKoontzGarboden2025.MorphClass.requiresVHave : MorphClass → Bool

Whether a morphological class requires the possessive verbalizer -iʔ. Derived from the root's denotation type: roots without an individual argument MUST go through v_have; roots with one MAY (Class 3) or may not (Class 1).

Equations

• HaninkKoontzGarboden2025.MorphClass.class1.requiresVHave = false
• HaninkKoontzGarboden2025.MorphClass.class2.requiresVHave = true
• HaninkKoontzGarboden2025.MorphClass.class3.requiresVHave = true

def HaninkKoontzGarboden2025.MorphClass.requiresNabla : MorphClass → Bool

Whether a morphological class requires the ʔil- prefix (∇ type-shift).

Equations

• HaninkKoontzGarboden2025.MorphClass.class1.requiresNabla = false
• HaninkKoontzGarboden2025.MorphClass.class2.requiresNabla = false
• HaninkKoontzGarboden2025.MorphClass.class3.requiresNabla = true

theorem HaninkKoontzGarboden2025.only_class1_zero_categorizes (mc : MorphClass) : mc.requiresVHave = false ↔ mc = MorphClass.class1

Class 1 roots are the only class that can be zero-categorized as verbs — they predicate directly without v_have (@cite{hanink-koontz-garboden-2025} §4.3 / Table 1; reaffirmed §7 Table 2).

theorem HaninkKoontzGarboden2025.no_indiv_arg_forces_vhave : MorphClass.class2.denotationType.hasIndivArg = false ∧ MorphClass.class2.requiresVHave = true

Quality-type roots (those without an individual argument) always require possessive morphology. This is the paper's central claim: the type mismatch between ⟨v,t⟩ and predication of individuals FORCES v_have.

theorem HaninkKoontzGarboden2025.nabla_implies_vhave (mc : MorphClass) : mc.requiresNabla = true → mc.requiresVHave = true

ʔil- always co-occurs with -iʔ: Class 3 has both. ∇ type-shifts the root to quality-type, which then needs v_have.

inductive HaninkKoontzGarboden2025.PCOp : Type

Operators in Wá·šiw PC verb derivation. Modeled as abstract labels for MH checking; compositional semantics is given by vHave and nabla above.

• root : PCOp
• possess : PCOp
• nabla : PCOp
• redupMorph : PCOp

@[implicit_reducible]

instance HaninkKoontzGarboden2025.instDecidableEqPCOp : DecidableEq PCOp

Equations

• HaninkKoontzGarboden2025.instDecidableEqPCOp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def HaninkKoontzGarboden2025.instReprPCOp.repr : PCOp → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HaninkKoontzGarboden2025.instReprPCOp : Repr PCOp

Equations

• HaninkKoontzGarboden2025.instReprPCOp = { reprPrec := HaninkKoontzGarboden2025.instReprPCOp.repr }

def HaninkKoontzGarboden2025.instBEqPCOp.beq : PCOp → PCOp → Bool

Equations

• HaninkKoontzGarboden2025.instBEqPCOp.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance HaninkKoontzGarboden2025.instBEqPCOp : BEq PCOp

Equations

• HaninkKoontzGarboden2025.instBEqPCOp = { beq := HaninkKoontzGarboden2025.instBEqPCOp.beq }

def HaninkKoontzGarboden2025.MorphClass.operators : MorphClass → List PCOp

Operators present in each morphological class. Class 1: just the root. Class 2: root + possession (from -iʔ). Class 3: root + ∇ + reduplication + possession.

Equations

• One or more equations did not get rendered due to their size.
• HaninkKoontzGarboden2025.MorphClass.class1.operators = [HaninkKoontzGarboden2025.PCOp.root]
• HaninkKoontzGarboden2025.MorphClass.class2.operators = [HaninkKoontzGarboden2025.PCOp.root, HaninkKoontzGarboden2025.PCOp.possess]

theorem HaninkKoontzGarboden2025.all_derivations_monotonic : KoontzGarboden2009.Monotonicity.isMonotonic MorphClass.class1.operators MorphClass.class2.operators = true ∧ KoontzGarboden2009.Monotonicity.isMonotonic MorphClass.class1.operators MorphClass.class3.operators = true ∧ KoontzGarboden2009.Monotonicity.isMonotonic MorphClass.class2.operators MorphClass.class3.operators = true

All three derivational relationships are monotonic — none remove operators from the LSR. Uses isMonotonic from KoontzGarboden2009.lean (the originating paper for the Monotonicity Hypothesis).

theorem HaninkKoontzGarboden2025.within_language_variation : ∃ (c₁ : MorphClass) (c₂ : MorphClass), c₁.denotationType ≠ c₂.denotationType ∧ c₁.requiresVHave ≠ c₂.requiresVHave ∧ c₁.canBeResultFinal ≠ c₂.canBeResultFinal

@cite{menon-pancheva-2014} claim all PC roots have the same semantic type crosslinguistically. @cite{hanink-koontz-garboden-2025} refutes this with language-internal evidence: Wá·šiw has PC roots of BOTH denotation types, correlated with different morphosyntax.

structure HaninkKoontzGarboden2025.WasiwPCRoot : Type

A Wá·šiw property concept root entry.

The theory-layer RootClassification is exposed as a derived projection toRootClassification rather than a stored field — all PC roots share arity := .noTheme, changeType := .propertyConcept, and have denotationType determined by morphClass.denotationType. Storing it redundantly would invite the encoding-conclusions-as-definitions anti-pattern (CLAUDE.md).

• stem : String
• gloss : String
• morphClass : MorphClass
• dixonCat : PCClass

def HaninkKoontzGarboden2025.instReprWasiwPCRoot.repr : WasiwPCRoot → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HaninkKoontzGarboden2025.instReprWasiwPCRoot : Repr WasiwPCRoot

Equations

• HaninkKoontzGarboden2025.instReprWasiwPCRoot = { reprPrec := HaninkKoontzGarboden2025.instReprWasiwPCRoot.repr }

def HaninkKoontzGarboden2025.WasiwPCRoot.toRootClassification (w : WasiwPCRoot) : RootClassification

The theory-layer RootClassification derived from a Wáshiw PC root. All PC roots are propertyConcept (+S −M −R −C) and noTheme; their denotationType is determined by MorphClass.denotationType.

Equations

• w.toRootClassification = { arity := RootArity.noTheme, changeType := RootType.propertyConcept, denotationType := some w.morphClass.denotationType }

def HaninkKoontzGarboden2025.mkWasiwRoot (stem gloss : String) (mc : MorphClass) (cat : PCClass) : WasiwPCRoot

Convenience constructor — kept stable for sampleRoots literals.

Equations

• HaninkKoontzGarboden2025.mkWasiwRoot stem gloss mc cat = { stem := stem, gloss := gloss, morphClass := mc, dixonCat := cat }

def HaninkKoontzGarboden2025.sampleRoots : List WasiwPCRoot

Selected sample of Wá·šiw PC roots from @cite{hanink-koontz-garboden-2025}'s Table A1 (Appendix). The full table reports 30 Class 1, 15 Class 2, and 35 Class 3 roots; the 36-root sample below covers ~13/11/12 from each class plus the 5 attested color roots (all Class 3 per §7), so proportions are not preserved — Class 2 is overrepresented and Class 1 undersampled relative to the corpus.

Equations

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

All Wáshiw PC roots are property-concept (changeType = .propertyConcept), noTheme arity, and have a denotation type determined by their morph class — these invariants are true by construction of WasiwPCRoot.toRootClassification, so no separate theorems are needed. The theorems below test substantive claims about the sample's composition, not its constructor's consistency.

theorem HaninkKoontzGarboden2025.color_roots_are_class3 : ((List.filter (fun (x : WasiwPCRoot) => x.dixonCat == PCClass.color) sampleRoots).all fun (x : WasiwPCRoot) => x.morphClass == MorphClass.class3) = true

All color roots are Class 3 — the only fully predictable Dixon category (@cite{hanink-koontz-garboden-2025} §7, Appendix).

theorem HaninkKoontzGarboden2025.class_distribution : (List.filter (fun (x : WasiwPCRoot) => x.morphClass == MorphClass.class1) sampleRoots).length = 13 ∧ (List.filter (fun (x : WasiwPCRoot) => x.morphClass == MorphClass.class2) sampleRoots).length = 11 ∧ (List.filter (fun (x : WasiwPCRoot) => x.morphClass == MorphClass.class3) sampleRoots).length = 12

Distribution across the sample (13/11/12 for Class 1/2/3).

theorem HaninkKoontzGarboden2025.statePred_unique_no_indiv (dt : RootDenotationType) : dt.hasIndivArg = false ↔ dt = RootDenotationType.statePred

statePred is the only RootDenotationType without an individual argument — it is the type that forces possessive morphology.

theorem HaninkKoontzGarboden2025.class1_class3_same_denotation : MorphClass.class1.denotationType = MorphClass.class3.denotationType

Class 1 and Class 3 share denotation type (both indivStatePred).

theorem HaninkKoontzGarboden2025.class2_unique_statePred (mc : MorphClass) : mc.denotationType = RootDenotationType.statePred ↔ mc = MorphClass.class2

Class 2 is the only class with statePred denotation type.

theorem HaninkKoontzGarboden2025.class2_characterization (mc : MorphClass) : mc.denotationType = RootDenotationType.statePred ↔ mc.canBeResultFinal = false ∧ mc = MorphClass.class2

The three key predictions form a single biconditional over morphological class, all derived from hasIndivArg:

mc = Class 2 ↔ statePred ↔ can't be bipartite final ↔ requires v_have

(The last implication is one-directional: Class 3 also requires v_have despite having indivStatePred, because ∇ converts it to quality-type before -iʔ applies.)