Charlow (2021): Post-suppositions and semantic theory

Exactly three boys saw exactly five movies has a cumulative reading: the boys who saw movies are three, and the movies they saw are five. Charlow shows that the obvious pointwise dynamic meaning for modified numerals derives only a weaker pseudo-cumulative reading, which is also true when four boys saw six movies, and compares three repairs: higher-order dynamic quantifiers whose cardinality tests take scope on their own, made safe by a subtyping discipline; Brasoveanu's post-suppositions, packaged as a Writer monad; and an update semantics whose maximization surveys whole contexts. The update semantics derives the cumulative reading from meanings of the pseudo-cumulative form.

Main definitions

• Evar, card, relTest: dref introduction (17), the cardinality test (19) and a dynamic verb (11); maximization (18) is Update.maxAt.
• pseudoCumulative, cumulative: the logical forms (5) and (6).
• exactly, exactlyHO: the dynamic quantifier (3) and the higher-order one (24), in mathlib's continuation monad.
• HasType: the typing (44) of logical forms, with t a subtype of T.
• PostSupp, exactlyPS, sentencePS: post-suppositional meanings (53) and the sentence (55).
• maxAtU, exactlyU, sentenceU: update-theoretic maximization (78), the quantifier (81) and the sentence (82).

Main results

• cumulative_scenarioA, cumulative_scenarioB, pseudoCumulative_scenarioB: on the models of Figure 1, (6) holds in Scenario A only, while (5) holds in Scenario B.
• scope27 through scope33: the six scopings of two higher-order quantifiers reduce to (27)–(30) and (32)–(33); four agree with (6) on Figure 1 and two are pseudo-cumulative.
• hasType_cumulative, not_hasType_pseudoCumulative: (45) has type T and (46) has none.
• reify_sentencePS: the post-suppositional sentence reifies to (6).
• lower_maxAtU_image: the two maximizations are alphabetic variants (79).
• sentenceU_scenarioA, sentenceU_scenarioB: (82) is cumulative on Figure 1, and down_sentenceULowered recovers (5) once the object's maximization is lifted from its pointwise counterpart, so that update-theoretic maximization is not distributive (not_isDistributive_maxAtU).

Implementation notes

• Registers model the paper's variables, and entities are finite sets of atoms, as in §2.1.
• A dynamic quantifier of type (e → t) → t is Cont (Update S) R; a higher-order one is Cont (Update S) (Cont (Update S) R), and (26) is the monad's joinM.
• The numerals are parameters. The cardinality test counts atoms (Mereology.atomCount).
• Contexts of the update semantics are sets of assignments, and truth at an assignment is a nonempty update of its singleton (CCP.down).
• The distributivity operators (48), (59) and (85), islands (§5.2) and §7 are not formalized, nor the subtyping of towers (40)–(41) beyond the typing of logical forms.

References

• [Cha21]
• [Bra13]

Pointwise dynamic meanings (§2)

def Charlow2021.Evar {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] (v : R) (P : E → Prop) : DynamicSemantics.Update S

Evar v P stores in v some entity satisfying P (17).

Equations

• Charlow2021.Evar v P = DynamicSemantics.Update.box {v} {i : S | P (DynamicSemantics.RegisterStructure.val v i)}

theorem Charlow2021.mem_Evar {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] {v : R} {P : E → Prop} {i j : S} : (i, j) ∈ Evar v P ↔ ∃ (x : E), P x ∧ j = DynamicSemantics.RegisterStructure.extend i v x

theorem Charlow2021.fixes_Evar {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] {v r : R} (h : r ≠ v) (P : E → Prop) : DynamicSemantics.Update.Fixes r (Evar v P)

def Charlow2021.relTest {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] (u v : R) (r : E → E → Prop) : DynamicSemantics.Update S

relTest u v r is the dynamic verb that tests r of the values of u and v (11).

Equations

• Charlow2021.relTest u v r = DynamicSemantics.Update.test {i : S | r (DynamicSemantics.RegisterStructure.val u i) (DynamicSemantics.RegisterStructure.val v i)}

theorem Charlow2021.mem_maxAt_Evar_comp_test {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] {u : R} {Q : E → Prop} {C : DynamicSemantics.Condition S} {i j : S} : (i, j) ∈ DynamicSemantics.Update.maxAt u (SetRel.comp (Evar u Q) (DynamicSemantics.Update.test C)) ↔ ∃ (y : E), j = DynamicSemantics.RegisterStructure.extend i u y ∧ Maximal (fun (y : E) => Q y ∧ DynamicSemantics.RegisterStructure.extend i u y ∈ C) y

Maximizing a register just introduced under a test keeps its maximal values.

