% Part: first-order-logic
% Chapter: syntax-and-semantics
% Section: terms-formulas

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

\begin{document}

\olfileid{fol}{syn}{frm}

\olsection{Terms and \printtoken{P}{formula}}

Once a first-order language~$\Lang L$ is given, we can define
expressions built up from the basic vocabulary of~$\Lang L$.  These
include in particular \emph{terms} and \emph{!!{formula}s}.

\begin{defn}[Terms]
\ollabel{defn:terms}
The set of \emph{terms}~$\Trm[L]$ of~$\Lang L$ is
defined inductively by:
\begin{enumerate}
\item Every !!{variable} is a term.
\item Every !!{constant} of~$\Lang L$ is a term.
\item If $f$ is an $n$-place !!{function} and $t_1$, \dots, $t_n$
  are terms, then $\Atom{f}{t_1, \ldots, t_n}$ is a term.
\tagitem{limitClause}{
  Nothing else is a term.}{}
\end{enumerate}
A term containing no !!{variable}s is a \emph{closed term}.
\end{defn}

\begin{explain}
The !!{constant}s appear in our specification of the language and the
terms as a separate category of symbols, but they could instead have
been included as zero-place !!{function}s.  We could then do without
the second clause in the definition of terms. We just have to
understand $\Atom{f}{t_1, \ldots, t_n}$ as just $f$ by itself if $n =
0$.
\end{explain}

\begin{defn}[Formulas]
\ollabel{defn:formulas}
The set of \emph{!!{formula}s}~$\Frm[L]$ of the language~$\Lang L$
is defined inductively as follows:
\begin{enumerate}
\tagitem{prvFalse}{$\lfalse$ is an atomic !!{formula}.}{}

\tagitem{prvTrue}{$\ltrue$ is an atomic !!{formula}.}{}

\item If $R$ is an $n$-place !!{predicate} of~$\Lang L$ and $t_1$, \dots,
  $t_n$ are terms of~$\Lang L$, then $\Atom{R}{t_1,\ldots, t_n}$ is an
  atomic !!{formula}.

\item If $t_1$ and $t_2$ are terms of~$\Lang L$, then $\Atom{\eq}{t_1, t_2}$
  is an atomic !!{formula}.

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

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

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

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

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

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

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

\tagitem{limitClause}{Nothing else is !!a{formula}.}{}
\end{enumerate}
\end{defn}

\begin{explain}
The definitions of the set of terms and that of !!{formula}s are
\emph{inductive definitions}.  Essentially, we construct the set of
!!{formula}s in infinitely many stages.  In the initial stage, we
pronounce all atomic formulas to be formulas; this corresponds to the
first few cases of the definition, i.e., the cases for
\iftag{prvTrue}{$\ltrue$, }{}%
\iftag{prvFalse}{$\lfalse$, }{}%
$\Atom{R}{t_1,\dots,t_n}$ and $\Atom{\eq}{t_1,t_2}$. ``Atomic
!!{formula}'' thus means any !!{formula} of this form.

The other cases of the definition give rules for constructing new
!!{formula}s out of !!{formula}s already constructed.  At the second
stage, we can use them to construct !!{formula}s out of atomic
!!{formula}s.  At the third stage, we construct new formulas from the
atomic formulas and those obtained in the second stage, and so on.  A
!!{formula} is anything that is eventually constructed at such a
stage, and nothing else.
\end{explain}

By convention, we write $\eq$ between its arguments and leave out the
parentheses: $\eq[t_1][t_2]$ is an abbreviation for
$\Atom{\eq}{t_1,t_2}$.  Moreover, $\lnot \Atom{\eq}{t_1,t_2}$ is
abbreviated as $\eq/[t_1][t_2]$. When writing a formula $(!B \ast !C)$
constructed from $!B$, $!C$ using a two-place connective~$\ast$, we
will often leave out the outermost pair of parentheses and write
simply~$!B \ast !C$.

\begin{intro}
Some logic texts require that the !!{variable}~$x$ must occur in~$!A$
in order for
\iftag{prvEx}{$\lexists[x][!A]$ }{}%
\iftag{notprvEx,notprvAll}{}{and }%
\iftag{prvAll}{$\lforall[x][!A]$ }{}%
to count as
\iftag{notprvEx,notprvAll}{!!a{formula}}{!!{formula}s}.
Nothing bad happens if you don't require this, and it makes things
easier.
\end{intro}

\begin{tagblock}{defNot,defOr,defAnd,defIf,defIff,defTrue,defFalse,defEx,defAll}
\begin{defn}
Formulas constructed using the defined operators are to be understood
as follows:

\begin{tagenumerate}{defTrue,defFalse,defNot,defOr,defAnd,defIf,defIff,defEx,defAll}

\tagitem{defTrue}{$\ltrue$ abbreviates
  \iftag{prvFalse}{$\lnot\lfalse$}{$(!A \lor \lnot !A)$ for some
    fixed atomic !!{formula}~$!A$}.}{}

\tagitem{defFalse}{$\lfalse$ abbreviates
  \iftag{prvTrue}{$\lnot\ltrue$}{$(!A \land \lnot !A)$ for some
    fixed atomic !!{formula}~$!A$}.}{}

