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.

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

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.