Changes and reader corrections

Changes from the source

All 611 source files are packaged byte-for-byte. The reading views convert TeX presentation into semantic HTML, native MathML, accessible diagrams, and words-only scripts.

Reader corrections

Sets

1. SETS-RC-001 — Reader correction: the source omits ‘the’ before ‘set’ in this caption. This reader supplies it; the source file is unchanged. Source: content/sets-functions-relations/sets/unions-and-intersections.tex, line 26.
2. SETS-RC-002 — Reader correction: the source has no space between the displayed formula and ‘is’. This reader restores the space; the source file is unchanged. Source: content/sets-functions-relations/sets/important-sets.tex, line 56.
3. SETS-RC-003 — Reader correction: the source omits ‘the’ before ‘length’. This reader supplies it; the source file is unchanged. Source: content/sets-functions-relations/sets/important-sets.tex, line 58.

The Size of Sets

Editorial projection note: the source gives this alternate exercise the same link label as the corresponding exercise in the earlier Reduction section. This edition assigns the alternate copy its own link target; unqualified references lead to the earlier copy. The canonical source is unchanged.

The exact correction changes only the alternate derived link label; the source files remain unchanged. The earlier Reduction exercise remains the destination for unqualified references.

Later-chapter dependency

Functions refers once to the Choice chapter. That later chapter is not bundled here; the reading page says so directly instead of creating a broken offline link.

The Sequent Calculus: four printed-source notes

The printed source and its spoken rendering are preserved without silent correction. These notes identify seven suspect printed locations.

1. proving-things.tex, lines 86, 104, 125, 147: Each cited inference reorders formulas in the antecedent, but the printed rule label names right exchange. Preserve and speak the printed right-exchange label, then disclose that the changed side is the antecedent and that left exchange appears intended.
2. soundness.tex, line 157: The immediately preceding argument establishes validity of the conclusion with the conjunction on the left; this sentence instead names the premise sequent. Preserve the printed claim and attach a note that the preceding argument appears to establish the conclusion sequent with A and B conjoined on the left.
3. soundness.tex, line 288: The proof discusses satisfaction of the right premise, but the printed expression is set difference rather than a sequent. Preserve and read the printed expression as capital Pi set difference capital Lambda, then disclose that capital Pi sequent arrow capital Lambda appears intended.
4. derivations.tex, line 70: The printed conclusion ends with a comma after capital Delta but supplies no following succedent formula. Preserve and speak the printed trailing comma as having no following formula, then disclose that it appears to be stray punctuation.

Arithmetization: 9 disclosed reader corrections

The accepted projected source remains immutable. Read, Listen, and Explore apply the reviewed reader wording and retain the source-side disclosure.

1. TR006-SOURCE-FORMULA-007 — The source compares a real-equivalence class with rational zero. The reader says real zero, which is the identity in the constructed ordered field, while preserving the printed formula and source MathML. Source: content/sets-functions-relations/arithmetization/cauchy.tex, line 150.
2. TR006-SOURCE-PROSE-001 — The reader supplies the missing word 'to' in the source explanation of multiplication by juxtaposition. Source: content/sets-functions-relations/arithmetization/integers.tex, line 55.
3. TR006-SOURCE-PROSE-002 — Nonemptiness, not the existence of an upper bound, supplies a member of S; the immutable source wording is retained separately. Source: content/sets-functions-relations/arithmetization/cuts.tex, line 64.
4. TR006-SOURCE-PROSE-003 — The reader supplies the missing noun 'details.' Source: content/sets-functions-relations/arithmetization/checking-details.tex, line 150.
5. TR006-SOURCE-PROSE-004 — The reader supplies the missing word 'is.' Source: content/sets-functions-relations/arithmetization/cauchy.tex, line 101.
6. TR006-SOURCE-PROSE-005 — The construction identifies reals with equivalence classes, not with the equivalence relation itself. Source: content/sets-functions-relations/arithmetization/cauchy.tex, lines 110, 111.
7. TR006-SOURCE-PROSE-006 — The reader removes the duplicated word 'we.' Source: content/sets-functions-relations/arithmetization/cauchy.tex, line 149.
8. TR006-SOURCE-PROSE-008 — The reader corrects the blended phrase 'hone on in' to 'home in on.' Source: content/sets-functions-relations/arithmetization/cauchy.tex, line 190.
9. TR006-SOURCE-PROSE-009 — The printed equality is a proposition, not an object that can be an upper bound. The reader identifies the common class intended by the surrounding proof while retaining the source formula and its MathML. Source: content/sets-functions-relations/arithmetization/cauchy.tex, line 226.

