The φ-feature geometry

The morphosyntactic feature geometry of pronouns: monovalent person, number, and class features organized as a dependency tree under a root Referring Expression node, with Participant (Speaker, Addressee) and Individuation (Group, Minimal with its dependent Augmented, and Class) as the organizing nodes, with the collective first-person node Multispeaker below Speaker. A feature appears only together with the nodes it depends on, so the feature content of a pronoun is a lower set of the dominance order; markedness is node count; and an organizing node with no dependent receives its default daughter — Speaker, Minimal, Inanimate — by rule. Person and number cells are assigned their geometries, the contrastive Minimal node being present only in inventories that activate it. The tree is of the same formal type as the phonological feature geometries of [Cle85] and [Sag86].

Main definitions

• Node, Node.parent, and dominance ≤, a PartialOrder with the root as ⊥; Node.below is the content a node brings with it.
• Node.defaultDependent?, fillDefaults: the default daughters and their fill-in.
• personNodes, numberNodes, cell: the geometries of person, of number, and of a person–number cell, relative to an active inventory.
• Licenses: an inventory licenses a cell when the cell's geometry lies within it.

Main results

• le_iff: dominance is membership in the parent chain, hence decidable.
• cell_isLowerSet: every assigned geometry is a lower set.
• fillDefaults_isLowerSet: default fill-in preserves lower sets.

References

• H. Harley and E. Ritter, Person and number in pronouns: A feature-geometric analysis
• [H. Harley, Hug a tree][harley-1994]
• [M. McGinnis, Agree and Fission in Georgian plurals][mcginnis-2013]
• G. N. Clements, The geometry of phonological features
• E. Sagey, The representation of features and relations in non-linear phonology

inductive Phi.Geometry.Node : Type

The nodes of the geometry: the root, the three organizing nodes, and their dependents.

• referringExpression : Node

  The root: every pronoun; bare, the third person.

• participant : Node

  Discourse participant: first and second person.

• speaker : Node

  Includes the speaker; Participant's default dependent.

• multispeaker : Node

  Includes the speaker and others: a collective first person, expressing first-person plurality through person where number does not.

• addressee : Node

  Includes the addressee.

• individuation : Node

  Number and class.

• group : Node

  More than one: plural.

• minimal : Node

  A minimal set; Individuation's default dependent, singular alone and dual together with Group.

• augmented : Node

  A minimal group and more: paucal or trial.

• nounClass : Node

  Gender and class.

• animate : Node

  Animate.

• inanimate : Node

  Inanimate or neuter; Class's default dependent.

• feminine : Node

  Feminine.

• masculine : Node

  Masculine.

@[instance_reducible]

instance Phi.Geometry.instDecidableEqNode : DecidableEq Node

Equations

• Phi.Geometry.instDecidableEqNode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Phi.Geometry.instReprNode : Repr Node

Equations

• Phi.Geometry.instReprNode = { reprPrec := Phi.Geometry.instReprNode.repr }

def Phi.Geometry.instReprNode.repr : Node → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Phi.Geometry.instReprNode.repr Phi.Geometry.Node.speaker prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phi.Geometry.Node.speaker")).group prec✝
• Phi.Geometry.instReprNode.repr Phi.Geometry.Node.addressee prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phi.Geometry.Node.addressee")).group prec✝
• Phi.Geometry.instReprNode.repr Phi.Geometry.Node.group prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phi.Geometry.Node.group")).group prec✝
• Phi.Geometry.instReprNode.repr Phi.Geometry.Node.minimal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phi.Geometry.Node.minimal")).group prec✝
• Phi.Geometry.instReprNode.repr Phi.Geometry.Node.augmented prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phi.Geometry.Node.augmented")).group prec✝
• Phi.Geometry.instReprNode.repr Phi.Geometry.Node.nounClass prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phi.Geometry.Node.nounClass")).group prec✝
• Phi.Geometry.instReprNode.repr Phi.Geometry.Node.animate prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phi.Geometry.Node.animate")).group prec✝
• Phi.Geometry.instReprNode.repr Phi.Geometry.Node.inanimate prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phi.Geometry.Node.inanimate")).group prec✝
• Phi.Geometry.instReprNode.repr Phi.Geometry.Node.feminine prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phi.Geometry.Node.feminine")).group prec✝
• Phi.Geometry.instReprNode.repr Phi.Geometry.Node.masculine prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Phi.Geometry.Node.masculine")).group prec✝

@[instance_reducible]

instance Phi.Geometry.instFintypeNode : Fintype Node

Equations

• Phi.Geometry.instFintypeNode = { elems := { val := ↑Phi.Geometry.Node.enumList, nodup := Phi.Geometry.Node.enumList_nodup }, complete := Phi.Geometry.instFintypeNode._proof_1 }

def Phi.Geometry.Node.parent : Node → Option Node

The node each node depends on; the root alone has none.

Equations

