Enderton (logic). Formally verify so-far solved 1.2 exercises.

Bookshelf/Enderton/Logic.tex

@@ -858,13 +858,22 @@
       \end{array}$$
   \end{proof}
 
-\subsection{\pending{Exercise 1.2.2b}}%
+\subsection{\verified{Exercise 1.2.2b}}%
 \hyperlabel{sub:exercise-1.2.2b}
 
   Define $\sigma_k$ recursively as follows: $\sigma_0 = (P \Rightarrow Q)$ and
     $\sigma_{k + 1} = (\sigma_k \Rightarrow P)$. For which values of $k$ is
     $\sigma_k$ a tautology? (Part (a) corresponds to $k = 2$.)
 
+  \code*{Enderton.Logic.Chapter\_1}
+    {Enderton.Logic.Chapter\_1.exercise\_1\_2\_2b\_i}
+
+  \code{Enderton.Logic.Chapter\_1}
+    {Enderton.Logic.Chapter\_1.exercise\_1\_2\_2b\_ii}
+
+  \code{Enderton.Logic.Chapter\_1}
+    {Enderton.Logic.Chapter\_1.exercise\_1\_2\_2b\_iii}
+
   \begin{proof}
 
     We prove that $\sigma_k$ is a tautology if and only if $k$ is an even
@@ -951,12 +960,15 @@
 
   \end{proof}
 
-\subsection{\pending{Exercise 1.2.3a}}%
+\subsection{\verified{Exercise 1.2.3a}}%
 \hyperlabel{sub:exercise-1.2.3a}
 
   Determine whether or not $((P \Rightarrow Q) \lor (Q \Rightarrow P))$ is a
     tautology.
 
+  \code*{Enderton.Logic.Chapter\_1}
+    {Enderton.Logic.Chapter\_1.exercise\_1\_2\_3a}
+
   \begin{proof}
     Consider the following truth table:
       $$\begin{array}{s|c|s|e|s|c|s}
@@ -971,12 +983,15 @@
       $((P \Rightarrow Q) \lor (Q \Rightarrow P))$ is a tautology.
   \end{proof}
 
-\subsection{\pending{Exercise 1.2.3b}}%
+\subsection{\verified{Exercise 1.2.3b}}%
 \hyperlabel{sub:exercise-1.2.3b}
 
   Determine whether or not $((P \land Q) \Rightarrow R)$ tautologically implies
     $((P \Rightarrow R) \lor (Q \Rightarrow R))$.
 
+  \code*{Enderton.Logic.Chapter\_1}
+    {Enderton.Logic.Chapter\_1.exercise\_1\_2\_3b}
+
   \begin{proof}
     Consider the following truth table:
       $$\begin{array}{s|s|s|e|e}
@@ -998,7 +1013,7 @@
       $((P \Rightarrow R) \lor (Q \Rightarrow R))$.
   \end{proof}
 
-\subsection{\pending{Exercise 1.2.4}}%
+\subsection{\unverified{Exercise 1.2.4}}%
 \hyperlabel{sub:exercise-1.2.4}
 
   Show that the following hold:
@@ -1103,7 +1118,7 @@
 
   \end{proof}
 
-\subsection{\pending{Exercise 1.2.5}}%
+\subsection{\verified{Exercise 1.2.5}}%
 \hyperlabel{sub:exercise-1.2.5}
 
   Prove or refute each of the following assertions:
@@ -1114,6 +1129,12 @@
         $\Sigma \vDash \alpha$ or $\Sigma \vDash \beta$.
     \end{enumerate}
 
+  \code{Enderton.Logic.Chapter\_1}
+    {Enderton.Logic.Chapter\_1.exercise\_1\_2\_5a}
+
+  \code{Enderton.Logic.Chapter\_1}
+    {Enderton.Logic.Chapter\_1.exercise\_1\_2\_5b}
+
   \begin{proof}
 
     \paragraph{(a)}%
@@ -1170,7 +1191,7 @@
 
   \end{proof}
 
-\subsection{\pending{Exercise 1.2.6a}}%
+\subsection{\unverified{Exercise 1.2.6a}}%
 \hyperlabel{sub:exercise-1.2.6a}
 
   Show that if $v_1$ and $v_2$ are \nameref{ref:truth-assignment}s which agree

