数学与逻辑：总结与挑战

摘要

本课结束本课程的第四单元，即数学与逻辑单元。它重建从数学模式通往演绎树的原理与机制之链，在每一环指出用到哪条原理、它在哪一课中确立；把已取得的成果放回课程计划中去衡量，并指明哪些只是略作预告的问题留给后面的单元；在结业测验中重复入门测验的各项技能；最后给出六道挑战题，难度高于各课的习题，要求综合几课的内容：编写一份含有命题、证明和引用的笔记，诊断能够编译却有缺陷而毫无提示的文档，把一种逻辑记法从一种传统转写到另一种传统，构造并调试一个有多个分支的演绎，预测一份物理报告的编号和量值，以及合并两份互不相容的导言区。

学习目标

重建本单元各机制的次序，指出每一机制所依据的原理。
解释为什么数学书写中有那么多缺陷能够毫无警告地通过编译，以及应在输出或日志的什么地方寻找它们的痕迹。
区分本单元已经确立的内容与只是预告、留待后续单元展开的内容。
预测一份含有方程、命题和单位的源文件所产生的编号、引用和量值，并加以改正。
设计一份导言区，确定一项工作的记号、命题和宏包加载顺序，使得更换约定时无须改动正文。

本单元的收获

本单元的目标是：公式中的每个符号都按其含义排版，一项工作的记号在所有页面上保持一致。这个目标的达成，依靠的是导言宣布为前几个单元已知的内容：引用，它取决于标签记录了什么；自定义命令，它把形式上的决定集中在导言区；以及阅读日志。因此，走过的路可以读成由五段组成的一条链。

行内公式与行间公式

关于行内公式与行间公式的一课确立了几乎所有其他原理都依赖的原理：在数学模式中，源代码的空格不起作用，引擎按照每个符号的类别（普通符号、二元运算符、关系符、标点、开符号或闭符号）来安排间距。由此推出：为什么变量不用 \textit 书写，为什么 $12,345$ 得到“12, 345”，为什么句子的标点放在行内公式之外。它说明了在 LuaLaTeX 中，写在模式之外的希腊字母不会报错，而是消失或不受控制地出现，日志中只有一行“Missing character”；把行间公式当作句子的一部分加标点，不留空行，也不用 $$；用 equation、\eqref、\numberwithin 和 \tag 编号；区分 \text 与 \mathrm；并研究了中文科技文献所用的小数点、在公式中作为标点而属于数字时要放进花括号的逗号、icomma 宏包，以及 siunitx 宏包：它的默认设置已经符合中文惯例，而 locale = UK 能防范从其他语言继承来的导言区。

符号与记号

关于符号与记号的一课从一条分组规则出发：^ 和 _ 作用于单个元素或花括号中的一组。它依次讲了分数、根式、希腊字母和字母表，其中包括使用 fontspec 时会无错消失的组合，如 \mathbf{\Gamma}；有名称的算子：中文文档不加载 babel，算子保持原名，而西班牙语的 babel 是各种会加以干预的语言中最典型的一例，它改变算子（\lim 带重音，新的 \sen，不变的 \sin），es-minimal 则取消这些改变；大型算子、定界符及其尺寸；陌生符号的查找；以及 unicode-math 和它的四项注意事项。最后把记号移到导言区，写成一次决定的自定义命令。

多行公式

关于多行公式的一课用 align 代替叠放的公式和 eqnarray，把 & 放在关系符之前，并确立：对齐环境是一张表，每个 \\ 一行，两个 & 之间的每一段一个单元格。由此推出它的无声缺陷（=&、多余的 &、末尾那个给空行编号的双反斜线、在带 \notag 的行上的标签）和它的显性错误；根据整体应带的编号在 gather、multline、split、aligned 和 gathered 之间作出选择；用 cases 和 dcases 排分段定义，用 \intertext 排文字，排矩阵和增广矩阵；用 subequations 给一组公式编号，并允许跨页断开。

定理与证明

