计算机数理逻辑-命题逻辑-演绎

1. 形式语言

语言按照语法分类大致可分为自然语言与形式语言两种。

自然语言（Natural Language）就是人类讲的语言，比如汉语、英语等。此类语言不是人为设计的语言，而是自然进化而成的。

形式语言（Formal Language）是为了满足特定的应用而人为设计的语言。例如数学使用的数字与运算符号、化学使用的分子式。编程语言同样也是一种形式语言，是专门用来表达计算过程的形式语言。

形式语言有严格的语法（Syntax）规则。语法规则是由符号（Token）与结构（Structure）的规则组成。

Token 相当于自然语言中的单词与标点、数学式中的数字与运算符。例如 6 = 3 + 3$，之所以无法构成一个等式，是因为 $ 符号并不属于合法的 Token 符号。

结构则是指 Token 的排列方式， 如 3 = + 3 虽然加号与等号均为核发的 Token 运算符，但是存在一定的结构错误。

关于 Token 的规则称为词法（Lexical）规则。而关于结构的规则称为语法（Semantic）规则。

当阅读一个自然语言句子或是形式语言句子时，首先要明白词法规则（Token），然后需要弄清楚句子的语法结构（如学习阅读外语句子时）。分析句子结构的过程就是解析（Parse）的过程

例如

  • 正则表达式
  • 自动机

2. Deductive Proof

The deductive systems studiedwere developed in an attempt to formalize mathematical reasoning.

  • 所研究的演绎系统是为了使数学推理正规化而开发的。

引入演绎证明方法的意义

  • The set of axioms may be infinite
  • Very few logics have decision procedures like propositional logic
  • A decision procedure may not give insight into the relationship between the axioms and the theorem
  • A decision procedure produces a ‘yes/no’ answer, so it is difficult to recognize intermediate results (lemmas). Clearly, the millions of mathematical theorems in existence could not have been inferred directly from axioms
    • A decision procedure produces a ‘yes/no’ answer, so it is difficult to recognize intermediate results (lemmas)

type

  • The second one $H$ will be familiar because it is a formalization of step-by-step proofs in mathematics: It contains a set of three axioms and one rule of inference; proofs are constructed as a sequence of formulas, each of which is either an axiom (or a formula that has been previously proved) or a derivation of a formula from previous formulas in the sequence using the rule of inference.
  • The system $G$ will be less familiar because it has one axiom and many rules of inference, but we present it first because it is almost trivial（恒真？） to prove the soundness and completeness of $G$ from its relationship with semantic tableaux

2.1. deductive system 演绎系统

  • A deductive system is a set of formulas called axioms and a set of rules of inference.
    • 公理axioms是用来推导其他命题的起点。和定理Theorem不同，一个公理（除非有冗余的）不能被其他公理推导出来，否则它就不是起点本身
    • A proof in a deductive system is a sequence of formulas $S={A_1,…,A_n}$ such that each formula A i is either an axiom or it can be inferred from previous formulas of the sequence $A_{j_1},…A_{j_n}$, where $j_1<⋯<j_k <i$, using a rule of inference. For $A_n$ , the last formula in the sequence, we say that $A_n$ is a theorem定理, the sequence S is a proof of $A_n$ , and $A_n$ is provable, denoted $⊢A_n$ . If ⊢A, then A may be used like an axiom in a subsequent proof.

      In proof theory, the turnstile is used to denote “provability” or “derivability”. For example, if T is a formal theory and S is a particular sentence in the language of the theory then T⊢S means that S is provable from T

  • if T, then S

一个 矢列 是一个二元组 (Γ,∆)，记为 Γ ⊢ ∆，这里 Γ,∆ 为命题的 有穷集合（可为空），称 Γ 为前件，∆ 为后件.命题逻辑的自然推理系统 G′ 由以下公理和规则组成，Γ,∆,Λ,Θ 表示任何命题有穷集合，A,B 表示任何命题，Γ,A,∆为集合 Γ ∪ {A} ∪ ∆ 的简写.

  • 规则的上矢列S1,S2 被称为前提，下矢列S 被称为结论.G′ 中规则被称为推
    理规则，规则中被作用的命题被称为主命题，而不变的命题被称为辅命题.
  • 每个公理和规则是模式（schema），它们可有无穷多个实例.

