逻辑学
研究哪些结论确实能从哪些假设中得出的学问。
逻辑学研究推理的形式而非内容。形式逻辑用符号代替语句，于是结论是否成立仅凭论证的形式即可判定，并可由机器检验。
逻辑词典
计算器、指南和练习用到的全部术语，集中定义在一处。
查一个术语，看它的记号，再把示例在计算器里打开，看它如何运作。本词典收录的术语在指南中首次出现时会被标出。
全部 62 个术语
基础概念
命题
非真即假、不能既真又假的陈述。
命题是恰好具有一个真值的陈述句。“正在下雨”是命题；疑问句或祈使句不是，因为它们没有可真可假的内容。
真值
⊤ / ⊥命题可取的两个值之一：真或假。
经典逻辑给每个命题恰好一个真值，记作 ⊤ 与 ⊥（或 1 与 0）。真值表的每一行就是对变元的一次赋值，以及公式在该赋值下的取值。
原子命题
内部不含任何联结词的命题。
原子命题不能再分解为更小的命题：其中没有否定、合取或其他联结词。其余都是复合命题，由原子搭建而成，真值由原子的真值决定。
命题变元
像 p 或 A 这样代表任意命题的字母。
命题变元是任意命题的占位符。计算器把单个字母当作变元，为每个变元在真值表中留一列，并为每种可能的取值组合留一行。
在计算器中p → q合式公式
语言的语法确实允许的符号串。
合式公式按规则构造：变元是合式公式，由较小的公式经联结词组成的也是。“p ∧ ∨ q”不是，因此计算器报错而不去猜测。
解释
对公式中所有变元的一次真值指派。
一个解释说明每个变元取什么值，从而确定整个公式的取值。含 n 个变元的公式有 2ⁿ 个解释，恰好就是其真值表的各行。
论证
为支持某个结论而提出的一组前提。
论证主张其结论可由前提推出。在计算器中用推出符号写下来——前提在前、结论在后——每一行都会被检查，看是否存在前提为真而结论为假的情形。
在计算器中p → q, p ⊨ q前提
论证为得出结论而假定的陈述。
前提是论证的出发点。有效性只问：在所有前提为真之处，结论是否也为真；前提是否真的成立是另一个问题，那正是可靠性所补充的。
在计算器中p → q, p ⊨ q结论
论证试图确立的陈述。
结论是前提所要支持的东西。在计算器中它是推出符号之后的表达式；当没有任何解释使前提为真而结论为假时，论证有效。
在计算器中p → q, p ⊨ q联结词
联结词
把较简单的命题组成复合命题的符号。
¬、∧、∨、→、↔ 这样的联结词把命题组成更大的命题，其真值只取决于成分命题的真值。真值表记录的正是这种依赖关系，每种输入组合一行。
否定
¬翻转真值：¬p 恰在 p 为假时为真。
否定是命题逻辑中唯一的一元联结词。写作 ¬p、~p 或 !p，它把真变假、把假变真，所以否定两次就回到原命题。
在计算器中¬p合取
∧只有两部分都为真时才为真：p ∧ q。
合取同时断定它的两个部分，即两个合取项。它在真值表中恰有一行为真——两个合取项都为真的那一行——因而是最严格的二元联结词。
在计算器中p ∧ q析取
∨至少一部分为真时即为真：p ∨ q。
逻辑中的析取是相容的：p 为真、q 为真、两者都为真时，p ∨ q 都为真。“或”的排斥读法只在两部分不同时为真，那是另一个联结词。
在计算器中p ∨ q排斥析取
⊕两个命题中恰有一个为真时才为真。
排斥析取记作 ⊕ 或 XOR，当两部分不同时成立，相同时不成立。它是双条件的否定，也可写成 (p ∨ q) ∧ ¬(p ∧ q)。
在计算器中(p ∨ q) ∧ ¬(p ∧ q)条件式
→p → q，只有 p 真而 q 假时才为假。
实质条件式说的不过是“并非前件真而后件假”，因此只要前件为假它就自动成立。这正是 p → q 等值于 ¬p ∨ q 的原因。
在计算器中p → q双条件式
↔p ↔ q，两部分真值相同时为真。
双条件式以彼此为条件断定两边：两部分同为真或同为假时它为真。若一个双条件式是重言式，它恰好表达一条逻辑等值。
在计算器中p ↔ q前件
条件式中“如果”的部分——p → q 里的 p。
前件是条件式所依赖的条件。前件为假时，无论后件如何，整个条件式都为真——→ 的真值表里多数令人意外之处都出自于此。
在计算器中p → q后件
条件式中“那么”的部分——p → q 里的 q。
后件是条件式声称在前件成立时随之成立的东西。后件为真使条件式为真，却不使前件为真：这样推断是一种形式谬误。
在计算器中p → q逆命题
把条件式两部分对调：q → p。
p → q 的逆命题是 q → p，两者并不等值：计算器会找到一行使其一成立而另一不成立。把它们当作可互换，就是肯定后件。
在计算器中q → p逆否命题
¬q → ¬p，其真值始终与 p → q 相同。
逆否命题把条件式的两部分都否定并对调。与逆命题不同，它与原式确实等值，因此数学中的逆否证明是正当的。
在计算器中(p → q) ≡ (¬q → ¬p)与非
↑合取的否定：除非两个输入都为真，否则为真。
与非记作 ↑，即 ¬(p ∧ q)。它是功能完备的：任何其他联结词都可仅用与非搭建，因此它是数字电路设计的主力。
在计算器中¬(p ∧ q)或非
↓析取的否定：只有两个输入都为假时才为真。
或非记作 ↓，即 ¬(p ∨ q)。与“与非”一样，它单独就是功能完备的，因此一个电路可以完全由或非门搭成。
在计算器中¬(p ∨ q)运算优先级
省略括号时哪个联结词先起作用。
否定结合最紧，其次是合取、析取、条件式，最后是双条件式。于是 ¬p ∧ q ∨ r 读作 ((¬p) ∧ q) ∨ r；当想要的读法不同时，用括号改变次序。
在计算器中¬p ∧ q ∨ r真值与推出
真值表
每种赋值一行，并给出公式在该行的取值。
真值表列出公式 n 个变元的全部 2ⁿ 个解释，并算出公式在每个解释下的取值。因为穷尽无遗，它能解决命题逻辑中的一切语义问题：等值、有效、可满足等等。
在计算器中p → q重言式
⊤在任何解释下都为真的公式。
重言式在真值表的每一行都为真，因而对世界一无所述：无论 p 是什么，p ∨ ¬p 都为真。两个公式等值，恰当它们之间的双条件式是重言式。
在计算器中p ∨ ¬p矛盾式
⊥在任何解释下都为假的公式。
像 p ∧ ¬p 这样的矛盾式在真值表的每一行都为假。从一组假设推出矛盾，就表明这些假设不能同时成立——这正是归谬证明的动力。
在计算器中p ∧ ¬p可真式
在有些解释下为真、在另一些解释下为假的公式。
可真式既非重言式也非矛盾式：它的真值表至少有一行为真、也至少有一行为假。人们写下的公式大多如此，这也正是它们有信息量的原因。
在计算器中p ∧ q可满足性
是否存在使公式为真的解释。
当公式真值表中至少有一行为真时它是可满足的，那一行就是它的一个模型。判定可满足性是 SAT 求解器的核心问题，也因此是大量自动推理的核心。
在计算器中p ∧ (p → q)逻辑等值
≡真值表完全相同的两个公式。
等值公式在任何解释下取值一致，因此可以处处相互替换而不改变所说的内容。在两个表达式之间写上等号，计算器就会逐行比较它们的列。
在计算器中(p → q) ≡ (¬p ∨ q)逻辑推论
⊨在前提成立的每个解释中结论也成立。
记作 Γ ⊨ φ，逻辑推论正是有效论证所主张的东西。检验方式是寻找反例：使所有前提为真而结论为假的解释。若不存在，推论关系成立。
在计算器中p → q, p ⊨ q有效性
没有任何解释使前提为真而结论为假。
有效性是论证形式的性质而非事实的性质：有效论证可以有假前提和假结论。它不可能有的，是真前提配上假结论。
在计算器中p → q, p ⊨ q可靠性
前提也确实为真的有效论证。
可靠性在形式主张之外再加一个事实主张：论证有效，且其前提成立。前一半单靠逻辑即可判定；后一半属于论证所谈论的那件事。
反模型
使前提为真而结论为假的解释。
反模型证明论证无效——一行就够。计算器会显示它找到的那一行，把“这推不出来”变成可以手工核对的具体赋值。
在计算器中p → q ⊨ q → p一致性
存在解释使集合中所有陈述同时为真。
当一组前提能够同时成立时，它是一致的。不一致的前提可以推出任何东西，因此建立在其上的论证在技术上有效，却毫无价值。
在计算器中p → q, ¬q ⊨ ¬p范式
文字
一个变元或它的否定，例如 p 或 ¬p。
文字是范式的原子：子句是文字的析取，极小项是文字的合取。变元不带否定时文字为正，带否定时为负。
在计算器中¬p子句
文字的析取，例如 p ∨ ¬q ∨ r。
子句是合取范式所由构成的一个个括号组。由于合取只有在每一部分都为真时才为真，CNF 公式恰在其所有子句都成立时成立。
在计算器中p ∨ ¬q ∨ r析取范式
“与”的“或”：文字合取式的析取。
每个公式都有析取范式，而且可以直接从真值表读出：每个为真的行给出一个合取式，用 ∨ 连接起来。计算器还给出最简析取范式，用更少的文字说同一件事。
在计算器中(p ∧ q) ∨ (¬p ∧ r)合取范式
“或”的“与”：子句的合取。
合取范式从真值表为假的行读出，每行一个子句。这是 SAT 求解器期待的输入格式，因此化为 CNF 是自动推理中的例行步骤。
在计算器中(p ∨ q) ∧ (¬p ∨ r)极小项
恰好指定真值表中一行的合取式。
极小项把每个变元都提到一次，或否定或不否定，因此恰有一个解释满足它。把为真各行的极小项收集起来并用 ∨ 连接，就得到公式的析取范式。
在计算器中p ∧ ¬q ∧ r极大项
恰好排除真值表中一行的析取式。
极大项把每个变元都提到一次，且只在一个解释下为假。取每个为假行的极大项并用 ∧ 连接，就得到公式的合取范式。
在计算器中p ∨ ¬q ∨ r德摩根定律
否定把 ∧ 变成 ∨、把 ∨ 变成 ∧：¬(p ∧ q) ≡ ¬p ∨ ¬q。
德摩根定律把否定推入合取或析取内部，并在途中翻转联结词。公式因此被推向范式，代码与电路中的否定也因此得以化简。
在计算器中¬(p ∧ q) ≡ ¬p ∨ ¬q双重否定
否定两次回到原式：¬¬p ≡ p。
在经典逻辑中双重否定两个方向都成立，所以 ¬¬p 与 p 总可互换。直觉主义逻辑只保留从 p 到 ¬¬p 的方向，两种系统就在这里分道扬镳。
在计算器中¬¬p ≡ p布尔代数与电路
布尔代数
两个值的代数，运算为 ∧、∨ 和 ¬。
布尔代数就是写成 0 与 1 上算术的命题逻辑，其交换律、分配律、吸收律和德摩根定律使表达式可以改写与化简。数字电路正是用这套数学设计的。
在计算器中(p ∧ q) ∨ (p ∧ ¬q) ≡ p卡诺图
把真值表排成网格，使化简一目了然。
卡诺图这样排列各行：相邻格子只差一个变元，且边缘首尾相接。它也写作 K 图、K-map 或 kmap。大小为 1、2、4 或 8 的相邻 1 组成的矩形块，可直接读作最简表达式中的项。
在计算器中(p ∧ q) ∨ (p ∧ ¬r)素蕴涵项
图上无法再扩大的一个方块组。
蕴涵项是使公式必为真的文字合取；若去掉任何一个文字就不再如此，它便是素的。在卡诺图上，素蕴涵项就是由 1 组成的极大矩形。
必要素蕴涵项
覆盖某个 1 的唯一素蕴涵项。
当图上某个 1 只属于一个极大方块组时，该组必定出现在任何最小覆盖中，因此先取。剩下的部分才是真正需要搜索的覆盖。
逻辑门
对输入计算一个联结词的电路元件。
与门、或门、非门、与非门、或非门和异或门是联结词在硬件中的对应物。公式与电路是同一对象的两种画法，因此计算器可以把表达式画成门电路图。
在计算器中(p ∧ q) ∨ ¬r证明与推理
推理规则
从已得公式走到新公式的合法一步。
推理规则是像肯定前件这样的模式，只要手头有恰当形式的公式即可使用。证明系统由少数几条这样的规则搭成，其选择保证只能推出真正成立的结论。
肯定前件
由 p → q 和 p 推出 q。
肯定前件是条件式的基本规则：给定一个条件式及其前件，后件随之成立。它的有效性在真值表中一目了然——两个前提都为真的唯一那行，结论也为真。
在计算器中p → q, p ⊨ q否定后件
由 p → q 和 ¬q 推出 ¬p。
否定后件反向走过条件式：后件不成立，前件就不可能成立。这是逆否命题在起作用，也是一切通过检验预测来反驳假说的论证的形式。
在计算器中p → q, ¬q ⊨ ¬p假言三段论
由 p → q 和 q → r 推出 p → r。
假言三段论把条件式串接起来，这正是长推导得以可能的原因：每一环都把论证推进一步，而无需断定任何前提。
在计算器中p → q, q → r ⊨ p → r析取三段论
由 p ∨ q 和 ¬p 推出 q。
析取三段论排除已被否定的一支：两种可能之一成立，而第一种不成立，那么第二种必定成立。这正是排除法推理背后的规则。
在计算器中p ∨ q, ¬p ⊨ q自然演绎
逐步应用推理规则来证明结论。
自然演绎用每个联结词的引入与消去规则从前提推出结论，允许作出临时假设并在之后解除。它证明真值表所检验的东西，却无需遍历每一行。
归谬法
假设反面、推出矛盾，从而断定原命题。
要证明 φ，先假设 ¬φ，再推出形如 ψ ∧ ¬ψ 的东西。既然没有解释能使矛盾为真，假设便不能成立，φ 随之得证。无理性与无穷性的证明通常就是这样进行的。
在计算器中p ∧ ¬p肯定后件
从 p → q 和 q 推到 p 的无效一步。
后件为真并不确立前件：造成它的可能另有其事。计算器会给出反模型——p 假、q 真——正是这一行把它与肯定前件区分开来。
在计算器中p → q, q ⊨ p否定前件
从 p → q 和 ¬p 推到 ¬q 的无效一步。
条件式对前件不成立时会发生什么只字未提，所以排除前件仍让后件悬而未决。反模型就是 p 为假而 q 为真的那一行。
在计算器中p → q, ¬p ⊨ ¬q命题逻辑之外
谓词逻辑
深入命题内部、考察对象及其性质的逻辑。
谓词逻辑增加了谓词、项和量词，于是“每个大于二的素数都是奇数”成为一个公式而非一个字母。它的表达力严格强于命题逻辑，任何真值表都无法判定它。
量词
∀ / ∃说明谓词对多少对象成立的符号。
两个经典量词是 ∀（所有）与 ∃（至少一个），每一个都是另一个加上内外否定后的结果。量词所约束的变元，正是谓词逻辑区别于命题逻辑之处。
全称量词
∀∀x φ：φ 对论域中每个对象都成立。
全称断言被单个反例推翻，而在空论域上空洞地成立。∀x φ 等值于 ¬∃x ¬φ，这正是德摩根定律在量词上的对应物。
存在量词
∃∃x φ：φ 对论域中至少一个对象成立。
存在断言只要举出一个见证即可确立。∃x φ 等值于 ¬∀x ¬φ，因此两个量词都可以由另一个连同否定来定义。
模态逻辑
□ / ◇以“必然”（□）和“可能”（◇）扩充的逻辑。
模态逻辑在可能世界而非单一解释中给公式赋值：当 φ 在每个可通达世界都成立时 □φ 成立，当它在某个世界成立时 ◇φ 成立。改变“可通达”的含义，就得到不同的模态系统。