Arithmetization: words-only presentation normalization

This semantic-neutral normalization prevents a redundant source symbol from entering continuous speech; the accepted projected source remains immutable.

1. SFR-ARITH-PRESENTATION-001 — The projected source has a redundant less-than character immediately before the words 'are all smaller than.' The prose reader omits that duplicate symbol; the exact accepted projected TeX remains available in Source and provenance. Source: content/sets-functions-relations/arithmetization/reals.tex, line 80.

Infinite Sets: 2 disclosed reader corrections

The accepted projected source remains immutable. Read, Listen, and Explore apply the reviewed reader wording and retain the source-side disclosure.

1. TR007-SOURCE-FORMULA-002 — The source nests a binary equinumerosity macro, syntactically comparing the proposition A is equinumerous with B to C. The reader preserves that printed source separately and states the sandwich proposition's intended conclusion: A is equinumerous with B and B is equinumerous with C. Source: content/sets-functions-relations/infinite/card-sb.tex, line 52.
2. TR007-SOURCE-PROSE-001 — The reader removes the stray word 'be' from the immutable source phrase 'must be characterize.' Source: content/sets-functions-relations/infinite/hilberts-hotel.tex, line 14.

Tableaux: seven disclosed reader corrections

The immutable source files remain byte-identical. Read, Listen, and Explore expose the reviewed reader interpretation; Source shows both exact source lines and each disclosure.

1. TR012-SOURCE-FORMULA-001 — The frozen source first writes Gamma sub one as C sub one through C sub n, then uses C sub one through C sub m in the next display. The reader preserves both indices and discloses the mismatch. Source: content/first-order-logic/tableaux/provability-consistency.tex, lines 26, 31.
2. TR012-SOURCE-FORMULA-006 — The frozen exercise accidentally groups not B inside the preceding signed-formula argument. The reader preserves the printed source and explicitly presents the intended three separate signed assumptions. Source: content/first-order-logic/tableaux/proving-things.tex, line 439.
3. TR012-SOURCE-FORMULA-007 — The reader preserves the printed D-sub-m subset relation as source MathML and explicitly identifies it as malformed. A separate reader projection gives the finite-family inclusion required by the surrounding derivability argument. Source: content/first-order-logic/tableaux/proof-theoretic-notions.tex, line 105.
4. TR012-SOURCE-PROOF-005 — The frozen proof prose names false-signed A, rather than true-signed not A, as the input to the true-negation rule and then numbers the derived line n plus one. The reader preserves the printed source and explicitly gives the rule-correct input and resulting n-plus-two line under the stated ordering. Source: content/first-order-logic/tableaux/provability-consistency.tex, lines 90, 91, 92, 93, 94, 95.
5. TR012-SOURCE-PROSE-002 — The reader removes the duplicated word in the source phrase 'left left.' Source: content/first-order-logic/tableaux/provability-consistency.tex, line 122.
6. TR012-SOURCE-PROSE-003 — The reader corrects the source phrase 'we can applying' to 'we can apply.' Source: content/first-order-logic/tableaux/provability-consistency.tex, line 138.
7. TR012-SOURCE-TABLEAU-004 — Eight frozen tableau commands group the formula inside the truth-value macro. The structural reader preserves the printed source and presents the intended separate truth sign and formula as an explicit reader correction. Source: content/first-order-logic/tableaux/provability-propositional.tex, lines 43, 44, 53, 54, 106, 107, 116, 117.

