Documentation

Linglib.Syntax.Person.Features

Bivalent person features #

Person decomposes into two features, [participant] and [author], the bivalent system Ackema and Neeleman trace to Halle. Read on participant sets, [participant] holds of the nonempty ones and [author] of those containing the speaker, so the participant sets and the features form a formal context (Person.Bears). A value's bundle is the set of features holding of all its participant sets, its intent in the context. Every set containing the speaker is nonempty, so the closed sets of features are exactly the lower sets of the chain participant < author: the containment filter that rules out an author who is no participant is the closure of the context. Harley and Ritter caution that a geometry encodes morphological dependency, which need not follow logical implication, so the chain stays a stipulated order, and its coincidence with the closure is a theorem about person. Two features see the tripartition and not clusivity: a tripartition value covers exactly the participant sets whose own features are its bundle.

Main definitions #

Person.Feature: the two features, ordered participant < author.
Person.Bears: the features a participant set bears.
Person.toFeatures: the bundle of a person value.
Person.prominence: the top of a value's bundle, the person hierarchy.
Person.Category.toFeatures: the bundle of a referential category.

Main results #

Person.wellFormed_iff_isIntent: the well-formed bundles are the closed sets of the context.
Person.card_wellFormed: there are three well-formed bundles, so no fourth person.
Person.mem_participantSets_iff: a tripartition value covers the participant sets whose features are its bundle.
Person.toFeatures_sup: the bundle of a coordination is the union of its conjuncts' bundles.
Person.mem_toFeatures_iff: a value bears exactly the features up to its prominence.
Person.prominence_le_iff: prominence is the order resolution induces up to clusivity.
Person.prominence_le_iff_subset: prominence orders values by inclusion of their bundles.
Person.Category.sharedPerson_isSome_iff: a set of categories has a person iff they share a bundle.

References #

inductive Person.Feature :

Person has two features, the author feature depending on the participant feature.

participant : Feature
[participant] holds of a referent including a speech-act participant.
author : Feature
[author] holds of a referent including the speaker.

Instances For

@[instance_reducible]

instance Person.instDecidableEqFeature :

DecidableEq Feature

Equations

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

def Person.instReprFeature.repr :

Feature → ℕ → Std.Format

Equations

Person.instReprFeature.repr Person.Feature.participant prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Person.Feature.participant")).group prec✝
Person.instReprFeature.repr Person.Feature.author prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Person.Feature.author")).group prec✝

Instances For

@[instance_reducible]

instance Person.instReprFeature :

Equations

Person.instReprFeature = { reprPrec := Person.instReprFeature.repr }

@[instance_reducible]

instance Person.instFintypeFeature :

Fintype Feature

Equations

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

def Person.Feature.rank :

Feature → Fin 2

Feature.rank places participant below author on the dependency chain.

Equations

Person.Feature.participant.rank = 0
Person.Feature.author.rank = 1

Instances For

@[instance_reducible]

instance Person.instLinearOrderFeature :

LinearOrder Feature

Equations

Person.instLinearOrderFeature = LinearOrder.lift' Person.Feature.rank Person.instLinearOrderFeature._proof_1

@[instance_reducible]

instance Person.instLocallyFiniteOrderBotFeature :

LocallyFiniteOrderBot Feature

Equations

Person.instLocallyFiniteOrderBotFeature = Fintype.toLocallyFiniteOrderBot

@[reducible, inline]

abbrev Person.Features :

A person feature bundle is the set of its positive features.

Equations

Person.Features = Finset Person.Feature

Instances For

The context of participant sets and features #

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

Feature → Prop

A participant set bears [participant] when it is nonempty and [author] when it contains the speaker.

Equations

Person.Bears s Person.Feature.participant = s.Nonempty
Person.Bears s Person.Feature.author = (Discourse.Role.speaker ∈ s)

Instances For

@[instance_reducible]

instance Person.instDecidablePredFeatureBears (s : Finset Discourse.Role) :

DecidablePred (Bears s)

Equations

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

theorem Person.Bears.participant {s : Finset Discourse.Role} (h : Bears s Feature.author) :

Bears s Feature.participant

theorem Person.wellFormed_iff_isIntent (t : Features) :

IsLowerSet ↑t ↔ Order.IsIntent Bears ↑t

The bundles passing the containment filter, the lower sets of the chain, are exactly the closed sets of features of the context.

theorem Person.intentClosure_singleton_author :

(intentClosure Bears) {Feature.author} = Set.univ

The author feature alone closes to both features.

theorem Person.not_wellFormed_singleton_author :

¬IsLowerSet ↑{Feature.author}

The bundle with the author feature alone violates containment.

theorem Person.card_wellFormed :

