Hammerly (2023): A set-based semantics for person, obviation, and animacy

[Ham23] derives the person partitions from bivalent features denoting first-order predicates, following the contrastive account of [CH19]. A feature denotes a set of ontological primitives, [Author] the speaker and [Participant] the speaker and the addressee (21), and composes with a lattice of referents by keeping those containing some member of that set or those containing none (24). Which features are active, and how they are read, follows from the successive division algorithm (26): a learner divides the inventory feature by feature until every category is distinguished, and a feature applies only where it makes a contrast (28), (29). Under [+Author] the participant feature makes no contrast, since every referent there contains the speaker, so a learner facing a clusivity contrast narrows it to [Participant*], 'includes a participant other than the speaker', in effect an addressee feature (p. 55). The account derives all and only the five partitions of [Har16a] (p. 55). Since [Participant] and [Participant*] are never active together, the tripartition grouping inclusive with second person, which a free addressee feature would generate, is excluded ((60), p. 72).

Main definitions

• Hammerly2023.Feature: [Author], [Participant] and the narrowed [Participant*].
• Hammerly2023.divide, Hammerly2023.sda: the successive division algorithm.
• Hammerly2023.Admissible: a contrastive hierarchy whose features all contrast and whose narrowing is licensed.

Main results

• image_graph_sda_eq_geometry: the admissible hierarchies derive exactly the partitions Harbour's bivalent geometry (9) generates, his five.
• sda_participant_author, sda_author_participantStar: the hierarchies of Figures 4 and 5, the tripartition and the quadripartition.
• not_admissible_participant_participantStar, not_admissible_participantStar: narrowing alongside the wide feature, or where the wide feature contrasts, is not licensed.

Implementation notes

Only the core persons of §3 are formalized, on participant sets, with the obviation and animacy features of §4 left aside. A hierarchy is a list of features, its order the contrastive scope; since the features denote first-order predicates, their order of composition does not matter (p. 52). Narrowing is licensed where the wide [Participant] would leave some cell undivided, the situation of the [+Author] cell in Figure 5.

References

• [Ham23]
• [CH19]
• [Har16a]

Features as first-order predicates (§3.1)

inductive Hammerly2023.Feature : Type

The person features: [Author], [Participant], and [Participant*], the participant feature narrowed under [+Author] (p. 55).

• author : Feature
• participant : Feature
• participantStar : Feature

@[instance_reducible]

instance Hammerly2023.instDecidableEqFeature : DecidableEq Feature

Equations

• Hammerly2023.instDecidableEqFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Hammerly2023.instFintypeFeature : Fintype Feature

Equations

• Hammerly2023.instFintypeFeature = { elems := { val := ↑Hammerly2023.Feature.enumList, nodup := Hammerly2023.Feature.enumList_nodup }, complete := Hammerly2023.instFintypeFeature._proof_1 }

def Hammerly2023.instReprFeature.repr : Feature → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Hammerly2023.instReprFeature : Repr Feature

Equations

• Hammerly2023.instReprFeature = { reprPrec := Hammerly2023.instReprFeature.repr }

def Hammerly2023.Feature.denotation : Feature → Finset Discourse.Role

The set a feature denotes (21): the speaker for [Author], the speaker and the addressee for [Participant], and the addressee alone for [Participant*].

Equations

• Hammerly2023.Feature.author.denotation = {Discourse.Role.speaker}
• Hammerly2023.Feature.participant.denotation = {Discourse.Role.speaker, Discourse.Role.addressee}
• Hammerly2023.Feature.participantStar.denotation = {Discourse.Role.addressee}

def Hammerly2023.Feature.Positive (f : Feature) (s : Finset Discourse.Role) : Prop

Positive composition keeps the referents containing some member of the feature's set (24a); negative composition keeps the others (24b).

Equations

• f.Positive s = (s ∩ f.denotation).Nonempty

@[instance_reducible]

instance Hammerly2023.instDecidablePredFinsetRolePositive (f : Feature) : DecidablePred f.Positive

Equations

• Hammerly2023.instDecidablePredFinsetRolePositive f x✝ = id inferInstance

The successive division algorithm (§3.2)

def Hammerly2023.Contrasts (f : Feature) (c : Finset (Finset Discourse.Role)) : Prop

A feature makes a contrast in a cell when it holds of some of its members and fails of others (28).

Equations

• Hammerly2023.Contrasts f c = ((Finset.filter f.Positive c).Nonempty ∧ {x ∈ c | ¬f.Positive x}.Nonempty)

@[instance_reducible]

instance Hammerly2023.instDecidablePredFinsetRoleContrasts (f : Feature) : DecidablePred (Contrasts f)

Equations

• Hammerly2023.instDecidablePredFinsetRoleContrasts f x✝ = id inferInstance