theorem Charlow2021.mem_maxAt_Evar_comp {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] {v : R} {P Q : E → Prop} {D : DynamicSemantics.Update S} (hD : DynamicSemantics.Update.Fixes v D) {i j : S} (hQ : ∀ (x : E), P x → ((∃ (k : S), (DynamicSemantics.RegisterStructure.extend i v x, k) ∈ D) ↔ Q x)) : (i, j) ∈ DynamicSemantics.Update.maxAt v (SetRel.comp (Evar v P) D) ↔ (DynamicSemantics.RegisterStructure.extend i v (DynamicSemantics.RegisterStructure.val v j), j) ∈ D ∧ Maximal (fun (x : E) => P x ∧ Q x) (DynamicSemantics.RegisterStructure.val v j)

Maximizing a register introduced before an update that keeps it, given when the update has an output.

def Charlow2021.card {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] [Fintype E] (v : R) (n : ℕ) : DynamicSemantics.Update S

card v n tests that the value of v has n atoms (19).

Equations

• Charlow2021.card v n = DynamicSemantics.Update.test {i : S | Mereology.atomCount E (DynamicSemantics.RegisterStructure.val v i) = n}

theorem Charlow2021.mem_comp_card {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] [Fintype E] {D : DynamicSemantics.Update S} {v : R} {n : ℕ} {i j : S} : (i, j) ∈ SetRel.comp D (card v n) ↔ (i, j) ∈ D ∧ Mereology.atomCount E (DynamicSemantics.RegisterStructure.val v j) = n

theorem Charlow2021.card_comp_card_comm {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] [Fintype E] (v u : R) (n m : ℕ) : SetRel.comp (card v n) (card u m) = SetRel.comp (card u m) (card v n)

Cardinality tests commute, so the order of the tests in (6) and (8) is immaterial (fn. 4).

def Charlow2021.pseudoCumulative {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] [Fintype E] (v u : R) (P Q : E → Prop) (r : E → E → Prop) (n m : ℕ) : DynamicSemantics.Update S

pseudoCumulative is the logical form (5), whose object's cardinality test is trapped under the subject's maximization.

Equations

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

def Charlow2021.cumulative {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] [Fintype E] (v u : R) (P Q : E → Prop) (r : E → E → Prop) (n m : ℕ) : DynamicSemantics.Update S

cumulative is the logical form (6), with both cardinality tests outside both maximizations.

Equations

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

Higher-order dynamic quantifiers (§3)

def Charlow2021.exactly {R S : Type u} {E : Type u_1} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] [Fintype E] (v : R) (n : ℕ) (P : E → Prop) : Cont (DynamicSemantics.Update S) R

exactly v n P is the dynamic quantifier (3), which introduces, maximizes and counts in one scope.

Equations

• Charlow2021.exactly v n P k = SetRel.comp (DynamicSemantics.Update.maxAt v (SetRel.comp (Charlow2021.Evar v P) (k v))) (Charlow2021.card v n)

def Charlow2021.exactlyHO {R S : Type u} {E : Type u_1} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] [Fintype E] (v : R) (n : ℕ) (P : E → Prop) : Cont (DynamicSemantics.Update S) (Cont (DynamicSemantics.Update S) R)

exactlyHO v n P is the higher-order dynamic quantifier (24), whose cardinality test scopes above its trace.

Equations

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

theorem Charlow2021.joinM_exactlyHO {R S : Type u} {E : Type u_1} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] [Fintype E] (v : R) (n : ℕ) (P : E → Prop) : joinM (exactlyHO v n P) = exactly v n P

The map (26) from higher-order to ordinary quantifiers is the continuation monad's joinM, and sends both the Lift (23) of (3) and (24) to (3).

theorem Charlow2021.joinM_pure_exactly {R S : Type u} {E : Type u_1} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] [Fintype E] (v : R) (n : ℕ) (P : E → Prop) : joinM (pure (exactly v n P)) = exactly v n P

theorem Charlow2021.scope27 {R S : Type u} {E : Type u_1} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] [Fintype E] (v u : R) (P Q : E → Prop) (r : E → E → Prop) (n m : ℕ) : (exactlyHO v n P fun (V : Cont (DynamicSemantics.Update S) R) => exactlyHO u m Q fun (U : Cont (DynamicSemantics.Update S) R) => V fun (a : R) => U fun (b : R) => relTest b a r) = cumulative v u P Q r n m

The scoping (27) is the cumulative logical form (6).

