Person systems

A person system partitions the participant sets, keeping apart the referents a language's paradigms distinguish; the attested systems are five of the fifteen partitions of the four sets. Resolution sends a coordination to the union of its conjuncts' participant sets, so a system assigns a coordination a person from its conjuncts' persons exactly when its partition is a congruence for union, a SupCon (Finset Role). Such a congruence is cut out by the down-sets of participant sets it respects (SupCon.r_iff_forall_le), and the nontrivial ones are the complements of the monotone person features: lacking any participant (below ∅), lacking the speaker (below {addressee}), and lacking the addressee (below {speaker}).

The tripartition is the congruence of the first two: a participant set's person is first if it contains the speaker, otherwise second if it contains the addressee, otherwise third, Zwicky's correspondence principle. Resolution in the tripartition therefore follows the hierarchy 1 > 2 > 3, which Corbett states as resolution rules.

Main definitions

• Person.tripartitionOf: the tripartition person of a participant set.
• Person.tripartition: the tripartition as a congruence for union.

Main results

• Person.tripartition_r_iff: the tripartition is generated by the participant and author features.
• Person.mem_participantSets_tripartitionOf: each class of the tripartition is the participant sets of its person.
• Person.tripartitionOf_union: in the tripartition, resolution selects the more prominent conjunct.

References

• [Har16a]
• [Zwi77a]
• [Cor06]

def Person.tripartitionOf (s : Finset Discourse.Role) : Person

The tripartition person of a participant set: its person without clusivity.

Equations

• Person.tripartitionOf s = (Person.ofParticipants s).coarsen

theorem Person.tripartitionOf_union_eq_coarsen (s t : Finset Discourse.Role) : tripartitionOf (s ∪ t) = (tripartitionOf s ⊔ tripartitionOf t).coarsen

The tripartition person of a union depends only on the tripartition persons of its parts.

def Person.tripartition : SupCon (Finset Discourse.Role)

The tripartition identifies the participant sets with the same tripartition person, a congruence for union.

Equations

• Person.tripartition = { toSetoid := Setoid.ker Person.tripartitionOf, sup := ⋯ }

theorem Person.tripartition_r_iff {s t : Finset Discourse.Role} : tripartition.toSetoid s t ↔ (s.Nonempty ↔ t.Nonempty) ∧ (Discourse.Role.speaker ∈ s ↔ Discourse.Role.speaker ∈ t)

The tripartition is generated by the participant and author features.

theorem Person.mem_participantSets_tripartitionOf {s t : Finset Discourse.Role} : t ∈ (tripartitionOf s).participantSets ↔ tripartition.toSetoid s t

Each class of the tripartition is the family of participant sets its person covers.

theorem Person.tripartitionOf_union (s t : Finset Discourse.Role) : tripartitionOf (s ∪ t) = if (tripartitionOf t).prominence ≤ (tripartitionOf s).prominence then tripartitionOf s else tripartitionOf t

In the tripartition, resolution selects the more prominent conjunct.