计算机数理逻辑-一阶逻辑-项与范式

2022-02-18

1. Terms 项

Variables.
- Any variable, constant or 0-ary function symbol is a term.
Functions.
- Any expression $f(t_1,…,t_n)$ of n arguments (where each argument $t_i$ is a term and $f$ is a function symbol of valence n) is a term. In particular, symbols denoting individual constants are nullary function symbols, and thus are terms.

Only expressions which can be obtained by finitely many applications of rules 1 and 2 are terms

2. prenex conjunctive normal form(PCNF) 前束范式

A formula is in prenex conjunctive normal form (PCNF) iff it is of the form:
- $Q_1x_1…Q_nx_nM$
where the $Q_i$ are quantifiers and $M$ is a quantifier-free formula in CNF. The sequence $Q_1x_1⋯Q_nx_n$ is the prefix and $M$ is the matrix

如果一个公示可以被写为量词在前，随后是被称为母体的无量词部分，则称其为前束范式的，所有经典逻辑公式都逻辑等价于某个前束范式公式

example

Let A be a closed formula in PCNF whose prefix consists only of universal quantifiers. The clausal form of A consists of the matrix of A written as a set of clauses
所以上个例子可以写为：

2.1. Skolem’s Theorem 斯科伦定理

In propositional logic, every formula is equivalent to one in CNF, but this is not true in first-order logic. However, a formula in first-order logic can be transformed into one in clausal form without modifying its satisfiability. 在不改变及可满足性的情况下
Skolem: Let $A$ be a closed formula. Then there exists a formula $A^′$ in clausal form such that $A≈A^′$

2.1.1. ≈ vs ≡

A≈A′ means that A is satisfiable if and only if A′ is satisfiable; that is, there exists a model for A if and only if there exists a model for A′. (may not be the same model)
This is not the same as logically equivalence A≡A′, which means that for all models $I$, $I$ is a model for A if and only if it is a model for A′. (same model)

In A=∀x∃yp(x,y), the quantifiers can be read: for all x, produce a value y associated with that x such that the predicate p is true.
But our intuitive concept of a function is the same: y=f(x) means that given x, f produces a value y associated with x. The existential quantifier can be removed giving A′=∀xp(x,f(x)).
- y=f(x)意味着给定x，f产生一个与x相关的值y。可以删除存在量词，给出 $A^′=∀xp(x,f(x))$

2.2. Skolem’s Algorithm 斯科伦算法

目的：将任意一阶逻辑公式转化为clause form

例子：$∀x(p(x)\rightarrow{q(x)})\rightarrow{}(∀xp(x)\rightarrow{}∀xq(x))$

Eliminate all binary Boolean operators other than ∨ and ∧
1. 消去除 ∨ 和 ∧ 外的所有二元操作符
Push negation operators inward, collapsing double negation, until they apply to atomic formulas only
1. 将否定运算符向内推，折叠双重否定，直到否定运算符只作用于原子式
Extract quantifiers from the matrix. Repeat until all quantifiers appear in the prefix and the matrix is quantifier-free.
1. 从矩阵中提取量词
2. 重复以上步骤，直到所有的量词都出现在前缀中，并且矩阵无量词
Use the distributive laws to transform the matrix into CNF. The formula is now in PCNF.
1. 使用分配律将矩阵转换为CNF。该公式现在是PCNF
For every existential quantifier $∃x$ in A, let $y_1,…,y_n$ be the universally quantified variables preceding $∃x$ and let f be a new n-ary function symbol.
1. Delete $∃x$ and replace every occurrence of x by $f(y_1,…,y_n)$.
2. If there are no universal quantifiers preceding ∃x, replace x by a new constant (0-ary function).
3. These new function symbols are Skolem functions and the process of replacing existential quantifiers by functions is Skolemization.
The formula can be written in clausal form by dropping the (universal) quantifiers and writing the matrix as sets of clauses
1. 该公式可以写成子句形式，即去掉（通用）量词，将矩阵写成子句的集合

注意最后一步大括号以及逗号分别取代的二元符号
- clause: {L,L,L}代表的是or
- set of clauses:{C,C,C}代表的是and
同时注意有一步是rename

example

2.3. Skolemised form 斯科伦范式

如果一阶逻辑式的前束范式只有全称量词，则称其为是符合Skolem 范式的

2.4. Properties of CNFs and clausal forms

For F be any formula and suppose $F⇒^{∗}_{CNF} F^{‘}$
- Then $F ≡ F^{‘}$

2.5. 为什么需要斯科伦范式

3. Herbrand Models 埃尔布朗模型

When function symbols are used to form terms, there is no easy way to describe the set of possible interpretations. The domain could be a numerical domain or a domain of data structures or almost anything else. The definition of even one function can choose to assign an arbitrary element of the domain to an arbitrary subset of arguments.

Herbrand models, which are a relatively limited set of interpretations that have the following property: If a set of clauses has a model then it has an Herbrand model.

a formula is satisfiable if and only if its clausal form is satisfiable and A set of clauses S has a model iff it has an Herbrand model.
- 反之亦然

