Repository navigation
docs(FOL): adopt a consistent terminology for the semantics - #34
Merged
Merged
Conversation
Follow the sequence signature, structure, assignment, satisfaction, model throughout the semantics of FOL: - write structures as 𝒜 = (D, I), or (D, I, F) with function symbols, in inline math, replacing 𝔸 and E, which clashed with the predicate E - reserve "interpretation" for I and "assignment" for g, and spell out what g[v := d] returns - write satisfaction as 𝒜 ⊨ α [g], and 𝒜 ⊨ α for sentences; drop the second notation, which conflated satisfaction with consequence - define a model of α as a structure that satisfies it, and state consequence and counterexamples in terms of models and structures - use ⊨ (U+22A8) instead of ⊧ (U+22A7) throughout - tighten the wording of a few sentences in the syntax section - fix typos AI-assisted: the terminology was discussed with an AI assistant, which also proposed the revised wording and typo fixes; every change was reviewed and approved by the author.
Contributor
There was a problem hiding this comment.
🟡 Changes recommended
Functional-symbol semantics are misstated, and the old consequence symbol remains in the PL chapter.
2 open findings
What changed in this PR
Standardizes terminology and notation in the FOL semantics chapter.
Changes:
- Clarifies structures, assignments, satisfaction, models, and consequence.
- Adopts
⊨notation and updates API documentation. - Corrects and refines Portuguese prose.
| File | Description |
|---|---|
CSwL/Logic/FOL.lean |
Revises FOL semantic terminology, notation, and explanations. |
🧠 Review effort: Balanced
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
This was referenced Oct 14, 2026
FOL: - spell out when a term is free for a variable: state the equivalent scope criterion, explain why each example is or is not free, make explicit that substitution only affects free occurrences - rate ex-fol-valid and ex-fol-consequence 5 instead of 2 - reflow the statement of the closedForm exercise Proof: - say that ∨ is inclusive where its rules are introduced - move the exchange exercise, renamed prop-exchange, next to the presentation of the connectives, and note that its argument is invalid - add a section on invalid arguments and counterexamples - present simp, simp only and simp … at h, and move them in the STYLE-CODE.md ledger from PL to Proof PL: - fix typos AI-assisted: typo fixes were drafted with an AI assistant; every change was reviewed and approved by the author.
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.
Summary
Revises the semantics section of
CSwL/Logic/FOL.leanso that it follows one terminology throughout: signature → structure → assignment → satisfaction → model.𝒜 = (D, I), or(D, I, F)with function symbols, in inline math. This replaces𝔸andE;Eclashed with the predicateEof theL₁example.I, and "assignment" onlyg. The text also spells out whatg[v := d]returns.𝒜 ⊨ α [g], and𝒜 ⊨ αfor sentences. The second notation is dropped because it conflated satisfaction with consequence.αis defined as a structure that satisfies it. Consequence and counterexamples are stated in terms of models and structures, and the docstrings ofFormula.ValidandFormula.Satisfiablenow say "structure".⊨(U+22A8) replaces⊧(U+22A7) everywhere.Verification
make studentbuilds.Follow-ups (not in this PR)
(D, I, F)into a Leanstructure, possibly aligned with Mathlib'sFirstOrder.Language.Structure.Valid/ValidTandImplies/ImpliesLboth exist, and whether domains should be required to beNonempty.🤖 Generated with Claude Code