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

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

\begin{document}

\olfileid{fol}{syn}{sbf}

\olsection{\printtoken{P}{subformula}}

\begin{explain}
It is often useful to talk about the !!{formula}s that ``make up'' a
given !!{formula}.  We call these its \emph{!!{subformula}s}.  Any
!!{formula} counts as !!a{subformula} of itself; a subformula of $!A$
other than $!A$ itself is a \emph{proper !!{subformula}}.
\end{explain}

\begin{defn}[Immediate !!^{subformula}]
If $!A$ is !!a{formula}, the \emph{immediate !!{subformula}s}
of $!A$ are defined inductively as follows:
\begin{enumerate}
\item Atomic !!{formula}s have no immediate !!{subformula}s.

\tagitem{prvNot}{\indcase{!A}{\lnot !B}{The only immediate
    !!{subformula} of $\indfrm$ is~$!B$.}}{}

\item \indcase{!A}{(!B \ast !C)}{The immediate !!{subformula}s of
  $\indfrm$ are $!B$ and $!C$ ($\ast$ is any one of the two-place
  connectives).}

\tagitem{prvAll}{\indcase{!A}{\lforall[x][!B]}{The only immediate
    !!{subformula} of $\indfrm$ is~$!B$.}}{}

\tagitem{prvEx}{\indcase{!A}{\lexists[x][!B]}{The only immediate
    !!{subformula} of $\indfrm$ is~$!B$.}}{}
\end{enumerate}
\end{defn}

\begin{defn}[Proper !!^{subformula}]
If $!A$ is !!a{formula}, the \emph{proper !!{subformula}s}
of $!A$ are defined recursively as follows:
\begin{enumerate}
\item Atomic !!{formula}s have no proper !!{subformula}s.

\tagitem{prvNot}{\indcase{!A}{\lnot !B}{The proper !!{subformula}s of
    $\indfrm$ are~$!B$ together with all proper !!{subformula}s
    of~$!B$.}}{}

\item \indcase{!A}{(!B \ast !C)}{The proper !!{subformula}s of
  $\indfrm$ are $!B$, $!C$, together with all proper !!{subformula}s
  of $!B$ and those of~$!C$.}

\tagitem{prvAll}{\indcase{!A}{\lforall[x][!B]}{The proper
    !!{subformula}s of $\indfrm$ are~$!B$ together with all proper
    !!{subformula}s of~$!B$.}}{}

\tagitem{prvEx}{\indcase{!A}{\lexists[x][!B]}{The proper
    !!{subformula}s of $\indfrm$ are~$!B$ together with all proper
    !!{subformula}s of~$!B$.}}{}
\end{enumerate}
\end{defn}

\begin{defn}[!!^{subformula}]
The !!{subformula}s of $!A$ are $!A$ itself together with all its
proper !!{subformula}s.
\end{defn}

\begin{explain}
Note the subtle difference in how we have defined immediate
!!{subformula}s and proper !!{subformula}s.  In the first case, we
have directly defined the immediate !!{subformula}s of a formula~$!A$
for each possible form of~$!A$.  It is an explicit definition by
cases, and the cases mirror the inductive definition of the set of
!!{formula}s.  In the second case, we have also mirrored the way the
set of all !!{formula}s is defined, but in each case we have also
included the proper !!{subformula}s of the smaller !!{formula}s $!B$,
$!C$ in addition to these !!{formula}s themselves.  This makes the
definition \emph{recursive}.  In general, a definition of a function
on an inductively defined set (in our case, !!{formula}s) is recursive
if the cases in the definition of the function make use of
the function itself. To be well defined, we must make sure, however,
that we only ever use the values of the function for arguments that
come ``before'' the one we are defining---in our case, when defining
``proper !!{subformula}'' for $(!B \ast !C)$ we only use the proper
!!{subformula}s of the ``earlier'' !!{formula}s $!B$ and $!C$.
\end{explain}

\begin{prop}
\ollabel{prop:subfrm-trans}
Suppose $!B$ is a subformula of $!A$ and $!C$ is a subformula of $!B$.
Then $!C$ is a subformula of $!A$. In other words, the subformula
relation is transitive.
\end{prop}

\begin{prob}
Prove \olref[fol][syn][sbf]{prop:subfrm-trans}.
\end{prob}

\begin{prop}
\ollabel{prop:count-subfrms}
Suppose $!A$ is a formula with $n$ connectives and quantifiers.
Then $!A$ has at most $2n+1$ subformulas.
\end{prop}

\begin{prob}
Prove \olref[fol][syn][sbf]{prop:count-subfrms}.
\end{prob}

\end{document}