Axiomatic Deduction: four disclosed reader corrections

The immutable source files remain byte-identical. Read, Listen, and Explore expose the reviewed reader interpretation; Source shows both exact source lines and each disclosure.

1. TR013-SOURCE-FORMULA-001 — The frozen source omits B before the membership sign in this induction-basis sentence. The reader supplies B, matching the same sentence and the immediately following case split. Source: content/first-order-logic/axiomatic-deduction/deduction-theorem.tex, line 67.
2. TR013-SOURCE-FORMULA-002 — The frozen source is missing the final closing parenthesis in this displayed conditional. The reader adds that delimiter while retaining source MathML for comparison. Source: content/first-order-logic/axiomatic-deduction/deduction-theorem.tex, lines 106, 107.
3. TR013-SOURCE-PROSE-004 — The reader corrects the frozen source spelling 'modus ponsens' to 'modus ponens.' Source: content/first-order-logic/axiomatic-deduction/provability-propositional.tex, line 58.
4. TR013-SOURCE-REFERENCE-003 — The frozen proof cites the first conjunction-elimination axiom twice. The two conclusions require the first and second conjunction-elimination axioms, so the reader names axiom land two for the second citation. Source: content/first-order-logic/axiomatic-deduction/provability-propositional.tex, line 33.

The Completeness Theorem: two disclosed reader corrections

The immutable source files remain byte-identical. Read, Listen, and Explore expose the reviewed reader interpretation; Source shows both exact source lines and each disclosure.

1. SAR-002 — Editorial projection note: the source omits an empty non-first-order alternative at this conditional boundary. This edition restores the boundary, so first-order-only material appears only in the first-order chapter; the canonical source is unchanged. Source: content/first-order-logic/completeness/construction-of-model.tex, line 75.
2. TR014-SOURCE-PROSE-001 — Source correction: in the propositional edition, a conditional in the source removes the replacement target from this sentence. This reader supplies the intended finite-satisfiability proposition; the source file is unchanged. Source: content/first-order-logic/completeness/compactness-direct.tex, lines 139, 140, 141, 142.

Introduction to First-Order Logic: six disclosed reader corrections

The immutable source files remain byte-identical. Read, Listen, and Explore expose the reviewed reader interpretation; Source shows both exact source lines and each disclosure.

1. TR015-READER-CORRECTION-001 — The source fragment omits the closing scope bracket of the universal formula. The reader rendering supplies that bracket explicitly. Source: content/first-order-logic/introduction/first-order-logic.tex, lines 69, 82.
2. TR015-READER-CORRECTION-002 — The source closes the universal scope only after the entailment. The reader rendering places that bracket before the premise comma and removes the resulting extra final bracket. Source: content/first-order-logic/introduction/first-order-logic.tex, line 51.
3. TR015-READER-CORRECTION-003 — The source closes the universal scope before the argument of the atomic formula. The reader rendering keeps that argument inside the atom and the quantified scope. Source: content/first-order-logic/introduction/substitution.tex, line 16.
4. TR015-READER-CORRECTION-004 — The source fragment contains one extra closing scope bracket. The reader rendering removes that extra bracket explicitly. Source: content/first-order-logic/introduction/first-order-logic.tex, lines 70, 84.
5. TR015-SOURCE-PROSE-CORRECTION-001 — In the general case there may be many predicates and constants; predicate or relation symbols, not individual constants, can have more than one place. Source: content/first-order-logic/introduction/satisfaction.tex, line 24.
6. TR015-SOURCE-PROSE-CORRECTION-002 — In this example the assignment values are zero, one, or two, the elements of the domain fixed above. Source: content/first-order-logic/introduction/satisfaction.tex, line 63.

Syntax of First-Order Logic: thirteen disclosed reader corrections

