Coppock & Wechsler (2018): The Proper Treatment of Egophoricity in Kathmandu Newari

This file formalizes Coppock and Wechsler's account of egophoric marking in Kathmandu Newari. Newari verbs carry no person agreement. A special egophoric form appears in statements about the speaker, in questions about the addressee, and in reports where the reported speaker was knowingly talking about herself. The plain form appears elsewhere.

A sentence is evaluated at a context, a world and an agent called the perspectival center, and the egophoric suffix presupposes that the subject is the center (ego). Every context has an authority, the speaker of a statement and the addressee of a question, and a speech act proposes its meaning with the authority as center. When the subject is not the authority the proposal is empty and the conversation cannot continue (inCrisis_assert_ego, inCrisis_ask_ego), which gives I in statements and you in questions. A report is true only if the reported speaker took the subject to be herself (says_ego_iff). A simpler account, on which the suffix presupposes that the subject is the authority, agrees on main clauses and fails when Syam comments on a photograph of himself that he does not recognize (lampshade).

Implementation notes

• The Table records the public side of the paper's discourse model, the common ground and its projections. The centered meaning is the argument of assert, ask and Says.
• Expressions of the paper's logic are given by their meanings rather than as syntax, and time is ignored as in the paper.

TODO

The paper marks the second-person question with the plain form as unacceptable. The account derives where the egophoric form is excluded, not where it is required.

References

• [CW18]
• [FB10]
• [Pea15]

Contexts, terms and meanings

structure CoppockWechsler2018.Context (W : Type u_5) (E : Type u_6) (P : Type u_7) (T : Type u_8) extends Reference.Context W E P T : Type (max (max (max u_5 u_6) u_7) u_8)

A context of utterance together with its authority, the person who vouches for what is said in it.

• agent : E
• addressee : E
• world : W
• time : T
• position : P
• authority : E

  The epistemic authority of the context.

def CoppockWechsler2018.Context.IsDeclarative {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Context W E P T) : Prop

A context is declarative when its authority is the speaker.

Equations

• c.IsDeclarative = (c.authority = c.agent)

def CoppockWechsler2018.Context.IsInterrogative {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Context W E P T) : Prop

A context is interrogative when its authority is the addressee.

Equations

• c.IsInterrogative = (c.authority = c.addressee)

@[reducible, inline]

abbrev CoppockWechsler2018.Term (W : Type u_5) (E : Type u_6) (P : Type u_7) (T : Type u_8) : Type (max (max (max (max u_6 u_8) u_7) u_6) u_5)

A term denotes an individual, which may depend on the context and on the perspectival center.

Equations

• CoppockWechsler2018.Term W E P T = (CoppockWechsler2018.Context W E P T → E → E)

def CoppockWechsler2018.I {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} : Term W E P T

The pronoun I denotes the speaker of the context.

Equations

• CoppockWechsler2018.I c x✝ = c.agent

def CoppockWechsler2018.you {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} : Term W E P T

The pronoun you denotes the addressee of the context.

Equations

• CoppockWechsler2018.you c x✝ = c.addressee

def CoppockWechsler2018.auth {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} : Term W E P T

The term auth denotes the authority of the context.

Equations

• CoppockWechsler2018.auth c x✝ = c.authority

def CoppockWechsler2018.self {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} : Term W E P T

The term self denotes the perspectival center.

Equations

• CoppockWechsler2018.self x✝ a = a

