The Language of FOL
We will now look at a more powerful system of formal logic called first order logic. What makes it more powerful than sentential logic is use of variables whose domain is decided by quantifiers. Since it is a formal system again, we must define the symbols and rules for the language.
Symbols
We have sentential connectives and parenthesis just like we had in sentential logic. Besides these, we need three other symbols which are:
- Variable symbols, $v_i$ as placeholder for elements from a class called domain of discourse or universe $|\mathfrak{A}|$ (we will come to this notation later).
- A quantifier symbol $\forall$ to specify if a variable ranges over $|\mathfrak{A}|$.
- Function symbols $f^\mathfrak{A}:|\mathfrak{A}|^n\mapsto|\mathfrak{A}|$, that takes an $n$-tuple of elements from the universe, and returns an element from the universe. A function symbol with $0$-arity ($n=0$ i.e. $f:\varnothing\mapsto|\mathfrak{A}|$) is called constant symbol.
- Predicates symbols $P^\mathfrak{U}\subseteq|\mathfrak{A}|^n$ are sets of $n$-tuple of elements from the universe.
Grammar for $\mathrm{wff}$
Terms are expressions formed by variables or function symbols applied to terms. They represent objects from the domain of discourse. Atomic formulas are expression formed by applying equality or predicate symbol to terms. Well formed formula for our language is an expression formed by predicates or by logical symbols applied to well formed formula (this logical symbol also contains the quantifier symbol).
All the variables used with a quantifier symbol comes along with a variable. These variable are called bound variables. Variables that are not bound by any quantifier is called free variable. A sentence is $\mathrm{wff}$ with no free variables.
Interpretation in FOL
To interpret FOL, we need a structure that maps all quantifiers, function, and predicate symbols in some ways to domain of discourse. $\forall$ is assigned $|\mathfrak{A}|$ itself, $f^\mathfrak{A}$ some $|\mathfrak{A}|^n\mapsto|\mathfrak{A}|$ and $P^\mathfrak{A}$ some subset of $|\mathfrak{A}|$.
A structure $\mathfrak{A}$ for our FOL is a model for it if it is satisfiable with some function $s:V\mapsto|\mathfrak{A}|$. To see if a structure $\mathfrak{A}$ models a $\mathrm{wff},\varphi$ with $s$ (denoted by $\models_\mathfrak{A}\varphi[s]$), we first need to extend $s$ to $\overline{s}:T\mapsto|\mathfrak{A}|$ where $T$ is the set of all terms. For terms that are variables, $\overline{s}=s$. For terms that composite of function symbols applied to terms, we define $\overline{s}(f^\mathfrak{A}(t_1,\ldots,t_n))=f^\mathfrak{A}(\overline{s}(t_1),\ldots,\overline{s}(t_n))$ . With $\overline{s}$ recursively defined from $s$, we check $\models_\mathfrak{A}\varphi[s]$ for atomic formulas as
- $\models_{\mathfrak{A}}=t_1t_2[s]$ $\mathrm{iff}$ $\overline{s}(t_1)=\overline{s}(t_2)$
- $\models_\mathfrak{A}P(t_1,\ldots,t_n)[s]$ $\mathrm{iff}$ $\langle\overline{s}(t_1),\ldots,\overline{s}(t_n)\rangle\in P^\mathfrak{A}$
With $\models_\mathfrak{A}\varphi[s]$ defined for atomic formulas, we can extends its definitions for other $\mathrm{wff}$ as
- $\models_\mathfrak{A}\neg\varphi[s]$ $\mathrm{iff}$ $\nvDash_\mathfrak{A}\varphi[s]$
- $\models_\mathfrak{A}\varphi\rightarrow\psi$ $\mathrm{iff}$ $\nvDash_\mathfrak{A}\varphi[s]\lor\models_\mathfrak{A}\psi[s]$
- $\models_\mathfrak{A}\forall x\ \psi[x]\longleftrightarrow\forall d\in|\mathfrak{A}|,\models_\mathfrak{A}\varphi[s(x\mid d)]$
where $s(x\mid d)(y)=\begin{cases}s(y)&\text{if }y\ne x\\d&\text{if }y=x\end{cases}$
Definability and Elementary Class
We saw that we need $s:V\mapsto|\mathfrak{A}|$ to decide if $\mathfrak{A}$ models a FOL. Variables can be bound or free. Since bound variables are used as $\forall v_i;\varphi$, no matter what $v_i$ assumes from $|\mathfrak{A}|$, $\varphi$ will be true. Hence the only variables that decides if $\mathfrak{A}$ with $s$ satisfies $\varphi$ are free variables.
$\models_\mathfrak{A}\varphi[[a_1,\ldots,a_n]]$ tells if $\mathfrak{A}$ models $\varphi$ when all the free variables $v_i$ in $\varphi$ are set to $a_i$. Every $\varphi$ defines a set ${\langle a_1,\ldots,a_k\rangle\mid\models_\mathfrak{A}\varphi[[a_1,\ldots,a_k]]}$. Such sets is called definable in $\mathfrak{A}$.
Since a sentence has no free variable, either all $s$ will satisfy a particular sentence or none. $\mathrm{Mod}\ \Sigma$ is the class of all models that satisfies a set of sentences $\Sigma$. A class $\mathcal{K}$ is an elementary class ($\mathrm{EC_\triangle}$) if $\exists\Sigma\ni\mathcal{K}=\text{Mod }\Sigma$.
Definability and elementary class helps us to understand the feasibility and limitations of FOL.
Homomorphism
A map $h:\mathfrak{A}\mapsto\mathfrak{B}$ is homomorphism if
- $\langle a_1,\ldots,a_n\rangle\in P^\mathfrak{A}\leftrightarrow\langle h(a_1),\ldots,h(a_n)\rangle\in P^\mathfrak{B}$
- $h(f^\mathfrak{A}(a_1,\ldots,a_n))=f^\mathfrak{B}(h(a_1),\ldots,h(a_2))$ An isomorphism, $h$ is an injective homomorphism.
Homomorphism Theorem: Let $h:\mathfrak{A}\mapsto\mathfrak{B}$ be a homomorphism and $s:V\mapsto|\mathfrak{A}|$. As previously, we can define $\overline{s}:T\mapsto|\mathfrak{A}|$ from $s$. Once done that, we can define $(h\circ s)(t)\coloneqq h(\overline{s}(t))$. The theorem states that $\forall$ quantifier free formula $\alpha$ not containing equality symbol, $\models_\mathfrak{A}\alpha[s]\ \longleftrightarrow\ \models_\mathfrak{B}\alpha[h\circ s]$
Note that if $h$ is not injective, $\mathrm{i.e.}\exists u,v\ni\overline{s}(u)\ne\overline{s}(v)\land h(\overline{s}(u))=h(\overline{s}(v))$, the equality that might be true in $\mathfrak{B}$ with $h\circ s$ might not be true in $\mathfrak{A}$ with $s$. Of course if we $h$ is injective, we can drop the condition on equality in the homomorphism theorem.
Similarly if $h$ is not surjective, $\forall$ in $\mathfrak{A}$ would assert for all elements in $|\mathfrak{A}|$, but $h\circ s$ will covers only $\mathrm{rng}\ h\subset|\mathfrak{B}|$ and so there might be elements in $|\mathfrak{B}|\setminus\mathrm{rng}\ h$ that might not respect $\forall$ in $\mathfrak{B}$. Again, if $h$ is surjective, we can drop the condition on quantifier in the homomorphism theorem.