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 a feature geometry in the sense of [Cle85] and [Sag86] whose nodes are the features themselves, a rooted tree in mathlib's terms: dominance the partial order, the root ⊥ and the parent Order.pred.

Main definitions

• Node, Node.ancestors and Node.pred, and dominance ≤, the tree of the parent map 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.
• personFeatures: the nodes a person bears, the root and default daughter included.
• Licenses: an inventory licenses a cell when the cell's geometry lies within it.

Main results

• 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
• M. McGinnis, Agree and Fission in Georgian plurals
• 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 are the root, the three organizing nodes, and their dependents.

• referringExpression : Node

  The root is borne by every pronoun, and alone it is the third person.

• participant : Node

  Discourse participant marks the first and second person.

• speaker : Node

  Includes the speaker; Participant's default dependent.

• multispeaker : Node

  Multispeaker 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

  Group marks more than one, the plural.

• minimal : Node

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

• augmented : Node

  Augmented marks a minimal group and more, the 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.ancestors : Node → List Node

The nodes a node depends on, nearest first, form the path from the node to the root.

Equations

• Phi.Geometry.Node.referringExpression.ancestors = []
• Phi.Geometry.Node.participant.ancestors = [Phi.Geometry.Node.referringExpression]
• Phi.Geometry.Node.individuation.ancestors = [Phi.Geometry.Node.referringExpression]
• Phi.Geometry.Node.speaker.ancestors = [Phi.Geometry.Node.participant, Phi.Geometry.Node.referringExpression]
• Phi.Geometry.Node.addressee.ancestors = [Phi.Geometry.Node.participant, Phi.Geometry.Node.referringExpression]
• Phi.Geometry.Node.multispeaker.ancestors = [Phi.Geometry.Node.speaker, Phi.Geometry.Node.participant, Phi.Geometry.Node.referringExpression]
• Phi.Geometry.Node.group.ancestors = [Phi.Geometry.Node.individuation, Phi.Geometry.Node.referringExpression]
• Phi.Geometry.Node.minimal.ancestors = [Phi.Geometry.Node.individuation, Phi.Geometry.Node.referringExpression]
• Phi.Geometry.Node.nounClass.ancestors = [Phi.Geometry.Node.individuation, Phi.Geometry.Node.referringExpression]
• Phi.Geometry.Node.augmented.ancestors = [Phi.Geometry.Node.minimal, Phi.Geometry.Node.individuation, Phi.Geometry.Node.referringExpression]
• Phi.Geometry.Node.animate.ancestors = [Phi.Geometry.Node.nounClass, Phi.Geometry.Node.individuation, Phi.Geometry.Node.referringExpression]
• Phi.Geometry.Node.inanimate.ancestors = [Phi.Geometry.Node.nounClass, Phi.Geometry.Node.individuation, Phi.Geometry.Node.referringExpression]
• Phi.Geometry.Node.feminine.ancestors = [Phi.Geometry.Node.animate, Phi.Geometry.Node.nounClass, Phi.Geometry.Node.individuation, Phi.Geometry.Node.referringExpression]
• Phi.Geometry.Node.masculine.ancestors = [Phi.Geometry.Node.animate, Phi.Geometry.Node.nounClass, Phi.Geometry.Node.individuation, Phi.Geometry.Node.referringExpression]

def Phi.Geometry.Node.pred (n : Node) : Node

The node a node depends on directly, the root fixed.

Equations

• n.pred = n.ancestors.head?.getD n

@[instance_reducible]

instance Phi.Geometry.Node.instPartialOrder : PartialOrder Node

a ≤ b when b depends on a, the dominance of the geometry: a is b or one of the nodes b depends on.

Equations

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

@[instance_reducible]

instance Phi.Geometry.Node.instDecidableLE : DecidableLE Node

Equations

• a.instDecidableLE b = { decide := decide (a = b) || decide (a ∈ b.ancestors), reflects_decide := ⋯ }

@[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.instPredOrder : PredOrder Node

The parent as the predecessor.

Equations

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

@[instance_reducible]

instance Phi.Geometry.Node.instLocallyFiniteOrder : LocallyFiniteOrder Node

Equations

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

theorem Phi.Geometry.Node.le_iff {a b : Node} : a ≤ b ↔ a = b ∨ a ∈ b.ancestors

Dominance is dependence.

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

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

Equations

• n.below = (List.filter (fun (x : Phi.Geometry.Node) => decide (x ≠ ⊥)) (n :: n.ancestors)).reverse

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} : 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 daughters of the organizing nodes are Speaker, Minimal, and 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

Default fill-in gives an organizing node present without any dependent 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 → Finset Node

In 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.

Equations

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

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

In 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 is 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) : IsLowerSet ↑(insert ⊥ (personNodes p))

def Phi.Geometry.personFeatures (p : Person) : Finset Node

A person bears the root, the nodes of its person geometry, and the default daughter of a bare Participant node, so that the first person bears Speaker.

Equations

• Phi.Geometry.personFeatures p = Phi.Geometry.fillDefaults (insert ⊥ (Phi.Geometry.personNodes p))

theorem Phi.Geometry.bot_mem_personFeatures (p : Person) : ⊥ ∈ personFeatures p

theorem Phi.Geometry.personFeatures_isLowerSet (p : Person) : IsLowerSet ↑(personFeatures p)

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.