Hello — while checking complete translation targets against the English source, I found seven small, high-confidence source defects. I verified each against current master at 1e960beff9ed7835bf3e3f1335e21af3439cd107 as well as the frozen translation authority 9620cc7.
This list deliberately excludes everything already raised in #432, #433, or the findings ledger linked from #432.
-
content/proof-theory/proof-search/tableaux.tex:29
shows that would show that → would show that (or simply shows that).
-
content/second-order-logic/metatheory/second-order-arithmetic.tex:41–42
\Domain{M})$. → \Domain{M}$). The parenthesis belongs to the surrounding “i.e.” clause, not inside the formula.
-
content/second-order-logic/metatheory/undecidability-and-axiomatizability.tex:33
$\Sat{M}{!P \lif !A$}. → $\Sat{M}{!P \lif !A}$. This closes the second argument of \Sat before math mode ends.
-
content/set-theory/ord-arithmetic/using-addition.tex:61
Insert the missing =: $\setrank{A \times B} = \max(\setrank{A}, \setrank{B}) \ordplus 2$.
-
content/first-order-logic/tableaux/provability-consistency.tex:122
On the left left side → On the left side.
-
content/sets-functions-relations/size-of-sets/non-enumerability-alt.tex:135
iff if → iff.
-
content/proof-theory/sequent-calculus/invertibility.tex:331,366,372
At line 331, \RightR{\lexists} → \RightR{\lforall}, since the displayed principal formula is universal. At lines 366 and 372, !B → !B(t), matching the existential-rule premise at line 360.
These are source-quality notes for maintainer review; no upstream endorsement of any translation is implied.
Hello — while checking complete translation targets against the English source, I found seven small, high-confidence source defects. I verified each against current
masterat1e960beff9ed7835bf3e3f1335e21af3439cd107as well as the frozen translation authority9620cc7.This list deliberately excludes everything already raised in #432, #433, or the findings ledger linked from #432.
content/proof-theory/proof-search/tableaux.tex:29shows that would show that→would show that(or simplyshows that).content/second-order-logic/metatheory/second-order-arithmetic.tex:41–42\Domain{M})$.→\Domain{M}$).The parenthesis belongs to the surrounding “i.e.” clause, not inside the formula.content/second-order-logic/metatheory/undecidability-and-axiomatizability.tex:33$\Sat{M}{!P \lif !A$}.→$\Sat{M}{!P \lif !A}$.This closes the second argument of\Satbefore math mode ends.content/set-theory/ord-arithmetic/using-addition.tex:61Insert the missing
=:$\setrank{A \times B} = \max(\setrank{A}, \setrank{B}) \ordplus 2$.content/first-order-logic/tableaux/provability-consistency.tex:122On the left left side→On the left side.content/sets-functions-relations/size-of-sets/non-enumerability-alt.tex:135iff if→iff.content/proof-theory/sequent-calculus/invertibility.tex:331,366,372At line 331,
\RightR{\lexists}→\RightR{\lforall}, since the displayed principal formula is universal. At lines 366 and 372,!B→!B(t), matching the existential-rule premise at line 360.These are source-quality notes for maintainer review; no upstream endorsement of any translation is implied.