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

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

\begin{document}

\olfileid{fol}{syn}{unq}

\olsection{Unique Readability}

\begin{explain}
The way we defined !!{formula}s guarantees that every !!{formula} has
a \emph{unique reading}, i.e., there is essentially only one way of
constructing it according to our formation rules for !!{formula}s and
only one way of ``interpreting'' it.  If this were not so, we would
have ambiguous !!{formula}s, i.e., !!{formula}s that have more than
one reading or intepretation---and that is clearly something we want
to avoid.  But more importantly, without this property, most of the
definitions and proofs we are going to give will not go through.

Perhaps the best way to make this clear is to see what would happen if
we had given bad rules for forming !!{formula}s that would not
guarantee unique readability.  For instance, we could have forgotten
the parentheses in the formation rules for connectives, e.g., we might
have allowed this:
\begin{quote}
If $!A$ and $!B$ are !!{formula}s, then so is $!A \lif !B$.
\end{quote}
Starting from an atomic formula $!D$, this would allow us to form $!D
\lif !D$. From this, together with $!D$, we would get $!D \lif !D
\lif !D$.  But there are two ways to do this:
\begin{enumerate}
\item We take $!D$ to be $!A$ and $!D \lif !D$ to be $!B$.
\item We take $!A$ to be $!D \lif !D$ and $!B$ is~$!D$.  
\end{enumerate}
Correspondingly, there are two ways to
``read'' the !!{formula}~$!D \lif !D \lif !D$. It is of the form $!B
\lif !C$ where $!B$ is $!D$ and $!C$ is $!D \lif !D$, but \emph{it is
  also} of the form $!B \lif !C$ with $!B$ being $!D \lif !D$ and $!C$
being~$!D$.

If this happens, our definitions will not always work. For instance,
when we define the !!{main operator} of a formula, we say: in a
formula of the form $!B \lif !C$, the !!{main operator} is the
indicated occurrence of~$\lif$. But if we can match the formula $!D
\lif !D \lif !D$ with $!B \lif !C$ in the two different ways mentioned
above, then in one case we get the first occurrence of $\lif$ as the
!!{main operator}, and in the second case the second occurrence.  But
we intend the !!{main operator} to be a \emph{function} of the
!!{formula}, i.e., every !!{formula} must have exactly one !!{main
  operator} occurrence.
\end{explain}

\begin{lem}
The number of left and right parentheses in !!a{formula}~$!A$ are
equal.
\end{lem}

\begin{proof}
We prove this by induction on the way $!A$ is constructed. This
requires two things: (a) We have to prove first that all atomic
formulas have the property in question (the induction basis). (b) Then
we have to prove that when we construct new formulas out of given
formulas, the new formulas have the property provided the old ones do.

Let $l(!A)$ be the number of left parentheses, and $r(!A)$ the number
of right parentheses in~$!A$, and $l(t)$ and $r(t)$ similarly the
number of left and right parentheses in a term~$t$.

\begin{prob}
    Prove that for any term~$t$, $l(t) = r(t)$.
\end{prob}

\begin{enumerate}
\tagitem{prvFalse}{\indcase{!A}{\lfalse}{$\indfrm$ has $0$ left and $0$
    right parentheses.}}{}

\tagitem{prvTrue}{\indcase{!A}{\ltrue}{$\indfrm$ has $0$ left and $0$
    right parentheses.}}{}

\item \indcase{!A}{\Atom{R}{t_1,\dots,t_n}}{$l(\indfrm) = 1 + l(t_1) +
  \dots + l(t_n) = 1 + r(t_1) + \dots + r(t_n) = r(\indfrm)$. Here we
  make use of the fact, left as an exercise, that $l(t) = r(t)$ for
  any term~$t$.}

\item \indcase{!A}{\eq[t_1][t_2]}{$l(\indfrm) = l(t_1) + l(t_2) =
  r(t_1) + r(t_2) = r(\indfrm)$.}

\tagitem{prvNot}{\indcase{!A}{\lnot !B}{By induction hypothesis,
    $l(!B) = r(!B)$. Thus $l(\indfrm) = l(!B) = r(!B) =
    r(\indfrm)$.}}{}

\item \indcase{!A}{(!B \ast !C)}{By induction hypothesis, $l(!B) =
  r(!B)$ and $l(!C) = r(!C)$.  Thus $l(\indfrm) = 1 + l(!B) + l(!C) =
  1 + r(!B) + r(!C) = r(\indfrm)$.}

\tagitem{prvAll}{\indcase{!A}{\lforall[x][!B]}{By induction
    hypothesis, $l(!B) = r(!B)$. Thus, $l(\indfrm) = l(!B) = r(!B) =
    r(\indfrm)$.}}{}

