Ney (2026): Insinuative reference and the coordination account

In insinuative reference ([Ney26]) a speaker uses a demonstrative, or another expression whose meaning must be supplemented in context, so that an innocuous avowable referent and a taboo unavowed referent are both possible semantic values; she intends the unavowed one and keeps the ability to deny it. Ney argues that the unavowed referent is a genuine semantic value (claim (i)), yet after the utterance it is available from the common ground neither that it is one (iia) nor that the speaker intended it to be (iib). This challenges the coordination account of [Kin13], on which a use has o as its semantic value iff (A) the speaker intends o and (B) a competent, reasonable, attentive hearer who knows the common ground would recognise that intention: given that the hearer's reasonableness is common ground (⟨TWO⟩), (B) seems to carry the intention and the reference into the common ground (⟨THREE⟩, ⟨FOUR⟩). Ney's reply is that the step needs a hidden premise, ⟨TWO*⟩, that it is common ground that a reasonable hearer would recognise the intention. Each interlocutor has a conception of reasonableness, her beliefs about which referential intentions every reasonable hearer would recognise; the account's conception is the intersection of the interlocutors'; and in insinuative reference the interlocutors share the relevant conception without that being common ground.

Hearers and the intentions they would recognise form a formal context in the sense of Mathlib.Order.Concept: the hearers reasonable by a conception's lights are its lowerPolar, and (B) over a set of hearers is membership in its upperPolar. The revised account (Model.semanticValues) quantifies over the hearers reasonable by the lights of at least one interlocutor, as Ney's revised statement does, and for conceptions closed under recognition this is the intersection of the conceptions (Model.semanticValues_eq); without closure the intersection formulation is strictly stronger (exists_mem_upperPolar_iUnion_not_mem). The chain is Model.commonKnowledge_mem_recognized (⟨TWO⟩ and ⟨TWO*⟩ give ⟨THREE⟩) and Model.commonKnowledge_mem_intends (⟨THREE⟩ contradicts (iib)). The reply is Model.not_commonKnowledge_mem_semanticValues and Model.not_commonKnowledge_mem_intends: a conception that is not common ground blocks (iia), and the speaker's blocks (iib). On a frame where each interlocutor knows her own conception and nothing about the other's, example (2) satisfies claim (i), ⟨TWO⟩, (iia) and (iib) together, with the speaker privately believing that the addressee recognises her intention (insinuation). On the same frame, the John Lennon example, whose referent every conception licenses, reaches the common ground (lennon). Deniability therefore sits in ⟨TWO*⟩ rather than ⟨TWO⟩, which is why denying ⟨TWO⟩, Ney's rejected first pass, would make the Lennon reference deniable too.

Implementation notes

A model fixes one use of a supplementive, so a conception of reasonableness restricted to the use is a set of candidate referents. What King's idealised hearer knows of the common ground, and the audience properties the common ground attributes to them ([Kin14a], via Ney's footnote 1), are absorbed into the recognition relation. The common ground is common knowledge among the interlocutors, the iterated mutual acceptance Ney describes ([Sta02]), and accessibility is read as "for all a knows", the modality of Ney's reasoning for ⟨TWO*⟩; the Filter common ground of Discourse.CommonGround inherits the results through Filter.GroundedIn (insinuation.not_mem_of_groundedIn). The speaker's intended referents form a set, since claim (i) lets avowable referents be semantic values as well. The paper passes from the intersection of the conceptions to "reasonable by the lights of at least one" with "Thus"; the IsIntent field states the closure this step needs, on the reading that a conception's "implicit and explicit beliefs" include whatever every hearer reasonable by it recognises.

TODO

Ney's three arguments for claim (i) against reading insinuative reference as indirect speech, the anaphora argument among them, the dialogue evidence for (iia) and (iib), and the reply about uptake need an implicature, anaphora and update apparatus; here they are premises. The distinctions from [Cam18]'s insinuation and from dogwhistles ([HMcC24]) are not formalized, and the paper's examples are not yet rows of Data/Examples.

References

• [Ney26]
• [Kin13]
• [Kin14a]
• [Sta02]
• [Cam18]
• [HMcC24]

Conceptions of reasonableness

