| Version 14 |
Version 13 |
| Let $\Sigma$ be a signature. The \emph{first order language} $\operatorname{FO}(\Sigma)$ on $\Sigma$ contains the following: |
Terms and formulas of first order logic are constructed with the classical logical symbols $\forall$,$\exists$, |
| \begin{itemize} |
$\And$, $\Or$, $\neg$, $\Implies$, $\Iff$, and also $($ and $)$, |
| \item the set of \emph{symbols} of $\operatorname{FO}(\Sigma)$, which is the disjoint union of the following sets: |
and a set |
| \begin{enumerate} |
\begin{displaymath} |
| \item $\Sigma$ (the \emph{non-logical symbols}), |
\Sigma=\left(\bigcup_{n\in\omega}\operatorname{Rel}_n\right)\cup\left(\bigcup_{n\in\omega}\operatorname{Fun}_n |
| \item a countably infinite set $V$ of variables, |
\right)\cup |
| \item the set of logical symbols $\lbrace \And, \Or, \neg, \Implies, \Iff, \forall, \exists \rbrace$, and |
\operatorname{Const} |
| \item the set of parentheses (left and right) $\lbrace (, )\rbrace$; |
\end{displaymath} |
| \end{enumerate} |
|
| \item the set of \emph{terms} of $L$, which is built inductively from the symbols of $\operatorname{FO}(\Sigma)$, as follows: |
where for each natural number $n$, |
|
|
|
\begin{description} |
|
\item[$\bullet$] $\operatorname{Rel}_n$ is a (usually countable) set of $n$-ary relation symbols. |
|
\item[$\bullet$] $\operatorname{Fun}_n$ is a (usually countable) set of $n$-ary function symbols. |
|
\item[$\bullet$] $\operatorname{Const}$ is a (usually countable) set of constant symbols. |
|
\end{description} |
|
|
|
We require that all these sets be disjoint. |
|
The elements of the set $\Sigma$ are the {\em only} non-logical |
|
symbols that we are allowed to use when we construct terms and |
|
formulas. They form the {\bf signature} of the language. |
|
So far they are only symbols, so they don't mean |
|
anything. For most structures that we encounter, the set $\Sigma$ is |
|
finite, but we allow it to be infinite, even uncountable, as this |
|
sometimes makes things easier, and just about everything still works |
|
when the signature is uncountable. We also assume that we have an |
|
unlimited supply of {\em variables}, with the only constraint that the collection of variables form a set, which should be disjoint from the other sets of non-logical symbols. |
|
|
|
The {\bf arity} of a function or relation symbol is the number of parameters the symbol is about to take. It is usually assumed to be a property of the symbol, and it is bad grammar to use an $n$-ary function or relation with $m$ parameters if $m\not=n$. |
|
|
|
Terms are |
|
built inductively according to the following rules : |
|
|
| \begin{enumerate} |
\begin{enumerate} |
|
\item Any variable $v\in V$ is a term;
|
\item Any variable is a term;
|
|
\item Any constant symbol in $\Sigma$ is a term;
|
\item Any constant symbol i is a term;
|
|
\item If $f$ is an $n$-ary function symbol in $\Sigma$, and $t_1,...,t_n$ are
|
\item If $f$ is an $n$-ary function symbol, and $t_1,...,t_n$ are
|
| terms, then $f(t_1,...,t_n)$ is a term. |
terms, then $f(t_1,...,t_n)$ is a term. |
| \end{enumerate} |
\end{enumerate} |
| \item the set of \emph{formulas} of $L$, which is built inductively from the terms of $\operatorname{FO}(\Sigma)$, as follows: |
|
|
With terms in hand, we build formulas inductively by a finite application of the following rules : |
|
|
| \begin{enumerate} |
\begin{enumerate} |
|
\item If $t_1$ and $t_2$ are terms, then $(t_1=t_2)$ is a formula;
|
\item If $t_1$ and $t_2$ are terms, then $t_1=t_2$ is a formula;
|
| \item If $R$ is an $n$-ary relation symbol and $t_1,...,t_n$ are |
\item If $R$ is an $n$-ary relation symbol and $t_1,...,t_n$ are |
| terms, then $(R(t_1,...,t_n))$ is a formula; |
terms, then $R(t_1,...,t_n)$ is a formula; |
| \item If $\varphi$ is a formula, then so is $(\neg\varphi)$; |
\item If $\varphi$ is a formula, then so is $\neg\varphi$; |
| \item If $\varphi$ and $\psi$ are formulas, then so is $(\varphi\Or\psi)$; |
\item If $\varphi$ and $\psi$ are formulas, then so is |
| \item If $\varphi$ is a formula, and $x$ is a variable, then $(\exists x(\varphi))$ is a formula. |
$\varphi\Or\psi$; |
|
\item If $\varphi$ is a formula, and $x$ is a variable, then $\exists |
|
x(\varphi)$ is a formula. |
| \end{enumerate} |
\end{enumerate} |
| \end{itemize} |
|
|
|
| For example, in the first order language of partially ordered rings, expressions such as |
|
| $$0,\quad x^2,\quad\mbox{ and } \quad y+zx$$ are terms, while |
|
| $$(x=xy),\quad (x+y \le yz),\quad \mbox{ and }\quad (\exists x ((x\le 0) \Or (0\le x)))$$ are formulas. |
|
|
|
| \textbf{Remarks}. |
|
| \begin{enumerate} |
|
| \item |
|
| It is a common practice to omit parentheses in formulas, when there is no ambiguity. As such, the parentheses are also called the \emph{auxiliary symbols}. |
|
| \item |
|
| The first two types of formulas, not involving logical connectives, are the \emph{atomic formulas}. It is evident that formulas are inductively built from atomic formulas. |
|
| \item |
|
| The other logical symbols are obtained in the following way : |
The other logical symbols are obtained in the following way : |
|
|
| \begin{alignat*} |
\begin{alignat*} |
| \varphi\varphi\And\psi&\Def\neg(\neg\varphi\Or\neg\psi)&\qquad |
\varphi\varphi\And\psi&\Def\neg(\neg\varphi\Or\neg\psi)&\qquad |
| \varphi\Implies\psi&\Def\neg\varphi\Or\psi\\ |
\varphi\Implies\psi&\Def\neg\varphi\Or\psi\\ |
| \varphi\Iff\psi&\Def(\varphi\Implies\psi)\And(\psi\Implies\varphi)&\qquad |
\varphi\Iff\psi&\Def(\varphi\Implies\psi)\And(\psi\Implies\varphi)&\qquad |
| \forall x(\varphi)&\Def\neg(\exists x(\neg\varphi)) |
\forall x(\varphi)&\Def\neg(\exists x(\neg\varphi)) |
| \end{alignat*} |
\end{alignat*} |
|
|
| All logical symbols are used when building formulas. |
All logical symbols are used when building formulas. |
| \end{enumerate} |
|