Bookshelf/Enderton/Logic/Chapter_1.lean

@@ -422,7 +422,7 @@ end Exercise_1_2_1
 
 section Exercise_1_2_2
 
-/-- #### Exercise 1.2.2a
+/-- #### Exercise 1.2.2 (a)
 
 Is `(((P → Q) → P) → P)` a tautology?
 -/
@@ -430,7 +430,7 @@ theorem exercise_1_2_2a (P Q : Prop)
   : (((P → Q) → P) → P) := by
   tauto
 
-/-! #### Exercise 1.2.2b
+/-! #### Exercise 1.2.2 (b)
 
 Define `σₖ` recursively as follows: `σ₀ = (P → Q)` and `σₖ₊₁ = (σₖ → P)`. For
 which values of `k` is `σₖ` a tautology? (Part (a) corresponds to `k = 2`.)
@@ -440,18 +440,83 @@ 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)
+theorem exercise_1_2_2b_i (P Q : Prop) {k : ℕ} (h : k > 0)
-  : σ P Q k := by
+  : σ P Q (2 * k) := by
-  sorry
+  induction k with
+  | zero => simp at h
+  | succ k ih =>
+    by_cases hk : k = 0
+    · rw [hk]
+      simp only [Nat.mul_one]
+      unfold σ σ σ
+      exact exercise_1_2_2a P Q
+    · have := ih (Nat.pos_of_ne_zero hk)
+      unfold σ σ
+      have hk₁ := calc 2 * k.succ
+        _ = 2 * (k + 1) := rfl
+        _ = 2 * k + 2 * 1 := rfl
+        _ = 2 * k + 2 := by simp
+      rw [hk₁]
+      simp only [Nat.add_eq, add_zero]
+      tauto
 
 theorem exercise_1_2_2b_ii
   : ¬ σ True False 0 := by
-  sorry
+  unfold σ
+  simp
 
-theorem exercise_1_2_2b_iii (n : ℕ) (h : Odd n)
+theorem exercise_1_2_2b_iii {k : ℕ} (h : Odd k)
- : ¬ σ False Q n := by
+  : ¬ σ False Q k := by
- sorry
+  by_cases hk : k = 1
+  · unfold σ σ
+    rw [hk]
+    simp
+  · have ⟨n, hn₁, hn₂⟩ : ∃ n : ℕ, k = (2 * n) + 1 ∧ n > 0 := by
+      have ⟨r, hr⟩ := h
+      refine ⟨r, hr, ?_⟩
+      by_contra nr
+      have : r = 0 := Nat.eq_zero_of_nonpos r nr
+      rw [this] at hr
+      simp only [mul_zero, zero_add] at hr
+      exact absurd hr hk
+    unfold σ
+    rw [hn₁]
+    simp only [Nat.add_eq, add_zero, not_forall, exists_prop, and_true]
+    exact exercise_1_2_2b_i False Q hn₂
 
 end Exercise_1_2_2
 
+/-- #### Exercise 1.2.3 (a)
+
+Determine whether or not `((P → Q)) ∨ (Q → P)` is a tautology.
+-/
+theorem exercise_1_2_3a (P Q : Prop)
+  : ((P → Q) ∨ (Q → P)) := by
+  tauto
+
+/-- #### Exercise 1.2.3 (b)
+
+Determine whether or not `((P ∧ Q) → R))` tautologically implies
+`((P → R) ∨ (Q → R))`.
+-/
+theorem exercise_1_2_3b (P Q R : Prop)
+  : ((P ∧ Q) → R) ↔ ((P → R) ∨ (Q → R)) := by
+  tauto
+
+/-! #### Exercise 1.2.5
+
+Prove or refute each of the following assertions:
+
+(a) If either `Σ ⊨ α` or `Σ ⊨ β`, then `Σ ⊨ (α ∨ β)`.
+(b) If `Σ ⊨ (α ∨ β)`, then either `Σ ⊨ α` or `Σ ⊨ β`.
+-/
+
+theorem exercise_1_2_5a (P α β : Prop)
+  : ((P → α) ∨ (P → β)) → (P → (α ∨ β)) := by
+  tauto
+
+theorem exercise_1_2_6b
+  : (False ∨ True) ∧ ¬ False := by
+  simp
+
 end Enderton.Logic.Chapter_1