A Mathematical Introduction to Logic -- Section 2.4

发表于 分类于 ， 阅读次数：

\(\def\tauequ{\mathbin{\vDash\style{display: inline-block; transform: scaleX(-1)}{\vDash}}}\) \(\def\Dashv{\mathbin{\style{display: inline-block; transform: scaleX(-1)}{\vDash}}}\) \(\def\DEF{\sf{D\scriptsize EF}.\quad}\) \(\def\DEFi{\sf{D\scriptsize EF}^*.\quad}\) \(\def\DEFn{\sf{D\scriptsize EF}_*.\quad}\) \(\def\DEFin{\sf{D\scriptsize EF}^*_*.\quad}\) \(\def\llbracket{\unicode{x27E6}}\) \(\def\rrbracket{\unicode{x27E7}}\) \(\def\PROOF{\sf{P\scriptsize ROOF}.\quad}\) \(\def\MYNOTE{\sf{M\scriptsize{Y}}\sf{N\scriptsize{OTE}}.\quad}\) \(\def\EXAMPLE{\bf\sf{E\scriptsize{XAMPLES}}\quad}\) 这是一个关于数理逻辑的读书笔记和学习总结, 书名是A Mathematical Introduction to Logic (以下简称AMIL), 作者Herbert B. Enderton, University of California

点击这里进入AMIL的目录

本文是Section 2.4, 内容是介绍演绎计算(Deductive Calculus).

由于中文版错误太多, 大部分章节读的是英文第二版, 所以笔记也是中英文夹杂着写的. 英文一般是关键原文. 中文有的是原文的翻译, 有的是我自己的理解, 还有的是 为了做练习写的证明和计算过程.

前缀关键字的含义:

  • \(\DEF\) : 表明后面是概念定义.
  • \(^*\) : 表明后面内容并不是数学上的精确表达.
  • \(_*\) : 表明后面的内容并不来自于这本书.
  • \(\MYNOTE\) : 后面的内容是我用自己的话做的总结,或心得体会

Suppose that \(\Sigma\vDash\tau\).

  1. What methods of proof might be required to demonstrate that fact?
  2. Is there necessarily a proof at all?

\(\MYNOTE\) 这一章是用来回答整本书的前言中提出的四个最需要关注的问题中的问题2 为了避免自然语言中关于证明概念的混乱, 正式的证明(proof)在这本书里被叫做演绎(deduction). 这一章的目标就是, 给"演绎"提供一个精确的数学概念, 使其在一阶逻辑的语境下是充分的和正确的.

Formal Deductions

演绎的定义

\(\DEF\) A deduction of \(\varphi\) from \(\Gamma\) is a finite sequence \(\langle\alpha_0,\ldots, \alpha_n\rangle\) of formulas such that \(\alpha_n\) is \(\varphi\) and for each \(k\leq n\), either

  1. \(\alpha_k\) is in \(\Gamma\cup\Lambda\), or
  2. \(\alpha_k\) is obtained by modus ponens from two earlier formulas in the sequence; that is, for some \(i\) and \(j\) less than \(k\), \(\alpha_j\) is \(\alpha_i\rightarrow\alpha_k\).

If such a deduction exists, we say that \(\varphi\) is deducible from \(\Gamma\), or that \(\varphi\) is theorem of \(\Gamma\), and we write "\(\Gamma\vdash\varphi\)". If \(\Gamma\) is \(\varnothing\), we write "\(\vdash\alpha\)" in place of "\(\varnothing\vdash\alpha\)". If \(\Gamma=\{\varphi\}\), we write "\(\varphi\vdash\alpha\)" in place of "\(\{\varphi\}\vdash\alpha\)".

Where

  • \(\Lambda\) is an selected infinite set of formulas to be called logical axioms(逻辑公理).
  • \(\Gamma\) is a set of formulas.
  • And the modus ponens(假言推理) is a rule of inference. It is usually stated: From the formulas \(\alpha\) and \(\alpha\rightarrow\beta\) we may infer \(\beta\):

