\documentclass{report}

\input{../../preamble}
\makecode{../..}

\externaldocument[S:]{Set}

\begin{document}

\header{A Mathematical Introduction to Logic}{Herbert B. Enderton}

\tableofcontents

\begingroup
\renewcommand\thechapter{R}

\chapter{Reference}%
\hyperlabel{chap:reference}

\section{\defined{Construction Sequence}}%
\hyperlabel{ref:construction-sequence}

  A \textbf{construction sequence} is a \nameref{ref:finite-sequence}
    $\ltuple{\epsilon_1}{\epsilon_n}$ of \nameref{ref:expression}s such that for
    each $i \leq n$ we have at least one of
    \begin{align*}
      & \epsilon_i \text{ is a sentence symbol} \\
      & \epsilon_i = \mathcal{E}_\neg(\epsilon_j) \text{ for some } j < i \\
      & \epsilon_i = \mathcal{E}_\square(\epsilon_j, \epsilon_k)
        \text{ for some } j < i, k < i
    \end{align*}
    where $\square$ is one of the binary connectives $\land$, $\lor$,
      $\Rightarrow$, $\Leftrightarrow$.

\section{\defined{Expression}}%
\hyperlabel{ref:expression}

  An \textbf{expression} is a \nameref{ref:finite-sequence} of symbols.

\section{\defined{Finite Sequence}}%
\hyperlabel{ref:finite-sequence}

  $S$ is a \textbf{finite sequence} (or \textbf{string}) of members of set $A$
    if and only if, for some positive integer $n$, we have
    $S = \ltuple{x_1}{x_n}$, where each $x_i \in A$.

\section{\defined{Formula-Building Operations}}%
\hyperlabel{ref:formula-building-operations}

  The \textbf{formula-building operations} (on expressions) are defined by the
  equations:
    \begin{align*}
      \mathcal{E}_{\neg}(\alpha)
        & = (\neg \alpha) \\
      \mathcal{E}_{\land}(\alpha, \beta)
        & = (\alpha \land \beta) \\
      \mathcal{E}_{\lor}(\alpha, \beta)
        & = (\alpha \lor \beta) \\
      \mathcal{E}_{\Rightarrow}(\alpha, \beta)
        & = (\alpha \Rightarrow \beta) \\
      \mathcal{E}_{\Leftrightarrow}(\alpha, \beta)
        & = (\alpha \Leftrightarrow \beta)
    \end{align*}

  \code*{Bookshelf/Enderton/Logic/Chapter\_1}
    {Enderton.Logic.Chapter\_1.Wff}

  \lean{Init/Prelude}
    {Not}

  \lean{Init/Prelude}
    {And}

  \lean{Init/Prelude}
    {Or}

  \lean{Init/Core}
    {Iff}

\section{\defined{\texorpdfstring{$n$}{n}-tuple}}%
\hyperlabel{ref:n-tuple}

  An \textbf{$n$-tuple} is recursively defined as
    $$\ltuple{x_1}{x_{n+1}} = \tuple{\ltuple{x_1}{x_n}, x_{n+1}}$$
    for $n > 1$.
  We also define $\tuple{x} = x$.

  \lean*{Init/Prelude}
    {Prod}

\section{\defined{Well-Formed Formula}}%
\hyperlabel{ref:well-formed-formula}

  A \textbf{well-formed formula} (wff) is an \nameref{ref:expression} that can
    be built up from the sentence symbols by applying some finite number of
    times the \nameref{ref:formula-building-operations}.

  \code*{Bookshelf/Enderton/Logic/Chapter\_1}
    {Enderton.Logic.Chapter\_1.Wff}

\endgroup

% Reset counter to mirror Enderton's book.
\setcounter{chapter}{0}
\addtocounter{chapter}{-1}
\chapter{Useful Facts About Sets}%
\hyperlabel{chap:useful-facts-about-sets}

