Add domain of discourse, quantifier negation and cycles of conditionals to Proof Writing by d-morrison · Pull Request #597 · Morrison-Lab/mds

d-morrison · 2026-11-03T16:39:23Z

Adds four blocks from mcs (CSCI 201), each with an example:

domain of discourse (after the predicate example);
De Morgan's laws for quantifiers (thm-negate-quantifiers, after the quantifier examples), with a remark on why its two laws share one theorem, as De Morgan's laws for propositions do;
a biconditional as two conditionals, and a cycle of conditionals (after the logical-equivalence example).

The first review asked for an example after each block, for premise and conclusion to get their own definitions, and for one rule of inference per theorem. That did not fit under the PR size cap, so logical argument, premise, conclusion and rule of inference moved to #600, and the six common rules follow it in their own PR. The cycle proof now splits into cases and no longer needs modus ponens.

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

mcs (CSCI 201) defines these general results locally. Moving them here, one block per subfile, lets mcs include them instead of keeping its own copies, per the mds/mcs consolidation plan. Each block keeps its mcs id. Adds domain of discourse, negating a quantifier, logical argument, rule of inference, the common rules of inference (modus ponens and five others; exm-formal-proof already uses modus ponens without naming it), a biconditional as two conditionals, and a cycle of conditionals. The inference rules sit after the notes on the entailment symbols, which they use. Part of #453. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019xfc9pMBq15Hq3DgNBx1ox

The review of #597 asked for an example after each new definition and result, as the rest of the Proof Writing page has. This adds one each for domain of discourse, the quantifier laws, a biconditional as two conditionals and a cycle of conditionals. The quantifier theorem is renamed "De Morgan's laws for quantifiers", with a remark saying why its two laws share one theorem, as De Morgan's laws for propositions do. The cycle proof now splits into the all-false case and the some-true case, and uses the definition of implies instead of modus ponens, so it no longer needs the inference rules. The biconditional and cycle results move before De Morgan's laws, so this PR and #596 touch different lines of the page. Logical argument, rule of inference and the inference rules move to their own PRs: the review asked for premise and conclusion to get their own definitions and for one rule per theorem, which does not fit under the PR size cap here. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019xfc9pMBq15Hq3DgNBx1ox

d-morrison · 2026-11-03T16:55:11Z

Addressed in 29d0ade:

Examples now follow domain of discourse, the quantifier laws, the biconditional split and the cycle.
The cycle proof is split into the all-false and the some-true cases.
Long when and so clauses are on their own lines.
Logical argument, rule of inference and the six rules moved out: Add logical argument, premise, conclusion and rule of inference #600 gives premise and conclusion their own definitions, and a later PR gives each rule its own theorem.

Rebutted:

The two quantifier laws stay in one theorem, now titled De Morgan's laws for quantifiers, with a remark saying why. That matches thm-de-morgan-logic, which states its two laws together.
No logic-operator macros exist in latex-macros/macros.qmd, and the rest of the page writes \neg, \land and \lor raw, so these do too. An inference-rule macro would belong in Morrison-Lab/macros; the bar display now appears only in Add logical argument, premise, conclusion and rule of inference #600 and the later rules PR.

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

Generated by Claude Code

The review asked for one clause per line in the biconditional and cycle examples. Also reword "every integer is not even" to the unambiguous "no integer is even", and state the pairing in the remark instead of claiming a reason the linked theorem does not give. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019xfc9pMBq15Hq3DgNBx1ox

… remark #598 links "negation" to def-not, so check-term-links now treats it as a defined term and flags these unlinked first uses after the merge of main. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019xfc9pMBq15Hq3DgNBx1ox

- exm-domain-of-discourse no longer writes the existential quantifier, which the page defines later, so it has no forward reference. - exm-equivalent-cycle puts its two "let" clauses on separate lines. - exm-negate-quantifiers applies both laws to the S and P(x) it sets up. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019xfc9pMBq15Hq3DgNBx1ox

d-morrison · 2026-11-03T18:48:08Z

