% Part: propositional-logic
% Chapter: propositional-logic
% Section: preliminaries

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

\begin{document}

\olfileid{pl}{syn}{pre}

\olsection{Preliminaries}

\begin{thm}[\emph{Principle of induction on !!{formula}s}]
  \ollabel{thm:induction}  
  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$;}{}
  \end{enumerate}
  then $P$ holds for all !!{formula}s.
\end{thm}

\begin{proof}
  Let $S$ be the collection of all !!{formula}s with
  property~$P$. Clearly $S \subseteq \Frm[L_0]$. $S$~satisfies all the
  conditions of \olref[fml]{defn:formulas}: it contains all atomic
  !!{formula}s and is closed under the !!{operator}s.  $\Frm[L_0]$ is
  the smallest such class, so $\Frm[L_0] \subseteq S$. So $\Frm[L_0] = S$, and
  every formula has property~$P$.
\end{proof}

\begin{prop}\ollabel{prop:balanced}
   Any !!{formula} in~$\Frm[L_0]$ is \emph{balanced}, in that it has
   as many left parentheses as right ones.
\end{prop}

\begin{prob}
Prove \olref[pl][syn][pre]{prop:balanced}
\end{prob}

\begin{prop} \ollabel{prop:noinit}
No proper initial segment of !!a{formula} is !!a{formula}.
\end{prop}

\begin{prob}
  Prove \olref[pl][syn][pre]{prop:noinit}
\end{prob}

\begin{prop}[Unique Readability]
Any !!{formula}~$!A$ in $ \Frm[L_0]$ has exactly one parsing as one of
the following
\begin{enumerate}
\tagitem{prvFalse}{$\lfalse$.}{}

\tagitem{prvTrue}{$\ltrue$.}{}

\item $\Obj p_n$ for some $\Obj p_n \in  \PVar$.
  
\tagitem{prvNot}{$\lnot !B$ for some !!{formula}~$!B$.}{}

\tagitem{prvAnd}{$(!B \land !C)$ for some !!{formula}s $!B$ and~$!C$.}{}

\tagitem{prvOr}{$(!B \lor !C)$ for some !!{formula}s $!B$ and~$!C$.}{}

\tagitem{prvIf}{$(!B \lif !C)$ for some !!{formula}s $!B$ and~$!C$.}{}

\tagitem{prvIff}{$(!B \liff !C)$ for some !!{formula}s $!B$ and~$!C$.}{}
\end{enumerate}
Moreover, this parsing is \emph{unique}.
\end{prop}

\begin{proof}
By induction on $!A$. For instance, suppose that $!A$ has two distinct
readings as $(!B \lif !C)$ and $(!B' \lif !C')$. Then $!B$ and $!B'$
must be the same (or else one would be a proper initial segment of the
other); so if the two readings of $!A$ are distinct it must be because
$!C$ and $!C'$ are distinct readings of the same sequence of symbols,
which is impossible by the inductive hypothesis.
\end{proof}


\begin{defn}[Uniform Substitution]
If $!A$ and $!B$ are !!{formula}s, and $\Obj p_i$ is a !!{propositional
variable}, then $\Subst{!A}{!B}{\Obj p_i}$ denotes the result of
replacing each occurrence of $\Obj p_i$ by an occurrence of $!B$ in $!A$;
similarly, the simultaneous substitution of $\Obj p_1$, \dots,~$\Obj p_n$ by
!!{formula}s $!B_1$, \dots,~$!B_n$ is denoted by
$\SSubst{!A}{\subst{!B_1}{\Obj p_1},\dots,\subst{!B_n}{\Obj p_n}}$.
\end{defn}

\begin{prob} For each of the five !!{formula}s below determine whether the 
 !!{formula} can be expressed as a substitution \( \Subst{!A}{!B}{\Obj p_i} \)
 where \( !A \) is (i) \( \Obj p_0 \); (ii) \( ( \lnot \Obj p_0 \land \Obj
 p_1) \); and (iii) \( ( ( \lnot \Obj p_0 \lif \Obj p_1 ) \land \Obj
 p_2 ) \). In each case specify the relevant substitution.
  \begin{enumerate}
    \item \( \Obj p_1 \) 
    \item \( ( \lnot \Obj p_0 \land \Obj p_0 ) \)
    \item \( ( ( \Obj p_0 \lor \Obj p_1 ) \land \Obj p_2 )  \)
    \item \( \lnot ( ( \Obj p_0 \lif \Obj p_1 ) \land \Obj p_2 ) \)
    \item \( (( \lnot ( \Obj p_0 \lif \Obj p_1 ) \lif ( \Obj p_0 \lor \Obj p_1 )) \land \lnot ( \Obj p_0 \land \Obj p_1 )) \)
  \end{enumerate}
\end{prob}

\begin{prob}
Give a mathematically rigorous definition of $\Subst{!A}{!B}{p}$ by
induction.
\end{prob}

\end{document}