\section{\unverified{Lemma 0A}}%
\hyperlabel{sec:lemma-0a}

  \begin{lemma}[0A]
    Assume that $\ltuple{x_1}{x_m} = \ltuple{y_1, \ldots, y_m}{y_{m+k}}$.
    Then $x_1 = \ltuple{y_1}{y_{k+1}}$.
  \end{lemma}

  \begin{proof}

    For natural number $m$, let $P(m)$ be the statement:
      \begin{induction}
        \hyperlabel{sec:lemma-0a-ih}
        If $\ltuple{x_1}{x_m} = \ltuple{y_1, \ldots, y_m}{y_{m+k}}$
          then $x_1 = \ltuple{y_1}{y_{k+1}}$.
      \end{induction}
    \noindent
    We proceed by induction on $m$.

    \paragraph{Base Case}%

      Suppose $\tuple{x_1} = \ltuple{y_1}{y_{1 + k}}$.
      By definition of an \nameref{ref:n-tuple}, $\tuple{x_1} = x_1$.
      Thus $x_1 = \ltuple{y_1}{y_{k + 1}}$.
      Hence $P(1)$ holds true.

    \paragraph{Inductive Step}%

      Suppose for $m \geq 1$ that $P(m)$ is true and assume
        \begin{equation}
          \hyperlabel{sec:lemma-0a-eq1}
          \ltuple{x_1}{x_{m+1}} = \ltuple{y_1, \ldots, y_{m+1}}{y_{m+1+k}}.
        \end{equation}
      By definition of an \nameref{ref:n-tuple}, we can decompose
        \eqref{sec:lemma-0a-eq1} into the following two identities
        \begin{align*}
          x_{m+1} & = y_{m+1+k} \\
          \ltuple{x_1}{x_m} & = \ltuple{y_1}{y_{m+k}}.
        \end{align*}
      By \ihref{sec:lemma-0a-ih}, $P(m)$ implies $x_1 = \ltuple{y_1}{y_{k+1}}$.
      Hence $P(m+1)$ holds true.

    \paragraph{Conclusion}%

      By induction, $P(m)$ holds true for all $m \geq 1$.

  \end{proof}

\chapter{Sentential Logic}%
\hyperlabel{chap:sentential-logic}

\section{The Language of Sentential Logic}%
\hyperlabel{sec:language-sentential-logic}

\subsection{\unverified{Induction Principle}}%
\hyperlabel{sub:induction-principle-1}

  \begin{theorem}
    If $S$ is a set of wffs containing all the sentence symbols and closed under
      all five formula-building operations, then $S$ is the set of \textit{all}
      wffs.
  \end{theorem}

  \code{Bookshelf/Enderton/Logic/Chapter\_1}
    {Enderton.Logic.Chapter\_1.Wff.rec}

  \begin{proof}
    We note every \nameref{ref:well-formed-formula} can be characterized by a
      \nameref{ref:construction-sequence}.
    For natural number $m$, let $P(m)$ be the statement:
      \begin{induction}
        \hyperlabel{sub:induction-principle-1-ih}
        Every wff characterized by a construction sequence of length $m$ is in
          $S$.
      \end{induction}
    \noindent
    We proceed by strong induction on $m$.

    \paragraph{Base Case}%

      Let $\phi$ denote a wff characterized by a construction sequence of length
        $1$.
      Then it must be that $\phi$ is a single sentence symbol.
      By hypothesis, $S$ contains all the sentence symbols.
      Thus $P(1)$ holds true.

    \paragraph{Inductive Step}%

      Suppose $P(0)$, $P(1)$, $\ldots$, $P(m)$ holds true and let $\phi$ denote
        a wff characterized by a construction sequence of length $m + 1$.
      By definition of a construction sequence, one of the following holds:
        \begin{align}
          & \phi \text{ is a sentence symbol}
            & \label{sub:induction-principle-1-eq1} \\
          & \phi = \mathcal{E}_\neg(\epsilon_j)
            \text{ for some } j < m + 1
            & \label{sub:induction-principle-1-eq2} \\
          & \phi = \mathcal{E}_\square(\epsilon_j, \epsilon_k)
            \text{ for some } j < m + 1, k < m + 1
            & \label{sub:induction-principle-1-eq3}
        \end{align}
        where $\square$ is one of the binary connectives $\land$, $\lor$,
          $\Rightarrow$, $\Leftrightarrow$.
      We consider each case in turn.

      \subparagraph{\eqref{sub:induction-principle-1-eq1}}%

        By hypothesis, all sentence symbols are in $S$.
        Thus $\phi \in S$.

      \subparagraph{\eqref{sub:induction-principle-1-eq2}}%

        Suppose $\phi = \mathcal{E}_\neg(\epsilon_j)$ for some $j < m + 1$.
        By \ihref{sub:induction-principle-1-ih}, $\epsilon_j$ is in $S$.
        By hypothesis, $S$ is closed under $\mathcal{E}_\neg$.
        Thus $\phi \in S$.

      \subparagraph{\eqref{sub:induction-principle-1-eq3}}%

        Suppose $\phi = \mathcal{E}_\square(\epsilon_j, \epsilon_k)$ for some
          $j < m + 1, k < m + 1$,
        By \ihref{sub:induction-principle-1-ih}, $\epsilon_j$ and $\epsilon_k$
          is in $S$.
        By hypothesis, $S$ is closed under $\mathcal{E}_\square$ for all
          possible candidates of $\square$.
        Thus $\phi \in S$.

      \subparagraph{Subconclusion}%

        Since the above three cases are exhaustive, $P(m + 1)$ holds.

    \paragraph{Conclusion}%

      By strong induction, $P(m)$ holds true for all natural numbers $m \geq 1$.
      Since every well-formed formula is characterized by a construction
        sequence, the set of all wffs is a subset of $S$.
      Likewise, it obviously holds that $S$ is a subset of all wffs.
      Thus $S$ is precisely the set of all wffs.

  \end{proof}

