<filename>content/first-order-logic/introduction/formulas.tex<gh_stars>100-1000
% Part: first-order-logic
% Chapter: introduction
% Section: formulas

\documentclass[../../../include/open-logic-section]{subfiles}

\begin{document}

\olfileid{fol}{int}{fml}

\section{\usetoken{P}{formula}}

Here is the approach we will use to rigorously specify !!{sentence}s
of first-order logic and to deal with the issues arising from the use
of !!{variable}s. We first define a \emph{different} set of
expressions: !!{formula}s. Once we've done that, we can consider the
role !!{variable}s play in them---and on the basis of some other
ideas, namely those of ``free'' and ``bound'' !!{variable}s, we can
define what !!a{sentence} is (namely, !!a{formula} without free
!!{variable}s). We do this not just because it makes the definition of
``!!{sentence}'' more manageable, but also because it will be crucial
to the way we define the semantic notion of satisfaction.

Let's define ``!!{formula}'' for a simple first-order language, one
containing only a single !!{predicate}~$\Obj P$ and a single
!!{constant}~$\Obj a$, and only the logical symbols $\lnot$, $\land$,
and~$\lexists$. Our full definitions will be much more general:
we'll allow infinitely many !!{predicate}s and !!{constant}s. In fact,
we will also consider !!{function}s which can be combined with
!!{constant}s and !!{variable}s to form ``terms.'' For now, $\Obj a$
and the variables will be our only terms.  We do need infinitely many
!!{variable}s.  We'll officially use the symbols $\Obj v_0$, $\Obj
v_1$, \dots, as variables.

\begin{defn}
The set of \emph{!!{formula}s}~$\Frm$ is defined as follows:
\begin{enumerate}
\item\ollabel{fmls-atom} $\Atom{\Obj P}{\Obj a}$ and $\Atom{\Obj
  P}{\Obj v_i}$ are !!{formula}s ($i \in \Nat$).

\tagitem{prvNot}{If $!A$ is !!a{formula}, then $\lnot !A$ is
  !!{formula}.}{}

\tagitem{prvAnd}{If $!A$ and $!B$ are !!{formula}s, then $(!A \land
  !B)$ is !!a{formula}.}{}

\tagitem{prvEx}{If $!A$ is !!a{formula} and $x$ is !!a{variable},
  then $\lexists[x][!A]$ is !!a{formula}.}{}

\tagitem{limitClause}{\ollabel{fmls-limit}Nothing else is !!a{formula}.}{}
\end{enumerate}
\end{defn}

\olref{fmls-atom} tell us that $\Atom{\Obj P}{\Obj a}$ and $\Atom{\Obj
P}{\Obj v_i}$ are !!{formula}s, for any $i \in \Nat$. These are
the so-called \emph{atomic} !!{formula}s. They give us something to
start from.  The other clauses give us ways of forming new
!!{formula}s from ones we have already formed. So for instance, we get
that $\lnot \Atom{\Obj P}{\Obj v_2}$ is !!a{formula}, since
$\Atom{\Obj P}{\Obj v_2}$ is already !!a{formula} by
\olref{fmls-atom}, and then we get that $\lexists[\Obj v_2][\lnot
\Atom{\Obj P}{\Obj v_2}]$ is another !!{formula}, and so on.
\olref{fmls-limit} tells us that \emph{only} strings we can form in
this way count as !!{formula}s. In particular, $\lexists[\Obj
v_0][\Atom{\Obj P}{\Obj a}]$ and $\lexists[\Obj v_0][\lexists[\Obj
v_0][\Atom{\Obj P}{\Obj a}]]$ \emph{do} count as !!{formula}s, and
$(\lnot \Atom{\Obj P}{\Obj a})$ does not.

This way of defining !!{formula}s is called an \emph{inductive
definition}, and it allows us to prove things about !!{formula}s using
a version of proof by induction called \emph{structural induction}.
These are discussed in a general way in \olref[mth][ind][idf]{sec} and
\olref[mth][ind][sti]{sec}, which you should review before delving
into the proofs later on. Basically, the idea is that if you want to
give a proof that something is true for all !!{formula}s you show
first that it is true for the atomic !!{formula}s, and then that
\emph{if} it's true for any !!{formula}~$!A$ (and~$!B$), it's
\emph{also} true for $\lnot !A$, $(!A \land !B)$, and
$\lexists[x][!A]$. For instance, this proves that it's true for
$\lexists[\Obj v_2][\lnot \Atom{\Obj P}{\Obj v_2}]$: from the first
part you know that it's true for the atomic !!{formula}~$\Atom{\Obj
P}{\Obj v_2}$. Then you get that it's true for $\lnot \Atom{\Obj
P}{\Obj v_2}$ by the second part, and then again that it's true for
$\lexists[\Obj v_2][\lnot \Atom{\Obj P}{\Obj v_2}]$ itself. Since all
!!{formula}s are inductively generated from atomic !!{formula}s, this
works for any of them.

\end{document}
