Fol semantics model - #26
Merged
Merged
Conversation
arademaker
commented
Sep 19, 2026
arademaker
commented
Member
- Revise Logics presentation
- Revise exercises about Proofs, PL and FOL
Rename `PL.Form` to `PL.Formula`, so the propositional and first-order chapters name their syntax type alike; `FOL.Formula` was already so called, and the two now differ only in their namespace, which is what the chapters say about them. In `IntroL`, give the type-class section a worked instance: an `Angle` showing that `BEq` may need an implementation of its own rather than always arriving by `deriving`. The `BEq` / `DecidableEq` contrast that followed the old text stays, after the example instead of before it. Revise the `FOL` prose, and add the `wadler2003` bibliography entry for the pretty-printing paper behind the `Repr` instances.
Rewrite the explanations of the connective and quantifier rules, induction and function extensionality, avoiding fragmented sentences; record that rule in STYLE-WRITING and sharpen the English-identifiers rule in CLAUDE.md. The prose revisions were drafted with AI assistance and reviewed by a human before being committed.
Present the tactics `left` and `right` and the projections `Iff.mp` and `Iff.mpr` that the examples already use, correct the statements of `by_cases` and `by_contra`, and fix typos in the prose and in the new STYLE-WRITING rule. Reduce the `include` of the `vestidos` exercise to the six hypotheses the proof needs. These revisions were made in response to an AI-assisted review of the previous commit.
There was a problem hiding this comment.
Copilot review overview
🟡 Changes recommended
Feature-ordering violations and stale provenance and semantics documentation must be corrected.
Get a fresh assessment by requesting another Copilot review.
Review effort: Lite
Findings: 2
Open (11)
What changed in this PR
This PR revises the Proof, PL, and FOL chapters, adding richer semantics, exercises, and a graph diagram while updating project documentation.
Changes:
- Refines proof and propositional-logic exposition and exercises.
- Adds FOL terms, finite-model evaluation, structured-term semantics, and infinite-domain discussion.
- Updates style guidance, provenance, metadata, and citations.
| File | Description |
|---|---|
CSwL/Logic/Proof.lean |
Revises proof exposition and exercises. |
CSwL/Logic/PL.lean |
Refactors propositional formulas and semantics. |
CSwL/Logic/FOL.lean |
Expands FOL syntax, models, evaluation, and exercises. |
CSwLMeta/Diagrams.lean |
Adds the FOL graph diagram. |
CSwLMeta.lean |
Registers the diagram module. |
PROVENANCE.md |
Updates exercise provenance. |
STYLE-CODE.md |
Updates feature-order documentation. |
STYLE-WRITING.md |
Adds prose-style guidance. |
CSwL/IntroL.lean |
Expands equality and pretty-printing material. |
CSwL/Sets.lean |
Removes obsolete entity-collision documentation. |
CLAUDE.md |
Clarifies English code-comment conventions. |
Bib.lean |
Adds the Wadler citation. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
|
|
||
| ::::exercise (rating := 2) (name := "implies-list") | ||
| Estenda a checagem de implicação proposicional para o caso de uma lista de premissas. O tipo é `Form.impliesL : List Form → Form → Bool`. | ||
| Em todos os casos, para fechar ou não as provas, você só precisa da tática {tactic}`native_decide`. Note que quando existe consequência lógica, o tipo `Bool` pode ser promovido à `Prop` automaticamente pelo Lean, então você não precisa escrever `P.implies Q = true`, basta `P.imples Q`. Mas quando queremos mostrar que a consequência não é verdadeira, precisamos de `P.implies Q = false`. |
Comment on lines
+226
to
+230
| Exercise 5.23 Write out the truth definition for formulas with terms | ||
|
|
||
| Exercise 5.24 logical consequences that holds? | ||
|
|
||
| Exercise 5.25 which logical consequences holds? |
| | `Logic/Proof` | `open` | `¬`, `∀`, `∃`, `∧`, `∨`, `↔`, `≠` | `intro`, `exact`, `apply`, `cases … with`, `constructor`, `obtain`, `have`, `use`, `left`, `right`, `rcases`, `by_cases`, `by_contra`, `assumption` | | ||
| | `Logic/PL` | `abbrev`, `private` | `×` | `simp`, `native_decide` | | ||
| | `Logic/FOL` | `mutual`, `deriving BEq` | `\|>`, `List.contains` | `induction … generalizing` | | ||
| | `Logic/FOL` | `mutual` | `\|>` | `induction … generalizing`, `decide`, `refine`, `omega`, `absurd` (term) | |
Comment on lines
+99
to
+105
| - **`decide` in `Logic/FOL`** — used once, by `mem_vertices` | ||
| (`cases v <;> decide`), and presented in the sentence right after it: it | ||
| closes a decidable proposition by computing it. That is the whole of what the | ||
| chapter needs from it; `Sets` still develops `Decidable` properly. `omega`, | ||
| `refine` and the term-level `absurd` arrive in the same chapter's | ||
| infinite-domain section, in exposition rather than in an exercise, and are | ||
| *not* presented — see the next entry. |
Closes #13 CSwFP/5.25 asks which of `∀x∀y(Rxy→Ryx), Rab ⊨ Rba` and `… ⊨ Raa` hold. Two things were missing. Consequence from a list of premises; and validity for a formula carrying constants. `Formula.ValidT` supplies the second. It is not a duplicate of `Formula.Valid`: a structure for a language without function symbols is `(D, I)`, and for one with them `(D, I, F)`. `Formula.ImpliesL` supplies the first, via `Formula.conjs`, and mirrors `PL.Formula.impliesL` from the previous chapter — likewise an exercise that later exercises then call. Two exercises follow: `ex-fol-implies-from-list`, where the reader defines `ImpliesL`, and `ex-fol-entails` for 5.25 itself. The semantics of FOL section is rewritten around `Assign` and `liftAssign`; `ex-fol-valid` gains an interpretation. Two exercise in `PL.lean` are clarified; and `PROVENANCE.md` fills in the entries for 5.20–5.24, which were blank, and records `collect-atoms-alternative`. Ports `:::details` from sf-in-lean, a collapsible aside for material that supports the narrative without belonging to it, and uses it for the undecidability of interpretation over the naturals. Verified: all four variants emit, and the generated `solutions` project builds, which is the check that sees `solution!` stripped to `all_goals`. AI-usage disclosure: the material on validity and consequence for formulas with terms in this change was drafted with the assistance of Claude Opus 5 (Anthropic, September 2026, via Claude Code). The assistant measured the cost of each alternative, wrote the definitions, exercises and proofs, and drafted the Portuguese prose. The author takes full responsibility for the final content. The author rewritten all prose in Portuguese and redefine the exercises.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.