\subsection{\unverified{Balanced Parentheses}}%
\hyperlabel{sub:balanced-parentheses}

  \begin{lemma}
    All well-formed formulas have an equal number of left and right parentheses.
  \end{lemma}

  \begin{proof}

    Define $$S = \{ \phi \mid
      \phi \text{ is a wff with a balanced number of parentheses} \}.$$
    We prove that (i) all the sentence symbols are members of $S$ and (ii)
      $S$ is closed under the five \nameref{ref:formula-building-operations}.
    We then conclude with (iii) the proof of the theorem statement.

    \paragraph{(i)}%
    \hyperlabel{par:balanced-parentheses-i}

      By definition, well-formed formulas comprising a single sentence symbol
        do not have any parentheses.
      Thus all sentence symbols are members of $S$.

    \paragraph{(ii)}%
    \hyperlabel{par:balanced-parentheses-ii}

      Let $\alpha, \beta \in S$.
      By definition, $\mathcal{E}_{\neg}(\alpha) = (\neg\alpha)$.
      Thus one additional left and right parenthesis is introduced.
      Since $\alpha$ is assumed to have an equal number of left and right
        parentheses, $\mathcal{E}_{\neg}(\alpha) \in S$.
      Likewise,
        $\mathcal{E}_{\square}(\alpha, \beta) = (\alpha \mathop{\square} \beta)$
        where $\square$ is one of the binary connectives $\land$, $\lor$,
          $\Rightarrow$, $\Leftrightarrow$.
      Again, an additional left and right parenthesis is introduced.
      Since $\alpha$ and $\beta$ are assumed to have a balanced number of
        parentheses, $\mathcal{E}_{\square}(\alpha, \beta) \in S$.
      Hence $S$ is closed under the five formula-building operations.

    \paragraph{(iii)}%

      By \nameref{par:balanced-parentheses-i} and
        \nameref{par:balanced-parentheses-ii}, the
        \nameref{sub:induction-principle-1} implies $S$ is the set of all wffs.
      Thus all well-formed formulas have an equal number of left and right
        parentheses.

  \end{proof}

