The lattice of persons

A person value covers the referents whose participants form one of its participant sets (Person.participantSets). As Zwicky proposes, a coordination refers to the union of its conjuncts' referents, so its participant sets are the pairwise unions ⊻ of theirs. Distinct values cover distinct participant sets, so this makes Person a join-semilattice whose join ⊔ is person resolution, with third person at the bottom. Dalrymple and Kaplan's marker sets are the participant sets of the quadripartition, and their union is the join (Person.ofParticipants_union).

Main definitions

• the SemilatticeSup Person instance: person resolution as the join.

Main results

• Person.participantSets_sup: the participant sets of a join are the pairwise unions.
• Person.ofParticipants_union: the person of a union of participant sets is the join of their persons.
• Person.coarsen_eq_iff: coarsening sends a value to the tripartition value covering it.

References

• [Zwi77a]
• [DK00a]

Participant sets

theorem Person.supClosed_participantSets (p : Person) : SupClosed ↑p.participantSets

The participant sets of a value are closed under union.

Resolution

@[instance_reducible]

instance Person.instMax : Max Person

In person resolution third person is neutral, the first person unmarked for clusivity absorbs the exclusive, and any other two distinct values together cover both the speaker and the addressee.

Equations

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

@[simp]

theorem Person.participantSets_sup (p q : Person) : (p ⊔ q).participantSets = p.participantSets ⊻ q.participantSets

The participant sets of a coordination are the unions of its conjuncts'.

@[instance_reducible]

instance Person.instSemilatticeSup : SemilatticeSup Person

Equations

• Person.instSemilatticeSup = SemilatticeSup.mk' Person.instSemilatticeSup._proof_4 Person.instSemilatticeSup._proof_5 Person.instSemilatticeSup._proof_6

@[instance_reducible]

instance Person.instDecidableLE : DecidableLE Person

Equations

• p.instDecidableLE q = instDecidableEqPerson (p ⊔ q) q

@[instance_reducible]

instance Person.instOrderBot : OrderBot Person

Equations

• Person.instOrderBot = { bot := Person.third, bot_le := Person.instOrderBot._proof_1 }

@[simp]

theorem Person.bot_eq_third : ⊥ = third

The person of a participant set

@[simp]

theorem Person.ofParticipants_empty : ofParticipants ∅ = ⊥

theorem Person.ofParticipants_union (s t : Finset Discourse.Role) : ofParticipants (s ∪ t) = ofParticipants s ⊔ ofParticipants t

The person of a union of participant sets is the join of their persons.

Coarsening

theorem Person.participantSets_subset_coarsen (p : Person) : p.participantSets ⊆ p.coarsen.participantSets

Coarsening a value never loses a participant set.

theorem Person.coarsen_eq_iff (p q : Person) : p.coarsen = q ↔ q.coarsen = q ∧ p.participantSets ⊆ q.participantSets

Coarsening sends a value to the tripartition value covering its participant sets.

theorem Person.coarsen_sup (p q : Person) : (p ⊔ q).coarsen = (p.coarsen ⊔ q.coarsen).coarsen

The tripartition value of a coordination depends only on the tripartition values of its conjuncts.