theorem Ney2026.exists_mem_upperPolar_iUnion_not_mem : ∃ (r : Bool → Bool → Prop) (K : Discourse.Role → Set Bool), ∃ e ∈ upperPolar r (⋃ (a : Discourse.Role), lowerPolar r (K a)), e ∉ upperPolar r (lowerPolar r (⋂ (a : Discourse.Role), K a))

The intersection formulation ([Ney26] p. 326) is at least as strong as "reasonable by the lights of at least one" (p. 327), and strictly stronger for conceptions that are not closed under recognition: a hearer recognising everything counts as reasonable by either conception below, a hearer recognising nothing only by their empty intersection.

structure Ney2026.Model (W : Type u_1) (H : Type u_2) (E : Type u_3) : Type (max (max u_1 u_2) u_3)

A conversation about one use of a supplementive, with worlds W, hearers H and candidate semantic values E.

• belief : Discourse.Role → SetRel W W

  w ~[belief a] v: at w, for all a knows, the world is v.

• recognizes : H → E → Prop

  recognizes h e: hearer h would recognise an intention to make e the semantic value.

• conception : Discourse.Role → W → Set E

  a's conception of reasonableness at w, restricted to the use: the referents such that, by a's lights, every reasonable hearer would recognise an intention to refer to them ([Ney26] p. 326).

• isIntent_conception (a : Discourse.Role) (w : W) : Order.IsIntent self.recognizes (self.conception a w)

  A conception contains whatever every hearer reasonable by its lights recognises.

• intends : W → Set E

  The referents the speaker intends to be semantic values of the use.

• intends_subset_conception (w : W) : self.intends w ⊆ self.conception Discourse.Role.speaker w

  The speaker intends only what, by her own lights, a reasonable hearer would recognise: otherwise the utterance would not be an apt way to refer ([Ney26] p. 326).

• addressee : W → H

  The actual addressee.

The revised coordination account

def Ney2026.Model.reasonable {W : Type u_1} {H : Type u_2} {E : Type u_3} (M : Model W H E) (w : W) : Set H

The hearers reasonable by the lights of at least one interlocutor ([Ney26] p. 327).

Equations

• M.reasonable w = ⋃ (a : Discourse.Role), lowerPolar M.recognizes (M.conception a w)

theorem Ney2026.Model.reasonable_subset {W : Type u_1} {H : Type u_2} {E : Type u_3} (M : Model W H E) (w : W) : M.reasonable w ⊆ lowerPolar M.recognizes (⋂ (a : Discourse.Role), M.conception a w)

A hearer reasonable by either interlocutor's lights is reasonable by the intersection of their conceptions ([Ney26] p. 326).

def Ney2026.Model.semanticValues {W : Type u_1} {H : Type u_2} {E : Type u_3} (M : Model W H E) (w : W) : Set E

The semantic values of the use at w on the revised coordination account ([Ney26] p. 327): the referents the speaker intends whose intended reference every hearer reasonable by the lights of at least one interlocutor would recognise.

Equations

• M.semanticValues w = M.intends w ∩ upperPolar M.recognizes (M.reasonable w)

theorem Ney2026.Model.semanticValues_eq {W : Type u_1} {H : Type u_2} {E : Type u_3} (M : Model W H E) (w : W) : M.semanticValues w = M.intends w ∩ ⋂ (a : Discourse.Role), M.conception a w

The relevant conception is the intersection of the interlocutors' ([Ney26] p. 326).

@[simp]

theorem Ney2026.Model.mem_semanticValues {W : Type u_1} {H : Type u_2} {E : Type u_3} (M : Model W H E) {o : E} {w : W} : o ∈ M.semanticValues w ↔ o ∈ M.intends w ∧ ∀ (a : Discourse.Role), o ∈ M.conception a w

theorem Ney2026.Model.semanticValues_subset_intends {W : Type u_1} {H : Type u_2} {E : Type u_3} (M : Model W H E) (w : W) : M.semanticValues w ⊆ M.intends w

def Ney2026.Model.recognized {W : Type u_1} {H : Type u_2} {E : Type u_3} (M : Model W H E) (w : W) : Set E

The referents whose intended reference the addressee recognises.

Equations

• M.recognized w = M.intends w ∩ {e : E | M.recognizes (M.addressee w) e}

The prima facie challenge

