The binary person scale

The load-bearing cut of person prominence puts the speech-act participants, first and second person, above the rest. It is Haspelmath's person scale (8a), locuphoric above aliophoric in his terms, the cut that Bonet's strong person-case constraint draws, and the coarsening of Person.prominence at the participant level.

Main declarations

• Person.Class: nonParticipant < participant, a two-element bounded linear order.
• Person.toClass: the class of a person, participant exactly when it IsSAP, and toClass_mono for its agreement with prominence.
• Person.kind_map_toClass_eq_downstream_iff: a scenario is downstream on the binary scale exactly when its higher-ranked argument alone is a speech-act participant.

References

• [Has21c]
• [Bon91]

inductive Person.Class : Type

The binary person scale ranks speech-act participants above non-participants.

• nonParticipant : Class
• participant : Class

@[instance_reducible]

instance Person.instDecidableEqClass : DecidableEq Class

Equations

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

@[instance_reducible]

instance Person.instReprClass : Repr Class

Equations

• Person.instReprClass = { reprPrec := Person.instReprClass.repr }

def Person.instReprClass.repr : Class → ℕ → Std.Format

Equations

• Person.instReprClass.repr Person.Class.nonParticipant prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Person.Class.nonParticipant")).group prec✝
• Person.instReprClass.repr Person.Class.participant prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Person.Class.participant")).group prec✝

@[instance_reducible]

instance Person.instFintypeClass : Fintype Class

Equations

• Person.instFintypeClass = { elems := { val := ↑Person.Class.enumList, nodup := Person.Class.enumList_nodup }, complete := Person.instFintypeClass._proof_1 }

@[instance_reducible]

instance Person.Class.instLinearOrder : LinearOrder Class

The scale orders nonParticipant < participant.

Equations

• Person.Class.instLinearOrder = LinearOrder.lift' (fun (x : Person.Class) => x.ctorIdx) Person.Class.instLinearOrder._proof_1

@[instance_reducible]

instance Person.Class.instBoundedOrder : BoundedOrder Class

The scale is bounded, ⊥ = nonParticipant and ⊤ = participant.

Equations

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

instance Person.Class.instIsSimpleOrder : IsSimpleOrder Class

def Person.toClass (p : Person) : Class

The class of a person is participant exactly when it is a speech-act participant.

Equations

• p.toClass = if p.IsSAP then Person.Class.participant else Person.Class.nonParticipant

@[simp]

theorem Person.toClass_eq_participant_iff {p : Person} : p.toClass = Class.participant ↔ p.IsSAP

@[simp]

theorem Person.toClass_eq_nonParticipant_iff {p : Person} : p.toClass = Class.nonParticipant ↔ ¬p.IsSAP

theorem Person.toClass_mono {p q : Person} (h : p.prominence ≤ q.prominence) : p.toClass ≤ q.toClass

The class is the coarsening of prominence at the participant level.

theorem Person.kind_map_toClass_eq_downstream_iff {s : Clause.Scenario Person} : (Clause.Scenario.map toClass s).kind = Clause.Scenario.Kind.downstream ↔ s.high.IsSAP ∧ ¬s.low.IsSAP

A scenario is downstream on the binary person scale exactly when its higher-ranked argument alone is a speech-act participant.