The domains of φ-features

Following Sauerland, a φ-feature is a presuppositional partial identity function on entities: it asserts nothing and is defined on a domain, so it denotes that domain, a Set of entities. A bundle denotes the intersection of its features' domains (Finset.inf) and the empty bundle everything, so over well-formed bundles the domains nest by specification (IsLowerSet.subset_or_subset with Finset.inf_mono), the Feature-Subset Principle as a consequence of the privative geometry. Person is read at parthood of the agent and the addressee of the context of utterance, number at atomicity, and gender at the gender a referent is socially assigned (Gendered). For gender Sauerland makes masculine the unmarked value, the one coordinations of mixed gender take, with feminine presupposing non-masculinity and neuter genderlessness, so the neuter domain lies inside the feminine one. The person domains are the participant-set extents of Person.Bears pulled back along the participants of a referent, and a tripartition value denotes the referents in its domain and in no stronger one.

Main definitions

• Person.dom, Number.dom, Gender.dom: the domain of an optional value.
• Reference.Context.participants: the discourse roles whose holders are part of a referent.

Main results

• Person.mem_dom_feature_iff: a person feature's domain is the pullback of Person.Bears.
• Person.participants_mem_participantSets_first, …_second, …_third: the tripartition values denote the referents in their domain and in no stronger one.
• Gender.dom_neuter_subset_dom_feminine: the neuter domain lies inside the feminine one.

Implementation notes

An absent feature, and a value without a bundle, the impersonal person, the numbers beyond the dual and the non-sex-based genders, denote the whole domain; the semantically unmarked values, third person, plural and masculine, are the empty bundles, whose unrestricted domain Wang finds recruited by honorification. A referent may be gendered neither way, and then only a form without a gender feature is defined of it, the account of singular they of Bjorkman and of Konnelly and Cowper. The person entries take the agent and the addressee as parts of the referent where Sauerland has them overlap it; the two coincide for an atomic agent and addressee. The two-feature decomposition does not see clusivity, so the inclusive is refined to referents including the addressee. The cells of the tripartition are stated one by one, since Maximize Presupposition (Competition.unblocked) yields them only when the agent is not part of the addressee; otherwise the first and second person domains coincide (Sauerland2003.unblocked_second_of_degenerate). The dual's minimality domain needs a mereological predicate the entity domain's order does not supply, so the dual restricts nothing.

References

• [Sau03]
• [Sau08b]
• [Bjo17]
• [KC20]
• [Wan23]

Person

