命题逻辑中,只能可以表示这样的命题链接词:“非”,“与”,“或”,“如果…那么”。但是如果要表达“所有”,“全部”,“存在”,“只有”的概念,就需要或者命题逻辑。这篇文章将会介绍谓词逻辑 (predicate logic),或者称作一阶逻辑 (first-order logic)。谓词用来表示事物的性质,以及事物之间的关系,事物可以是确定的具体的客体,比如“小明”,比如“小明的桌子”,也可以是抽象的不确定的变体,比如“一个人”,“一张桌子”,因为是变体,我们不知道具体指的是哪个人哪张桌子。变体一般有一个取值范围,称作域domain,比如“在这个房间里的桌子”,域就被限制在“这个房间”。

谓词的组成部分

全称量词,存在量词,谓词

例子:所有的学生都比讲师年轻。
这个句子中须有构造以下的谓词:

  • S(x)S(x): xx是一个学生;
  • I(x)I(x): xx是一个讲师;
  • Y(x,y)Y(x,y): xxyy年轻。

其中,xxyy为谓词的参数,可替代成实际的对象。

加入两个量词:

  • 全称量词 universal quantifier x\forall x:对于所有的xx
  • 存在量词 existential quantifier x\exists x: 存在一个xx

例子:存在某个讲师,所有的学生都比他年轻:
x(S(x)(y(I(y)Y(x,y))))\forall x(S(x) \rightarrow (\exists y (I(y) \land Y(x,y))))

x.S(x)\forall x. S(x)中,xx 被所有可能的值取代,然后检查相应的值。

设 A 为一个谓词公式,(∀x)P(x)或(∃x)P(x)为公式 A 的子公式,此时紧跟在∀、∃之后的 x 称为量词的指导变项作用变项,P(x)称为相应量词的作用域或辖域(scope),即为量词所约束的范围。在辖域中 x 的一切出现均称为约束出现,受指导变项所约束。所有约束出现的变项称为约束变项(bounded variable);在 A 中除了约束变项外出现的变项均称为自由变项(free variable),不受指导变项的约束。

函数符号 function symbol