关于定理与证明的一课把“声明而不模仿”的思想用到命题上：借助 amsthm，\newtheorem 规定每类命题的标题、编号和样式。它推出何时宜用共享计数器、何时宜用独立计数器，何时按节或按章编号，以及哪种样式对应所断言的、所规定的和起伴随作用的内容。它用 proof 排证明，其标题来自 \proofname（luatexja 不定义它，需要自己设定），并用 \qedhere 纠正孤零零的方块；用在 amsthm 之后加载的 cleveref 引用，每个环境一个 \crefname，并发现在 \newtheorem 的共享计数器下，cleveref 把每个命题都叫作“定理”，这个缺陷由 thmtools 纠正。

逻辑与演绎

关于逻辑与演绎的一课把对象语言与元语言分开，\to 对 \Rightarrow，并介绍符号 \vdash、\models 和 \equiv；把符号类别的原理用于否定的波浪号、集合的竖线和函数的冒号；提出每个联结词一个命令，不带参数时用来更换符号，带参数时用来更换句法；汇集模态符号的宏包；用 array 排真值表；用 bussproofs 构造自然演绎树，其栈的逻辑解释了它的两种错误，并介绍了 Fitch 式方框和标准形式的论证。

下图把五段汇成一条链。中间一列的每个节点是一种机制或一条规则，按彼此依赖的顺序编号，并用弧线连到它所用到的前面的环节；四周浮动的是支撑，即这条链一再求助的原理，每个支撑用实线连到依靠它的环节，用虚线连到确立它的环节，在前几个单元中确立的支撑则画成圆环。点击一个支撑，会突出显示所有用到它的环节；每个环节都链接到讲解它的那一课。

链的支柱

A标签记录什么. 标签记录在它之前、在它所在环境中最后分配的编号，并不知道自己附着在什么上。在上一单元确立。本单元中不加证明而采用。
B自定义命令. 自定义命令为一种功能命名，它的定义在导言区写一次，就决定了它的形式；改动定义就改动整篇文档。在上一单元确立。本单元中不加证明而采用。
C加载顺序. 宏包按读入的顺序加载，后加载的宏包会调整、保留或撤销先加载的宏包所做的事。在上一单元确立。本单元中不加证明而采用。
D符号的类别. 在数学模式中，引擎按每个符号的类别（普通符号、二元运算符、关系符、标点、开符号、闭符号）安排间距，并忽略源代码的空格。确立于: 1. 两种模式.
E无错消失的东西. 在 LuaLaTeX 中，当前字体中没有的符号不会中止编译：它会消失，只在日志中留下一行“Missing character”。确立于: 2. 写错模式的符号.
F一个元素或一组. 下标、上标和参数作用于紧随其后的元素，或作用于花括号中的一组；花括号本身不印出。确立于: 6. 下标与上标.
G对齐就是表格. 对齐环境为每个 \\ 建一行，为两个 & 之间的每一段建一个单元格，即使这一行是空的。确立于: 11. 用 align 对齐.
H树的栈. 有 n 个前提的推理取走栈中最后 n 棵树，返回一棵；如果最后恰好剩下一棵，证明才会印出。确立于: 23. 演绎树.

第 1 段行内公式与行间公式
- 预测一个符号、一个变量或一个词写错模式时的结果。
- 把行内公式和行间公式当作句子的一部分加标点。
- 为行间公式编号并引用它们。
- 按中文科技文献的惯例书写小数和量值，用或不用 siunitx。
1. 两种模式. 在数学模式中，字母是变量，源代码的空格不起作用，间距由每个符号的类别决定，且不允许空行。
  依据: D (符号的类别). 证明于: 行内公式与行间公式.
2. 写错模式的符号. 正文中的 _ 产生“Missing $ inserted”；公式之外的 \alpha 消失或粘连着出现；公式中的一个词是变量之积，要放进 \text 或 \mathrm，二者不能互换。
  使用: 1. 两种模式. 依据: E (无错消失的东西). 证明于: 行内公式与行间公式.
