[arademaker]

The chapter had been reduced to a skeleton of four headings. It now has the four sections, in the order the headings fix: linguistic form and translation into logic (6.1), the fragment of English (4.2), predicate logic as representation language (6.2), and the model together with evaluation in it (6.3 and 6.4). The order is forced, since 6.2 translates the 4.2 grammar category by category.

The fragment is Sent, NP, RCN and VP in one mutual block over the lexical categories, with ToString for the surface string. The translation is lfSent, lfNP, lfVP and lfRCN, with lfDET building a fresh bound variable and Russell's analysis for the definite article. The model is the fairy-tale structure over A–Z and Unspec, and evaluation reuses Interp, FInterp, Assign and Formula.eval from Logic/FOL.lean rather than restating them. The chapter closes by spending mem_entities as the hdom of Formula.eval_iff_denote, so checkSentence's Bool and the proposition the sentence states are shown to agree.

Six exercises, all rated 2: preposition-phrase, complex-relative- clauses, fragment-translations, check-sentence, help-defeat and reflexive-ditransitive.

Decisions that depart from the source, all recorded in DEVIATIONS.md:

• A grammar is extended by declaring a category that contains the old one, not by redeclaring the mutual group. Adding a word still needs a new constructor, so the lexicon is complete from the declaration and CSwFP/4.6 is absorbed into the presentation.
• most is out of DET, because it has no first-order translation and a Lean function has to be total. AV, To, INF and TINF are out for the same reason and because CSwFP/6 never translates them.
• Constructors are named after the rules they implement — npDet, rcnSubj, rcnObj, vpTrans — not NP1, RCN1, VP1.
• adjective-types and the categorial section it belonged to are gone; 6.1 makes the same point about type raising.

Bib.lean gains Carroll and Russell. PROVENANCE.md gains the chapter's table and drops feature-value, withdrawn in the previous commit. STYLE-CODE.md records that the pattern-matching fun reaches ordinary code here.

The generated student project builds.

AI-usage disclosure: this chapter was drafted with the assistance of Claude Opus 5 (Anthropic, September 2026, via Claude Code). The assistant read the source material, chose the encoding of the grammar and its extensions, wrote the Lean definitions, exercises and proofs, drafted the Portuguese prose as a translation of the source, and updated the project's records. The author takes full responsibility for the final content. To be manually revised yet.

Update before merging

• The chapter is renamed English → ModelChecking ("Verificação de modelos com lógica de primeira ordem"), following CSwFP's chapter title, since the whole book is about English. Tag, namespace, Book.lean, the ledger in STYLE-CODE.md, CSwFP.yaml (which replaced PROVENANCE.md on main), DEVIATIONS.md and README.md follow.
• The branch is merged with main (Lean v4.35.0, allowNonModules); the book and the student and solutions variants build.
• The review of the chapter is not finished and continues in Revise ModelChecking.lean #15, which stays open. Merged now so that CSwFP/7, which builds on this fragment and model, can start from main.

[Copilot]

Copilot review overview

🟡 Changes recommended

The PR leaves a stale README reference and introduces spelling and code-comment language issues.

Get a fresh assessment by requesting another Copilot review.

Review effort: Lite
Findings: 3

Open (3)

• Correct misspelling of guillemets · New
• Translate Portuguese code comments into English · New
• Update README chapter list to remove nonexistent ModelChecking.lean · New

What changed in this PR

Expands English.lean from a skeleton into the English-fragment chapter, including grammar, translations, model evaluation, and exercises.

Changes:

• Added grammar, FOL translation, fairy-tale model, evaluation, and six exercises.
• Updated provenance, deviations, and Lean style records.
• Added Carroll and Russell bibliography entries.

File	Description
CSwL/​English.lean	New chapter content and exercises
DEVIATIONS.md	Updated chapter placement and design decisions
PROVENANCE.md	Added exercise provenance and counts
STYLE-CODE.md	Recorded newly introduced Lean syntax
Bib.lean	Added bibliography entries

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[HenriqueBorges6]

Part 1 Review: Chapter Framing & Section 8.1 (Linguistic Forms and Logic Translations)

