diff --git a/Bookshelf/Enderton/Logic.tex b/Bookshelf/Enderton/Logic.tex
index 1bf97aa..8f1862c 100644
--- a/Bookshelf/Enderton/Logic.tex
+++ b/Bookshelf/Enderton/Logic.tex
@@ -5,6 +5,12 @@
 
 \externaldocument[S:]{Set}
 
+% Truth table start and final color
+\definecolor{TTStart}{gray}{0.95}
+\definecolor{TTEnd}{rgb}{1,1,0}
+\newcolumntype{s}{>{\columncolor{TTStart}}c}
+\newcolumntype{e}{>{\columncolor{TTEnd}}c}
+
 \begin{document}
 
 \header{A Mathematical Introduction to Logic}{Herbert B. Enderton}
@@ -796,32 +802,64 @@
 
   \end{proof}
 
-\subsection{\sorry{Exercise 1.2.1}}%
+\subsection{\verified{Exercise 1.2.1}}%
 \hyperlabel{sub:exercise-1.2.1}
 
   Show that neither of the following two formulas tautologically implies the
     other:
-    \begin{gather*}
-      (A \Leftrightarrow (B \Leftrightarrow C)), \\
+    \begin{gather}
+      (A \Leftrightarrow (B \Leftrightarrow C)),
+        \hyperlabel{sub:exercise-1.2.1-eq1} \\
       ((A \land (B \land C)) \lor ((\neg A) \land ((\neg B) \land (\neg C)))).
-    \end{gather*}
+        \hyperlabel{sub:exercise-1.2.1-eq2}
+    \end{gather}
   \textit{Suggestion}: Only two \nameref{ref:truth-assignment}s are needed, not
     eight.
 
+  \code*{Enderton.Logic.Chapter\_1}
+    {Enderton.Logic.Chapter\_1.exercise\_1\_2\_1\_i}
+
+  \code{Enderton.Logic.Chapter\_1}
+    {Enderton.Logic.Chapter\_1.exercise\_1\_2\_1\_ii}
+
   \begin{proof}
-    TODO
+    First, suppose $A = T$, $B = F$, and $C = F$.
+    Then \eqref{sub:exercise-1.2.1-eq1} evaluates to $T$ but
+      \eqref{sub:exercise-1.2.1-eq2} evaluates to $F$.
+    Therefore $\eqref{sub:exercise-1.2.1-eq1} \not\vDash
+      \eqref{sub:exercise-1.2.1-eq2}$.
+
+    Next, suppose $A = F$, $B = F$, and $C = F$.
+    Then \eqref{sub:exercise-1.2.1-eq2} evaluates to $T$ but
+      \eqref{sub:exercise-1.2.1-eq1} evaluates to $F$.
+    Therefore $\eqref{sub:exercise-1.2.1-eq2} \not\vDash
+      \eqref{sub:exercise-1.2.1-eq1}$.
   \end{proof}
 
-\subsection{\sorry{Exercise 1.2.2a}}%
+\subsection{\verified{Exercise 1.2.2a}}%
 \hyperlabel{sub:exercise-1.2.2a}
 
   Is $(((P \Rightarrow Q) \Rightarrow P) \Rightarrow P)$ a tautology?
 
+  \code*{Enderton.Logic.Chapter\_1}
+    {Enderton.Logic.Chapter\_1.exercise\_1\_2\_2a}
+
   \begin{proof}
-    TODO
+    Yes.
+    To prove, consider the following truth table:
+    $$
+      \begin{array}{s|c|s|c|s|e|s}
+        (((P & \Rightarrow & Q) & \Rightarrow & P) & \Rightarrow & P) \\
+        \hline
+        T & T & T & T & T & T & T \\
+        T & F & F & T & T & T & T \\
+        F & T & T & F & F & T & F \\
+        F & T & F & F & F & T & F
+      \end{array}
+    $$
   \end{proof}
 
-\subsection{\sorry{Exercise 1.2.2b}}%
+\subsection{\pending{Exercise 1.2.2b}}%
 \hyperlabel{sub:exercise-1.2.2b}
 
   Define $\sigma_k$ recursively as follows: $\sigma_0 = (P \Rightarrow Q)$ and
@@ -829,7 +867,95 @@
     $\sigma_k$ a tautology? (Part (a) corresponds to $k = 2$.)
 
   \begin{proof}