\[ \frac{\alpha,\alpha\rightarrow\beta}{\beta}. \]

\(\MYNOTE\) Deduction(演绎)被定义为一个finite sequence(有限序列).

归纳原则

\(\sf{I\scriptsize{NDUCTION}}\enspace\sf{P\scriptsize{RINCIPLE}}\quad\)(归纳原则) Suppose that \(S\) is a set of wffs that includes \(\Gamma\cup\Lambda\) and is closed under modus ponens. Then \(S\) contains every theorem of \(\Gamma\). Where we say that a set \(S\) of formulas is closed under modus ponens if whenever both \(\alpha\in S\) and \(\alpha\rightarrow\beta\in S\) then also \(\beta\in S\)

\(\MYNOTE\) 这个定义是section 1.4里给出的归纳原则的定义的特例. 书中描述定理的归纳与命题逻辑中归纳合式公式的区别有两点, 一是这里的modus ponens运算是部分定义的, 一个是生成的定理集合不是自由生成的. 这里什么是部分定义存疑.

逻辑公理

\(\DEF\) Say that a wff \(\varphi\) is a generalization(概化) of \(\psi\) iff for some \(n\geq 0\) and some variables \(x_1,\ldots,x_n\), \[ \varphi=\forall x_1\dots\forall x_n\psi. \] In particular, \(n=0\) is included. It means any wff is a generalization of itself.

The logical axioms are then all generalizations of wffs of the following forms (6 groups), where \(x\) and \(y\) are variables and \(\alpha\) and \(\beta\) are wffs:

  1. Tautologies;
  2. \(\forall x\alpha\rightarrow\alpha^x_t\), where t is substitutable for \(x\) in \(\alpha\);
  3. \(\forall x(\alpha\rightarrow\beta)\rightarrow(\forall x\alpha\rightarrow\forall x\beta)\);
  4. \(\alpha\rightarrow\forall x\alpha\), where \(x\) does not occur free in \(\alpha\)