theorem Charlow2021.scope28 {R S : Type u} {E : Type u_1} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] [Fintype E] (v u : R) (P Q : E → Prop) (r : E → E → Prop) (n m : ℕ) : (exactlyHO v n P fun (V : Cont (DynamicSemantics.Update S) R) => exactlyHO u m Q fun (U : Cont (DynamicSemantics.Update S) R) => U fun (b : R) => V fun (a : R) => relTest b a r) = cumulative u v Q P (flip r) m n

The scoping (28) reverses the traces, and is (6) with the object's maximization outside.

theorem Charlow2021.scope29 {R S : Type u} {E : Type u_1} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] [Fintype E] (v u : R) (P Q : E → Prop) (r : E → E → Prop) (n m : ℕ) : (exactlyHO u m Q fun (U : Cont (DynamicSemantics.Update S) R) => exactlyHO v n P fun (V : Cont (DynamicSemantics.Update S) R) => V fun (a : R) => U fun (b : R) => relTest b a r) = cumulative v u P Q r n m

The scoping (29) reverses the quantifiers, which only reorders the tests of (27).

theorem Charlow2021.scope30 {R S : Type u} {E : Type u_1} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] [Fintype E] (v u : R) (P Q : E → Prop) (r : E → E → Prop) (n m : ℕ) : (exactlyHO u m Q fun (U : Cont (DynamicSemantics.Update S) R) => exactlyHO v n P fun (V : Cont (DynamicSemantics.Update S) R) => U fun (b : R) => V fun (a : R) => relTest b a r) = cumulative u v Q P (flip r) m n

The scoping (30) reverses both.

theorem Charlow2021.scope32 {R S : Type u} {E : Type u_1} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] [Fintype E] (v u : R) (P Q : E → Prop) (r : E → E → Prop) (n m : ℕ) : (exactlyHO v n P fun (V : Cont (DynamicSemantics.Update S) R) => V fun (a : R) => exactlyHO u m Q fun (U : Cont (DynamicSemantics.Update S) R) => U fun (b : R) => relTest b a r) = pseudoCumulative v u P Q r n m

The scoping (32) puts the object under the subject's trace, giving the pseudo-cumulative (5).

theorem Charlow2021.scope33 {R S : Type u} {E : Type u_1} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] [Fintype E] (v u : R) (P Q : E → Prop) (r : E → E → Prop) (n m : ℕ) : (exactlyHO u m Q fun (U : Cont (DynamicSemantics.Update S) R) => U fun (b : R) => exactlyHO v n P fun (V : Cont (DynamicSemantics.Update S) R) => V fun (a : R) => relTest b a r) = pseudoCumulative u v Q P (flip r) m n

The scoping (33) puts the subject under the object's trace.

Subtyping (§4.2)

inductive Charlow2021.LF (R : Type u_3) (E : Type u_4) : Type (max u_3 u_4)

LF R E is the syntax of logical forms built from the operators typed in (44).

• dref {R : Type u_3} {E : Type u_4} (v : R) (P : E → Prop) : LF R E
• max {R : Type u_3} {E : Type u_4} (v : R) (K : LF R E) : LF R E
• card {R : Type u_3} {E : Type u_4} (v : R) (n : ℕ) : LF R E
• rel {R : Type u_3} {E : Type u_4} (u v : R) (r : E → E → Prop) : LF R E
• seq {R : Type u_3} {E : Type u_4} (K L : LF R E) : LF R E

inductive Charlow2021.Ty : Type

Ty has the types of possibly incomplete (t) and definitely complete (T) sentences (39).

• t : Ty
• T : Ty

inductive Charlow2021.HasType {R : Type u_1} {E : Type u_2} : LF R E → Ty → Prop

HasType K A is the typing (44), under which dref introduction and verbs are t, cardinality tests are T, maximization takes and returns t, and dynamic conjunction is polymorphic, with t a subtype of T (39).

• dref {R : Type u_1} {E : Type u_2} (v : R) (P : E → Prop) : HasType (LF.dref v P) Ty.t
• rel {R : Type u_1} {E : Type u_2} (u v : R) (r : E → E → Prop) : HasType (LF.rel u v r) Ty.t
• card {R : Type u_1} {E : Type u_2} (v : R) (n : ℕ) : HasType (LF.card v n) Ty.T
• max {R : Type u_1} {E : Type u_2} (v : R) {K : LF R E} : HasType K Ty.t → HasType (LF.max v K) Ty.t
• seq {R : Type u_1} {E : Type u_2} {K L : LF R E} {A : Ty} : HasType K A → HasType L A → HasType (K.seq L) A
• sub {R : Type u_1} {E : Type u_2} {K : LF R E} : HasType K Ty.t → HasType K Ty.T

theorem Charlow2021.HasType.of_max {R : Type u_1} {E : Type u_2} {v : R} {K : LF R E} {A : Ty} (h : HasType (LF.max v K) A) : HasType K Ty.t

