Mathematical logic (4) First order logic 一阶逻辑

1. Basic 基础组成

1.1 Domain 论域

The set of objects to be discussed is called Domain.

1.2 Constants 常元

The symbol to describe a concrete objects in domain is called constant.

e.g. Alice, Bob, $0$, $1$, $\dots$

1.3 Variables 变元

A symbol to represent an uncertain objects in domain is called variable.

e.g. $x,y,z,w,\dots$

1.4 Predicates 谓词

Predicates are symbols represents a property of an individual object or a relationship amon multiple individuals.

e.g. $S(x)$ : $x$ is a student; $R(x, y)$ : $x <br y$.

The arity of predicates is the number of its arguments(参数)：e.g. $Q^3$ can receive three arguments written as $Q(x, y, z)$.

1.5 Quantifiers 量词

1. Universal Quantifier $\forall$ : The value for variable ranges throughout the domain.

2. Existential Quantifier $\exists$ : The value for variable is limited to some objects in domain.

1.6 Functions 函词

A symbol represents the mapping from a set of individuals to an individual is called Function.

Like predicates, function has arity represents the numbers of input objects.

e.g. $m(x, y)$ : the product of $x$ and $y$.

2. Syntax 语义

2.1 Alphabet

Non-logical symbols :

1. Constant symbols: $c_1,c_2,\dots$
2. Predicates: $P,Q,P^2_1,\dots$
3. Functions: $f,g,h,f^1_2,g^2_1,\dots$

Logical symols :

1. Quantifiers: $\forall,\exists$
2. Variables: $x,y,z,x_1,,x_2,\dots,y_1,\dots$
3. Connectives: $\neg, \land, \lor, \to, \leftrightarrow$
4. Punctuations: $(,)$ and ,
5. Equality: $=$

2.2 Terms 项

• Constant symbols and variables are (atomic) terms.
• If $f^{(n)}$ is a function and $t_1,t_2,\dots,t_n \in Term(\mathscr{L})$, then $f^{(n)}(t_1,t_2,\dots,t_n) \in Term(\mathscr{L})$

2.3 Atom 原子公式

• $P(t_1,t_2,\dots,t_n) \in Atom(\mathscr{L})$ if $t_1,t_2,\dots,t_n \in Term(\mathscr{L})$ and $P$ is an $n$-ary predicate.
• $=(t_1,t_2)$ (or, $t_1=t_2$) $\in Atom(\mathscr{L})$ where $t_1,t_2 \in Term(\mathscr{L})$

2.4 Formulas 公式

$\alpha \in Form(\mathscr{L})$ if and only if :

1. $Atom(\mathscr{L}) \in Form(\mathscr{L})$.
2. If $\alpha \in Form(\mathscr{L})$, then $(\neg \alpha) \in Form(\mathscr{L})$.
3. If $\alpha, \beta \in Form(\mathscr{L})$, then $(\alpha*\beta) \in Form(\mathscr{L})$, where $*$ is one of $\land, \lor, \to, \leftrightarrow$.
4. If $\alpha \in Form(\mathscr{L})$ and $x$ is a variable, then $(\forall x \alpha), (\exists x \alpha) \in Form(\mathscr{L})$.

2.4.1 Precedence 优先顺序

• $\forall x, \exists x$ have the same precedence as $\neg$.
• The rest remains as in proposition logic.

2.4.2 Conventions

• Parenthese around quantifiers can be omitted.
• The order of priority in which to consider $\neg, \exists, \forall$ is determined by the order in which they are listed.

2.5 Formalization 形式化

3. Semantics 语义

3.1 Basic

3.1.1 Scope 辖域

Formula $\alpha$ is the scope of the quatifier $\forall x(\exists x)$ if $\forall x(\exists x)$ is adjacent to $\alpha$, and any proper prefix of $\alpha$ is not a formula.

e.g. $\forall x P(x)\land Q(x)$, $P(x)$ is the scope of $\forall x$.

3.1.2 Free and Bound Variables 自由变元和约束变元

• Free Variable : the variable is not within the scope of the relative quantifier.
• Bound Variable : the variable is within the scope of the relative quantifier.

3.1.3 Sentence 语句

A formula with no free variables is called closed formula, or a sentence.

e.g.

• $\forall y \exists x f(x) = y$ is a sentence.

Closure(封闭式) :

If $\{x_1,x_2,\dots,x_n\}$ are all the free variables of a formula $\alpha$, then

• Universal closure: $\forall x_1 \dots \forall x_n \alpha$
• Existential closure: $\exists x_1 \dots \exists x_n \alpha$

3.2 Interpretation 解释