The review process began with an independent reading and note-taking pass, followed by a collaborative session with Gemini 3.8 Flash to audit these notes and consolidate actionable comments and suggestions. The AI assistant was also used for investigative tasks, such as tracing prerequisite concepts introduced across earlier chapters and clarifying the author's pedagogical intent.

[HenriqueBorges6]

The sentence "A tradução lógica de (1) não revela nenhum constituinte correspondente ao sintagma nominal quantificado que faz de sujeito" condenses four technical linguistic concepts (constituinte, sintagma nominal, quantificado, faz de sujeito) into a single clause without any prior definition in the book (Chapters 1–7 never introduced Noun Phrases or syntactic constituents).

For students without a formal background in linguistics, this creates an unnecessary barrier to understanding what is otherwise a straightforward and fascinating observation: that while "Every dwarf" forms a unified syntactic block (a sub-tree / constituent) in natural language, its FOL translation dismantles that block across the entire formula (into a quantifier ∀x, a conditional premise Dwarf x → ..., and a bound variable x).

Introducing the notion of a Noun Phrase (NP) and contrasting the surface syntactic block with its dismantled representation in FOL makes the passage much more accessible and pedagogical.

Suggested change

	Os lógicos que usaram a lógica de predicados de primeira ordem para analisar a estrutura lógica da língua natural se impressionaram com o fato de que as traduções lógicas de sentenças com expressões quantificadas não pareciam acompanhar a estrutura linguística. Nas traduções lógicas, as expressões quantificadas pareciam ter desaparecido. A tradução lógica de (1) não revela nenhum constituinte correspondente ao sintagma nominal quantificado que faz de sujeito.
	1. Every dwarf loved Goldilocks.
	2. `∀x (Dwarf x → Love x g)`
	Em linguística, chamamos de _sintagma nominal_ (_Noun Phrase_, ou `NP`) qualquer bloco de palavras centrado em um substantivo que funcione como uma unidade sintática (como um sujeito ou objeto). Quando esse bloco é encabeçado por palavras lógicas como _every_ ("todo"), _some_ ("algum") ou _no_ ("nenhum"), temos um *sintagma nominal quantificado*.
	Ao tentar traduzir a língua natural para a lógica de predicados de primeira ordem, os lógicos notaram uma discrepância marcante: a fórmula lógica final não acompanhava a estrutura gramatical visível da oração. Considere o exemplo:
	1. _Every dwarf loved Goldilocks._ ("Todo anão amava Goldilocks.")
	2. `∀x (Dwarf x → Love x g)`
	Na oração original em inglês, _Every dwarf_ é o sujeito evidente da frase, formando um bloco sintático coeso. No entanto, na tradução formal (2), esse constituinte parece ter se dissolvido: não há nenhum símbolo único que corresponda a _every dwarf_. Em seu lugar, encontramos um quantificador universal `∀x`, uma implicação condicional e uma variável ligada `x`.

[HenriqueBorges6]

The original text explains Frege's observation in an overly abstract way ("uma expressão quantificada como every dwarf não dá origem a um conceito por si só") and includes a literal English blockquote about material implication.

Pedagogically, the key intuition is the loss of individual reference:

• Proper names like Alice or Goldilocks refer directly to specific individuals in the domain (mapped to logical constants like a or g).
• Quantified phrases like Every dwarf do not refer to any single individual. Instead of picking out an entity, the quantifier sets up a universal condition over the entire universe of discourse ("for any object x, if x is a dwarf, then x loved Goldilocks").

Because there is no concrete individual to point to, first-order logic cannot represent every dwarf as a standalone term: it is contextually eliminated, meaning its semantic contribution exists only as a global condition over the sentence. Explaining this contrast directly makes the logic crystal clear to the reader.