• Phi.Geometry.Node.referringExpression.parent = none
• Phi.Geometry.Node.participant.parent = some Phi.Geometry.Node.referringExpression
• Phi.Geometry.Node.individuation.parent = some Phi.Geometry.Node.referringExpression
• Phi.Geometry.Node.speaker.parent = some Phi.Geometry.Node.participant
• Phi.Geometry.Node.addressee.parent = some Phi.Geometry.Node.participant
• Phi.Geometry.Node.multispeaker.parent = some Phi.Geometry.Node.speaker
• Phi.Geometry.Node.group.parent = some Phi.Geometry.Node.individuation
• Phi.Geometry.Node.minimal.parent = some Phi.Geometry.Node.individuation
• Phi.Geometry.Node.nounClass.parent = some Phi.Geometry.Node.individuation
• Phi.Geometry.Node.augmented.parent = some Phi.Geometry.Node.minimal
• Phi.Geometry.Node.animate.parent = some Phi.Geometry.Node.nounClass
• Phi.Geometry.Node.inanimate.parent = some Phi.Geometry.Node.nounClass
• Phi.Geometry.Node.feminine.parent = some Phi.Geometry.Node.animate
• Phi.Geometry.Node.masculine.parent = some Phi.Geometry.Node.animate

def Phi.Geometry.Node.ancestorsAux : ℕ → Node → List Node

The first k links of the parent chain.

Equations

• Phi.Geometry.Node.ancestorsAux 0 x✝ = []
• Phi.Geometry.Node.ancestorsAux k.succ x✝ = match x✝.parent with | none => [] | some p => p :: Phi.Geometry.Node.ancestorsAux k p

def Phi.Geometry.Node.ancestors (n : Node) : List Node

The proper ancestors of a node, nearest first; the tree has depth four.

Equations

• n.ancestors = Phi.Geometry.Node.ancestorsAux 4 n

def Phi.Geometry.Node.Dominates (a b : Node) : Prop

Dominance: a lies on the parent chain of b, so that b depends on a.

Equations

• a.Dominates b = Relation.ReflTransGen (fun (x y : Phi.Geometry.Node) => x.parent = some y) b a

theorem Phi.Geometry.Node.parent_mem_ancestorsAux {n p : Node} (h : n.parent = some p) (k : ℕ) : p ∈ ancestorsAux (k + 1) n

theorem Phi.Geometry.Node.dominates_of_mem_ancestorsAux (k : ℕ) {a b : Node} : a ∈ ancestorsAux k b → a.Dominates b

theorem Phi.Geometry.Node.mem_ancestors_of_parent_of_mem_ancestors {a b m : Node} : m ∈ b.ancestors → m.parent = some a → a ∈ b.ancestors

theorem Phi.Geometry.Node.dominates_iff (a b : Node) : a.Dominates b ↔ a = b ∨ a ∈ b.ancestors

Dominance is membership in the parent chain.

@[instance_reducible]

instance Phi.Geometry.Node.instPartialOrder : PartialOrder Node

The dominance order: a ≤ b when b depends on a.

Equations

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

theorem Phi.Geometry.Node.le_iff (a b : Node) : a ≤ b ↔ a = b ∨ a ∈ b.ancestors

@[instance_reducible]

instance Phi.Geometry.Node.instDecidableLE : DecidableLE Node

Equations

• a.instDecidableLE b = decidable_of_iff (a = b ∨ a ∈ b.ancestors) ⋯

@[instance_reducible]

instance Phi.Geometry.Node.instDecidableLT : DecidableLT Node

Equations

• Phi.Geometry.Node.instDecidableLT = decidableLTOfDecidableLE

@[instance_reducible]

instance Phi.Geometry.Node.instOrderBot : OrderBot Node

The root dominates every node.

Equations

• Phi.Geometry.Node.instOrderBot = { bot := Phi.Geometry.Node.referringExpression, bot_le := Phi.Geometry.Node.instOrderBot._proof_1 }

@[instance_reducible]

instance Phi.Geometry.Node.instLocallyFiniteOrder : LocallyFiniteOrder Node

Equations

• Phi.Geometry.Node.instLocallyFiniteOrder = Fintype.toLocallyFiniteOrder

theorem Phi.Geometry.Node.lt_of_parent {a b : Node} (h : b.parent = some a) : a < b

def Phi.Geometry.Node.all : List Node

Every node.

Equations

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

theorem Phi.Geometry.Node.mem_all (n : Node) : n ∈ all

def Phi.Geometry.Node.below (n : Node) : List Node

The nodes a node depends on, itself included and the root excluded: the content a privative feature brings with it.

Equations

• n.below = List.filter (fun (a : Phi.Geometry.Node) => decide (⊥ < a ∧ a ≤ n)) Phi.Geometry.Node.all

theorem Phi.Geometry.Node.mem_below {a n : Node} : a ∈ n.below ↔ ⊥ < a ∧ a ≤ n

theorem Phi.Geometry.Node.toFinset_below (n : Node) : n.below.toFinset = Finset.Ioc ⊥ n

theorem Phi.Geometry.Node.below_subset_below {a b : Node} (h : a ≤ b) : a.below ⊆ b.below