The immutable source files remain byte-identical. Read, Listen, and Explore expose the reviewed reader interpretation; Source shows both exact source lines and each disclosure.

1. occurrence-correction-projected-formula-0006646 — The source table places the closing parenthesis outside the math delimiter. The reader rendering includes it in the displayed conjunction. Source: content/first-order-logic/syntax-and-semantics/main-operator.tex, line 90.
2. occurrence-correction-projected-formula-0006648 — The source table places the closing parenthesis outside the math delimiter. The reader rendering includes it in the displayed disjunction. Source: content/first-order-logic/syntax-and-semantics/main-operator.tex, line 91.
3. occurrence-correction-projected-formula-0006650 — The source table places the closing parenthesis outside the math delimiter. The reader rendering includes it in the displayed conditional. Source: content/first-order-logic/syntax-and-semantics/main-operator.tex, line 92.
4. occurrence-correction-projected-formula-0006725 — The source uses k both as the declared arity and as the final zero-based argument index, which displays k plus one arguments. The reader preserves and explicitly flags this mismatch. Source: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 45.
5. occurrence-correction-projected-formula-0006727 — The displayed index range contains k plus one argument positions, although the preceding source calls the function k-ary. The reader preserves and explicitly flags this mismatch. Source: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 46.
6. occurrence-correction-projected-formula-0006728 — The source calls f k-ary but displays arguments indexed from m sub zero through m sub k, which is k plus one displayed arguments. The reader preserves that source mismatch and does not silently choose a correction. Source: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 46.
7. occurrence-correction-projected-formula-0006791 — The reader interprets n as the final sequence index. The source calls the following m a length, but a sequence indexed zero through n has length n plus one. Source: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 183.
8. occurrence-correction-projected-formula-0006792 — The source calls m a sequence length while inducting on the final index n. Since a sequence indexed from zero through n has n plus one entries, the literal length statement is off by one. The reader treats m and n as final indices; equivalently, the proof may induct on length n plus one and use all shorter lengths. Source: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 185.
9. occurrence-correction-projected-formula-0006794 — The printed sentence has a garden-path construction: 'either A is syntactically identical to A sub n is atomic.' The reader supplies appositive wording so the intended claim is that A, identical to the final entry A sub n, is atomic. Source: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 186.
10. occurrence-correction-projected-formula-0006803 — The source prints the undefined language L sub zero here, although this theorem fixes the first-order language L. The reader uses L and preserves the printed source in the source view. Source: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 199.
11. occurrence-correction-projected-formula-0006804 — The source prints material-equivalence notation in this proof case, while the formation clauses and the argument require syntactic identity. The reader uses syntactic identity and preserves the printed source in the source view. Source: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 200.
12. occurrence-correction-projected-formula-0006810 — The source says the proper initial sequences have length less than n. The correct final-index statement is that they end at indices less than n; equivalently their lengths are less than n plus one. Source: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 205.
13. occurrence-correction-projected-formula-0006813 — The source again prints the undefined language L sub zero here. The theorem concerns the fixed first-order language L, which the reader uses while preserving the printed source in the source view. Source: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 206.

Semantics of First-Order Logic: seven disclosed reader corrections

The immutable source files remain byte-identical. Read, Listen, and Explore expose the reviewed reader interpretation; Source shows both exact source lines and each disclosure.

