Enderton (logic). Continue working through section 1.1.

Bookshelf/Enderton/Logic.tex

@@ -63,7 +63,7 @@
     \end{align*}
 
   \code*{Bookshelf/Enderton/Logic/Chapter\_1}
-    {Enderton.Logic.Chapter\_1.WFF}
+    {Enderton.Logic.Chapter\_1.Wff}
 
   \lean{Init/Prelude}
     {Not}
@@ -96,7 +96,7 @@
     times the \nameref{ref:formula-building-operations}.
 
   \code*{Bookshelf/Enderton/Logic/Chapter\_1}
-    {Enderton.Logic.Chapter\_1.WFF}
+    {Enderton.Logic.Chapter\_1.Wff}
 
 \endgroup
 
@@ -169,6 +169,9 @@
       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}.
@@ -244,6 +247,109 @@
 
   \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}
 
@@ -258,7 +364,7 @@
   \begin{answer}
 
     We begin first with the English sentences:
-      \begin{enumerate}[i]
+      \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
@@ -327,21 +433,21 @@
     \hyperlabel{par:exercise-1.1.2-ii}
 
       Define $L$ to be the length function mapping arbitrary wff to its length.
-      Let $\phi, \psi \in S$.
+      Let $\alpha, \beta \in S$.
-      Then $L(\phi)$ and $L(\psi)$ each evaluate to 1, 4, 5, or a value larger
+      Then $L(\alpha)$ and $L(\beta)$ each evaluate to 1, 4, 5, or a value
-        than 6.
+        larger than 6.
 
-      By definition, $\mathcal{E}_{\neg}(\phi) = (\neg \phi)$.
+      By definition, $\mathcal{E}_{\neg}(\alpha) = (\neg \alpha)$.
-      Thus $L(\mathcal{E}_{\neg}(\phi)) = L(\phi) + 3$.
+      Thus $L(\mathcal{E}_{\neg}(\alpha)) = L(\alpha) + 3$.
-      Enumerating through the possible values of $L(\phi)$ shows
+      Enumerating through the possible values of $L(\alpha)$ shows
-        $\mathcal{E}_{\neg}(\phi) \in S$.
+        $\mathcal{E}_{\neg}(\alpha) \in S$.
       Likewise,
-        $\mathcal{E}_{\square}(\phi, \psi) = (\phi \mathop{\square} \psi)$
+        $\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}(\phi, \psi)) = L(\phi) + L(\psi) + 3$.
+      Thus $L(\mathcal{E}_{\square}(\alpha, \beta)) = L(\alpha) + L(\beta) + 3$.
-      Again, enumerating through the possible values of $L(\phi)$ and $L(\psi)$
+      Again, enumerating through the possible values of $L(\alpha)$ and
-        shows $\mathcal{E}_{\square}(\phi, \psi) \in S$.
+        $L(\beta)$ shows $\mathcal{E}_{\square}(\alpha, \beta) \in S$.
 
       Hence $S$ is closed under the five formula-building operations.
 
@@ -368,7 +474,7 @@
 
   \end{proof}
 
-\subsection{\pending{Exercise 1.1.3}}%
+\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
@@ -379,6 +485,9 @@
     $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
@@ -413,10 +522,10 @@
         $\mathcal{E}_{\neg}(\alpha)$ does not change.
       Thus $\mathcal{E}_{\neg}(\alpha) \in S$.
       Likewise,
-        $\mathcal{E}_{\square}(\phi, \psi) = (\phi \mathop{\square} \psi)$
+        $\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}(\phi, \psi)$ has $s_\alpha + s_\beta$
+      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*}
@@ -424,7 +533,7 @@
             & = (c_\alpha + 1) + (c_\beta + 1) \\
             & = (c_\alpha + c_\beta + 1) + 1,
         \end{align*}
-      meaning $\mathcal{E}_{\square}(\phi, \psi) \in S$.
+      meaning $\mathcal{E}_{\square}(\alpha, \beta) \in S$.
 
       Hence $S$ is closed under the five formula-building operations.
 
@@ -493,46 +602,101 @@
 
   \end{proof}
 
-\subsection{\sorry{Exercise 1.1.5}}%
+\subsection{\pending{Exercise 1.1.5}}%
 \hyperlabel{sub:exercise-1.1.5}
 
   Suppose that $\alpha$ is a wff not containing the negation symbol $\neg$.
 
-\subsubsection{\sorry{Exercise 1.1.5a}}%
+\subsubsection{\verified{Exercise 1.1.5a}}%
-\hyperlabel{ssub:exercise-1.1.5-a}
+\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}
-    TODO
+
+    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{\sorry{Exercise 1.1.6a}}%
+\subsubsection{\pending{Exercise 1.1.5b}}%
-\hyperlabel{ssub:exercise-1.1.6-a}
+\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 $k + 1$.
+    symbols is of the form $k + 1$.
+
+  \code*{Enderton.Logic.Chapter\_1}
+    {Enderton.Logic.Chapter\_1.exercise\_1\_1\_5\_b}
 
   \begin{proof}
