翻译-Introduction À La Logique-教材01

$$ %{\rm \LaTeX}\text{ Definitions are here. } \newcommand{\hl}[2][yellow]{\bbox[#1]{\vph{fg()}#2}} % 高亮 \newcommand{\cl}[1][Green]{\color{#1}} \def\setLan{\mathcal{L}} % 词汇表 \def\setVar{\mathcal{V}} % 变量集 \def\setTrm{\mathcal{T}} % 项集 \def\setFml{\mathcal{F}} % 公式集 \def\setAtm{\mathcal{Atom}} % 原子公式 \def\setCal{\mathcal{C}} % 演算 \let\ph=\phantom \let\hph=\hphantom \let\vph=\vphantom \let\ttt=\texttt \def\setVarLib{{\rm VL}} % 自由变量集 % \def\Hypo{{\rm\Gamma}} \def\pillar#1{\vph{(fg)}\smash{#1}} % 推理规则 \def\axm{\pillar{\rm ax}} \def\aff{\pillar{\rm aff}} \def\intrTo{\pillar{\to_{\rm i}}} \def\elimTo{\pillar{\to_{\rm e}}} \def\intrCon{\pillar{\land_{\rm i}}} \def\elimConL{\pillar{\land_{\rm e}^{\rm g}}} \def\elimConR{\pillar{\land_{\rm e}^{\rm d}}} \def\intrDisL{\pillar{\lor_{\rm i}^{\rm g}}} \def\intrDisR{\pillar{\lor_{\rm i}^{\rm d}}} \def\elimDis{\pillar{\lor_{\rm e}}} \def\intrNeg{\pillar{\lnot_{\rm i}}} \def\elimNeg{\pillar{\lnot_{\rm e}}} \def\clssBot{\pillar{\bot_{\rm c}}} \def\intrAll{\pillar{\forall_{\rm i}}} \def\elimAll{\pillar{\forall_{\rm e}}} \def\intrExt{\pillar{\exists_{\rm i}}} \def\elimExt{\pillar{\exists_{\rm e}}} \def\intrEql{\pillar{=_{\rm i}}} \def\elimEql{\pillar{=_{\rm e}}} % 派生规则 \def\Coupure{\pillar{\textrm{coup}}} \def\ConL{\pillar{\land_{\rm g}}} \def\DisL{\pillar{\lor_{\rm g}}} \def\ToL{\pillar{\to_{\rm g}}} \def\NegL{\pillar{\lnot_{\rm g}}} \def\AllL{\pillar{\forall_{\rm g}}} \def\ExtL{\pillar{\exists_{\rm g}}} \def\BotIntu{\pillar{\bot_{\rm i}}} \def\LPeirce{\pillar{\textrm{l.p.}}} \def\TierExc{\pillar{\textrm{t.e.}}} \def\ContPos{\pillar{\textrm{c.c.}}} \def\EqlLA{\pillar{=_{\rm g}}} \def\EqlLB{\pillar{='_{\rm g}}} \def\EqlC{\pillar{=_{\rm c}}} \def\morgCon{\pillar{\land_{\rm m}}} \def\morgDis{\pillar{\lor_{\rm m}}} \def\morgTo{\pillar{\to_{\rm m}}} \def\morgAll{\pillar{\forall_{\rm m}}} \def\morgExt{\pillar{\exists_{\rm m}}} % 错误规则 \def\errr{\pillar{\rm !!!}} % 文字高亮 \def\Hprev#1{{\cl[ForestGreen]{#1}}} \def\Hnext#1{{\hl[LightBlue]{#1}}} \def\EQprev#1{{\cl[YellowOrange]{#1}}} \def\EQnext#1{{\hl[pink]{#1}}} \def\Omis#1{{\color{Gray}#1}} % \def\indent{\ph{\ttt{00}}} % 缩进 % \def\inj#1{\textrm{Inj}[#1]} % 单射 \def\surj#1{\textrm{Surj}[#1]}% 满射 \def\bij#1{\textrm{Bij}[#1]} % 双射 \def\inv#1{\textrm{Inv}[#1]} % 对合 % \def\deduct#1{\mathcal{#1}} % 推导 \def\trou#1{\langle #1\rangle} % 带洞公式 % \def\setAxm{\mathcal{A}} % 公理集 \def\setRgl{\mathcal{R}} % 规则集 \def\hilbTo{R_\to} % 希尔伯特规则 : 箭头 \def\hilbAll{R_\forall} % 希尔伯特规则 : 全称量词 \def\hilbExt{R_\exists} % 希尔伯特规则 : 存在量词 $$

1.1 简介 Introduction

在（代数、分析、几何等）数学课上 我们推演各种数学对象（整数，实数，矩阵，数列，连续函数，曲线等）的性质。 为了能证明这些性质，我们应先确保所研究的数学对象是良定义的（整数是什么？实数是什么？等等）。

而在一阶逻辑 Logique du Premier Ordre ——尤其是在推演理论 注：也称作证明论 里， 我们研究的数学对象则是逻辑公式 Formule 及其对应的推演 Démonstration。正因如此， 我们有必要对这些数学对象给出精确的定义。项和公式共同构成了语言的语法，其极度简洁，允许我们 表达无歧义不迂回的内容。

• 项 Termes：即数学性质中提到的数学对象。

  • 在代数中项可以是群（或环、域、线性空间等）中的元素。 有时我们也需要操纵这些元素构成的集合（如子群、线性子空间等）。 描述这些数学对象的项被称作二阶项 Termes du Second Ordre。 在第 6 章之前我们暂时先不考虑这些东西。

  • 在分析中项可以是实数或（函数空间中的）函数。

• 公式 Formules：描述了待研究数学对象所具有的性质。

  • 在代数中公式可以用来描述两个元素的运算满足交换律， 或者是线性子空间的维数等于 $3$，等等。

  • 在分析中公式可以用来描述函数的连续性，数列的收敛性，等等。

  • 集合论中公式可以用来描述两个集合的包含关系， 或者是某个元素属于某个集合，等等。

• 推演 Démonstrations：允许我们确定一个逻辑公式为真 Vraie。 “真”这个词本身的精确定义也需要被定义（见第 2 章）。更准确地说， 推演是一种基于假设的推导，允许我们“从真得出真”；在此过程中 结论的真实性这一问题被转移到了假设上，假设的真实性不依赖于逻辑， 而是取决于我们对所讨论事物的认知。

  正如域是数的形式化，推演是我们在数学中常进行的推理的形式化。

注意：本章仅讨论一阶逻辑中公式和推演的语法 Syntaxe —— 意味着不会出现“真 Vrai”和“假 Faux”这样的词。 真值（称作语义 Sémantique）则会在下一章中详细介绍。 当然，想读懂一个公式或理解一个推演，我们还需要为其赋予某种“意义”； 但这种意义并不属于我们的研究范围。一台计算机（可能完全不理解自己在做什么） 可以毫无障碍地操作关于群、线性空间等数学对象的定理的推演， 并且无需在头脑中保留任何用来支撑直觉的实例。当然， 我们会在本章的例子中引入这样的直觉， 但请记住：这么做的目的仅仅是为了帮助理解。

本章我们还会推导出一些与项、公式和推演有关的重要结论， 这意味着我们会写出一些描述这些数学对象的公式（称作元公式 Méta-Formules） 并进行相应的元推演 Méta-Démonstrations。

另外注意：可别把 项、公式、推演所在的层次和 元公式、元推演所在的层次给弄混了。

为了方便读者区分这两个层次，我们将使用下表中的对应关系 来指派“对象”层次和“元”层次中相关概念的词汇。

在大部分情况下我们也会保留对象层级的记号。比如， 我们不会在元层面上用 $\forall$ 表示“对任意…”。

1.2 公式 les Formules

1.2.1 语言 le Langage

对于不同的数学领域我们会使用不同的语言，这些语言 因其所使用的符号而彼此区分（见 1.2.例子.2） 。 下面的定义阐述了一个简单事实：只需给出一串符号列表 便可描述一门语言。

我们有时也用词汇表 Vocabulaire 或者是签名 Signature 来指代语言。

术语谓词 Prédicat 也可以用来表示关系。我们有时也会用 谓词演算 Calcul des Prédicats 来指代一阶逻辑 Logique du Premier Ordre。

1.2.2 项 les Termes

接下来我们会提供一个无限集合 $\setVar$， 其包含了所有变量符号 Symboles des Variables。 变量可以是 $x$，$y$，$z$，$\ldots$（也可以带脚标：$x_1$，$\ldots$）。

项 Termes（默认为一阶的 du Premier Ordre） 代表与语言中的对象。准确来说是：

1.2.3 公式 les Formules

逻辑公式由原子公式 Atomiques 通过 连结词 Connecteurs 和 量词 Quantificateurs 构造形成。我们会使用下列连结词和量词：

• 一元连结词：$\lnot$，读作非 Non。
• 二元连结词：
  • $\land$，读作且 Et。想想 $x \in A \cap B$，其含义为 $x \in A$ 且 $x \in B$。
  • $\lor$，读作或 Ou。想想 $x \in A \cup B$，其含义为 $x \in A$ 或 $x \in B$。
  • $\to$，读作蕴含 Implique 或箭头 Flèche。
• 量词：
  • $\exists$，读作会存在 Il Existe
  • $\forall$，读作对所有 Pour Tout。

上述连结词记法是标准记法，使用它们是为了避免 公式（本书所研究的对象层面）与 日常语言（元语言层面） 之间产生混淆。

你或许会发现某些逻辑书籍采用下述记法：

• $\to$ 会被记作 $\supset$。结论可看作是假设的子集。
• $\forall$ 会被记作 $\bigwedge$。它是且的推广。
• $\exists$ 会被记作 $\bigvee$。它是或的推广。

逻辑连结词的选择是相对随意的，我们可以选择其他连结词。比如可以添加 $\leftrightarrow$（表示逻辑等价）或者是 $\uparrow$（Sheffer 竖线 Sheffer Stroke，在电路中尤其常用），等等。

和项一样，我们将对公式的尺寸使用递归定义概念（或证明结论）。

最后一点便是对公式的尺寸进行递归定义（或归纳证明）的具体描述。

1.2.4 自由变量和约束变量 Variables Libres et variables Liées

引入量词 $\forall$ 和 $\exists$ 后 会带来两个与变量命名相关的问题。

1. 例如，通常我们会认为 公式 $\forall x~(x \cdot z = z \cdot x)$ 和 公式 $\forall y~(y \cdot z = z \cdot y)$ 相同并认为 公式 $\forall x~(x \cdot y = y \cdot x)$ 和 公式 $\forall x~(x \cdot z = z \cdot x)$ 不同，因为 前者表达了对象 $y$ 的某个性质，而 后者表达了对象 $z$ 的某个性质。 这意味着我们认为两个公式在对某些变量（称作 约束变量 Variables Liées 或 哑变量 Variables Muettes） 进行重命名操作后是等价的， 因此我们实际上是在一个商集中工作。 这在数学中非常常见， 但要形式化定义该等价关系并不像想象中那么简单。 公式 $\forall x~(x \cdot z = z \cdot x)$ 和 公式 $\forall z~(z \cdot z = z \cdot z)$ 并不相同： 我们不能直接把 $x$ 替换为 $z$！

2. 我们经常需要在另一个项或公式中将某个变量 替换（或代换 Substituer）为某个项。例如， 如果已经定义 $Z[z] : \forall x~(x \cdot z = z \cdot x)$ 并且想要写出 $Z[2x]$， 那么我们就需要重命名约束变量 $x$ 并写下 $\forall y~(y \cdot 2x = 2x \cdot y)$。

为了不让本章的阅读变得过于乏味，我们 不会形式化这两个概念（重命名和代换）， 而是只给出非正式定义 并依托读者对这些概念的直觉理解—— 因为我们在数学中经常会操作这些概念。

我们也可以用下述方式定义这些概念：

1. 公式 $F$ 中变量 $x$ 的一个 出现 Occurence 是 该变量在公式 $F$ 中的一个位置。不要将其与变量本身这个对象混淆。
2. 公式 $F$ 中变量 $x$ 的一个出现是 约束的 Liées（或 哑的 Muette） 当且仅当在通向该出现所处叶子的分支中 存在 $\forall x$ 或 $\exists x$， 否则该出现便是 自由的 Libre。
3. 变量 $x$ 在公式 $F$ 中是自由的当且仅当其至少有一次自由出现。 哑变量或约束变量是指出现在公式中但非自由的变量。下述陈述留作习题： 变量 $x$ 在公式 $F$ 中是自由的当且仅当 $x \in \setVarLib(F)$。

1.2.5 代换 Substitutions

公式 $F[x]$ 代表了对象 $x$ 的某个性质。 我们希望能够在 $F$ 中将变量 $x$ 替换为项 $t$（也称为将 $t$ 代换到 $x$ 中）， 这个操作记作 $F[x := t]$（或者更简单地记作 $F[t]$——如果上下文足够清晰的话）。 这会导致两个困难：

1. 很明显只有 $x$ 的自由出现才可以被替换。 假如 $F[x]$ 为公式 $(\forall x~ x^{2} > 0) \land (x < 1)$。 那么 $F$ 的含义是“所有元素的平方均为正数，并且对象 $x$ 小于 $1$”。 如果 $t = \sin(y)$， 那么 $F[t]$ 的含义是“所有对象的平方均为正数，并且 $\sin(y)$ 小于 $1$”。 将 $F[t]$ 写作公式 $(\forall x~\sin^{2}(y) > 0) \land \sin(y) < 1$”并不符合我们的预期； 而将其写作 $(\forall\sin(y)~\sin^{2}(y) > 0) \land \sin(y) < 1$ 就更糟了！ （ $\forall$ 后面只能有变量。）
2. 这里同样存在捕获问题。 一个学生清楚地知道： 如果函数 $f$ 被定义为 $f(x) = \int_{0}^{1} e^{(x+y)^{2}}~dy$， 那么 $f(y^{2})$ 并不是 $\int_{0}^{1} e^{(y^{2}+y)^{2}}~dy$， 而应该是 $\int_{0}^{1} e^{(y^{2}+z)^{2}}~dz$。 为了避免变量 $y$（在结果中当然应为自由变量）被积分符号所捕获， 有必要对变量名进行更改。 下面的例子与刚才的问题完全相同： 如果 $F[x]$ 为 $\forall y~(y \cdot x = x \cdot y)$， 那么 $F[y^{-1}]$ 并不是 $\forall y~(y \cdot y^{-1} = y^{-1} \cdot y)$， 而应该是 $\forall z~(z \cdot y^{-1} = y^{-1} \cdot z)$。

1.2.6 命题演算 Calcul Propositionnel

如果语言中的关系符号都是零元关系符号（甚至连 $=$ 符号都没有）， 那么量词便变得无用（因为公式中不可能包含变量）。 于是我们便得到了命题演算 Calcul Propositionnel， 其定义如下：

1.3 使用自然推演描述推演 les Démonstrations en Déduction Naturelle

1.3.1 简介 Introduction

数学教材（尤其是本书）中的推演是由数学符号和包含“关键词”的短语组成的，例如：

• 因此 donc，
• 由于 parce que，
• 如果 si，
• 当且仅当 si et seulement si，
• 必有 il est nécessaire que，
• 只需 il suffit de，
• 任取一 $x$ 满足 prenons un $x$ tel que，
• 假设 supposons que，
• 取如下反例 chercons une contrdiction，

等等；这些短语被假定会被所有人以相同的方式理解，但并非总是如此。 例如我们稍后会看到“取某个 $x$ 满足”这一表达 可能有两种截然不同的含义， 而一旦弄错可能会造成非常严重的问题。

在书籍或课程中，推演的目的是说服读者相信该命题的真实性。 根据读者的水平，推演会有不同的详细程度： 在硕士课程中被认为显而易见的东西 在学士课程中可能并非如此；就好比在 在初中课程里一个计算过程可能会被详细解释，而 在高中课程里其则会被心算完成且无需被解释。

在作业中， 批改者知道学生所要求的结果是真实的，并且他知道（正确的）推演。 学生则必须说服批改者自己明白如何（正确地）推演所要求的结果。 因此学生需要提供的推演的详细程度取决于批改者的信任程度： 在一份优秀的答卷中，一句“由归纳证明显然”通常是可被接受的；而 如果一份答卷里前面已出现过一个所谓的“显然”，但它明显是……错误的， 那么这种说法就绝对不会被接受。

为了能够适当地处理细节程度的问题，我们需要知道什么是完整的推演。 这一形式化工作是在本世纪初完成的。这里给出了 自然推演 Dédution Naturelle 中推演的概念。 我们将在本章末尾和第 5 章中看到其他形式化方法。

几个可能令人惊讶的事实

• 规则的个数是有限的： 每个连结词（包括相等）都有两条规则， 然后再加上三条通用规则。 下面的事实似乎并太明显： 有限个数的规则足以推演所有为真的命题， 不过我们将在第 2 章中 证明该结论（其本质是完备性定理）并 澄清其含义。这个证明并不简单。

• 这些规则在所有数学领域中都是共用的：代数、分析、几何等。 也就是说我们已经成功地将推理中的所有通用部分都提取出来。 稍后会看到推演是由一系列有序对 $(\Hypo, A)$ 组成的，其中 $\Hypo$ 是一个集合，由一群公式（假设）构成；而 $A$ 是一个公式（结论）。 在研究数论、几何或实分析时，除了规则之外， 我们还会使用一些被称为公理 Axiomes 的假设。 它们表达了我们所操作对象的特殊属性。例如 在 $\mathbb{N}$ 中每个元素都有一个后继， 在 $\mathbb{R}$ 中两个元素之间总有另一个元素。 在第 3 章中我们将研究一些理论 Théories 的例子。

1.3.2 相继式 les Séquents

我们在推演公式的时候会用到一个假设集， 这个集合可能会在推演过程中发生变化： 当我们说“假设 $F$ 并推演出 $G$”时， $F$ 就是一个新的假设，我们可以用它来推演出 $G$。 为了形式化这一点，我们引入了相继式的概念。

1.3.3 推演规则 les Règles de Démonstration

推演规则是构建推演的积木块。 一个形式化的推演是一群有限（且正确！）的规则的组合， 这个组合不是线性的（不是一个序列），而是树状的。 我们需要频繁创建分支：例如要推演出 $A \land B$， 我们需要完成两件事（推演出 $A$ 以及推演出 $B$）。

下面是一套规则选取方案： 我们本可以介绍其他（替代或附加）规则， 它们亦能引申出相同的证明记号； 但是被选取的这些规则是“自然的”， 它们对应于我们在数学中通常所做的推理。 除了下面的规则之外，我们在实际应用中还会使用其他许多规则； 但这些规则都可以从前面的规则中推导出来， 因此将其称作是派生规则 Règles Dérivées。 我们将在第 1.3.8 节中看到一些例子。

传统上我们将树的 根（相继式结论）写在下方并将 叶子写在上方：大自然正是如此！ 不过我们也经常从根向叶子构建树： 由于在纸张上也有从上到下书写的传统， 因此将根写在上方、叶子写在下方也并非不合理。 必须做出选择！于是决定采用逻辑教材中最常见的做法。

a) 规则如何解读 Comment Lire les Règles ?

1. 一条规则由下述部分组成：

   • 一个集合，包含一系列前提 Prémisses： 每个前提都是一个相继式。 前提的个数可以为零个、一个或多个， 它们的排列顺序并不重要；
   • 一个相继式，代表结论 Conclusion；
   • 一条水平线，用于分隔前提（上方）和结论（下方）。 水平线的的右侧会标注规则的名称。

   例如：

   $\qquad\begin{prooftree} \AXC{\({\overbracket[.5pt]{\Hprev{\Hypo}}^\mathclap{\text{一群假设 hypothese}} \vdash A\to B}\)} \AXC{\(\overbracket[.5pt]{\Hprev{\Hypo} \vdash A}^\mathclap{\text{前提 premise}}\)} \RightLabel{\(\rightarrow_{\rm e}\)} \BIC{\(\underbracket[.5pt]{\Hnext{\Hypo} \vdash B}_\mathclap{\text{相继式结论 sequent conclusion}}\)} \end{prooftree}$

   这条规则拥有 两个前提（$\Hypo \vdash A \to B$ 和 $\Hypo \vdash A$）和 一个结论（$\Hypo \vdash B$）。

2. 每条规则有两种理解方式：

   • 自下而上 de Bas en Haut ： 如果我们想要推演出结论， 那么只需通过使用该规则来推演出前提即可。 这便是我们在寻找推演时所采用的解读方式。 这对应于分析 Analyse。

   • 自上而下 de Haut en Bas ： 如果前提均已被推演出， 那么结论则可被推演出。 这是我们在撰写推演时所采用的解读方式。 这对应于概括 Synthèse；

   每条规则后都有一段非形式化文字 用来说明该规则的直观含义， 并在必要时给出一些补充说明。这些文字 有时会以自上而下的方式解读规则， 有时则以自下而上的方式解读规则； 这是因为有些规则 在某一个方向上会比 在另一个方向上更容易理解。

3. 每个逻辑连结词符号都有与之对应的两条规则：

   • 引入规则 Règles d’Introduction， 用于推演以该符号为主要运算符的公式；
   • 消去规则 Règles d’Élimination， 用于使用以该符号为主要运算符的公式。

4. 由于等号具有特殊的地位， 因此我们也为其引入了两条规则。 在第 3 章中我们将看到 另一种利用该符号特殊地位的方法。

5. 除了上述规则之外，还有三条通用规则：

   头两条规则（公理和弱化）不对应于任何连结词： 第一条规则是唯一一条没有前提的规则， 因此它对应于其所处推演片段中的某个末端（树的叶子）； 第二条规则意味着在推演片段中某些假设可能并未被使用。

   第三条规则（谬误消去（古典逻辑）） 常常与涉及 $\lnot$ 的规则一起出现。 然而它具有特殊的地位：它是唯一一条对应于归谬论的推演规则。 其作用在第 4 章中将会得到更好的体现， 在那里我们将研究一种不使用该规则的推演模型。

b) 规则 les Règles