theorem Charlow2021.HasType.right_of_seq {R : Type u_1} {E : Type u_2} {K L : LF R E} (h : HasType (K.seq L) Ty.t) : HasType L Ty.t

theorem Charlow2021.not_hasType_card_t {R : Type u_1} {E : Type u_2} (v : R) (n : ℕ) : ¬HasType (LF.card v n) Ty.t

def Charlow2021.LF.cumulative {R : Type u_1} {E : Type u_2} (v u : R) (P Q : E → Prop) (r : E → E → Prop) (n m : ℕ) : LF R E

LF.cumulative is the logical form (45).

Equations

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

def Charlow2021.LF.pseudoCumulative {R : Type u_1} {E : Type u_2} (v u : R) (P Q : E → Prop) (r : E → E → Prop) (n m : ℕ) : LF R E

LF.pseudoCumulative is the logical form (46).

Equations

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

theorem Charlow2021.hasType_cumulative {R : Type u_1} {E : Type u_2} (v u : R) (P Q : E → Prop) (r : E → E → Prop) (n m : ℕ) : HasType (LF.cumulative v u P Q r n m) Ty.T

(45) has type T.

theorem Charlow2021.not_hasType_pseudoCumulative {R : Type u_1} {E : Type u_2} (v u : R) (P Q : E → Prop) (r : E → E → Prop) (n m : ℕ) (A : Ty) : ¬HasType (LF.pseudoCumulative v u P Q r n m) A

(46) has no type, since its object's cardinality test forces the scope of Mv to type T.

def Charlow2021.LF.denote {R : Type u_1} {E : Type u_2} {S : Type u_3} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] [Fintype E] : LF R E → DynamicSemantics.Update S

K.denote is the update that the logical form K denotes.

Equations

• (Charlow2021.LF.dref v P).denote = Charlow2021.Evar v P
• (Charlow2021.LF.max v K).denote = DynamicSemantics.Update.maxAt v K.denote
• (Charlow2021.LF.card v n).denote = Charlow2021.card v n
• (Charlow2021.LF.rel u v r).denote = Charlow2021.relTest u v r
• (K.seq L).denote = SetRel.comp K.denote L.denote

theorem Charlow2021.denote_cumulative {R : Type u_1} {E : Type u_2} (v u : R) (P Q : E → Prop) (r : E → E → Prop) (n m : ℕ) {S : Type u_3} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] [Fintype E] : (LF.cumulative v u P Q r n m).denote = cumulative v u P Q r n m

theorem Charlow2021.denote_pseudoCumulative {R : Type u_1} {E : Type u_2} (v u : R) (P Q : E → Prop) (r : E → E → Prop) (n m : ℕ) {S : Type u_3} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] [Fintype E] : (LF.pseudoCumulative v u P Q r n m).denote = pseudoCumulative v u P Q r n m

Post-suppositions (§5, Appendix B)

@[reducible, inline]

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

A post-suppositional meaning (52) is a computation of the Writer monad over the update monoid, whose log is its post-supposition; pure and bind are (120) and (121), the unit being the dynamic tautology T of (15).

Equations

• Charlow2021.PostSupp S = Writer (DynamicSemantics.Update S)

def Charlow2021.exactlyPS {R S : Type u} {E : Type u_1} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] [Fintype E] (v : R) (n : ℕ) (P : E → Prop) : PostSupp S (Cont (DynamicSemantics.Update S) R)

exactlyPS v n P is the post-suppositional modified numeral (53), whose cardinality test is post-supposed.

Equations

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

def Charlow2021.sentencePS {R S : Type u} {E : Type u_1} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] [Fintype E] (v u : R) (P Q : E → Prop) (r : E → E → Prop) (n m : ℕ) : PostSupp S (DynamicSemantics.Update S)

sentencePS is the sentence (55), composed by Combine⁺, which is the Writer monad's <*> (122).

Equations

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

def Charlow2021.PostSupp.reify {S : Type u} (p : PostSupp S (DynamicSemantics.Update S)) : DynamicSemantics.Update S

Reification (58) conjoins a meaning with its post-supposition.

Equations

• p.reify = SetRel.comp (Writer.val p) (Writer.log p)

theorem Charlow2021.val_sentencePS {R S : Type u} {E : Type u_1} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] [Fintype E] (v u : R) (P Q : E → Prop) (r : E → E → Prop) (n m : ℕ) : Writer.val (sentencePS v u P Q r n m) = DynamicSemantics.Update.maxAt v (SetRel.comp (Evar v P) (DynamicSemantics.Update.maxAt u (SetRel.comp (Evar u Q) (relTest u v r))))

