feat(Composition): add the chapter from CSwFP/7.1–7.6

Bib.lean

@@ -153,4 +153,22 @@ def FAA2025 : Article where
   number  := inlines!""
   url     := "https://github.com/sorrachai/FAA2025"
 
+def mostowski1957 : Article where
+  title   := inlines!"On a generalization of quantifiers"
+  authors := #[inlines!"Andrzej Mostowski"]
+  journal := inlines!"Fundamenta Mathematicae"
+  year    := 1957
+  month   := none
+  volume  := inlines!"44"
+  number  := inlines!""
+
+def barwise1981 : Article where
+  title   := inlines!"Generalized quantifiers and natural language"
+  authors := #[inlines!"Jon Barwise", inlines!"Robin Cooper"]
+  journal := inlines!"Linguistics and Philosophy"
+  year    := 1981
+  month   := none
+  volume  := inlines!"4"
+  number  := inlines!""
+
 end Bib

Book.lean

@@ -9,6 +9,7 @@ import CSwL.SeaBattle
 import CSwL.Morphology
 import CSwL.InfEngine
 import CSwL.ModelChecking
+import CSwL.Composition
 
 import VersoManual
 
@@ -35,3 +36,4 @@ set_option verso.code.warnLineLength 80
 {include CSwL.Morphology}
 {include CSwL.InfEngine}
 {include CSwL.ModelChecking}
+{include CSwL.Composition}

CSwFP.yaml

@@ -129,6 +129,36 @@ exercises:
     6.6 (p. 146): TODO, goes with 6.5 to Logic/FOL
     6.7 (p. 147): check-sentence
 
+  CSwFP/7:
+    7.1 (p. 158): tree-of-numbers
+    7.2 (p. 158): tree-patterns
+    7.3 (p. 158): gen-tree
+    7.4 (p. 161): symm-pattern
+    7.5 (p. 161): turned into a quiz
+    7.6 (p. 161): turned into a quiz
+    7.7 (p. 162): mon-not
+    7.8 (p. 162): mon-and
+    7.9 (p. 162): mon-or
+    7.10 (p. 162): mon-up-down
+    7.11 (p. 163): deferred with the automata (issue 41)
+    7.12 (p. 164): deferred with the automata (issue 41)
+    7.13 (p. 165): dropped with 7.3
+    7.14 (p. 165): dropped with 7.3
+    7.15 (p. 166): dropped with 7.3
+    7.16 (p. 166): dropped with 7.3
+    7.17 (p. 166): dropped with 7.3
+    7.18 (p. 166): dropped with 7.3
+    7.19 (p. 168): dropped with 7.3
+    7.20 (p. 170): dropped with 7.4
+    7.21 (p. 170): dropped with 7.4
+    7.22 (p. 172): dropped with 7.4
+    7.23 (p. 173): dropped with 7.4
+    7.24 (p. 175): snow-white-helped
+    7.25 (p. 179): at-least-at-most
+    7.26 (p. 180): deferred with 7.7 (issue 43)
+    7.27 (p. 181): deferred with 7.7 (issue 43)
+    7.28 (p. 182): deferred with 7.7 (issue 43)
+
 original:
   IntroL.lean: [sum-of-squares, sum-to, sum-list, count-zeros]
   Logic/Proof.lean:
@@ -160,6 +190,21 @@ original:
   Morphology/Phonemes.lean: [append-suffix-text]
   Morphology/SwedishPlural.lean: [swedish-plural]
   InfEngine.lean: [inconsistent-kb, ferio]
+  Composition/Quantification.lean:
+    - at-most-two     # from the prose on "At least two A are B" in 7.2
+    - at-least-n      # from the prose on "at least n" and "at most m" in 7.2
+    - subalternation  # from the prose on existential presuppositions in 7.2
+    - no-cons         # from the prose on CONS in 7.2
+    - only-not-cons   # from the prose on (7.8), "Only dwarfs sing during work"
+    - many-not-ext    # from the prose on EXT in 7.2, "many in the sense of relatively many"
+    - the-quant       # from the prose on ISOM in 7.2 and the Russellian `the` of 7.5
+    - poss-not-isom   # from the prose on ISOM in 7.2: EXT and CONS do not imply ISOM
+    - some-not-refl   # from the prose on reflexive quantifiers in 7.2
+    - no-mon-down     # from the prose on MON↓ in 7.2
+    - even-not-mon    # from the prose on "an even number of" in 7.2, neither MON↑ nor MON↓
+    - left-mon-pattern # from the prose on ↑MON and ↓MON in 7.2, "left to the reader"
+    - lang-and-or     # from the prose on quantifier automata in 7.2
+    - all-kstar       # from the prose in 7.2, "all corresponds to the regular language 1∗"
 
 depends:
   bangu-proof: bangu-form