1. occurrence-correction-projected-formula-0007228 — The source writes only equals three after already naming the interpreted function value in the same sentence. The reader repeats f superscript M of x comma y so the isolated occurrence has its actual left-hand side. Source: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 187.
2. occurrence-correction-projected-formula-0007240 — The source appends the assignment marker s to the interpreted relation rather than to a satisfaction statement. The reader omits that stray assignment marker. Source: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 213.
3. occurrence-correction-projected-formula-0007293 — The source omits m from the second case in the phrase 'm equals one and m equals two.' The reader supplies m before equals two. Source: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 331.
4. occurrence-correction-projected-formula-0007401 — The source starts the argument-value tuple with t sub i although the displayed sequence runs from the first through the k-th term. The reader uses t sub one. Source: content/first-order-logic/syntax-and-semantics/assignments.tex, line 91.
5. TR017-SOURCE-PROSE-001 — a structure for the set-theory language requires a set and a single two-place relation. Source: content/first-order-logic/syntax-and-semantics/structures.tex, line 77.
6. TR017-SOURCE-PROSE-002 — for every m in the domain of M, either the antecedent fails or the existential consequent holds. Source: content/first-order-logic/syntax-and-semantics/satisfaction.tex, line 347.
7. TR017-SOURCE-PROSE-003 — If Gamma is a set of sentences, we say that. Source: content/first-order-logic/syntax-and-semantics/assignments.tex, line 241.

Theories and Their Models: four disclosed reader corrections

The immutable source and accepted projected transcript remain byte-identical. Read, Listen, and Explore expose the reviewed reader interpretation; Source shows the exact source lines and each disclosure.

1. TR018-SOURCE-001 — The final v sub two lacks the object-language marker used for every neighboring variable. The reader supplies that marker without changing the frozen source occurrence. Source: content/first-order-logic/models-theories/expressing-relations.tex, line 64.
2. TR018-SOURCE-002 — The extensionality row opens the scope of the z quantifier with a parenthesis instead of the square bracket required by the local quantifier macro. The reader restores the scope bracket. Source: content/first-order-logic/models-theories/theories.tex, line 75.
3. TR018-SOURCE-003 — At line 121, the source closes the universal-u implication before its aligned existential consequent; at line 123, it closes the universal-x implication before its aligned totality-and-uniqueness consequent. The reader groups both displayed consequents inside their respective universal implications without changing the frozen source. Source: content/first-order-logic/models-theories/set-theory.tex, lines 121, 123.
4. TR018-SOURCE-004 — The injectivity antecedent closes both universal scopes before the aligned existence clause. The reader groups that clause into the antecedent described by the following prose. Source: content/first-order-logic/models-theories/set-theory.tex, line 134.

First-order Derivation Systems: bounded reader and conformance interventions

The six authority files are already shared with the earlier profile and remain byte-identical. The canonical FOL projection is separately bound.

1. TR019-SOURCE-001 — The frozen source misspells unsatisfiability as ‘unsatisfiablity.’ Read and Listen use the standard spelling; Source preserves and identifies the exact source text. Source: content/first-order-logic/proof-systems/introduction.tex, line 86.
2. TR019-SOURCE-LABEL-001 — The source labels two true-signed conjunction-expansion steps as true-conditional steps. The reader preserves and explicitly identifies those labels. Source: content/first-order-logic/proof-systems/tableaux.tex, line 53.
3. TR019-HTML-CONFORMANCE-001 — The cumulative Read and Listen HTML is normalized to valid paragraph and block structure. All 667 inherited formula-help disclosures remain associated with their exact formula IDs; authored text, MathML, formula order, and source anchors remain unchanged.

First-order Sequent Calculus: preserved printed anomalies and listener repair

The fifteen authority files and accepted projected transcript remain byte-identical. The four anomalies are disclosed at seven exact source anchors. The accepted listener evidence closes 77 exact seams (58 context-composition duplications and 19 glued-word boundaries) without changing semantic identities.

1. TR020-SOURCE-NOTE-001: Each cited inference reorders formulas in the antecedent, but the printed rule label names right exchange. Preserve and speak the printed right-exchange label, then disclose that the changed side is the antecedent and that left exchange appears intended.
2. TR020-SOURCE-NOTE-002: The immediately preceding argument establishes validity of the conclusion with the conjunction on the left; this sentence instead names the premise sequent. Preserve the printed claim and disclose that the preceding argument appears to establish the conclusion sequent with A and B conjoined on the left.
3. TR020-SOURCE-NOTE-003: The proof discusses satisfaction of the right premise, but the printed expression is set difference rather than a sequent. Preserve and read the printed expression as capital Pi set difference capital Lambda, then disclose that capital Pi sequent arrow capital Lambda appears intended.
4. TR020-SOURCE-NOTE-004: The printed conclusion ends with a comma after capital Delta but supplies no following succedent formula. Preserve and speak the printed trailing comma as having no following formula, then disclose that it appears to be stray punctuation.

