Ginzburg & Cooper (2004): Clarification, Ellipsis, and Contextual Updates

[GC04]

Formalization of the core running example from [GC04]:

A: "Did Bo leave?" B: "Bo?"

This study applies the KOS framework (DGB, IS, C-PARAMS, coercion operations) to derive both CE readings — clausal and constituent — from the same antecedent sign, and demonstrates the speaker/addressee IS asymmetry.

Key Claims Formalized

1. Proper names introduce C-PARAMS (referent binding) — ex. 28
2. The running example has 5 C-PARAMS — ex. 32
3. Parameter focussing yields clausal CE reading — ex. 53/54
4. Parameter identification yields constituent CE reading — ex. 59/60
5. Both coercions take the antecedent sign and target the same SAL-UTT
6. Existential generalization removes a parameter without clarification — ex. 77/78
7. Speaker resolves all params; addressee may not — ex. 82
8. Partial assignment triggers PENDING, not grounding
9. Updates require structured representations (Hybrid Content Hypothesis) — ex. 2/16

inductive GinzburgCooper2004.CEReading : Type

The two readings of a clarification ellipsis. [GC04] ex. 4b–c.

• clausal : CEReading

  "Are you asking whether p?" — polar question about propositional content. Paraphrasable as a polar interrogative. Presupposes shared belief about the sub-utterance's content.

• constituent : CEReading

  "Who/what do you mean by X?" — wh-question about the referent/predicate. Paraphrasable as a wh-interrogative. No shared-belief presupposition.

def GinzburgCooper2004.instReprCEReading.repr : CEReading → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance GinzburgCooper2004.instReprCEReading : Repr CEReading

Equations

• GinzburgCooper2004.instReprCEReading = { reprPrec := GinzburgCooper2004.instReprCEReading.repr }

@[implicit_reducible]

instance GinzburgCooper2004.instDecidableEqCEReading : DecidableEq CEReading

Equations

• GinzburgCooper2004.instDecidableEqCEReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

1994/2004 Clarification Ellipsis Apparatus

This section was previously in Discourse/Gameboard/Basic.lean §§6, 7, 8, 9, 10, 12, 15. It is paper-specific to [GC04]: in [Gin12], the corresponding machinery uses dgb-params (record types built on the shared CParam) rather than CtxtAssignment, and CCURs (Clarification Context Update Rules) rather than the three coercion operations (parameterFocussing, parameterIdentification, existentialGeneralization).

We preserve the 2004 formulation here because this study replicates the 2004 paper directly — the apparatus is single-consumer paper-specific content, demoted from substrate to consumer per the linglib pattern (cf. Core/FormFrequency.lean → Studies/Haspelmath2021.lean §0).

The shared substrate primitives — CParam, CParamSet, SubUtterance — remain in Gameboard/Defs.lean since they survive into the 2012 framework as the dgb-params/sub-constituents apparatus.

The four general theorems about coercion operations are namespaced under Apparatus to avoid colliding with this file's specific-instance theorems on the running example.

structure GinzburgCooper2004.Apparatus.CtxtAssignment : Type

A contextual assignment maps parameter indices to values.

Grounding requires a total assignment (all C-PARAMS resolved). Clarification arises when the assignment is partial. [GC04] §6, ex. 81–82.

• bindings : List (String × String)

@[implicit_reducible]

instance GinzburgCooper2004.Apparatus.instReprCtxtAssignment : Repr CtxtAssignment

Equations

• GinzburgCooper2004.Apparatus.instReprCtxtAssignment = { reprPrec := GinzburgCooper2004.Apparatus.instReprCtxtAssignment.repr }

def GinzburgCooper2004.Apparatus.instReprCtxtAssignment.repr : CtxtAssignment → ℕ → Std.Format

Equations

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

def GinzburgCooper2004.Apparatus.instDecidableEqCtxtAssignment.decEq (x✝ x✝¹ : CtxtAssignment) : Decidable (x✝ = x✝¹)

Equations