def Hammerly2023.divide (f : Feature) (c : Finset (Finset Discourse.Role)) : List (Finset (Finset Discourse.Role))

A feature divides a cell into its positive and negative parts where it makes a contrast, and leaves it whole otherwise.

Equations

• Hammerly2023.divide f c = if Hammerly2023.Contrasts f c then [Finset.filter f.Positive c, {x ∈ c | ¬f.Positive x}] else [c]

def Hammerly2023.sda (h : List Feature) : List (Finset (Finset Discourse.Role))

The cells a contrastive hierarchy derives (26): starting from the whole person space, each feature in turn divides every current cell.

Equations

• Hammerly2023.sda h = List.foldl (fun (cells : List (Finset (Finset Discourse.Role))) (f : Hammerly2023.Feature) => List.flatMap (Hammerly2023.divide f) cells) [Finset.univ] h

def Hammerly2023.AdmissibleFrom : List (Finset (Finset Discourse.Role)) → List Feature → Prop

A hierarchy is admissible from the current cells when each feature contrasts in some cell (29), and [Participant*] occurs only where the wide [Participant] would leave some cell undivided (p. 55).

Equations

• One or more equations did not get rendered due to their size.
• Hammerly2023.AdmissibleFrom x✝ [] = True

@[instance_reducible]

instance Hammerly2023.instDecidableAdmissibleFrom (cells : List (Finset (Finset Discourse.Role))) (h : List Feature) : Decidable (AdmissibleFrom cells h)

Equations

• One or more equations did not get rendered due to their size.
• Hammerly2023.instDecidableAdmissibleFrom x✝ [] = isTrue trivial

def Hammerly2023.Admissible (h : List Feature) : Prop

An admissible contrastive hierarchy: no feature twice, never [Participant] and [Participant*] together, and admissible from the undivided person space.

Equations

• Hammerly2023.Admissible h = (h.Nodup ∧ ¬(Hammerly2023.Feature.participant ∈ h ∧ Hammerly2023.Feature.participantStar ∈ h) ∧ Hammerly2023.AdmissibleFrom [Finset.univ] h)

@[instance_reducible]

instance Hammerly2023.instDecidablePredListFeatureAdmissible : DecidablePred Admissible

Equations

• Hammerly2023.instDecidablePredListFeatureAdmissible x✝ = id inferInstance

def Hammerly2023.hierarchies : List (List Feature)

The contrastive hierarchies over the three features: every ordering of every subset.

Equations

• Hammerly2023.hierarchies = List.flatMap List.permutations' [Hammerly2023.Feature.author, Hammerly2023.Feature.participant, Hammerly2023.Feature.participantStar].sublists

def Hammerly2023.cellGraph (cells : List (Finset (Finset Discourse.Role))) : Finset (Finset Discourse.Role × Finset Discourse.Role)

The graph of a partition given by its cells, as a finset of pairs of participant sets.

Equations

• Hammerly2023.cellGraph cells = {p : Finset Discourse.Role × Finset Discourse.Role | ∃ c ∈ cells, p.1 ∈ c ∧ p.2 ∈ c}

The derived partitions

theorem Hammerly2023.sda_participant_author : sda [Feature.participant, Feature.author] = [{{Discourse.Role.speaker}, {Discourse.Role.speaker, Discourse.Role.addressee}}, {{Discourse.Role.addressee}}, {∅}]

Figure 4: [Participant] over [Author] gives the tripartition.

theorem Hammerly2023.sda_author_participantStar : sda [Feature.author, Feature.participantStar] = [{{Discourse.Role.speaker, Discourse.Role.addressee}}, {{Discourse.Role.speaker}}, {{Discourse.Role.addressee}}, {∅}]

Figure 5: [Author] over the narrowed [Participant*] gives the quadripartition.

theorem Hammerly2023.admissible_author_participantStar : Admissible [Feature.author, Feature.participantStar]

theorem Hammerly2023.not_admissible_participant_participantStar : ¬Admissible [Feature.participant, Feature.participantStar]

Narrowing beside the wide feature is excluded, which would derive the tripartition grouping inclusive with second person (60).

theorem Hammerly2023.not_admissible_participantStar : ¬Admissible [Feature.participantStar]

Narrowing is not licensed at the top, where the wide feature divides the space.

theorem Hammerly2023.image_graph_sda_eq_geometry : (List.map (cellGraph ∘ sda) (List.filter (fun (b : List Feature) => decide (Admissible b)) hierarchies)).toFinset = Finset.image Harbour2016.graph (Finset.filter Harbour2016.Admissible Finset.univ)

The admissible hierarchies derive exactly the partitions that Harbour's bivalent geometry (9) generates, his five (p. 55; [Har16a] p. 193). Several hierarchies can derive one partition: [Author] over the wide [Participant] gives the tripartition, as Figure 4's [Participant] over [Author] does, since under [+Author] the wide feature makes no contrast.