@@ -267,7 +312,29 @@ sections:
         `[0..]` becomes a theorem, since Lean is not lazy.
     6.6 Further Reading: omitted
 
-  CSwFP/7 The Composition of Meaning in Natural Language: not yet taken up
+  CSwFP/7:
+    7.1 Rules of the Game: Composition
+    7.2 Quantification:
+      to: Composition
+      why: TODO, its Aristotle-to-Frege opening retells what InfEngine
+        already presents with the syllogisms.
+    7.3 The Language of Typed Logic and Its Semantics:
+      to: dropped
+      why: Lean is the typed logic. Its types, lambda terms, application and
+        evaluation are what IntroL presents with the lambda calculus of 2.4,
+        and the semantics of 7.3 is Lean's own evaluation.
+    7.4 Reducing Expressions of Typed Logic:
+      to: dropped
+      why: Lean reduces and substitutes for the reader, and no later section
+        handles terms as data. CSLib's lambda calculi do not fit, since the named
+        one is untyped, and the typed one is locally nameless.
+    7.5 Typed Meanings for Natural Language: Composition
+    7.6 Implementing Semantic Interpretation: Composition
+    7.7 Handling Ambiguity:
+      to: deferred
+      why: its benefit is unclear for now, and the implementation within
+        reach looked of little use (issue 43).
+    7.8 Further Reading: omitted
   CSwFP/8 Extension and Intension: not yet taken up
   CSwFP/9 Parsing: not yet taken up
   CSwFP/10 Handling Relations and Scoping: not yet taken up

CSwL/Composition.lean

@@ -0,0 +1,73 @@
+import CSwLMeta
+import Bib
+import CSwL.ModelChecking
+import Mathlib.Data.Set.Function
+import Mathlib.Data.Set.Card
+import Mathlib.Computability.Language
+import CSwL.Composition.Rules
+import CSwL.Composition.Quantification
+import CSwL.Composition.TypedMeanings
+import CSwL.Composition.Interpretation
+
+open Verso.Genre Manual
+open CSwLMeta
+
+#doc (Manual) "A composição do significado na língua natural" =>
+%%%
+tag := "Composition"
+file := "Composition"
+%%%
+
+:::dev NOW
+Plan. The headings follow CSwFP/7.1–7.6, without 7.3 and 7.4 (7.7 is
+deferred, issue 43; 7.8, further reading, is omitted).
+Sections are written `terse` first (see `STYLE-CODE.md`). Code comes in the
+section that presents each idea, not only in 7.6:
+
+- 7.2: `every` and `a` (also `some`, `no`, `most`) as relations between
+  predicates; EXT, CONS and ISOM as `Prop`s over `Set`; the tree of numbers
+  and the numeric quantifiers; ex. 7.7–7.10 as monotonicity theorems; ex.
+  7.11 with Mathlib's `DFA` (optional).
+- 7.3 and 7.4 are dropped (see `CSwFP.yaml`): Lean's types are the typed
+  logic (`Entity` for e, `Bool` for t), and Lean does the reductions. No
+  deep embedding, since CSwFP/8 needs intensional types.
+- 7.5: the semantic rules as Lean functions. Its opening says in a few
+  lines that e is `Entity` and t is `Bool`.
+- 7.6: `intSent` and friends over `ModelChecking`'s `Sent`, with `intDET`
+  built from the 7.2 definitions; a theorem that the direct interpretation
+  agrees with `checkSentence`, if it turns out feasible.
+- 7.7: deferred (issue 43).
+
+The chapter's key point for the cues: direct interpretation admits
+quantifiers, such as *most*, that first-order logic cannot express.
+
+A first draft translation of the chapter opening, 7.1 and 7.2 up to the
+conditions on quantifier relations is in commits `76821ee` and `95047b3`.
+:::
+
+:::terse
+- Em {ref "ModelChecking"}[Verificação de modelos com lógica de primeira
+  ordem] o caminho era indireto: sentença, depois fórmula, depois avaliação no
+  modelo.
+- Agora o caminho é direto: cada expressão da língua é ligada ao modelo, sem
+  fórmula intermediária.
+- Os modelos da lógica de predicados se estendem à lógica tipada, que dá os
+  significados das palavras e o modo de compô-los.
+- O ganho central: quantificadores como *most*, que a lógica de primeira ordem
+  não exprime, passam a ter interpretação direta.
+:::
+
+::::full
+:::dev BeforeNextRelease
+TODO: translate the CSwFP/7 summary, with Lean in place of Haskell as the
+lambda-calculus engine of `ModelChecking`.
+:::
+::::
+
+{include 1 CSwL.Composition.Rules}
+
+{include 1 CSwL.Composition.Quantification}
+
+{include 1 CSwL.Composition.TypedMeanings}
+
+{include 1 CSwL.Composition.Interpretation}