Charlow (2021): post-suppositions and semantic theory

Formalizes [Cha21]'s account of cumulative readings of modified numerals — "exactly three boys saw exactly five movies" — which gives a compositional re-formulation of [Bra13]'s post-suppositional analysis and measures it against the rival repairs the paper canvasses.

The empirical problem: in the pointwise dynamic system (§2), the only derivable reading is the pseudo-cumulative one, where one quantifier's cardinality test is trapped inside the other's maximization operator. Speakers judge the sentence false when four boys participated but some three-boy subgroup saw exactly five movies — the cumulative reading, in which both cardinality tests take widest scope. Four repairs are formalized side by side:

Repair	Type	Cumulative reading
Tower GQs (§3)	Cont (Update S) (Update S → Update S)	✓ derived by scope-taking
Completeness typing (§4)	Completeness annotations	pseudo-cumulative ruled ill-typed
Post-suppositions (§5, App. B)	PostSupp S A (Writer monad)	✓ via deferred cardinality tests
Update semantics (§6)	StateCCP W E	✓ via non-distributive Mvar_u

Main declarations

• cumulativeReading, pseudoCumulativeReading: decidable model-checks over the finite witness scenarios; scenarioB_pseudo_true exhibits the pointwise system's overgeneration.
• Evar, Mvar, CardTest, exactlyN_pw: pointwise dynamic GQ operators; pseudoCumulative and cumulative are the two competing LFs.
• TowerGQ, exactlyN_tower: scope-taking GQs via the substrate Cont monad; cumulativeTower_eq_cumulative proves the tower derivation yields cumulative.
• Completeness, subtypeOf: the complete/incomplete type discipline; pseudo_cumulative_illtyped rules out the bad LF.
• PostSupp: bi-dimensional meanings as mathlib's WriterT (Update S) Id, with Monad/LawfulMonad from the scoped Monoid (Update S) instance; reify_cumulativePostsup proves reification recovers cumulative.
• Evar_u, Mvar_u, CardTest_u: state-level (update-theoretic) GQs; Mvar_u_nondistributive isolates the non-distributivity that produces cumulative readings, while exactlyN_u_distributive shows the single-quantifier pipeline is nevertheless distributive.

Implementation notes

Suffix conventions track the paper's systems: _pw pointwise, _tower, _postsup, _u update-theoretic. The post-suppositional architecture (cardinality tests as a distinguished class of meanings discharged after maximization) is [Bra13]'s; Charlow's contribution is the compositional packaging — §5.1's bi-dimensional pairs, implemented in Appendix B as a Writer monad.

References

• [Cha21]
• [Bra13] (the post-suppositional architecture)
• [Mus96], [Bra07] (the pointwise substrate)
• [BS14] (tower notation)

Witness models: the cumulative-reading puzzle

"Exactly three boys saw exactly five movies." Scenario A (3 boys, 5 movies) verifies both readings. Scenario B (4 boys, 6 movies, with a 3-boy subgroup that saw exactly 5) falsifies the cumulative reading while verifying the pseudo-cumulative one; speakers judge the sentence false there. Both scenarios are the paper's Figure 1, after [Bra13]; scenarioB_saw is one witness graph consistent with the paper's Scenario B constraints.

inductive Charlow2021.Boy3 : Type

• b1 : Boy3
• b2 : Boy3
• b3 : Boy3

@[implicit_reducible]

instance Charlow2021.instDecidableEqBoy3 : DecidableEq Boy3

Equations

• Charlow2021.instDecidableEqBoy3 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Charlow2021.instReprBoy3 : Repr Boy3

Equations

• Charlow2021.instReprBoy3 = { reprPrec := Charlow2021.instReprBoy3.repr }

def Charlow2021.instReprBoy3.repr : Boy3 → ℕ → Std.Format

Equations

• Charlow2021.instReprBoy3.repr Charlow2021.Boy3.b1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Charlow2021.Boy3.b1")).group prec✝
• Charlow2021.instReprBoy3.repr Charlow2021.Boy3.b2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Charlow2021.Boy3.b2")).group prec✝
• Charlow2021.instReprBoy3.repr Charlow2021.Boy3.b3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Charlow2021.Boy3.b3")).group prec✝

inductive Charlow2021.Movie5 : Type

• m1 : Movie5
• m2 : Movie5
• m3 : Movie5
• m4 : Movie5
• m5 : Movie5