def Person.Feature.dom {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [PartialOrder E] (c : Reference.Context W E P T) : Feature → Set E

At a context of utterance, [author] is defined of the referents including the agent and [participant] of those including the agent or the addressee.

Equations

• Person.Feature.dom c Person.Feature.author = Set.Ici c.agent
• Person.Feature.dom c Person.Feature.participant = Set.Ici c.agent ∪ Set.Ici c.addressee

def Person.dom {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [PartialOrder E] (c : Reference.Context W E P T) : Option Person → Set E

At a context of utterance, the first person is defined of the referents including the agent, the inclusive of those including the agent and the addressee, and the second of those including the agent or the addressee; the third person and an absent value, the impersonal, restrict nothing.

Equations

• Person.dom c (some Person.firstInclusive) = Set.Ici c.agent ∩ Set.Ici c.addressee
• Person.dom c x✝ = (Option.map Person.toFeatures x✝).elim Set.univ fun (x : Person.Features) => Finset.inf x (Person.Feature.dom c)

@[simp]

theorem Person.dom_none {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [PartialOrder E] (c : Reference.Context W E P T) : dom c none = Set.univ

@[simp]

theorem Person.mem_dom_first {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [PartialOrder E] (c : Reference.Context W E P T) (x : E) : x ∈ dom c (some first) ↔ c.agent ≤ x

@[simp]

theorem Person.mem_dom_firstInclusive {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [PartialOrder E] (c : Reference.Context W E P T) (x : E) : x ∈ dom c (some firstInclusive) ↔ c.agent ≤ x ∧ c.addressee ≤ x

@[simp]

theorem Person.mem_dom_firstExclusive {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [PartialOrder E] (c : Reference.Context W E P T) (x : E) : x ∈ dom c (some firstExclusive) ↔ c.agent ≤ x

@[simp]

theorem Person.mem_dom_second {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [PartialOrder E] (c : Reference.Context W E P T) (x : E) : x ∈ dom c (some second) ↔ c.agent ≤ x ∨ c.addressee ≤ x

@[simp]

theorem Person.dom_third {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [PartialOrder E] (c : Reference.Context W E P T) : dom c (some third) = Set.univ

theorem Person.dom_firstInclusive_subset_dom_first {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [PartialOrder E] (c : Reference.Context W E P T) : dom c (some firstInclusive) ⊆ dom c (some first)

The inclusive lies inside the first person.

noncomputable def Reference.Context.participants {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [PartialOrder E] (c : Context W E P T) (x : E) : Finset Discourse.Role

The participants of a referent at a context are the discourse roles whose holders, the agent and the addressee, are part of it.

Equations

• c.participants x = {r : Discourse.Role | (match r with | Discourse.Role.speaker => c.agent | Discourse.Role.addressee => c.addressee) ≤ x}

@[simp]

theorem Reference.Context.speaker_mem_participants {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [PartialOrder E] (c : Context W E P T) (x : E) : Discourse.Role.speaker ∈ c.participants x ↔ c.agent ≤ x

@[simp]

theorem Reference.Context.addressee_mem_participants {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [PartialOrder E] (c : Context W E P T) (x : E) : Discourse.Role.addressee ∈ c.participants x ↔ c.addressee ≤ x

theorem Person.mem_dom_feature_iff {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [PartialOrder E] (c : Reference.Context W E P T) (x : E) (f : Feature) : x ∈ Feature.dom c f ↔ Bears (c.participants x) f

A person feature's domain holds the referents whose participants bear the feature.

theorem Person.participants_mem_participantSets_first {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [PartialOrder E] (c : Reference.Context W E P T) (x : E) : c.participants x ∈ first.participantSets ↔ x ∈ dom c (some first)

The first person denotes the referents in its domain.

theorem Person.participants_mem_participantSets_second {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [PartialOrder E] (c : Reference.Context W E P T) (x : E) : c.participants x ∈ second.participantSets ↔ x ∈ dom c (some second) ∧ x ∉ dom c (some first)

The second person denotes the referents in its domain and not in the first person's.

theorem Person.participants_mem_participantSets_third {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [PartialOrder E] (c : Reference.Context W E P T) (x : E) : c.participants x ∈ third.participantSets ↔ x ∉ dom c (some second)

The third person denotes the referents outside the second person's domain, which contains the first person's.

Number

def Number.Feature.dom {E : Type u_1} [PartialOrder E] : Feature → Set E

[atomic] is defined of the atoms, and [minimal], pending a minimality predicate, of everything.

Equations

• Number.Feature.atomic.dom = {x : E | Mereology.Atom x}
• Number.Feature.minimal.dom = Set.univ

def Number.dom {E : Type u_1} [PartialOrder E] (n : Option Number) : Set E

The singular is defined of the atoms; the plural, the dual (pending a minimality predicate), an absent value and a value without a bundle restrict nothing.

Equations

• Number.dom n = (n.bind Number.Features.ofNumber).elim Set.univ fun (x : Number.Features) => Finset.inf x Number.Feature.dom

@[simp]

theorem Number.dom_none {E : Type u_1} [PartialOrder E] : dom none = Set.univ

@[simp]

theorem Number.mem_dom_singular {E : Type u_1} [PartialOrder E] (x : E) : x ∈ dom (some singular) ↔ Mereology.Atom x

@[simp]

theorem Number.dom_dual {E : Type u_1} [PartialOrder E] : dom (some dual) = Set.univ

@[simp]

theorem Number.dom_plural {E : Type u_1} [PartialOrder E] : dom (some plural) = Set.univ

Gender

class Gendered (E : Type u_1) : Type u_1

A gendered entity domain has disjoint sets of referents gendered masculine and gendered feminine, as socially constituted. Grammatical gender presupposes it, and a referent may be gendered neither way.

• masculine : Set E

  The referents gendered masculine.

• feminine : Set E

  The referents gendered feminine.

• disjoint : Disjoint masculine feminine

  No referent is gendered both ways.

def Gender.Feature.dom {E : Type u_1} [Gendered E] : Feature → Set E

Over a gendered entity domain, [feminine] is defined of the referents not gendered masculine and [neuter] of those not gendered feminine.

Equations

• Gender.Feature.feminine.dom = Gendered.masculineᶜ
• Gender.Feature.neuter.dom = Gendered.feminineᶜ

def Gender.dom {E : Type u_1} [Gendered E] (g : Option Gender) : Set E

Over a gendered entity domain, the feminine is defined of the referents not gendered masculine and the neuter of those gendered neither way; the masculine, an absent value and the non-sex-based genders restrict nothing.

Equations

• Gender.dom g = (g.bind Gender.Features.fromGender).elim Set.univ fun (x : Gender.Features) => Finset.inf x Gender.Feature.dom

@[simp]

theorem Gender.dom_none {E : Type u_1} [Gendered E] : dom none = Set.univ

@[simp]

theorem Gender.mem_dom_neuter {E : Type u_1} [Gendered E] (x : E) : x ∈ dom (some neuter) ↔ x ∉ Gendered.masculine ∧ x ∉ Gendered.feminine

@[simp]

theorem Gender.mem_dom_feminine {E : Type u_1} [Gendered E] (x : E) : x ∈ dom (some feminine) ↔ x ∉ Gendered.masculine

@[simp]

theorem Gender.dom_masculine {E : Type u_1} [Gendered E] : dom (some masculine) = Set.univ

theorem Gender.dom_neuter_subset_dom_feminine {E : Type u_1} [Gendered E] : dom (some neuter) ⊆ dom (some feminine)

The neuter domain lies inside the feminine one, the containment [+neuter] → [+feminine] of the decomposition as a fact about referents.