# Homework (II)

**Problem 1.** Show that the law of double negation holds *constructively* for *negative* propositions, i.e. $A \iff \neg \neg A$ whenever $A$ is a propositional formula of the from $\neg P$.

- Write a natural deduction proof.
- Write a
`Lean`

proof.

**Problem 2.** Here is a proof of $\neg (P \iff \neg P)$ using the Law of Excluded Middle.

Is it possible to prove $\neg (P \iff \neg P)$ constructively (i.e. without using classical logic)? If so, construct such a proof. If no, give your reason and/or intuition why you think a constructive proof is not possible.

**Problem 3.** Using classical reasoning, show that for all propositions $P$ and $Q$ the following formulae are tautologies:

- $P \lor (P\To Q)$
- $(P \To Q) \lor (Q \To P)$

**Problem 4.** In this exercise weâ€™ll learn about *Peirceâ€™s law*, a curiosity of classical logic. Let $P$, $Q$ and $R$ be propositions.

- With the help of the law of double negation construct a proof of proposition \[ ((P \Rightarrow Q) \Rightarrow P) \Rightarrow P \] in the style of natural deduction.
- Write this proof in
`Lean`

.

**Problem 5.** An integer $m$ is said to *divide* an integer $n$, written $m \mid n$, if there exists an integer $k$ such that $n = mk$. We write $m \nmid n$ for $\neg (m \mid n)$. With this definition in hand, decide whether the following proof that $3 \nmid 20$ is constructive or not? Justify your answer.

Proof. Assume to the contrary that $3 \mid 20$. Then there exists a $k$ such that $20 = 3k$. By the fundamental theorem of arithmetic, $k$ has some unique prime factorization $k = 3 \prod_{i=1}^{n} p_i$. So $20$ factors into primes as $20 = 3 \prod_{i=1}^{n} p_i$. But we also know that $20 = 2 \times 2 \times 5$. The existence of two distinct prime factorizations for $20$ contradicts the uniqueness guaranteed by the fundamental theorem of arithmetic. We thus conclude that $3 \nmid 20$.

**Problem 6.** Give a constructive proof of the fact that the multiplication of two non-zero rational numbers is non-zero.

### Tips & Hints

- For problem 6, you might want to use the fact that a non-zero rational number has a multiplicative inverse.