Privative Feature Pairs

@cite{harbour-2016}

A neutral abstraction over pairs of privative features with containment: the inner feature entails the outer feature ([+inner] → [+outer]).

This pattern recurs across the two φ-feature domains established in @cite{harbour-2016}:

• Person: [±author] (inner) ⊂ [±participant] (outer)
• Number: [±atomic] (inner) ⊂ [±minimal] (outer)

In each case, the containment constraint rules out one of the four Boolean combinations, yielding exactly three well-formed cells:

outer	inner	Status	Person	Number
+	+	most specified	1st person	singular
+	−	intermediate	2nd person	dual
−	−	least specified	3rd person	plural
−	+	ill-formed	—	—

@cite{harbour-2016} calls this shared skeleton the phi kernel: the same formal mechanism generates the partition structure of both person and number.

structure Features.PrivativePair : Type

A pair of privative features with a containment relation.

inner entails outer: bearing the inner feature requires bearing the outer feature. The four Boolean combinations reduce to three well-formed cells:

• ⟨true, true⟩ — [+outer, +inner] (most specified)
• ⟨true, false⟩ — [+outer, −inner] (intermediate)
• ⟨false, false⟩ — [−outer, −inner] (least specified)

The fourth combination ⟨false, true⟩ ([−outer, +inner]) violates containment.

Instances:

• Features.Person.Features: outer = hasParticipant, inner = hasAuthor
• Features.Number.Features: outer = isMinimal, inner = isAtomic

• outer : Bool

  The entailed (outer) feature.

• inner : Bool

  The entailing (inner) feature — implies outer.

def Features.instDecidableEqPrivativePair.decEq (x✝ x✝¹ : PrivativePair) : Decidable (x✝ = x✝¹)

Equations