Suggested change

	Na tradução (2) o constituinte *every dwarf* desapareceu; ele foi contextualmente eliminado. Frege observa que uma expressão quantificada como *every dwarf* não dá origem a um conceito por si só, e só pode ser interpretada no contexto da tradução da sentença inteira. Considerando este exemplo em particular, a tradução literal de (2) seria:
	> All objects in the domain of discourse have the property of either not being dwarves or
	being objects who loved Goldilocks.
	Nessa reformulação da sentença (1), o sintagma *every dwarf* não ocorre mais.
	Essa discrepância decorre da perda de individualidade que o quantificador introduz. Se a sentença fosse _Alice loved Goldilocks_, o sujeito apontaria para uma pessoa específica no mundo, representada diretamente na lógica por uma constante individual `a` (resultando em `Love a g`).
	Contudo, ao dizermos _Every dwarf_, não estamos nos referindo a um anão em particular: não existe no mundo um indivíduo chamado "Todo anão". Em vez de apontar para uma entidade isolada, o quantificador estabelece uma condição geral sobre todos os objetos do universo: _para qualquer objeto x, se x for um anão, então x amou Goldilocks_ (o que equivale logicamente a dizer que ou esse objeto não é um anão, ou ele amou Goldilocks).
	É a isso que lógicos como Gottlob Frege chamavam de *eliminação contextual*: expressões quantificadas não denotam indivíduos e, por isso, deixam de existir como termos isolados na lógica de predicados. Seu significado só se manifesta na forma como condicionam a oração inteira.

[HenriqueBorges6]

This passage introduces higher-order typed semantics and Montague-style Type Raising (λP ↦ P g) to reconcile surface syntax with logical form, but encounters three pedagogical hurdles:

1. Missing conceptual bridge: While compositionality was introduced informally in IntroCS and basic lambda syntax on Nat was shown in IntroL ({ref "lambda"}), treating natural language constituents as higher-order typed lambdas and viewing β-reduction as semantic evaluation is completely new. Explicitly referencing {ref "IntroCS"} and {ref "lambda"} helps students connect the dots. (As a broader suggestion, IntroL could eventually include a minimal higher-order function example to pave the way for this).
2. Translation calque: The phrase "aplainam as aparências lógicas" is a literal calque of "smooth out logical appearances"; replacing it with "harmoniza a análise lógica" sounds natural in Portuguese.
3. Intuitive motivation for Type Raising: Without explaining why we invert the functional relationship (turning the subject into the caller and the predicate into the argument), λP ↦ P g appears arbitrary. Motivating it as a way to give proper names and quantifiers the exact same functional interface (Term → LF) → LF makes the mechanism click.