A dependent brings more than what it depends on.

def Phi.Geometry.Node.defaultDependent? : Node → Option Node

The default daughter of an organizing node: Speaker, Minimal, Inanimate.

Equations

• Phi.Geometry.Node.participant.defaultDependent? = some Phi.Geometry.Node.speaker
• Phi.Geometry.Node.individuation.defaultDependent? = some Phi.Geometry.Node.minimal
• Phi.Geometry.Node.nounClass.defaultDependent? = some Phi.Geometry.Node.inanimate
• x✝.defaultDependent? = none

Default fill-in

def Phi.Geometry.fillDefaults (s : Finset Node) : Finset Node

Fill in defaults: an organizing node present without any dependent receives its default daughter. The node count of a geometry is taken before fill-in.

Equations

• Phi.Geometry.fillDefaults s = s ∪ {d : Phi.Geometry.Node | ∃ o ∈ s, o.defaultDependent? = some d ∧ ∀ c ∈ s, ¬o < c}

theorem Phi.Geometry.subset_fillDefaults (s : Finset Node) : s ⊆ fillDefaults s

theorem Phi.Geometry.fillDefaults_isLowerSet {s : Finset Node} (hs : IsLowerSet ↑s) : IsLowerSet ↑(fillDefaults s)

Person and number cells

def Phi.Geometry.personNodes : Person → Option (Finset Node)

The person geometries: first person is the bare Participant node (Speaker by default), exclusive Participant with Speaker, inclusive Participant with Speaker and Addressee, second Participant with Addressee, third nothing; the impersonal has no geometry.

Equations

• Phi.Geometry.personNodes Person.first = some {Phi.Geometry.Node.participant}
• Phi.Geometry.personNodes Person.firstExclusive = some {Phi.Geometry.Node.participant, Phi.Geometry.Node.speaker}
• Phi.Geometry.personNodes Person.firstInclusive = some {Phi.Geometry.Node.participant, Phi.Geometry.Node.speaker, Phi.Geometry.Node.addressee}
• Phi.Geometry.personNodes Person.second = some {Phi.Geometry.Node.participant, Phi.Geometry.Node.addressee}
• Phi.Geometry.personNodes Person.third = some ∅
• Phi.Geometry.personNodes Person.zero = none

def Phi.Geometry.numberNodes (active : Finset Node) : Number → Option (Finset Node)

The number geometries, relative to an active inventory: singular is the bare Individuation node, with Minimal where the inventory activates it contrastively; plural adds Group; dual Minimal with Group; paucal and trial add Augmented; the number-neutral value is nothing. Greater numbers and the minimal–augmented values have no geometry.

Equations

• One or more equations did not get rendered due to their size.
• Phi.Geometry.numberNodes active Number.plural = some {Phi.Geometry.Node.individuation, Phi.Geometry.Node.group}
• Phi.Geometry.numberNodes active Number.dual = some {Phi.Geometry.Node.individuation, Phi.Geometry.Node.minimal, Phi.Geometry.Node.group}
• Phi.Geometry.numberNodes active Number.trial = some {Phi.Geometry.Node.individuation, Phi.Geometry.Node.minimal, Phi.Geometry.Node.group, Phi.Geometry.Node.augmented}
• Phi.Geometry.numberNodes active Number.paucal = some {Phi.Geometry.Node.individuation, Phi.Geometry.Node.minimal, Phi.Geometry.Node.group, Phi.Geometry.Node.augmented}
• Phi.Geometry.numberNodes active Number.general = some ∅
• Phi.Geometry.numberNodes active x✝ = none

def Phi.Geometry.cell (active : Finset Node) (p : Person) (n : Number) : Option (Finset Node)

The geometry of a person–number cell: the root with the person and number nodes, the latter only in an inventory that activates Individuation.

Equations

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

def Phi.Geometry.Licenses (active : Finset Node) (p : Person) (n : Number) : Prop

An inventory licenses a cell when the cell's geometry lies within it.

Equations

• Phi.Geometry.Licenses active p n = ∃ g ∈ Phi.Geometry.cell active p n, g ⊆ active

@[instance_reducible]

instance Phi.Geometry.instDecidableLicenses (active : Finset Node) (p : Person) (n : Number) : Decidable (Licenses active p n)

Equations

• Phi.Geometry.instDecidableLicenses active p n = Phi.Geometry.instDecidableLicenses._aux_1 active p n

theorem Phi.Geometry.personNodes_isLowerSet {p : Person} {ps : Finset Node} (h : personNodes p = some ps) : IsLowerSet ↑(insert ⊥ ps)

theorem Phi.Geometry.numberNodes_isLowerSet {active : Finset Node} {n : Number} {ns : Finset Node} (h : numberNodes active n = some ns) : IsLowerSet ↑(insert ⊥ ns)

theorem Phi.Geometry.cell_isLowerSet {active : Finset Node} {p : Person} {n : Number} {g : Finset Node} (h : cell active p n = some g) : IsLowerSet ↑g

Every assigned geometry is a lower set.