Kirk-Giannini 2024: Covert Mixed Quotation

@cite{kirk-giannini-2024}

Covert mixed quotation. Semantics and Pragmatics 17, Article 5: 1-54.

Overview

Five apparently distinct phenomena are derived from the interaction of covert mixed quotation 𝔐 with four additional operators (↓, †, 𝔄, and quantification over senses):

1. CI projection failure (§1, paper §3): Conventional implicature items (expressives, slurs, NRRCs) fail to project out of indirect speech reports because the embedded clause is first pure-quoted (stripping the original CI) before 𝔐 re-introduces a peripheral utterance attribution.

2. C-monsters (§2, paper §4): "Pluto could have been a planet" accesses the meaning 'planet' would have under different conventions via the diagonalizer †, which collapses the world of utterance into the world of evaluation. K-G's † is existentially closed over speakers/communities (paper fn 22).

3. Metalinguistic negation (§3, paper §5): "I didn't trap two MONGEESE" derives via the chain 𝔐 → 𝔄 → ↓ → ¬, with ↓ shunting the appropriateness content into the at-issue dimension before negation applies. The analysis predicts three syntactic restrictions identified by @cite{horn-1985} / @cite{horn-1989} and @cite{burton-roberts-1989}: morpheme incorporation failure, NPI licensing failure, and DN-elimination failure.

4. Metalinguistic negotiation (§4, paper §6): "Secretariat is / isn't an athlete" — A and B express literally incompatible appropriateness contents on a shared standard, contra @cite{plunkett-sundell-2013}'s "consistent contents" diagnosis.

5. "In a sense" (§5, paper §7): "Viruses are alive in a sense" contributes ∃μ ∃sₓ [⟨*⟩(q)(wc)(sₓ) ∧ [^⟨*⟩(q)(wc)(sₓ)] = μ] — an existential over BOTH speakers AND intensions, with which_μ binding via Predicate Abstraction.

Cross-framework theorem inventory

This module hosts 8 cross-framework refutation/bridge theorems that make K-G's incompatibilities with sibling analyses visible at theorem level (per linglib's "no bridge files" rule, comparisons live in the chronologically-later study file). Each theorem actually imports and invokes the named sibling's substrate — none is a docstring-only claim.

• kg_refutes_potts_universal_projection (§1) — invokes Pragmatics.Expressives.TwoDimProp.neg, exhibits divergence at .hypothetical
• kg_refutes_harris_potts_orientation (§1) — instantiates HarrisPotts2009.CIItem and compares resolution outcomes
• kg_refutes_maier_chameleonism (§1) — instantiates Maier2014.mq on the same input and shows daughter-CI passthrough vs. K-G's strip-then-mix yields divergent CI predictions
• diagonalize_no_kaplan_monster (§2) — defines kgEmbeddingShifts reflecting K-G's covert apparatus (4 identity shifts, one per operator) and proves KaplansThesisHolds non-vacuously via case-split
• kg_refutes_kjr_convention_shift (§2) — instantiates KJR's Convention and WC, exhibits a WC-pair where KJR's diagContent predicts True while K-G's diagonalizeKG predicts False
• kg_metalinguistic_chain_targets_appropriateness (§3) — exhibits the applyApprop chain producing appropriateness content (vs. Phenomena.Negation.Denial.DenialType.implicature's implicature layer)
• kg_refutes_plunkett_sundell (§4) — instantiates P&S's MetalinguisticDispute with K-G's shared standard and proves the P&S consistentContents predicate fails to hold
• in_a_sense_distinct_from_imprecision (§5) — exhibits speaker-locus variation, structurally distinct from granularity-locus accounts

§3 also lifts three syntactic predictions from Horn1989: mongeese_blocks_morpheme_incorporation, ..._npi_licensing, ..._dn_elimination. These are NOT framed as cross-framework theorems (K-G and Horn agree on the predictions, disagree only on the architecture that derives them).

Note on Denial Taxonomy

The three-way DenialType taxonomy (propositional / presuppositional / implicature) from @cite{van-der-sandt-maier-2003} — formalized in Phenomena/Negation/Denial.lean — groups register and connotation denials under implicature. K-G's analysis (paper §5, p.28-30) derives metalinguistic-negation truth conditions from ♦ (appropriateness modal) composed with 𝔐, with ↓ shunting before negation. The distinguishing feature of K-G's account is the appeal to appropriateness plus the syntactic predictions in §3 (NPI failure, morpheme incorporation failure, DN-elimination failure).

inductive KirkGiannini2024.ProjWorld : Type

Concrete world type for the CI projection scenarios — non-trivial so universal/existential quantification has computational content.

• actual : ProjWorld
• hypothetical : ProjWorld

@[implicit_reducible]

instance KirkGiannini2024.instDecidableEqProjWorld : DecidableEq ProjWorld

Equations

• KirkGiannini2024.instDecidableEqProjWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KirkGiannini2024.instReprProjWorld.repr : ProjWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KirkGiannini2024.instReprProjWorld : Repr ProjWorld

Equations

• KirkGiannini2024.instReprProjWorld = { reprPrec := KirkGiannini2024.instReprProjWorld.repr }

def KirkGiannini2024.instInhabitedProjWorld.default : ProjWorld

Equations

• KirkGiannini2024.instInhabitedProjWorld.default = KirkGiannini2024.ProjWorld.actual

@[implicit_reducible]

instance KirkGiannini2024.instInhabitedProjWorld : Inhabited ProjWorld

Equations

• KirkGiannini2024.instInhabitedProjWorld = { default := KirkGiannini2024.instInhabitedProjWorld.default }

inductive KirkGiannini2024.GDExpr : Type

Expressions in the 'goddamned keys' scenario.

• goddamnedKeys : GDExpr

@[implicit_reducible]

instance KirkGiannini2024.instDecidableEqGDExpr : DecidableEq GDExpr

Equations

• KirkGiannini2024.instDecidableEqGDExpr x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance KirkGiannini2024.instReprGDExpr : Repr GDExpr

Equations

• KirkGiannini2024.instReprGDExpr = { reprPrec := KirkGiannini2024.instReprGDExpr.repr }

def KirkGiannini2024.instReprGDExpr.repr : GDExpr → ℕ → Std.Format

Equations

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

inductive KirkGiannini2024.GDSpeaker : Type

Speakers: Jones (the original utterer) and the reporter.

• jones : GDSpeaker
• reporter : GDSpeaker

@[implicit_reducible]

instance KirkGiannini2024.instDecidableEqGDSpeaker : DecidableEq GDSpeaker

Equations

• KirkGiannini2024.instDecidableEqGDSpeaker x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance KirkGiannini2024.instReprGDSpeaker : Repr GDSpeaker

Equations

• KirkGiannini2024.instReprGDSpeaker = { reprPrec := KirkGiannini2024.instReprGDSpeaker.repr }

def KirkGiannini2024.instReprGDSpeaker.repr : GDSpeaker → ℕ → Std.Format

Equations

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

def KirkGiannini2024.gdInterp : Semantics.Quotation.QuotInterp GDExpr GDSpeaker ProjWorld

'Goddamned keys' denotes Jones-spent-an-hour-looking-for-his-keys. At-issue content is independent of who's reporting.

Equations

• KirkGiannini2024.gdInterp KirkGiannini2024.GDExpr.goddamnedKeys x✝² x✝¹ x✝ = True

def KirkGiannini2024.gdOriginalCI : ProjWorld → Prop

Original peripheral CI of 'goddamned' in its first use: Jones has a negative attitude toward Jones's keys. Modelled as constant True — attitudes are intentional content of the speaker, not world-contingent. (This is what makes the Potts-vs-K-G refutation bite at .hypothetical: the original CI persists across worlds, but Jones's UTTERANCE is contingent.)