\subsection{\verified{Parentheses Count}}%
\hyperlabel{sub:parentheses-count}

  \begin{lemma}
    Let $\phi$ be a well-formed formula and $c$ be the number of places at which
      a sentential connective symbol exists.
    Then there is $2c$ parentheses in $\phi$.
  \end{lemma}

  \code{Enderton.Logic.Chapter\_1}
    {Enderton.Logic.Chapter\_1.paren\_count\_double\_sentential\_count}

  \begin{proof}

    Define $$S = \{ \phi \mid
      \phi \text{ is a wff with } 2c \text{ parentheses} \}.$$
    We prove that (i) all the sentence symbols are members of $S$ and (ii)
      $S$ is closed under the five \nameref{ref:formula-building-operations}.
    We then conclude with (iii) the proof of the theorem statement.

    \paragraph{(i)}%
    \hyperlabel{par:parentheses-count-i}

      A sentence symbol, by itself, has no sentential connectives.
      Likewise, it has 0 parentheses.
      Thus $S$ contains every sentence symbol.

    \paragraph{(ii)}%
    \hyperlabel{par:parentheses-count-ii}

      Let $\alpha, \beta \in S$.
      By definition, $\mathcal{E}_{\neg}(\alpha) = (\neg \alpha)$.
      Then $\mathcal{E}_{\neg}(\alpha)$ introduces two additional parentheses
         and one additional sentential connective symbol.
      Thus $\mathcal{E}_{\neg}(\alpha) \in S$.
      Likewise,
        $\mathcal{E}_{\square}(\alpha, \beta) = (\alpha \mathop{\square} \beta)$
        where $\square$ is one of the binary connectives $\land$, $\lor$,
          $\Rightarrow$, $\Leftrightarrow$.
      $\mathcal{E}_{\square}(\alpha, \beta)$ also introduces two additional
        parentheses and one additional connective symbol.
      Thus $\mathcal{E}_{\square}(\alpha, \beta) \in S$.
      Hence $S$ is closed under the five formula-building operations.

    \paragraph{(iii)}%

      By \nameref{par:parentheses-count-i} and
        \nameref{par:parentheses-count-ii}, the
        \nameref{sub:induction-principle-1} implies $S$ is the set of all wffs.
      Thus every wff has $2c$ parentheses in $\phi$, where $c$ denotes the
        number of places at which a sentential connective symbol exists.

  \end{proof}

\section{Exercises 1}%
\hyperlabel{sec:exercises-1}

\subsection{\unverified{Exercise 1.1.1}}%
\hyperlabel{sub:exercise-1.1.1}

  Give three sentences in English together with translations into our formal
    language.
  The sentences should be chosen so as to have an interesting structure, and the
    translations should each contain 15 or more symbols.

  \begin{answer}

    We begin first with the English sentences:
      \begin{enumerate}[(i)]
        \item He can juggle beach balls, bowling pins, and hackysacks unless
          he is tired, in which case he can only juggle beach balls.
        \item
          If Lauren goes to the moves with Sam, he will watch Barbie and
            eat popcorn, but if Lauren does not, he will watch Oppenheimer and
            eat gummy worms.
        \item
          Trees produce oxygen if they are alive and well, able to pull
            nutrients from the earth, and receive ample water.
      \end{enumerate}

    \paragraph{(i)}%

      We use the following translation: "To juggle beach balls" (B),
        "to juggle bowling pins" (P), "to juggle hackysacks" (H), and
        "he is tired" (T).
      This yields the following translation:
        $$(B \land ((\neg T) \Rightarrow (P \land H))).$$

    \paragraph{(ii)}%

      We use the following translation: "Lauren goes to the movies" (L),
        "Sam will watch Oppenheimer" (O), "Sam will watch "Barbie" (B),
        "Sam will eat popcorn" (P), and "Sam will eay gummy worms" (G).
      This yields the following translation:
        $$(((L \land B) \land P) \lor (((\neg L) \land O) \land G)).$$

    \paragraph{(iii)}%

      We use the following translation: "Trees produce oxygen" (O),
        "the tree is alive" (A), "the tree is well" (W), "can pull nutrients
        from the earth" (N), and "receives ample water" (R).
      This yields the following translation:
        $$(O \iff (((A \land W) \land N) \land R)).$$

  \end{answer}

