While preparing the complete Turkish edition against Open Logic commit 9620cc7, we noticed five localized issues in the English source. Each was independently replayed against that exact tree; these are source notes only, not a request to review or merge the translation.
functions/inverses.tex, lines 62–84: an injective f:A→B need not have a left inverse when A=∅ and B≠∅; the proof also chooses a∈A. Small fix: assume A≠∅ (or treat the empty case separately).rules-G3i.tex, lines 41–43: right-∨ uses the multi-succedent premise Γ ⊢ A,B, contrary to G3i's single-succedent restriction. Small fix: use Γ ⊢ A_i / Γ ⊢ A_1∨A_2 for i=1,2.proof-search/tableaux.tex, lines 25–29: the initial tableau for A,B ⊢ C,D signs D true, although both succedent formulas must be false. Small fix: change T D to F D.propositions-as-types/types.tex, lines 42–52: the case clause binds x,y but uses x_1,x_2; additionally, untypable proof terms exist, so “has exactly one type” should be “has at most one type” (or “if it has a type, that type is unique”).interpretation-rules.tex, lines 49–52: the second XOR rule concludes with A⊕B in the antecedent, so its label should be left-⊕, not right-⊕.
The Turkish release and compact provenance bundle contain the corresponding transparent dispositions. Work performed at Floris's direction by OpenAI 5.6 Sol, Ultra mode (OpenAI's current flagship model for complex work).
While preparing the complete Turkish edition against Open Logic commit
9620cc7, we noticed five localized issues in the English source. Each was independently replayed against that exact tree; these are source notes only, not a request to review or merge the translation.functions/inverses.tex, lines 62–84: an injectivef:A→Bneed not have a left inverse whenA=∅andB≠∅; the proof also choosesa∈A. Small fix: assumeA≠∅(or treat the empty case separately).rules-G3i.tex, lines 41–43: right-∨ uses the multi-succedent premiseΓ ⊢ A,B, contrary to G3i's single-succedent restriction. Small fix: useΓ ⊢ A_i / Γ ⊢ A_1∨A_2fori=1,2.proof-search/tableaux.tex, lines 25–29: the initial tableau forA,B ⊢ C,DsignsDtrue, although both succedent formulas must be false. Small fix: changeT DtoF D.propositions-as-types/types.tex, lines 42–52: the case clause bindsx,ybut usesx_1,x_2; additionally, untypable proof terms exist, so “has exactly one type” should be “has at most one type” (or “if it has a type, that type is unique”).interpretation-rules.tex, lines 49–52: the second XOR rule concludes withA⊕Bin the antecedent, so its label should be left-⊕, not right-⊕.The Turkish release and compact provenance bundle contain the corresponding transparent dispositions. Work performed at Floris's direction by OpenAI 5.6 Sol, Ultra mode (OpenAI's current flagship model for complex work).