---

公理 Axiome

$\qquad\begin{prooftree} \AXC{}\RL{\(\axm\)} \UIC{\(\Hnext{\Hypo}, A\vdash A\)} \end{prooftree}$

如果相继式的结论是假设之一， 那么该相继式当然是可被推演的。

---

弱化 Affaiblissement

$\qquad \begin{prooftree} \AXC{\(\Hprev{\Hypo} \vdash A\)}\RL{\(\aff\)} \UIC{\(\Hnext{\Hypo},B\vdash A\)} \end{prooftree}$

自上而下： 如果能够利用 $\Hypo$ 推演出 $A$， 那么也能利用 $\Hypo \cup \{B\}$ 推演出 $A$。

自下而上： 一部分假设可能是冗余的。

---

箭头引入 Introduction de l’Implication

$\qquad \begin{prooftree} \AXC{\(\Hprev{\Hypo},A\vdash B\)}\RL{\(\intrTo\)} \UIC{\(\Hnext{\Hypo}\vdash A\to B\)} \end{prooftree}$

自下而上： 要想推演出 $A \to B$， 只需假设 $A$ （即将 $A$ 加入进假设）并推演出 $B$ 即可。

---

箭头消去 Élimination de l’Implication

这条规则在很久以前就以肯定前件 Modus Ponens 著称。