theorem Ney2026.Model.commonKnowledge_mem_recognized {W : Type u_1} {H : Type u_2} {E : Type u_3} (M : Model W H E) {o : E} {w : W} (two : ModalLogic.CommonKnowledge M.belief Set.univ (fun (v : W) => M.addressee v ∈ M.reasonable v) w) (twoStar : ModalLogic.CommonKnowledge M.belief Set.univ (fun (x : W) => o ∈ M.semanticValues x) w) : ModalLogic.CommonKnowledge M.belief Set.univ (fun (x : W) => o ∈ M.recognized x) w

⟨TWO⟩ and ⟨TWO*⟩ give ⟨THREE⟩ ([Ney26] pp. 322, 325): if it is common ground that the addressee is reasonable and that o is a semantic value, it is common ground that the addressee recognises the intention to refer to o.

theorem Ney2026.Model.commonKnowledge_mem_intends {W : Type u_1} {H : Type u_2} {E : Type u_3} (M : Model W H E) {o : E} {w : W} (three : ModalLogic.CommonKnowledge M.belief Set.univ (fun (x : W) => o ∈ M.recognized x) w) : ModalLogic.CommonKnowledge M.belief Set.univ (fun (x : W) => o ∈ M.intends x) w

⟨THREE⟩ is incompatible with (iib) ([Ney26] p. 322): a common-ground recognition of the intention makes the intention common ground.

The response

theorem Ney2026.Model.not_commonKnowledge_mem_semanticValues {W : Type u_1} {H : Type u_2} {E : Type u_3} (M : Model W H E) {o : E} {w : W} (a : Discourse.Role) (h : ¬ModalLogic.CommonKnowledge M.belief Set.univ (fun (x : W) => o ∈ M.conception a x) w) : ¬ModalLogic.CommonKnowledge M.belief Set.univ (fun (x : W) => o ∈ M.semanticValues x) w

If it is not common ground that a's conception licenses o, it is not common ground that o is a semantic value (iia): ⟨TWO*⟩ fails ([Ney26] pp. 325–326).

theorem Ney2026.Model.not_commonKnowledge_mem_intends {W : Type u_1} {H : Type u_2} {E : Type u_3} (M : Model W H E) {o : E} {w : W} (h : ¬ModalLogic.CommonKnowledge M.belief Set.univ (fun (x : W) => o ∈ M.conception Discourse.Role.speaker x) w) : ¬ModalLogic.CommonKnowledge M.belief Set.univ (fun (x : W) => o ∈ M.intends x) w

If it is not common ground that the speaker's conception licenses o, it is not common ground that she intends o (iib): she can deny the intention by denying the conception ([Ney26] p. 326).

theorem Ney2026.isIntent_mem {E : Type u_1} (C : Set E) : Order.IsIntent (fun (h : Set E) (e : E) => e ∈ h) C

When hearers are the sets of referents they would recognise, every conception is closed.

Private conceptions

@[reducible, inline]

abbrev Ney2026.World : Type

A world records which interlocutors hold a conception licensing the unavowed referent.

Equations

• Ney2026.World = Finset Discourse.Role

def Ney2026.privately (a : Discourse.Role) : SetRel World World

Each interlocutor knows whether she holds the conception and nothing about the other.

Equations

• Ney2026.privately a = {p : Ney2026.World × Ney2026.World | a ∈ p.1 ↔ a ∈ p.2}

instance Ney2026.instIsS5FrameWorldPrivately (a : Discourse.Role) : ModalLogic.IsS5Frame (privately a)

Example (2)

inductive Ney2026.Referent : Type

The possible referents of they in (2), "They are crossing the border, bringing drugs, disease and crime" ([Ney26] p. 307): the unavowed Hispanic immigrants and the avowable gang members and drug smugglers (p. 308).

• hispanicImmigrants : Referent
• smugglers : Referent

def Ney2026.insinuation : Model World (Set Referent) Referent

Example (2): every conception licenses the avowable referent, and the insinuative one also licenses the unavowed referent; the speaker intends the unavowed referent when her conception licenses it and the avowable one otherwise; the addressee recognises what either conception requires.

Equations

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

theorem Ney2026.insinuation.mem_conception (a : Discourse.Role) : Referent.hispanicImmigrants ∈ insinuation.conception a Finset.univ

In fact both interlocutors hold the conception ([Ney26] p. 326).