And if the language includes equality, then we addition

  1. \(x=x\);
  2. \(x=y\rightarrow(\alpha\rightarrow\alpha')\), where \(\alpha\) is atomic and \(\alpha'\) is obtained from \(\alpha\) by replacing \(x\) in zero or more (but not necessarily all) places by \(y\).

How our particular list of logical axioms was formed.

  1. The tautologies were included to handle the sentential connective symbols.
  2. Group 2 reflects the intended meaning of the quantifier symbol.
  3. Group 3, group 4 and generalizations of axioms are added to prove the generalization theorem below.
  4. Group 5 and group 6 will turn out to be just enough to prove the crucial properties of equality.

Two objections(反对理由) to simply use the set of all valid formulas as logical axioms:

  1. The validity was defined semantically, but we need a class \(\Lambda\) with a finitary, syntactical definition. (前者"语义"是依赖于structure的, 后者"语法"仅跟符号的安排有关.)
  2. We prefer a decidable set \(\Lambda\), and the set of validities fails to be decidable.

Substitution 替换

\(\DEF\) Let \(x\) be a variable, \(t\) a term. We define the phrase "\(t\) is substitutable for \(x\) in \(\alpha\)"(对于合式公式\(\alpha\)中的变量\(x\), \(t\)是可替换的) as follows:

  1. For atomic \(\alpha\), \(t\) is always substitutable for \(x\) in \(\alpha\).
  2. \(t\) is substitutable for \(x\) in \(\lnot(\alpha)\) iff it is substitutable for \(x\) in \(\alpha\). \(t\) is substitutable for x in \((\alpha\rightarrow\beta)\) iff it is substitutable for \(x\) in both \(\alpha\) and \(\beta\).
  3. \(t\) is substitutable for \(x\) in \(\forall y\alpha\) iff either
    1. \(x\) does not occur free in \(\forall y\alpha\), or
    2. \(y\) does not occur in \(t\) and \(t\) is substitutable for \(x\) in \(\alpha\).

\(\MYNOTE\) 这个递归定义的关键就是上边第三点, 确保t中没有变量能够被\(\forall y\)前缀捕获(capture), 就是可替换的.

\(\EXAMPLE\)

  1. \(\varphi^x_x=\varphi\).
  2. \((Qx\rightarrow\forall{x}Px)^x_y=(Qy\rightarrow\forall{x}Px)\).
  3. If \(\alpha\) is \(\lnot\forall{y}x=y\), then \(\forall{x}\alpha\rightarrow\alpha^x_z\) is \(\forall{x}\lnot\forall{y}x=y\rightarrow\lnot\forall{y}z=y\).
  4. For \(\alpha\) as in 3, \(\forall{x}\alpha\rightarrow\alpha^x_y\) is \(\forall{x}\lnot\forall{y}x=y\rightarrow\lnot\forall{y}y=y\).

第4个是反例, y对于公式中的x是不可替换的.

Tautologies 重言式

可以用两种方法定义逻辑公理第一组的重言式.

\(\DEF\) Axiom group 1 consists of generalization of formulas to be called tautologies. These are the wffs obtainable from tautologies of sentential logic(having only the connectives \(\lnot\) and \(\rightarrow\)) by replacing each sentence symbol by a wff of the first-order language.

\(\DEF\)

  1. The prime formulas are the atomic formulas and those of the form \(\forall x\alpha\).
  2. The nonprime formulas are the others, i.e., those of the form \(\lnot\alpha\) or \(\alpha\rightarrow\beta\).

Any tautology of sentential logic (that uses only the connectives \(\lnot\), \(\rightarrow\)) where the sentence symbols is taken to be the prime formulas of the first-order language is in axiom group 1.

Three remarks:

  1. 这种替换将命题逻辑里的命题符号扩展到不可数.
  2. 不用包括所有的重言式, 因为没有好办法证明一个公式是重言式.
  3. 由于明确了一阶逻辑公式同时也是命题逻辑公式, 命题逻辑的概念也可以被使用. 注意如果\(\Gamma\) tautologically implies(重言蕴含) \(\varphi\), 那么\(\Gamma\) logically implies(逻辑蕴含) \(\varphi\), 但反过来不成立.

Theorem 24B

\(\Gamma\href{ #Deduction}{\vdash}\varphi\) iff \(\Gamma\cup\Lambda\) tautologically implies \(\varphi\)

Deductions and Metatheorems

定理"theorem"这个词本节有两个含义, 一个实在一阶逻辑里若\(\Gamma\vdash\alpha\), 我们说\(\alpha\)是\(\Gamma\)的定理. 但我们也把一些自然语言表达的陈述叫做定理. 一般这不会造成混淆. 但为了避免误解, 也可以把本节如下一些自然语言描述的定理称作元定理(metatheorem), 来强调它们是关于演绎和定理的结果.

Generalization Theorem 概化定理

If \(\Gamma\href{ #Deduction}{\vdash}\varphi\) and \(x\) do not occur free in any formula in \(\Gamma\), then \(\Gamma\vdash\forall{x}\varphi\)

反映了一个非形式的感觉: 如果在没有对\(x\)做特定假设的前提下能够证明一个包含_\(x\)_的公式, 那么就可以说"因为\(x\)是任意的, 我们有\(\forall x\_x\_\). 一旦给定了从\(\Gamma\)到\(\varphi\)的演绎, 就可以将其转化为从\(\Gamma\)到\(\forall x\varphi\)的演绎.

Lemma 24C (Rule T) 规则T

If \(\Gamma\href{ #Deduction}{\vdash}\alpha_1,\ldots,\Gamma\vdash\alpha_n\) and \(\{\alpha_1,\ldots,\alpha_n\}\) tautologically implies \(\beta\), then \(\Gamma\vdash\beta\).

Deduction Theorem 演绎定理

If \(\Gamma;\gamma\href{ #Deduction}{\vdash}\varphi\), then \(\Gamma\vdash(\gamma\rightarrow\varphi)\)

反向也成立, 实际上反向就是假言推论.

Corollary 24D (Contraposition) 逆否

\(\Gamma;\varphi\href{ #Deduction}{\vdash}\lnot\psi\) iff \(\Gamma;\psi\vdash\lnot\varphi\)

Corollary 24E (Reductio ad Absurdum) 归谬法, 反证法

\(\DEF\) Say that a set of formulas is inconsistent iff for some \(\beta\), both \(\beta\) and \(\lnot\beta\) are theorems of the set.

Corollary 24E(Reductio ad Absurdum): If \(\Gamma;\varphi\) is inconsistent, then \(\Gamma\href{ #Deduction}{\vdash}\lnot\varphi\).

\(\EXAMPLE\) 证明: \(\vdash\exists{x}\forall{y}\varphi\rightarrow\forall{y}\exists{x}\varphi\) Working backward:

  • It suffices to show that \(\exists{x}\forall{y}\varphi\vdash\forall{y}\exists{x}\varphi\), by the deduction theorem.
  • It suffices to show that \(\exists{x}\forall{y}\varphi\vdash\exists{x}\varphi\), by the generalization theorem.
  • It suffices to show that \(\lnot\forall{x}\lnot\forall{y}\varphi\vdash\lnot\forall{x}\lnot\varphi\), as this is the same as the preceding.
  • It suffices to show that \(\forall{x}\lnot\varphi\vdash\forall{x}\lnot\forall{y}\varphi\), by the contraposition (and rule T)
  • It suffices to show that \(\forall{x}\lnot\varphi\vdash\lnot\forall{y}\varphi\), by the generalization theorem.
  • It suffices to show that \(\{\forall{x}\lnot\varphi, \forall{y}\varphi\}\) is inconsistent, by the reductio ad absurdum.
  • It suffices to show that \(\forall{x}\lnot\varphi\vdash\lnot\varphi\) and \(\forall{y}\varphi\vdash\varphi\) by anxiom group 2 and modus ponens

Strategy 策略

Assume that \(\varphi\) is indeed deducible from \(\Gamma\) but that you are seeking a proof of this fact. There are several cases:

  1. Suppose that \(\varphi\) is \((\psi\rightarrow\theta)\). Then it will suffice to show that \(\Gamma;\psi\vdash\theta\).
  2. Suppose that \(\varphi\) is \(\forall{x}\psi\). If \(x\) does not occur free in \(\Gamma\), then it will suffice to show that \(\Gamma\vdash\psi\). (Even if \(x\) should occur free in \(\Gamma\), the difficulty can be circumvented. These will always be a variable \(y\) such that \(\Gamma\vdash\forall y\psi^x_y\) and \(\forall{y}\psi^x_y\vdash\forall{x}\psi\) re-replacement lemma)
  3. Finally, suppose that \(\varphi\) is the negation of another formula.
    1. If \(\varphi\) is \(\lnot(\psi\rightarrow\theta)\), then it will suffice to show that \(\Gamma\vdash\psi\) and \(\Gamma\vdash\lnot\theta\) (by rule T.
    2. If \(\varphi\) is \(\lnot\lnot\psi\), then of course it will suffice to show that \(\Gamma\vdash\psi\).
    3. The remaining case is where \(\varphi\) is \(\lnot\forall x\psi\). It would suffice to show that \(\Gamma\vdash\lnot\psi^x_t\), where t is some term substitutable for \(x\) in \(\psi\). (Unfortunately this is not always possible.) Or contraposition is handy here: \(\Gamma;\alpha\vdash\lnot\forall x\psi\) iff \(\Gamma;\forall x\psi\vdash\lnot\alpha\). (A variation on this is: \(\Gamma;\forall y\alpha\vdash\lnot\forall x\psi\) if \(\Gamma;\forall x\psi\vdash\lnot\alpha\).) If all else fails, one can try reductio ad absurdum.

\(\MYNOTE\) 这里就是根据定理的语法形式给出了常用的证明策略.

\(\EXAMPLE\)

  • Q2A. If \(x\) does not occur free in \(\alpha\), then \(\vdash(\alpha\rightarrow\forall x\beta)\leftrightarrow\forall x(\alpha\rightarrow\beta)\).
  • Q3B. If \(x\) does not occur free in \(\alpha\), then \(\vdash(\exists x\beta\rightarrow\alpha)\leftrightarrow\forall x(\beta\rightarrow\alpha)\).
  • \(\vdash x=y\rightarrow\forall zPxz\rightarrow\forall zPyz\)

Theorem 24F (Generalization on Constants 常量概化定理)

Assume that \(\Gamma\vdash\varphi\) and that \(c\) is a constant symbol that does not occur in \(\Gamma\). Then there is a variable \(y\) (which does not occur in \(\varphi\)) such that \(\Gamma\vdash\forall y\varphi^c_y\). Furthermore, there is a deduction of \(\forall y\varphi^c_y\) from \(\Gamma\) in which \(c\) does not occur.

\(\MYNOTE\) \(c\)在\(\Gamma\)里不存在, 在\(\varphi\)里存在. \(y\)在\(\varphi\)里不存在. 整个演绎过程里可以没有\(c\).

Gorollary 24G

Assume that \(\Gamma\vdash\varphi^x_c\), where the constant symbol \(c\) does not occur in \(\Gamma\) or in \(\varphi\). Then \(\Gamma\vdash\forall x\varphi\), and there is a deduction of \(\forall x\varphi\) from \(\Gamma\) in which \(c\) does not occur.

Corollary 24H (Rule EI)

Assume that the constant symbol \(c\) does not occur in \(\varphi\), \(\psi\), or \(\Gamma\), and that \[\Gamma;\varphi^x_c\vdash\psi\] Then \[\Gamma;\exists x\varphi\vdash\psi\] and there is a deduction of \(\psi\) from \(\Gamma;\exists x\varphi\) in which \(c\) does not occur.

"EI" stands for "existential instantiation"(存在实例).

Alphabetic Variants 字母变换式

Theorem 24I (Existence of Alphabetic Variants 字母变换式存在定理)

Let \(\varphi\) be a formula, \(t\) a term and \(x\) a variable. Then we can find a formula \(\varphi'\) (which differs from \(\varphi\) only in the choice of quantified variables) such that

  1. \(\varphi\vdash\varphi'\) and \(\varphi'\vdash\varphi\);
  2. \(t\) is substitutable for \(x\) in \(\varphi'\).

这个定理中构造的\(\varphi'\), 称为Alphabetic variants(字母变换式). 该定理的含义是: 在无法进行替换时, 选择正确的字母变换式可以解决问题.

Equality 相等

  • EQ1: \(\vdash\forall xx=x\)
  • EQ2. \(\forall x\forall y(x=y\rightarrow y=x)\)
  • EQ3: \(\vdash\forall x\forall y\forall z(x=y\rightarrow y=z\rightarrow x=z)\)
  • EQ4: for a two-place predicate symbol \(P\): \[\vdash\forall x_1\forall x_2\forall y_1\forall y_2(x_1=y_1\rightarrow x_2=y_2\rightarrow Px_1 x_2\rightarrow Py_1 y_2)\]
  • EQ5. Let f be a two-place function symbol. Then \[\vdash\forall x_1\forall x_2\forall y_1\forall y_2(x_1=y_1\rightarrow x_2=y_2\rightarrow fx_1 x_2=fy_1 y_2)\]