% Part: first-order-logic
% Chapter: syntax-and-semantics
% Section: free-vars-sentences

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

\begin{document}

\olfileid{fol}{syn}{fvs}

\olsection{Free \printtoken{P}{variable} and \printtoken{P}{sentence}}

\begin{defn}[Free occurrences of !!a{variable}]
\ollabel{defn:free-occ}
The \emph{free} occurrences of !!a{variable} in !!a{formula} are defined
inductively as follows:
\begin{enumerate}
\item \indcase*{!A}{$!A$ is atomic}{all !!{variable} occurrences in
  $\indfrm$ are free.}

\tagitem{prvNot}{\indcase{!A}{\lnot !B}{the free !!{variable}
  occurrences of $\indfrm$ are exactly those of $!B$.}}{}

\item \indcase{!A}{(!B \ast !C)}{the free
  !!{variable} occurrences of $\indfrm$ are those in $!B$
  together with those in~$!C$.}

\tagitem{prvAll}{\indcase{!A}{\lforall[x][!B]}{the free !!{variable}
  occurrences in $\indfrm$ are all of those in~$!B$ except for
  occurrences of~$x$.}}{}

\tagitem{prvEx}{\indcase{!A}{\lexists[x][!B]}{the free !!{variable}
  occurrences in $\indfrm$ are all of those in~$!B$ except for
  occurrences of~$x$.}}{}
\end{enumerate}
\end{defn}

\begin{defn}[Bound Variables]
An occurrence of !!a{variable} in a formula~$!A$ is \emph{bound} if
it is not free.
\end{defn}

\begin{prob}
Give an inductive definition of the bound variable occurrences along
the lines of \olref[fol][syn][fvs]{defn:free-occ}.
\end{prob}

\begin{defn}[Scope]
\iftag{prvAll}{If $\lforall[x][!B]$ is an occurrence of a subformula
  in a formula~$!A$, then the corresponding occurrence of~$!B$ in~$!A$
  is called the \emph{scope} of the corresponding occurrence
  of~$\lforall[x]$. \iftag{prvEx}{Similarly for $\lexists[x]$.}{}}{If
  $\lexists[x][!B]$ is an occurrence of a subformula in a
  formula~$!A$, then the corresponding occurrence of~$!B$ in~$!A$ is
  called the \emph{scope} of the corresponding occurrence
  of~$\lexists[x]$.}

If $!B$ is the scope of a quantifier occurrence
\iftag{prvAll}{$\lforall[x]$\iftag{prvEx}{ or
    $\lexists[x]$}{}}{$\lexists[x]$} in~$!A$, then the free occurrences of
$x$ in~$!B$ are bound in \iftag{prvAll}{$\lforall[x][!B]$\iftag{prvEx}{ and
$\lexists[x][!B]$}{}}{$\lexists[x][!B]$}. We say that these
occurrences are \emph{bound by} the
mentioned quantifier occurrence.
\end{defn}

\begin{ex}
Consider the following formula:
\[
\lexists[\Obj v_0][\underbrace{\Atom{\Obj A^2_0}{\Obj v_0,\Obj v_1}}_{!B}] 
\]
$!B$ represents the scope of $\lexists[\Obj v_0]$. 
The quantifier binds the occurrence of $\Obj v_0$ in $!B$, but
does not bind the occurrence of $\Obj v_1$. So $\Obj v_1$ is
a free variable in this case.


We can now see how this might work in a more complicated 
!!{formula}~$!A$:
\[
\lforall[\Obj v_0][\underbrace{(\Atom{\Obj A^1_0}{\Obj v_0} \lif
    \Atom{\Obj A^2_0}{\Obj v_0, \Obj v_1})}_{!B}] \lif \lexists[\Obj
  v_1][\underbrace{(\Atom{\Obj A^2_1}{\Obj v_0, \Obj v_1} \lor \lforall[\Obj v_0][\overbrace{\lnot \Atom{\Obj A^1_1}{\Obj v_0}}^{!D}])}_{!C}]
\]
$!B$ is the scope of the first $\lforall[\Obj v_0]$, $!C$ is the scope
of $\lexists[\Obj v_1]$, and $!D$ is the scope of the second
$\lforall[\Obj v_0]$.  The first $\lforall[\Obj v_0]$ binds the
occurrences of $\Obj v_0$ in~$!B$, $\lexists[\Obj v_1]$ binds the occurrence
of $\Obj v_1$ in $!C$, and the second $\lforall[\Obj v_0]$ binds the
occurrence of $\Obj v_0$ in~$!D$.  The first occurrence of $\Obj v_1$
and the fourth occurrence of $\Obj v_0$ are free in~$!A$. The last
occurrence of $\Obj v_0$ is free in $!D$, but bound in $!C$ and~$!A$.
\end{ex}

\begin{defn}[Sentence]
!!^a{formula}~$!A$ is \article{sentence} \emph{!!{sentence}} iff it
contains no free occurrences of !!{variable}s.
\end{defn}

% add examples!

\end{document}