除了比命题逻辑多量词以为,谓词逻辑还有函数符号 function symbols。比如:
所有的小孩都是比他的目前年轻。
xy(C(x)M(y,x)Y(x,y)\forall x \forall y (C(x) \land M(y,x) \rightarrow Y(x,y)
其中:C(x)C(x) 表示xx是个小孩,$M(x,y) 表示y是x的妈妈,Y(x,y)表示x$ 比yy年轻。
由于每个人只有一个亲生的妈妈,所以可以直接用function symbol来表示某个人的妈妈,比如m(x)m(x)表示xx的妈妈。上面的例子,就可以用如下公式表达:
xy(C(x)Y(x,m(x)))\forall x \forall y (C(x) \rightarrow Y(x,m(x)))

项 terms

The terms of our language are made up of variables, constant symbols and functions applied to those. Functions may be nested, as in m(m(x))m(m(x)) or g(m(a),c)g(m(a), c): the grade obtained by Andy’s mother in the course cc.

Definition Terms are defined as follows.

  • Any variable is a term.
  • If cFc\in F is a nullary function, then cc is a term.
  • If t1,t2,...,tnt_1,t_2,...,t_n are terms and $f \in F $ has arity n>0n > 0, then f(t1,t2,...,tn)f(t_1,t_2,...,t_n) is a term.
  • Nothing else is a term.

In Backus Naur form we may write
$$t::=x\ |\ c\ |\ f(t,…,t)$$

formulas

The choice of sets P (denotes the set of predicates) and F (the set of function symbol) for predicate and function symbols, respectively, is driven by what we intend to describe.

For example, if we work on a database representing relations between our kin we might want to consider P = {M, F, S, D}, referring to being male, being female, being a son of . . . and being a daughter of . . . . Naturally, F and M are unary predicates (they take one argument) whereas D and S are binary (taking two). Similarly, we may define F = {mother-of,father-of}.

Definition We define the set of formulas over (F,P) inductively, using the already defined set of terms over F:

  • If p ∈ P is a predicate symbol of arity n ≥ 1, and if t1,t2,...,tnt1,t2,...,tn are terms over FF, then p(t1,t2,...,tn)p(t1,t2,...,tn) is a formula.
  • If is a formula, then so is (¬φ).
  • If φ and ψ are formulas, then so are (φ∧ψ), (φ∨ψ) and (φ→ψ).
  • If φ is a formula and x is a variable, then (∀x φ) and (∃x φ) are formulas.
  • Nothing else is a formula.

Note how the arguments given to predicates are always terms. This can also be seen in the Backus Naur form (BNF) for predicate logic:

\phi ::= P (t1, t2, . . . , tn)\ |\ (\neg\phi)\ |\ (\phi ∧ \phi)\ |\ (\phi ∨ \phi)\ |\ (\phi → \phi) \\ |\ (\forall x \phi)\ |\ (\exists x \phi)

谓词的语义

models

回想一下我们如何评估命题逻辑中的公式。 例如,公式(p∨¬q)→(q→p)通过计算一个真值(T或F),根据给定的估值(p和q的假设值)来计算。 这个活动本质上是在真值表中找一行对应的。对于谓词逻辑的公式,比如如下公式,怎样定义每个项的值呢?
∀x ∃y ((P (x) ∨ ¬Q(y)) → (Q(x) → P (y)))

我们可以直接定义P(x)或者Q(y)的值吗?这显示不太可行,因为x和y都是一个变量。如果是∀x ,我们需要对所有x的值都做判断,假设x为一个班上的学生,因此对于每个具体的学生,P(x)都有一个值。因此,前提是x的范围是固定的,我们可以定义一个赋值表,像命题逻辑一样。对于谓词P(t1,t2,…,tn),有n个参数,假设每个参数都有m种可能,因此,整个赋值表就有mnm^n种情况。

定义: Let FF be a set of function symbols and PP a set of predicate symbols, each symbol with a fixed number of required arguments. A model MM of the pair (F,P)(F,P) consists of the following set of data:

    1. A non-empty set AA, the universe of concrete values;
  1. for each nullary function symbol fFf \in F, a concrete element fMAf^M \in A
  2. for each fFf\in F with arity n>0n>0, a concrete function f^M:A^n→A from AnA^n, the set of n-tuples over AA, to AA; and
  3. for each p∈P with arity n>0,a subset p^M⊆ A^n of n-tuples over AA.

The distinction between ff and fMf^M and between PP and PMP^M is most important. The symbols ff and PP are just that: symbols, whereas fMf^M and PMP^M denote a concrete function (or element) and relation in a model MM, respectively.

environment

A look-up table or environment for a universe AA of concrete values is a function l : var → A from the set of variables var to AA. For such an ll, we denote by l[x → a] the look-up table which maps xx to a and any other variable yy to l(y)l(y).

定义: Given a model MM for a pair (F,P)(F,P) and given an environment ll, we define the satisfaction relation M \models_l φ for each logical formula φ over the pair (F,P)(F,P) and look-up table ll by structural induction on φ. If M \models_l φ holds, we say that φ computes to TT in the model MM with respect to the environment ll.

  • PP: If φ is of the form P(t1,t2,...,tn)P(t1,t2,...,tn), then we interpret the terms t1,t2,...,tnt1,t2,...,tn in our set AA by replacing all variables with their values according to ll. In this way we compute concrete values a1,a2,...,ana1,a2,...,an of AA for each of these terms, where we interpret any function symbol f ∈ F by fMf^M. Now MlP(t1,t2,...,tn)M \models_l P(t1,t2,...,tn) holds iff (a1,a2,...,an)(a1,a2,...,an) is in the set pMp^M .
  • ∀x: The relation M\models_l ∀x ψ holds iff M\models_l[x →a] ψ holds for all a ∈ A.
  • ∃x: Dually, M \models_l ∃x ψ holds iff M \models_l[x →a] ψ holds for some a ∈ A.
  • ¬: The relation M \models_l ¬ψ holds iff it is not the case that M \models_l ψ holds.
  • ∨: The relation M \models_l ψ1 ∨ψ2 holds iff M \models_l ψ1 or M \models_l ψ2 holds.
  • ∧: The relation M \models_l ψ1 ∧ψ2 holds iff M \models_l ψ1 and M \models_l ψ2 hold.
  • →: The relation M \models_l ψ1 → ψ2 holds iff M \models_l ψ2 holds whenever M \models_l ψ1 holds.

例子:Let F = {alma} and P = {loves} where alma is a constant and loves a predicate with two arguments. The model MM we choose here consists of the privacy-respecting

  • set A=a,b,cA = {a, b, c},
  • the constant function almaM=aalma^M = a and
  • the predicate loves={(a,a),(b,a),(c,a)}loves = \{(a, a), (b, a), (c, a)\}, which has two arguments as required.

We want to check whether the model MM satisfies:

  • None of Alma’s lovers’ lovers love her.
  • $∀x ∀y (loves(x, alma) ∧ loves(y, x) → ¬loves(y, alma)) $

Does the model MM satisfy this formula? Well, it does not; for we may choose aa for xx and bb for yy. Since (a,a)(a,a) is in the set lovesMloves^M and (b,a)(b,a) is in the set lovesMloves^M, we would need that the latter does not hold since it is the interpretation of loves(y,alma)loves(y, alma); this cannot be.

And what changes if we modify MM to M′, where we keep AA and almaMalma^M, M′ but redefine the interpretation of loves as loves={(b,a),(c,b)}loves = \{ (b, a), (c, b)\}? Well, now there is exactly one lover of Alma’s lovers, namely cc; but cc is not one of Alma’s lovers. Thus, the formula holds in the model M′.

semantic entailment

In propositional logic, the semantic entailment φ1, φ2, . . . , φn \models ψ holds iff: whenever all φ1, φ2, . . . , φn evaluate to T, the formula ψ evaluates to T as well. How can we define such a notion for formulas in predicate logic, considering that M \models_l φ is indexed with an environment?

Let Γ be a (possibly infinite) set of formulas in predicate logic and ψ a formula of predicate logic.

  1. Semantic entailment Γ \models ψ holds iff for all models MM and look-up tables ll, whenever $M \models_l φ $ holds forall φ∈Γ, then M \models_l ψ holds as well.
  2. Formula ψ is satisfiable iff there is some model MM and some environment ll such that M \models_l ψ holds.
  3. Formula ψ is valid iff M \models_l ψ holds for all models MM and environments ll in which we can check ψ.
  4. The set Γ is consistent or satisfiable iff there is a model MM and a look-up table l such that M \models_l φ holds for all φ∈Γ.

In predicate logic, the symbol is overloaded: it denotes model checks ‘M \models φ’ and semantic entailment ‘φ1,φ2,...,φn \models ψ.’ Computationally, each of these notions means trouble. First, establishing M \models φ will cause problems, if done on a machine, as soon as the universe of values AA of MM is infinite. In that case, checking the sentence ∀xψ, where x is free in ψ, amounts to verifying M\models_{[x →a]} ψ for infinitely many elements a.

Second, and much more seriously, in trying to verify that φ1, φ2, . . . , φn \models ψ holds, we have to check things out for all possible models, all models which are equipped with the right structure (i.e. they have functions and predicates with the matching number of arguments). This task is impossible to perform mechanically. This should be contrasted to the situation in propositional logic, where the computation of the truth tables for the propositions involved was the basis for computing this relationship successfully.

Undecidability of predicate logic

Given a formula φ in propositional logic we can, at least in principle, determine whether $ \models φ$ holds: if φ has nn propositional atoms, then the truth table of φ contains 2n2^n lines; and $ \models φ$ holds if, and only if, the column for φ (of length 2n2^n) contains only T entries.

Validity in predicate logic: Given a logical formula φ in predicate logic, does $ \models φ$ hold, yes or no?

We prove this by a well-known technique called problem reduction. The problem that is known not to be solvable, the Post correspondence problem, is interesting in its own right and, upon first reflection, does not seem to have a lot to do with predicate logic.

The Post correspondence problem. Given a finite sequence of pairs (s1,t1),(s2,t2),...,(sk,tk)(s1,t1),(s2,t2),...,(sk,tk) such that all sisi and titi are binary strings of positive length, is there a sequence of indices i1,i2,...,ini1, i2, . . . , in with n ≥ 1 such that the concatenation of strings si1si2...sinsi1 si2 . . . sin equals ti1ti2...tinti1 ti2 . . . tin ?

Theorem The decision problem of validity in predicate logic is undecidable: no program exists which, given any φ, decides whether \models φ.

Summary


A first-order theory T is characterized by its signature Σ and a set of axioms.

The signature Σ is a set of constant, function, and predicate symbols; the function and predicate symbols have fixed arity. A Σ-formula is a first-order formula whose constant, function, and predicate symbols all appear in Σ.

A term is a variable, constant symbol, or application of a function to a set of terms.

An atom is the application of a predicate symbol to a set of terms.

A literal is an atom or its negation. The axioms of T are a (countable) set of Σ-formulae.

A T -interpretation I : ⟨D, α⟩ is a structure consisting of a domain D and an assignment α that assigns meaning to the symbols of Σ: α assigns each constant symbol c a value α_I [c] ∈ D; each n-ary function symbol ff a function α_I[f] : D^n → D; and each n-ary predicate symbol p a predicate α_I[p] : D^n → B. Moreover, each axiom of T evaluates to true on II according to first-order semantics; in other words, II satisfies each axiom.

One of the main questions about a Σ-formula F is whether it is T-satisfiable: Does there exist a T -interpretation that satisfies F ? A decision procedure for a theory is an algorithm that decides whether a given Σ-formula is T -satisfiable.