3.1. Herbrand Universes (for domain)

Let $Σ = (\mathcal{F}, P)$ denote the signature标识 of a clause set N
- $\mathcal{F}$：ground terms
- $P$: predicate
The Herbrand universe is $T_Σ$, i.e., the set of all ground terms over Σ
- Suppose N = {P(a), ¬P(x) ∨ P(f (x, b))}
- Then F consists of one binary function symbol f and two constants a and b Herbrand universe over Σ:
  - $T_Σ = {a, b, f (a, a), f (a, b), f (b, a), f (b, b), f (a, f (a, a)), . . .}$
If Σ contains non-constant function symbols then TΣ is infinite
Important assumption: There is at least one constant in the signature Σ
- - If there are no constant symbols or 0-ary function symbols in S, initialize the inductive definition of $H_S$ with an arbitrary constant symbol a.
- Suppose N = {P(x), ¬P(x) ∨ P(f (x, y))}. Then include a (fresh) in Σ
  - $T_Σ = {a, f (a, a), f (a, f (a, a)), f (f (a, a), f (a, a)), . . .}$
The Herbrand universe is just the set of ground terms（aka no variables）that can be formed from symbols in S. Obviously, if S contains a function symbol, the Herbrand universe is infinite since $f(f(…(a)…))∈H_S$

3.2. Herbrand Interpretations

A Herbrand interpretation, denoted $I$, is a set of ground atoms (理解为ground atomic formula) over $Σ$

$I = {A_1, . . . , A_n, . . .}$
Note: $I \models A$ iff $A ∈ I$
- is equivalent to $I \not\models A$ iff $A \notin{} I$
- 很神奇也很废话，只要解集中包括了这个解，就为真

注意此处将对某一公式的解的验证转化为对该公式的Herbrand解的验证
Truth in I of any set N of clauses/quantifier-free formulae:

example

only positive literals can belong to $I$
对于最后一个例子，herbrand universe == domain？✔

3.3. all ground instances

Let N be a set of Σ-clauses. Then

N is true in a standard interpretation
- iff N has a Herbrand model (over Σ)
- iff $G_Σ(N)$ has a Herbrand model (over Σ)
We use it for model construction required for the completeness proof of the resolution system
- 我们用它来构建归结系统的完整性证明所需的解释

3.4. Herbrand’s theorem

3.4.1. Using Herbrand’s theorem to find a model

也就是说，将原命题的sat问题，转化为 $I \models G_Σ(N)$ 问题
- 先将原公式formula转化为CNF形式
- 从CNF提取标识signature $Σ$
- 求 $T_Σ$ , $G_Σ(N)$ 和 $I$
  - $I$: apply Predicate(s) to $T_Σ$
- 查看是否 $G_Σ(N) \in I$

3.4.2. Verification

ground clauses == ground instance
可以理解为一种巧证

4. Formulas in number theory, informal meaning in $N$

Even：偶数

5. Translating English into first-order logic formulas

forall: $\rightarrow$
‘For every human . . . ’ for $∀x$ you can write ‘Everyone . . . ’, which is more natural

不能写成$\lnot P \land O \land C$，只能写成implication的形式
- 因为不能not + function?

6. Substitution 替换

一个function
$σ : X → T_{Σ}(X)$
such that the set $Dom(σ) =^{def}{x ∈ X | σ(x) \neq{x}}$ is finite
- Dom(σ) is the domain of σ
- $Cod(σ) =^{def} {σ(x) | x ∈ Dom(σ)}$ is the codomain of σ

Example

F = P(g(x), y, x)
F{x/a, y/f (z)} = P(g(a), f (z), a)

一般式

6.1. Modification of a substitution

6.2. Restriction

only for a free variable
The captured variable must be renamed into a “fresh” variable, say x’, F{y/x} = ∃x’(x’ > x)
1. 也就是不能用x换y，导致歧义

6.3. substitution instance

instance就是由substitution所产生的

We say that a formula φ is an instance of a formula ψ if there exists a substitution σ for the free variables in ψ such that ψσ is a renamed variant of φ
We say Eσ (or σ(E)) is formed by applying σ to E, where E is an expression (a term or formula)

Example σ = {x/a, y/b}
- P(g(x), y, x)σ = P(g(x)σ, yσ, xσ) = P(g(xσ), yσ, xσ) = P(g(a), b, a)

6.4. identity substitution 一致性替换

The identity substitution, which maps every variable to itself, is the neutral element of substitution composition

6.5. Codomain 到达域

到达域（英语：Codomain），或称为陪域、余定义域、上域、终域、共变域、目标集
一个函数的到达域指的是至少包含所有此函数的输出值的一个集合。在函数符号 ${\displaystyle f\colon X\rightarrow Y}$ 中， ${\displaystyle Y}$ 是函数 ${\displaystyle f}$ 的到达域
不是值域
- ${\displaystyle f}$ 的值域是 ${\displaystyle Y}$ 的一个子集，若 ${\displaystyle f}$ 是一个满射函数，则 ${\displaystyle f}$ 的到达域和值域相等