Kirk-Giannini 2024: Covert mixed quotation

Mixed quotation arises compositionally from pure quotation and a phonologically null operator 𝔐 with two meanings, both saturated by its pure-quoted sister q: the at-issue ⦇q⦈(w_c)(s_x), the extension of q as uttered by the anaphorically retrieved speaker s_x at the world of the context ([Sha10]'s quotative interpretation function ⦇∗⦈), and the peripheral R(s_x, u_x, q), that s_x produced the utterance u_x of q ([Pot05]'s second dimension, as [Pot07a] uses it for quotation). Three further covert items combine with it: ↓ shunts the peripheral proposition into the at-issue dimension, † diagonalizes ⦇∗⦈ so that q means at a world w what s_x would mean by it there, and 𝔄 is the appropriateness modal ⧫ applied to 𝔐's peripheral proposition. Covert 𝔐 then accounts for non-projecting CI items (26″), c-monsters (29, [KJR20]'s Pluto data), metalinguistic negation (3, [Hor89]), metalinguistic negotiation (6, [PS13]'s Secretariat dispute) and 'in a sense' (7′).

Model interprets ⦇∗⦈, R and the accessibility relation of ⧫ in the appendix's intended model, with the output type of ⦇∗⦈ fixed to propositions; mq, shunt, approp and Model.dagger are the four covert items on TwoDim, † being Function.extend, so that Model.exists_dagger_iff identifies the paper's footnote-22 assumption with Function.FactorsThrough; appropAssertion and metaNeg are the forms ↓[… 𝔄𝔐q …] and its negation, whose at-issue content metaNeg_atIssue_iff gives as ¬p ∨ ¬⧫R. Parsetrees and the tree admissibility conditions are not represented, each rule appearing as the operator it licenses.

References

• C. D. Kirk-Giannini, Covert Mixed Quotation (2024)
• C. Shan, The character of quotation (2010)
• C. Potts, The Logic of Conventional Implicatures (2005)
• C. Potts, The dimensions of quotation (2007)
• E. McCready, Varieties of conventional implicature (2010)
• A. W. Kocurek, E. Jerzak and R. E. Rudolph, Against conventional wisdom (2020)
• L. R. Horn, A Natural History of Negation (1989)
• D. Plunkett and T. Sundell, Disagreement and the semantics of normative and evaluative terms (2013)
• R. C. Stalnaker, A Theory of Conditionals (1968)

structure KirkGiannini2024.Model (W : Type u_1) (Expr : Type u_2) (Speaker : Type u_3) (Utt : Type u_4) : Type (max (max (max u_1 u_2) u_3) u_4)

The constants of ℒ_MQ interpreted in the intended model.

• quot : Expr → W → Speaker → W → Prop

  ⦇∗⦈: quot q w₁ s is the intension contributed by an utterance of q by s at w₁.

• utter : Speaker → Utt → Expr → W → Prop

  R: utter s u q w iff s produces the utterance u of q at w.

• appropriate : SetRel W W

  Accessibility of ⧫, □[M.appropriate]: w ~[appropriate] v iff v is among the worlds characterizing what is or would be appropriate at w.

Diagonalization

def KirkGiannini2024.Model.mqAtIssue {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (wc : W) (s : Speaker) : Expr → W → Prop

𝔐's at-issue meaning λq.⦇q⦈(w_c)(s) as a function of the speaker s.

Equations

• M.mqAtIssue wc s q = M.quot q wc s

def KirkGiannini2024.Model.diag {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (s : Speaker) : Expr → W → Prop

⦇∗⦈∗: M.diag s q w is the extension at w of q as uttered by s at w.

Equations

• M.diag s q w = M.quot q w s w

theorem KirkGiannini2024.Model.mqAtIssue_wc {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (wc : W) (s : Speaker) (q : Expr) : M.mqAtIssue wc s q wc = M.diag s q wc

At the world of the context diagonalization is invisible, so (Conventional Wisdom) holds for unembedded material.

noncomputable def KirkGiannini2024.Model.dagger {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (wc : W) : (Expr → W → Prop) → Expr → W → Prop

† ⇝ λf | ∃s. f = λq.⦇q⦈(w_c)(s). f∗: ⦇∗⦈∗ extended along 𝔐's at-issue meaning. The paper leaves † undefined off that domain; Function.extend returns ⊥ there.

Equations

• M.dagger wc = Function.extend (M.mqAtIssue wc) M.diag ⊥

theorem KirkGiannini2024.Model.dagger_mqAtIssue {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (wc : W) (h : Function.FactorsThrough M.diag (M.mqAtIssue wc)) (s : Speaker) : M.dagger wc (M.mqAtIssue wc s) = M.diag s

The paper's footnote-22 assumption: no two speakers agree on the intensions of all expressions at w_c while differing on some at another world. Under it † returns ⦇∗⦈∗ of the speaker whose meaning it was given.

theorem KirkGiannini2024.Model.exists_dagger_iff {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (wc : W) : (∃ (d : (Expr → W → Prop) → Expr → W → Prop), ∀ (s : Speaker), d (M.mqAtIssue wc s) = M.diag s) ↔ Function.FactorsThrough M.diag (M.mqAtIssue wc)

The assumption is also necessary: some function sends each λq.⦇q⦈(w_c)(s) to ⦇∗⦈∗(s) iff ⦇∗⦈∗ factors through 𝔐's at-issue meaning.

The covert lexicon on two-dimensional meanings

def KirkGiannini2024.mq {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (wc : W) (sx : Speaker) (ux : Utt) (q : Expr) : ConventionalImplicature.TwoDim W (W → Prop)

𝔐 ⇝ λq.⦇q⦈(w_c)(s_x) • λq.R(s_x, u_x, q), both saturated by the pure-quoted sister q (a-to-p Shunting).

Equations

• KirkGiannini2024.mq M wc sx ux q = { atIssue := M.quot q wc sx, notAtIssue := M.utter sx ux q }

def KirkGiannini2024.shunt {W : Type u_1} (p : ConventionalImplicature.TwoDim W (W → Prop)) : ConventionalImplicature.TwoDim W (W → Prop)

↓ ⇝ λp.p̌ with p-to-a Shunting ([McC10b]): the peripheral proposition is conjoined with the at-issue one, and the single peripheral dimension is then empty.

Equations

• KirkGiannini2024.shunt p = { atIssue := p.atIssue ⊓ p.notAtIssue, notAtIssue := ⊤ }

def KirkGiannini2024.approp {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (p : ConventionalImplicature.TwoDim W (W → Prop)) : ConventionalImplicature.TwoDim W (W → Prop)

𝔄 ⇝ ⧫ with Peripheral Intensional Function Application: the peripheral proposition is replaced by ⧫ of its intension, the at-issue meaning passing up unchanged.

Equations

• KirkGiannini2024.approp M p = { atIssue := p.atIssue, notAtIssue := ModalLogic.Box M.appropriate p.notAtIssue }

noncomputable def KirkGiannini2024.daggerMQ {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (wc : W) (sx : Speaker) (ux : Utt) (q : Expr) : ConventionalImplicature.TwoDim W (W → Prop)

†𝔐: † applied to 𝔐's at-issue meaning, the peripheral meaning passing up unchanged.

Equations

• KirkGiannini2024.daggerMQ M wc sx ux q = { atIssue := M.dagger wc (M.mqAtIssue wc sx) q, notAtIssue := M.utter sx ux q }

@[simp]

theorem KirkGiannini2024.mq_atIssue {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (wc : W) (sx : Speaker) (ux : Utt) (q : Expr) (w : W) : (mq M wc sx ux q).atIssue w ↔ M.quot q wc sx w

@[simp]

theorem KirkGiannini2024.mq_notAtIssue {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (wc : W) (sx : Speaker) (ux : Utt) (q : Expr) (w : W) : (mq M wc sx ux q).notAtIssue w ↔ M.utter sx ux q w

@[simp]

theorem KirkGiannini2024.shunt_atIssue {W : Type u_1} (p : ConventionalImplicature.TwoDim W (W → Prop)) (w : W) : (shunt p).atIssue w ↔ p.atIssue w ∧ p.notAtIssue w

@[simp]

theorem KirkGiannini2024.shunt_notAtIssue {W : Type u_1} (p : ConventionalImplicature.TwoDim W (W → Prop)) (w : W) : (shunt p).notAtIssue w

@[simp]

theorem KirkGiannini2024.approp_atIssue {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (p : ConventionalImplicature.TwoDim W (W → Prop)) (w : W) : (approp M p).atIssue w ↔ p.atIssue w

@[simp]

theorem KirkGiannini2024.approp_notAtIssue {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (p : ConventionalImplicature.TwoDim W (W → Prop)) (w : W) : (approp M p).notAtIssue w ↔ ModalLogic.Box M.appropriate p.notAtIssue w

theorem KirkGiannini2024.daggerMQ_atIssue {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (wc : W) (sx : Speaker) (ux : Utt) (h : Function.FactorsThrough M.diag (M.mqAtIssue wc)) (q : Expr) : (daggerMQ M wc sx ux q).atIssue = M.diag sx q

theorem KirkGiannini2024.shunt_mq_atIssue {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (wc : W) (sx : Speaker) (ux : Utt) (q : Expr) (w : W) : (shunt (mq M wc sx ux q)).atIssue w ↔ M.quot q wc sx w ∧ M.utter sx ux q w

(10′) and (12): ↓ at the clause boundary makes 'Peter orders ‘[eI]pricots’' say that Peter orders apricots and utters ‘[eI]pricots’ in so doing, available to a higher quantifier or conditional.

Conventional implicature items (§3)

theorem KirkGiannini2024.report_mq {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (wc : W) (sx : Speaker) (ux : Utt) (lex : Expr → ConventionalImplicature.TwoDim W (W → Prop)) (F : (W → Prop) → W → Prop) (q : Expr) (h : M.quot q wc sx = (lex q).atIssue) : (F <$> mq M wc sx ux q).atIssue = (F <$> lex q).atIssue ∧ (F <$> mq M wc sx ux q).notAtIssue = M.utter sx ux q

(26) and (26″): a speech report F of a CI item q whose meaning is lex q, whose peripheral content projects unquoted (TwoDim.map_notAtIssue) but, 𝔪-quoted, is replaced by the attribution R(s_x, u_x, q) while the at-issue content is unchanged, given that ⦇∗⦈ returns only at-issue content.

C-monsters (§4)

theorem KirkGiannini2024.selectionConditional_daggerMQ {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (wc : W) (sx : Speaker) (ux : Utt) (h : Function.FactorsThrough M.diag (M.mqAtIssue wc)) (s : Conditional.SelectionFunction W) (q : Expr) (C : Set W) (w : W) (hq : {v : W | M.quot q v sx v}.Nonempty) : w ∈ Conditional.selectionConditional s {v : W | (daggerMQ M wc sx ux q).atIssue v} C ↔ s.sel w {v : W | M.quot q v sx v} ∈ C

(29) 'If Pluto were a planet, …' with †𝔐 around 'planet': the antecedent contributes the diagonal ⦇'planet'⦈∗(s_x), so a [Sta68] selection function takes the conditional to the nearest world whose conventions for 'planet', as s_x would use it there, include Pluto, when there is such a world.

Metalinguistic negation and negotiation (§5–6)

def KirkGiannini2024.appropAssertion {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (wc : W) (sx : Speaker) (ux : Utt) (q : Expr) : ConventionalImplicature.TwoDim W (W → Prop)

↓[… 𝔄𝔐q …]: the quoted clause conjoined with the appropriateness of q's verbatim use. A's assertion in (6), the antecedent of (35″), the prejacent of (36).

Equations

• KirkGiannini2024.appropAssertion M wc sx ux q = KirkGiannini2024.shunt (KirkGiannini2024.approp M (KirkGiannini2024.mq M wc sx ux q))

def KirkGiannini2024.metaNeg {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (wc : W) (sx : Speaker) (ux : Utt) (q : Expr) : ConventionalImplicature.TwoDim W (W → Prop)

not ↓[… 𝔄𝔐q …]: metalinguistic negation, (3), and B's denial in (6).

Equations

• KirkGiannini2024.metaNeg M wc sx ux q = (KirkGiannini2024.appropAssertion M wc sx ux q).neg

theorem KirkGiannini2024.appropAssertion_atIssue {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (wc : W) (sx : Speaker) (ux : Utt) (q : Expr) (w : W) : (appropAssertion M wc sx ux q).atIssue w ↔ M.quot q wc sx w ∧ ModalLogic.Box M.appropriate (M.utter sx ux q) w

theorem KirkGiannini2024.metaNeg_atIssue {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (wc : W) (sx : Speaker) (ux : Utt) (q : Expr) (w : W) : (metaNeg M wc sx ux q).atIssue w ↔ ¬(M.quot q wc sx w ∧ ModalLogic.Box M.appropriate (M.utter sx ux q) w)

theorem KirkGiannini2024.metaNeg_atIssue_iff {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (wc : W) (sx : Speaker) (ux : Utt) (q : Expr) (w : W) : (metaNeg M wc sx ux q).atIssue w ↔ ¬M.quot q wc sx w ∨ ¬ModalLogic.Box M.appropriate (M.utter sx ux q) w

(3) is true iff the quoted clause fails or its verbatim use is inappropriate.

theorem KirkGiannini2024.metaNeg_atIssue_iff_not {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (wc : W) (sx : Speaker) (ux : Utt) (q : Expr) (w : W) : (metaNeg M wc sx ux q).atIssue w ↔ ¬(appropAssertion M wc sx ux q).atIssue w

B's utterance in (6) expresses the negation of A's, the retrieved speaker and utterance being the same: the disputants' contents are incompatible.

theorem KirkGiannini2024.metaNeg_correction {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (wc : W) (sx : Speaker) (ux : Utt) {q q' : Expr} {w : W} (h : M.quot q wc sx = M.quot q' wc sx) (h₁ : (metaNeg M wc sx ux q).atIssue w) (h₂ : (mq M wc sx ux q').atIssue w) : ¬ModalLogic.Box M.appropriate (M.utter sx ux q) w

The correction in (3): its second clause q' ('mongooses') expresses in the mouth of s_x what q ('mongeese') does, so together with it the first clause entails that using q is not appropriate.

theorem KirkGiannini2024.metaNeg_of_not_box {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (wc : W) (sx : Speaker) (ux : Utt) {q : Expr} {w : W} (hb : ¬ModalLogic.Box M.appropriate (M.utter sx ux q) w) : (metaNeg M wc sx ux q).atIssue w

Whenever verbatim use of q is inappropriate, (3)'s form is true whatever the quoted clause's truth value: (37) 'She's not happy' can be said of someone ecstatic, whereas (38) 'She's unhappy', whose negation is incorporated below the covert material, cannot.

theorem KirkGiannini2024.metaNeg_compl {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (wc : W) (sx : Speaker) (ux : Utt) {q q₀ : Expr} {w : W} (h : M.quot q wc sx = (M.quot q₀ wc sx)ᶜ) : (metaNeg M wc sx ux q).atIssue w ↔ M.quot q₀ wc sx w ∨ ¬ModalLogic.Box M.appropriate (M.utter sx ux q) w

(41) 'She's not not happy' with 'not happy' 𝔪-quoted says that she is happy or that 'not happy' is inappropriate, so (42) 'She's happy' does not follow: double negation is not eliminated.

theorem KirkGiannini2024.appropAssertion_atIssue_iff_box {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (wc : W) (sx : Speaker) (ux : Utt) {q : Expr} {w : W} (hp : M.quot q wc sx w) : (appropAssertion M wc sx ux q).atIssue w ↔ ModalLogic.Box M.appropriate (M.utter sx ux q) w

(6) with its uncontroversial at-issue content granted: A asserts that characterizing Secretariat with 'athlete' is appropriate.

theorem KirkGiannini2024.metaNeg_atIssue_iff_not_box {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (wc : W) (sx : Speaker) (ux : Utt) {q : Expr} {w : W} (hp : M.quot q wc sx w) : (metaNeg M wc sx ux q).atIssue w ↔ ¬ModalLogic.Box M.appropriate (M.utter sx ux q) w

(6) with its uncontroversial at-issue content granted: B denies that characterizing Secretariat with 'athlete' is appropriate.

'In a sense' (§7)

def KirkGiannini2024.inTheSenseThat {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (wc : W) (q : Expr) (μ : W → Prop) (w : W) : Prop

'In The Sense That', (43): ⌜𝔪S𝔪 in the sense that S′⌝ with μ the intension of S′ is ∃s_x[⦇S⦈(w_c)(s_x) ∧ [^⦇S⦈(w_c)(s_x)] = μ], which as a predicate of μ is the relative clause of (7′).

Equations

• KirkGiannini2024.inTheSenseThat M wc q μ w = ∃ (s : Speaker), M.quot q wc s w ∧ M.quot q wc s = μ

def KirkGiannini2024.inASense {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (wc : W) (q : Expr) (w : W) : Prop

(7′) 'There is a sense which viruses are alive in': ∃μ∃s_x[…].

Equations

• KirkGiannini2024.inASense M wc q w = ∃ (μ : W → Prop), KirkGiannini2024.inTheSenseThat M wc q μ w

theorem KirkGiannini2024.inTheSenseThat_iff {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (wc : W) (q : Expr) (μ : W → Prop) (w : W) : inTheSenseThat M wc q μ w ↔ μ w ∧ ∃ (s : Speaker), M.quot q wc s = μ

theorem KirkGiannini2024.inASense_iff {W : Type u_1} {Expr : Type u_2} {Speaker : Type u_3} {Utt : Type u_4} (M : Model W Expr Speaker Utt) (wc : W) (q : Expr) (w : W) : inASense M wc q w ↔ ∃ (s : Speaker), M.quot q wc s w

(7′) is true iff some speaker's use of the sentence at w_c expresses a truth at w; the paper restricts the speakers quantified over to not-too-outlandish ones.