Person Feature Geometry [HR02] [BR03]

[BR09] [Pre14] [PZ18]

The privative-feature geometry [HR02] decomposes person into a containment hierarchy where each sub-feature implies the next:

[φ] → [PERSON] → [participant] → [author]
[φ] → [NUMBER] → [plural]

This decomposition drives relativized probing ([Pre14] §4.2, recalling [Riz90]'s Relativized Minimality): a probe seeking [participant] skips DPs that lack it (3rd person), targeting only 1st/2nd person DPs. A separate probe seeking [plural] skips DPs that lack it (singulars), targeting only plurals.

[BR03] introduce the split π/# probes (person probing first) and the Person Licensing Condition, deriving the Person Case Constraint with an unrelativized π-probe — the dative matches it and absorbs it (see Studies/BejarRezac2003.lean); [BR09] develop the system into Cyclic Agree. [Pre14] §4.4 ports the split-probe + PLC system to Kichean Agent Focus, adding the relativization of π⁰ to [participant] and #⁰ to [plural] — reframing earlier "omnivorous hierarchy" accounts. [Pre14] Ch. 7 then argues against direct hierarchy/scale primitives like [+participant] > [+plural] > default, on five grounds: restrictedness of "salience" effects to AF, K'ichee' formal addressee la (a 2nd-person form patterning as 3rd-person under AF), the AF person restriction (1+2 blocked but 3pl+3pl licit), the morphophonological 1st/2nd vs 3rd asymmetry (clitic doubling vs direct exponence, [Pre14] §3.4 and §4.4), and the Zulu parallel ([Hal12]: the same machinery over augmented/augmentless). The relativized-probing mechanism derives the same surface patterns without committing to a salience scale.

Extended Geometry: [±proximate]

[PZ18] extend the hierarchy with a [±proximate] feature for the Person Case Constraint:

[+author] ⊂ [+participant] ⊂ [+proximate]

1P and 2P are inherently [+proximate]. 3P arguments are [-proximate] by default but can be contextually marked [+proximate] (when co-occurring with another 3P). The [±proximate] distinction also captures the 3P proximate/obviative split in direct/inverse alignment systems ([PZ18] §2.1 (11)).

Relationship to Core PersonFeatures

DecomposedPerson extends Person.Features (the framework-neutral [±participant, ±author] decomposition) with the Minimalism-specific [±proximate] feature. The two-feature core is shared across all theoretical frameworks; [±proximate] is specific to [PZ18]'s P-Constraint.

Person Type

decomposePerson takes Person (.first | .second |.third) — the canonical person type shared across the library — rather than a raw Nat. This eliminates meaningless person values and grounds the decomposition in the same type used by DifferentialIndexing, Prominence.PersonLevel.isSAP, etc.

Note on probeResolutionRank

The probeResolutionRank function below assigns rank 2 to [+participant] DPs, rank 1 to [+plural, −participant] DPs, and rank 0 elsewhere — the surface effect of the two-probe (π⁰ before #⁰) system on a single DP. Its derived status is a theorem: target resolution is Probe.cascade over the two probes (Probe/Basic.lean), and the rank comparison agrees with the cascade on the φ-cell inventory (Preminger2014.afAgreementTarget_eq_rank). It is not a salience scale ([Pre14] Ch. 7).

structure Minimalist.DecomposedPersonextends Person.Features : Type

Person features decomposed according to [Pre14]'s geometry, extended with [±proximate] from [PZ18].

Extends Person.Features (the framework-neutral [±participant, ±author] core) with the Minimalism-specific [±proximate] feature:

• [proximate] marks potential point-of-view centers. 1P/2P are inherently [+proximate]; 3P can be contextually [+proximate].
• [participant] distinguishes 1st/2nd from 3rd person.
• [author] distinguishes 1st from 2nd person.

The geometry imposes a containment hierarchy: [+author] → [+participant] → [+proximate]

Note: The paper treats these as privative features: 3rd person simply LACKS [participant], rather than bearing [−participant]. We encode this as Bool for computational convenience; the well-formedness constraint wellFormed ensures the privative entailments are maintained.

• hasParticipant : Bool
• hasAuthor : Bool
• hasProximate : Bool

  Bears [proximate]? SAPs inherently; 3P contextually.

@[implicit_reducible]

instance Minimalist.instDecidableEqDecomposedPerson : DecidableEq DecomposedPerson

Equations

• Minimalist.instDecidableEqDecomposedPerson = Minimalist.instDecidableEqDecomposedPerson.decEq

def Minimalist.instDecidableEqDecomposedPerson.decEq (x✝ x✝¹ : DecomposedPerson) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Minimalist.instReprDecomposedPerson : Repr DecomposedPerson

Equations

• Minimalist.instReprDecomposedPerson = { reprPrec := Minimalist.instReprDecomposedPerson.repr }

def Minimalist.instReprDecomposedPerson.repr : DecomposedPerson → ℕ → Std.Format

Equations

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

def Minimalist.DecomposedPerson.wellFormed (dp : DecomposedPerson) : Bool

Geometry well-formedness: [author] → [participant] → [proximate]. Each feature entails the next in the containment hierarchy.

Equations

• dp.wellFormed = ((!dp.hasAuthor || dp.hasParticipant) && (!dp.hasParticipant || dp.hasProximate))

def Minimalist.decomposePerson : Person → DecomposedPerson

Decompose a person value into sub-features.

• 1st person: [+proximate, +participant, +author]
• 2nd person: [+proximate, +participant, −author]
• 3rd person: [−proximate, −participant, −author]

3rd person is [-proximate] by default; contextual [+proximate] marking is handled by the P-Constraint evaluation.

Equations

• Minimalist.decomposePerson Person.first = { hasParticipant := true, hasAuthor := true, hasProximate := true }
• Minimalist.decomposePerson Person.firstInclusive = { hasParticipant := true, hasAuthor := true, hasProximate := true }
• Minimalist.decomposePerson Person.firstExclusive = { hasParticipant := true, hasAuthor := true, hasProximate := true }
• Minimalist.decomposePerson Person.second = { hasParticipant := true, hasAuthor := false, hasProximate := true }
• Minimalist.decomposePerson Person.third = { hasParticipant := false, hasAuthor := false, hasProximate := false }
• Minimalist.decomposePerson Person.zero = { hasParticipant := false, hasAuthor := false, hasProximate := false }

inductive Minimalist.Probe.Target : Type

What a phi-probe seeks.

In the AF construction, two probes operate:

• π⁰ seeks [participant]: targets 1st/2nd person DPs
• #⁰ seeks [plural]: targets plural DPs

π⁰ is merged below #⁰ and probes first — person-before-number probing, inherited from [BR03].

• participant : Target

  π⁰: person probe, seeks [participant].

• plural : Target

  #⁰: number probe, seeks [plural].

@[implicit_reducible]

instance Minimalist.Probe.instDecidableEqTarget : DecidableEq Target

Equations

• Minimalist.Probe.instDecidableEqTarget x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Minimalist.Probe.instReprTarget : Repr Target

Equations

• Minimalist.Probe.instReprTarget = { reprPrec := Minimalist.Probe.instReprTarget.repr }

def Minimalist.Probe.instReprTarget.repr : Target → ℕ → Std.Format

Equations

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

def Minimalist.probeVisible (target : Probe.Target) (person : Person) (isPlural : Bool) : Bool

Is a DP visible to this probe? Relativized probing: probes skip DPs that lack the feature they seek.

A DP with person value person and number isPlural is visible to the probe iff it bears the probe's target feature.

Equations

• Minimalist.probeVisible Minimalist.Probe.Target.participant person isPlural = (Minimalist.decomposePerson person).hasParticipant
• Minimalist.probeVisible Minimalist.Probe.Target.plural person isPlural = isPlural

def Minimalist.probeResolutionRank (person : Person) (isPlural : Bool) : ℕ

Probe resolution rank for a DP under the two-probe (π⁰ ≫ #⁰) system.

A surface-effect summary of which probe targets a given DP:

• Rank 2: visible to π⁰ ([+participant])
• Rank 1: visible to #⁰ but not π⁰ ([+plural, −participant])
• Rank 0: invisible to both probes (3SG default)

Derived from the probing mechanism ([BR03]), not stipulated as a salience scale: π⁰ is merged below #⁰ and probes earlier in the derivation, its clitic output beats other exponence in the single morphological slot, and each probe targets any DP bearing the sought feature. The rank captures the combined effect on a single DP; its derived status is Preminger2014.afAgreementTarget_eq_rank (cascade resolution, Probe/Basic.lean). It is not a salience scale ([Pre14] Ch. 7).

Equations

• Minimalist.probeResolutionRank person isPlural = if (Minimalist.decomposePerson person).hasParticipant = true then 2 else if isPlural = true then 1 else 0

theorem Minimalist.all_decompositions_wellFormed (p : Person) : (decomposePerson p).wellFormed = true

All person values yield well-formed decompositions.

theorem Minimalist.decomposePerson_toFeatures_eq (p : Person) (f : Person.Features) : p.toFeatures = some f → (decomposePerson p).toFeatures = f

decomposePerson is consistent with the framework-neutral Person.toFeatures: the [±participant, ±author] core of the Minimalist decomposition agrees with Core Person.Features.

theorem Minimalist.rank_hierarchy : probeResolutionRank Person.first false > probeResolutionRank Person.third true ∧ probeResolutionRank Person.third true > probeResolutionRank Person.third false

Rank is monotone in the probe hierarchy: any DP visible to π⁰ (rank 2) outranks any DP visible only to #⁰ (rank 1), which outranks any DP invisible to both (rank 0).