\subsection{\pending{Exercise 1.1.2}}%
\hyperlabel{sub:exercise-1.1.2}

  Show that there are no wffs of length 2, 3, or 6, but that any other positive
    length is possible.

  \code*{Enderton.Logic.Chapter\_1}
    {Enderton.Logic.Chapter\_1.exercise\_1\_1\_2\_i}

  \code{Enderton.Logic.Chapter\_1}
    {Enderton.Logic.Chapter\_1.exercise\_1\_1\_2\_ii}

  \begin{proof}

    Define $$S = \{ \phi \mid
      \phi \text{ is a wff and the length of } \phi
        \text{ is not } 2, 3, \text{or } 6. \}.$$
    We prove that (i) all the sentence symbols are members of $S$ and (ii)
      $S$ is closed under the five \nameref{ref:formula-building-operations}.
    We then conclude with (iii) the proof of the theorem statement.

    \paragraph{(i)}%
    \hyperlabel{par:exercise-1.1.2-i}

      Sentence symbols, by definition, have length 1.
      Thus every sentence symbol is a member of $S$.

    \paragraph{(ii)}%
    \hyperlabel{par:exercise-1.1.2-ii}

      Define $L$ to be the length function mapping arbitrary wff to its length.
      Let $\alpha, \beta \in S$.
      Then $L(\alpha)$ and $L(\beta)$ each evaluate to 1, 4, 5, or a value
        larger than 6.

      By definition, $\mathcal{E}_{\neg}(\alpha) = (\neg \alpha)$.
      Thus $L(\mathcal{E}_{\neg}(\alpha)) = L(\alpha) + 3$.
      Enumerating through the possible values of $L(\alpha)$ shows
        $\mathcal{E}_{\neg}(\alpha) \in S$.
      Likewise,
        $\mathcal{E}_{\square}(\alpha, \beta) = (\alpha \mathop{\square} \beta)$
        where $\square$ is one of the binary connectives $\land$, $\lor$,
          $\Rightarrow$, $\Leftrightarrow$.
      Thus $L(\mathcal{E}_{\square}(\alpha, \beta)) = L(\alpha) + L(\beta) + 3$.
      Again, enumerating through the possible values of $L(\alpha)$ and
        $L(\beta)$ shows $\mathcal{E}_{\square}(\alpha, \beta) \in S$.

      Hence $S$ is closed under the five formula-building operations.

    \paragraph{(iii)}%

      By \nameref{par:exercise-1.1.2-i} and \nameref{par:exercise-1.1.2-ii}, the
        \nameref{sub:induction-principle-1} implies $S$ is the set of all wffs.
      It remains to be shown that a wff of any positive length excluding 2, 3,
        and 6 are possible.

      Let $\phi_1 = A_1$, $\phi_2 = (A_1 \land A_2)$, and
        $\phi_3 = ((A_1 \land A_2) \land A_3)$.
      Note these are wffs of lengths 1, 5, and 9 respectively.
      Then $n$ repeated applications of $\mathcal{E}_{\neg}$ yields wffs of
        length $1 + 3n$, $5 + 3n$, and $9 + 3n$ respectively.
      But
        \begin{align*}
          & \{ 1 + 3n \mid n \in \mathbb{N} \}, \\
          & \{ 5 + 3n \mid n \in \mathbb{N} \}, \text{ and } \\
          & \{ 9 + 3n \mid n \in \mathbb{N} \}
        \end{align*}
        form a \nameref{S:ref:partition} of set $\mathbb{N} - \{ 2, 3, 6 \}$.
      Thus a wff of any other positive length besides 2, 3, and 6 is possible.

  \end{proof}

\subsection{\verified{Exercise 1.1.3}}%
\hyperlabel{sub:exercise-1.1.3}

  Let $\alpha$ be a wff; let $c$ be the number of places at which binary
    connective symbols $(\land, \lor, \Rightarrow, \Leftrightarrow)$ occur in
    $\alpha$; let $s$ be the number of places at which sentence symbols occur in
    $\alpha$.
  (For example, if $\alpha$ is $(A \Rightarrow (\neg A))$ then $c = 1$ and
    $s = 2$.)
  Show by using the induction principle that $s = c + 1$.

  \code*{Enderton.Logic.Chapter\_1}
    {Enderton.Logic.Chapter\_1.exercise\_1\_1\_3}

  \begin{proof}

    Define
      \begin{equation}
        \hyperlabel{sub:exercise-1.1.3-eq1}
        S = \{\phi \mid \phi \text{ is a wff such that } s = c + 1\}.
      \end{equation}
    We prove that (i) all the sentence symbols are members of $S$ and (ii)
      $S$ is closed under the five \nameref{ref:formula-building-operations}.
    We then conclude with (iii) the proof of the theorem statement.

    \paragraph{(i)}%
    \hyperlabel{par:exercise-1.1.3-i}

      Let $\phi = A_n$ be an arbitrary sentence symbol.
      The number of places at which sentence symbols occur in $\phi$ is 1.
      The number of places at which binary connective symbols occur in $\phi$ is
        0.
      Hence $\phi \in S$.

    \paragraph{(ii)}%
    \hyperlabel{par:exercise-1.1.3-ii}

      Let $\alpha, \beta \in S$.
      Denote the number of places at which sentence symbols occur in each as
        $s_\alpha$ and $s_\beta$ respectively.
      Likewise, denote the number of places at which binary connective symbols
        occur as $c_\alpha$ and $c_\beta$.

      By definition, $\mathcal{E}_{\neg}(\alpha) = (\neg\alpha)$.
      The number of sentence and binary connective symbols in
        $\mathcal{E}_{\neg}(\alpha)$ does not change.
      Thus $\mathcal{E}_{\neg}(\alpha) \in S$.
      Likewise,
        $\mathcal{E}_{\square}(\alpha, \beta) = (\alpha \mathop{\square} \beta)$
        where $\square$ is one of the binary connectives $\land$, $\lor$,
          $\Rightarrow$, $\Leftrightarrow$.
      Therefore $\mathcal{E}_{\square}(\alpha, \beta)$ has $s_\alpha + s_\beta$
        sentence symbols and $c_\alpha + c_\beta + 1$ binary connective symbols.
      But \eqref{sub:exercise-1.1.3-eq1} implies
        \begin{align*}
          s_\alpha + s_\beta
            & = (c_\alpha + 1) + (c_\beta + 1) \\
            & = (c_\alpha + c_\beta + 1) + 1,
        \end{align*}
      meaning $\mathcal{E}_{\square}(\alpha, \beta) \in S$.

      Hence $S$ is closed under the five formula-building operations.

    \paragraph{(iii)}%
    \hyperlabel{par:exercise-1.1.3-iii}

      By \nameref{par:exercise-1.1.3-i} and \nameref{par:exercise-1.1.3-ii}, the
        \nameref{sub:induction-principle-1} indicates $S$ is the set of all
        wffs.

  \end{proof}