theorem Charlow2021.log_sentencePS {R S : Type u} {E : Type u_1} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] [Fintype E] (v u : R) (P Q : E → Prop) (r : E → E → Prop) (n m : ℕ) : Writer.log (sentencePS v u P Q r n m) = SetRel.comp (card v n) (card u m)

theorem Charlow2021.reify_sentencePS {R S : Type u} {E : Type u_1} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] [Fintype E] (v u : R) (P Q : E → Prop) (r : E → E → Prop) (n m : ℕ) : (sentencePS v u P Q r n m).reify = cumulative v u P Q r n m

Reifying (55) gives (57), which is the cumulative (6).

Update semantics (§6)

def Charlow2021.maxAtU {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] (v : R) (K : DynamicSemantics.CCP S) : DynamicSemantics.CCP S

Update-theoretic maximization (78) keeps the outputs whose value of v is maximal in the whole updated context.

Equations

• Charlow2021.maxAtU v K s = {j : S | j ∈ K s ∧ ∀ h ∈ K s, ¬DynamicSemantics.RegisterStructure.val v j < DynamicSemantics.RegisterStructure.val v h}

theorem Charlow2021.lower_maxAtU_image {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] (v : R) (D : DynamicSemantics.Update S) : (maxAtU v (SetRel.image D)).lower = DynamicSemantics.Update.maxAt v D

Pointwise maximization is update-theoretic maximization on a singleton (79).

def Charlow2021.exactlyU {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] [Fintype E] (v : R) (n : ℕ) (P : E → Prop) : Cont (DynamicSemantics.CCP S) R

exactlyU v n P is the update-theoretic modified numeral (81), of the same form as (3).

Equations

• Charlow2021.exactlyU v n P k = (Charlow2021.maxAtU v (DynamicSemantics.CCP.seq (SetRel.image (Charlow2021.Evar v P)) (k v))).seq (SetRel.image (Charlow2021.card v n))

def Charlow2021.sentenceU {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] [Fintype E] (v u : R) (P Q : E → Prop) (r : E → E → Prop) (n m : ℕ) : DynamicSemantics.CCP S

sentenceU is the sentence (82), with the quantifiers in surface scope.

Equations

• Charlow2021.sentenceU v u P Q r n m = Charlow2021.exactlyU v n P fun (a : R) => Charlow2021.exactlyU u m Q fun (b : R) => SetRel.image (Charlow2021.relTest b a r)

def Charlow2021.sentenceULowered {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] [Fintype E] (v u : R) (P Q : E → Prop) (r : E → E → Prop) (n m : ℕ) : DynamicSemantics.CCP S

sentenceULowered is (82) with the object's maximization replaced by the lift of its pointwise counterpart (p. 34).

Equations

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

theorem Charlow2021.down_sentenceULowered {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] [PartialOrder E] [Fintype E] (v u : R) (P Q : E → Prop) (r : E → E → Prop) (n m : ℕ) : (sentenceULowered v u P Q r n m).down = SetRel.dom (pseudoCumulative v u P Q r n m)

Lifting the object's maximization from its pointwise counterpart brings back the pseudo-cumulative reading (p. 34).

The models of Figure 1

inductive Charlow2021.Ent : Type

Ent has the atoms of Figure 1, four boys and six movies.

• b1 : Ent
• b2 : Ent
• b3 : Ent
• b4 : Ent
• m1 : Ent
• m2 : Ent
• m3 : Ent
• m4 : Ent
• m5 : Ent
• m6 : Ent

@[instance_reducible]

instance Charlow2021.instDecidableEqEnt : DecidableEq Ent

Equations

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

@[instance_reducible]

instance Charlow2021.instFintypeEnt : Fintype Ent

Equations

• Charlow2021.instFintypeEnt = { elems := { val := ↑Charlow2021.Ent.enumList, nodup := Charlow2021.Ent.enumList_nodup }, complete := Charlow2021.instFintypeEnt._proof_1 }

inductive Charlow2021.Reg : Type

Reg has the two registers, v for boys and u for movies.

• u : Reg
• v : Reg

@[instance_reducible]

instance Charlow2021.instDecidableEqReg : DecidableEq Reg

Equations

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

structure Charlow2021.Scenario : Type

A scenario of Figure 1 gives the boys, the movies, and who saw what.

• boys : Finset Ent
• movies : Finset Ent
• sees : Finset (Ent × Ent)

def Charlow2021.Scenario.Boys (σ : Scenario) (X : Finset Ent) : Prop

σ.Boys X says that X is a plurality of boys.

Equations

• σ.Boys X = (X.Nonempty ∧ X ⊆ σ.boys)