-    TODO
-  \end{proof}
 
-\subsection{\sorry{Exercise 1.1.6}}%
+    Let $\phi$ be a \nameref{ref:well-formed-formula}.
-\hyperlabel{sub:exercise-1.1.6}
+    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.
 
-  Suppose that $\alpha$ is a wff not containing the negation symbol $\neg$.
-  \begin{enumerate}[(a)]
-    \item Show that the length of $\alpha$ (i.e., the number of symbols in the
-      string) is odd.
-    \item Show that more than a quarter of the symbols are sentence symbols.
-  \end{enumerate}
-
-  \begin{proof}
-    TODO
   \end{proof}
 
 \end{document}

Bookshelf/Enderton/Logic/Chapter_1.lean

@@ -1,6 +1,9 @@
+import Common.Logic.Basic
 import Common.Nat.Basic
+import Mathlib.Algebra.Parity
 import Mathlib.Data.Nat.Basic
 import Mathlib.Tactic.NormNum
+import Mathlib.Tactic.Ring
 
 /-! # Enderton.Logic.Chapter_1
 
@@ -23,7 +26,7 @@ inductive Wff where
 namespace Wff
 
 /--
-Returns the length of the expression, including symbols.
+Returns the length of the expression, i.e. a count of all symbols..
 -/
 def length : Wff → ℕ
   | Wff.SS   _     => 1
@@ -34,7 +37,7 @@ def length : Wff → ℕ
   | Wff.Iff  e₁ e₂ => length e₁ + length e₂ + 3
 
 /--
-Every well-formed formula has a positive length.
+Every `Wff` has a positive length.
 -/
 theorem length_gt_zero (φ : Wff)
   : length φ > 0 := by
@@ -47,16 +50,122 @@ theorem length_gt_zero (φ : Wff)
   | Cond _ _
   |  Iff _ _ => simp
 
+/--
+The number of sentence symbols found in the provided `Wff`.
+-/
+def sentenceSymbolCount : Wff → ℕ
+  | Wff.SS   _     => 1
+  | Wff.Not  e     => sentenceSymbolCount e
+  | Wff.And  e₁ e₂
+  | Wff.Or   e₁ e₂
+  | Wff.Cond e₁ e₂
+  | Wff.Iff  e₁ e₂ => sentenceSymbolCount e₁ + sentenceSymbolCount e₂
+
+/--
+The number of sentential connective symbols found in the provided `Wff`.
+-/
+def sententialSymbolCount : Wff → ℕ
+  | Wff.SS   _     => 0
+  | Wff.Not  e     => sententialSymbolCount e + 1
+  | Wff.And  e₁ e₂
+  | Wff.Or   e₁ e₂
+  | Wff.Cond e₁ e₂
+  | Wff.Iff  e₁ e₂ => sententialSymbolCount e₁ + sententialSymbolCount e₂ + 1
+
+/--
+The number of binary connective symbols found in the provided `Wff`.
+-/
+def binarySymbolCount : Wff → ℕ
+  | Wff.SS   _     => 0
+  | Wff.Not  e     => binarySymbolCount e
+  | Wff.And  e₁ e₂
+  | Wff.Or   e₁ e₂
+  | Wff.Cond e₁ e₂
+  | Wff.Iff  e₁ e₂ => binarySymbolCount e₁ + binarySymbolCount e₂ + 1
+
+/--
+The number of parentheses found in the provided `Wff`.
+-/
+def parenCount : Wff → ℕ
+  | Wff.SS   _     => 0
+  | Wff.Not  e     => 2 + parenCount e
+  | Wff.And  e₁ e₂
+  | Wff.Or   e₁ e₂
+  | Wff.Cond e₁ e₂
+  | Wff.Iff  e₁ e₂ => 2 + parenCount e₁ + parenCount e₂
+
+/--
+Whether or not the `Wff` contains a `¬`.
+-/
+def hasNotSymbol : Wff → Prop
+  | Wff.SS   _     => False
+  | Wff.Not  _     => True
+  | Wff.And  e₁ e₂
+  | Wff.Or   e₁ e₂
+  | Wff.Cond e₁ e₂
+  | Wff.Iff  e₁ e₂ => hasNotSymbol e₁ ∨ hasNotSymbol e₂
+
+/--
+If a `Wff` does not contain the `¬` symbol, it has the same number of sentential
+connective symbols as it does binary connective symbols. In other words, the
+negation symbol is the only non-binary sentential connective.
+-/
+lemma no_neg_sentential_count_eq_binary_count {φ : Wff} (h : ¬φ.hasNotSymbol)
+  : φ.sententialSymbolCount = φ.binarySymbolCount := by
+  sorry
+
+/-- #### Parentheses Count
+
+Let `φ` 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 `φ`.
+-/
+theorem paren_count_double_sentential_count (φ : Wff)
+  : φ.parenCount = 2 * φ.sententialSymbolCount := by
+  induction φ with
+  | SS _ =>
+    unfold parenCount sententialSymbolCount
+    simp
+  | Not e ih =>
+    unfold parenCount sententialSymbolCount
+    rw [ih]
+    ring
+  | And  e₁ e₂ ih₁ ih₂
+  | Or   e₁ e₂ ih₁ ih₂
+  | Cond e₁ e₂ ih₁ ih₂
+  | Iff  e₁ e₂ ih₁ ih₂ =>
+    unfold parenCount sententialSymbolCount
+    rw [ih₁, ih₂]
+    ring
+
+/--
+The length of a `Wff` corresponds to the summation of sentence symbols,
+sentential connective symbols, and parentheses.
+-/
+theorem length_eq_sum_symbol_count (φ : Wff)
+  : φ.length = φ.sentenceSymbolCount +
+               φ.sententialSymbolCount +
+               φ.parenCount := by
+  induction φ with
+  | SS _ =>
+    unfold length sentenceSymbolCount sententialSymbolCount parenCount
+    simp
+  | Not e ih =>
+    unfold length sentenceSymbolCount sententialSymbolCount parenCount
+    rw [ih]
+    ac_rfl
+  | And  e₁ e₂ ih₁ ih₂
+  | Or   e₁ e₂ ih₁ ih₂
+  | Cond e₁ e₂ ih₁ ih₂
+  | Iff  e₁ e₂ ih₁ ih₂ =>
+    unfold length sentenceSymbolCount sententialSymbolCount parenCount
+    rw [ih₁, ih₂]
+    ac_rfl
+
 end Wff
 