-    TODO
+
+    We prove that $\sigma_k$ is a tautology if and only if $k$ is an even
+      integer greater than zero.
+    To do so, we show (i) that $\sigma_k$ is a tautology for all even $k > 0$,
+      (ii) $\sigma_0$ is not a tautology, and (iii) $\sigma_k$ is not a
+      tautology for all odd $k$.
+
+    \paragraph{(i)}%
+    \hyperlabel{par:exercise-1.2.2b-i}
+
+      Let $P(k)$ be the predicate, "$\sigma_k$ is a tautology."
+      We prove $P(k)$ holds true for all even $k > 0$ via induction.
+
+      \subparagraph{Base Case}%
+
+        Let $k = 2$.
+        By definition,
+          $$\sigma_2 = (((P \Rightarrow Q) \Rightarrow P) \Rightarrow P).$$
+        \nameref{sub:exercise-1.2.2a} indicates $\sigma_2$ is a tautology.
+        Hence $P(2)$ is true.
+
+      \subparagraph{Inductive Step}%
+
+        Suppose $P(k)$ holds for some even $k > 0$.
+        By definition,
+          $$\sigma_{k + 2} = ((\sigma_{k} \Rightarrow P) \Rightarrow P).$$
+        Consider the truth table of the above:
+        $$
+          \begin{array}{c|c|s|e|s}
+            ((\sigma_k & \Rightarrow & P) & \Rightarrow & P) \\
+            \hline
+            T & T & T & T & T \\
+            T & T & T & T & T \\
+            T & F & F & T & F \\
+            T & F & F & T & F
+          \end{array}
+        $$
+        This shows $\sigma_{k+2}$ is a tautology.
+        Hence $P(k + 2)$ is true.
+
+      \subparagraph{Subconclusion}%
+
+        By induction, $P(k)$ is true for all even $k > 0$.
+
+    \paragraph{(ii)}%
+
+      By definition, $$\sigma_0 = (P \Rightarrow Q).$$
+      This is clearly not a tautology since $\sigma_0$ evaluates to $F$ when
+        $P = T$ and $Q = F$.
+
+    \paragraph{(iii)}%
+
+      Let $k > 0$ be an odd natural number.
+      There are two cases to consider:
+
+      \subparagraph{Case 1}%
+
+        Suppose $k = 1$.
+        Then $\sigma_k = \sigma_1 = ((P \Rightarrow Q) \Rightarrow P)$.
+        The following truth table shows $\sigma_1$ is not a tautology:
+        $$
+          \begin{array}{s|c|s|e|s}
+            (((P & \Rightarrow & Q) & \Rightarrow & P) \\
+            \hline
+            T & T & T & T & T \\
+            T & F & F & T & T \\
+            F & T & T & F & F \\
+            F & T & F & F & F
+          \end{array}
+        $$
+
+      \subparagraph{Case 2}%
+
+        Suppose $k > 1$.
+        Then $k - 1 > 0$ is an even number.
+        By definition, $$\sigma_k = (\sigma_{k-1} \Rightarrow P).$$
+        By \eqref{par:exercise-1.2.2b-i}, $\sigma_{k-1}$ is a tautology.
+        The following truth table shows $\sigma_k$ is not:
+        $$
+          \begin{array}{c|e|s}
+            (\sigma_{k-1} & \Rightarrow & P) \\
+            \hline
+            T & T & T \\
+            T & T & T \\
+            T & F & F \\
+            T & F & F
+          \end{array}
+        $$
+
   \end{proof}
 
 \subsection{\sorry{Exercise 1.2.3a}}%
diff --git a/Bookshelf/Enderton/Logic/Chapter_1.lean b/Bookshelf/Enderton/Logic/Chapter_1.lean
index 2614e4b..92e87ed 100644
--- a/Bookshelf/Enderton/Logic/Chapter_1.lean
+++ b/Bookshelf/Enderton/Logic/Chapter_1.lean
@@ -390,4 +390,68 @@ theorem exercise_1_1_5_b (α : Wff) (hα : ¬α.hasNotSymbol)
   ]
   exact inv_lt_one (by norm_num)
 
