Homework 6

1. Prove that $P \lor Q$ is logically equivalent to $Q \lor P$.

2. Show that $(\exists x, P(x)) \land Q$ is logically equivalent to $\exists x, (P(x) \land Q)$.

3. (hard) Show that $\lnot(P\to Q)$ is logically equivalent to $P\land \lnot Q$.

4. Show that it is not true that for all real numbers $x$, we have $x^2\geq x$.

5. Show that 7 is not even.

6. Let $p$ and $k$ be natural numbers, with $k\ne 1$, $k\ne p$, and $k\mid p$. Show that $p$ is not prime.

Notes

For 1, 2, 3, please write the problems only in Lean, not on paper.

For 3, the point of the exercise is that you are proving the lemma not_imp, from Table 5.1. So don't use that lemma or the tactic push_neg which depends on it; instead prove this from scratch. You will need to use the law of the excluded middle (the tactic by_cases).

For 4, 5, 6, please give a proof which begins with negation-normalization. In Lean this is the tactic push_neg. On paper your proof will begin, "It suffices to prove that ..." (and then state the logically equivalent goal obtained by negation-normalization).

For 5 and 6, please give proofs from first principles; that is, don't use the similar textbook lemmas (Int.odd_iff_not_even, not_prime).