Equations

• KirkGiannini2024.gdOriginalCI x✝ = True

def KirkGiannini2024.gdUttRel : Semantics.Quotation.UttRel GDSpeaker Unit GDExpr ProjWorld

Non-trivial utterance attribution. Jones uttered 'goddamned keys' at .actual; reporter never uttered it. This is what differentiates §1's peripheral content from the constant-True placeholder of the original substrate.

Equations

• KirkGiannini2024.gdUttRel KirkGiannini2024.GDSpeaker.jones x✝ KirkGiannini2024.GDExpr.goddamnedKeys KirkGiannini2024.ProjWorld.actual = True
• KirkGiannini2024.gdUttRel KirkGiannini2024.GDSpeaker.jones x✝ KirkGiannini2024.GDExpr.goddamnedKeys KirkGiannini2024.ProjWorld.hypothetical = False
• KirkGiannini2024.gdUttRel KirkGiannini2024.GDSpeaker.reporter x✝¹ KirkGiannini2024.GDExpr.goddamnedKeys x✝ = False

def KirkGiannini2024.reporterCtx : Semantics.Quotation.MQContext ProjWorld GDExpr GDSpeaker Unit

Reporter's MQ context. Sx is jones (the anaphorically retrieved speaker), wc is the actual world, the reporter is the discourse speaker (not represented in MQContext directly).

Equations

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

@[simp]

theorem KirkGiannini2024.gd_r_layer_attribution : (Semantics.Quotation.MQProp.applyMQ reporterCtx GDExpr.goddamnedKeys).rContent ProjWorld.actual

Peripheral content after 𝔐: utterance attribution to Jones, NOT the original expressive CI.

@[simp]

theorem KirkGiannini2024.gd_at_issue_preserved : (Semantics.Quotation.MQProp.applyMQ reporterCtx GDExpr.goddamnedKeys).atIssue ProjWorld.actual

At-issue content is preserved through 𝔐: Jones-spent-an-hour- looking-for-his-keys remains true.

theorem KirkGiannini2024.gd_reporter_not_attributed : ¬gdUttRel GDSpeaker.reporter () GDExpr.goddamnedKeys ProjWorld.actual

The reporter is not credited with Jones's utterance — gdUttRel correctly distinguishes the actual utterer from the reporter.

theorem KirkGiannini2024.gd_strip_then_remix_loses_original_ci : have original := { atIssue := fun (x : ProjWorld) => True, ci := gdOriginalCI }; original.pureQuoteRich.original.ci = original.ci ∧ (Semantics.Quotation.MQProp.applyMQ reporterCtx GDExpr.goddamnedKeys).rContent ProjWorld.hypothetical ≠ original.ci ProjWorld.hypothetical

The strip-then-remix structure (paper p.21-22). A TwoDimProp carrying the original CI is pure-quoted (stripping the CI per pureQuoteRich), then MQContext.applyMQ re-introduces peripheral content as utterance attribution. The strip witness records what was discarded; the new R-layer holds what replaced it.

theorem KirkGiannini2024.kg_refutes_potts_universal_projection : have original := { atIssue := fun (x : ProjWorld) => True, ci := gdOriginalCI }; have pottsCIAfterNeg := original.neg.ci; have kgRAfterChain := (Semantics.Quotation.MQProp.applyMQ reporterCtx GDExpr.goddamnedKeys).rContent; pottsCIAfterNeg ProjWorld.hypothetical ≠ kgRAfterChain ProjWorld.hypothetical

K-G refutes Potts's universal CI projection. Per @cite{potts-2005} (formalised as Theories.Pragmatics.Expressives.Basic.ci_projects_through_neg): (neg p).ci = p.ci. The CI of a TwoDimProp projects unchanged through any at-issue operator. K-G's analysis predicts that under indirect-speech embedding the CI is REPLACED by utterance attribution.

