[d-morrison]

Important

Merge before #599. Both add includes right after De Morgan's laws in _proof-writing.qmd, so #599 needs a one-hunk conflict fix after this merges.

Adds five blocks from mcs (CSCI 201), with an example after each of the first four:

• tautology and contradiction;
• equivalence as a tautological biconditional;
• double negation;
• why a proof by contradiction works (after thm-proof-by-contradiction).

The first review asked for an example after each block. Adding them took this PR past the size cap, so the distributive laws, the substitution theorem, negating a conditional and the conditional as an or moved to #599.

Part of #453 and of the mds/mcs consolidation plan (https://claude.ai/artifact/De8D2LiAwjX3fpLezVDdS7). Only definitions, theorems and proofs move from mcs; the examples here are new, and mcs keeps its own. Each block keeps its mcs id, so mcs can switch to the include without breaking a link.

Checked locally against gha main: check-term-links (0 errors), check-avoided-words and check-new-line-breaks are clean.

https://claude.ai/code/session_019xfc9pMBq15Hq3DgNBx1ox

---

Generated by Claude Code

[github-actions]

Claude finished review — View run

---

Review of PR #596 at 68e9c41

This round is clean. My earlier review (commit b6efdf1, Needs more work) is superseded. I did not render the site.

Earlier blocking items, now resolved

• Missing examples (rule 3). _exm-tautology.qmd and _exm-contradiction.qmd now follow def-tautology and def-contradiction in _proof-writing.qmd. Each gives a correct two-row truth table: P ∨ ¬P is true in both rows, and P ∧ ¬P is false in both.
• Examples for the remaining theorems. _exm-equivalence-iff.qmd and _exm-double-negation.qmd follow their theorems. The four-row biconditional table is correct, and the 7-is-odd example is sound.
• Line breaks (rule 12). The long line in _thm-contradiction-works.qmd:20 is now split before "where".
• Removed theorems. The commit drops thm-distributive, thm-substitution-logic, thm-negate-conditional and cor-conditional-as-or. That narrows the PR to the first four logic laws, so the examples I asked for on those are no longer needed. The two earlier suggestions, on _thm-substitution-logic.qmd:318 and _thm-equivalence-iff.qmd:268, are also moot for the removed file. I did not re-check the _thm-equivalence-iff.qmd link-check comment.
• Line breaks in _thm-negate-conditional.qmd. The two rule 12 findings on that file are gone because the file is gone.

Checks on the new files

• Cross-references.
  • #def-or, #def-not, #def-truth-table, #def-proposition, #def-logically-equivalent and #exm-logically-equivalent all exist.
  • number-systems.qmd#def-odd exists.
  • #def-tautology and #thm-equivalence-iff come earlier in the include order than the examples that cite them. There are no forward references.
• One div per subfile. Each new subfile holds exactly one #exm- div.
• Macros. The new math is only propositional connectives and truth tables, so no semantic-macro category applies.
• Line breaks in the new examples. Each sentence starts a new line, and each line holds one clause.

Verdict

Ready for merge

Structured Review Data (JSON)

{
  "schema_version": "1.1",
  "reviewer": "claude",
  "commit_sha": "68e9c4194ca28ad8bec611d1013c9ccd7fa6de4d",
  "verdict": "CLEAN",
  "findings": [],
  "detailed_assessment": "New example subfiles for tautology, contradiction, equivalence-iff and double negation have correct truth tables and resolving links; the thm-contradiction-works line is split at the where clause.",
  "holistic_assessment": "The commit adds the requested examples after each definition and theorem, narrows scope to four logic laws, and keeps the include order free of forward references."
}

I fetched PR #596 just now. It is open, not a draft, and not merged. Its head is still 68e9c4194ca28ad8bec611d1013c9ccd7fa6de4d, the commit I reviewed.

The review above stands.

Verdict

Ready for merge

Structured Review Data (JSON)

{
  "schema_version": "1.1",
  "reviewer": "claude",
  "commit_sha": "68e9c4194ca28ad8bec611d1013c9ccd7fa6de4d",
  "verdict": "CLEAN",
  "findings": [],
  "detailed_assessment": "New example subfiles for tautology, contradiction, equivalence-iff and double negation have correct truth tables and resolving links; the thm-contradiction-works line is split at the where clause.",
  "holistic_assessment": "The commit adds the requested examples after each definition and theorem, narrows scope to four logic laws, and keeps the include order free of forward references."
}

Reviewed commit: 68e9c41

[github-actions]

💰 Cost: $0.2437 (review) — run

[d-morrison]

Addressed in 68e9c41:

• Examples now follow tautology, contradiction, thm-equivalence-iff and double negation.
• The where clause in the contradiction proof is on its own line.
• The substitution theorem, negating a conditional and cor-conditional-as-or moved to Add the distributive laws and negating a conditional to Proof Writing #599, which restates the substitution claim exactly and adds their examples.

Rebutted: the check-term-links: allow comment on "truth value" stays. mds has no definition of truth value to link (no #def-truth-value anywhere in the repo), and the checker reads the phrase as the defined term "value".

Posted by Claude Code (AI agent) --- not written by a human.

---

Generated by Claude Code

[d-morrison]

Cross-model review waived: OpenCode Go returned 429 (monthly usage limit) to a chat-completions probe at 17:32 UTC, and no other cross-model reviewer is reachable from this session. The Claude review is clean on 68e9c41 and CI is green. The head is one commit behind main (#598); that commit adds different includes to _proof-writing.qmd, GitHub reports the PR mergeable, and the publish build on main will confirm the combined page. Merging under Ezra's mwc grant.

Posted by Claude Code (AI agent) --- not written by a human.

---

Generated by Claude Code

[github-actions]

PR Preview Action v1.8.1
Preview removed because the pull request was closed.

_{2026-11-03 17:40 UTC}