\subsection{\unverified{Exercise 1.1.4}}%
\hyperlabel{sub:exercise-1.1.4}

  Assume we have a construction sequence ending in $\phi$, where $\phi$ does not
    contain the symbol $A_4$.
  Suppose we delete all the expressions in the construction sequence that
    contain $A_4$.
  Show that the result is still a legal construction sequence.

  \begin{proof}


    Let $S$ denote a \nameref{ref:construction-sequence}
      $\ltuple{\epsilon_1}{\epsilon_n}$ such that $\epsilon_n = \phi$.
    Let $S' = \ltuple{\epsilon_{i_1}}{\epsilon_{i_m}}$ denote the construction
      sequence resulting from deleting all expressions in $S$ containing $A_4$.
    Fix $1 \leq j \leq m$.
    Then there exists some $1 \leq k \leq n$ such that
      $\epsilon_{i_j} = \epsilon_k$.
    By definition of a construction sequence, there are three cases to consider:

    \paragraph{Case 1}%

      Suppose $\epsilon_k$ is a sentence symbol.
      Then $\epsilon_{i_j}$ is also sentence symbol.

    \paragraph{Case 2}%

      Suppose $\epsilon_k = \mathcal{E}_{\neg}(\epsilon_a)$ for some $a < k$.
      It must be that $A_4$ is not found in $\epsilon_a$, else an immediate
        contradiction is raised.
      Therefore $\epsilon_a$ is a member of $S'$ that precedes $\epsilon_{i_j}$.
      Hence $\epsilon_{i_j} = \mathcal{E}_{\neg}(\epsilon_{i_a})$ for some
        $a < j$.

    \paragraph{Case 3}%

      Suppose $\epsilon_k = \mathcal{E}_{\square}(\epsilon_a, \epsilon_b)$ for
        some $a, b < k$ where $\square$ is one of the binary connectives
        $\land$, $\lor$, $\Rightarrow$, $\Leftrightarrow$.
      It must be that $A_4$ is found in neither $\epsilon_a$ nor $\epsilon_b$,
        else an immediate contradiction is raised.
      Therefore $\epsilon_a$ and $\epsilon_b$ is a member of $S'$, both of which
        precede $\epsilon_{i_j}$.
      Hence
        $\epsilon_{i_j} = \mathcal{E}_{\square}(\epsilon_{i_a}, \epsilon_{i_b})$
        for some $a, b < j$.

    \paragraph{Conclusion}%

      Since the above cases are exhaustive and apply to an arbitrary member of
        $S'$, it must be that every member of $S'$ is valid.
      Hence $S'$ is still a legal construction sequence.

  \end{proof}

\subsection{\verified{Exercise 1.1.5}}%
\hyperlabel{sub:exercise-1.1.5}

  Suppose that $\alpha$ is a wff not containing the negation symbol $\neg$.