3. 句子中的公式. 行内公式限制自身高度，把句子的标点留在外面；行间公式在内部加标点，不留空行，用 \[…\] 或 equation，绝不用 $$。
  使用: 1. 两种模式. 依据: D (符号的类别). 证明于: 行内公式与行间公式.
4. 编号与引用. equation 编号，其标签放在内部；\eqref 加上括号；\numberwithin 按节编号；\tag 放一个标记而不消耗编号。
  使用: 3. 句子中的公式. 依据: A (标签记录什么). 证明于: 行内公式与行间公式.
5. 小数点与逗号. 公式中的逗号是标点，属于数字的逗号要放进花括号，{,}；点是普通符号；luatexja 和 babel 都不转换它们，siunitx 的约定来自 \sisetup，而不是来自语言设置。
  使用: 1. 两种模式. 依据: D (符号的类别). 证明于: 行内公式与行间公式.
第 2 段符号与记号
- 为下标和上标分组，并预测缺少花括号时少了什么。
- 按学科的约定选择字母表、变体和算子。
- 预见 babel 在算子上的改变：中文文档里没有，西班牙语里很多。
- 在导言区确定文档的记号。
1. 下标与上标. x^10 只把 1 升上去；x^{10} 把整组升上去；同类的两个下标或上标接连出现，产生“Double subscript”或“Double superscript”。
  使用: 1. 两种模式. 依据: F (一个元素或一组). 证明于: 符号与记号.
2. 字母与字母表. 每种字母表表明所命名对象的种类；使用 fontspec 时，\mathbf{\Gamma} 会消失，\mathbf{\alpha} 不会变粗，符号的粗体要用 \boldsymbol。
  使用: 6. 下标与上标. 依据: E (无错消失的东西). 证明于: 符号与记号.
3. 有名称的算子. 算子用直立体排并带有自己的间距；中文文档不加载 babel，什么也不变；西班牙语的 babel 给 \lim、\max、\min 和 \inf 加重音，定义 \sen，不碰 \sin，而 es-minimal 把这些全部取消。
  使用: 6. 下标与上标. 依据: D (符号的类别). 证明于: 符号与记号.
4. 定界符. \left 和 \right 量取所包围的内容，并且成对使用；手动尺寸提供精细控制；mathtools 定义 \abs 这样的成对定界符。
  使用: 6. 下标与上标. 依据: D (符号的类别), F (一个元素或一组). 证明于: 符号与记号.
5. 导言区中的记号. \R、\vect、\dd 或 \abs 只定义一次；unicode-math 放在 amsmath 之后，其后不再加载 amssymb，粗体要用 \symbf。
  使用: 7. 字母与字母表, 8. 有名称的算子, 9. 定界符. 依据: B (自定义命令), C (加载顺序), E (无错消失的东西). 证明于: 符号与记号.
第 3 段多行公式
- 用 align 对齐等式串和方程组，把 & 放在关系符之前。
- 决定哪些行编号，并预测编号。
- 按结构和整体的编号选择环境。
- 排分段定义、矩阵和插入的文字。
1. 用 align 对齐. & 放在关系符之前，\\ 开启一行；=& 和多余的 & 会无声地改变结果，空行则中止编译。
  使用: 3. 句子中的公式. 依据: G (对齐就是表格), D (符号的类别). 证明于: 多行公式.
2. 哪些行编号. align 给每一行编号，包括末尾的 \\ 留下的空行；\notag 去掉编号而不消耗它，这一行上的标签记录的是下一个编号行的编号。
  使用: 11. 用 align 对齐, 4. 编号与引用. 依据: G (对齐就是表格), A (标签记录什么). 证明于: 多行公式.
3. 整体一个编号. equation 中的 split 给等式串一个编号；aligned 和 gathered 是不编号的块；subequations 给一组公式加字母，整组只消耗一个编号。
  使用: 11. 用 align 对齐, 12. 哪些行编号. 依据: A (标签记录什么). 证明于: 多行公式.