$\qquad \begin{prooftree} \AXC{\(\Hprev{\Hypo}\vdash A\to B\)} \AXC{\(\Hprev{\Hypo}\vdash A\)} \RL{\(\elimTo\)} \BIC{\(\Hnext{\Hypo} \vdash B\)} \end{prooftree}$

自下而上： 如果 $A \to B$ 已被推演出， 那么为了推演出 $B$ 只需推演出 $A$ 即可。

---

合取引入 Introduction de la Conjonction

$\qquad \begin{prooftree} \AXC{\(\Hprev{\Hypo}\vdash A\)} \AXC{\(\Hprev{\Hypo}\vdash B\)} \RL{\(\intrCon\)} \BIC{\(\Hnext{\Hypo} \vdash A\land B\)} \end{prooftree}$

自下而上： 要想推演出 $A \land B$， 只需分别推演出 $A$ 和 $B$ 即可。

---

合取消去 Élimination de la Conjonction

$\qquad \begin{prooftree} \AXC{\(\Hprev{\Hypo}\vdash A\land B\)}\RL{\(\elimConL\)} \UIC{\(\Hnext{\Hypo}\vdash A\)} \end{prooftree} \qquad \begin{prooftree} \AXC{\(\Hprev{\Hypo}\vdash A\land B\)}\RL{\(\elimConR\)} \UIC{\(\Hnext{\Hypo}\vdash B\)} \end{prooftree} $

自上而下： 依据 $A \land B$， 我们可以推演出 $A$（左消去）和 $B$（右消去）。

---

析取引入 Introduction de la Disjonction

$\qquad \begin{prooftree} \AXC{\(\Hprev{\Hypo} \vdash A\)}\RL{\(\intrDisL\)} \UIC{\(\Hnext{\Hypo} \vdash A\lor B\)} \end{prooftree} \qquad \begin{prooftree} \AXC{\(\Hprev{\Hypo} \vdash B\)}\RL{\(\intrDisR\)} \UIC{\(\Hnext{\Hypo} \vdash A\lor B\)} \end{prooftree}$

自下而上： 要想推演出 $A \lor B$， 只需推演出 $A$ 或者是推演出 $B$。 该规则可能令人感到困惑, 因为结论比前提更弱。 下面的例子应该能帮助理解该规则。

设想我们拥有一个如下形式的定理 $\forall x~\{(x < 4) \lor (x = 4) \to A\}$， 并且我们需要将该定理应用于 $x = \pi$ 上以证明某个结果。 首先需要形式地验证 $\pi$ 小于或等于 $4$。 易知 $\pi$ （严格）小于 4， 但唯有 $\pi$ 小于或等于 4 才能允许我们在当前情形下应用该定理。 正是规则 $\intrDisL$ 使得这一点成为可能。

设想我们需要证明一个如下形式的性质：“对任意整数 $n$，$u_n \leq 4$”， 并且为了证明它，我们需要区分 $n$ 为偶数和 $n$ 为奇数的情况（比如研究如递归数列）。 假如现在 $u_{2p} = 4$ 可以得出， $u_{2p+1} < 4$ 可通过对 $p$ 进行归纳得出，但 $u_{2p+1} \leq 4$ 无法通过归纳得出！ 那么这时该规则便是必须的。

---

析取消去 Élimination de la Disjonction

$\qquad \begin{prooftree} \AXC{\(\Hprev{\Hypo} \vdash A\lor B\)} \AXC{\(\Hprev{\Hypo},A \vdash C\)} \AXC{\(\Hprev{\Hypo},B \vdash C\)}\RL{\(\elimDis\)} \TIC{\(\Hnext{\Hypo} \vdash C\)} \end{prooftree}$

自下而上： 如果想推演出 $C$， 并且 $A \lor B$ 已被推演出， 那么只需分别在假设 $A$ 和假设 $B$ 的条件下推演出 $C$ 即可。

这便是分类讨论。比方说， 如果我们需要证明一个关于整数 $n$ 的性质，那么 我们可以按照 $n$ 为偶数和 $n$ 为奇数的情况进行区分。 我们也可按照 $n$ 为素数和 $n$ 为合数的情况进行区分。

---

否定引入 Introduction de la Négation

$\qquad \begin{prooftree} \AXC{\(\Hprev{\Hypo},A \vdash \bot\)}\RL{\(\intrNeg\)} \UIC{\(\Hnext{\Hypo} \vdash \lnot A\)} \end{prooftree}$

自下而上： 要想推演出 $\lnot A$， 只需假设 $A$ 并推演出谬误 $\bot$ 即可。 也请阅读一下 $\clssBot$ 规则后的评论。

---

否定消去 Élimination de la Négation

$\qquad \begin{prooftree} \AXC{\(\Hprev{\Hypo}\vdash \lnot A\)} \AXC{\(\Hprev{\Hypo}\vdash A\)}\RL{\(\elimNeg\)} \BIC{\(\Hnext{\Hypo} \vdash \bot\)} \end{prooftree}$

自上而下： 如果我们已经推演出 $\lnot A$ 和 $A$， 那么我们便可推演出谬误 $\bot$。 也请阅读一下 $\clssBot$ 规则后的评论。

---

谬误消去（古典逻辑） Absurdité Classique

$\qquad \begin{prooftree} \AXC{\(\Hprev{\Hypo},\lnot A\vdash \bot\)}\RL{\(\clssBot\)} \UIC{\(\Hnext{\Hypo}\vdash A\)} \end{prooftree}$

