计算机数理逻辑-一阶逻辑-语法与语义

1. 引入

命题逻辑对于算术等数学理论的形式化来说，表现力并不充分。一个算术表达式，如$x+2>y-1$，既不是真的，也不是假的。

  1. 它的真假取决于变量x和y的值
  2. 我们需要将运算符+和-的含义形式化，作为将一对数字映射为一个数字的函数
  3. 像>这样的关系运算符必须被形式化为将一对数字映射为真值 (也就是predicate)

2. 命题逻辑vs一阶逻辑

  1. 命题逻辑（Propositional Logic）

    1. 形如 ¬P，P∧Q，P∨Q，P → Q ，P↔Q的语句，值为True或者False
    2. 推理规则较简单，往往通过（1.真值表 2.为数不多的推理规则，例如Modus ponesn等几个）
    3. 缺点：不能或者很难表示复杂的语句，不能记录推理过程中的变化

  2. 一阶逻辑（First Order Logic），简称FOL

    1. 包含的东西有常量（Constant symbol），谓词符号（Predicate symbol），函数符号（Function symbol），变量（Variable），联结词（来源于命题逻辑 ∧∨→↔），量词（Quantifiers, ∃∀）

  3. 命题逻辑(很少部分人叫它作零阶逻辑). 在命题逻辑里, 每一个字母就代表一个命题, 所以命题逻辑只能表达句子之间的关系, 比如“p&q”, “if p then q”等等的真值如何从p和q的真值中计算出来.

  4. 一阶逻辑则引入了两个量词, 即universal quantifier(倒A)和existential quantifier(倒E), 并且加入了一阶谓词和individual variables和individual constants. 这些导致一阶逻辑可以量化individuals in the domain.

    1. 比如经典的三段论就可以被一阶逻辑表达
      1
      2
      3
      4
      5
      6
      7
      For all x, Hx->Mx

      Hs

      ----

      Ms

2.1. vs Propositional Logic vs Set Theory vs Elementary Number Theory

Propositional Logic

  • Equality: no
  • Predicate symbols: A1, A2, . . .
  • Constant symbols: none
  • Function symbols: none

Set Theory

  • Equality: yes
  • Predicate symbols: ∈
  • Constant symbols: ∅
  • Function symbols: none

Elementary Number Theory初等数论

  • Equality: yes
  • Predicate symbols: <
  • Constant symbols: 0
  • Function symbols: S (successor), +, ×, exp

3. 集合论vs一阶逻辑

  • 集合论作为公理系统，一阶逻辑作为推理系统，共同为数学打下基石
  • 谈论某一理论时，都需要有上层语言（meta-language）作为基础。对于最上层的语言研究一般归于哲学的范畴
    • 基于上层语言，我们可以定义一阶语言（一阶逻辑的语言），语言中字母表、项、公式的不同可以产生不同的“子语言”。如：初等算术语言，群论语言，集合论语言
    • 定义一阶语言的模型，模型对语言做出解释（可以看成是语义部分）。譬如对于初等算术语言，有初等算术的标准模型
    • 一阶语言的推理系统给出了一阶逻辑的语法。不同的推理系统如自然推理系统和 PK 推理系统可以证明是等价的。同时注意到，推理系统可以独立于模型（语义）而存在。而推理系统的 soundness 和 completeness 保证了语义与语法的一致性
  • 同阶下，一阶语言的集合论是一阶逻辑的一部分（一阶语言+公式集），但一阶逻辑又不能表达所有的集合论（高阶）

4. Syntax

Logical Symbols

  • Parentheses: (, )
  • Propositional connectives: ¬, ∨, ∧, →, ↔
  • Variables: v1, v2, . . .
  • Quantifiers: ∀, ∃
    • Quantifiers allow a purely syntactical expression of the statement that the relation represented by a predicate is true for some or all elements of the domain
    • 量词允许以纯语法的方式来表达谓词所代表的关系对域中的某些或所有元素来说是真的

Parameters

  • Equality symbol (optional): =
  • Predicate谓词 symbols: e.g. p(x), x > y
  • Constant symbols: e.g. 0, John, π
  • Function symbols: e.g. f(x), x + y, x +[2] y

注意

  • 大写P、Q、R等默认位predicate
  • 小写p、q、r才是函数
  • not非+predicate有意义，但非+函数没有意义

4.1. Predicate 谓词

  • Predicates are used to represent functions from a domain to truth values
    • 谓词被用来表示从域到真值的函数
    • $p^n$ is called an n-ary predicate

4.2. Quantifier 量词

  • ∀ is the universal quantifier and is read for all.
  • ∃ is the existential quantifier and is read there exists
  • A universal or existential formula ∀xA or ∃xA is a quantified formula
  • In many presentations of first-order logic, ∀ is defined in the logic and ∃ is considered to be an abbreviation of ¬ ∀¬

