Person — referent semantics for the values

[Har16a] [DK00] [Cys09]

The denotation of a person value as a region of referents: over an ontology with speaker i and addressee u, each value constrains which of the two distinguished roles the referent (a Finset of individuals) includes. zero (impersonal) is context-dependent and gets none — the approximatives precedent of Number.interp.

The region semantics grounds the rest of the API:

• interp_resolve — coordination unions referents, and the regions are closed under it: a p-referent united with a q-referent lies in the resolve p q region. Person.resolve_profile's profile disjunction is the (i, u)-shadow of this fact (toProfile_sound).
• IsSAP is the region property "forces a speech-act participant" (isSAP_iff_forces).
• [Har16a]'s partition calculus generates exactly these regions — the certification theorem lives with the calculus in Studies/Harbour2016.lean (quad_cells_are_interp_regions); the marker-set rendering is [DK00]'s Fula encoding (Studies/DalrympleKaplan2000.lean, person_resolve_is_union).

def Person.interp {D : Type u_1} (i u : D) : Person → Option (Finset D → Prop)

The region of referents a person value picks out, over an ontology with speaker i and addressee u: first includes the speaker (addressee open — the tripartition cell), the quadripartition cells fix both roles, zero is context-dependent (none).

Equations

• Person.interp i u Person.first = some fun (s : Finset D) => i ∈ s
• Person.interp i u Person.firstInclusive = some fun (s : Finset D) => i ∈ s ∧ u ∈ s
• Person.interp i u Person.firstExclusive = some fun (s : Finset D) => i ∈ s ∧ u ∉ s
• Person.interp i u Person.second = some fun (s : Finset D) => u ∈ s ∧ i ∉ s
• Person.interp i u Person.third = some fun (s : Finset D) => i ∉ s ∧ u ∉ s
• Person.interp i u Person.zero = none

def Person.region {D : Type u_1} (i u : D) (p : Person) : Finset D → Prop

The region, with the empty region for zero.

Equations

• Person.region i u p = (Person.interp i u p).getD fun (x : Finset D) => False

@[implicit_reducible]

instance Person.instDecidableRegion {D : Type u_1} [DecidableEq D] (i u : D) (p : Person) (s : Finset D) : Decidable (region i u p s)

Equations

• Person.instDecidableRegion i u Person.first s = Person.instDecidableRegion._aux_1 i u s
• Person.instDecidableRegion i u Person.firstInclusive s = Person.instDecidableRegion._aux_3 i u s
• Person.instDecidableRegion i u Person.firstExclusive s = Person.instDecidableRegion._aux_5 i u s
• Person.instDecidableRegion i u Person.second s = Person.instDecidableRegion._aux_7 i u s
• Person.instDecidableRegion i u Person.third s = Person.instDecidableRegion._aux_9 i u s
• Person.instDecidableRegion i u Person.zero s = isFalse ⋯

theorem Person.interp_isSome_iff {D : Type u_1} [DecidableEq D] (i u : D) (p : Person) : (interp i u p).isSome = true ↔ p ≠ zero

interp is defined exactly off the impersonal.

theorem Person.interp_resolve {D : Type u_1} [DecidableEq D] (i u : D) (p q : Person) : p ≠ zero → q ≠ zero → ∀ (s t : Finset D), region i u p s → region i u q t → region i u (p.resolve q) (s ∪ t)

Resolution is referent union: the regions are closed under coordination — a p-referent united with a q-referent is a resolve p q-referent. The resolution table of Features/Person/Resolve.lean is the shadow of this closure.

theorem Person.toProfile_speaker {D : Type u_1} [DecidableEq D] (i u : D) (p : Person) (pr : Profile) : p.toProfile = some pr → ∀ (s : Finset D), region i u p s → (pr.speaker = true ↔ i ∈ s)

The profile of Features/Person/Resolve.lean is the (i, u)-shadow of the region: speaker records whether the region forces i ∈ s, and a determinate addressee slot records the forced u-status.

theorem Person.toProfile_addressee {D : Type u_1} [DecidableEq D] (i u : D) (p : Person) (pr : Profile) (b : Bool) : p.toProfile = some pr → pr.addressee = some b → ∀ (s : Finset D), region i u p s → (u ∈ s ↔ b = true)

A determinate addressee slot records the forced u-status of the region.

theorem Person.isSAP_iff_forces {D : Type u_1} [DecidableEq D] (i u : D) (p : Person) : p ≠ zero → (p.IsSAP ↔ ∀ (s : Finset D), region i u p s → i ∈ s ∨ u ∈ s)

IsSAP is the semantic property "the region forces a speech-act participant in the referent": first/second persons do, third does not (the empty referent witnesses).

theorem Person.region_coarsen {D : Type u_1} (i u : D) (p : Person) (s : Finset D) : region i u p s → region i u p.coarsen s

Coarsening widens the region: dropping clusivity loses information, never referents.