Fintype.card { pf : Features // IsLowerSet ↑pf } = 3

Exactly three bundles pass the containment filter.

The bundle of a person value #

def Person.toFeatures (p : Person) :

The bundle of a person value is the set of features its participant sets all bear.

Equations

p.toFeatures = {f : Person.Feature | ∀ s ∈ p.participantSets, Person.Bears s f}

Instances For

theorem Person.coe_toFeatures (p : Person) :

↑p.toFeatures = upperPolar Bears ↑p.participantSets

A value's bundle is the intent of its participant sets.

@[simp]

theorem Person.toFeatures_first :

first.toFeatures = {Feature.participant, Feature.author}

@[simp]

theorem Person.toFeatures_firstInclusive :

firstInclusive.toFeatures = {Feature.participant, Feature.author}

@[simp]

theorem Person.toFeatures_firstExclusive :

firstExclusive.toFeatures = {Feature.participant, Feature.author}

@[simp]

theorem Person.toFeatures_second :

second.toFeatures = {Feature.participant}

@[simp]

theorem Person.toFeatures_third :

third.toFeatures = ∅

@[simp]

theorem Person.toFeatures_coarsen (p : Person) :

p.coarsen.toFeatures = p.toFeatures

Coarsening does not change a value's bundle, since the features do not see clusivity.

theorem Person.toFeatures_sup (p q : Person) :

(p ⊔ q).toFeatures = p.toFeatures ∪ q.toFeatures

The bundle of a coordination is the union of its conjuncts' bundles.

theorem Person.toFeatures_wellFormed (p : Person) :

IsLowerSet ↑p.toFeatures

Every bundle is well-formed.

theorem Person.isSAP_iff_participant {p : Person} :

p.IsSAP ↔ Feature.participant ∈ p.toFeatures

IsSAP is featural participanthood.

theorem Person.includesSpeaker_iff_author {p : Person} :

p.IncludesSpeaker ↔ Feature.author ∈ p.toFeatures

IncludesSpeaker is featural authorhood.

theorem Person.mem_participantSets_iff {p : Person} (hp : p.coarsen = p) (s : Finset Discourse.Role) :

s ∈ p.participantSets ↔ Finset.filter (Bears s) Finset.univ = p.toFeatures

A tripartition value covers exactly the participant sets whose features are its bundle, the sets in the domain of its bundle and in no domain of a more specified one.

theorem Person.coarsen_ofParticipants_eq_iff (s t : Finset Discourse.Role) :

(ofParticipants s).coarsen = (ofParticipants t).coarsen ↔ Finset.filter (Bears s) Finset.univ = Finset.filter (Bears t) Finset.univ

Two participant sets have the same tripartition person iff they bear the same features.

Prominence #

A bundle is a lower set of the chain participant < author, so it is determined by its top feature, and ordering values by their tops is the person hierarchy 1 > 2 > 3. It is the order coordination induces up to clusivity: a coordination takes the person of its most prominent conjunct, as Zwicky's hierarchy of reference and Corbett's resolution rules state.

def Person.prominence (p : Person) :

WithBot Feature

The prominence of a value is the top feature of its bundle: [author] for the first person, [participant] for the second, none for the third.

Equations

p.prominence = Finset.max p.toFeatures

Instances For

@[simp]

theorem Person.prominence_first :

first.prominence = ↑Feature.author

@[simp]

theorem Person.prominence_firstInclusive :

firstInclusive.prominence = ↑Feature.author

@[simp]

theorem Person.prominence_firstExclusive :

firstExclusive.prominence = ↑Feature.author

@[simp]

theorem Person.prominence_second :

second.prominence = ↑Feature.participant

@[simp]

theorem Person.prominence_third :

third.prominence = ⊥

theorem Person.mem_toFeatures_iff {p : Person} {f : Feature} :

f ∈ p.toFeatures ↔ ↑f ≤ p.prominence

A value bears exactly the features up to its prominence.

theorem Person.prominence_le_iff_subset {p q : Person} :

p.prominence ≤ q.prominence ↔ p.toFeatures ⊆ q.toFeatures

Prominence orders values by inclusion of their bundles.

theorem Person.prominence_le_iff {p q : Person} :

p.prominence ≤ q.prominence ↔ (p ⊔ q).coarsen = q.coarsen

Prominence is the order resolution induces up to clusivity, p being at most as prominent as q iff coordinating them gives q's tripartition value.

The features of a referential category #

def Person.Category.toFeatures (c : Category) :

The bundle of a category is the set of features its participants bear. The features underdetermine the first person complex, whose three categories share a bundle; the decomposition that distinguishes the exclusive is Harbour's (Studies.Harbour2016.signOf).

Equations

c.toFeatures = Finset.filter (Person.Bears c.participants) Finset.univ

Instances For

@[simp]

theorem Person.Category.mem_toFeatures {c : Category} {f : Feature} :

f ∈ c.toFeatures ↔ Bears c.participants f

@[simp]

theorem Person.Category.author_mem_toFeatures {c : Category} :

Feature.author ∈ c.toFeatures ↔ c.IncludesSpeaker

@[simp]

theorem Person.Category.participant_mem_toFeatures {c : Category} :

Feature.participant ∈ c.toFeatures ↔ c.IncludesSpeaker ∨ c.IncludesAddressee

theorem Person.Category.toFeatures_person (c : Category) :

c.person.toFeatures = c.toFeatures

The bundle of a category is the bundle of its person.

theorem Person.Category.toFeatures_wellFormed (c : Category) :

IsLowerSet ↑c.toFeatures

Every category yields a well-formed bundle.

theorem Person.Category.sharedPerson_isSome_iff (s : Finset Category) :

(sharedPerson s).isSome = true ↔ s.Nonempty ∧ ∀ c ∈ s, ∀ d ∈ s, c.toFeatures = d.toFeatures

A set of categories has a person iff the categories share a bundle.