4.3. 断言符号？

断言是容许一个、甚至多个对象，所以对于自然数 $n,j$ 我们约定 $A_{j}^{n}(x_1,x_2,…,x_n)$ 为一阶逻辑的合法词汇，它在直观上表示一个有 ${\displaystyle{} n}$ 个”对象”的断言，我们称它为 ${\displaystyle{} n}$ 元断言符号。下标的自然数 ${\displaystyle{} j}$ 只是拿来和其他同为 ${\displaystyle{} n}$ 元的断言符号作区别

4.4. signature 标识

  • 在一阶逻辑中的标识(signature)为包含函数常数(function constants)和谓词常数(predicate constants)俩种元素的一个集合

  • 例如：$Σ = (F, P) = ({ a_1,…,a_n, f_1,…, f_k } , { \simeq{}/2, P_1,…, P_m } )$

4.5. arity 元数

函数或运算的元数是指所需的参数或算子的数量。关系的元数则是指其对应之笛卡儿积的维度

  • 一元unary函数、二元binary…
  • Equality （not Assignment）is a special predicate symbol of arity 2.
  • Constant symbols can also be thought of as functions whose arity is 0.

5. Formula

  • 也就是WFF合式公式，即一切符合一阶逻辑语法的组合，包括用谓词量词函数变量联结词操作符进行组合

5.1. Atomic Formulas 原子公式

  • An atomic formula is an expression of the form: $P(t_1, . . . , t_n)$ here P is a predicate symbol of arity n and $t_1,. . . ,t_n$ are terms.
    • 原子公式=n元谓词+n项
  • If the language includes the equality symbol, we consider the equality symbol to be a special predicate of arity 2

5.2. Well-formed Formulas 合式公式