-/-! #### Exercise 1.1.2
+/--
-
+An enumeration of values `m` and `n` can take on in equation `m + n = 3`.
-Show that there are no wffs of length `2`, `3`, or `6`, but that any other
-positive length is possible.
 -/
-
-section Exercise_1_1_2
-
 private lemma eq_3_by_cases (m n : ℕ) (h : m + n = 3)
   : m = 0 ∧ n = 3 ∨
     m = 1 ∧ n = 2 ∨
@@ -93,10 +202,16 @@ private lemma eq_3_by_cases (m n : ℕ) (h : m + n = 3)
     right; right; right
     exact ⟨m_eq_3, h⟩
 
+/-! #### Exercise 1.1.2
+
+Show that there are no wffs of length `2`, `3`, or `6`, but that any other
+positive length is possible.
+-/
+
 theorem exercise_1_1_2_i (φ : Wff)
   : φ.length ≠ 2 ∧ φ.length ≠ 3 ∧ φ.length ≠ 6 := by
   induction φ with
-  | SS c =>
+  | SS _ =>
     unfold Wff.length
     simp
   | Not e ih =>
@@ -140,45 +255,95 @@ theorem exercise_1_1_2_i (φ : Wff)
         intro h₃
         exact absurd h₃.left ih₁.right.left
 
-theorem exercise_1_1_2_ii (n : ℕ) (h : n ≠ 2 ∧ n ≠ 3 ∧ n ≠ 6)
+theorem exercise_1_1_2_ii (n : ℕ) (h : n ∈ Set.univ \ {2, 3, 6})
   : ∃ φ : Wff, φ.length = n := by
   let φ₁ := Wff.SS 1
   let φ₂ := Wff.And φ₁ (Wff.SS 2)
   let φ₃ := Wff.And φ₂ (Wff.SS 3)
   sorry
 
-end Exercise_1_1_2
+/-- #### Exercise 1.1.3
-
-/-! #### Exercise 1.1.3
 
 Let `α` be a wff; let `c` be the number of places at which binary connective
 symbols (`∧`, `∨`, `→`, `↔`) occur in `α`; let `s` be the number of places at
 which sentence symbols occur in `α`. (For example, if `α` is `(A → (¬ A))` then
 `c = 1` and `s = 2`.) Show by using the induction principle that `s = c + 1`.
 -/
