Logophoric pronouns — the pronominal carrier of perspectival orientation

[Sel87]

The pronoun member of the cross-categorial logophoric series: LogophoricPronoun extends the general Pronoun (Syntax/Pronoun/Basic.lean) with its [Sel87] orientation — the minimum perspectival role (pivot/self/source, Features/Logophoricity.lean) an antecedent must fill to license it. Ewe yè is one such object: a logophoric pronoun licensed only by a self (an attitude holder); long-distance zibun is another, licensed by any pivot.

This is one carrier of the series, not its home: logophoricity is word-class-neutral (the Logophoric capability and the LogophoricRole taxonomy live in Features/Logophoricity.lean). Verbal logophoric marking (Gokana) or a logophoric long-distance reflexive would be sibling carriers — a different word-class object supplying its own instance : Logophoric That — read by the same [Logophoric α] generic code.

The licensing is orthogonal to Bound (Syntax/Pronoun/Capabilities.lean): a form's perspectival orientation is not its Principle A/B/C role. zibun below is a Principle-A reflexive (Bound.IsAnaphor) whose logophoric licensing is nonetheless the pivot orientation, not configurational binding — [Sel87]'s thesis that logophoric anaphora is role-oriented, made concrete by carrying both axes on one object (zibun_anaphor_yet_pivot_oriented).

Main declarations

• LogophoricPronoun — the lexical object (extends Pronoun + requiredRole).
• instance : Logophoric LogophoricPronoun — the pronoun carrier of the series.
• Proform / Bound instances routing the object through the Pronoun API.
• ye, zibun — worked [Sel87] entries; licensing derived from the hierarchy.

structure LogophoricPronounextends Pronoun : Type

A single logophoric pronoun — the general Pronoun (surface form + φ-features) plus its [Sel87] orientation: the minimum perspectival role an antecedent must fill to license it (self for a logophoric pronoun proper, pivot for a long-distance reflexive). Carries no denotation of its own; its perspectival anchor is the LogophoricRole an embedding context's shift makes available (cf. Core/Context/Shifts.lean's attitudeShift/perspectiveShift).

• form : String
• person : Option Person
• number : Option Number
• case_ : Option Case
• gender : Option Gender
• script : Option String
• pronType : Option UD.PronType
• bindingClass : Option Features.BindingClass
• strength : Option Strength
• requiredRole : Features.Logophoricity.LogophoricRole

  The minimum [Sel87] role an antecedent must fill to license this form.

@[implicit_reducible]

instance instReprLogophoricPronoun : Repr LogophoricPronoun

Equations

• instReprLogophoricPronoun = { reprPrec := instReprLogophoricPronoun.repr }

def instReprLogophoricPronoun.repr : LogophoricPronoun → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance instDecidableEqLogophoricPronoun : DecidableEq LogophoricPronoun

Equations

• instDecidableEqLogophoricPronoun = instDecidableEqLogophoricPronoun.decEq

def instDecidableEqLogophoricPronoun.decEq (x✝ x✝¹ : LogophoricPronoun) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance instProformLogophoricPronoun : Proform LogophoricPronoun

A logophoric pronoun is a Proform (form + φ via its Pronoun core).

Equations

• instProformLogophoricPronoun = { form := fun (p : LogophoricPronoun) => p.form, phi := fun (p : LogophoricPronoun) => p.toWord.phi }

@[implicit_reducible]

instance instBoundLogophoricPronoun : Bound LogophoricPronoun

Its binding class is the Pronoun core's, defaulting an undeclared shell to .pronoun — independent of its logophoric orientation.

Equations

• instBoundLogophoricPronoun = { bindingClass := fun (p : LogophoricPronoun) => p.bindingClass.getD Features.BindingClass.pronoun }

@[implicit_reducible]

instance instLogophoricLogophoricPronoun : Features.Logophoricity.Logophoric LogophoricPronoun

The logophoric pronoun is a carrier of the word-class-neutral Logophoric capability.

Equations

• instLogophoricLogophoricPronoun = { requiredRole := LogophoricPronoun.requiredRole }

Worked entries ([Sel87])

def ye : LogophoricPronoun

Ewe yè — a dedicated logophoric pronoun. Its antecedent must be at least a self (an attitude holder): [Sel87] "antecedent must be at least a self". Principle-B by default (no declared anaphor shell); the logophoric orientation, not the binding class, does the work.

Equations

• ye = { form := "yè", person := some Person.third, requiredRole := Features.Logophoricity.LogophoricRole.self }

def zibun : LogophoricPronoun

Japanese long-distance zibun — a perspectival reflexive. Its antecedent need only be a pivot (any point-of-view centre): [Sel87] "antecedent must be a pivot". Morphologically a Principle-A reflexive (bindingClass := .reflexive), so its licensing axis (pivot) and its binding axis (anaphor) are distinct — the orthogonality the Logophoric/Bound split encodes.

Equations

• zibun = { form := "zibun", bindingClass := some Features.BindingClass.reflexive, requiredRole := Features.Logophoricity.LogophoricRole.pivot }

Licensing, derived from the hierarchy

theorem ye_licensed_by_self : Features.Logophoricity.Logophoric.LicensedBy ye Features.Logophoricity.LogophoricRole.self

yè is licensed by a self antecedent — it reaches its own requirement.

theorem ye_licensed_by_source : Features.Logophoricity.Logophoric.LicensedBy ye Features.Logophoricity.LogophoricRole.source

yè is licensed by a source antecedent — a reporter is also a self (self ≤ source).

theorem ye_not_licensed_by_pivot : ¬Features.Logophoricity.Logophoric.LicensedBy ye Features.Logophoricity.LogophoricRole.pivot

yè is not licensed by a bare pivot antecedent: a point-of-view centre that is not an attitude holder fails yè's self requirement (¬ self ≤ pivot). The discriminating case that makes the capability non-vacuous.

theorem zibun_licensed_by_pivot : Features.Logophoricity.Logophoric.LicensedBy zibun Features.Logophoricity.LogophoricRole.pivot

Long-distance zibun is licensed by any pivot — the weakest centre suffices.

theorem zibun_anaphor_yet_pivot_oriented : Bound.IsAnaphor zibun ∧ Features.Logophoricity.Logophoric.requiredRole zibun = Features.Logophoricity.LogophoricRole.pivot

Orthogonality of orientation and binding: zibun is a Principle-A anaphor (Bound.IsAnaphor) yet its logophoric licensing is the pivot orientation, not its binding class — [Sel87]'s role-oriented anaphora, carried as two independent axes on one object.

theorem any_logophoric_licensed_by_source (p : LogophoricPronoun) : Features.Logophoricity.Logophoric.LicensedBy p Features.Logophoricity.LogophoricRole.source

Generic consumer of the capability: every logophoric pronoun is licensed by a source antecedent, via the carrier-independent Logophoric.source_licenses. Validates that the abstraction is usable over [Logophoric α], not just on these entries.