def Charlow2021.Scenario.Movies (σ : Scenario) (Y : Finset Ent) : Prop

σ.Movies Y says that Y is a plurality of movies.

Equations

• σ.Movies Y = (Y.Nonempty ∧ Y ⊆ σ.movies)

def Charlow2021.Scenario.Saw (σ : Scenario) (Y X : Finset Ent) : Prop

σ.Saw Y X is the cumulative closure of seeing, object first, so that every boy in X saw a movie in Y and every movie in Y was seen by a boy in X.

Equations

• σ.Saw Y X = Set.LiftRel (fun (b m : Charlow2021.Ent) => (b, m) ∈ σ.sees) ↑X ↑Y

def Charlow2021.Scenario.seen (σ : Scenario) (X : Finset Ent) : Finset Ent

σ.seen X is the set of movies that some boy in X saw.

Equations

• σ.seen X = {m ∈ σ.movies | ∃ b ∈ X, (b, m) ∈ σ.sees}

def Charlow2021.Scenario.WellFormed (σ : Scenario) : Prop

Every seeing is of a movie by a boy.

Equations

• σ.WellFormed = (σ.sees ⊆ σ.boys ×ˢ σ.movies)

def Charlow2021.Scenario.Total (σ : Scenario) : Prop

Every boy saw some movie.

Equations

• σ.Total = ∀ b ∈ σ.boys, ∃ (m : Charlow2021.Ent), (b, m) ∈ σ.sees

def Charlow2021.Scenario.swap (σ : Scenario) : Scenario

σ.swap exchanges the roles of boys and movies.

Equations

• σ.swap = { boys := σ.movies, movies := σ.boys, sees := Finset.image Prod.swap σ.sees }

@[instance_reducible]

instance Charlow2021.Scenario.instDecidableWellFormed (σ : Scenario) : Decidable σ.WellFormed

Equations

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

@[instance_reducible]

instance Charlow2021.Scenario.instDecidableTotal (σ : Scenario) : Decidable σ.Total

Equations

• σ.instDecidableTotal = { decide := decide (∀ a ∈ Finset.univ, (fun (b : Charlow2021.Ent) => b ∈ σ.boys → ∃ (m : Charlow2021.Ent), (b, m) ∈ σ.sees) a), reflects_decide := ⋯ }

@[instance_reducible]

instance Charlow2021.Scenario.instDecidablePredFinsetEntBoys (σ : Scenario) : DecidablePred σ.Boys

Equations

• σ.instDecidablePredFinsetEntBoys x✝ = { decide := decide x✝.Nonempty && decide (x✝ ⊆ σ.boys), reflects_decide := ⋯ }

theorem Charlow2021.Scenario.mem_swap_sees {σ : Scenario} {x y : Ent} : (x, y) ∈ σ.swap.sees ↔ (y, x) ∈ σ.sees

theorem Charlow2021.Scenario.swap_saw {σ : Scenario} : σ.swap.Saw = flip σ.Saw

theorem Charlow2021.Scenario.subset_seen {σ : Scenario} {X Y : Finset Ent} (hY : Y ⊆ σ.movies) (h : σ.Saw Y X) : Y ⊆ σ.seen X

theorem Charlow2021.Scenario.saw_seen {σ : Scenario} (hw : σ.WellFormed) (ht : σ.Total) {X : Finset Ent} (hX : X ⊆ σ.boys) : σ.Saw (σ.seen X) X

theorem Charlow2021.Scenario.movies_seen {σ : Scenario} (hw : σ.WellFormed) (ht : σ.Total) {X : Finset Ent} (hX : σ.Boys X) : σ.Movies (σ.seen X)

theorem Charlow2021.Scenario.maximal_saw_iff {σ : Scenario} (hw : σ.WellFormed) (ht : σ.Total) {X Y : Finset Ent} (hX : σ.Boys X) : Maximal (fun (Y : Finset Ent) => σ.Movies Y ∧ σ.Saw Y X) Y ↔ Y = σ.seen X

The movies some boys saw are the greatest plurality they saw.

theorem Charlow2021.Scenario.maximal_boys_iff {σ : Scenario} (hne : σ.boys.Nonempty) {X : Finset Ent} : Maximal σ.Boys X ↔ X = σ.boys

def Charlow2021.scenarioA : Scenario

Scenario A of Figure 1 has three boys who saw five movies.

Equations

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

def Charlow2021.scenarioB : Scenario

Scenario B of Figure 1 adds to Scenario A a fourth boy, who saw a sixth movie.

Equations

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

@[reducible, inline]

abbrev Charlow2021.St : Type

An assignment gives each register a plurality.

Equations