First-order Natural Deduction: preserved printed prose defects and listener repair

The fourteen authority files and accepted projected transcript remain byte-identical. The two prose defects are disclosed at four exact source anchors. The accepted listener evidence closes 300 exact seams (seven heading placeholders, 283 proof-formula boundaries, and ten reference targets) without changing semantic identities.

1. TR021-SOURCE-PROSE-001: The coordinated clause omits 'is called' before 'the conclusion of the inference'. Read 'the sentence below is called the conclusion of the inference', followed by an explicit reader-correction note.
2. TR021-SOURCE-PROSE-002: The editorial sentence omits 'of' between 'definitions' and 'the provability relation'. Read 'the definitions of the provability relation', followed by an explicit reader-correction note.

First-order Tableaux: preserved printed prose defects and listener repair

The fourteen authority files and accepted projected transcript remain byte-identical. Seven source defects are disclosed at twenty exact source anchors. The final producer-only listener chain closes 230 exact repairs: thirteen imported chapter-anchor phrases removed, 162 binding-adjacent punctuation integrations, 54 broader prose punctuation integrations, and one independently accepted semantic grouping repair. The accepted-reader layer then applies 27 presentation-normalization decisions at 163 exact listener applications and speaks two preserved source-semantic discrepancy notices at their source-order positions. Stable identities and immutable source bytes are unchanged; fresh reader audit remains required.

1. TR022-SOURCE-FORMULA-001: Gamma one ends at C sub n, but the next displayed tableau row ends at C sub m — The frozen source first writes Gamma sub one as C sub one through C sub n, then uses C sub one through C sub m in the next display. The reader preserves both indices and discloses the mismatch.
2. TR022-SOURCE-FORMULA-006: The source places comma not B inside the formula argument carrying the true sign, then separately gives false-signed A. — The frozen exercise accidentally groups not B inside the preceding signed-formula argument. The reader preserves the printed source and explicitly presents the intended three separate signed assumptions.
3. TR022-SOURCE-FORMULA-007: The frozen source prints D sub one, through D sub m is a subset of Gamma; grammatically, only D sub m is placed to the left of the subset relation, although D sub m is a formula rather than a set. — The reader preserves the printed D-sub-m subset relation as source MathML and explicitly identifies it as malformed. A separate reader projection gives the finite-family inclusion required by the surrounding derivability argument.
4. TR022-SOURCE-PROOF-005: After replacing false-signed A by true-signed not A, the source says to apply the true-negation rule to false-signed A and identifies the derived false-signed A as line n plus one. — The frozen proof prose names false-signed A, rather than true-signed not A, as the input to the true-negation rule and then numbers the derived line n plus one. The reader preserves the printed source and explicitly gives the rule-correct input and resulting n-plus-two line under the stated ordering.
5. TR022-SOURCE-PROSE-002: left left — The reader removes the duplicated word in the source phrase 'left left.'
6. TR022-SOURCE-PROSE-003: we can applying — The reader corrects the source phrase 'we can applying' to 'we can apply.'
7. TR022-SOURCE-TABLEAU-004: The truth-value sign macro encloses the formula where sFmla expects separate sign and formula arguments. — Eight frozen tableau commands group the formula inside the truth-value macro. The structural reader preserves the printed source and presents the intended separate truth sign and formula as an explicit reader correction.

Axiomatic Deduction: disclosed source corrections and listener presentation

All fourteen authority files and the projected transcript remain byte-identical. Five source defects are disclosed at six exact anchors. The reader applies 21 bounded Listen normalization decisions across 68 applications and 121 atomic edits, preserving all formula, reference, formal-object, source, and MathML identities.