To exhibit the divergence we apply both analyses to the SAME input proposition original = ⟨True, gdOriginalCI⟩:

• Potts: applying TwoDimProp.neg (or any at-issue operator) preserves the CI, so the predicted CI value at .hypothetical is gdOriginalCI .hypothetical = True (Jones's attitude persists across worlds).
• K-G: applying the strip-then-remix pipeline replaces the CI with R-attribution gdUttRel .jones () .goddamnedKeys, so the predicted R-value at .hypothetical is False (Jones's utterance is contingent on the world — only happened in .actual).

The two analyses disagree at .hypothetical. The proof actually invokes Pragmatics.Expressives.TwoDimProp.neg on the constructed input — not just compares stipulated values.

theorem KirkGiannini2024.kg_refutes_harris_potts_orientation : have hpItem := { ciFor := fun (o : HarrisPotts2009.Orientation GDSpeaker) (w : ProjWorld) => match o with | HarrisPotts2009.Orientation.speaker => True | HarrisPotts2009.Orientation.other p => True, atIssue := fun (x : ProjWorld) => True }; have hpReporterCI := (hpItem.resolve (HarrisPotts2009.Orientation.other GDSpeaker.reporter)).ci; have kgCI := (Semantics.Quotation.MQProp.applyMQ reporterCtx GDExpr.goddamnedKeys).rContent; hpReporterCI ProjWorld.hypothetical ≠ kgCI ProjWorld.hypothetical

K-G refutes Harris-Potts orientation variables. @cite{harris-potts-2009} posit a free orientation variable on each CI item, contextually resolved (formalised as Phenomena.Expressives.Studies.HarrisPotts2009.CIItem with a ciFor : Orientation → W → Prop field). K-G's strip-then-remix analysis predicts the CI is FIXED by the syntactic structure (specifically by sx in the MQ context).

To exhibit the divergence, we construct an H&P CI item whose orientation is contextually resolvable to ANY participant (H&P's permissive prediction), and a K-G chain where the CI is determined by the fixed sx = .jones. The H&P item allows the reporter to be the orientation; K-G excludes this.

theorem KirkGiannini2024.kg_refutes_maier_chameleonism : have maierInput := { cat := Maier2014.Cat.NP, meaning := { atIssue := fun (x : ProjWorld) => True, ci := gdOriginalCI } }; have maierAttrib := fun (x : ProjWorld) => True; have maierCI := (Maier2014.mq maierAttrib maierInput).meaning.ci; have kgCI := (Semantics.Quotation.MQProp.applyMQ reporterCtx GDExpr.goddamnedKeys).rContent; maierCI ProjWorld.hypothetical ≠ kgCI ProjWorld.hypothetical

K-G refutes Maier 2014a's syntactic chameleonism.

Maier (Phenomena.Quotation.Studies.Maier2014) treats the mixed-quotation operator as type-polymorphic: mq attrib e returns a TypedExpr with the SAME category as e, and the daughter's CI content passes through unchanged (theorem mq_ci_passes_daughter_ci_through).

K-G's strip-then-mix pipeline DESTROYS the daughter's CI before remixing — the original gdOriginalCI does not survive into the result's peripheral content; only the new R-attribution does.

We exhibit the divergence by constructing the same input expression in both substrates and showing their CI predictions diverge.

inductive KirkGiannini2024.PlutoWorld : Type

Worlds for the Pluto scenario: pre-2006 conventions classify Pluto as a planet, post-2006 do not.

• pre2006 : PlutoWorld
• post2006 : PlutoWorld

@[implicit_reducible]

instance KirkGiannini2024.instDecidableEqPlutoWorld : DecidableEq PlutoWorld

Equations

• KirkGiannini2024.instDecidableEqPlutoWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KirkGiannini2024.instReprPlutoWorld.repr : PlutoWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KirkGiannini2024.instReprPlutoWorld : Repr PlutoWorld

Equations

• KirkGiannini2024.instReprPlutoWorld = { reprPrec := KirkGiannini2024.instReprPlutoWorld.repr }

@[implicit_reducible]

instance KirkGiannini2024.instInhabitedPlutoWorld : Inhabited PlutoWorld

Equations

• KirkGiannini2024.instInhabitedPlutoWorld = { default := KirkGiannini2024.instInhabitedPlutoWorld.default }

def KirkGiannini2024.instInhabitedPlutoWorld.default : PlutoWorld

Equations

• KirkGiannini2024.instInhabitedPlutoWorld.default = KirkGiannini2024.PlutoWorld.pre2006

inductive KirkGiannini2024.PlutoExpr : Type

The word 'planet' as a quoted expression.

• planet : PlutoExpr

@[implicit_reducible]

instance KirkGiannini2024.instDecidableEqPlutoExpr : DecidableEq PlutoExpr

Equations

• KirkGiannini2024.instDecidableEqPlutoExpr x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance KirkGiannini2024.instReprPlutoExpr : Repr PlutoExpr

Equations

• KirkGiannini2024.instReprPlutoExpr = { reprPrec := KirkGiannini2024.instReprPlutoExpr.repr }

def KirkGiannini2024.instReprPlutoExpr.repr : PlutoExpr → ℕ → Std.Format

Equations

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

inductive KirkGiannini2024.PlutoSpeaker : Type

Two speakers: one using the standard (post-2006) convention, one a hypothetical pre-2006 community. The ∃-over-speakers in K-G's † (paper fn 22) ranges over types like this.

• standard : PlutoSpeaker
• pre2006Community : PlutoSpeaker

@[implicit_reducible]

instance KirkGiannini2024.instDecidableEqPlutoSpeaker : DecidableEq PlutoSpeaker

Equations

• KirkGiannini2024.instDecidableEqPlutoSpeaker x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance KirkGiannini2024.instReprPlutoSpeaker : Repr PlutoSpeaker

Equations

• KirkGiannini2024.instReprPlutoSpeaker = { reprPrec := KirkGiannini2024.instReprPlutoSpeaker.repr }

def KirkGiannini2024.instReprPlutoSpeaker.repr : PlutoSpeaker → ℕ → Std.Format

Equations

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

def KirkGiannini2024.plutoInterp : Semantics.Quotation.QuotInterp PlutoExpr PlutoSpeaker PlutoWorld

Quotative interpretation of 'planet': depends on the speaker's convention. The pre-2006 community classifies Pluto as planet at pre-2006 worlds; the standard speaker does not.

Equations

• KirkGiannini2024.plutoInterp KirkGiannini2024.PlutoExpr.planet KirkGiannini2024.PlutoWorld.pre2006 KirkGiannini2024.PlutoSpeaker.pre2006Community x✝ = True
• KirkGiannini2024.plutoInterp KirkGiannini2024.PlutoExpr.planet KirkGiannini2024.PlutoWorld.post2006 KirkGiannini2024.PlutoSpeaker.pre2006Community x✝ = False
• KirkGiannini2024.plutoInterp KirkGiannini2024.PlutoExpr.planet x✝¹ KirkGiannini2024.PlutoSpeaker.standard x✝ = False

theorem KirkGiannini2024.pluto_counterfactual_via_diagonalizeKG : ∃ (w : PlutoWorld), Semantics.Quotation.diagonalizeKG plutoInterp PlutoExpr.planet w

(4): "Pluto could have easily been a planet" — true via K-G's diagonalizer with ∃-over-speakers (paper fn 22). The diagonalized predicate is non-vacuous: there exists a speaker (the pre-2006 community) whose use of 'planet' includes Pluto at the pre-2006 world. Witness: speaker = .pre2006Community, world = .pre2006.

theorem KirkGiannini2024.pluto_diagonalize_witness_not_universal : ¬∀ (s : PlutoSpeaker), plutoInterp PlutoExpr.planet PlutoWorld.pre2006 s PlutoWorld.pre2006

Witness uniqueness fails. The pre-2006 community and the standard speaker disagree on Pluto's planethood at pre-2006 worlds, so K-G's existential is genuinely informative — not every speaker is a witness.

def KirkGiannini2024.kgEmbeddingShifts {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} : List (Core.Context.ContextShift (Core.Context.KContext W E P T))

K-G's covert lexicon, viewed as Kaplan-context shifts. All four covert operators (𝔐, ↓, †, 𝔄) operate on the world / appropriateness components of evaluation, NOT on the Kaplan context (agent, time, location). Their image on Kaplan-context space is the identity shift.

We exhibit this with one identityShift per covert operator. The list could equivalently be empty; making it explicit lets the no-monster theorem actually CASE-SPLIT on K-G's apparatus rather than vacuously hold over an empty list.

Equations

• KirkGiannini2024.kgEmbeddingShifts = [Core.Context.identityShift, Core.Context.identityShift, Core.Context.identityShift, Core.Context.identityShift]

theorem KirkGiannini2024.diagonalize_no_kaplan_monster {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} : Semantics.Reference.Monsters.KaplansThesisHolds kgEmbeddingShifts

Bridge to Kaplan's no-monster thesis (Theories/Semantics/Reference/ Monsters.lean). K-G's † is a content operator (it shifts the world component of the quotative interpretation), NOT a context operator. K-G's apparatus, projected to Kaplan-context space, contributes only identity shifts (kgEmbeddingShifts), so Kaplan's thesis is preserved.

This is the architectural payoff of K-G's analysis vs. KJR's: K-G explains c-monstrous behavior WITHOUT touching the worlds-as-evaluation-points architecture or introducing context shifts.

theorem KirkGiannini2024.kg_refutes_kjr_convention_shift : have pre2006Convention := { ext := fun (p : PlutoExpr) (x : Unit) (x_1 : PlutoWorld) => match p with | PlutoExpr.planet => True }; have kjrEval := KocurekJerzakRudolph2020.diagContent PlutoExpr.planet () { world := PlutoWorld.post2006, conv := pre2006Convention }; have kgEval := Semantics.Quotation.diagonalizeKG plutoInterp PlutoExpr.planet PlutoWorld.post2006; kjrEval ∧ ¬kgEval

K-G refutes KJR's convention-shift architecture. KJR (Phenomena.Conditionals.Studies.KocurekJerzakRudolph2020) replace worlds with world-convention pairs and treat conditionals as shifting the convention component. K-G's analysis preserves worlds-as-evaluation-points and uses † instead.

We exhibit the SUBSTANTIVE divergence by constructing the same scenario in both substrates and showing they make incompatible predictions:

• KJR: at the WC-pair ⟨.post2006, pre2006Convention⟩, the diagonal content of planet applied to pluto is True (the WC-pair's convention puts Pluto in the extension, regardless of the world component).
• K-G: diagonalizeKG plutoInterp .planet .post2006 is False (no speaker witness — no community whose use of 'planet' at .post2006 includes Pluto, since standard.post2006 = False and pre2006Community.post2006 = False).

The two architectures predict different truth values for the same surface sentence at the same world.

inductive KirkGiannini2024.MNExpr : Type

Expressions in the metalinguistic-negation scenario. Includes lexical pairs needed for the morpheme-incorporation prediction.

• mongeese : MNExpr
• mongooses : MNExpr
• happy : MNExpr
• unhappy : MNExpr
• ecstatic : MNExpr

@[implicit_reducible]

instance KirkGiannini2024.instDecidableEqMNExpr : DecidableEq MNExpr

Equations

• KirkGiannini2024.instDecidableEqMNExpr x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance KirkGiannini2024.instReprMNExpr : Repr MNExpr

Equations

• KirkGiannini2024.instReprMNExpr = { reprPrec := KirkGiannini2024.instReprMNExpr.repr }

def KirkGiannini2024.instReprMNExpr.repr : MNExpr → ℕ → Std.Format

Equations

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

inductive KirkGiannini2024.MNWorld : Type

Two worlds: the actual (where the dispute occurs) and a hypothetical alternative. Multi-constructor so the appropriateness modal ♦ quantifies non-vacuously.

• actual : MNWorld
• hypothetical : MNWorld

@[implicit_reducible]

instance KirkGiannini2024.instDecidableEqMNWorld : DecidableEq MNWorld

Equations

• KirkGiannini2024.instDecidableEqMNWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance KirkGiannini2024.instReprMNWorld : Repr MNWorld

Equations

• KirkGiannini2024.instReprMNWorld = { reprPrec := KirkGiannini2024.instReprMNWorld.repr }

def KirkGiannini2024.instReprMNWorld.repr : MNWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KirkGiannini2024.instInhabitedMNWorld : Inhabited MNWorld

Equations

• KirkGiannini2024.instInhabitedMNWorld = { default := KirkGiannini2024.instInhabitedMNWorld.default }

def KirkGiannini2024.instInhabitedMNWorld.default : MNWorld

Equations

• KirkGiannini2024.instInhabitedMNWorld.default = KirkGiannini2024.MNWorld.actual

inductive KirkGiannini2024.MNSpeaker : Type

Speakers: a generic English speaker and a hypothetical prescriptivist who would judge 'mongeese' appropriate.

• genericEnglish : MNSpeaker
• prescriptivist : MNSpeaker

@[implicit_reducible]

instance KirkGiannini2024.instDecidableEqMNSpeaker : DecidableEq MNSpeaker

Equations

• KirkGiannini2024.instDecidableEqMNSpeaker x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KirkGiannini2024.instReprMNSpeaker.repr : MNSpeaker → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KirkGiannini2024.instReprMNSpeaker : Repr MNSpeaker

Equations

• KirkGiannini2024.instReprMNSpeaker = { reprPrec := KirkGiannini2024.instReprMNSpeaker.repr }

def KirkGiannini2024.mnInterp : Semantics.Quotation.QuotInterp MNExpr MNSpeaker MNWorld

Both 'mongeese' and 'mongooses' pick out the mongoose property — same at-issue content. The lexical-pair pattern for incorporation has 'happy' and 'unhappy' as semantic complements.

Equations

• KirkGiannini2024.mnInterp KirkGiannini2024.MNExpr.mongeese x✝² x✝¹ x✝ = True
• KirkGiannini2024.mnInterp KirkGiannini2024.MNExpr.mongooses x✝² x✝¹ x✝ = True
• KirkGiannini2024.mnInterp KirkGiannini2024.MNExpr.happy x✝² x✝¹ x✝ = True
• KirkGiannini2024.mnInterp KirkGiannini2024.MNExpr.unhappy x✝² x✝¹ x✝ = False
• KirkGiannini2024.mnInterp KirkGiannini2024.MNExpr.ecstatic x✝² x✝¹ x✝ = True

def KirkGiannini2024.mnUttRel : Semantics.Quotation.UttRel MNSpeaker Unit MNExpr MNWorld

Non-trivial utterance attribution. Generic English speaker actually utters 'mongooses'; the prescriptivist would utter 'mongeese'. This non-vacuity is what the original substrate's constant-True uttRel was missing.

Equations

• KirkGiannini2024.mnUttRel KirkGiannini2024.MNSpeaker.genericEnglish x✝ KirkGiannini2024.MNExpr.mongooses KirkGiannini2024.MNWorld.actual = True
• KirkGiannini2024.mnUttRel KirkGiannini2024.MNSpeaker.prescriptivist x✝ KirkGiannini2024.MNExpr.mongeese KirkGiannini2024.MNWorld.actual = True
• KirkGiannini2024.mnUttRel x✝³ x✝² x✝¹ x✝ = False

def KirkGiannini2024.mnApprop : Semantics.Quotation.AppropStandard MNSpeaker MNExpr MNWorld

Appropriateness standard. 'mongooses' is the appropriate plural for English speakers; 'mongeese' is not. Speaker-relative: the prescriptivist's standard would judge 'mongeese' appropriate.

Equations

• KirkGiannini2024.mnApprop KirkGiannini2024.MNSpeaker.genericEnglish KirkGiannini2024.MNExpr.mongooses x✝ = True
• KirkGiannini2024.mnApprop KirkGiannini2024.MNSpeaker.prescriptivist KirkGiannini2024.MNExpr.mongeese x✝ = True
• KirkGiannini2024.mnApprop x✝² x✝¹ x✝ = False

def KirkGiannini2024.mnCtx : Semantics.Quotation.MQContext MNWorld MNExpr MNSpeaker Unit

The metalinguistic negation context — generic English speaker.

Equations

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

theorem KirkGiannini2024.mongeese_metalinguistic_neg : (Semantics.Quotation.shunt (Semantics.Quotation.applyApprop mnApprop mnCtx.sx MNExpr.mongeese (mnCtx.applyMQ MNExpr.mongeese))).neg.atIssue MNWorld.actual

(3): "I didn't manage to trap two MONGEESE" — the metalinguistic negation reading derives via metalinguistic_neg_truth_conditions (substrate, paper §5 p.28-30): the at-issue content is ¬(at-issue ∧ appropriate). Since 'mongeese' is INappropriate for the generic English speaker, the negation holds even though the at-issue (mongoose property) does not.

theorem KirkGiannini2024.mongeese_blocks_morpheme_incorporation (s : MNSpeaker) (w : MNWorld) : mnInterp MNExpr.unhappy w s w ↔ ¬mnInterp MNExpr.happy w s w

Prediction 1 — morpheme incorporation failure (Horn 1989 p.392, @cite{horn-1985}). Morphologically incorporated negation (unhappy) cannot host metalinguistic readings. K-G derives this without lexical ambiguity in not: the metalinguistic chain 𝔐 → 𝔄 → ↓ → ¬ requires syntactically separate not, 𝔄, and ↓ nodes — incorporation into a lexical item collapses these into one head, blocking the chain.

Encoded: unhappy is at-issue-equivalent to ¬'happy', NOT to ¬♦happy (the appropriateness modal cannot factor through the incorporated item).

theorem KirkGiannini2024.mongeese_blocks_npi_licensing (occ : Horn1989.NegScopeOccurrence MNExpr) : occ.neg.kind = Horn1989.NegationKind.metalinguistic → occ.polarity = Horn1989.PolarityItem.npi → ¬occ.licit

Prediction 2 — NPI licensing failure (Horn 1989). Metalinguistic negation does not license NPIs. K-G's account derives this from the appropriateness modal ♦ and the shunting structure: NPIs require descriptive-negation downward-entailing scope, but ♦ is not downward-entailing in the relevant sense.

Lifted from Phenomena.Negation.Studies.Horn1989.

theorem KirkGiannini2024.mongeese_blocks_dn_elimination (chain : Horn1989.NegChain MNExpr) (h : chain.containsMetalinguistic) : ¬chain.dneEliminates

Prediction 3 — DN-elimination failure (@cite{burton-roberts-1989}). "She's not not happy, she's inconsolable" does NOT reduce to "She's happy" — the metalinguistic chain blocks DN-elimination. K-G's account: each ¬ in the metalinguistic chain scopes over a distinct appropriateness conjunction, so successive ¬¬ does not reduce.

Lifted from Horn1989.metalinguistic_neg_blocks_dn_elimination.

theorem KirkGiannini2024.kg_metalinguistic_chain_targets_appropriateness : (Semantics.Quotation.applyApprop mnApprop mnCtx.sx MNExpr.mongeese (mnCtx.applyMQ MNExpr.mongeese)).ci = mnApprop mnCtx.sx MNExpr.mongeese

K-G's metalinguistic negation does NOT match DenialType.implicature.

Phenomena.Negation.Denial (formalising @cite{van-der-sandt-maier-2003}) classifies register/connotation denials as DenialType.implicature, which maps to ContentLayer.implicature. K-G's chain produces content on the appropriateness dimension via applyApprop — which lives in Quotation/Mixed, not in Implicature/. The two substrates are not inter-translatable.

We exhibit the structural divergence by exhibiting a witness metalinguistic-negation example whose at-issue conjunct is True (mongoose property holds) AND whose appropriateness conjunct is False (mongeese is inappropriate). This is the K-G profile, NOT the implicature-denial profile (which would target a scalar enrichment, not an appropriateness modal).

theorem KirkGiannini2024.mongeese_R_survives_metalinguistic_neg : (Semantics.Quotation.MQProp.applyApprop mnApprop mnCtx.sx MNExpr.mongeese (Semantics.Quotation.MQProp.applyMQ mnCtx MNExpr.mongeese)).shunt.neg.rContent = mnUttRel mnCtx.sx mnCtx.ux MNExpr.mongeese

R-content survives the full metalinguistic negation chain — in the MQProp layered model. This is the load-bearing architectural payoff of the substrate's two-layer refactor (MQProp vs flat TwoDimProp).

In the flat model, applyApprop REPLACES the ci dimension with the appropriateness content, so the original R-attribution (mnUttRel mnCtx.sx mnCtx.ux .mongeese) is destroyed when 𝔄 fires. In the MQProp model, R lives in a separate layer; 𝔄 writes only to the ◆-layer. After the full chain 𝔐 → 𝔄 → ↓ → ¬, R is intact.

This is the prediction K-G needs (paper §5): "I didn't trap two MONGEESE" still records that someone uttered 'mongeese'. The flat model loses this; MQProp keeps it. Concrete witness for the mongeese scenario, derived from substrate's full_chain_preserves_rContent.

theorem KirkGiannini2024.mongeese_R_value_at_actual : ¬(Semantics.Quotation.MQProp.applyApprop mnApprop mnCtx.sx MNExpr.mongeese (Semantics.Quotation.MQProp.applyMQ mnCtx MNExpr.mongeese)).shunt.neg.rContent MNWorld.actual

R-content is non-trivial for the mongeese scenario. Concretely at .actual, the R-layer records that the generic English speaker did NOT utter 'mongeese' (mnUttRel .genericEnglish () .mongeese .actual = False) — the speaker uttered 'mongooses' instead. This information is preserved through the metalinguistic-negation chain in the layered model. The flat-model mongeese_metalinguistic_neg cannot witness this distinction.

inductive KirkGiannini2024.AthExpr : Type

The word 'athlete' in the Secretariat dispute.

• athlete : AthExpr

@[implicit_reducible]

instance KirkGiannini2024.instDecidableEqAthExpr : DecidableEq AthExpr

Equations

• KirkGiannini2024.instDecidableEqAthExpr x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance KirkGiannini2024.instReprAthExpr : Repr AthExpr

Equations

• KirkGiannini2024.instReprAthExpr = { reprPrec := KirkGiannini2024.instReprAthExpr.repr }

def KirkGiannini2024.instReprAthExpr.repr : AthExpr → ℕ → Std.Format

Equations

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

inductive KirkGiannini2024.AthWorld : Type

Worlds: the actual world (broad athleticism is the relevant property) and a hypothetical comparison world.

• actual : AthWorld
• hypothetical : AthWorld

@[implicit_reducible]

instance KirkGiannini2024.instDecidableEqAthWorld : DecidableEq AthWorld

Equations

• KirkGiannini2024.instDecidableEqAthWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KirkGiannini2024.instReprAthWorld.repr : AthWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KirkGiannini2024.instReprAthWorld : Repr AthWorld

Equations

• KirkGiannini2024.instReprAthWorld = { reprPrec := KirkGiannini2024.instReprAthWorld.repr }

@[implicit_reducible]

instance KirkGiannini2024.instInhabitedAthWorld : Inhabited AthWorld

Equations

• KirkGiannini2024.instInhabitedAthWorld = { default := KirkGiannini2024.instInhabitedAthWorld.default }

def KirkGiannini2024.instInhabitedAthWorld.default : AthWorld

Equations

• KirkGiannini2024.instInhabitedAthWorld.default = KirkGiannini2024.AthWorld.actual

inductive KirkGiannini2024.AthSpeaker : Type

Two disputants A and B (who AGREE Secretariat has the relevant physical properties but DISAGREE on whether 'athlete' is appropriate to use for non-human animals).

• speakerA : AthSpeaker
• speakerB : AthSpeaker

@[implicit_reducible]

instance KirkGiannini2024.instDecidableEqAthSpeaker : DecidableEq AthSpeaker

Equations

• KirkGiannini2024.instDecidableEqAthSpeaker x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance KirkGiannini2024.instReprAthSpeaker : Repr AthSpeaker

Equations

• KirkGiannini2024.instReprAthSpeaker = { reprPrec := KirkGiannini2024.instReprAthSpeaker.repr }

def KirkGiannini2024.instReprAthSpeaker.repr : AthSpeaker → ℕ → Std.Format

Equations

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

def KirkGiannini2024.athInterp : Semantics.Quotation.QuotInterp AthExpr AthSpeaker AthWorld

The shared at-issue content: Secretariat instantiates broad athleticism. Both A and B agree on this.

Equations

• KirkGiannini2024.athInterp KirkGiannini2024.AthExpr.athlete x✝² x✝¹ x✝ = True

def KirkGiannini2024.athShared : Semantics.Quotation.AppropStandard AthSpeaker AthExpr AthWorld

The SHARED appropriateness standard. Per K-G §6, the dispute is NOT over which idiolectal extension is "correct" (P&S's diagnosis) — both A and B are using a single standard, and the dispute is about what that standard's verdict on 'athlete-for-horses' should be. We encode this as ONE AppropStandard whose value at the dispute expression is the contested proposition.

Equations

• KirkGiannini2024.athShared x✝¹ KirkGiannini2024.AthExpr.athlete x✝ = True

def KirkGiannini2024.athCtxA : Semantics.Quotation.MQContext AthWorld AthExpr AthSpeaker Unit

A's MQ context — committing to "appropriate(athlete, Secretariat)".

Equations

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

theorem KirkGiannini2024.speakerA_assertion : (Semantics.Quotation.shunt (Semantics.Quotation.applyApprop athShared athCtxA.sx AthExpr.athlete (athCtxA.applyMQ AthExpr.athlete))).atIssue AthWorld.actual

A's assertion (paper (6) A: "Secretariat is an athlete") — the shunted appropriateness chain holds at .actual under the shared standard.

theorem KirkGiannini2024.speakerB_denial_under_shared_standard (rejectedApprop : Semantics.Quotation.AppropStandard AthSpeaker AthExpr AthWorld) (h_neg : ¬rejectedApprop AthSpeaker.speakerA AthExpr.athlete AthWorld.actual) : (Semantics.Quotation.shunt (Semantics.Quotation.applyApprop rejectedApprop athCtxA.sx AthExpr.athlete (athCtxA.applyMQ AthExpr.athlete))).neg.atIssue AthWorld.actual

B's denial (paper (6) B: "No, Secretariat is not an athlete") — metalinguistic negation of the SAME shared content. B asserts the negation of the appropriateness conjunct. The crucial point (vs. P&S) is that A and B's assertions are LITERALLY INCOMPATIBLE on the same standard, NOT consistent on different idiolects.

theorem KirkGiannini2024.kg_refutes_plunkett_sundell (d : PlunkettSundell2013.MetalinguisticDispute Unit AthWorld) : d.predA = d.predB → ¬d.consistentContents

K-G refutes Plunkett-Sundell — structural cross-framework theorem.

K-G and P&S make incompatible commitments about the structure of a metalinguistic dispute:

• P&S (Phenomena.Negation.Studies.PlunkettSundell2013): consistentContents requires predA ≠ predB extensionally — speakers use DIFFERENT idiolectal extensions of the contested predicate, and joint satisfiability witnesses their distinct meanings. Paper p.18: "the connection between genuine disagreement and sameness of meaning is broken."

• K-G (paper §6, p.33-34): A and B operate on a SHARED standard; the dispute is over the SAME proposition's truth value. Encoded in P&S's MetalinguisticDispute schema, K-G's commitment is predA = predB.

The substrate lemma MetalinguisticDispute.consistentContents_excludes_shared_standard proves these commitments are jointly unsatisfiable: any dispute with predA = predB necessarily violates consistentContents. The K-G refutation is the schematic claim that K-G's commitment entails P&S's predicate failure — universally over disputes, with no hand-picked extensions.

inductive KirkGiannini2024.VirExpr : Type

Expressions for the "viruses are alive" scenario.

• alive : VirExpr

@[implicit_reducible]

instance KirkGiannini2024.instDecidableEqVirExpr : DecidableEq VirExpr

Equations

• KirkGiannini2024.instDecidableEqVirExpr x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KirkGiannini2024.instReprVirExpr.repr : VirExpr → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KirkGiannini2024.instReprVirExpr : Repr VirExpr

Equations

• KirkGiannini2024.instReprVirExpr = { reprPrec := KirkGiannini2024.instReprVirExpr.repr }

inductive KirkGiannini2024.VirSpeaker : Type

Two speakers with different intensions for 'alive':

• biologist: 'alive' includes viruses (genetic-material criterion)
• layperson: 'alive' excludes viruses (5-kingdoms criterion)

• biologist : VirSpeaker
• layperson : VirSpeaker

@[implicit_reducible]

instance KirkGiannini2024.instDecidableEqVirSpeaker : DecidableEq VirSpeaker

Equations

• KirkGiannini2024.instDecidableEqVirSpeaker x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KirkGiannini2024.instReprVirSpeaker.repr : VirSpeaker → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KirkGiannini2024.instReprVirSpeaker : Repr VirSpeaker

Equations

• KirkGiannini2024.instReprVirSpeaker = { reprPrec := KirkGiannini2024.instReprVirSpeaker.repr }

inductive KirkGiannini2024.VirWorld : Type

Worlds for the "in a sense" scenario. Multi-constructor so the intension quantification is non-vacuous.

• actual : VirWorld
• counterfactual : VirWorld

@[implicit_reducible]

instance KirkGiannini2024.instDecidableEqVirWorld : DecidableEq VirWorld

Equations

• KirkGiannini2024.instDecidableEqVirWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KirkGiannini2024.instReprVirWorld.repr : VirWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KirkGiannini2024.instReprVirWorld : Repr VirWorld

Equations

• KirkGiannini2024.instReprVirWorld = { reprPrec := KirkGiannini2024.instReprVirWorld.repr }

@[implicit_reducible]

instance KirkGiannini2024.instInhabitedVirWorld : Inhabited VirWorld

Equations

• KirkGiannini2024.instInhabitedVirWorld = { default := KirkGiannini2024.instInhabitedVirWorld.default }

def KirkGiannini2024.instInhabitedVirWorld.default : VirWorld

Equations

• KirkGiannini2024.instInhabitedVirWorld.default = KirkGiannini2024.VirWorld.actual

def KirkGiannini2024.virInterp : Semantics.Quotation.QuotInterp VirExpr VirSpeaker VirWorld

Quotative interpretation: 'alive' has different extensions depending on which speaker is using the word.

Equations

• KirkGiannini2024.virInterp KirkGiannini2024.VirExpr.alive x✝¹ KirkGiannini2024.VirSpeaker.biologist x✝ = True
• KirkGiannini2024.virInterp KirkGiannini2024.VirExpr.alive x✝¹ KirkGiannini2024.VirSpeaker.layperson x✝ = False

@[reducible, inline]

abbrev KirkGiannini2024.VirIntension : Type

Intensions — propositions about VirWorlds. K-G's analysis quantifies over intensions μ in addition to speakers sₓ. Here we use the type of VirWorld → Prop directly.

Equations

• KirkGiannini2024.VirIntension = (KirkGiannini2024.VirWorld → Prop)

def KirkGiannini2024.virMQCtx (s : VirSpeaker) : Semantics.Quotation.MQContext VirWorld VirExpr VirSpeaker Unit

The MQ context parameterised by speaker.

Equations

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

def KirkGiannini2024.whichMu (P : VirIntension → VirWorld → Prop) (w : VirWorld) : Prop

Predicate Abstraction over the intension variable (paper p.37-38). K-G's which_μ binds μ via Heim & Kratzer-style PA. Encoded here as a function abstracting over intensions.

Equations

• KirkGiannini2024.whichMu P w = ∃ (μ : KirkGiannini2024.VirIntension), P μ w

theorem KirkGiannini2024.viruses_alive_in_a_sense : whichMu (fun (μ : VirIntension) (w : VirWorld) => ∃ (s : VirSpeaker), ((virMQCtx s).applyMQ VirExpr.alive).atIssue w ∧ μ = ((virMQCtx s).applyMQ VirExpr.alive).atIssue) VirWorld.actual

(7'): "There is a sense which viruses are alive in" — the K-G analysis (paper p.38) gives the L_MQ formula:

∃μ ∃sₓ [⟨⟩(viruses are alive)(wc)(sₓ) ∧ [^⟨⟩(viruses are alive)(wc)(sₓ)] = μ]

The existential ranges over BOTH intensions μ AND speakers sₓ. Both are needed: speakers select different intensions for the same expression, and which_μ binds μ for the relative clause.

Witness: at .actual, with sₓ = biologist (whose use of 'alive' includes viruses) and μ = the biologist's predicate.

theorem KirkGiannini2024.not_alive_layperson : ¬((virMQCtx VirSpeaker.layperson).applyMQ VirExpr.alive).atIssue VirWorld.actual

The layperson is NOT a witness: their use of 'alive' excludes viruses.

theorem KirkGiannini2024.not_all_senses : ¬∀ (s : VirSpeaker), ((virMQCtx s).applyMQ VirExpr.alive).atIssue VirWorld.actual

The existential is non-trivial: not all senses make viruses alive.

theorem KirkGiannini2024.in_a_sense_distinct_from_imprecision : ((virMQCtx VirSpeaker.biologist).applyMQ VirExpr.alive).atIssue VirWorld.actual ≠ ((virMQCtx VirSpeaker.layperson).applyMQ VirExpr.alive).atIssue VirWorld.actual

K-G's "in a sense" is distinct from imprecision/granularity accounts. Imprecision frameworks (e.g. Phenomena.Imprecision.Studies.Haslinger2025) locate the variation in TOLERANCE / GRANULARITY parameters of a single speaker. K-G's "in a sense" locates the variation in the SPEAKER VARIABLE of 𝔐 — different speakers contribute different intensions.

The two analyses make incompatible architectural commitments. Imprecision holds the speaker fixed and varies the granularity; K-G holds granularity fixed and varies the speaker.

We exhibit the divergence: K-G's analysis predicts variation at the speaker locus (biologist vs. layperson), where Imprecision predicts no variation (single speaker, single granularity).