• Charlow2021.St = (Charlow2021.Reg → Finset Charlow2021.Ent)

theorem Charlow2021.atomCount_eq_card {α : Type u_1} [Fintype α] [DecidableEq α] (X : Finset α) : Mereology.atomCount (Finset α) X = X.card

Pluralities are finite sets of atoms, which # counts (§2.1).

theorem Charlow2021.mem_maxAt_object {σ : Scenario} {a b : Reg} (hab : a ≠ b) (hw : σ.WellFormed) (ht : σ.Total) {X : Finset Ent} (hX : σ.Boys X) {i k : St} : (Function.update i a X, k) ∈ DynamicSemantics.Update.maxAt b (SetRel.comp (Evar b σ.Movies) (relTest b a σ.Saw)) ↔ k = Function.update (Function.update i a X) b (σ.seen X)

The object's maximization stores the movies the subject's boys saw.

theorem Charlow2021.fixes_maxAt_object {σ : Scenario} {a b : Reg} (hab : a ≠ b) : DynamicSemantics.Update.Fixes a (DynamicSemantics.Update.maxAt b (SetRel.comp (Evar b σ.Movies) (relTest b a σ.Saw)))

theorem Charlow2021.update_update_apply {a b : Reg} (hab : a ≠ b) (i : St) (X Y : Finset Ent) : Function.update (Function.update i a X) b Y a = X

theorem Charlow2021.mem_dom_cumulative {σ : Scenario} {a b : Reg} (hab : a ≠ b) (hw : σ.WellFormed) (ht : σ.Total) (hne : σ.boys.Nonempty) (n m : ℕ) (i : St) : i ∈ SetRel.dom (cumulative a b σ.Boys σ.Movies σ.Saw n m) ↔ (σ.seen σ.boys).card = m ∧ σ.boys.card = n

(6) is true exactly when all the boys are n and the movies they saw m.

theorem Charlow2021.mem_dom_pseudoCumulative {σ : Scenario} {a b : Reg} (hab : a ≠ b) (hw : σ.WellFormed) (ht : σ.Total) (n m : ℕ) (i : St) : i ∈ SetRel.dom (pseudoCumulative a b σ.Boys σ.Movies σ.Saw n m) ↔ ∃ (X : Finset Ent), Maximal (fun (X : Finset Ent) => σ.Boys X ∧ (σ.seen X).card = m) X ∧ X.card = n

(5) is true exactly when some maximal plurality of boys who saw m movies is n boys.

theorem Charlow2021.seen_mono {σ : Scenario} {X X' : Finset Ent} (h : X ⊆ X') : σ.seen X ⊆ σ.seen X'

theorem Charlow2021.mem_image_Evar {r : Reg} {P : Finset Ent → Prop} {s : Set St} {j : St} : j ∈ SetRel.image (Evar r P) s ↔ ∃ i ∈ s, ∃ (x : Finset Ent), P x ∧ j = Function.update i r x

theorem Charlow2021.mem_object_context {σ : Scenario} {i j : St} : j ∈ DynamicSemantics.CCP.seq (SetRel.image (Evar Reg.u σ.Movies)) (SetRel.image (relTest Reg.u Reg.v σ.Saw)) (SetRel.image (Evar Reg.v σ.Boys) {i}) ↔ ∃ (X : Finset Ent) (Y : Finset Ent), σ.Boys X ∧ σ.Movies Y ∧ σ.Saw Y X ∧ j = Function.update (Function.update i Reg.v X) Reg.u Y

After the subject's dref and the object's dref and verb, the context holds every pair of boys and movies they saw.

theorem Charlow2021.mem_maxAtU_object {σ : Scenario} (hw : σ.WellFormed) (ht : σ.Total) (hne : σ.boys.Nonempty) {i j : St} : j ∈ maxAtU Reg.u (DynamicSemantics.CCP.seq (SetRel.image (Evar Reg.u σ.Movies)) (SetRel.image (relTest Reg.u Reg.v σ.Saw))) (SetRel.image (Evar Reg.v σ.Boys) {i}) ↔ ∃ (X : Finset Ent), σ.Boys X ∧ σ.Saw (σ.seen σ.boys) X ∧ j = Function.update (Function.update i Reg.v X) Reg.u (σ.seen σ.boys)

Update-theoretic maximization of the object keeps the movies seen by all the boys.

theorem Charlow2021.mem_down_sentenceU {σ : Scenario} (hw : σ.WellFormed) (ht : σ.Total) (hne : σ.boys.Nonempty) (n m : ℕ) (i : St) : i ∈ (sentenceU Reg.v Reg.u σ.Boys σ.Movies σ.Saw n m).down ↔ (σ.seen σ.boys).card = m ∧ σ.boys.card = n

