Logophoric roles

Sells replaces a single notion of logophoricity with three discourse roles, each defined with respect to a proposition: the source, the intentional agent of the communication; the self, whose mental state or attitude the proposition describes; and the pivot, with respect to whose location the proposition is evaluated. A report predicates each role of the external speaker or of a referent inside the sentence, and the roles form a hierarchy: where the source is internal so is the self, and where the self is internal so is the pivot. The order here is that hierarchy, the pivot least.

Main definitions

• Reference.LogophoricRole: the three roles, a bounded linear order.

Implementation notes

• The discourse environments the hierarchy sorts, and the forms oriented to each role, are in Studies/Sells1987.lean.

References

• [Sel87]

inductive Reference.LogophoricRole : Type

The discourse roles of [Sel87], ordered by his hierarchy with the pivot least.

• pivot : LogophoricRole

  The one with respect to whose location the content of the report is evaluated.

• self : LogophoricRole

  The one whose mental state or attitude the content of the report describes.

• source : LogophoricRole

  The intentional agent of the communication.

@[instance_reducible]

instance Reference.instDecidableEqLogophoricRole : DecidableEq LogophoricRole

Equations

• Reference.instDecidableEqLogophoricRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Reference.instFintypeLogophoricRole : Fintype LogophoricRole

Equations

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

def Reference.instReprLogophoricRole.repr : LogophoricRole → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Reference.instReprLogophoricRole : Repr LogophoricRole

Equations

• Reference.instReprLogophoricRole = { reprPrec := Reference.instReprLogophoricRole.repr }

def Reference.LogophoricRole.toNat : LogophoricRole → ℕ

The rank of a role in the hierarchy.

Equations

• Reference.LogophoricRole.pivot.toNat = 0
• Reference.LogophoricRole.self.toNat = 1
• Reference.LogophoricRole.source.toNat = 2

theorem Reference.LogophoricRole.toNat_injective : Function.Injective toNat

@[instance_reducible]

instance Reference.LogophoricRole.instLinearOrder : LinearOrder LogophoricRole

Equations

• Reference.LogophoricRole.instLinearOrder = LinearOrder.lift' Reference.LogophoricRole.toNat Reference.LogophoricRole.toNat_injective

@[instance_reducible]

instance Reference.LogophoricRole.instBoundedOrder : BoundedOrder LogophoricRole

Equations

• Reference.LogophoricRole.instBoundedOrder = { top := Reference.LogophoricRole.source, le_top := ⋯, bot := Reference.LogophoricRole.pivot, bot_le := ⋯ }