def CoppockWechsler2018.name {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (x : E) : Term W E P T

A name denotes the same individual at every context and center.

Equations

• CoppockWechsler2018.name x x✝¹ x✝ = x

@[reducible, inline]

abbrev CoppockWechsler2018.CenteredProp (W : Type u_5) (E : Type u_6) : Type (max u_6 u_5)

A centered proposition is true, false or undefined at a world together with a center. It is undefined where its presupposition fails.

Equations

• CoppockWechsler2018.CenteredProp W E = (Pearson2015.Centered W E → SignType)

noncomputable def CoppockWechsler2018.ego {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (V : E → W → Prop) (t : Term W E P T) (c : Context W E P T) : CenteredProp W E

The meaning of a clause whose verb carries the egophoric suffix. It asserts that the subject has the property V and presupposes that the subject is the center.

Equations

• CoppockWechsler2018.ego V t c = {p : Pearson2015.Centered W E | t c p.2 = p.2}.indicator fun (p : Pearson2015.Centered W E) => SignType.ofProp (V (t c p.2) p.1)

noncomputable def CoppockWechsler2018.plain {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (V : E → W → Prop) (t : Term W E P T) (c : Context W E P T) : CenteredProp W E

The meaning of a clause whose verb is in the plain form. It asserts that the subject has the property V and presupposes nothing.

Equations

• CoppockWechsler2018.plain V t c p = SignType.ofProp (V (t c p.2) p.1)

noncomputable def CoppockWechsler2018.egoAuth {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (V : E → W → Prop) (t : Term W E P T) (c : Context W E P T) : CenteredProp W E

The meaning of an egophoric clause on the authority-indexical account, which presupposes that the subject is the authority of the context rather than the center.

Equations

• CoppockWechsler2018.egoAuth V t c = {p : Pearson2015.Centered W E | t c p.2 = c.authority}.indicator fun (p : Pearson2015.Centered W E) => SignType.ofProp (V (t c p.2) p.1)

def CoppockWechsler2018.uncenter {W : Type u_1} {E : Type u_2} (φ : CenteredProp W E) (x : E) : Set W

Filling in x as the center of a centered proposition gives an ordinary proposition, the set of worlds where it is defined and true of x.

Equations

• CoppockWechsler2018.uncenter φ x = {w : W | φ (w, x) = 1}

@[simp]

theorem CoppockWechsler2018.ego_eq_one_iff {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {V : E → W → Prop} {t : Term W E P T} {c : Context W E P T} {p : Pearson2015.Centered W E} : ego V t c p = 1 ↔ t c p.2 = p.2 ∧ V (t c p.2) p.1

@[simp]

theorem CoppockWechsler2018.plain_eq_one_iff {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {V : E → W → Prop} {t : Term W E P T} {c : Context W E P T} {p : Pearson2015.Centered W E} : plain V t c p = 1 ↔ V (t c p.2) p.1

theorem CoppockWechsler2018.uncenter_ego_of_eq {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {V : E → W → Prop} {t : Term W E P T} {c : Context W E P T} {x : E} (h : t c x = x) : uncenter (ego V t c) x = {w : W | V x w}

theorem CoppockWechsler2018.uncenter_ego_of_ne {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {V : E → W → Prop} {t : Term W E P T} {c : Context W E P T} {x : E} (h : t c x ≠ x) : uncenter (ego V t c) x = ∅

theorem CoppockWechsler2018.uncenter_neg_ego_of_eq {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {V : E → W → Prop} {t : Term W E P T} {c : Context W E P T} {x : E} (h : t c x = x) : uncenter (-ego V t c) x = {w : W | V x w}ᶜ

theorem CoppockWechsler2018.uncenter_neg_ego_of_ne {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {V : E → W → Prop} {t : Term W E P T} {c : Context W E P T} {x : E} (h : t c x ≠ x) : uncenter (-ego V t c) x = ∅

theorem CoppockWechsler2018.uncenter_egoAuth {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {V : E → W → Prop} {t : Term W E P T} {c : Context W E P T} : uncenter (egoAuth V t c) c.authority = uncenter (ego V t c) c.authority

In a main clause the two accounts propose the same thing for the common ground.

Moves on the Table

def CoppockWechsler2018.assert {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (K : Commitment.Table E W) (c : Context W E P T) (φ : CenteredProp W E) : Commitment.Table E W

Asserting φ commits the authority of the context and proposes φ, with the authority as center, for the common ground.

Equations

• CoppockWechsler2018.assert K c φ = K.assert c.authority (CoppockWechsler2018.uncenter φ c.authority)

def CoppockWechsler2018.ask {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (K : Commitment.Table E W) (c : Context W E P T) (φ : CenteredProp W E) : Commitment.Table E W

Asking whether φ puts its two answers on the Table, each with the authority as center. Both answers keep the presupposition of φ.

Equations

• CoppockWechsler2018.ask K c φ = K.push (Question.ofSet (CoppockWechsler2018.uncenter φ c.authority) ⊔ Question.ofSet (CoppockWechsler2018.uncenter (-φ) c.authority))

theorem CoppockWechsler2018.inCrisis_push_ofSet_empty {W : Type u_1} {E : Type u_2} {K : Commitment.Table E W} : (K.push (Question.ofSet ∅)).InCrisis

If the only answer to the issue on top of the Table is the empty proposition, the conversation has no consistent continuation.

theorem CoppockWechsler2018.inCrisis_assert_ego {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {V : E → W → Prop} {t : Term W E P T} {c : Context W E P T} {K : Commitment.Table E W} (h : t c c.authority ≠ c.authority) : (assert K c (ego V t c)).InCrisis

Asserting an egophoric clause whose subject is not the authority leaves the conversation with no consistent continuation.

theorem CoppockWechsler2018.inCrisis_ask_ego {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {V : E → W → Prop} {t : Term W E P T} {c : Context W E P T} {K : Commitment.Table E W} (h : t c c.authority ≠ c.authority) : (ask K c (ego V t c)).InCrisis

Asking an egophoric question whose subject is not the authority leaves the conversation with no consistent continuation.

theorem CoppockWechsler2018.assert_ego_of_eq {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {V : E → W → Prop} {t : Term W E P T} {c : Context W E P T} {K : Commitment.Table E W} (h : t c c.authority = c.authority) : assert K c (ego V t c) = K.assert c.authority {w : W | V c.authority w}

When the subject is the authority, asserting an egophoric clause is an ordinary assertion that the authority has the property.

theorem CoppockWechsler2018.ask_ego_of_eq {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {V : E → W → Prop} {t : Term W E P T} {c : Context W E P T} {K : Commitment.Table E W} (h : t c c.authority = c.authority) : ask K c (ego V t c) = K.polarQuestion {w : W | V c.authority w}

When the subject is the authority, asking an egophoric question is an ordinary polar question about whether the authority has the property.

theorem CoppockWechsler2018.not_inCrisis_assert_ego {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {V : E → W → Prop} {t : Term W E P T} {c : Context W E P T} {K : Commitment.Table E W} (h : t c c.authority = c.authority) (hK : K.IsStable) (hV : K.commonGround ⊓ Filter.principal {w : W | V c.authority w} ≠ ⊥) : ¬(assert K c (ego V t c)).InCrisis

When the subject is the authority, an egophoric assertion can be continued consistently, provided the Table is empty and the common ground allows that the authority has the property.

theorem CoppockWechsler2018.not_inCrisis_ask_ego {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {V : E → W → Prop} {t : Term W E P T} {c : Context W E P T} {K : Commitment.Table E W} (h : t c c.authority = c.authority) (hK : K.IsStable) (hV : K.commonGround ⊓ Filter.principal {w : W | V c.authority w} ≠ ⊥) (hV' : K.commonGround ⊓ Filter.principal {w : W | V c.authority w}ᶜ ≠ ⊥) : ¬(ask K c (ego V t c)).InCrisis

When the subject is the authority, an egophoric question can be continued consistently, provided the Table is empty and the common ground leaves open whether the authority has the property.

Which subjects the egophoric form allows

theorem CoppockWechsler2018.inCrisis_assert_ego_you {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {V : E → W → Prop} {c : Context W E P T} {K : Commitment.Table E W} (hne : c.agent ≠ c.addressee) (hc : c.IsDeclarative) : (assert K c (ego V you c)).InCrisis

A statement with you as the subject of an egophoric verb has no consistent continuation.

theorem CoppockWechsler2018.inCrisis_ask_ego_I {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {V : E → W → Prop} {c : Context W E P T} {K : Commitment.Table E W} (hne : c.agent ≠ c.addressee) (hc : c.IsInterrogative) : (ask K c (ego V I c)).InCrisis

A question with I as the subject of an egophoric verb has no consistent continuation.

theorem CoppockWechsler2018.inCrisis_assert_ego_I_of_source {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {V : E → W → Prop} {c : Context W E P T} {K : Commitment.Table E W} (hs : c.agent ≠ c.authority) : (assert K c (ego V I c)).InCrisis

When an evidential makes someone other than the speaker the authority, a statement with I as the subject of an egophoric verb has no consistent continuation.

theorem CoppockWechsler2018.eq_authority_of_not_inCrisis_assert {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {V : E → W → Prop} {t : Term W E P T} {c : Context W E P T} {K : Commitment.Table E W} (h : ¬(assert K c (ego V t c)).InCrisis) : t c c.authority = c.authority

If an egophoric assertion can be continued consistently, its subject is the authority.

theorem CoppockWechsler2018.eq_authority_of_not_inCrisis_ask {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {V : E → W → Prop} {t : Term W E P T} {c : Context W E P T} {K : Commitment.Table E W} (h : ¬(ask K c (ego V t c)).InCrisis) : t c c.authority = c.authority

If an egophoric question can be continued consistently, its subject is the authority.

The paper's examples

def CoppockWechsler2018.subject? {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (r : Datum) : Option (Term W E P T)

The subject of an example is I or you, according to the person of its pronoun.

Equations

• CoppockWechsler2018.subject? r = match r.feature? "subject" with | some "1" => some CoppockWechsler2018.I | some "2" => some CoppockWechsler2018.you | x => none

def CoppockWechsler2018.context? {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (r : Datum) (c₀ : Reference.Context W E P T) : Option (Context W E P T)

The context of an example has the speaker as its authority if the example is a statement and the addressee if it is a question.

Equations

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

theorem CoppockWechsler2018.ego_acceptable_iff {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c₀ : Reference.Context W E P T) (hne : c₀.agent ≠ c₀.addressee) (r : Datum) : r ∈ Examples.all → r.feature? "marking" = some "ego" → ∃ t ∈ subject? r, ∃ c ∈ context? r c₀, r.judgment = Judgment.acceptable ↔ t c c.authority = c.authority

Among the paper's examples with an egophoric verb, the acceptable ones are exactly those whose subject is the authority.

Speech reports

def CoppockWechsler2018.Says {W : Type u_1} {E : Type u_2} (R : Pearson2015.Centered W E → Pearson2015.Centered W E → Prop) (x : E) (φ : CenteredProp W E) (w : W) : Prop

x says φ in w when φ is defined and true at every world and center compatible with what x says in w.

Equations

• CoppockWechsler2018.Says R x φ w = ∀ (p : Pearson2015.Centered W E), R (w, x) p → φ p = 1

noncomputable def CoppockWechsler2018.report {W : Type u_1} {E : Type u_2} (R : Pearson2015.Centered W E → Pearson2015.Centered W E → Prop) (x : E) (φ : CenteredProp W E) : CenteredProp W E

The meaning of x says that φ, which is the same at every center.

Equations

• CoppockWechsler2018.report R x φ p = SignType.ofProp (CoppockWechsler2018.Says R x φ p.1)

@[simp]

theorem CoppockWechsler2018.report_eq_one_iff {W : Type u_1} {E : Type u_2} {x : E} {R : Pearson2015.Centered W E → Pearson2015.Centered W E → Prop} {φ : CenteredProp W E} {p : Pearson2015.Centered W E} : report R x φ p = 1 ↔ Says R x φ p.1

theorem CoppockWechsler2018.says_iff_sayDeSe {W : Type u_1} {E : Type u_2} {x : E} {R : Pearson2015.Centered W E → Pearson2015.Centered W E → Prop} {φ : CenteredProp W E} {w : W} {alts : List (Pearson2015.Centered W E)} (h : ∀ (p : Pearson2015.Centered W E), R (w, x) p ↔ p ∈ alts) : Says R x φ w ↔ Pearson2015.sayDeSe alts fun (a : E) (w' : W) => φ (w', a) = 1

Says agrees with Pearson2015.sayDeSe when the say relation is listed as alternatives.

theorem CoppockWechsler2018.says_ego_iff {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {V : E → W → Prop} {t : Term W E P T} {c : Context W E P T} {x : E} {R : Pearson2015.Centered W E → Pearson2015.Centered W E → Prop} {w : W} : Says R x (ego V t c) w ↔ (∀ (p : Pearson2015.Centered W E), R (w, x) p → t c p.2 = p.2) ∧ Says R x (ego V self c) w

An egophoric report is true exactly when the reported speaker takes the subject to be herself and ascribes the property to herself.

theorem CoppockWechsler2018.says_plain_of_says_ego {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {V : E → W → Prop} {t : Term W E P T} {c : Context W E P T} {x : E} {R : Pearson2015.Centered W E → Pearson2015.Centered W E → Prop} {w : W} (h : Says R x (ego V t c) w) : Says R x (plain V t c) w

If an egophoric report is true, so is the corresponding plain report.

structure CoppockWechsler2018.SelfAware {W : Type u_1} {E : Type u_2} (R : Pearson2015.Centered W E → Pearson2015.Centered W E → Prop) (x : E) : Prop

A speaker is self-aware when she says something at every world and takes herself to be who she is.

• serial (w : W) : ∃ (p : Pearson2015.Centered W E), R (w, x) p
• center (w : W) (p : Pearson2015.Centered W E) : R (w, x) p → p.2 = x

theorem CoppockWechsler2018.eq_of_says_report_ego {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {V : E → W → Prop} {c : Context W E P T} {x : E} {R : Pearson2015.Centered W E → Pearson2015.Centered W E → Prop} {w : W} {y z : E} (hy : ∀ (w : W), ∃ (p : Pearson2015.Centered W E), R (w, y) p) (hx : SelfAware R x) (h : Says R y (report R x (ego V (name z) c)) w) : z = x

When one report is embedded in another, the subject of the egophoric verb is the speaker of the inner report, whoever the outer speaker is.

The authority-indexical account

def CoppockWechsler2018.authorityShift {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (x : E) : Function.End (Context W E P T)

On the authority-indexical account a report shifts the context so that the reported speaker becomes the authority.

Equations

• CoppockWechsler2018.authorityShift x c = { toContext := c.toContext, authority := x }

theorem CoppockWechsler2018.isMonster_authorityShift {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {c : Context W E P T} {x : E} (h : c.authority ≠ x) : Reference.IsMonster (authorityShift x)

The shift changes the context, so it is a monster in Kaplan's sense.

theorem CoppockWechsler2018.says_egoAuth_name_iff {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} {V : E → W → Prop} {c : Context W E P T} {x : E} {R : Pearson2015.Centered W E → Pearson2015.Centered W E → Prop} {w : W} {z : E} (hR : ∃ (p : Pearson2015.Centered W E), R (w, x) p) : Says R x (egoAuth V (name z) (authorityShift x c)) w ↔ z = x ∧ Says R x (plain V (name z) c) w

On the authority-indexical account a shifted report about a named individual is true exactly when the individual is the reported speaker and the plain report is true.

The unrecognized photograph

Syam points at a photograph of a man with a lampshade on his head and says that guy drank too much. He does not realize that the man is himself.

inductive CoppockWechsler2018.Person : Type

The people of the scenario are Syam and the man Syam takes himself to be.

• syam : Person
• other : Person

@[instance_reducible]

instance CoppockWechsler2018.instDecidableEqPerson : DecidableEq Person

Equations

• CoppockWechsler2018.instDecidableEqPerson x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive CoppockWechsler2018.World : Type

The worlds of the scenario are the actual world and the world as Syam describes it.

• actual : World
• said : World

@[instance_reducible]

instance CoppockWechsler2018.instDecidableEqWorld : DecidableEq World

Equations

• CoppockWechsler2018.instDecidableEqWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def CoppockWechsler2018.sayAlt : Pearson2015.Centered World Person → Pearson2015.Centered World Person → Prop

Everything Syam says is compatible with his being someone other than the man in the photograph.

Equations

• CoppockWechsler2018.sayAlt p q = (p = (CoppockWechsler2018.World.actual, CoppockWechsler2018.Person.syam) ∧ q = (CoppockWechsler2018.World.said, CoppockWechsler2018.Person.other))

def CoppockWechsler2018.drank : Person → World → Prop

The man in the photograph drank too much in the world Syam describes.

Equations

• CoppockWechsler2018.drank x w = (x = CoppockWechsler2018.Person.syam ∧ w = CoppockWechsler2018.World.said)

theorem CoppockWechsler2018.lampshade (c : Context World Person Unit Unit) : Says sayAlt Person.syam (plain drank (name Person.syam) c) World.actual ∧ ¬Says sayAlt Person.syam (ego drank (name Person.syam) c) World.actual ∧ Says sayAlt Person.syam (egoAuth drank (name Person.syam) (authorityShift Person.syam c)) World.actual

In the photograph scenario the plain report is true and the egophoric report is false. The authority-indexical account makes the egophoric report true, because it checks only that the subject is the reported speaker.