(82) is true exactly when all the boys are n and the movies they saw m, so it has the cumulative reading (§6.2).

theorem Charlow2021.scenarioA_wellFormed : scenarioA.WellFormed

theorem Charlow2021.scenarioB_wellFormed : scenarioB.WellFormed

theorem Charlow2021.scenarioA_total : scenarioA.Total

theorem Charlow2021.scenarioB_total : scenarioB.Total

theorem Charlow2021.scenarioA_swap_wellFormed : scenarioA.swap.WellFormed

theorem Charlow2021.scenarioB_swap_wellFormed : scenarioB.swap.WellFormed

theorem Charlow2021.scenarioA_swap_total : scenarioA.swap.Total

theorem Charlow2021.scenarioB_swap_total : scenarioB.swap.Total

theorem Charlow2021.cumulative_scenarioA (i : St) : i ∈ SetRel.dom (cumulative Reg.v Reg.u scenarioA.Boys scenarioA.Movies scenarioA.Saw 3 5)

The cumulative (6) is true in Scenario A (§1.3).

theorem Charlow2021.cumulative_scenarioB (i : St) : i ∉ SetRel.dom (cumulative Reg.v Reg.u scenarioB.Boys scenarioB.Movies scenarioB.Saw 3 5)

The cumulative (6) is false in Scenario B (§1.3).

theorem Charlow2021.pseudoCumulative_scenarioA (i : St) : i ∈ SetRel.dom (pseudoCumulative Reg.v Reg.u scenarioA.Boys scenarioA.Movies scenarioA.Saw 3 5)

The pseudo-cumulative (5) is true in Scenario A as well (§1.1).

theorem Charlow2021.maximal_b123 : Maximal (fun (X : Finset Ent) => scenarioB.Boys X ∧ (scenarioB.seen X).card = 5) {Ent.b1, Ent.b2, Ent.b3}

Of the boys of Scenario B who saw exactly five movies, b1 ⊔ b2 ⊔ b3 is maximal.

theorem Charlow2021.pseudoCumulative_scenarioB (i : St) : i ∈ SetRel.dom (pseudoCumulative Reg.v Reg.u scenarioB.Boys scenarioB.Movies scenarioB.Saw 3 5)

The pseudo-cumulative (5) is true in Scenario B (§2.3).

theorem Charlow2021.cumulative_swap_scenarioA (i : St) : i ∈ SetRel.dom (cumulative Reg.u Reg.v scenarioA.Movies scenarioA.Boys (flip scenarioA.Saw) 5 3)

The scopings (28) and (30) agree with (6) in Scenario A.

theorem Charlow2021.cumulative_swap_scenarioB (i : St) : i ∉ SetRel.dom (cumulative Reg.u Reg.v scenarioB.Movies scenarioB.Boys (flip scenarioB.Saw) 5 3)

The scopings (28) and (30) agree with (6) in Scenario B.

theorem Charlow2021.maximal_m12345 : Maximal (fun (Y : Finset Ent) => scenarioB.swap.Boys Y ∧ (scenarioB.swap.seen Y).card = 3) {Ent.m1, Ent.m2, Ent.m3, Ent.m4, Ent.m5}

Of the movies of Scenario B seen by exactly three boys, m1 ⊔ ⋯ ⊔ m5 is maximal.

theorem Charlow2021.pseudoCumulative_swap_scenarioB (i : St) : i ∈ SetRel.dom (pseudoCumulative Reg.u Reg.v scenarioB.Movies scenarioB.Boys (flip scenarioB.Saw) 5 3)

The scoping (33) is pseudo-cumulative, and true in Scenario B.

theorem Charlow2021.sentenceU_scenarioA (i : St) : i ∈ (sentenceU Reg.v Reg.u scenarioA.Boys scenarioA.Movies scenarioA.Saw 3 5).down

(82) is true in Scenario A.

theorem Charlow2021.sentenceU_scenarioB (i : St) : i ∉ (sentenceU Reg.v Reg.u scenarioB.Boys scenarioB.Movies scenarioB.Saw 3 5).down

(82) is false in Scenario B, though it has the form of the pseudo-cumulative (5).

theorem Charlow2021.not_isDistributive_maxAtU : ¬(maxAtU Reg.u (DynamicSemantics.CCP.seq (SetRel.image (Evar Reg.u scenarioB.Movies)) (SetRel.image (relTest Reg.u Reg.v scenarioB.Saw)))).IsDistributive

Update-theoretic maximization is not distributive, since otherwise it would be the lift of its pointwise counterpart, and (82) would be true in Scenario B (§6.2).