## 谓词的组成部分

### 全称量词，存在量词，谓词

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

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

$\forall x(S(x) \rightarrow (\exists y (I(y) \land Y(x,y))))$

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

### 函数符号 function symbol

$\forall x \forall y (C(x) \land M(y,x) \rightarrow Y(x,y)$

$\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))$ or $g(m(a), c)$: the grade obtained by Andy’s mother in the course $c$.

Definition Terms are defined as follows.

• Any variable is a term.
• If $c\in F$ is a nullary function, then $c$ is a term.
• If $t_1,t_2,...,t_n$ are terms and $f \in F$ has arity $n > 0$, then $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,...,tn$ are terms over $F$, then $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

∀x ∃y ((P (x) ∨ ¬Q(y)) → (Q(x) → P (y)))

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

The distinction between $f$ and $f^M$ and between $P$ and $P^M$ is most important. The symbols $f$ and $P$ are just that: symbols, whereas $f^M$ and $P^M$ denote a concrete function (or element) and relation in a model $M$, respectively.

### environment

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

• $P$: If φ is of the form $P(t1,t2,...,tn)$, then we interpret the terms $t1,t2,...,tn$ in our set $A$ by replacing all variables with their values according to $l$. In this way we compute concrete values $a1,a2,...,an$ of $A$ for each of these terms, where we interpret any function symbol f ∈ F by $f^M$. Now $M \models_l P(t1,t2,...,tn)$ holds iff $(a1,a2,...,an)$ is in the set $p^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.

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

We want to check whether the model $M$ satisfies:

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

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

And what changes if we modify $M$ to M′, where we keep $A$ and $alma^M$, M′ but redefine the interpretation of loves as $loves = \{ (b, a), (c, b)\}$? Well, now there is exactly one lover of Alma’s lovers, namely $c$; but $c$ 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 $M$ and look-up tables $l$, whenever $M \models_l φ$ holds forall φ∈Γ, then M \models_l ψ holds as well.
2. Formula ψ is satisfiable iff there is some model $M$ and some environment $l$ such that M \models_l ψ holds.
3. Formula ψ is valid iff M \models_l ψ holds for all models $M$ and environments $l$ in which we can check ψ.
4. The set Γ is consistent or satisfiable iff there is a model $M$ 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 $A$ of $M$ 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 $n$ propositional atoms, then the truth table of φ contains $2^n$ lines; and $\models φ$ holds if, and only if, the column for φ (of length $2^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)$ such that all $si$ and $ti$ are binary strings of positive length, is there a sequence of indices $i1, i2, . . . , in$ with n ≥ 1 such that the concatenation of strings $si1 si2 . . . sin$ equals $ti1 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 $f$ 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 $I$ according to first-order semantics; in other words, $I$ 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.