\tagitem{defNot}{$\lnot !A$ abbreviates $!A \lif \lfalse$.}{}

\tagitem{defOr}{$!A \lor !B$ abbreviates
  \iftag{prvAnd}{$\lnot(\lnot !A \land \lnot !B)$}{$\lnot !A \lif
    !B$}.}{}

\tagitem{defAnd}{$!A \land !B$ abbreviates
  \iftag{prvOr}{$\lnot(\lnot !A \lor \lnot !B)$}{$\lnot (!A \lif
    \lnot !B)$}.}{}

\tagitem{defIf}{$!A \lif !B$ abbreviates
  \iftag{prvOr}{$\lnot !A \lor !B)$}{$\lnot (!A \land \lnot !B)$}.}{}

\tagitem{defIff}{$!A \liff !B$ abbreviates $(!A \lif !B) \land (!B
  \lif !A)$.}{}

\tagitem{defAll}{$\lforall[x][!A]$ abbreviates $\lnot\lexists[x][\lnot !A]$.}{}

\tagitem{defEx}{$\lexists[x][!A]$ abbreviates $\lnot\lforall[x][\lnot !A]$.}{}
\end{tagenumerate}
\end{defn}
\end{tagblock}

If we work in a language for a specific application, we will often
write two-place !!{predicate}s and !!{function}s between the
respective terms, e.g., $t_1 < t_2$ and $(t_1 + t_2)$ in the language
of arithmetic and $t_1 \in t_2$ in the language of set theory.  The
successor function in the language of arithmetic is even written
conventionally \emph{after} its argument:~$t'$.  Officially, however,
these are just conventional abbreviations for $\Atom{\Obj A^2_0}{t_1, t_2}$,
$\Obj f^2_0(t_1, t_2)$, $\Atom{\Obj A^2_0}{t_1, t_2}$ and $f^1_0(t)$,
respectively.

\begin{defn}[Syntactic identity]
The symbol $\ident$ expresses syntactic identity between strings of
symbols, i.e., $!A \ident !B$ iff $!A$ and $!B$ are strings of symbols
of the same length and which contain the same symbol in each place.
\end{defn}

The $\ident$ symbol may be flanked by strings obtained by
concatenation, e.g., $!A \ident (!B \lor !C)$ means: the string of
symbols~$!A$ is the same string as the one obtained by concatenating
an opening parenthesis, the string $!B$, the $\lor$ symbol, the
string~$!C$, and a closing parenthesis, in this order. If this is the
case, then we know that the first symbol of~$!A$ is an opening
parenthesis, $!A$ contains $!B$ as a substring (starting at the second
symbol), that substring is followed by~$\lor$, etc.

As terms and !!{formula}s are built up from basic elements via inductive
definitions, we can use the following induction principles to prove
things about them.

\begin{lem}[\emph{Principle of induction on terms}]
    \ollabel{lem:trmind}
    Let $\Lang L$ be a first-order language.
    If some property~$P$ is such that
    %
    \begin{enumerate}
        \item it holds for every !!{variable}~$v$,
        %
        \item it holds for every !!{constant}~$a$ of~$\Lang L$, and
        %
        \item it holds for $f(t_1,\dotsc,t_n)$ whenever it holds for
        $t_1$,~\dots, $t_n$ and $f$~is an $n$-place
            !!{function} of~$\Lang L$
    \end{enumerate}
    (assuming $t_1$,~\dots, $t_n$ are terms of~$\Lang{L}$),
    then $P$ holds for every term in~$\Trm[L]$.
\end{lem}

\begin{prob}
    Prove \olref[fol][syn][frm]{lem:trmind}.
\end{prob}

\begin{lem}[\emph{Principle of induction on !!{formula}s}]
    \ollabel{thm:frmind}
    Let $\Lang L$ be a first-order language.
    If some property~$P$ holds for all the atomic !!{formula}s
    and is such that
    %
    \begin{enumerate}
        \tagitem{prvNot}{it holds for $\lnot !A$ whenever it
            holds for~$!A$;}{}
        \tagitem{prvAnd}{it holds for $(!A \land !B)$
            whenever it holds for $!A$ and~$!B$;}{}
        \tagitem{prvOr}{it holds for $(!A \lor !B)$
            whenever it holds for $!A$ and~$!B$;}{}
        \tagitem{prvIf}{it holds for $(!A \lif !B)$
            whenever it holds for $!A$ and~$!B$;}{}
        \tagitem{prvIff}{it holds for $(!A \liff !B)$
            whenever it holds for $!A$ and~$!B$;}{}
        \tagitem{prvEx}{it holds for $\lexists[x][!A]$
            whenever it holds for~$!A$;}{}
        \tagitem{prvAll}{it holds for $\lforall[x][!A]$
            whenever it holds for~$!A$;}{}
  \end{enumerate}
  (assuming $!A$ and $!B$ are !!{formula}s of~$\Lang{L}$),
  then $P$ holds for all formulas in~$\Frm[L]$.
\end{lem}

\end{document}