Hudson 2010: kinship as an inheritance network @cite{hudson-2010}

The "one network" thesis: Word Grammar models all conceptual knowledge — linguistic and non-linguistic alike — as a single inheritance network of isA links and labelled property relations. The kinship system is Hudson's running non-linguistic example (§3.2 with Fig 3.7, cross-referenced from §7.2.6 "Syntactic triangles" on p. 160) and serves as the foil for the syntactic triangle of Figure 7.6 (p. 161, "A triangle in syntax and in kinship").

This study file is the Phenomena-level demonstration that the same Core.Inheritance.Network infrastructure used by WordGrammar.englishAuxNet also supports a kinship hierarchy. Two demos:

1. A small kinship taxonomy as a Network, with isA links (mother isA parent, parent isA ancestor), described by the same propositional IsA relation and the same parents/ancestors computational helpers used by WordGrammar.englishAuxNet.
2. The Fig 7.6 triangle pattern: grandparentOf is the relational composition parentOf ∘r parentOf (mathlib's Relation.Comp) — the same shape Hudson uses for syntactic raising (HAVE's subject is also the subject of HAVE's valent).

The point is structural: a single Network α R type carries both the syntactic word-class hierarchy of WordGrammar.englishAuxNet (over nodes typed by linguistic categories) and the kinship taxonomy below (over nodes typed by KinRole). No Bridge theorem is needed — the identity is by construction at the level of the type Network.

inductive Phenomena.Kinship.Studies.Hudson2010.KinRole : Type

Atomic kinship roles. The taxonomy: grandmother and grandfather are grandparents; mother and father are parents; parents and grandparents are ancestors.

• mother : KinRole
• father : KinRole
• parent : KinRole
• grandmother : KinRole
• grandfather : KinRole
• grandparent : KinRole
• ancestor : KinRole

@[implicit_reducible]

instance Phenomena.Kinship.Studies.Hudson2010.instReprKinRole : Repr KinRole

Equations

• Phenomena.Kinship.Studies.Hudson2010.instReprKinRole = { reprPrec := Phenomena.Kinship.Studies.Hudson2010.instReprKinRole.repr }

def Phenomena.Kinship.Studies.Hudson2010.instReprKinRole.repr : KinRole → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Kinship.Studies.Hudson2010.instDecidableEqKinRole : DecidableEq KinRole

Equations

• Phenomena.Kinship.Studies.Hudson2010.instDecidableEqKinRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Kinship.Studies.Hudson2010.kinshipNet : Core.Inheritance.Network KinRole Empty

A small kinship inheritance network. All links are isA edges; the taxonomy is mother / father → parent, grandmother / grandfather → grandparent, and parent / grandparent → ancestor. The relation-label type is Empty: there are no prop links here, only the isA backbone, so no labels are reachable. The Fig 7.6 triangle below uses an abstract ParentRel α rather than a network prop link, so no kinship-specific label type is needed.

Equations

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

theorem Phenomena.Kinship.Studies.Hudson2010.mother_IsA_parent : Core.Inheritance.IsA kinshipNet KinRole.mother KinRole.parent

A mother is a parent (one step).

theorem Phenomena.Kinship.Studies.Hudson2010.mother_IsA_ancestor : Core.Inheritance.IsA kinshipNet KinRole.mother KinRole.ancestor

A mother is an ancestor (two steps via parent).

theorem Phenomena.Kinship.Studies.Hudson2010.grandmother_IsA_ancestor : Core.Inheritance.IsA kinshipNet KinRole.grandmother KinRole.ancestor

A grandmother is an ancestor (two steps via grandparent).

theorem Phenomena.Kinship.Studies.Hudson2010.mother_not_IsA_grandmother : ¬Core.Inheritance.IsA kinshipNet KinRole.mother KinRole.grandmother

A mother is not a grandmother — the taxonomy doesn't conflate the two, even though both are ancestors. Now stated as the full propositional ¬ IsA kinshipNet .mother .grandmother, decidable thanks to path compression landed in Core.Inheritance.Basic.

theorem Phenomena.Kinship.Studies.Hudson2010.ancestor_has_no_proper_ancestors : Core.Inheritance.ancestors kinshipNet KinRole.ancestor = []

The ancestor node sits at the top: nothing is its ancestor.

theorem Phenomena.Kinship.Studies.Hudson2010.mother_le_ancestor : Core.Inheritance.IsAOrder.mk kinshipNet KinRole.mother ≤ Core.Inheritance.IsAOrder.mk kinshipNet KinRole.ancestor

The same fact as mother_IsA_ancestor via mathlib's ≤. The IsAOrder.mk wrapper tags the nodes as inhabiting the preorder view of kinshipNet, so instance search picks up the Preorder (IsAOrder kinshipNet) instance instead of unfolding to KinRole and looking for the (nonexistent) LE KinRole.

@[reducible, inline]

abbrev Phenomena.Kinship.Studies.Hudson2010.ParentRel (α : Type) : Type

The "parent of" relation between people. Modelled abstractly as a binary relation over an arbitrary type of individuals.

Equations

• Phenomena.Kinship.Studies.Hudson2010.ParentRel α = (α → α → Prop)

@[reducible, inline]

abbrev Phenomena.Kinship.Studies.Hudson2010.grandparentOf {α : Type} (parentOf : ParentRel α) : α → α → Prop

grandparentOf is the relational composition of parentOf with itself — the kinship side of @cite{hudson-2010}'s Figure 7.6 (p. 161): "my grandmother is someone who is the mother of one of my parents". This is mathlib's Relation.Comp, not a fresh definition.

Equations

• Phenomena.Kinship.Studies.Hudson2010.grandparentOf parentOf = Relation.Comp parentOf parentOf

Hudson's kinship instance of Fig 7.6: the triangle commutes by definition, since grandparentOf is parentOf ∘r parentOf.

theorem Phenomena.Kinship.Studies.Hudson2010.kinship_triangle_commutes {α : Type} (parentOf : ParentRel α) (a c : α) : grandparentOf parentOf a c ↔ ∃ (b : α), parentOf a b ∧ parentOf b c

The triangle for kinship commutes by definition. This is the formal counterpart of Hudson's prose on p. 160 (§7.2.6): "my grandmother is someone who is the mother of one of my parents".

theorem Phenomena.Kinship.Studies.Hudson2010.kinship_triangle_witness {α : Type} (parentOf : ParentRel α) (a b c : α) (h1 : parentOf a b) (h2 : parentOf b c) : grandparentOf parentOf a c

Given an apex grandparent a, an intermediate parent b, and a base person c, the composition witness exists.