• GinzburgCooper2004.Apparatus.instDecidableEqCtxtAssignment.decEq { bindings := a } { bindings := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance GinzburgCooper2004.Apparatus.instDecidableEqCtxtAssignment : DecidableEq CtxtAssignment

Equations

• GinzburgCooper2004.Apparatus.instDecidableEqCtxtAssignment = GinzburgCooper2004.Apparatus.instDecidableEqCtxtAssignment.decEq

def GinzburgCooper2004.Apparatus.CtxtAssignment.resolves (f : CtxtAssignment) (cp : Discourse.Gameboard.CParam) : Bool

Does the assignment resolve a given parameter?

Equations

• f.resolves cp = f.bindings.any fun (x : String × String) => x.1 == cp.index

def GinzburgCooper2004.Apparatus.CtxtAssignment.resolvesAll (f : CtxtAssignment) (ps : Discourse.Gameboard.CParamSet) : Bool

Does the assignment resolve all parameters in a set?

Equations

• f.resolvesAll ps = List.all ps f.resolves

def GinzburgCooper2004.Apparatus.CtxtAssignment.unresolved (f : CtxtAssignment) (ps : Discourse.Gameboard.CParamSet) : Discourse.Gameboard.CParamSet

Which parameters remain unresolved?

Equations

• f.unresolved ps = List.filter (fun (x : Discourse.Gameboard.CParam) => !f.resolves x) ps

structure GinzburgCooper2004.Apparatus.UttSkeleton : Type

An utterance skeleton: a sign with C-PARAMS and CONSTITS.

The CONSTITS feature (ex. 30) provides access to all sub-utterances. C-PARAMS (ex. 28–29) are the contextual dependencies introduced by the sign, amalgamated from daughters via the Non-local Amalgamation Constraint. [GC04] §3.

• phon : String
• cat : String
• cont : String
• cparams : Discourse.Gameboard.CParamSet
• constits : List Discourse.Gameboard.SubUtterance

def GinzburgCooper2004.Apparatus.instReprUttSkeleton.repr : UttSkeleton → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance GinzburgCooper2004.Apparatus.instReprUttSkeleton : Repr UttSkeleton

Equations

• GinzburgCooper2004.Apparatus.instReprUttSkeleton = { reprPrec := GinzburgCooper2004.Apparatus.instReprUttSkeleton.repr }

@[implicit_reducible]

instance GinzburgCooper2004.Apparatus.instDecidableEqUttSkeleton : DecidableEq UttSkeleton

Equations

• GinzburgCooper2004.Apparatus.instDecidableEqUttSkeleton = GinzburgCooper2004.Apparatus.instDecidableEqUttSkeleton.decEq

def GinzburgCooper2004.Apparatus.instDecidableEqUttSkeleton.decEq (x✝ x✝¹ : UttSkeleton) : Decidable (x✝ = x✝¹)

Equations

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

def GinzburgCooper2004.Apparatus.UttSkeleton.constitForParam (u : UttSkeleton) (paramIdx : String) : Option Discourse.Gameboard.SubUtterance

Find the constituent whose CONT matches a parameter index.

Equations

• u.constitForParam paramIdx = List.find? (fun (x : Discourse.Gameboard.SubUtterance) => x.cont == paramIdx) u.constits

structure GinzburgCooper2004.Apparatus.SignAssignment : Type

A sign paired with a contextual assignment.

[GC04] ex. 81 p.353. The assignment f records which C-PARAMS have been resolved. Grounding checks whether f is total.

• sign : UttSkeleton
• assignment : CtxtAssignment

@[implicit_reducible]

instance GinzburgCooper2004.Apparatus.instReprSignAssignment : Repr SignAssignment

Equations

• GinzburgCooper2004.Apparatus.instReprSignAssignment = { reprPrec := GinzburgCooper2004.Apparatus.instReprSignAssignment.repr }

def GinzburgCooper2004.Apparatus.instReprSignAssignment.repr : SignAssignment → ℕ → Std.Format

Equations

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

def GinzburgCooper2004.Apparatus.instDecidableEqSignAssignment.decEq (x✝ x✝¹ : SignAssignment) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance GinzburgCooper2004.Apparatus.instDecidableEqSignAssignment : DecidableEq SignAssignment

Equations

• GinzburgCooper2004.Apparatus.instDecidableEqSignAssignment = GinzburgCooper2004.Apparatus.instDecidableEqSignAssignment.decEq

structure GinzburgCooper2004.Apparatus.CEState (QContent : Type) : Type

Clarification Ellipsis processing state.

[GC04]: MAX-QUD and SAL-UTT are processing state for the CE analysis. These are NOT part of the [Gin12] DGB or TIS (in 2012, MaxQUD is computed from the QUD poset's maximal element, not stored separately).

This state can be used alongside the 2012 TIS when CE processing is needed.

• maxQud : Option QContent

  The currently maximal question — for CE coercion operations

• salUtt : Option Discourse.Gameboard.SubUtterance

  The salient sub-utterance — target of clarification

• pendingUtts : List SignAssignment

  Pending utterances awaiting C-PARAMS resolution

inductive GinzburgCooper2004.Apparatus.CoercionOp : Type

The three coercion operations on signs with unresolved C-PARAMS. [GC04] §5.

• paramFocussing : CoercionOp

  Clausal CE reading: polar question about content (ex. 53)

• paramIdentification : CoercionOp

  Constituent CE reading: wh-question about speaker meaning (ex. 59)

• existentialGeneralization : CoercionOp

  Ground without clarification: ∃-quantify a parameter (ex. 77)

@[implicit_reducible]

instance GinzburgCooper2004.Apparatus.instReprCoercionOp : Repr CoercionOp

Equations

• GinzburgCooper2004.Apparatus.instReprCoercionOp = { reprPrec := GinzburgCooper2004.Apparatus.instReprCoercionOp.repr }

def GinzburgCooper2004.Apparatus.instReprCoercionOp.repr : CoercionOp → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance GinzburgCooper2004.Apparatus.instDecidableEqCoercionOp : DecidableEq CoercionOp

Equations

• GinzburgCooper2004.Apparatus.instDecidableEqCoercionOp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure GinzburgCooper2004.Apparatus.CoercionOutput : Type

Output of a coercion operation: partial specification for the clarification context.

• op : CoercionOp
• salUtt : Discourse.Gameboard.SubUtterance

  SAL-UTT: the sub-utterance to be echoed

• maxQud : String

  MAX-QUD: the question raised (string representation)

@[implicit_reducible]

instance GinzburgCooper2004.Apparatus.instReprCoercionOutput : Repr CoercionOutput

Equations

• GinzburgCooper2004.Apparatus.instReprCoercionOutput = { reprPrec := GinzburgCooper2004.Apparatus.instReprCoercionOutput.repr }

def GinzburgCooper2004.Apparatus.instReprCoercionOutput.repr : CoercionOutput → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance GinzburgCooper2004.Apparatus.instDecidableEqCoercionOutput : DecidableEq CoercionOutput

Equations

• GinzburgCooper2004.Apparatus.instDecidableEqCoercionOutput = GinzburgCooper2004.Apparatus.instDecidableEqCoercionOutput.decEq

def GinzburgCooper2004.Apparatus.instDecidableEqCoercionOutput.decEq (x✝ x✝¹ : CoercionOutput) : Decidable (x✝ = x✝¹)

Equations

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

def GinzburgCooper2004.Apparatus.parameterFocussing (antecedent : UttSkeleton) (paramIdx : String) : Option CoercionOutput

Parameter focussing ([GC04] ex. 53): derive clausal CE reading.

Takes the antecedent sign and a problematic parameter index. Finds the constituent that introduced the parameter. Produces MAX-QUD = polar question about the antecedent content.

Equations

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

def GinzburgCooper2004.Apparatus.parameterIdentification (antecedent : UttSkeleton) (paramIdx : String) : Option CoercionOutput

Parameter identification ([GC04] ex. 59): derive constituent CE reading.

Produces MAX-QUD = wh-question about speaker meaning.

Equations

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

def GinzburgCooper2004.Apparatus.existentialGeneralization (sk : UttSkeleton) (paramIdx : String) : UttSkeleton

Contextual existential generalization ([GC04] ex. 77): ground without clarifying.

Removes a parameter from C-PARAMS by existentially quantifying it.

Equations

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

structure GinzburgCooper2004.Apparatus.IS (Fact QContent : Type) : Type

Information State for the [GC04] model.

Bundles a DGB with CE processing state (pending utterances). Uses String for both Fact and QContent, matching the string-based representations in the 2004 paper. The Participant type parameter is set to String, and the LocProp Cont is set to String since this is a 2004-era model.

This is NOT the [Gin12] TIS — it predates the genre/agenda private state. It exists to support the CE running example.

• dgb : Discourse.Gameboard.DGB String Fact QContent String
• pending : List SignAssignment

  Utterances awaiting full C-PARAMS resolution

• ce : CEState QContent

def GinzburgCooper2004.Apparatus.IS.initial {Fact QContent : Type} : IS Fact QContent

An empty IS.

Equations

• GinzburgCooper2004.Apparatus.IS.initial = { }

def GinzburgCooper2004.Apparatus.IS.integrateUtterance {Fact QContent : Type} [BEq Fact] (is_ : IS Fact QContent) (skel : UttSkeleton) (assign : CtxtAssignment) (toFact : String → Fact) : IS Fact QContent

Integrate an utterance into the IS.

If the assignment fully resolves all C-PARAMS, the utterance is grounded: its content goes to FACTS. Otherwise, it goes to PENDING. [GC04] §6, ex. 82.

Equations

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

def GinzburgCooper2004.Apparatus.IS.integrateUtteranceStr (is_ : IS String String) (skel : UttSkeleton) (assign : CtxtAssignment) : IS String String

String-specialized integration (content IS the fact).

Equations

• is_.integrateUtteranceStr skel assign = is_.integrateUtterance skel assign id

def GinzburgCooper2004.Apparatus.IS.applyCoercion {Fact QContent : Type} (is_ : IS Fact QContent) (co : CoercionOutput) (toQ : String → QContent) : IS Fact QContent

Apply a coercion output to the IS: set MAX-QUD and SAL-UTT.

Equations

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

def GinzburgCooper2004.Apparatus.IS.applyCoercionStr (is_ : IS String String) (co : CoercionOutput) : IS String String

String-specialized coercion application.

Equations

• is_.applyCoercionStr co = is_.applyCoercion co id

def GinzburgCooper2004.Apparatus.UttSkeleton.toLocProp (sk : UttSkeleton) : Discourse.Gameboard.LocProp String

Convert an UttSkeleton to a string-content LocProp. Subsumes the 2004 skeleton representation in the 2012 LocProp framework.

Equations

• sk.toLocProp = { phon := sk.phon, cat := sk.cat, cont := sk.cont, cparams := sk.cparams, constits := sk.constits }

def GinzburgCooper2004.Apparatus.locPropToSkeleton (lp : Discourse.Gameboard.LocProp String) : UttSkeleton

Convert a LocProp String back to an UttSkeleton. Plain function (not LocProp.toSkeleton) because LocProp lives in Discourse.Gameboard and dot notation looks there for the method, not in Apparatus. Use as locPropToSkeleton lp.

Equations

• GinzburgCooper2004.Apparatus.locPropToSkeleton lp = { phon := lp.phon, cat := lp.cat, cont := lp.cont, cparams := lp.cparams, constits := lp.constits }

theorem GinzburgCooper2004.Apparatus.skeleton_locprop_roundtrip (sk : UttSkeleton) : locPropToSkeleton sk.toLocProp = sk

Round-trip: UttSkeleton → LocProp → UttSkeleton is identity.

theorem GinzburgCooper2004.Apparatus.coercions_same_salUtt (ant : UttSkeleton) (idx : String) : Option.map CoercionOutput.salUtt (parameterFocussing ant idx) = Option.map CoercionOutput.salUtt (parameterIdentification ant idx)

Both coercion operations target the same SAL-UTT.

theorem GinzburgCooper2004.Apparatus.coercions_different_op (ant : UttSkeleton) (idx : String) (r1 r2 : CoercionOutput) (h1 : parameterFocussing ant idx = some r1) (h2 : parameterIdentification ant idx = some r2) : r1.op ≠ r2.op

The two coercion operations produce different operation types.

theorem GinzburgCooper2004.Apparatus.resolved_means_no_unresolved (f : CtxtAssignment) (ps : Discourse.Gameboard.CParamSet) (h : f.resolvesAll ps = true) : f.unresolved ps = []

A fully resolved assignment leaves no unresolved parameters.

theorem GinzburgCooper2004.Apparatus.existential_gen_weakens (sk : UttSkeleton) (idx : String) : List.length (existentialGeneralization sk idx).cparams ≤ List.length sk.cparams

Existential generalization never increases the parameter count.

def GinzburgCooper2004.cpBo : Discourse.Gameboard.CParam

C-PARAM for "Bo": binds variable b to the referent named "Bo". [GC04] ex. 28.

Equations

• GinzburgCooper2004.cpBo = { index := "b", restriction := "named(Bo)(b)" }

def GinzburgCooper2004.cpTime : Discourse.Gameboard.CParam

C-PARAM for temporal precedence.

Equations

• GinzburgCooper2004.cpTime = { index := "t", restriction := "precedes(t,k)" }

def GinzburgCooper2004.cpSpkr : Discourse.Gameboard.CParam

C-PARAM for speaker.

Equations

• GinzburgCooper2004.cpSpkr = { index := "i", restriction := "spkr(i)" }

def GinzburgCooper2004.cpAddr : Discourse.Gameboard.CParam

C-PARAM for addressee.

Equations

• GinzburgCooper2004.cpAddr = { index := "j", restriction := "addr(j)" }

def GinzburgCooper2004.cpUttTime : Discourse.Gameboard.CParam

C-PARAM for utterance time.

Equations

• GinzburgCooper2004.cpUttTime = { index := "k", restriction := "utt-time(k)" }

def GinzburgCooper2004.didBoLeaveCParams : Discourse.Gameboard.CParamSet

The full C-PARAMS set for "Did Bo leave?" — 5 parameters. [GC04] ex. 32.

Equations

• GinzburgCooper2004.didBoLeaveCParams = [GinzburgCooper2004.cpBo, GinzburgCooper2004.cpTime, GinzburgCooper2004.cpSpkr, GinzburgCooper2004.cpAddr, GinzburgCooper2004.cpUttTime]

def GinzburgCooper2004.suDid : Discourse.Gameboard.SubUtterance

Equations

• GinzburgCooper2004.suDid = { phon := "Did", cat := "AUX", cont := "ask" }

def GinzburgCooper2004.suBo : Discourse.Gameboard.SubUtterance

Equations

• GinzburgCooper2004.suBo = { phon := "Bo", cat := "NP", cont := "b" }

def GinzburgCooper2004.suLeave : Discourse.Gameboard.SubUtterance

Equations

• GinzburgCooper2004.suLeave = { phon := "leave", cat := "V", cont := "leave-rel" }

def GinzburgCooper2004.suDidBoLeave : Discourse.Gameboard.SubUtterance

Equations

• GinzburgCooper2004.suDidBoLeave = { phon := "Did Bo leave", cat := "S", cont := "ask(i,j,?.leave-rel(b,t))" }

def GinzburgCooper2004.didBoLeave : Apparatus.UttSkeleton

Full utterance skeleton for "Did Bo leave?" with all 5 C-PARAMS. [GC04] ex. 32.

Equations

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

def GinzburgCooper2004.speakerAssignment : Apparatus.CtxtAssignment

Speaker (A) resolves all parameters: she knows who Bo is, who she is, who the addressee is, and the temporal parameters. [GC04] ex. 82b.

Equations

• GinzburgCooper2004.speakerAssignment = { bindings := [("b", "B"), ("t", "T0"), ("i", "A"), ("j", "B"), ("k", "T1")] }

def GinzburgCooper2004.addresseeAssignment : Apparatus.CtxtAssignment

Addressee (B) resolves all parameters EXCEPT b (Bo's referent). B doesn't know who "Bo" refers to. [GC04] ex. 82c.

Equations

• GinzburgCooper2004.addresseeAssignment = { bindings := [("t", "T0"), ("i", "A"), ("j", "B"), ("k", "T1")] }

def GinzburgCooper2004.speakerIS : Apparatus.IS String String

A's IS after uttering "Did Bo leave?": fully grounded. Speaker resolves all C-PARAMS, so the utterance goes straight to FACTS.

Equations

• GinzburgCooper2004.speakerIS = GinzburgCooper2004.Apparatus.IS.initial.integrateUtteranceStr GinzburgCooper2004.didBoLeave GinzburgCooper2004.speakerAssignment

def GinzburgCooper2004.addresseeIS : Apparatus.IS String String

B's IS after hearing "Did Bo leave?": partial assignment → pending. Addressee cannot resolve b, so the utterance goes to PENDING.

Equations

• GinzburgCooper2004.addresseeIS = GinzburgCooper2004.Apparatus.IS.initial.integrateUtteranceStr GinzburgCooper2004.didBoLeave GinzburgCooper2004.addresseeAssignment

def GinzburgCooper2004.focussingOnBo : Option Apparatus.CoercionOutput

Parameter focussing on "Bo" (parameter b): clausal CE reading. [GC04] ex. 53–54. Output: SAL-UTT = "Bo" constituent, MAX-QUD = ?b.ask(i,j,?.leave-rel(b,t)) Paraphrase: "Are you asking if b left?"

Equations

• GinzburgCooper2004.focussingOnBo = GinzburgCooper2004.Apparatus.parameterFocussing GinzburgCooper2004.didBoLeave "b"

def GinzburgCooper2004.identificationOnBo : Option Apparatus.CoercionOutput

Parameter identification on "Bo" (parameter b): constituent CE reading. [GC04] ex. 59–60. Output: SAL-UTT = "Bo" constituent, MAX-QUD = ?c.spkr-meaning-rel(addr,Bo,c) Paraphrase: "Who do you mean by Bo?"

Equations

• GinzburgCooper2004.identificationOnBo = GinzburgCooper2004.Apparatus.parameterIdentification GinzburgCooper2004.didBoLeave "b"

def GinzburgCooper2004.existGenOnBo : Apparatus.UttSkeleton

Existential generalization on "Bo" (parameter b). [GC04] ex. 77–78. Removes b from C-PARAMS, weakens content to ∃b.ask(i,j,?.leave-rel(b,t)).

Equations

• GinzburgCooper2004.existGenOnBo = GinzburgCooper2004.Apparatus.existentialGeneralization GinzburgCooper2004.didBoLeave "b"

def GinzburgCooper2004.addresseeISAfterFocussing : Option (Apparatus.IS String String)

B applies parameter focussing to set up clarification context.

Equations

• GinzburgCooper2004.addresseeISAfterFocussing = Option.map GinzburgCooper2004.addresseeIS.applyCoercionStr GinzburgCooper2004.focussingOnBo

def GinzburgCooper2004.addresseeISAfterIdentification : Option (Apparatus.IS String String)

B applies parameter identification to set up clarification context.

Equations

• GinzburgCooper2004.addresseeISAfterIdentification = Option.map GinzburgCooper2004.addresseeIS.applyCoercionStr GinzburgCooper2004.identificationOnBo

theorem GinzburgCooper2004.five_cparams : List.length didBoLeave.cparams = 5

The running example has exactly 5 C-PARAMS.

theorem GinzburgCooper2004.four_constits : didBoLeave.constits.length = 4

The running example has 4 constituents (Did, Bo, leave, Did Bo leave).

theorem GinzburgCooper2004.speaker_resolves_all : speakerAssignment.resolvesAll didBoLeaveCParams = true

Speaker resolves all C-PARAMS.

theorem GinzburgCooper2004.addressee_partial : addresseeAssignment.resolvesAll didBoLeaveCParams = false

Addressee does NOT resolve all C-PARAMS (missing b).

theorem GinzburgCooper2004.addressee_unresolved_is_bo : List.map Discourse.Gameboard.CParam.index (addresseeAssignment.unresolved didBoLeaveCParams) = ["b"]

The unresolved parameter for B is exactly {b}.

theorem GinzburgCooper2004.speaker_grounds : speakerIS.dgb.facts = ["ask(i,j,?.leave-rel(b,t))"]

Speaker's utterance is grounded (added to FACTS).

theorem GinzburgCooper2004.addressee_no_facts : addresseeIS.dgb.facts = []

Addressee's utterance is NOT grounded (no new facts).

theorem GinzburgCooper2004.addressee_has_pending : addresseeIS.pending.length = 1

Addressee's utterance goes to PENDING.

theorem GinzburgCooper2004.focussing_available : focussingOnBo.isSome = true

Parameter focussing succeeds on "Bo".

theorem GinzburgCooper2004.identification_available : identificationOnBo.isSome = true

Parameter identification succeeds on "Bo".

theorem GinzburgCooper2004.coercions_same_salUtt : Option.map Apparatus.CoercionOutput.salUtt focussingOnBo = Option.map Apparatus.CoercionOutput.salUtt identificationOnBo

Both coercions target the same SAL-UTT (the "Bo" constituent).

theorem GinzburgCooper2004.salUtt_is_bo : Option.map (fun (x : Apparatus.CoercionOutput) => x.salUtt.phon) focussingOnBo = some "Bo"

The SAL-UTT is "Bo".

theorem GinzburgCooper2004.different_ops : Option.map Apparatus.CoercionOutput.op focussingOnBo ≠ Option.map Apparatus.CoercionOutput.op identificationOnBo

Focussing and identification produce different operation types.

theorem GinzburgCooper2004.exist_gen_removes_bo : List.length existGenOnBo.cparams = 4

Existential generalization removes exactly one parameter.

theorem GinzburgCooper2004.exist_gen_keeps_others : List.map Discourse.Gameboard.CParam.index existGenOnBo.cparams = ["t", "i", "j", "k"]

The removed parameter is b.

theorem GinzburgCooper2004.exist_gen_weakens_content : existGenOnBo.cont = "∃b.ask(i,j,?.leave-rel(b,t))"

Existential generalization wraps content with ∃.

theorem GinzburgCooper2004.focussing_maxqud : Option.map (fun (x : Apparatus.CoercionOutput) => x.maxQud) focussingOnBo = some "?b.ask(i,j,?.leave-rel(b,t))"

Focussing MAX-QUD is a question about the antecedent content.

theorem GinzburgCooper2004.identification_maxqud : Option.map (fun (x : Apparatus.CoercionOutput) => x.maxQud) identificationOnBo = some "?c.spkr-meaning-rel(addr,Bo,c)"

Identification MAX-QUD is a speaker-meaning question.

def GinzburgCooper2004.coercionToReading : Apparatus.CoercionOp → CEReading

The KOS theory's coercion operations correspond to the empirical CE readings: parameterFocussing ↔ clausal, parameterIdentification ↔ constituent. [GC04] §5.

Equations

• GinzburgCooper2004.coercionToReading GinzburgCooper2004.Apparatus.CoercionOp.paramFocussing = GinzburgCooper2004.CEReading.clausal
• GinzburgCooper2004.coercionToReading GinzburgCooper2004.Apparatus.CoercionOp.paramIdentification = GinzburgCooper2004.CEReading.constituent
• GinzburgCooper2004.coercionToReading GinzburgCooper2004.Apparatus.CoercionOp.existentialGeneralization = GinzburgCooper2004.CEReading.clausal

theorem GinzburgCooper2004.readings_biject_coercions : coercionToReading Apparatus.CoercionOp.paramFocussing ≠ coercionToReading Apparatus.CoercionOp.paramIdentification

The CE data's two readings map to distinct coercion operations.

theorem GinzburgCooper2004.hybrid_content_evidence : didBoLeave.constitForParam "b" = some suBo ∧ didBoLeave.constitForParam "leave-rel" = some suLeave

Hybrid Content Hypothesis ([GC04] ex. 2/16): The content updated in dynamic semantics consists of structure expressing detailed relationships between the content and formal properties (syntax, phonology etc) of the various parts of an utterance.

Evidence: The same propositional content ("Bo left") yields different clarification potentials depending on phonological/syntactic structure. The utterance skeleton encodes this structure via CONSTITS and C-PARAMS.

theorem GinzburgCooper2004.running_example_matches_ce_data : List.map (fun (x : String × Features.Judgment) => x.1) Examples.ex_4a_bo.readings = ["clausal", "constituent"]

The proper-name CE (ex. 4a) carries both readings, in the order the coercion bridge predicts: clausal, then constituent.

theorem GinzburgCooper2004.shared_belief_gates_clausal : Examples.ex_11.readings = [("clausal", Features.Judgment.unacceptable), ("constituent", Features.Judgment.acceptable)] ∧ Examples.ex_12.readings = [("clausal", Features.Judgment.acceptable), ("constituent", Features.Judgment.acceptable)]

Shared-belief minimal pair (ex. 11 vs 12): when A and B are in different locations, "Here?" lacks the clausal reading (no shared belief about the content of "here"); when co-located, both readings survive.

theorem GinzburgCooper2004.indexical_blocks_clausal : List.lookup "clausal" Examples.ex_13a.readings = some Features.Judgment.unacceptable

Indexical CE (ex. 13a): "I?" across speakers shifts reference, so shared belief about content fails and the clausal reading is blocked.