Suggested change

	As propriedades lógicas das sentenças que envolvem expressões quantificadas (e descrições, analisadas em termos de quantificadores) sugeriam, de fato, que o modo como um sintagma nominal simples, como um nome próprio, se combina com um predicado é logicamente diferente do modo como um sintagma nominal quantificado ou uma descrição definida se combina com um predicado. Isso levou à crença de que a forma linguística das expressões da língua natural era enganosa.
	A aplicação das ferramentas lógicas de abstração e redução do cálculo lambda nos permite ver que essa conclusão era injustificada. Traduzindo a língua natural em expressões de uma lógica tipada, veremos que os constituintes da língua natural correspondem a expressões tipadas que se combinam umas com as outras como funções e argumentos. Depois da redução completa dos resultados, as expressões quantificadas e outros constituintes podem ter sido contextualmente eliminados, mas essa eliminação é resultado do processo de redução, e não da suposta forma enganosa da sentença original. Assim, embora as traduções lógicas completamente reduzidas de sentenças da língua natural possam ser enganosas em algum sentido, as expressões originais, não reduzidas, não são.
	Como exemplo do modo como as ferramentas do cálculo lambda aplainam as aparências lógicas, considere a lógica da combinação de sujeitos e predicados. Nos casos mais simples — como *Goldilocks laughed* — poderíamos dizer que o predicado toma o sujeito como argumento. Mas isso não funciona para sujeitos quantificados, como em *no one laughed*. Tudo se resolve, porém, se dissermos que o sujeito sempre toma o predicado como seu argumento, e fizermos isso valer também para os sujeitos simples, elevando logicamente seu estatuto de argumento a função. Com expressões lambda isso é bastante fácil: traduzimos *Goldilocks* não como a constante `g`, e sim como a expressão `λP ↦ P g`. Essa expressão denota uma função de propriedades em valores de verdade, e pode portanto tomar a tradução de um predicado como argumento. A tradução de *no one* é do mesmo tipo `λP ↦ ¬∃x (Person x ∧ P x)`.
	Antes da redução, as traduções de *Goldilocks laughed* e de *no one laughed* se parecem muito. As semelhanças só desaparecem depois que as duas traduções são reduzidas às suas formas mais simples.
	Essa discrepância levou muitos lógicos do início do século XX a supor que a língua natural era inerentemente imperfeita ou enganosa. Contudo, o desenvolvimento da semântica formal por Richard Montague revelou que essa conclusão era precipitada.
	A chave para resolver esse impasse está em retomar o princípio da composicionalidade (visto em {ref "IntroCS"}[IntroCS]) sob a ótica do cálculo lambda (apresentado em {ref "lambda"}[IntroL]). Quando traduzimos a língua natural para uma lógica tipada, cada constituinte da oração corresponde a uma expressão funcional bem tipada. A combinação gramatical das palavras passa a refletir diretamente a aplicação de _funções aos seus argumentos_. O desaparecimento contextual dos quantificadores é simplesmente o resultado da computação dessas funções (a β-redução), e não uma falha estrutural da sentença original.
	Para ilustrar como o cálculo lambda harmoniza a análise lógica, considere a combinação de sujeitos e predicados:
	* Na sentença simples _Goldilocks laughed_, a intuição imediata da lógica de primeira ordem é tratar o predicado como a função que consome o sujeito: `Laughed(g)`.
	* No entanto, essa estratégia falha para sujeitos quantificados como _No one laughed_: não existe um indivíduo "ninguém" que possamos passar como argumento para `Laughed`.
	A solução elegante de Montague consiste em _inverter a relação funcional_ para todos os sujeitos (processo conhecido como *elevação de tipo*, ou _type raising_): em vez de o predicado consumir o sujeito, é o sujeito que consome o predicado como argumento!
	Com expressões lambda, isso se torna direto:
	1. O nome próprio _Goldilocks_ deixa de ser tratado como a constante individual `g` e passa a ser a função de ordem superior `λP ↦ P g`. Essa função recebe uma propriedade `P` e afirma que `g` tem essa propriedade.
	2. O sintagma quantificado _no one_ recebe exatamente a mesma assinatura de tipo: `λP ↦ ¬∃x (Person x ∧ P x)`, consumindo igualmente uma propriedade `P`.
	Assim, tanto _Goldilocks laughed_ quanto _no one laughed_ combinam-se sintática e semanticamente da mesma maneira: o sujeito aplica-se ao predicado. A aparente assimetria só ressurge quando efetuamos a β-redução para simplificar a fórmula lógica final.

[HenriqueBorges6]

In the original text, this closing paragraph outlined the roadmap of the remainder of the chapter (english-lf and english-model). With the chapter-level introductory framing added in Step 1, repeating that forward-looking summary here becomes redundant and introduces an inverted sequence (discussing Section 8.3 before 8.2).

Furthermore, the mention of "interpretar indiretamente" was left unelaborated. Reframing this paragraph achieves two key improvements:

1. It clarifies the notion of indirect interpretation (translating natural language into an intermediate formal logic whose semantics is already well-defined, rather than mapping English directly onto model structures).
2. It provides a natural narrative bridge into Section 8.2: to translate sentences into logical forms, our first concrete milestone is formally specifying the syntax of the fragment.

Suggested change

	Em {ref "english-lf"}[FOL como linguagem de representação] demonstramos isso construindo fórmulas da lógica de predicados como traduções das sentenças da língua natural geradas pelo fragmento de {ref "english-fragment"}[Um fragmento do inglês]. Essa tradução é o primeiro passo para interpretar indiretamente as expressões da língua natural. O passo seguinte, em {ref "english-model"}[Uma estrutura de primeira ordem], é atribuir às fórmulas da lógica de predicados um objeto modelo-teórico como denotação. Desse modo, a expressão da língua natural representada recebe uma interpretação modelo-teórica. No caminho, veremos as limitações desse procedimento.
	Esse método nos permite realizar a _interpretação indireta_ da língua natural: em vez de tentar avaliar sentenças em inglês diretamente em um modelo, nós as traduzimos primeiro para fórmulas da lógica de primeira ordem, cuja semântica formal já dominamos.
	Para que essa tradução composicional seja viável, porém, precisamos de um ponto de partida indispensável: delimitar a estrutura sintática das sentenças que queremos analisar. É a essa tarefa de modelagem gramatical que nos dedicamos a seguir em {ref "english-fragment"}[Um fragmento do inglês].