From 90ad58d09d1d8aeffcb9cd2546da83f738c3b464 Mon Sep 17 00:00:00 2001 From: Jiecheng Z Date: Fri, 15 Sep 2023 16:26:30 +0800 Subject: [PATCH 1/2] Update quantifiers_and_equality.md Sorry, I ignore the hint in the `( )`. I think it would be more easier to catch if just put the hint in the code. --- quantifiers_and_equality.md | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/quantifiers_and_equality.md b/quantifiers_and_equality.md index a092eb9..bdfcb6a 100644 --- a/quantifiers_and_equality.md +++ b/quantifiers_and_equality.md @@ -927,16 +927,17 @@ You should also try to understand why the reverse implication is not derivable i 2. It is often possible to bring a component of a formula outside a universal quantifier, when it does not depend on the quantified - variable. Try proving these (one direction of the second of these - requires classical logic): + variable. Try proving these: ```lean variable (α : Type) (p q : α → Prop) variable (r : Prop) example : α → ((∀ x : α, r) ↔ r) := sorry -example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r := sorry example : (∀ x, r → p x) ↔ (r → ∀ x, p x) := sorry + +open classical +example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r := sorry ``` 3. Consider the "barber paradox," that is, the claim that in a certain From 6da5258a214a09ac96c32ec986cc941ef4493c36 Mon Sep 17 00:00:00 2001 From: Jiecheng Z Date: Sat, 16 Sep 2023 07:43:42 +0800 Subject: [PATCH 2/2] Update quantifiers_and_equality.md For question 3. I can solve it with em but I don't know if I am right. Also add a fix. If I am wrong. Please give me a hint. --- quantifiers_and_equality.md | 1 + 1 file changed, 1 insertion(+) diff --git a/quantifiers_and_equality.md b/quantifiers_and_equality.md index bdfcb6a..23828bf 100644 --- a/quantifiers_and_equality.md +++ b/quantifiers_and_equality.md @@ -945,6 +945,7 @@ example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r := sorry do not shave themselves. Prove that this is a contradiction: ```lean +open classical variable (men : Type) (barber : men) variable (shaves : men → men → Prop)