Repository navigation
Revise ModelChecking.lean #15
Description
The chapter is planned and listed in README.md as unwritten. English.lean
must first define Sent, NP, DET, CN, RCN, VP, TV, DV, ADJ
and That.
In CSwFP, Chapter 6 presents the transformation of the English fragment from Section 4.2 into FOL. Section 6.3 talks about a model for FOL, but this model is already specific for the vocabulary of Section 4.2. Section 6.4 talks about the intrepretation of the FOL formulas produced in 6.2 into the model presented in 6.3. Finally section 6.5 completes 6.4 with terms.
We need to reformulate this presentation. Complete present syntax/semantics/interpretation of FOL. CSwL/ModelChecking.lean the translation of English Syntax to FOL, a model for the result and the interpretation of the translation into the model, following what was done in FOL.lean.
We need to revise CSwL/FOL.lean, the semantics should not go to Prop. We need a MWE to bring the code from 6.4 and 6.5 to here.
The CSwL/English.lean will combine/adapt from sections CSwFP/4.2, CSwFP/5.6 and CSwFP/6.1, CSwFP/6.2 (especific to the vocabulary of CSwFP/6.1), and CSwFP/6.4 (specfic to the vocabulary of CSwFP/6.1).
Activity
[-]`ModelChecking.lean` does not exist[/-][+]Revise `English.lean`[/+][-]Revise `English.lean`[/-][+]Revise `ModelChecking.lean`[/+]arademaker commentedon Oct 19, 2026
PR #29 is being merged before the review is finished, and its review comments are still to be analysed. None of the threads was resolved; the links below stay valid after the merge.
Prose review of the chapter opening (HenriqueBorges6, review summary), all open:
ModelChecking.lean:18— the chapter has no high-level framing; proposes an opening.ModelChecking.lean:30— "constituinte", "sintagma nominal", "quantificado", "faz de sujeito" in one clause, none of them introduced before.ModelChecking.lean:36— Frege's observation is explained too abstractly; the key intuition is the loss of individual reference.ModelChecking.lean:44— type raising (λP ↦ P g) arrives without a conceptual bridge.ModelChecking.lean:46— the closing roadmap paragraph becomes redundant with a chapter-level introduction.Automated review (Copilot):
ModelChecking.lean.