自下而上： 要想推演出 $A$， 只需假设 $\lnot A$ 并推演出谬误 $\bot$ 即可。

$\elimNeg$ 和 $\intrNeg$ 两条规则使得 $\bot$ 这一符号变得有意义。 它表示“通用的”假，独立于我们所使用的语言。 当我们在推演中声称“获得了一个矛盾”时， 意味着我们已经证明了某个“显然为假”的东西：比如 一个公式以及其否定（见规则 $\elimNeg$）、 $0 = 1$ 或 任何与所使用语言相关的其他公式。 后面我们将看到（见第 4.3.3 节的引理.4.3.3）$\lnot A$ 等价于 $A \to \bot$； 因此完全可以不使用连结词 $\lnot$ 并删除与之对应的两条规则。

规则 $\clssBot$ 对应于归谬论。 我们将在引理.4.3.3中看到（见第 4.3.3 节）该规则意味着 $\lnot\lnot A$ 等价于 $A$，即： “‘$A$ 为假’这句话是错的当且仅当 $A$ 就为真”。 该规则并非显而易见： 它对于某些结果的证明是必须的，也就是说 有些结果无法在不依赖归谬论的情况下被证明。

另外注意到：与其他规则不同， 该规则可以在任何时候被使用： 我们始终可以声称“为了证明 $A$，我假设 $\lnot A$ 并寻找矛盾”。 但这会使搜寻证明（变得稍微）更加困难。

---

全称引入 Introduction du Quantificateur Universel

$\qquad \begin{prooftree} \AXC{\(\Hprev{\Hypo} \vdash A\)} \AXC{\(x\) 在 \(\Hprev{\Hypo}\) 的元素中无自由出现} \RL{\(\intrAll\)} \BIC{\(\Hnext{\Hypo} \vdash \forall x ~A\)} \end{prooftree}$

自下而上： 要想推演出 $\forall x~A$， 只需推演出 $A$——条件是 $x$ 在假设中不能有自由出现。

要想证明 $\forall x~A$ 就 需要证明 $A$ 对于任意对象 $x$ 都成立。条件 “$x$ 在 $\Hypo$ 的元素中无自由出现”是对 “$x$ 是任意的”的形式化描述。这一附加条件意味着 我们对 $x$ 没有任何假设， 因为 $x$ 不能出现在假设中。

该条件是至关重要的， 忘记检验该条件常导致错误。

如果该条件未被满足， 那么 $x$ 可能并非任意的。 需要记住公式在约束变量的重命名操作下是等价的，因此 公式 $\forall y~A[x := y]$ 与 公式 $\forall x~A$ 是相同的。 此时只需将 $A$ 中的 $x$ 重命名为另一个满足该条件的字母 $y$， 并证明 $A[x := y]$ 即可。

---

全称消去 Élimination du Quantificateur Universel

$\qquad \begin{prooftree} \AXC{\(\Hprev{\Hypo} \vdash \forall x ~A\)}\RL{\(\elimAll\)} \UIC{\(\Hnext{\Hypo} \vdash A[x:=t]\)} \end{prooftree}$

自上而下： 利用 $\forall x~A$ 我们可以推导出 $A[x := t]$，$t$ 为任意项。 也可以这样说：如果已经证明了 $A$ 对于任意 $x$ 都成立， 那么我们就可以使用 $A$ 来处理任意对象 $t$。 前面已经提到过，项表示我们所处理的对象， 在进行替换时（如有必要）需重命名 $A$ 中的约束变量以避免捕获 $t$ 中的变量。 该条件同样适用于下一条规则。

---

存在引入 Introduction du quantificateur existentiel

$\qquad \begin{prooftree} \AXC{\(\Hprev{\Hypo} \vdash A[x:=t]\)}\RL{\(\intrExt\)} \UIC{\(\Hnext{\Hypo} \vdash \exists x~A\)} \end{prooftree}$

自上而下： 要想推演出 $\exists x~A$， 只需找到一个对象（即一个项）$t$， 并推演出 $A[x := t]$ 即可。

---

存在消去 Élimination du Quantificateur Existentiel

$\qquad \begin{prooftree} \AXC{\(\Hprev{\Hypo} \vdash \exists x~A\)} \AXC{\(\Hprev{\Hypo},A \vdash C\)} \AXC{\(x\) 在 \(\Hprev{\Hypo}\) 的元素和 \(C\) 中均无自由出现}\RL{\(\elimExt\)} \TIC{\(\Hnext{\Hypo} \vdash C\)} \end{prooftree}$

自上而下： 当我们拥有一个形如 $\exists x~A$ 的假设时， 我们可通过“取”一个满足 $A$ 的 $x$ 来使用该假设。 形式地说，“取”意味着为其赋予一个名字。

$x$ 的约束条件是对如下事实的形式化描述： 假设所断言存在的对象 没有任何理由是推演过程中引入的对象之一。 该条件至关重要，忘记检验该条件常导致错误。 与规则 $\intrAll$ 的情况类似， 如果该条件未被满足， 那么只需将公式 $\exists x~A$ 中的 $x$ 重命名即可，即给 $x$ 赋予一个新名字。

另一个常见的错误是发明下述规则：

$\qquad\begin{prooftree} \AXC{\(\Hprev{\Hypo} \vdash \exists x~A\)}\RL{\(\elimExt\)} \UIC{\(\Hnext{\Hypo} \vdash A\)} \end{prooftree}$

后面会看到相关的例子。

我们也可以将 $\elimExt$ 表述为如下形式：

$\qquad \begin{prooftree} \AXC{\(\Hprev{\Hypo}\vdash \exists x~A\)}\RL{\(\elimExt\)} \UIC{\(\Hnext{\Hypo}\vdash A[x:=f(y_1,\ldots,y_n)]\)} \end{prooftree}$

当中 $f$ 为一个“新”的函数符号， $y_1$，$\ldots$，$y_n$ 为 $A$ 中的自由变量。 注意到该规则不再涉及任何辅助公式 $C$， 如此便需要说明引入这些新名字的意义，并且 这还会带来其他一些麻烦（见第 2.7 节）。

---

等号引入 Introduction de l’Égalité

$\qquad\begin{prooftree} \AXC{}\RL{\(\intrEql\)} \UIC{\(\Hnext{\Hypo} \vdash t=t\)} \end{prooftree}$

我们始终可以推演出 $t = t$， 此规则意味着等号具有自反性。

---

等号消去 Élimination de l’Égalité

$\qquad \begin{prooftree} \AXC{\(\Hprev{\Hypo} \vdash A[x:=\EQprev{t}]\)} \AXC{\(\Hprev{\Hypo} \vdash t = u\)} \RL{\(\elimEql\)} \BIC{\(\Hnext{\Hypo} \vdash A[x:=\EQnext{u}]\)} \end{prooftree}$

自上而下： 如果我们已经推演出 $A[x := t]$ 和 $t = u$， 那么我们便可推演出 $A[x := u]$。

这条规则意味着任何两个相等的对象都拥有相同的性质。 不过注意，公式 $t = u$ 和 $u = t$ 在形式上并不相同： 只有在证明了等号的对称性（见1.3.例子.9）之后 我们才能以这种方式来解读该规则。

c) 规则如何使用 Comment Utiliser une Règles ?

每条规则都代表一个模式 Schéma： 我们将其中的字母替换为公式、项、假设集、变量。 当然，这种替换必须保持一致性：例如， 同一个字母的两次出现必须被实例化为同一个公式。

下面是规则 $\elimTo$ 的一个应用案例：

$\qquad \begin{prooftree} \AXC{\(\vdash f(x)=f(y) \to x=y\)} \AXC{\(\vdash f(x)=f(y)\)} \RL{\(\elimTo\)} \BIC{\(\vdash x=y\)} \end{prooftree}$

其中

• $\Hypo$ 被替换为了空集，
• $A$ 被替换为了 $f(x)=f(y)$，
• $B$ 被替换为了 $x=y$。

该规则断言： 如果我们已经证明了两条前提 $\vdash f(x)=f(y) \to x=y$ 和 $\vdash f(x)=f(y)$， 那么我们便证明了结论 $\vdash x=y$。

d) 推演如何撰写 Comment Écrire une Démonstration Formelle ?

一个例子比一段文字更有说服力。 下面示范如何推演出公式 $\lnot A \leftrightarrow (A \to \bot)$。 为了节省空间，我们为多次出现的假设集赋予了名称：

• $\Hypo = \lnot A, A$
• $\Hypo' = A \to \bot, A$。

$\qquad\begin{prooftree} \AXC{}\RL{\(\axm\)} \UIC{\(\Hprev{{\Hnext{\Hypo}}} \vdash \lnot A\)} \AXC{}\RL{\(\axm\)} \UIC{\(\Hprev{{\Hnext{\Hypo}}} \vdash A\)} \RL{\(\elimNeg\)} \BIC{\(\Hnext{\Hprev{\lnot A},A}\vdash \bot\)} \RL{\(\intrTo\)} \UIC{\(\Hnext{\lnot A} \vdash A \to \bot\)} \RL{\(\intrTo\)} \UIC{\(\vdash \lnot A \to (A\to \bot)\)} % ------------ \AXC{}\RL{\(\axm\)} \UIC{\(\Hnext{\Hprev{\Hypo'}\vdash A\to \bot}\)} \AXC{}\RL{\(\axm\)} \UIC{\(\Hnext{\Hprev{\Hypo'}\vdash A}\)} \RL{\(\elimTo\)} \BIC{\(\Hnext{\Hprev{A\to \bot}, A}\vdash \bot\)} \RL{\(\intrNeg\)} \UIC{\(\Hnext{A\to \bot} \vdash \lnot A\)} \RL{\(\intrTo\)} \UIC{\(\vdash (A\to \bot)\to \lnot A\)} \RL{\(\intrCon\)} \BIC{\(\vdash \lnot A \leftrightarrow (A\to \bot)\)} \end{prooftree}$