@[implicit_reducible]

instance Charlow2021.instDecidableEqMovie5 : DecidableEq Movie5

Equations

• Charlow2021.instDecidableEqMovie5 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Charlow2021.instReprMovie5 : Repr Movie5

Equations

• Charlow2021.instReprMovie5 = { reprPrec := Charlow2021.instReprMovie5.repr }

def Charlow2021.instReprMovie5.repr : Movie5 → ℕ → Std.Format

Equations

• Charlow2021.instReprMovie5.repr Charlow2021.Movie5.m1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Charlow2021.Movie5.m1")).group prec✝
• Charlow2021.instReprMovie5.repr Charlow2021.Movie5.m2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Charlow2021.Movie5.m2")).group prec✝
• Charlow2021.instReprMovie5.repr Charlow2021.Movie5.m3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Charlow2021.Movie5.m3")).group prec✝
• Charlow2021.instReprMovie5.repr Charlow2021.Movie5.m4 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Charlow2021.Movie5.m4")).group prec✝
• Charlow2021.instReprMovie5.repr Charlow2021.Movie5.m5 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Charlow2021.Movie5.m5")).group prec✝

inductive Charlow2021.Boy4 : Type

• b1 : Boy4
• b2 : Boy4
• b3 : Boy4
• b4 : Boy4

@[implicit_reducible]

instance Charlow2021.instDecidableEqBoy4 : DecidableEq Boy4

Equations

• Charlow2021.instDecidableEqBoy4 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Charlow2021.instReprBoy4 : Repr Boy4

Equations

• Charlow2021.instReprBoy4 = { reprPrec := Charlow2021.instReprBoy4.repr }

def Charlow2021.instReprBoy4.repr : Boy4 → ℕ → Std.Format

Equations

• Charlow2021.instReprBoy4.repr Charlow2021.Boy4.b1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Charlow2021.Boy4.b1")).group prec✝
• Charlow2021.instReprBoy4.repr Charlow2021.Boy4.b2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Charlow2021.Boy4.b2")).group prec✝
• Charlow2021.instReprBoy4.repr Charlow2021.Boy4.b3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Charlow2021.Boy4.b3")).group prec✝
• Charlow2021.instReprBoy4.repr Charlow2021.Boy4.b4 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Charlow2021.Boy4.b4")).group prec✝

inductive Charlow2021.Movie6 : Type

• m1 : Movie6
• m2 : Movie6
• m3 : Movie6
• m4 : Movie6
• m5 : Movie6
• m6 : Movie6

@[implicit_reducible]

instance Charlow2021.instDecidableEqMovie6 : DecidableEq Movie6

Equations

• Charlow2021.instDecidableEqMovie6 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Charlow2021.instReprMovie6.repr : Movie6 → ℕ → Std.Format

Equations

• Charlow2021.instReprMovie6.repr Charlow2021.Movie6.m1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Charlow2021.Movie6.m1")).group prec✝
• Charlow2021.instReprMovie6.repr Charlow2021.Movie6.m2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Charlow2021.Movie6.m2")).group prec✝
• Charlow2021.instReprMovie6.repr Charlow2021.Movie6.m3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Charlow2021.Movie6.m3")).group prec✝
• Charlow2021.instReprMovie6.repr Charlow2021.Movie6.m4 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Charlow2021.Movie6.m4")).group prec✝
• Charlow2021.instReprMovie6.repr Charlow2021.Movie6.m5 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Charlow2021.Movie6.m5")).group prec✝
• Charlow2021.instReprMovie6.repr Charlow2021.Movie6.m6 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Charlow2021.Movie6.m6")).group prec✝

@[implicit_reducible]

instance Charlow2021.instReprMovie6 : Repr Movie6

Equations

• Charlow2021.instReprMovie6 = { reprPrec := Charlow2021.instReprMovie6.repr }

def Charlow2021.scenarioA_saw : Boy3 → Movie5 → Bool

Scenario A seeing relation: b1 saw m1, m2; b2 saw m3, m4; b3 saw m5.

Equations

• Charlow2021.scenarioA_saw Charlow2021.Boy3.b1 Charlow2021.Movie5.m1 = true
• Charlow2021.scenarioA_saw Charlow2021.Boy3.b1 Charlow2021.Movie5.m2 = true
• Charlow2021.scenarioA_saw Charlow2021.Boy3.b2 Charlow2021.Movie5.m3 = true
• Charlow2021.scenarioA_saw Charlow2021.Boy3.b2 Charlow2021.Movie5.m4 = true
• Charlow2021.scenarioA_saw Charlow2021.Boy3.b3 Charlow2021.Movie5.m5 = true
• Charlow2021.scenarioA_saw x✝¹ x✝ = false