1. TR023-SOURCE-FORMULA-001: either belongs to Gamma union the singleton set containing A or is an axiom — The frozen source omits B before the membership sign in this induction-basis sentence. The reader supplies B, matching the same sentence and the immediately following case split.
2. TR023-SOURCE-FORMULA-002: The displayed transitivity formula opens the outer consequent and does not close it. — The frozen source is missing the final closing parenthesis in this displayed conditional. The reader adds that delimiter while retaining source MathML for comparison.
3. TR023-SOURCE-FORMULA-005: The sixth display row leaves open the consequent that begins with the conditional from A to the conditional from C to universal D of x. — The frozen quantified deduction-theorem display is missing one final closing parenthesis in its sixth formula row. The reader adds that delimiter while retaining exact source MathML for comparison.
4. TR023-SOURCE-PROSE-004: modus ponsens — The reader corrects the frozen source spelling 'modus ponsens' to 'modus ponens.'
5. TR023-SOURCE-REFERENCE-003: From axiom land one and axiom land one — The frozen proof cites the first conjunction-elimination axiom twice. The two conclusions require the first and second conjunction-elimination axioms, so the reader names axiom land two for the second citation.

OLAB-TR-024 — First-Order Completeness

Five source corrections are disclosed at their exact anchors; no source bytes or semantic MathML are silently changed. Listener repairs are carried from the independently accepted v2 stream.

OLAB-TR-025–027 — Beyond and Model Theory batch

Twenty-two source corrections are disclosed at exact anchors. Two forward references from Models of Arithmetic now link to their exact source targets in Representability in Q. No authority source byte is changed.

OLAB-TR-028–032 — Model theory, computability, and Turing machines

Sixty-nine reviewed reader corrections are disclosed at source anchors. Sixteen diagrams have authored nonvisual descriptions, and both transition tables retain native structural MathML plus plain-language descriptions. The external tape-snapshot asset is packaged byte-for-byte. No authority source byte is changed.

OLAB-TR-033 — Undecidability

Thirty reviewed reader corrections are disclosed at exact source anchors. Three machine diagrams have authored nonvisual descriptions. All 13 exercises remain question-only and unsolved; no authority source byte is changed.

OLAB-TR-034 — Introduction to Incompleteness

25 reviewed reader corrections, including 6 native-MathML repairs, are disclosed at exact source anchors. The exercise remains question-only and unsolved; no authority source byte is changed.

OLAB-TR-035 — Arithmetization of Syntax

Twenty enacted corrections and eight preserved anomaly notes are disclosed at source anchors; 15 formula occurrences have source-preserving reader MathML repairs. Seven exercises remain unsolved. Reader prose repairs are marked in the body and recorded at exact original source offsets.

OLAB-TR-036–044 — source and reader projections

The batch retains 61 source-anomaly notes and enacts six source-derived reader corrections, including five formula-reader repairs. Source-generated math is separately identified. Two valid original formulas split by the frozen delimiter census are rendered completely once in Read and Explore; their original fragment records remain forensic source evidence. No original source byte or stable census ID is changed.

OLAB-TR-045–049 and part-wrapper projection

The five chapter packets preserve 25 disclosed source-anomaly notes and enact no silent source correction. Ordered tables and proof trees retain source order, native MathML, stable formula IDs, exact source anchors, and words-only listener descriptions. The independently accepted Propositional Logic part wrapper is inserted before its first chapter and remains explicitly owned by part:pl; its historical sfr:infinite census cursor is provenance only. Original source bytes and all source, author, and human-contributor credits remain preserved.

OLAB-TR-050–079 producer-candidate projection

The thirty packet projections preserve 76 disclosed source-anomaly notes and enact no silent source correction. Source math, tables, proof trees, derivations, tableaux, and graphs retain packet order, native MathML, stable identities, exact source anchors, and words-only listener descriptions. Accepted predecessor profile-route bytes remain unchanged. Independent whole-book audit is required before promotion or a completion claim.