逻辑与演绎 · Topos Uranos

摘要

本课讲授如何用 LaTeX 书写逻辑，使之同样适用于学习数学、计算机科学或哲学的人。它区分对象语言的联结词与元语言的箭头，介绍各联结词及其变体、其他传统的记法（马蹄形、波浪号、圆点和波兰记法），以及为每个联结词定义专用命令的好处；确定量词的间距；排版描述法表示的集合，并说明键盘上的竖线与 \mid 为何间距不同；汇集元逻辑、相继式和模态逻辑的符号，并指出定义各符号的宏包；用 array 排版真值表；用 bussproofs 构造自然演绎树（其栈的逻辑可以解释它的错误），用 logicproof 构造 Fitch 式方框；以带编号前提和结论的标准形式陈列论证；最后讲哪些做法应当避免，并附上每种错误的真实日志。

学习目标

根据公式所断言的内容，在对象语言的联结词与元语言的箭头之间、在 \models、\vdash、\equiv 与 \Leftrightarrow 之间作出选择。
预测量词、描述法集合以及波浪号否定的间距，并改正那些不产生任何警告的疏忽。
为每个联结词定义一个命令，并说明它允许哪种传统的转换、不允许哪种。
跟踪 bussproofs 栈的状态来构造自然演绎树，并根据日志诊断其中的错误。
排版真值表和标准形式的论证，并为给定的证明在树与 Fitch 式方框之间作出选择。

语言的两个层次

逻辑文本总是在两个层次上说话。一是对象语言，即所研究的公式的语言，有它的联结词和量词；二是元语言，即作者的语言，它对这些公式作出断言：某个公式可由另一些公式推出，两个公式等值，某个公式在每个模型中都真。记法必须把两个层次分开，因为放错位置的箭头不是排印上的疏忽，而是另一个断言。本课以符号与记号一课中的符号和算子、定理与证明一课中的环境为前提；这里研究逻辑特有的内容。想了解这些记法所表达的理论，可以学习课程数理逻辑 I：命题逻辑。