Replies to the review at faed525 (#597 (comment)). The next push carries the fixes.

Two laws in thm-negate-quantifiers: deferred to Split De Morgan's laws into one theorem per law (propositions and quantifiers) #603. Splitting this theorem means adding a second theorem with its own example, and this PR already holds 10 files, the per-PR cap. thm-de-morgan-logic on main has the same shape and should be split the same way, so Split De Morgan's laws into one theorem per law (propositions and quantifiers) #603 covers both pairs in one change.
Forward reference in exm-domain-of-discourse: fixed. The example now says "$P(x)$ is true for $x = \sqrt{2}$" and "false for every $x$", with no quantifier symbol.
Line break in exm-equivalent-cycle.qmd:5: fixed. "and let:" now has its own line.
Unused $S$ and $P(x)$ in exm-negate-quantifiers: fixed. The example now applies both laws to them in symbols, then in words.
check-term-links: allow on "truth value" and "values": kept. No def-truth-value exists in mds, and the checker reads "value" as the term defined on the Functions page, which comes later, so a link there would be a forward reference.

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

Generated by Claude Code

mcs (CSCI 201) defines these locally. Moving them here lets mcs include them instead of keeping its own copies, per the mds/mcs consolidation plan. Logical argument and rule of inference keep their mcs ids. They were in #597 until its review asked for premise and conclusion to get their own definitions, which mcs folds into the logical-argument div. Each definition now has an example; the one for rule of inference shows a pattern that is not one (affirming the consequent), so it does not repeat the common rules, which follow in their own PR. Part of #453. Claude-Session: https://claude.ai/code/session_019xfc9pMBq15Hq3DgNBx1ox Co-authored-by: Claude <noreply@anthropic.com>

The proof called Q the conclusion of a true conditional. #600 made conclusion a defined term for arguments, later on the page, so the word now reads as an unlinked first use (check-term-links) and linking it would be a forward reference. State the step in symbols instead. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019xfc9pMBq15Hq3DgNBx1ox

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019xfc9pMBq15Hq3DgNBx1ox

github-actions · 2026-11-03T21:17:31Z

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

_{2026-11-03 22:54 UTC}

d-morrison · 2026-11-03T21:18:02Z

Merging under the session mwc grant (Ezra, 2026-11-03): CI is green, the Claude review on head 76084ba is clean, and check-pr-fully-clean.py exits 0.

The cross-model review gate is waived because no qualifying reviewer could run. OpenCode Go (opencode.ai/zen/go/v1/chat/completions, deepseek-v4-pro) returned HTTP 429 (monthly GoUsageLimitError) at 2026-11-03 13:17 PST, and no other cross-harness reviewer is reachable from this cloud session.

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

Generated by Claude Code

github-actions · 2026-11-03T22:02:56Z

Claude finished review — View run

I fetched PR #597 live just now. It is open, not a draft, and not merged. Its head is b8bf085bdda03a285e5179796e5409ed99ed32fa, the commit I reviewed. The review above applies to the current head.

Verdict

Ready for merge

Structured Review Data (JSON)

{
  "schema_version": "1.1",
  "reviewer": "claude",
  "commit_sha": "b8bf085bdda03a285e5179796e5409ed99ed32fa",
  "verdict": "CLEAN",
  "findings": [],
  "detailed_assessment": "Merge b8bf085 only brings main (#605) into the branch and matches git's automatic merge, and the PR diff over _proof-writing.qmd and the proof-writing subfiles has no conflict markers.",
  "holistic_assessment": "The PR's own content is unchanged since the clean review of e0609f4, so scope, integration and regression risk are unchanged and the prior Ready for merge verdict stands."
}

Reviewed commit: b8bf085

github-actions · 2026-11-03T22:02:57Z

💰 Cost: $0.2034 (review) — run

d-morrison · 2026-11-03T22:53:32Z

Merging under the session mwc grant (Ezra, 2026-11-03): CI is green, the Claude review on head b8bf085 is clean, and check-pr-fully-clean.py exits 0.

The cross-model review gate is waived because no qualifying reviewer could run. OpenCode Go (opencode.ai/zen/go/v1/chat/completions, deepseek-v4-pro) returned HTTP 429 at 2026-11-03 14:53 PST, and no other cross-harness reviewer is reachable from this cloud session.

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

Generated by Claude Code