符合语法规则的公式

  • The set of well-formed formulas is the set of expressions generated from the atomic formulas by the operations E¬, E→, and $Q_{i}i$ = 1, 2, . . .
  1. 原子公式为合式公式。(美观起见，在原子公式外面包一层括弧也是公式)
  2. 若 ${\displaystyle {\mathcal {A}}}$ 为合式公式，则 (${\displaystyle (\neg {\mathcal {A}})}$ 为合式公式。
  3. 若 ${\displaystyle {\mathcal {A}}}$ 与 ${\displaystyle {\mathcal {B}}}$ 为公式，则 ${\displaystyle ({\mathcal {A}}\Rightarrow {\mathcal {B}})}$ 为公式。
  4. 若 ${\displaystyle {\mathcal {A}}}$ 为公式， ${\displaystyle x}$ 为任意变量，则 ${\displaystyle (\forall x{\mathcal {A}})}$ 为公式。 (美观起见 ${\displaystyle (\forall x){\mathcal {A}}:=\forall x{\mathcal {A}}}$ ，也就是里面的量词有无外包括弧都是公式)
    合式公式只能透过以上四点，于有限步骤内置构出来

5.3. Quantified formula 量化公式

  • A universal or existential formula $∀xA$ or $∃xA$ is a quantified formula.
  • x is the quantified variable and its scope is the formula A.
  • It is not required that x actually appear in the scope of its quantification.

5.3.1. Free and Bound Variables 自由变量和约束变量

量词所施用的公式被称为 量词的范围(scope) 。若变量 ${\displaystyle x}$ 某次出现在 ${\displaystyle \forall x}$ 的范围内，称这样出现的 ${\displaystyle x}$ 为不自由/被约束的 ${\displaystyle x}$ (not free/bounded)；反过来说，不出现在 ${\displaystyle \forall x}$ 的范围内的某个 ${\displaystyle x}$ 被称为自由的 ${\displaystyle x}$，（∃同理）

  • （封闭公式、句子）If no variable occurs free in a $wff x$, then $x$ is a sentence
  • If α is an atomic formula, then
    • x occurs free in α iff x occurs in α.
    • x occurs free in (¬α) iff x occurs free in α.
    • x occurs free in (α → β) iff x occurs free in α or in β.
    • x occurs free in ∀ $v_i$ α iff x occurs free in α and $x\neq{v_i}$

5.4. ground formula 基态公式

ground=no variables 不含变量的

  • A ground term is a term which does not contain any variables. (也就是只包括常量和函数名)
  • A ground atomic formula is an atomic formula, all of whose terms are ground. (也就是只包括谓词，常量和函数名)
  • A ground literal is a ground atomic formula or the negation of one.
    • 也就是一阶逻辑和命题逻辑中的字面量不是一个东西
  • A ground formula is a quantifier-free无量词 formula, all of whose atomic formula are ground.
  • A is a ground instance of a quantifier-free formula A′ iff it can be obtained from A′ by substituting ground terms for the (free) variables in A′
    • 用ground term来替代变量
  • The terms a, f(a,b), g(b,f(a,b)) are ground.
  • P(f(a,b),a) is a ground atomic formula (also a ground literal)
  • ¬ P(f(a,b),a) is a ground literal.
  • P(f(x,y),a) is not a ground atomic formula because of the variables x,y

6. Semantic: Interpretation

  • In propositional logic, the truth of a formula was determined by a truth assignment over the propositional symbols.
  • In first-order logic, we use a model (also called a structure) to determine the truth of a formula
  • In propositional logic, an interpretation is a mapping from atomic propositions to truth values.
  • In first-order logic, the analogous concept is a mapping from atomic formulas to truth values.
    • However, atomic formulas contain variables and constants that must be assigned elements of some domain; once that is done, the predicates are interpreted as relations over the domain.（比如大于小于关系）

6.1. Closed Formula 闭公式

6.1.1. Closure 闭包

  • If a formula has no free variables, it is closed. If ${x_1,…,x_n}$ are all the free variables of A, the universal closure of A is $∀x_1 …∀x_n$ A and the existential closure is $∃x_1…∃x_n$ A.

Example

  1. p(x,y) has two free variables x and y, ∃yp(x,y) has one free variable x and ∀x∃yp(x,y) is closed. The universal closure of p(x,y) is ∀x∀yp(x,y) and its existential closure is ∃x∃yp(x,y).
  2. In $∀xp(x)∧q(x)$, the occurrence of x in $p(x)$ is bound and the occurrence in $q(x)$ is free. The universal closure is $∀x(∀xp(x)∧q(x))$.
    1. Obviously, it would have been better to write the formula as $∀xp(x)∧q(y)$ with y as the free variable; its universal closure is ∀y(∀xp(x)∧q(y))
    2. 这个其实就是把 $∀xp(x)$ 简写了，实际应该就是 $∀x(p(x))$，量词后紧跟的就是作用域(scope)

6.1.2. Validity and Satisfiability

  • Let A be a closed formula of first-order logic
    • A is true in I or I is a model for A iff $v_I(A)=T$ . Notation: I⊧A.
    • A is valid if for all interpretations I, I⊧A. Notation: ⊨A
    • A is satisfiable if for some interpretation I, I⊧A.
    • A is unsatisfiable if it is not satisfiable.
    • A is falsifiable if it is not valid

$∀x∀y(P(x,y)→p(y,x))$

  • The formula is satisfiable in an interpretation where P is assigned a symmetric relation like =. It is not valid because the formula is falsified in an interpretation that assigns to p a non-symmetric relation like <

6.2. An Interpretation for a Set of Formulas

In propositional logic, the concept of interpretation and the definition of properties such as satisfiability can be extended to sets of formulas. The same holds for first-order logic

  • Let U={A 1,…} be a set of formulas where {p 1,…,p m } are all the predicates appearing in all A i ∈S and {a 1,…,a k } are all the constants appearing in all A i ∈S. An interpretation $I_v$ for S is as triple:
    • ${D,{R_1,…R_n},{d_1,…d_n}}$
  • where D is a non-empty set called the domain, R i is an $n_i$-ary relation on D that is assigned to the $n_i$-ary predicate p i and d i ∈D is an element of D that is assigned to the constant a i

6.3. Assignment

6.3.1. Interpretation vs Substitution vs Assignment

  • 有domain和无domain的区别
  • 替代只是单纯的重命名
  • 感觉上，assignment的结果是值，而interpretation的是true/false
    • 但实际看来应该是一个东西

7. Logical Equivalence in FOL

  • Let U={A 1,A 2} be a pair of closed formulas. A 1 is logically equivalent to A 2 iff $v_{I_{U}}(A_1)=v_{I_{U}}(A_2)$ for all interpretations . Notation: $A_1≡A_2$

对等duality公式

  • 用于公式化简和转化为范式

  • ¬∀x.A ≡ ∃x.¬A

  • ¬∃x.A ≡ ∀x.¬A

  • Theorem (Equivalent Replacement Theorem)
    • Suppose A, B, C are first-order formulas and A is a subformula of C
    • If A ≡ B, then C(. . . A . . .) ≡ C(. . . B . . .)

8. 语义表

语义表的方法对于显示一个公式是不可满足的来说是合理和完整的，但是它不是一个可满足性的决定程序，因为表的分支可能是无限的。当一个tableau被构造出来时，一个普遍量词后面跟着一个存在量词可能会导致一个无限的分支：存在公式被用一个新的常数实例化，然后普遍公式的实例化会导致一个新的存在量词公式的出现，如此无限地下去。有一些公式只在无限域中是可满足的。

9. 参考