上述记法称作是树状表示法 Notation Arborescente。 在该推演中，其中一个分支应用了下述规则：

• $\axm$ 用于证明 $\Hypo \vdash \lnot A$ 和 $\Hypo \vdash A$
• $\elimNeg$ 用于推导出 $\Hypo \vdash \bot$
• $\intrTo$ 用于推导出 $\lnot A \vdash A \to \bot$
• $\intrTo$ 用于推导出 $\vdash \lnot A \to (A \to \bot)$

另一个分支则应用了下述规则：

• $\axm$ 用于证明 $\Hypo' \vdash A \to \bot$ 和 $\Hypo' \vdash A$
• $\elimTo$ 用于推导出 $\Hypo' \vdash \bot$
• $\intrNeg$ 用于推导出 $A \to \bot \vdash \lnot A$
• $\intrTo$ 用于推导出 $\vdash (A \to \bot) \to \lnot A$

最后我们应用规则 $\intrCon$ 来证明结论（提示： $B \leftrightarrow C$ 是 $ (B \to C) \land (C \to B)$ 的缩写）。

e) 推演如何搜寻 Comment Trouver une Démonstration ?

当我们要求学生推演出一个结果（例如在考试中）时， 他将会面临两大困难：寻找推演和撰写推演。

刚刚我们已经看到什么才算是完整的证明。 至于找到合适的细节程度这一环节 通常不会带来太大困难，并且随着经验的积累 这会变得越来越容易。

那么该如何找到一个推演呢？在第 3 章（涉及到不完备性定理）中我们将会看到 通用的方法并不存在。想象力、直觉和经验始终都有发挥的场景。 然而对于大学一、二年级课程中大多数常见的习题来说， 这一部分所占的比重相对较小； 如果学生已经充分地剖析了问题， 那么他往往就能够“看出”解法。

接下来我们会介绍一些启发思路。 在这里只介绍我们是如何找到上面所示的推演的：

• 首先需要证明逻辑等价。这是一个 $\land$ 命题的缩写。 根据规则 $\intrCon$，我们需要证明两件事： $\vdash \lnot A \to (A \to \bot)$ 和 $\vdash (A \to \bot) \to \lnot A$。

  • 为了证明 $\vdash \lnot A \to (A \to \bot)$，我们应用规则 $\intrTo$。
    • 现在需要证明 $\lnot A \vdash A \to \bot$。为了证明它，我们再次应用规则 $\intrTo$。
      • 现在需要证明 $\Hypo \vdash \bot$。 此时我们无法再应用任何引入规则。唯一能够推进的规则是 $\elimNeg$。
        • 现在需要证明 $\Hypo \vdash \lnot A$ 和 $\Hypo \vdash A$。 这两个相继式均可通过规则 $\axm$ 得出。
  • 为了证明 $\vdash (A \to \bot) \to \lnot A$，我们应用规则 $\intrTo$。
    • 现在需要证明 $A \to \bot \vdash \lnot A$。为了证明它，我们应用规则 $\intrNeg$。
      • 现在需要证明 $\Hypo' \vdash \bot$。 此时我们无法再应用任何引入规则。 唯一能够推进的规则是 $\elimTo$。
        • 现在需要证明 $\Hypo' \vdash A \to \bot$ 和 $\Hypo' \vdash A$。 这两个相继式均可通过规则 $\axm$ 得出。

注意到：上述推演的两种阅读方式（撰写和搜寻）之间唯一的区别在于，

• 对于前者我们是从上到下阅读树状结构，而
• 对于后者我们是从下到上阅读树状结构。

f) 一些启发思路 Quelques Heuristiques

重复下述步骤通常是一个不错的思路：

1. 如果能够套用引入规则，就套用它。
2. 否则对假设（或定理）套用消去规则。

需要注意有些规则是可逆的，即 如果前提可被推演出， 那么结论也可被推演出—— 也就是说套用该规则可能“没有损失”， 但并非所有规则都是如此；例如， $\intrCon$ 是可逆的，但 $\intrAll$ 就不是。 因此在使用不可逆规则时， 我们需要提醒自己可能走上了错误的路， 如果最终无法得到结果， 那么就需要回头重新选择方向。

另外注意：

• 要想应用规则 $\intrExt$ 和 $\elimAll$， 必须提供一个显示的项 $t$。 这是一个常见的错误来源： 人们声称应用了该规则但却未提供项 $t$。
• 规则 $\intrAll$ 和 $\elimExt$ 中不会有任何项出现。 但是需要注意变量的名称。

某些辅助证明软件会通过如下方式来帮助用户。

• 对于规则 $\intrAll$ 和 $\elimExt$， 软件会自动进行必要的重命名。
• 对于规则 $\intrExt$ 和 $\elimAll$， 软件会引入符号“?”来询问用户该规则应使用哪个项。 通常建议立即给出该答案，尽管有时在实际操作中并不会这样做。 考虑下述情况：在我们将描述函数满足连续性的假设套用到 某个在后面才会提供的 $\varepsilon$ 上时， 我们需要非常谨慎地确保 这个 $\varepsilon$ 不应依赖于 在套用规则 $\elimAll$ 时尚未被引入的对象。 所有辅助证明软件都会自动执行这样的检查。

最后需要指出的是：上述策略对应于推演树的自下而上构造。 尽管如此，在搜寻推演的过程中 我们经常需要混合使用两种方式： 既需要自下而上，又需要自上而下。 例如我们可能需要从已知事实（即树的叶子，无论是作为假设还是定理）出发 以得到一个结果并最终得出结论。

g) 命题逻辑的规则 les Règles de Démonstration du Calcul Propositionnel

命题演算是一阶逻辑的一个特殊情况。 推理规则是相同的。 下面的性质似乎是显而易见的： 假设 $\Hypo$ 中的元素和 $A$ 为 $\setCal_P$ 中的公式。 相继式 $\Hypo \vdash A$ 可被推演出当且仅当 它可在不使用规则 $\intrAll$、$\elimAll$、$\intrExt$、$\elimExt$、$\intrEql$、$\elimEql$ 的情况下被推演出。 然而对应的证明可不简单， 需要用到第 5 章才会介绍的切割消去定理。

在尝试证明 $\setCal_P$ 中的公式时， 我们只需避免使用这些规则即可！

1.3.4 推演示例 Exemples de Démonstration

下面的例子会突出展示各条规则的作用。 这里我们采用树状表示法来撰写推演。 下一个小节我们将放弃这种过于冗长的记法。

为了简化树状结构，我们为某些假设集赋予了名称。 它们的定义会在推演中首次引入该名称的地方给出（以自下而上方式阅读）。

1.3.5 推演错误示例 Quelques Démonstrations Fausses

接下来我们将展示一些常见的失误， 它们可能会在推演（明显？）错误的公式时犯下。 这些失误源于对规则的错误应用或对规则的发明。 规则的错误使用将用 $\errr$ 来标记。

1.3.6 无相继式的自然推演 Déduction Naturelle Sans Séquents

本小节中我们将介绍一种等价的自然推演系统， 它不使用相继式。在使用相继式的推演系统中， 每使用一个推演规则时都需要复制一遍假设集。 而在下面要介绍的系统中假设集只需要写一遍， 我们只对结论应用规则。 一个以 $A_1$，$\ldots$，$A_n$ 为假设得出的关于 $A$ 的推演 可表示为如下形式：

$\qquad\begin{prooftree} \AXC{\(A_1\ldots A_n\)}\noLine \UIC{\(\ph{A_1}\mathclap{\vdots}\ph{A_n}\)} \UIC{\(A\)} \end{prooftree}$

一个推演是一个有限树，当中每个节点都被一个公式所标记。 推演树的构造始于每个叶子，然后向下生长直至根部为止。

最基本的步骤即“公理”规则——即在假设 $A$ 下推导出公式 $A$。可简记为 $A$。 更为复杂的推演则是通过应用逻辑规则来构造的。

• 规则 $\intrTo$

  $\qquad\begin{prooftree} \AXC{\([A]\)}\noLine \UIC{\(\vdots\)}\noLine \UIC{\(B\)} \RL{\(\intrTo\)} \UIC{\(A\to B\)} \end{prooftree}$

  说明：基于

  • 以 $A$ 为假设得出的关于 $B$ 的推演，以及

  我们可以推出一个

  • 关于 $A\to B$ 的推演。

  第二个推演的假设集等于第一个推演的假设集去掉 $A$， 此时可以说我们“卸载 Déchargé”掉了 $A$。 形式地说就是：所有 $A$ 的出现都被替换为了 $[A]$。

  如此假设集便可以分为两类：

  • 主要假设 Hypothèses Principales： 会一直被保留到推演结束。
  • 辅助假设 Hypothèses Auxiliaires： 只用于构造子推演，随后会被卸载掉。

  一个以 $\Hypo$ 为假设的关于 $A$ 的推演形如一棵树， 其结论是 $A$ ，而其主要假设全部都在 $\Hypo$ 中。

• 规则 $\elimTo$

  $\qquad \begin{prooftree} \AXC{\(\vdots\)}\noLine \UIC{\(A\to B\)} \AXC{\(\vdots\)}\noLine \UIC{\(A\)} \RL{\(\elimTo\)} \BIC{\(B\)} \end{prooftree}$

  说明：基于

  • 关于 $A\to B$ 的推演以及
  • 关于 $A$ 的推演，

  我们可以推出一个

  • 关于 $B$ 的推演。

  第三个推演的假设集是前两者的假设集的并集。