4. 分段、矩阵与文字. cases 有两列，把多余的 & 变成行尾；dcases 按行间公式的尺寸排版；矩阵允许十列；array 能画竖线；\intertext 不打断对齐。
  使用: 11. 用 align 对齐. 依据: G (对齐就是表格). 证明于: 多行公式.
第 4 段定理与证明
- 声明命题及其样式和计数器。
- 预测共享或独立系列的编号。
- 让证明的结束符号落在正确的位置。
- 用名称引用命题。
1. 声明的命题. amsthm 的 \newtheorem 写在导言区，规定标题、编号和外观；标题由作者书写，带星号的形式不编号。
  依据: B (自定义命令). 证明于: 定理与证明.
2. 计数器与样式. [thm] 构成单一系列，编号表明位置；[section] 或 [chapter] 按章节编号；plain、definition 和 remark 分别对应所断言的、所规定的和起伴随作用的内容。
  使用: 15. 声明的命题. 依据: B (自定义命令). 证明于: 定理与证明.
3. 证明. proof 的标题来自 \proofname，luatexja 不定义它，要自己设为“证明”；方块放在最后一段的末尾；若证明以公式或列表结束，\qedhere 把它放到位，旁边有编号时除外。
  使用: 15. 声明的命题, 11. 用 align 对齐. 证明于: 定理与证明.
4. 引用命题. 标签放在环境内部；amsthm 在 cleveref 之前加载，每个环境一个 \crefname；在 \newtheorem 的共享计数器下，一切都叫“定理”，thmtools 纠正这一点。
  使用: 16. 计数器与样式, 4. 编号与引用. 依据: A (标签记录什么), C (加载顺序). 证明于: 定理与证明.
第 5 段逻辑与演绎
- 在记法中区分对象语言与元语言。
- 纠正波浪号、竖线、冒号和量词的间距。
- 在导言区更换传统。
- 构造并调试演绎树、真值表和论证。
1. 语言的两个层次. \to 是对象语言的联结词，\Rightarrow 是元语言的箭头；\vdash 断言可推演，\models 断言语义后承。
  使用: 8. 有名称的算子. 证明于: 逻辑与演绎.
2. 逻辑的间距. \sim 是关系符，要放进花括号；键盘上的竖线是普通符号，\mid 是关系符；: 是关系符，\colon 是标点；量词的辖域由括号决定。
  使用: 19. 语言的两个层次, 5. 小数点与逗号. 依据: D (符号的类别). 证明于: 逻辑与演绎.
3. 每个联结词一个命令. 不带参数时，命令把符号从一种传统换成另一种；带参数时，定义还决定顺序和括号，并能写出波兰记法。
  使用: 20. 逻辑的间距, 10. 导言区中的记号. 依据: B (自定义命令), F (一个元素或一组). 证明于: 逻辑与演绎.
4. 模态符号与真值表. \Box、\Diamond 和 \vDash 需要 amssymb，先加载的 latexsym 会改变菱形；真值表是一个 array，其中 T 和 F 用直立体。
  使用: 19. 语言的两个层次, 14. 分段、矩阵与文字. 依据: C (加载顺序), G (对齐就是表格). 证明于: 逻辑与演绎.
5. 演绎树. 在 bussproofs 中，\AxiomC 放一片叶子，推理取走最后的几棵树；树不够时报“Hypotheses missing!”，树多余时在印出时报“Proof tree badly specified.”。
  使用: 19. 语言的两个层次. 依据: H (树的栈). 证明于: 逻辑与演绎.
6. 方框与标准形式. logicproof 把 Fitch 式方框排成带 subproof 的表格；标准形式的论证给前提编号，并用一条横线和 \therefore 隔开结论。
  使用: 23. 演绎树, 22. 模态符号与真值表. 依据: G (对齐就是表格). 证明于: 逻辑与演绎.

走向表格与图形. 这条链停在公式、命题和演绎都已完整并编号之处：表格在这里只服务于矩阵、真值表和证明，到下一单元将成长为文档中的表格与图形，带有题注、编号和在页面上的位置。