From 0cc0cce2b5d458e0479ebd9133f01ad1b0ed289d Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Sun, 20 Aug 2023 09:30:07 -0600 Subject: [PATCH] Enderton (logic). Formally verify so-far solved 1.2 exercises. --- Bookshelf/Enderton/Logic.tex | 33 ++++++++-- Bookshelf/Enderton/Logic/Chapter_1.lean | 83 ++++++++++++++++++++++--- 2 files changed, 101 insertions(+), 15 deletions(-) diff --git a/Bookshelf/Enderton/Logic.tex b/Bookshelf/Enderton/Logic.tex index af50981..71cc037 100644 --- a/Bookshelf/Enderton/Logic.tex +++ b/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 diff --git a/Bookshelf/Enderton/Logic/Chapter_1.lean b/Bookshelf/Enderton/Logic/Chapter_1.lean index 1fe0010..004c9ca 100644 --- a/Bookshelf/Enderton/Logic/Chapter_1.lean +++ b/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) - : σ P Q k := by - sorry +theorem exercise_1_2_2b_i (P Q : Prop) {k : ℕ} (h : k > 0) + : σ P Q (2 * k) := by + 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) - : ¬ σ False Q n := by - sorry +theorem exercise_1_2_2b_iii {k : ℕ} (h : Odd k) + : ¬ σ False Q k := by + 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