下面列出剩下的规则。

a) 规则 les Règles

---

公理 Axiome

$\qquad \begin{prooftree} \AXC{\(A\)} \RL{\(\axm\)} \UIC{\(A\)} \end{prooftree}$

---

弱化 Affaiblissement

$\qquad \begin{prooftree} \AXC{\(\vdots\)}\noLine \UIC{\(A\)} \AXC{\(B\)} \RL{\(\aff\)} \BIC{\(A\)} \end{prooftree}$

---

箭头引入 Introduction de l’Implication

$\qquad \begin{prooftree} \AXC{\([A]\)} \noLine \UIC{\(\vdots\)}\noLine \UIC{\(B\)} \RL{\(\intrTo\)} \UIC{\(A\to B\)} \end{prooftree}$

---

箭头消去 Élimination de l’Implication

$\qquad \begin{prooftree} \AXC{\(\vdots\)}\noLine \UIC{\(A\to B\)} \AXC{\(\vdots\)}\noLine \UIC{\(A\)}\RL{\(\elimTo\)} \BIC{\(B\)} \end{prooftree}$

---

合取引入 Introduction de la Conjonction

$\qquad \begin{prooftree} \AXC{\(\vdots\)}\noLine \UIC{\(A\)} \AXC{\(\vdots\)}\noLine \UIC{\(B\)}\RL{\(\intrCon\)} \BIC{\(A\wedge B\)} \end{prooftree}$

---

合取消去 Élimination de la Conjonction

$\qquad \begin{prooftree} \AXC{\(\vdots\)}\noLine \UIC{\(A\wedge B\)}\RL{\(\elimConL\)} \UIC{\(A\)} \end{prooftree} \qquad\begin{prooftree} \AXC{\(\vdots\)}\noLine \UIC{\(A\wedge B\)}\RL{\(\elimConR\)} \UIC{\(B\)} \end{prooftree}$

---

析取引入 Introduction de la Disjonction

$\qquad\begin{prooftree} \AXC{\(\vdots\)}\noLine \UIC{\(A\)}\RL{\(\intrDisL\)} \UIC{\(A\vee B\)} \end{prooftree} \qquad\begin{prooftree} \AXC{\(\vdots\)}\noLine \UIC{\(B\)}\RL{\(\intrDisR\)} \UIC{\(A\vee B\)} \end{prooftree}$

---

析取消去 Élimination de la Disjonction

$\qquad\begin{prooftree} \AXC{\(\vdots\)}\noLine \UIC{\(A\vee B\)} \AXC{\([A]\)}\noLine \UIC{\(\vdots\)}\noLine \UIC{\(C\)} \AXC{\([B]\)}\noLine \UIC{\(\vdots\)}\noLine \UIC{\(C\)}\RL{\(\elimDis\)} \TIC{\(C\)} \end{prooftree}$

---

否定引入 Introduction de la Négation

$\qquad\begin{prooftree} \AXC{\([A]\)}\noLine \UIC{\(\vdots\)}\noLine \UIC{\(\bot\)}\RL{\(\intrNeg\)} \UIC{\(\neg A\)} \end{prooftree}$

---

否定消去 Élimination de la Négation

$\qquad\begin{prooftree} \AXC{\(\vdots\)}\noLine \UIC{\(\neg A\)} \AXC{\(\vdots\)}\noLine \UIC{\(A\)} \RL{\(\elimNeg\)} \BIC{\(\bot\)} \end{prooftree}$

---

谬误消去（古典逻辑） Absurdité Classique

$\qquad\begin{prooftree} \AXC{\([\neg A]\)}\noLine \UIC{\(\vdots\)}\noLine \UIC{\(\bot\)}\RL{\(\clssBot\)} \UIC{\(A\)} \end{prooftree}$

---

全称引入 Introduction du Quantificateur Universel

$\qquad\begin{prooftree} \AXC{\(\vdots\)}\noLine \UIC{\(A\)}\RL{\(\intrAll\)} \UIC{\(\forall x~A\)} \end{prooftree}$

$x$ 在下述推演的假设集中不能有自由出现：

• 关于 $A$ 的推演

---

全称消去 Élimination du Quantificateur Universel

$\qquad\begin{prooftree} \AXC{\(\vdots\)}\noLine \UIC{\(\forall x~A\)}\RL{\(\elimAll\)} \UIC{\(A[x:=t]\)} \end{prooftree}$

---

存在引入 Introduction du Quantificateur Existentiel

$\qquad\begin{prooftree} \AXC{\(\vdots\)}\noLine \UIC{\(A[x:=t]\)}\RL{\(\intrExt\)} \UIC{\(\exists x ~A\)} \end{prooftree}$

---

存在消去 Élimination du Quantificateur Existentiel

$\qquad\begin{prooftree} \AXC{\(\vdots\)}\noLine \UIC{\(\exists x~A\)} \AXC{\([A]\)}\noLine \UIC{\(\vdots\)}\noLine \UIC{\(C\)}\RL{\(\elimExt\)} \BIC{\(C\)} \end{prooftree}$

$x$ 在下述推演的假设集中不能有自由出现：

• 关于 $\exists x$ 的推演
• 关于 $A$ 的推演
• 以 $A$ 为假设的关于 $C$ 的推演

---

等号引入 Introduction de l’Égalité

$\qquad\begin{prooftree} \AXC{\([t=t]\)}\RL{\(\intrEql\)} \UIC{\(t=t\)} \end{prooftree}$

$t = t$ 会被卸载，因为证明它无需任何假设。

---

等号消去 Élimination de l’Égalité

$\qquad\begin{prooftree} \AXC{\(\vdots\)}\noLine \UIC{\(A[x:=\EQprev{t}]\)} \AXC{\(\vdots\)}\noLine \UIC{\(t=u\)}\RL{\(\elimEql\)} \BIC{\(A[x:=\EQnext{u}]\)} \end{prooftree}$

---

b) 推演示例 Exemples de Démonstrations

相较于使用相继式的版本， 上述推演会更简洁一些。

1.3.7 推演的另一种表示方式 une Autre Présentation des Démonstrations

推演超过几行树状表示法就会变得难以使用。 因此我们倾向于采用一种 线性表示法 Notation Linéaire：

有三种情况。

a) 规则只有一个前提 La règle a une seule prémisse

我们直接在下一行继续前提的推演。例如

$\qquad \begin{aligned}[t] \ph{\ttt{(00) }} &\Hnext{\Hypo} \vdash A\to B &&\intrTo \\ &\Hprev{\Hypo} , A\vdash B &&\ldots \end{aligned}$

b) 规则至少有两个前提 La règle a au moins deux prémisses

我们为每个前提提供一个编号，并在这些前提的推演开始之前引用对应的编号；另外 我们使用缩进来突显出推演的树状结构。例如

$\qquad \begin{aligned}[t] &\Hnext{\Hypo} \vdash B &&\elimTo \ttt{(01) (02)}\\\ttt{(01) } &\indent \Hprev{\Hypo} , A\vdash B &&\ldots \\ &\indent \ldots &&\ldots \\\ttt{(02) } &\indent \Hprev{\Hypo} \vdash A &&\ldots \\ &\indent \ldots &&\ldots \end{aligned}$

第二个（或者之后的）前提对应的推演 可能会离被调用的位置太远。

此时我们可以先列出所有前提后再分别证明它们。 下面是同一个例子：

$\qquad \begin{aligned}[t] &\Hnext{\Hypo} \vdash B &&\elimTo \\ &\indent \ttt{01:= } \Hprev{\Hypo} \vdash A\to B \\ &\indent \ttt{02:= } \Hprev{\Hypo} \vdash A \\\ttt{(01) } &\indent \Hypo , A\vdash B &&\ldots \\ &\indent \ldots &&\ldots \\\ttt{(02) } &\indent \Hypo \vdash A &&\ldots \\ &\indent \ldots &&\ldots \end{aligned}$

c) 规则没有前提 La règle n’a pas de prémisse

此部分推演就算是结束了。 于是可以转向推演另一条规则的前提——如果还有的话。 否则推演就结束了。

为了简化记号，我们经常会给在推演中多次出现的 上下文（见下例第 3 行）、公式或项赋予名称。 此时我们会使用表达式：“$\Hypo := \dots$”或“$F := \dots$” 。

1.3.8 派生规则 Règles Dérivées

在下一章我们将专注于对推演进行推理。 选择一个最小的规则集在这方面会是一个重要的优势， 但这也会使得推演变得更加冗长。 因此有必要引入一些工具来简化推演。 本小节我们将使用基本规则来证明一些 派生规则 Règles Dérivées， 如此我们后面就可以直接使用这些规则（无需重新证明它们）来简化推演。 当然读者也可以根据需求创建自己的工具。 另外读者也可能注意到：课上（如代数课）见过的定理 其实也是某种工具，它们允许读者推演出代数习题中的公式！

a) 切规则 Règle de Coupure

下面的规则对应于 引理 Lemme 的概念： 我们通过添加一个假设来证明一个公式， 然后再回头证明该假设。 我们将在第 5 章中回顾该规则。

b) 左规则 Règles Gauche

1.3.命题.19 至 1.3.命题.23 介绍了 左规则 Règles Gauche。 这些规则允许我们在相继式的左侧引入连结词。

c) 否定相关的规则 Règles Liées à la Négation

1.3.命题.25 至 1.3.命题.28 提供了 归谬法的另一种形式。在第 4 章我们将比较 下述规则与 谬误消去（古典逻辑） 的作用。