def Charlow2021.scenarioB_saw : Boy4 → Movie6 → Bool

Scenario B seeing relation: four boys collectively saw six movies, but the subgroup {b1, b2, b3} saw exactly five.

Equations

• Charlow2021.scenarioB_saw Charlow2021.Boy4.b1 Charlow2021.Movie6.m1 = true
• Charlow2021.scenarioB_saw Charlow2021.Boy4.b1 Charlow2021.Movie6.m2 = true
• Charlow2021.scenarioB_saw Charlow2021.Boy4.b2 Charlow2021.Movie6.m3 = true
• Charlow2021.scenarioB_saw Charlow2021.Boy4.b2 Charlow2021.Movie6.m4 = true
• Charlow2021.scenarioB_saw Charlow2021.Boy4.b3 Charlow2021.Movie6.m5 = true
• Charlow2021.scenarioB_saw Charlow2021.Boy4.b4 Charlow2021.Movie6.m6 = true
• Charlow2021.scenarioB_saw x✝¹ x✝ = false

def Charlow2021.cumulativeReading {B : Type u_1} {M : Type u_2} (saw : B → M → Bool) (allBoys : List B) (allMovies : List M) (nBoys nMovies : ℕ) : Bool

Cumulative reading as a global count: exactly nBoys boys saw a movie and exactly nMovies movies were seen.

Equations

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

def Charlow2021.pseudoCumulativeReading {B : Type u_1} {M : Type u_2} (saw : B → M → Bool) (allBoys : List B) (allMovies : List M) (nBoys nMovies : ℕ) : Bool

Pseudo-cumulative reading: some nBoys-sized subset of the boys collectively saw exactly nMovies movies (not required to be the maximal such group).

Equations

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

def Charlow2021.allBoys3 : List Boy3

Equations

• Charlow2021.allBoys3 = [Charlow2021.Boy3.b1, Charlow2021.Boy3.b2, Charlow2021.Boy3.b3]

def Charlow2021.allMovies5 : List Movie5

Equations

• Charlow2021.allMovies5 = [Charlow2021.Movie5.m1, Charlow2021.Movie5.m2, Charlow2021.Movie5.m3, Charlow2021.Movie5.m4, Charlow2021.Movie5.m5]

def Charlow2021.allBoys4 : List Boy4

Equations

• Charlow2021.allBoys4 = [Charlow2021.Boy4.b1, Charlow2021.Boy4.b2, Charlow2021.Boy4.b3, Charlow2021.Boy4.b4]

def Charlow2021.allMovies6 : List Movie6

Equations

• Charlow2021.allMovies6 = [Charlow2021.Movie6.m1, Charlow2021.Movie6.m2, Charlow2021.Movie6.m3, Charlow2021.Movie6.m4, Charlow2021.Movie6.m5, Charlow2021.Movie6.m6]

theorem Charlow2021.scenarioA_cumulative_true : cumulativeReading scenarioA_saw allBoys3 allMovies5 3 5 = true

Scenario A verifies the cumulative reading: 3 boys saw, 5 movies seen.

theorem Charlow2021.scenarioA_pseudo_true : pseudoCumulativeReading scenarioA_saw allBoys3 allMovies5 3 5 = true

Scenario A also verifies the pseudo-cumulative reading.

theorem Charlow2021.scenarioB_cumulative_false : cumulativeReading scenarioB_saw allBoys4 allMovies6 3 5 = false

Scenario B falsifies the cumulative reading: 4 boys saw (not 3) and 6 movies were seen (not 5). This matches speakers' judgments.

theorem Charlow2021.scenarioB_pseudo_true : pseudoCumulativeReading scenarioB_saw allBoys4 allMovies6 3 5 = true

Scenario B verifies the pseudo-cumulative reading — the pointwise system's overgeneration: {b1, b2, b3} saw exactly five movies.

Pointwise dynamic GQs (§2)

[Mus96]/[Bra07]-style operators over the pointwise Update S := S → S → Prop. The pointwise system derives only the pseudo-cumulative LF; the cumulative LF is the target the repairs below must reach.