% Print case for \lexists if prvEx and not prvAll
\tagitem{prvAll,notprvEx}{}{\indcase{!A}{\lexists[x][!B]}{By induction
    hypothesis, $l(!B) = r(!B)$. Thus, $l(\indfrm) = l(!B) = r(!B) =
    r(\indfrm)$.}}

% Just say similarly if prvEx and prvAll
\tagitem{notprvAll,notprvEx}{}{\indcase{!A}{\lexists[x][!B]}{Similarly.}}
\end{enumerate}
\end{proof}

\begin{defn}[Proper prefix]
A string of symbols $!B$ is a \emph{proper prefix} of a string of symbols~$!A$ if
concatenating $!B$ and a non-empty string of symbols yields~$!A$.
\end{defn}

\begin{lem}\ollabel{lem:no-prefix}
If $!A$ is !!a{formula}, and $!B$ is a proper prefix of $!A$, then
$!B$ is not !!a{formula}.
\end{lem}

\begin{proof}
Exercise.
\end{proof}

\begin{prob}
Prove \olref[fol][syn][unq]{lem:no-prefix}.
\end{prob}

\begin{prop}
\ollabel{prop:unique-atomic}
If $!A$ is an atomic !!{formula}, then it satisfies one, and only one
of the following conditions.
\begin{enumerate}
\tagitem{prvFalse}{$!A \ident \lfalse$.}{}
\tagitem{prvTrue}{$!A \ident \ltrue$.}{}
\item $!A \ident \Atom{R}{t_1,\dots,t_n}$ where $R$ is an $n$-place
  !!{predicate}, $t_1$, \dots, $t_n$ are terms, and each of $R$,
  $t_1$, \dots, $t_n$ is uniquely determined.
\item $!A \ident \eq[t_1][t_2]$ where $t_1$ and $t_2$ are uniquely
  determined terms.
\end{enumerate}
\end{prop}

\begin{proof}
Exercise.
\end{proof}

\begin{prob}
Prove \olref[fol][syn][unq]{prop:unique-atomic} (Hint: Formulate and
prove a version of \olref[fol][syn][unq]{lem:no-prefix} for terms.)
\end{prob}

\begin{prop}[Unique Readability]
Every !!{formula} satisfies one, and only one of the following conditions.
\begin{enumerate}
\item $!A$ is atomic.

\tagitem{prvNot}{$!A$ is of the form $\lnot !B$.}{}

\tagitem{prvAnd}{$!A$ is of the form $(!B \land !C)$.}{}

\tagitem{prvOr}{$!A$ is of the form $(!B \lor !C)$.}{}

\tagitem{prvIf}{$!A$ is of the form $(!B \lif !C)$.}{}

\tagitem{prvIff}{$!A$ is of the form $(!B \liff !C)$.}{}

\tagitem{prvAll}{$!A$ is of the form $\lforall[x][!B]$.}{}

\tagitem{prvEx}{$!A$ is of the form $\lexists[x][!B]$.}{}
\end{enumerate}
Moreover, in each case $!B$, or $!B$ and $!C$, are uniquely
determined.  This means that, e.g., there are no different pairs $!B$,
$!C$ and $!B'$, $!C'$ so that $!A$ is both of the form 
\iftag{prvIf}{$(!B \lif !C)$ and $(!B' \lif !C')$.}{
    \iftag{prvOr}{$(!B \lor !C)$ and $(!B' \lor !C')$.}{
      \iftag{prvAnd}{$(!B \land !C)$ and $(!B' \land !C')$.}{}}}
\end{prop}

\begin{proof}
The formation rules require that if !!a{formula} is not atomic, it
must start with an opening parenthesis~(, \iftag{prvNot}{$\lnot$,}{}
or a quantifier. On the other hand, every !!{formula} that starts with
one of the following symbols must be atomic: !!a{predicate}, !!a{function}, !!a{constant}\iftag{prvFalse}{, $\lfalse$}{}\iftag{prvTrue}{, $\ltrue$}{}.

So we really only have to show that if $!A$ is of the form $(!B \ast
!C)$ and also of the form $(!B' \mathbin{\ast'} !C')$, then $!B \ident
!B'$, $!C \ident !C'$, and $\ast = {\ast'}$.

So suppose both $!A \ident (!B \ast !C)$ and $!A \ident (!B'
\mathbin{\ast'} !C')$.  Then either $!B \ident !B'$ or not.  If it is,
clearly $\ast = {\ast'}$ and $!C \ident !C'$, since they then are
substrings of $!A$ that begin in the same place and are of the same
length.  The other case is $!B \not\ident !B'$.  Since $!B$ and
$!B'$ are both substrings of $!A$ that begin at the same place, one
must be a proper prefix of the other.  But this is impossible by
\olref{lem:no-prefix}.
\end{proof}


\end{document}