FOL(2) - semantics

 

In contrast with PL, in FOL, the concept of T/F differs by structures. by stucture, I mean we have some rules translating formal language into given language.

 

we define structure a function $\mathfrak{A}=<|\mathfrak{A}|;P,f,c>$ whose domain is parameters satisfying below.

 

1.  $\mathfrak{A}$ assigns to $\forall$ the universe of $\mathfrak{A}$, $|\mathfrak{A}|$ which is nonempty set.

 

2. $\mathfrak{A}$ assigns to every $P$ of $n$-place predicate symbol a relation $P^{\mathfrak{A}} \subseteq |\mathfrak{A}|^n$ where $P^{\mathfrak{A}}$ a set of n-tuples given by some interpretation.

 

3. $\mathfrak{A}$ assigns to each $n$-place function symbol $f$ a function $f^{\mathfrak{A}} : |\mathfrak{A}|^n \rightarrow |\mathfrak{A}|$.

 

4. $\mathfrak{A}$ assigns to each constant symbol c $c^{\mathfrak{A}} \in \mathfrak{A}$.

 

 

intuitionistic idea of structure is giving meaning to parameters(function, predicate, constant symbol). if we are given some structure, then $\forall$ means everything in $|\mathfrak{A}|$, $P$ $P^{\mathfrak{A}}$, $f$ $f^{\mathfrak{A}}$, and $c$ $c^{\mathfrak{A}}$.

 

 

now define concept of truth. be careful that in FOL, 'truth' is defined in some structures. truth concept without structure is not defined in FOL(but defined in PL). thus we must define 'sentence $\sigma$ is true in structure

$\mathfrak{A}$'. we symbolize this as '$\models_{\mathfrak{A}} \sigma$'. before defining this, we have to give some boring concepts about wffs.

 

$\models_{\mathfrak{A}}\sigma$
 

let $\varphi$ be a wff of the given language, and $\mathfrak{A}$ a given structure. we'll define '$\mathfrak{A}$ satisfies $\varphi$ with $s$' symbolized as $\models_{\mathfrak{A}} \varphi[s]$.

 

define $s : V \rightarrow |\mathfrak{A}|$ where $V$ is a set of variables, and $|\mathfrak{A}|$ the universe of our structure. and extend $s$ to $\bar{s}$ where $$\bar{s} : T \rightarrow |\mathfrak{A}|$$ where $T$ is a set of terms satisfying below.

 

1. if $x \in V$, $\bar{s}(x)=s(x)$

2. for each constant symbol $c$, $\bar{s}(c)=c^{\mathfrak{A}}$.

3. if $t_1,t_2,\ldots, t_n$ are terms and $f$ is a function symbol, then $\bar{s}(ft_1\ldots t_n)=f^{\mathfrak{A}}(\bar{s}(t_1),\ldots, \bar{s}(t_n))$.

 

now define satisfaction as below.

 

1. $\models_{\mathfrak{A}}=t_1t_2[s]$ iff $\bar{s}(t_1)=\bar{s}(t_2)$

2. for a $n$-place predicate symbol P, $\models_{\mathfrak{A}} Pt_1\ldots t_n[s]$ iff $<\bar{s}(t_1), \ldots, \bar{s}(t_n)> \in P^{\mathfrak{A}}$.

 

1-2 is about atomic formulas.

 

3. $\models_{\mathfrak{A}} \neg \varphi[s]$ iff $\not\models_{\mathfrak{A}} \varphi[s]$

4. $\models_{\mathfrak{A}} (\varphi \rightarrow \psi)[s]$ iff $\not\models_{\mathfrak{A}} \varphi[s]$ or $\models_{\mathfrak{A}} \psi[s]$

5. $\models_{\mathfrak{A}} \forall \varphi$ iff for every $d \in |\mathfrak{A}|$, $\models_{\mathfrak{A}} \varphi[s(x|d)]$ where $s(x|d)$ is exactly same with $s$ except at $x$. at $x$, $s(x|d)(x)=d$. which is expressed as $$s(x|d)(y) = s(y)\quad\text{if y $\neq$ x}, \text{or}\quad d \quad\text{if y=x}$$

 

 

Lemma for sentence satisfaction : assume that $s_1$ and $s_2$ are functions from $V$ into $|\mathfrak{A}|$ which agree at all variables (if any) that occur free in the wff $\varphi$. Then $\models_{\mathfrak{A}} \varphi[s_1]$ iff $\models_{\mathfrak{A}} \varphi[s_2]$.

 

proof : use induction on formulas type 2-5(especially, at atomic formula, use strong induction for terms for all $i<k$).

 

theorem : for a sentence $\sigma$, one of (a), (b) holds.

 

(a) $\mathfrak{A}$ satisfies $\psi$ for every $s$, or
(b) there does not exist $s$ where $\sigma$ is satisfied in $\mathfrak{A}$.

 

if (a) holds, we say $\sigma$ is true in $\mathfrak{A}$, and $\mathfrak{A}$ is a model of $\sigma$. otherwise, $\sigma$ is false in $\mathfrak{A}$. each is symbolized as $\models_{\mathfrak{A}} \sigma$ and $\not\models_{\mathfrak{A}} \sigma$

 

satisfaction of abbrevated some formulas.

 

1. $\models_{\mathfrak{A}} (\alpha \wedge \beta)[s]$ iff $\models_{\mathfrak{A}} \alpha[s]$ and $\models_{\mathfrak{A}} \beta[s]$

 

2. $\models_{\mathfrak{A}} (\alpha \vee \beta)[s]$ iff $\models_{\mathfrak{A}} \alpha[s]$ or $\models_{\mathfrak{A}} \beta[s]$

 

3. $\models_{\mathfrak{A}} (\alpha \leftrightarrow \beta)[s]$ iff $\models_{\mathfrak{A}} (\alpha \rightarrow \beta)[s]$ and $\models_{\mathfrak{A}} (\beta \rightarrow \alpha)[s]$

 

4. $\models_{\mathfrak{A}} \exists x \alpha[s]$ iff for some $d \in \mathfrak{A}$, $\models_{\mathfrak{A}} \alpha[s(x|d)]$.

 

 

Logical Implication

 

definition : Let $\Gamma$ be a set of wffs, $\varphi$ a wff. Then $\Gamma$ logically implies $\varphi$, written $\Gamma \models \varphi$ iff for every structure $\mathfrak{A}$ for the language and every function $s : V \rightarrow |\mathfrak{A}|$ such that $\mathfrak{A}$ satisfies every member of $\Gamma$ with $s$, $\mathfrak{A}$ also satisfies $\varphi$ with $s$.

 

simply, $\Gamma \models \varphi$ iff for every $s$ and $\mathfrak{A}$, $\models_{\mathfrak{A}} \Gamma[s] \rightarrow \models_{\mathfrak{A}} \varphi[s]$.

 

 

another deifnitions.

$\psi \models \varphi$ and $\varphi \models \psi$ iff $\psi$ and $\varphi$ are logically equivalent. and $\varphi$ is valid iff $\emptyset \models \varphi$(shortly $\models \varphi$).