-
-section Exercise_1_1_3
-
-private def binary_symbol_count : Wff → ℕ
-  | Wff.SS   _     => 0
-  | Wff.Not  e     => binary_symbol_count e
-  | Wff.And  e₁ e₂
-  | Wff.Or   e₁ e₂
-  | Wff.Cond e₁ e₂
-  | Wff.Iff  e₁ e₂ => binary_symbol_count e₁ + binary_symbol_count e₂ + 1
-
-private def sentence_symbol_count : Wff → ℕ
-  | Wff.SS   _     => 1
-  | Wff.Not  e     => sentence_symbol_count e
-  | Wff.And  e₁ e₂
-  | Wff.Or   e₁ e₂
-  | Wff.Cond e₁ e₂
-  | Wff.Iff  e₁ e₂ => sentence_symbol_count e₁ + sentence_symbol_count e₂
-
 theorem exercise_1_1_3 (φ : Wff)
-  : sentence_symbol_count φ = binary_symbol_count φ + 1 := by
+  : φ.sentenceSymbolCount = φ.binarySymbolCount + 1 := by
-  sorry
+  induction φ with
+  | SS _ =>
+    unfold Wff.sentenceSymbolCount Wff.binarySymbolCount
+    simp
+  | Not e ih =>
+    unfold Wff.sentenceSymbolCount Wff.binarySymbolCount
+    exact ih
+  | And  e₁ e₂ ih₁ ih₂
+  | Or   e₁ e₂ ih₁ ih₂
+  | Cond e₁ e₂ ih₁ ih₂
+  | Iff  e₁ e₂ ih₁ ih₂ =>
+    unfold Wff.sentenceSymbolCount Wff.binarySymbolCount
+    rw [ih₁, ih₂]
+    ring
 
-end Exercise_1_1_3
+/-- #### Exercise 1.1.5 (a)
+
+Suppose that `α` is a wff not containing the negation symbol `¬`. Show that the
+length of `α` (i.e., the number of symbols in the string) is odd.
+
+*Suggestion*: Apply induction to show that the length is of the form `4k + 1`.
+-/
+theorem exercise_1_1_5_a (α : Wff) (hα : ¬α.hasNotSymbol)
+  : Odd α.length := by
+  suffices ∃ k : ℕ, α.length = 4 * k + 1 by
+    have ⟨k, hk⟩ := this
+    unfold Odd
+    exact ⟨2 * k, by rw [hk, ← mul_assoc]; norm_num⟩
+  induction α with
+  | SS _ =>
+    refine ⟨0, ?_⟩
+    unfold Wff.length
+    simp
+  | Not e _ =>
+    unfold Wff.hasNotSymbol at hα
+    exfalso
+    exact hα trivial
+  | And  e₁ e₂ ih₁ ih₂
+  | Or   e₁ e₂ ih₁ ih₂
+  | Cond e₁ e₂ ih₁ ih₂
+  | Iff  e₁ e₂ ih₁ ih₂  =>
+    unfold Wff.hasNotSymbol at hα
+    rw [not_or_de_morgan] at hα
+    have ⟨k₁, hk₁⟩ := ih₁ hα.left
+    have ⟨k₂, hk₂⟩ := ih₂ hα.right
+    refine ⟨k₁ + k₂ + 1, ?_⟩
+    unfold Wff.length
+    rw [hk₁, hk₂]
+    ring
+
+/-- #### Exercise 1.1.5 (b)
+
+Suppose that `α` is a wff not containing the negation symbol `¬`. Show that more
+than a quarter of the symbols are sentence symbols.
+
+*Suggestion*: Apply induction to show that the number of sentence symbols is
+`k + 1`.
+-/
+theorem exercise_1_1_5_b (α : Wff) (hα : ¬α.hasNotSymbol)
+  : α.sentenceSymbolCount > α.length / 4 := by
+  have h₁ := α.sentenceSymbolCount
+  have h₂ := α.sententialSymbolCount
+  have h₃ := α.parenCount
+  rw [
+    α.length_eq_sum_symbol_count,
+    Wff.paren_count_double_sentential_count α,
+    Wff.no_neg_sentential_count_eq_binary_count hα,
+    exercise_1_1_3 α
+  ]
+  generalize Wff.binarySymbolCount α = k
+  calc k + 1
+    _ = 4 * (k + 1) / 4 := Eq.symm $ Nat.mul_div_cancel_left (k + 1) (by simp)
+    _ = (k + 4 + k + 2 * k) / 4 := by ring_nf
+    _ > (k + 1 + k + 2 * k) / 4 := by sorry
 
 end Enderton.Logic.Chapter_1

Bookshelf/Enderton/Set.lean

@@ -1,5 +1,6 @@
 import Bookshelf.Enderton.Set.Chapter_1
 import Bookshelf.Enderton.Set.Chapter_2
 import Bookshelf.Enderton.Set.Chapter_3
+import Bookshelf.Enderton.Set.Chapter_4
 import Bookshelf.Enderton.Set.OrderedPair
 import Bookshelf.Enderton.Set.Relation