c) 等号相关的规则 Règles Liées à l’Égalité

d) 德摩根律 Lois de Morgan

1.3.9 线性记法的简化 Simplification de la Notation Linéaire

前面介绍的线性记法在呈现平常数学中的例子时依然显得过于繁琐。 下面的约定会进一步简化记法。

a) 省略弱化规则 Affaiblissements implicites

我们以后就不再标注弱化规则了，只需保留有用的假设。 考虑下述推演：

$\qquad\begin{aligned}[t]\ph{\ttt(01) } &\Hnext{A,B,C}\vdash D\wedge E &&\intrCon \\ &\indent\ttt{01:= } \Hprev{A,B,C}\vdash D \\ &\indent\ttt{02:= } \Hprev{A,B,C}\vdash E \\\ttt{(01) } &\indent \Hnext{A,B},C\vdash D &&\aff \\ &\indent \Hprev{A,B}\vdash D &&\ldots \\ &\indent \ldots \\\ttt{(02) } &\indent \Hnext{A},B,\Hnext{C}\vdash E &&\aff \\ &\indent \Hprev{A,C}\vdash E &&\ldots \\ &\indent \ldots \end{aligned}$

将被写作

$\qquad\begin{aligned}[t]\ph{\ttt{(01) }} &A,B,C\vdash D\wedge E &&\intrCon\Omis{,\aff\times 2} \\ &\indent\ttt{01:= } A,B\vdash D \\ &\indent\ttt{02:= } A,B\vdash E \\\ttt{(01) } &\indent A,B\vdash D &&\ldots \\ &\indent \ldots \\\ttt{(02) } &\indent A,C\vdash E &&\ldots \\ &\indent \ldots \end{aligned}$

b) 连续应用规则 Succession de règles

我们经常会直观地连续使用一系列相关的规则（它们属于同一个推理“模块”）。 它们会被合并为一个规则。这里有两个例子：

• 下述推演

  $\qquad\begin{aligned}[t]\ph{\ttt{(01) }} &\Hnext{\forall x(A[x]\to B[x]), A[t]}\vdash C &&\AllL\\ &\Hprev{\forall x(A[x]\to B[x])}, \Hnext{A[t]\to B[t], \Hprev{A[t]}} \vdash C &&\aff\\ &\Hprev{A[t]\to B[t], A[t]}\vdash C &&\ToL\\ &A[t], \Hnext{B[t]}\vdash C &&\aff\\ &\Hprev{B[t]}\vdash C &&\ldots \end{aligned}$

  省略弱化规则后

  $\qquad\begin{aligned}[t]\ph{\ttt{(01) }} &\forall x~(A[x]\to B[x]),A[t]\vdash C &&\AllL,\Omis\aff \\ &A[t]\to B[t],A[t]\vdash C &&\ToL,\Omis\aff \\ &B[t]\vdash C &&\ldots \end{aligned}$

  将被写作

  $\qquad \begin{aligned}[t]\ph{\ttt{(01) }} &H:=\forall x~(A[x]\to B[x]) \\ &H,A[t]\vdash C &&\AllL[t],\ToL \text{ 以获得 } H,\Omis\aff \\ &B[t]\vdash C &&\ldots \end{aligned}$

• 下述推演

  $\qquad \begin{aligned}[t] &A\vee(B\vee C) \vdash D &&\DisL~\ttt{(01)}~\ttt{(02)} \\\ttt{(01) } &\indent A\vdash D &&\ldots \\\ttt{(02) } &\indent B\vee C\vdash D &&\DisL~\ttt{(03)}~\ttt{(04)}\\\ttt{(03) } &\indent\indent B\vdash D &&\ldots \\\ttt{(04) } &\indent\indent C\vdash D &&\ldots \end{aligned}$

  将被写作

  $\qquad \begin{aligned}[t] &A\vee(B\vee C)\vdash D &&\DisL \times 2~\ttt{(01)}~\ttt{(02)}~\ttt{(03)} \\\ttt{(01) } &\indent A\vdash D &&\ldots \\\ttt{(02) } &\indent B\vdash D &&\ldots \\\ttt{(03) } &\indent C\vdash D &&\ldots \end{aligned}$

c) 省略子推演 Omission de sous-démonstrations

有时推演的某一部分并不会引起我们的兴趣。比如 当我们更愿意把注意力放在推演的某一个部分，或者是 当我们认为某一部分推演是显而易见的，又或者是 某个推演与前面写过的推演十分相似。 此时我们只需给出一些提示来完成整个证明即可。

索引

术语定义例子命题记号注意约定译注

• 一阶逻辑 Logique du Premier Ordre： 又称谓词演算 Calcul des Prédicats（见 §01-01）
• 元公式 Méta-Formules（见 §01-01）
• 元推演 Méta-Démonstrations（见 §01-01）
• 语言 Langage： 又称词汇表 Vocabulaire 或者 签名 Signature（见 §01-02-01）
• 常量符号 Symboles de Constante（见 §01-02-01）
• 函数符号 Symboles de Fonction（见 §01-02-01）
• 元数 Arité（见 §01-02-01）
• 关系符号 Les Symboles de Relation（见 §01-02-01）
• 词汇表 Vocabulaire（见 §01-02-01）
• 签名 Signature（见 §01-02-01）
• 谓词 Prédicat（见 §01-02-01）
• 谓词演算 Calcul des Prédicats（见 §01-02-01）
• 底 Bottom（见 §01-02-01）
• 谬误 Absurd（见 §01-02-01）
• 变量符号 Symboles des Variables（见 §01-02-02）
• 项 Termes（见 §01-02-02）
• 应用 Application（见 §01-02-02）
• 闭项 Terme Clos（见 §01-02-02）
• 中缀表示法 Notation Infixée（见 §01-02-02）
• 前缀表示法 Notation Préfixée（见 §01-02-02）
• 项的尺寸 Taille（见 §01-02-02）
• 项的长度 Longueur（见 §01-02-02）
• 连结词 Connecteurs（见 §01-02-03）
• 量词 Quantificateurs（见 §01-02-03）
• 存在量词 Quantificateur Existentiel（见 §01-02-03）
• 全称量词 Quantificateur Universel（见 §01-02-03）
• 原子公式 Atomiques（见 §01-02-03）
• 公式 Formules（见 §01-02-03）
• 子公式 Sous-Formule（见 §01-02-03）
• 公式的语言 Langage de la Formule（见 §01-02-03）
• 公式的尺寸 Taille： 又称公式的长度 Longueur d’une Formule（见 §01-02-03）
• 公式的长度 Longueur（见 §01-02-03）
• 公式的主要运算符 Opérateur Principal： 又称公式的主要连结词 Connecteur Principal（见 §01-02-03）
• 公式的主要连结词 Connecteur Principal（见 §01-02-03）
• 约束变量 Variables Liées（见 §01-02-04）
• 哑变量 Variables Muettes（见 §01-02-04）
• 代换 Substituer（见 §01-02-04）
• 自由变量 Variables Libres（见 §01-02-04）
• 变量的出现 Occurence de Variable（见 §01-02-04）
• 变量的约束出现 Occurence Liée： 又称变量的哑出现 Occurence Muette（见 §01-02-04）
• 变量的哑出现 Occurence Muette（见 §01-02-04）
• 变量的自由出现 Occurence Libre（见 §01-02-04）
• $\alpha$ 等价 $\alpha$-Équivalentes（见 §01-02-04）
• 变量的捕获 Capturée（见 §01-02-04）
• de Bruijn 指数 Indices de De Bruijn（见 §01-02-04）
• 闭公式 Formule Close（见 §01-02-04）
• 闭包 Clôture（见 §01-02-04）
• 高阶逻辑 Logique d’Ordre Supérieur（见 §01-02-04）
• 多类型逻辑 Logique Multi-Sortes（见 §01-02-04）
• 命题演算 Calcul Propositionnel（见 §01-02-06）
• 命题变量 Variable Propositionnelles（见 §01-02-06）
• 自然推演 Dédution Naturelle（见 §01-03-01）
• 公理 Axiomes（见 §01-03-01）
• 相继式 Séquent（见 §01-03-02）
• 假设 Hypothèses（见 §01-03-02）
• 语境 Contexte（见 §01-03-02）
• 可被推演的相继式 Séquent Démontrable： 又称可被推导的相继式 Séquent Dérivable（见 §01-03-02）
• 可被推导的相继式 Séquent Dérivable（见 §01-03-02）
• 可被推演的公式 Formule Démontrable（见 §01-03-02）
• 派生规则 Règles Dérivées（见 §01-03-03）
• 前提 Prémisses（见 §01-03-03）
• 结论 Conclusion（见 §01-03-03）
• 规则的自下而上诠释 Lecture de Bas en Haut（见 §01-03-03）
• 规则的自上而下诠释 Lecture de Haut en Bas（见 §01-03-03）
• 引入规则 Règles d’Introduction（见 §01-03-03）
• 消去规则 Règles d’Élimination（见 §01-03-03）
• 肯定前件 Modus Ponens（见 §01-03-03）
• 模式 Schéma（见 §01-03-03）
• 推演的树状表示法 Notation Arborescente（见 §01-03-03）
• 卸载 Déchargé（见 §01-03-06）
• 主要假设 Hypothèses Principales（见 §01-03-06）
• 辅助假设 Hypothèses Auxiliaires（见 §01-03-06）
• 推演的线性表示法 Notation Linéaire（见 §01-03-07）
• 引理 Lemme（见 §01-03-08）
• 左规则 Règles Gauche（见 §01-03-08）
• 谬误消去（直觉主义） Absurdité Intuitionniste（见 §01-03-08）
• 皮尔士定律（见 §01-03-08）
• 排中律 Loi du Tiers Exclu（见 §01-03-08）
• 换质换位律 Loi de Contraposition（见 §01-03-08）

