Person — resolution

[Cor06] [Zwi77] [DK00]

Resolution in coordination: the person of a coordinate structure from the persons of its conjuncts (you and I → first inclusive). The canonical table returns the finest analytical value (first + second = firstInclusive); systems without the distinction coarsen via resolveIn, exactly as Number.resolve's canonical dual coarsens to plural in {sg, pl} systems.

The table is not stipulated: resolve_profile derives it from referent union. A person value constrains which discourse roles the referent includes (Profile: speaker yes/no, addressee yes/no/underdetermined — the tripartition first leaves the addressee slot open), and coordination unions referents — so resolution is pointwise disjunction on profiles, [DK00]'s set-union semantics for person resolution. The Zwicky hierarchy (1 < 2 < 3, [Zwi77]) falls out: in a tripartition system, resolution is minimum of hierarchyRank (resolveIn_tripartition_min).

zero (impersonal) does not participate in attested resolution; it is treated as an identity by convention (documented, not an empirical claim).

Canonical resolution

def Person.resolve : Person → Person → Person

Canonical person resolution: the finest analytical value for the coordination of two referents. Speaker inclusion dominates; coordination with the addressee yields the inclusive. zero is an identity by convention.

Equations

• Person.zero.resolve x✝ = x✝
• x✝.resolve Person.zero = x✝
• Person.firstInclusive.resolve x✝ = Person.firstInclusive
• x✝.resolve Person.firstInclusive = Person.firstInclusive
• Person.first.resolve Person.second = Person.firstInclusive
• Person.second.resolve Person.first = Person.firstInclusive
• Person.firstExclusive.resolve Person.second = Person.firstInclusive
• Person.second.resolve Person.firstExclusive = Person.firstInclusive
• Person.first.resolve x✝ = Person.first
• x✝.resolve Person.first = Person.first
• Person.firstExclusive.resolve x✝ = Person.firstExclusive
• x✝.resolve Person.firstExclusive = Person.firstExclusive
• Person.second.resolve x✝ = Person.second
• x✝.resolve Person.second = Person.second
• Person.third.resolve Person.third = Person.third

theorem Person.resolve_comm (a b : Person) : a.resolve b = b.resolve a

theorem Person.resolve_assoc (a b c : Person) : (a.resolve b).resolve c = a.resolve (b.resolve c)

@[simp]

theorem Person.resolve_zero_left (p : Person) : zero.resolve p = p

@[simp]

theorem Person.resolve_zero_right (p : Person) : p.resolve zero = p

The grounding: resolution is referent union

A person value constrains the discourse roles in the referent. The profile records speaker inclusion (determinate for every value) and addressee inclusion (none = underdetermined: the tripartition first says nothing about the addressee). Coordination unions referents, so the resolved profile is the pointwise disjunction — with none ∨ false = none: if one conjunct's addressee status is open, so is the coordination's.

structure Person.Profile : Type

Discourse-role inclusion profile of a (non-impersonal) person value.

• speaker : Bool

  The referent includes the speaker.

• addressee : Option Bool

  The referent includes the addressee; none = underdetermined.

def Person.instDecidableEqProfile.decEq (x✝ x✝¹ : Profile) : Decidable (x✝ = x✝¹)

Equations

• Person.instDecidableEqProfile.decEq { speaker := a, addressee := a_1 } { speaker := b, addressee := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance Person.instDecidableEqProfile : DecidableEq Profile

Equations

• Person.instDecidableEqProfile = Person.instDecidableEqProfile.decEq

def Person.instReprProfile.repr : Profile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Person.instReprProfile : Repr Profile

Equations

• Person.instReprProfile = { reprPrec := Person.instReprProfile.repr }

def Person.toProfile : Person → Option Profile

The profile of each value; zero constrains roles in a context-dependent way and has none.

Equations

• Person.first.toProfile = some { speaker := true, addressee := none }
• Person.firstInclusive.toProfile = some { speaker := true, addressee := some true }
• Person.firstExclusive.toProfile = some { speaker := true, addressee := some false }
• Person.second.toProfile = some { speaker := false, addressee := some true }
• Person.third.toProfile = some { speaker := false, addressee := some false }
• Person.zero.toProfile = none

def Person.Profile.or (p q : Profile) : Profile

Profiles of unions: pointwise disjunction (three-valued on the addressee slot).

Equations

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

theorem Person.resolve_profile (p q : Person) : p ≠ zero → q ≠ zero → (p.resolve q).toProfile = p.toProfile.bind fun (pp : Profile) => Option.map pp.or q.toProfile

The resolution table is referent union ([DK00]): for referential persons, the profile of the resolved value is the disjunction of the conjuncts' profiles. The table is derived, not stipulated.

theorem Person.toProfile_injOn (p q : Person) : p ≠ zero → q ≠ zero → p.toProfile = q.toProfile → p = q

Distinct values have distinct profiles: the referential inventory is exactly the profile space reachable from referents.

System-relative resolution

def Person.coarsenTo (sys : List Person) (p : Person) : Person

Coarsen a value into a system: keep it if present, else collapse clusivity.

Equations

• Person.coarsenTo sys p = if p ∈ sys then p else if p.coarsen ∈ sys then p.coarsen else p

def Person.resolveIn (sys : List Person) (a b : Person) : Person

Resolution within a system: canonical resolution, coarsened.

Equations

• Person.resolveIn sys a b = Person.coarsenTo sys (a.resolve b)

theorem Person.resolveIn_comm (sys : List Person) (a b : Person) : resolveIn sys a b = resolveIn sys b a

def Person.System.resolve (ns : System) (a b : Person) : Person

Resolution typed by a Person.System.

Equations

• ns.resolve a b = Person.resolveIn ns.values a b

theorem Person.resolve_quadripartition_incl : System.quadripartition.resolve firstExclusive second = firstInclusive

In a clusivity system: you and I resolves to the inclusive.

theorem Person.resolve_tripartition_first : System.tripartition.resolve first second = first

In a tripartition system the canonical inclusive coarsens to plain first: English you and I → we.

theorem Person.resolveIn_tripartition_min (p q : Person) : p ∈ System.tripartition.values → q ∈ System.tripartition.values → (System.tripartition.resolve p q).hierarchyRank = min p.hierarchyRank q.hierarchyRank

The Zwicky hierarchy as a corollary ([Zwi77]): in a tripartition system, resolution is minimum of hierarchyRank — 1 < 2 < 3 is not a primitive but the shadow of referent union.