sequent序贯

  • If U and V are (possibly empty) sets of formulas, then U⇒V is a sequent

2.2. 演绎vs归纳

3. Gentzen System

相继式演算（Sequent calculus，又译矢列演算、矢列式演算、序贯演算）

  • An axiom of $G$ is a set of literals U containing a complementary pair. Rule of inference are used to infer a set of formulas U from one or two other sets of formulas $U_1$ and $U_2$; there are two types of rules
  • Let ${α_1,α_2}\subseteq{U_1}$ and let $U_1’=U_1-{ α_1,α_2 }$. Then $U=U_1’\cup{α}$ can be inferred
  • Let ${β_1}⊆U_1$, ${β_2}⊆U_2$ and let $U_1’=U_1-{β_1}$, $U_2’=U_2-{β_2}$. Then $U=U_1’\cup{U_2’}\cup { β }$ can be inferred.

  • The set or sets of formulas $U_1,U_2$ are the premises前提 and set of formulas U that is inferred is the conclusion结论

  • A set of formulas $U$ that is an axiom or a conclusion is said to be proved (aka derive推导), denoted ⊢U

    • 这个符号因为名叫turnstile闸机

  • $⊢A$

    • I know A is true
    • A is a theorem in the system

  • $P⊢Q$

    • From P, I know that Q
    • Q is derivable from P in the system 衍生
    • P is provable from Q 证明

  • The following notation is used for rules of inference:

  • Prove ⊢(p∨q)→(q∨p) in G

3.1. vs Semantic Tableaux

  • 上下翻转
  • Let A be a formula in propositional logic. Then ⊢A in $G$ if and only if there is a closed semantic tableau for ¬ A.
    • 当且仅当语义树叶子结点全部时互补文字集时，公式才可证

3.2. ⊨ vs ⊢ （蕴含 vs 可证）

⊨A if and only if ⊢A in $G$.

  • A为真当且仅当A可证

    A is valid iff ¬ A is unsatisfiable iff there is a closed semantic tableau for ¬ A iff there is a proof of A in $G$

想像文氏图有助于理解，下图为蕴含

  • Soundness：若 Γ ⊢ ∆ 在 G′ 中可证，则 Γ ⊢ ∆ 有效
  • completeness：若 Γ ⊢ ∆ 有效，则 Γ ⊢ ∆ 在 G′ 中可证.这就是 G′ 的完全性

3.3. ⊨ vs ⊢ vs →

  • $a⊢b \equiv ⊢a\rightarrow{b} \equiv \lnot a \lor b ⊢ \bot$
  • $a⊢b \equiv ⊨a\rightarrow{b}$

注意⊧不是该语言中的符号，而是在上层语言 (meta-language) 中.在上层语言中，人们也需要用联结词如 iff，not，and，or，imply 等

上层语言是一种用于描述另一种语言的语言

4. Hilbert System

In Gentzen systems there is one axiom and many rules of inference, while in a Hilbert system there are several axioms but only one rule of inference.

在Gentzen系统中，有一个公理和许多推理规则，而在Hilbert系统中，有几个公理但只有一个推理规则

  • axioms：
  • rule of inference： modus ponens辩证法
    • the formula B can be inferred from A and A→B
  • 实际上就是 Binary Resolution(BR) 归结的特例

5. 相继式演绎 vs 希尔伯特演绎

Both the deductive systems and are sound and complete. Completeness of follows directly from the completeness of the method of semantic tableaux as a decision procedure for satisfiability and validity in propositional logic. However, the method of semantic tableaux is not very efficient.

6. 参考