def Charlow2021.Evar {S : Type u_1} {E : Type u_2} [Semantics.Dynamic.Core.AssignmentStructure S E] (v : Semantics.Dynamic.Core.Dref S E) (P : E → Prop) : Semantics.Dynamic.Core.Update S

Existential dref introduction (eq. 17): introduce a referent satisfying P at dref v.

Equations

• Charlow2021.Evar v P i j = ∃ (x : E), P x ∧ j = Semantics.Dynamic.Core.AssignmentStructure.extend i v x

def Charlow2021.Mvar {S : Type u_1} {E : Type u_2} [PartialOrder E] (v : Semantics.Dynamic.Core.Dref S E) (D : Semantics.Dynamic.Core.Update S) : Semantics.Dynamic.Core.Update S

Mereological maximization (eq. 18): retain outputs of D whose v-value is maximal among the v-values of all outputs of D.

Equations

• Charlow2021.Mvar v D i j = (D i j ∧ Maximal (fun (x : E) => ∃ (k : S), D i k ∧ v k = x) (v j))

def Charlow2021.CardTest {S : Type u_1} {E : Type u_2} [PartialOrder E] [Fintype E] (v : Semantics.Dynamic.Core.Dref S E) (n : ℕ) : Semantics.Dynamic.Core.Update S

Cardinality test (eq. 19): test (identity on assignments) that the atom count of v equals n.

Equations

• Charlow2021.CardTest v n i j = (i = j ∧ Mereology.atomCount E (v j) = n)

def Charlow2021.sawDRS {S : Type u_1} {E : Type u_2} (u v : Semantics.Dynamic.Core.Dref S E) (R : E → E → Prop) : Semantics.Dynamic.Core.Update S

Transitive verb as a test that R holds between two drefs.

Equations

• Charlow2021.sawDRS u v R = Semantics.Dynamic.Core.test fun (i : S) => R (u i) (v i)

def Charlow2021.exactlyN_pw {S : Type u_1} {E : Type u_2} [Semantics.Dynamic.Core.AssignmentStructure S E] [PartialOrder E] [Fintype E] (v : Semantics.Dynamic.Core.Dref S E) (P : E → Prop) (n : ℕ) : Semantics.Dynamic.Core.Update S

Composed pointwise "exactly n" with trivial nuclear scope: E^v P ; M_v(E^v P) ; n_v (the flat counterpart of the scope-taking dynamic-GQ entry, eq. 3).

Equations

• Charlow2021.exactlyN_pw v P n = Charlow2021.Evar v P ⨟ Charlow2021.Mvar v (Charlow2021.Evar v P) ⨟ Charlow2021.CardTest v n