+/-! #### Exercise 1.2.1
+
+Show that neither of the following two formulas tautologically implies the
+other:
+```
+(A ↔ (B ↔ C))
+((A ∧ (B ∧ C)) ∨ ((¬ A) ∧ ((¬ B) ∧ (¬ C)))).
+```
+*Suggestion*: Only two truth assignments are needed, not eight.
+-/
+section Exercise_1_2_1
+
+private def f₁ (A B C : Prop) : Prop :=
+  A ↔ (B ↔ C)
+
+private def f₂ (A B C : Prop) : Prop :=
+  ((A ∧ (B ∧ C)) ∨ ((¬ A) ∧ ((¬ B) ∧ (¬ C))))
+
+theorem exercise_1_2_1_i
+  : f₁ True False False ≠ f₂ True False False := by
+  unfold f₁ f₂
+  simp
+
+theorem exercise_1_2_1_ii
+  : f₁ False False False ≠ f₂ False False False := by
+  unfold f₁ f₂
+  simp
+
+end Exercise_1_2_1
+
+section Exercise_1_2_2
+
+/-- #### Exercise 1.2.2a
+
+Is `(((P → Q) → P) → P)` a tautology?
+-/
+theorem exercise_1_2_2a (P Q : Prop)
+  : (((P → Q) → P) → P) := by
+  tauto
+
+/-! #### Exercise 1.2.2b
+
+Define `σₖ` recursively as follows: `σ₀ = (P → Q)` and `σₖ₊₁ = (σₖ → P)`. For
+which values of `k` is `σₖ` a tautology? (Part (a) corresponds to `k = 2`.)
+-/
+
+private def σ (P Q : Prop) : ℕ → Prop
+  | 0 => P → Q
+  | n + 1 => σ P Q n → P
+
+theorem exercise_1_2_2b_i (k : ℕ) (h : Even k ∧ k > 0)
+  : σ P Q k := by
+  sorry
+
+theorem exercise_1_2_2b_ii
+  : ¬ σ True False 0 := by
+  sorry
+
+theorem exercise_1_2_2b_iii (n : ℕ) (h : Odd n)
+ : ¬ σ False Q n := by
+ sorry
+
+end Exercise_1_2_2
+
 end Enderton.Logic.Chapter_1
diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex
index e95adf8..c279881 100644
--- a/Bookshelf/Enderton/Set.tex
+++ b/Bookshelf/Enderton/Set.tex
@@ -6,6 +6,8 @@
 \input{../../preamble}
 \makecode{../..}
 
+\externaldocument[S:]{../../Common/Real/Sequence}
+
 \newcommand{\ineq}{\,\mathop{\underline{\in}}\,}
 
 \begin{document}
@@ -854,7 +856,7 @@
       Therefore $V_1 = A \cup \powerset{V_0}$.
       This proves $P(1)$ holds true.
 
-    \paragraph{Induction Step}%
+    \paragraph{Inductive Step}%
 
       Suppose $P(n)$ holds true for some $n \geq 1$.
       Consider $V_{n+1}$.
@@ -8611,7 +8613,7 @@
     TODO
   \end{proof}
 
-\subsection{\sorry{Exercise 6.2}}%
+\subsection{\unverified{Exercise 6.2}}%
 \hyperlabel{sub:exercise-6-2}
 
   Show that in Fig. 32 we have:
@@ -8622,7 +8624,32 @@
     \end{align*}
 
   \begin{proof}
-    TODO
+    \begin{figure}[ht]
+      \label{sub:exercise-6-2-fig1}
+      \includegraphics[width=0.6\textwidth]{fig-32}
+      \centering
+    \end{figure}
+    Let $m, n \in \omega$.
+    We note the next point following $(m, n)$ that coincides with the $x$-axis
+      is $(m + n, 0)$.
+    We can then formulate the sum of points seen as
+      \begin{equation}
+        \hyperlabel{sub:exercise-5-2-eq1}
+        \left[ \sum_{i=0}^{m + n} (i + 1) \right] - n.
+      \end{equation}
+    All that remains is showing \eqref{sub:exercise-5-2-eq1} identifies with
+      the equation for $J$.
+    \eqref{sub:exercise-5-2-eq1} is an arithmetic series.
+    By \nameref{S:sub:sum-arithmetic-series},
+      \begin{align*}
+        \left[ \sum_{i=0}^{m + n} (i + 1) \right] - n
+          & = \frac{[(m + n) + 1][1 + (m + n + 1)]}{2} - n \\
+          & = \frac{[(m + n) + 1][(m + n) + 2]}{2} - n \\
+          & = \frac{(m + n)^2 + 2(m + n) + (m + n) - 2n}{2} \\
+          & = \frac{1}{2}[(m + n)^2 + 3m + n] \\
+          & = J(m, n).
+      \end{align*}
+    Hence $J$ is correctly defined.
   \end{proof}
 
 \subsection{\sorry{Exercise 6.3}}%
diff --git a/Bookshelf/Enderton/Set/images/fig-32.png b/Bookshelf/Enderton/Set/images/fig-32.png
new file mode 100644
index 0000000..d0724ed
Binary files /dev/null and b/Bookshelf/Enderton/Set/images/fig-32.png differ
diff --git a/preamble.tex b/preamble.tex
index 249ba19..18c67ac 100644
--- a/preamble.tex
+++ b/preamble.tex
@@ -1,5 +1,6 @@
 \usepackage{amsfonts, amsmath, amssymb, amsthm}
 \usepackage{bigfoot}
+\usepackage{colortbl}
 \usepackage{comment}
 \usepackage[shortlabels]{enumitem}
 \usepackage{etoolbox}