An interpretation $\mathcal{I}$ consists of :

• A non-empty domain $D$ of $\mathcal{I}$.
• Constant symbol $c^\mathcal{I}$ in $D$.
• Function symbol $f^\mathcal{I}$.
• Predicate symbol $P^\mathcal{I}$.

e.g. Define an interpretation $\mathcal{I}$ by

• Domain: $D = \{1, 2 ,3\}$
• Constant: $\alpha^\mathcal{I} = 1, b^\mathcal{I} = 2, c^\mathcal{I} = 3$
• Function: $f^\mathcal{I}:(x, y) \mapsto min\{x, y\}$
• Predicates: $P^\mathcal{I} = \{1, 3\}, Q^\mathcal{I} = \{\langle1,2\rangle,\langle3,3\rangle,\langle3,1\rangle\}$

3.3 Environment 环境

An environment $E$ is a function that assigns a value in the domain to every symbol in the language.

The combination of interpretation and environment supplies a value for every formulas in FOL.

3.4 Truth Value of Formulas

3.4.1 Valuation for Terms

• If term $t$ is a constant $c$, then $t^{(\mathcal{I},E)} = c^{\mathcal{I}}$.

• If term $t$ is a free variable $x$, then $t^{(\mathcal{I},E)}= x^E$.

• If term $t$ is a function $f(t_1,t_2,\dots,t_n)$, then $t^{(\mathcal{I},E)} = f^\mathcal{I}(t_1^{(\mathcal{I},E)},t_2^{(\mathcal{I},E)},\dots,t_n^{(\mathcal{I},E)})$.

3.4.2 Valution for Well-Formed Formulas

3.4.3 Defination 定义

For any environment $E$ and domain element $d$, the new environment $E$ with $x$ re-assigned to $d$, denoted $E[x \mapsto d]$, is given by:

$$E[x \mapsto d](y) = \left\{ \begin{aligned} &d &&\text{if } y \text{ is } x \\ &E(y) &&\text{if } y \text{ is not } x\\ \end{aligned} \right.$$

3.4.4 Valuation for Quantified Formulas

$$(\forall x \ \alpha)^{(\mathcal{I},E)} = \left\{ \begin{aligned} &1 &&\text{if } \alpha^{(\mathcal{I},E[x \mapsto d])} = 1\text{ for every } d \in dom(\mathcal{I}) \\ &0 &&\text{otherwise} \end{aligned} \right.$$

$$(\exists x \ \alpha)^{(\mathcal{I},E)} = \left\{ \begin{aligned} &1 &&\text{if } \alpha^{(\mathcal{I},E[x \mapsto d])} = 1\text{ for some } d \in dom(\mathcal{I}) \\ &0 &&\text{otherwise} \end{aligned} \right.$$

4. Entailment 蕴涵

4.1 Satisfaction and Validity 可满足性和永真性

An interpretation $\mathcal{I}$ and environment $E$ satisfy a formula $\alpha$, denoted $\mathcal{I} \models_E \alpha$, iff $\alpha^{(\mathcal{I},E)}=1$.

Otherwise, they don’t satisfy $\alpha$, denoted $\mathcal{I} \not\models_E \alpha$ if $\alpha^{(\mathcal{I},E)}=0$.

Typically, if $\mathcal{I} \models_E \alpha$ for every $E$, then $I$ satisfy $\alpha$, denoted $\mathcal{I} \models \alpha$.

For a formula $\alpha$:

• Valid: if $\mathcal{I} \models_E \alpha$ for every $\mathcal{I}$ and $E$ (like tautology in proposition logic).
• Satisfiable: if $\mathcal{I} \models_E \alpha$ for some $\mathcal{I}$ and $E$.
• Unsatisfiable: if $\mathcal{I} \not\models_E \alpha$ for every $\mathcal{I}$ and $E$.

4.2 Semantic Entailment 语意蕴涵

$\Sigma$ is a set of FOL formulas and $\alpha$ is a formula, we say $\Sigma \models \alpha$ if and only if, for any $\mathcal{I}$ and $E$, if $\mathcal{I} \models_E \Sigma$ then $\mathcal{I} \models_E \alpha$.

$\emptyset \models \alpha$ means $\alpha$ is valid.

4.2.1 Prove Entailment 蕴含证明

e.g. Prove that

$$\forall x (\neg y) \models \neg (\exists x \ y)$$

Proof:

Assume $\mathcal{I} \models_E \forall x (\neg y)$, then we obtain

$$\begin{aligned} &\text{For every } a \in dom(\mathcal{I}), \mathcal{I} \models_{E[x \mapsto a]} (\neg y) \\ \equiv \ &\text{For every } a \in dom(\mathcal{I}), \mathcal{I} \not\models_{E[x \mapsto a]} \ y \end {aligned}$$

by the entailment rules of negation, this means if $\mathcal{I} \models_E (\exists x \ y)$, there will raise a contradiction for no $a \in dom(\mathcal{I}) \text{ such that } \mathcal{I} \models_{E[x \mapsto a]} \ y$.

Hence, $\mathcal{I} \models_E \neg(\exists x \ y)$ holds. Q.E.D.

$$$$

5. Natural Dedution 自然演绎

5.1 Substitution 代换

For a variable $x$, a term $t$ and a formula $\alpha$, $\alpha[t/x]$ denotes the resulting formula by replacing each free occurence of $x$ in $\alpha$ with $t$.

e.g. $(\forall x P(x)\land P(y))[u/x] \iff P(u) \land P(y)$

5.2 Inference Rules

Name	$\vdash$-notation	inference notation
$\forall$-elimination	If $\Sigma \vdash_{ND}(\forall x \ \alpha)$, then $\Sigma \vdash_{ND}\alpha[t/x]$	$\dfrac{(\forall \ \alpha)}{\alpha[t/x]}$
$\forall$-introduction	If $\Sigma \vdash_{ND} \alpha[u/x]$ and $u$ is not free in $\Sigma,\alpha$, then $\Sigma \vdash_{ND} \forall \alpha$	$\dfrac{\boxed{\begin{aligned}&u \ \text{fresh} \\ & \quad \ \vdots \\ &\alpha[u/x]\end{aligned}}}{\forall x \ \alpha}$
$\exists$-elimination	If $\Sigma,\alpha[u/x]\vdash_{ND}\beta$ with $u$ fresh, then $\Sigma, (\exists x \ \alpha)\vdash_{ND}\beta$	$\dfrac{(\exists x \ \alpha) \quad \boxed{\begin{aligned}&\alpha[u/x], u \ \text{fresh} \\ & \quad \quad \ \ \ \vdots \\ &\quad \quad \ \ \beta\end{aligned}}}{\beta}$
$\exists$-introdution	If $\Sigma\vdash_{ND}\alpha[t/x]$, then $\Sigma \vdash_{ND} (\exists x \ \alpha)$	$\dfrac{\alpha[t/x]}{(\exists x \ \alpha)}$

e.g.

$$\text{i}. \quad \exists x (\neg P(x)) \vdash \neg (\forall x P(x))$$

Proof :

$$\begin{aligned} &1. \quad \exists x (\neg P(x)) \quad \quad \text{Premise} \\ &\boxed{ \begin{aligned} &2. \quad \forall x P(x) \quad \quad \quad \text{Assumption} \\ &\boxed{ \begin{aligned} &3. \quad \neg P(u), \ u \ \text{fresh} \\ &4. \quad P(u) \quad \quad \quad \quad \forall_e: 2 \\ &5. \quad \perp \quad \quad \quad \quad \quad \perp_i: 3, 4 \\ \end{aligned} }\\ &6. \quad \perp \quad \quad \quad \quad \quad \exists_e: 1, 3-5 \\ \end{aligned} }\\ &7. \quad \neg (\forall x P(x)) \quad \quad \neg_i: 2-6 \\ \\ \\ \end{aligned}$$

$$\text{ii}. \quad \neg (\forall P(x)) \vdash \exists x(\neg P(x))$$

Proof :

$$\begin{aligned} &1. \quad \neg (\forall x P(x)) \quad \quad \text{Premise} \\ &\boxed{ \begin{aligned} &2. \quad \neg \exists x(\neg P(x)) \quad \ \text{Assumption} \\ &\boxed{ \begin{aligned} &3. \quad u \ \ \text{fresh} \\ &\boxed{ \begin{aligned} &4. \quad \neg P(u) \quad \quad \quad \ \text{Assumption} \\ &5. \quad \exists \neg P(x) \quad \quad \ \ \ \exists_i: 4 \\ &6. \quad \perp \quad \quad \quad \quad \quad \perp_i: 2, 5 \\ \end{aligned} }\\ &7. \quad P(u) \quad \quad \quad \quad \ \text{Reductio ad Absurbum: 4-6} \\ \end{aligned} }\\ &8. \quad \forall x P(x) \quad \quad \quad \ \ \forall_i: 3-7 \\ &9. \quad \perp \quad \quad \quad \quad \quad\ \ \perp_i: 1, 8 \\ \end{aligned} }\\ &10. \quad \exists x \neg P(x) \quad \quad \ \ \text{Reductio ad Absurbum: 2-9} \\ \end{aligned}$$