def Charlow2021.pseudoCumulative {S : Type u_1} {E : Type u_2} [Semantics.Dynamic.Core.AssignmentStructure S E] [PartialOrder E] [Fintype E] (v u : Semantics.Dynamic.Core.Dref S E) (boys movies : E → Prop) (saw' : E → E → Prop) : Semantics.Dynamic.Core.Update S

The pseudo-cumulative LF (5): the object's cardinality test is trapped inside the subject's maximization.

Equations

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

def Charlow2021.cumulative {S : Type u_1} {E : Type u_2} [Semantics.Dynamic.Core.AssignmentStructure S E] [PartialOrder E] [Fintype E] (v u : Semantics.Dynamic.Core.Dref S E) (boys movies : E → Prop) (saw' : E → E → Prop) : Semantics.Dynamic.Core.Update S

The cumulative LF (6): both cardinality tests scope outside both maximizations.

Equations

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

Higher-order (tower) GQs (§3)

A modified numeral denotes a scope-taking dynamic meaning rather than a flat Update S. The flat continuized type Cont (Update S) (Update S) does not suffice: its continuation receives an already-maximized update, so the nuclear scope can only attach outside maximization.

@[reducible, inline]

abbrev Charlow2021.TowerGQ (S : Type u_3) : Type u_3

Higher-order dynamic GQ type, (Q → t) → t with Q ::= (e→t)→t (eq. 24), rendered via the substrate continuation monad with answer type Update S and the scope argument flattened to Update S → Update S (the dref is supplied by the GQ itself). §3.4 introduces [BS14]-style tower notation for these meanings.

Equations

• Charlow2021.TowerGQ S = Semantics.Composition.Continuation.Cont (Semantics.Dynamic.Core.Update S) (Semantics.Dynamic.Core.Update S → Semantics.Dynamic.Core.Update S)

def Charlow2021.exactlyN_tower {S : Type u_1} {E : Type u_2} [Semantics.Dynamic.Core.AssignmentStructure S E] [PartialOrder E] [Fintype E] (v : Semantics.Dynamic.Core.Dref S E) (P : E → Prop) (n : ℕ) : TowerGQ S

"Exactly n" as a higher-order GQ (eq. 24): λc. c (λk. M_v(E^v P ; k v)) ; n_v, with the scope-taker rendered as Update S → Update S. The cardinality test is evaluated after the higher-order scope argument c — the key that unlocks cumulative readings.

Equations

• Charlow2021.exactlyN_tower v P n k = (k fun (body : Semantics.Dynamic.Core.Update S) => Charlow2021.Mvar v (Charlow2021.Evar v P ⨟ body)) ⨟ Charlow2021.CardTest v n

def Charlow2021.cumulativeTower {S : Type u_1} {E : Type u_2} [Semantics.Dynamic.Core.AssignmentStructure S E] [PartialOrder E] [Fintype E] (v u : Semantics.Dynamic.Core.Dref S E) (boys movies : E → Prop) (saw' : E → E → Prop) : Semantics.Dynamic.Core.Update S

Higher-order derivation of "exactly 3 boys saw exactly 5 movies" (eq. 27, derived in §3.3 by β-reduction of the linearized terms; §3.4's towers are notational sugar for the same derivation): sawDRS threads inside both maximizations while both cardinality tests land outside.

Equations

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

theorem Charlow2021.cumulativeTower_eq_cumulative {S : Type u_1} {E : Type u_2} [Semantics.Dynamic.Core.AssignmentStructure S E] [PartialOrder E] [Fintype E] (v u : Semantics.Dynamic.Core.Dref S E) (boys movies : E → Prop) (saw' : E → E → Prop) : cumulativeTower v u boys movies saw' = cumulative v u boys movies saw'

The tower derivation produces exactly the cumulative LF (6) — the reading the pointwise system cannot reach.

Completeness typing (§4)

A type discipline distinguishing complete (T) from incomplete (t) dynamic meanings: maximization traffics in incomplete meanings, cardinality tests output complete ones, and t ⊏ T but not T ⊏ t. The pseudo-cumulative LF then fails to type-check.

inductive Charlow2021.Completeness : Type

Completeness level: incomplete (t, awaiting a cardinality test) vs complete (T, ready for discourse integration).

• incomplete : Completeness
• complete : Completeness

@[implicit_reducible]

instance Charlow2021.instDecidableEqCompleteness : DecidableEq Completeness

Equations

• Charlow2021.instDecidableEqCompleteness x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Charlow2021.instReprCompleteness.repr : Completeness → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Charlow2021.instReprCompleteness : Repr Completeness

Equations

• Charlow2021.instReprCompleteness = { reprPrec := Charlow2021.instReprCompleteness.repr }

def Charlow2021.subtypeOf : Completeness → Completeness → Prop

Subtyping: t ⊏ T (incomplete promotes to complete) but not T ⊏ t.

Equations

• Charlow2021.subtypeOf Charlow2021.Completeness.incomplete x✝ = True
• Charlow2021.subtypeOf Charlow2021.Completeness.complete Charlow2021.Completeness.complete = True
• Charlow2021.subtypeOf Charlow2021.Completeness.complete Charlow2021.Completeness.incomplete = False

@[implicit_reducible]

instance Charlow2021.instDecidableRelCompletenessSubtypeOf : DecidableRel subtypeOf

Equations

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

def Charlow2021.«term_⊏_» : Lean.TrailingParserDescr

Subtyping: t ⊏ T (incomplete promotes to complete) but not T ⊏ t.

Equations

• Charlow2021.«term_⊏_» = Lean.ParserDescr.trailingNode `Charlow2021.«term_⊏_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊏ ") (Lean.ParserDescr.cat `term 51))

def Charlow2021.Evar_type : Completeness

E^v outputs an incomplete meaning.

Equations

• Charlow2021.Evar_type = Charlow2021.Completeness.incomplete

def Charlow2021.Mvar_type : Completeness

M_v outputs an incomplete meaning (and demands incomplete input).

Equations

• Charlow2021.Mvar_type = Charlow2021.Completeness.incomplete

def Charlow2021.CardTest_type : Completeness

A cardinality test outputs a complete meaning.

Equations

• Charlow2021.CardTest_type = Charlow2021.Completeness.complete

def Charlow2021.dynConj_type (c : Completeness) : Completeness

Dynamic conjunction preserves completeness.

Equations

• Charlow2021.dynConj_type c = c

theorem Charlow2021.cumulative_welltyped : subtypeOf (dynConj_type (dynConj_type Mvar_type)) CardTest_type

The cumulative LF is well-typed (eq. 45): the nested maximizations yield an incomplete meaning, which the outer cardinality tests accept since t ⊏ T.

theorem Charlow2021.pseudo_cumulative_illtyped : ¬subtypeOf CardTest_type Mvar_type

The pseudo-cumulative LF is ill-typed (eq. 46): a cardinality test (complete) cannot feed maximization, which demands incomplete input.

Post-suppositional GQs (§5, Appendix B)

[Bra13]'s post-suppositional architecture in [Cha21]'s compositional packaging: a bi-dimensional meaning pairs an at-issue value with post-suppositional content — an Update accumulated via dynamic conjunction and discharged at the discourse level after scope-taking (§5.1) — implemented in Appendix B as a Writer monad over the monoid (Update S, dseq, test ⊤).

@[reducible, inline]

abbrev Charlow2021.PostSupp (S A : Type u) : Type u

Bi-dimensional meaning (§5.1): an at-issue value paired with accumulated post-suppositional content — mathlib's Writer monad WriterT (Update S) Id over the monoid (Update S, ⨟, test ⊤). The Monad/LawfulMonad instances come from mathlib via the scoped Monoid (Update S) instance, and agree with the paper's pure/bind (Appendix B, eqs. 120–121): pure carries the trivial post-supposition; bind accumulates post-suppositions via dseq.

Equations

• Charlow2021.PostSupp S A = WriterT (Semantics.Dynamic.Core.Update S) Id A

def Charlow2021.PostSupp.mk {S A : Type u} (a : A) (w : Semantics.Dynamic.Core.Update S) : PostSupp S A

Construct a bi-dimensional meaning from an at-issue value and a post-supposition.

Equations

• Charlow2021.PostSupp.mk a w = WriterT.mk (a, w)

def Charlow2021.PostSupp.val {S A : Type u} (p : PostSupp S A) : A

The at-issue value.

Equations

• p.val = (WriterT.run p).1

def Charlow2021.PostSupp.postsup {S A : Type u} (p : PostSupp S A) : Semantics.Dynamic.Core.Update S

Accumulated post-suppositional content.

Equations

• p.postsup = (WriterT.run p).2

@[simp]

theorem Charlow2021.PostSupp.val_mk {S A : Type u} (a : A) (w : Semantics.Dynamic.Core.Update S) : (PostSupp.mk a w).val = a

@[simp]

theorem Charlow2021.PostSupp.postsup_mk {S A : Type u} (a : A) (w : Semantics.Dynamic.Core.Update S) : (PostSupp.mk a w).postsup = w

@[simp]

theorem Charlow2021.PostSupp.val_pure {S A : Type u} (a : A) : (pure a).val = a

@[simp]

theorem Charlow2021.PostSupp.postsup_pure {S A : Type u} (a : A) : (pure a).postsup = Semantics.Dynamic.Core.test fun (x : S) => True

@[simp]

theorem Charlow2021.PostSupp.val_bind {S A B : Type u} (m : PostSupp S A) (f : A → PostSupp S B) : (m >>= f).val = (f m.val).val

@[simp]

theorem Charlow2021.PostSupp.postsup_bind {S A B : Type u} (m : PostSupp S A) (f : A → PostSupp S B) : (m >>= f).postsup = m.postsup ⨟ (f m.val).postsup

def Charlow2021.PostSupp.reify {S : Type u} (p : PostSupp S (Semantics.Dynamic.Core.Update S)) : Semantics.Dynamic.Core.Update S

Reification (the bullet operator, eq. 58): sequence the at-issue update with its accumulated post-supposition.

Equations

• p.reify = p.val ⨟ p.postsup

@[simp]

theorem Charlow2021.PostSupp.reify_pure {S : Type u} (D : Semantics.Dynamic.Core.Update S) : (pure D).reify = D

def Charlow2021.PostSupp.trueAt {S : Type u} (p : PostSupp S (Semantics.Dynamic.Core.Update S)) (i : S) : Prop

Truth of a bi-dimensional meaning at an assignment (eq. 56): the reified update is true at i in the substrate sense.

Equations

• p.trueAt i = Semantics.Dynamic.Core.trueAt p.reify i

def Charlow2021.exactlyN_postsup {S : Type u_1} {E : Type u_2} [Semantics.Dynamic.Core.AssignmentStructure S E] [PartialOrder E] [Fintype E] (v : Semantics.Dynamic.Core.Dref S E) (P : E → Prop) (n : ℕ) : PostSupp S (Semantics.Dynamic.Core.Update S)

"Exactly n" as a bi-dimensional meaning (eq. 53): maximized dref introduction at issue; the cardinality test deferred as a post-supposition.

Equations

• Charlow2021.exactlyN_postsup v P n = Charlow2021.PostSupp.mk (Charlow2021.Mvar v (Charlow2021.Evar v P)) (Charlow2021.CardTest v n)

def Charlow2021.cumulativePostsup {S : Type u_1} {E : Type u_2} [Semantics.Dynamic.Core.AssignmentStructure S E] [PartialOrder E] [Fintype E] (v u : Semantics.Dynamic.Core.Dref S E) (boys movies : E → Prop) (saw' : E → E → Prop) : PostSupp S (Semantics.Dynamic.Core.Update S)

Bi-dimensional derivation of "exactly 3 boys saw exactly 5 movies": nested maximizations at issue; both cardinality tests accumulate post-suppositionally (under bind, tests from different quantifiers simply dseq-accumulate, independent of scope).

Equations

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

theorem Charlow2021.reify_cumulativePostsup {S : Type u_1} {E : Type u_2} [Semantics.Dynamic.Core.AssignmentStructure S E] [PartialOrder E] [Fintype E] (v u : Semantics.Dynamic.Core.Dref S E) (boys movies : E → Prop) (saw' : E → E → Prop) : (cumulativePostsup v u boys movies saw').reify = cumulative v u boys movies saw'

Reifying the bi-dimensional derivation recovers exactly the cumulative LF (6): deferring cardinality tests as post-suppositions yields the cumulative reading.

Update-theoretic GQs (§6)

The same operators defined directly over StateCCP W E := State W E → State W E. Mvar_u maximizes over the entire context, not per-assignment; this makes it non-distributive, which is what produces cumulative readings without towers, typing, or post-suppositions.

def Charlow2021.Evar_u {W : Type u_1} {E : Type u_2} (v : ℕ) (P : E → Prop) : Semantics.Dynamic.Core.StateCCP W E

Existential dref introduction at the state level (eq. 74): for each world–assignment pair in the context, non-deterministically extend the assignment at position v with an entity satisfying P.

Equations

• Charlow2021.Evar_u v P s = {p : W × Core.Assignment E | ∃ q ∈ s, p.1 = q.1 ∧ ∃ (x : E), P x ∧ p.2 = Function.update q.2 v x}

def Charlow2021.Mvar_u {W : Type u_1} {E : Type u_2} (v : ℕ) (K : Semantics.Dynamic.Core.StateCCP W E) [PartialOrder E] : Semantics.Dynamic.Core.StateCCP W E

Mereological maximization at the state level (eq. 78): apply K, then retain only output pairs whose v-value is maximal across the entire output state. This is the non-distributive operator.

Equations

• Charlow2021.Mvar_u v K s = {p : W × Core.Assignment E | p ∈ K s ∧ Maximal (fun (x : E) => ∃ q ∈ K s, q.2 v = x) (p.2 v)}

def Charlow2021.CardTest_u {W : Type u_1} {E : Type u_2} (v n : ℕ) [PartialOrder E] [Fintype E] : Semantics.Dynamic.Core.StateCCP W E

Cardinality test at the state level (eq. 75): filter the context for pairs where the atom count of v equals n.

Equations

• Charlow2021.CardTest_u v n s = {p : W × Core.Assignment E | p ∈ s ∧ Mereology.atomCount E (p.2 v) = n}

def Charlow2021.dseq_u {W : Type u_1} {E : Type u_2} (L R : Semantics.Dynamic.Core.StateCCP W E) : Semantics.Dynamic.Core.StateCCP W E

Dynamic sequencing at the state level (eq. 80): function composition, s[L ; R] := R (L s).

Equations

• Charlow2021.dseq_u L R = R ∘ L

def Charlow2021.RelTest {W : Type u_1} {E : Type u_2} (v₁ v₂ : ℕ) (R : E → E → Prop) : Semantics.Dynamic.Core.StateCCP W E

Relational test at the state level (eq. 73, the paper's entry for saw): filter for assignments where R (g v₁) (g v₂) holds.

Equations

• Charlow2021.RelTest v₁ v₂ R s = {p : W × Core.Assignment E | p ∈ s ∧ R (p.2 v₁) (p.2 v₂)}

def Charlow2021.exactlyN_u {W : Type u_1} {E : Type u_2} (v : ℕ) (P : E → Prop) (n : ℕ) [PartialOrder E] [Fintype E] : Semantics.Dynamic.Core.StateCCP W E

Single-quantifier "exactly n" pipeline, E^v P ; M_v(E^v P) ; n_v — the trivial-scope instantiation of the scope-taking update GQ (eq. 81).

Equations

• Charlow2021.exactlyN_u v P n = Charlow2021.dseq_u (Charlow2021.dseq_u (Charlow2021.Evar_u v P) (Charlow2021.Mvar_u v (Charlow2021.Evar_u v P))) (Charlow2021.CardTest_u v n)

def Charlow2021.sentenceMeaning_u {W : Type u_1} {E : Type u_2} (v u : ℕ) (PSubj PObj : E → Prop) (R : E → E → Prop) (nSubj nObj : ℕ) [PartialOrder E] [Fintype E] : Semantics.Dynamic.Core.StateCCP W E

Update-theoretic meaning of "exactly nSubj PSubj R exactly nObj PObj" (eq. 82): M_v(E^v P_subj ; M_u(E^u P_obj ; R u v) ; n_obj) ; n_subj. This has the same shape as the pointwise pseudo-cumulative LF (5) — the object's cardinality test sits inside M_v — yet because Mvar_u maximizes over the whole context it correctly represents the cumulative reading (the paper's (83)/(84) contrast).

Equations

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

theorem Charlow2021.Mvar_u_nondistributive {W : Type u_1} {E : Type u_2} [PartialOrder E] [Nonempty W] (a b : E) (hab : a < b) : ∃ (v : ℕ) (K : Semantics.Dynamic.Core.StateCCP W E), ¬Semantics.Dynamic.Core.IsDistributive (Mvar_u v K)

M_v is not distributive: it surveys the entire context to determine which assignments carry maximal v-values. With two pairs whose v-values are a < b, whole-context maximization discards the a-pair, but per-element processing keeps both.

theorem Charlow2021.CardTest_u_distributive {W : Type u_1} {E : Type u_2} [PartialOrder E] [Fintype E] (v n : ℕ) : Semantics.Dynamic.Core.IsDistributive (CardTest_u v n)

Cardinality tests are distributive: they inspect one pair at a time.

theorem Charlow2021.exactlyN_u_distributive {W : Type u_1} {E : Type u_2} [PartialOrder E] [Fintype E] (v : ℕ) (P : E → Prop) (n : ℕ) : Semantics.Dynamic.Core.IsDistributive (exactlyN_u v P n)

The composed "exactly n" pipeline is distributive despite containing the non-distributive Mvar_u: Evar_u normalizes the v-values to {x | P x} regardless of input, so maximization selects the same elements whether processing the full state or per-element. Cumulative readings arise from the non-distributivity of Mvar_u itself (Mvar_u_nondistributive), not from the single-quantifier pipeline.

Comparing the repairs

The tower and post-suppositional derivations provably recover the cumulative LF (cumulativeTower_eq_cumulative, reify_cumulativePostsup); completeness typing instead rules the pseudo-cumulative LF out (pseudo_cumulative_illtyped); update semantics derives cumulativity from the non-distributivity of Mvar_u (Mvar_u_nondistributive) with no apparatus beyond StateCCP.

theorem Charlow2021.dependent_indefinites_need_extra {W : Type u_1} {E : Type u_2} [Nonempty W] [Nonempty E] : ¬∀ (depIndef : Semantics.Dynamic.Core.StateCCP W E), Semantics.Dynamic.Core.IsDistributive depIndef

Dependent indefinites (§7.2) outrun distributive update semantics: not every state-level CCP is distributive. Witness: the constant CCP λ _ => Set.univ maps ∅ to Set.univ, but per-element processing of ∅ yields ∅.