• Features.instDecidableEqPrivativePair.decEq { outer := a, inner := a_1 } { outer := b, inner := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance Features.instDecidableEqPrivativePair : DecidableEq PrivativePair

Equations

• Features.instDecidableEqPrivativePair = Features.instDecidableEqPrivativePair.decEq

@[implicit_reducible]

instance Features.instReprPrivativePair : Repr PrivativePair

Equations

• Features.instReprPrivativePair = { reprPrec := Features.instReprPrivativePair.repr }

def Features.instReprPrivativePair.repr : PrivativePair → Nat → Std.Format

Equations

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

def Features.instInhabitedPrivativePair.default : PrivativePair

Equations

• Features.instInhabitedPrivativePair.default = { outer := default, inner := default }

@[implicit_reducible]

instance Features.instInhabitedPrivativePair : Inhabited PrivativePair

Equations

• Features.instInhabitedPrivativePair = { default := Features.instInhabitedPrivativePair.default }

def Features.instBEqPrivativePair.beq : PrivativePair → PrivativePair → Bool

Equations

• Features.instBEqPrivativePair.beq { outer := a, inner := a_1 } { outer := b, inner := b_1 } = (a == b && a_1 == b_1)
• Features.instBEqPrivativePair.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Features.instBEqPrivativePair : BEq PrivativePair

Equations

• Features.instBEqPrivativePair = { beq := Features.instBEqPrivativePair.beq }

def Features.PrivativePair.wellFormed (p : PrivativePair) : Bool

Well-formedness: [+inner] → [+outer]. The inner feature entails the outer feature.

Equations

• p.wellFormed = (!p.inner || p.outer)

def Features.PrivativePair.maximal : PrivativePair

Most specified cell: [+outer, +inner]. Person: 1st (speaker). Number: singular (atom).

Equations

• Features.PrivativePair.maximal = { outer := true, inner := true }

def Features.PrivativePair.intermediate : PrivativePair

Intermediate cell: [+outer, −inner]. Person: 2nd (non-speaker participant). Number: dual (minimal non-atom).

Equations

• Features.PrivativePair.intermediate = { outer := true, inner := false }

def Features.PrivativePair.minimal : PrivativePair

Least specified cell: [−outer, −inner]. Person: 3rd (non-participant). Number: plural (non-minimal non-atom).

Equations

• Features.PrivativePair.minimal = { outer := false, inner := false }

@[simp]

theorem Features.PrivativePair.maximal_wellFormed : maximal.wellFormed = true

@[simp]

theorem Features.PrivativePair.intermediate_wellFormed : intermediate.wellFormed = true

@[simp]

theorem Features.PrivativePair.minimal_wellFormed : minimal.wellFormed = true

theorem Features.PrivativePair.illFormed_unique : { outer := false, inner := true }.wellFormed = false

The unique ill-formed combination.

theorem Features.PrivativePair.exactly_three : (List.filter wellFormed [{ outer := true, inner := true }, { outer := true, inner := false }, { outer := false, inner := true }, { outer := false, inner := false }]).length = 3

There are exactly 3 well-formed combinations.

theorem Features.PrivativePair.classification (p : PrivativePair) (h : p.wellFormed = true) : p = maximal ∨ p = intermediate ∨ p = minimal

Every well-formed pair is one of the three canonical cells.

theorem Features.PrivativePair.inner_implies_outer (p : PrivativePair) (h : p.wellFormed = true) (hi : p.inner = true) : p.outer = true

Inner feature entails outer for well-formed pairs.

def Features.PrivativePair.specLevel (p : PrivativePair) : Nat

Specification level: counts the number of positive features. Maximal = 2, intermediate = 1, minimal = 0.

This defines a natural linear order on the three cells: more specified means more privative features are present.

Equations

• p.specLevel = p.outer.toNat + p.inner.toNat

@[simp]

theorem Features.PrivativePair.spec_maximal : maximal.specLevel = 2

@[simp]

theorem Features.PrivativePair.spec_intermediate : intermediate.specLevel = 1

@[simp]

theorem Features.PrivativePair.spec_minimal : minimal.specLevel = 0

theorem Features.PrivativePair.spec_strict_order : maximal.specLevel > intermediate.specLevel ∧ intermediate.specLevel > minimal.specLevel

Specification is strictly ordered across cells.

theorem Features.PrivativePair.no_four_way (a b c d : PrivativePair) : a.wellFormed = true → b.wellFormed = true → c.wellFormed = true → d.wellFormed = true → a ≠ b → a ≠ c → a ≠ d → b ≠ c → b ≠ d → c ≠ d → False

No four-way distinction. Any partition based on a privative pair has at most 3 cells. This is the core impossibility result: a single privative pair cannot support a 4-way contrast.

For person: no language has a 4-way singular person distinction. For number: no language has a 4-way base number distinction from two features alone.

class Features.PhiFeatures (α : Type) : Type

Any type that is isomorphic to PrivativePair.

Person.Features and Number.Features instantiate this class, inheriting no_four_way, classification, specLevel, etc. by construction — no per-domain bridge theorems needed.

• toPair : α → PrivativePair

  Embed into the canonical privative pair.

• ofPair : PrivativePair → α

  Recover from the canonical privative pair.

• roundtrip (a : α) : ofPair (toPair a) = a

  Round-trip: ofPair ∘ toPair = id.

theorem Features.PhiFeatures.injective {α : Type} [inst : PhiFeatures α] : Function.Injective toPair

The embedding is injective (follows from roundtrip).

def Features.PhiFeatures.wellFormed {α : Type} [inst : PhiFeatures α] (a : α) : Bool

Well-formedness via the embedding.

Equations

• Features.PhiFeatures.wellFormed a = (Features.PhiFeatures.toPair a).wellFormed

theorem Features.PhiFeatures.no_four_way {α : Type} [inst : PhiFeatures α] [DecidableEq α] (a b c d : α) (ha : wellFormed a = true) (hb : wellFormed b = true) (hc : wellFormed c = true) (hd : wellFormed d = true) (hab : a ≠ b) (hac : a ≠ c) (had : a ≠ d) (hbc : b ≠ c) (hbd : b ≠ d) (hcd : c ≠ d) : False

No 4-way distinction for any PhiFeatures instance.

def Features.PhiFeatures.specLevel {α : Type} [inst : PhiFeatures α] (a : α) : Nat

Specification level via the embedding.

Equations

• Features.PhiFeatures.specLevel a = (Features.PhiFeatures.toPair a).specLevel