theorem Ney2026.insinuation.mem_semanticValues : Referent.hispanicImmigrants ∈ insinuation.semanticValues Finset.univ

Claim (i): the unavowed referent is a semantic value.

theorem Ney2026.insinuation.not_knows_speaker : ¬ModalLogic.Box (insinuation.belief Discourse.Role.speaker) (fun (x : World) => Referent.hispanicImmigrants ∈ insinuation.conception Discourse.Role.addressee x) Finset.univ

The speaker does not know the addressee shares her conception ([Ney26] p. 326).

theorem Ney2026.insinuation.not_knows_addressee : ¬ModalLogic.Box (insinuation.belief Discourse.Role.addressee) (fun (x : World) => Referent.hispanicImmigrants ∈ insinuation.conception Discourse.Role.speaker x) Finset.univ

The addressee does not know the speaker shares hers ([Ney26] p. 326).

theorem Ney2026.insinuation.knows_mem_recognized : ModalLogic.Box (insinuation.belief Discourse.Role.speaker) (fun (x : World) => Referent.hispanicImmigrants ∈ insinuation.recognized x) Finset.univ

The speaker knows that the addressee recognises the unavowed intention, an individual belief ([Ney26] p. 325).

theorem Ney2026.insinuation.not_knows_knows_mem_recognized : ¬ModalLogic.Box (insinuation.belief Discourse.Role.addressee) (ModalLogic.Box (insinuation.belief Discourse.Role.speaker) fun (x : World) => Referent.hispanicImmigrants ∈ insinuation.recognized x) Finset.univ

For all the addressee knows, the speaker does not know that the addressee recognises the unavowed intention ([Ney26] p. 325).

theorem Ney2026.insinuation.commonKnowledge_two : ModalLogic.CommonKnowledge insinuation.belief Set.univ (fun (v : World) => insinuation.addressee v ∈ insinuation.reasonable v) Finset.univ

⟨TWO⟩: it is common ground that the addressee is reasonable ([Ney26] p. 325).

theorem Ney2026.insinuation.not_commonKnowledge_mem_semanticValues : ¬ModalLogic.CommonKnowledge insinuation.belief Set.univ (fun (x : World) => Referent.hispanicImmigrants ∈ insinuation.semanticValues x) Finset.univ

(iia): it is not common ground that the unavowed referent is a semantic value.

theorem Ney2026.insinuation.not_commonKnowledge_mem_intends : ¬ModalLogic.CommonKnowledge insinuation.belief Set.univ (fun (x : World) => Referent.hispanicImmigrants ∈ insinuation.intends x) Finset.univ

(iib): it is not common ground that the speaker intended it.

theorem Ney2026.insinuation.not_mem_of_groundedIn {cg : Filter World} (h : cg.GroundedIn insinuation.belief Set.univ) (hw : Finset.univ ∈ cg.ker) : {v : World | Referent.hispanicImmigrants ∈ insinuation.intends v} ∉ cg

(iib) for any Filter common ground grounded in the interlocutors' common knowledge whose context set contains the actual world.

theorem Ney2026.insinuation.eavesdropper : Referent.hispanicImmigrants ∈ insinuation.recognized {Discourse.Role.speaker} ∧ Referent.hispanicImmigrants ∉ insinuation.semanticValues {Discourse.Role.speaker}

The eavesdropper ([Ney26] pp. 325–326): where only the speaker holds the conception, the addressee recognises the intention, yet the unavowed referent is not a semantic value.

The Lennon example

inductive Ney2026.LennonReferent : Type

The possible referents in "this is where John Lennon was born", said pointing across a busy street ([Ney26] p. 324).

• house : LennonReferent
• car : LennonReferent

def Ney2026.lennon : Model World (Set LennonReferent) LennonReferent

The Lennon example on the same frame: every conception licenses the house.

Equations

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

theorem Ney2026.lennon_commonKnowledge_mem_recognized : ModalLogic.CommonKnowledge lennon.belief Set.univ (fun (x : World) => LennonReferent.house ∈ lennon.recognized x) Finset.univ

With ⟨TWO⟩ as in example (2), the reference to the house is common ground: denying ⟨TWO*⟩, not ⟨TWO⟩, separates insinuative reference from ordinary reliance on a reasonable hearer ([Ney26] p. 324).