• 1.2.定义.1： 语言，常量符号，函数符号，关系符号（见 §01-02-01）
• 1.2.定义.3： 项（自下而上和自上而下定义），闭项，项的高度（见 §01-02-02）
• 1.2.定义.5： 项的尺寸（见 §01-02-02）
• 1.2.定义.6： 原子公式（语法定义），公式（语法定义）（见 §01-02-03）
• 1.2.定义.10： 子公式，公式的语言（见 §01-02-03）
• 1.2.定义.12： 公式的尺寸（又称长度）（见 §01-02-03）
• 1.2.定义.13： 公式的主要运算符（又称主要连结词）（见 §01-02-03）
• 1.2.定义.14： 公式的自由变量（见 §01-02-04）
• 1.2.定义.16： $\alpha$-等价（见 §01-02-04）
• 1.2.定义.19： 闭公式，闭包（见 §01-02-04）
• 1.2.定义.20： 代换（见 §01-02-05）
• 1.2.定义.21： 命题演算的公式集（见 §01-02-06）
• 1.3.定义.1： 相继式，语境，结论（见 §01-03-02）
• 1.3.定义.3： 可被推演的相继式，可被推演的公式（见 §01-03-02）

• 1.2.例子.2： 语言 $\setLan_1$，$\setLan_2$，$\setLan_3$，$\setLan_4$，$\setLan_5$（见 §01-02-01）
• 1.2.例子.4： 语言 $\setLan_1$，$\setLan_2$，$\setLan_3$，$\setLan_4$，$\setLan_5$ 中的项（见 §01-02-02）
• 1.2.例子.7： 语言 $\setLan_1$，$\setLan_2$，$\setLan_3$，$\setLan_4$，$\setLan_5$ 中的公式（见 §01-02-03）
• 1.2.例子.9： 语言 $\setLan_1$，$\setLan_5$ 中的公式（见 §01-02-03）
• 1.2.例子.11： 语言 $\setLan_5$ 中公式的子公式以及公式语言（见 §01-02-03）
• 1.2.例子.15： 语言 $\setLan_2$ 或 $\setLan_5$ 中公式的自由变量（见 §01-02-04）
• 1.2.例子.17： $\alpha$-等价（见 §01-02-04）
• 1.2.例子.22： 命题演算中的公式（见 §01-02-06）
• 1.3.例子.4： $\vdash (A \land B \to C) \leftrightarrow (A \to B \to C)$（见 §01-03-04）
• 1.3.例子.5： $\vdash (C\to A) \lor (C\to B)\to (C\to A\lor B)$（见 §01-03-04）
• 1.3.例子.6： $\vdash (\forall x~A\lor \forall x~B) \to \forall x~(A\lor B)$（见 §01-03-04）
• 1.3.例子.7： $\vdash \exists x~(A\wedge B) \to (\exists x~A \wedge \exists x~B)$（见 §01-03-04）
• 1.3.例子.8： $\vdash \neg (A\wedge B)\to (\neg A\vee \neg B)$（见 §01-03-04）
• 1.3.例子.9： 等号的对称性（见 §01-03-04）
• 1.3.例子.10： 等号的传递性（见 §01-03-04）
• 1.3.例子.11： 错误使用臆想规则推演出 $\vdash A\vee B \to A\wedge B$（见 §01-03-05）
• 1.3.例子.12： 错误使用存在消去推演出 $\vdash \exists x~A \to \forall x~A$（见 §01-03-05）
• 1.3.例子.13： 错误使用存在消去推演出 $\vdash \exists x~A \land \exists x~B \to \exists x~(A \land B)$（见 §01-03-05）
• 1.3.例子.14： 错误使用全称引入推演出 $\vdash \forall x~(A \lor B) \to \forall x~A \lor \forall x~B$（见 §01-03-05）
• 1.3.例子.15： 德摩根律 $\vdash \neg (A\vee B) \leftrightarrow (\neg A\wedge \neg B)$（见 §01-03-06）
• 1.3.例子.15b： 德摩根律 $\vdash \neg\exists x~A \leftrightarrow \forall x~\neg A$（见 §01-03-06）
• 1.3.例子.15c： 排中律 $\vdash A\vee \neg A$（见 §01-03-06）
• 1.3.例子.17： 1.3.例子.8 的线性表示法（见 §01-03-07）

• 1.3.命题.18： 切规则是可被推演的（见 §01-03-08）
• 1.3.命题.19： 合取左规则是可被推演的（见 §01-03-08）
• 1.3.命题.20： 析取左规则是可被推演的（见 §01-03-08）
• 1.3.命题.21： 箭头左规则是可被推演的（见 §01-03-08）
• 1.3.命题.22： 箭头左规则是可被推演的（见 §01-03-08）
• 1.3.命题.23： 否定左规则是可被推演的（见 §01-03-08）
• 1.3.命题.24： 存在左规则是可被推演的（见 §01-03-08）
• 1.3.命题.25： 谬误消去（直觉主义）是可被推演的（见 §01-03-08）
• 1.3.命题.26： 皮尔士定律是可被推演的（见 §01-03-08）
• 1.3.命题.27： 排中律是可被推演的（见 §01-03-08）
• 1.3.命题.28： 换质换位律是可被推演的（见 §01-03-08）
• 1.3.命题.29： 等号左规则是可被推演的（见 §01-03-08）
• 1.3.命题.29b： 等号左规则的推论1是可被推演的（见 §01-03-08）
• 1.3.命题.29c： 等号左规则的推论2是可被推演的（见 §01-03-08）
• 1.3.命题.30： 德摩根律（合取）是可被推演的（见 §01-03-08）
• 1.3.命题.30b： 德摩根率（析取）是可被推演的（见 §01-03-08）
• 1.3.命题.30c： 德摩根率（箭头）是可被推演的（见 §01-03-08）
• 1.3.命题.30d： 德摩根率（全称）是可被推演的（见 §01-03-08）
• 1.3.命题.30e： 德摩根率（存在）是可被推演的（见 §01-03-08）

• 1.2.记号.8： 连结词优先级（见 §01-02-03）
• 1.2.记号.18： 带自由变量的公式记法（见 §01-02-04）
• 1.3.记号.2： 语境（见 §01-03-02）
• 1.3.记号.16： 推演的线性表示法（见 §01-03-07）

• 1.2.1.注意.01： 常量符号，函数符号，关系符号（见 §01-02-01）
• 1.2.2.注意.01： 项（语法定义），函数的前缀中缀表示法（见 §01-02-02）
• 1.2.2.注意.02： 项的树状表示，项的函数的递归定义，项的性质的归纳证明（高度）（见 §01-02-02）
• 1.2.2.注意.03： 项的性质的归纳证明（尺寸）（见 §01-02-02）
• 1.2.3.注意.01： 公式（自上而下定义），二元关系的前缀中缀表示法（见 §01-02-03）
• 1.2.3.注意.02： 直觉主义视角下的1.2.例子.7（见 §01-02-03）
• 1.2.3.注意.03： 公式的树状表示（见 §01-02-03）
• 1.2.3.注意.04： 子公式在公式树状表示中的含义（见 §01-02-03）
• 1.2.3.注意.05： 公式函数的递归定义，公式性质的归纳证明（高度和尺寸）（见 §01-02-03）
• 1.2.4.注意.01： 变量的自由出现和约束出现（见 §01-02-04）
• 1.2.4.注意.02： $\alpha$-等价在人类和计算机的视角中（见 §01-02-04）
• 1.2.4.注意.03： 一阶逻辑的局限性，高阶逻辑（见 §01-02-04）
• 1.2.5.注意.01： 代换，重命名，连续代换（见 §01-02-05）
• 1.2.6.注意.01： 命题变量（见 §01-02-06）
• 1.3.2.注意.01： 相继式中语境和结论的闭性（见 §01-03-02）
• 1.3.2.注意.02： 可被推演的相继式和公式（见 §01-03-02）
• 1.3.3.注意.01： 关于全称引入和存在消去（见 §01-03-03）
• 1.3.3.注意.02： $\lnot$ 的另一种写法（见 §01-03-03）
• 1.3.4.注意.01： 1.3.例子.4（见 §01-03-04）
• 1.3.4.注意.02： 1.3.例子.6 里的全称引入、全称消去以及暗藏的等号消去（见 §01-03-04）
• 1.3.4.注意.03： 1.3.例子.7 里的存在消去、存在引入以及暗藏的等号消去（见 §01-03-04）
• 1.3.4.注意.04： 1.3.例子.8 其实是在证明德摩根律的一个方向（见 §01-03-04）
• 1.3.9.注意.01： 简化的线性记法中关于项的替换的补充说明（见 §01-03-09）

• 1.2.4.约定.01： 变量的自由出现和约束出现不可重名（见 §01-02-04）

• 1.3.6.译注.01： 1-3-例子-15 的线性表示法（见 §01-03-06）
• 1.3.6.译注.02： 1-3-例子-15b 的线性表示法（见 §01-03-06）

杂项

定义：ID 使用 defn:<编号>，Callouts 使用 [!info]

命题：ID 使用 prop:<编号>，Callouts 使用 [!info]

记号：ID 使用 note:<编号>，Callouts 使用 [!info]

例子：ID 使用 xmpl:<编号>，Callouts 使用 [!example]

注意：ID 使用 tips:S<章节>-<序号>，Callouts 使用 [!tip]

约定：ID 使用 conv:S<章节>-<序号>，Callouts 使用 [!tip]

译注：ID 使用 mark:<...>，Callouts 使用 [!note]