Inverse number

Kiowa-Tanoan verbal agreement distinguishes singular, dual, plural and inverse. Inverse is not a number value alongside the others ([Cor00], §5.5: inverse systems "are a matter of morphological arrangement and not of semantic values"); on [Har11]'s analysis it is what a D head shows when its [±atomic] and [±minimal] features are valued from two sources, the noun's inherent number and its natural number, and one feature receives both values. A Valuation records the values each feature has received, Valuation.agree merges an inherent and a natural valuation, and Valuation.category reads off the agreement category: inverse iff some feature is valued both ways, otherwise the number the values spell.

References

• G. G. Corbett, Number
• D. Harbour, Valence and atomic number
• D. Harbour, Paucity, abundance, and the theory of number

structure Number.Inverse.Valuation : Type

The values a D head has received in [±atomic] and [±minimal].

• atomic : Finset Bool

  The values received in [±atomic].

• minimal : Finset Bool

  The values received in [±minimal].

def Number.Inverse.instDecidableEqValuation.decEq (x✝ x✝¹ : Valuation) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Number.Inverse.instDecidableEqValuation : DecidableEq Valuation

Equations

• Number.Inverse.instDecidableEqValuation = Number.Inverse.instDecidableEqValuation.decEq

inductive Number.Inverse.Category : Type

The four categories of Kiowa-Tanoan verbal agreement.

• singular : Category
• dual : Category
• plural : Category
• inverse : Category

@[instance_reducible]

instance Number.Inverse.instDecidableEqCategory : DecidableEq Category

Equations

• Number.Inverse.instDecidableEqCategory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Number.Inverse.instReprCategory : Repr Category

Equations

• Number.Inverse.instReprCategory = { reprPrec := Number.Inverse.instReprCategory.repr }

def Number.Inverse.instReprCategory.repr : Category → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Number.Inverse.instFintypeCategory : Fintype Category

Equations

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

@[instance_reducible]

instance Number.Inverse.Valuation.instEmptyCollection : EmptyCollection Valuation

No values received.

Equations

• Number.Inverse.Valuation.instEmptyCollection = { emptyCollection := { atomic := ∅, minimal := ∅ } }

def Number.Inverse.Valuation.ofNumber : Number → Valuation

The valuation a natural number contributes, [Har14a]'s decomposition.

Equations

• Number.Inverse.Valuation.ofNumber Number.singular = { atomic := {true}, minimal := {true} }
• Number.Inverse.Valuation.ofNumber Number.dual = { atomic := {false}, minimal := {true} }
• Number.Inverse.Valuation.ofNumber Number.plural = { atomic := {false}, minimal := {false} }
• Number.Inverse.Valuation.ofNumber x✝ = ∅

def Number.Inverse.Valuation.agree (inherent natural : Valuation) : Valuation

D agrees with both the inherent and the natural number, receiving every value of each feature even when they clash.

Equations

• inherent.agree natural = { atomic := inherent.atomic ∪ natural.atomic, minimal := inherent.minimal ∪ natural.minimal }

def Number.Inverse.Valuation.IsInverse (v : Valuation) : Prop

Some feature has received both values.

Equations

• v.IsInverse = (v.atomic = Finset.univ ∨ v.minimal = Finset.univ)

@[instance_reducible]

instance Number.Inverse.Valuation.instDecidablePredIsInverse : DecidablePred IsInverse

Equations

• v.instDecidablePredIsInverse = { decide := decide (v.atomic = Finset.univ) || decide (v.minimal = Finset.univ), reflects_decide := ⋯ }

def Number.Inverse.Valuation.category (v : Valuation) : Option Category

The agreement category a valuation shows: inverse when a feature is valued both ways, otherwise the number its values spell, if any.

Equations

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

theorem Number.Inverse.Valuation.category_ofNumber_singular : (ofNumber singular).category = some Category.singular

A natural number alone shows itself.

theorem Number.Inverse.Valuation.category_ofNumber_dual : (ofNumber dual).category = some Category.dual

theorem Number.Inverse.Valuation.category_ofNumber_plural : (ofNumber plural).category = some Category.plural