\subsubsection{\verified{Exercise 1.1.5a}}%
\hyperlabel{ssub:exercise-1.1.5.a}

  Show that the length of $\alpha$ (i.e., the number of symbols in the string)
    is odd.
  \textit{Suggestion}: Apply induction to show that the length is of the form
    $4k + 1$.

  \code*{Enderton.Logic.Chapter\_1}
    {Enderton.Logic.Chapter\_1.exercise\_1\_1\_5\_a}

  \begin{proof}

    Define $L$ to be the length function mapping arbitrary
      \nameref{ref:well-formed-formula} to its length and let
      \begin{equation}
        \hyperlabel{ssub:exercise-1.1.5.a-eq1}
        S = \{\phi \mid
          \phi \text{ is a wff containing } \neg \text{ or }
          \exists k \in \mathbb{N}, L(\phi) = 4k + 1\}.
      \end{equation}
    We prove that (i) all the sentence symbols are members of $S$ and (ii)
      $S$ is closed under the five \nameref{ref:formula-building-operations}.
    We then conclude with (iii) the proof of the theorem statement.

    \paragraph{(i)}%
    \hyperlabel{par:exercise-1.1.5.a-i}

      Every sentence symbol has length 1 by definition.
      That is, every sentence symbol has length $(4)(0) + 1$.
      Hence $S$ contains every sentence symbol.

    \paragraph{(ii)}%
    \hyperlabel{par:exercise-1.1.5.a-ii}

      Let $\alpha, \beta \in S$.
      Then there exists some $k_\alpha$ and $k_\beta$ such that
        $L(\alpha) = 4k_\alpha + 1$ and $L(\beta) = 4k_\beta + 1$.
      Clearly $S$ is closed under $\mathcal{E}_{\neg}$.
      Next consider
        $\mathcal{E}_{\square}(\alpha, \beta) = (\alpha \mathop{\square} \beta)$
        where $\square$ is one of the binary connectives $\land$, $\lor$,
          $\Rightarrow$, $\Leftrightarrow$.
      Then
        \begin{align*}
          L(\alpha, \beta)
            & = L(\alpha) + L(\beta) + 3 \\
            & = (4k_\alpha + 1) + (4k_\beta + 1) + 3 \\
            & = 4k_\alpha + 4k_\beta + 4 + 1 \\
            & = 4(k_\alpha + k_\beta + 1) + 1.
        \end{align*}
      Therefore, there exists a $k \in \mathbb{N}$, namely
        $k = k_\alpha + k_\beta + 1$, such that
        $L(\mathcal{E}_{\square}(\alpha, \beta)) = 4k + 1$.

      Hence $S$ is closed under the five formula-building operations.

    \paragraph{(iii)}%

      By \nameref{par:exercise-1.1.5.a-i} and \nameref{par:exercise-1.1.5.a-ii},
        the \nameref{sub:induction-principle-1} indicates $S$ is the set of all
        wffs.
      Thus all well-formed formulas not containing symbol $\neg$ has length
        $4k + 1$ for some $k \in \mathbb{N}$.
      Therefore these well-formed formulas have odd length.

  \end{proof}

\subsubsection{\verified{Exercise 1.1.5b}}%
\hyperlabel{ssub:exercise-1.1.5-b}

  Show that more than a quarter of the symbols are sentence symbols.
  \textit{Suggestion}: Apply induction to show that the number of sentence
    symbols is of the form $k + 1$.

  \code*{Enderton.Logic.Chapter\_1}
    {Enderton.Logic.Chapter\_1.exercise\_1\_1\_5\_b}

  \begin{proof}

    Let $\phi$ be a \nameref{ref:well-formed-formula}.
    By \nameref{sub:exercise-1.1.3}, the number of sentence symbols of $\phi$ is
      $k + 1$, where $k$ is the number of places at which binary connective
      symbols occur in $\phi$.
    By \nameref{sub:parentheses-count}, the number of parentheses in $\phi$ is
      $2k$.
    Thus $\phi$ has length $(k + 1) + k + 2k = 4k + 1$.
    But $$\frac{k + 1}{4k + 1} > \frac{k + 1}{4k + 4} = \frac{1}{4}.$$
    Hence more than a quarter of the symbols of $\phi$ are sentence symbols.

  \end{proof}

\end{document}
