refactor(FOL): derive Repr and add ToString for the syntax types

[arademaker]

Logic/FOL was the one chapter whose syntax types printed through a hand-written Repr over Std.Format, so #eval of a formula showed its notation and there was no way to see its structure. InfEngine and ModelChecking already follow the other pattern: deriving Repr for the constructor tree, plus a ToString instance for the notation.

This moves Variable, Term and Formula to that pattern:

• deriving Repr on the three types; #eval f shows the tree.
• Variable.format, Term.format and Formula.format become toText functions to String, with ToString instances; toString f gives the same notation as before (∀x R[x, x]).
• ToString, how #eval chooses between Repr and ToString, and s! strings are presented at their first use, with Variable; the Formula paragraph becomes a short reminder.
• The ledger in STYLE-CODE.md moves ToString and s! strings from InfEngine to Logic/FOL and drops Std.Format. InfEngine used ToString without presenting it, so this also closes that gap.
• ModelChecking: #eval toString (lfSent tr1) in the prose, and the lfDET signature display is dropped.

Needed by the step-by-step example from syntax tree to formula that is being added to ModelChecking (#15), which shows both views of the same formula.

Verified locally: make all builds the four variants (the solutions project compiles standalone).

This change was prepared with the assistance of Claude Code (Anthropic); all edits were reviewed by the author.

[Copilot]

🟢 Approval recommended

Only a minor presentation-before-use convention issue remains; no blocking defects were identified.

1 open issue

• Avoid using $ syntax before it is introduced · New

What changed in this PR

Separates FOL syntax-tree output from readable logical notation, supporting the planned ModelChecking examples.

Changes:

• Derives Repr and adds ToString printers for FOL syntax types.
• Explains both display modes and updates the feature ledger.
• Adjusts ModelChecking prose and removes a redundant signature display.

File	Description
STYLE-CODE.md	Updates first-use entries for printing features.
CSwL/​ModelChecking.lean	Updates the display example and removes the signature display.
CSwL/​Logic/​FOL.lean	Separates structural and notation printing, with explanatory examples.

_{Review effort: Balanced}