Version without JavaScript, read-only: workshops, quizzes and running code are not available here. Full version · Catalogue · Sign in
Exercise sheet 6
Natural deduction
Write Fitch-style proofs, from the most direct ones to those that need proof by contradiction, and relate proof and truth. Chapter 6.
Proofs are written as in chapter 6: one line per formula, with its justification; a temporary assumption opens a box (│), and the rule that discharges it closes it.
Solution
1.
| # | Formula | Justification |
|---|---|---|
| 1 | │ $p$ | assumed |
| 2 | $p \to p$ | $\to_i$ 1–1 |
2.
| # | Formula | Justification |
|---|---|---|
| 1 | $p \land q$ | hypothesis |
| 2 | $q$ | $\land_{e2}$ 1 |
| 3 | $p$ | $\land_{e1}$ 1 |
| 4 | $q \land p$ | $\land_i$ 2, 3 |
3.
| # | Formula | Justification |
|---|---|---|
| 1 | │ $p$ | assumed |
| 2 | │ │ $q$ | assumed |
| 3 | │ │ $p$ | reiteration of 1 |
| 4 | │ $q \to p$ | $\to_i$ 2–3 |
| 5 | $p \to (q \to p)$ | $\to_i$ 1–4 |
We are allowed to copy a line from an outer box that is still open (reiteration).
Solution
1.
| # | Formula | Justification |
|---|---|---|
| 1 | $p \to (q \to r)$ | hypothesis |
| 2 | │ $p \land q$ | assumed |
| 3 | │ $p$ | $\land_{e1}$ 2 |
| 4 | │ $q$ | $\land_{e2}$ 2 |
| 5 | │ $q \to r$ | $\to_e$ 1, 3 |
| 6 | │ $r$ | $\to_e$ 5, 4 |
| 7 | $p \land q \to r$ | $\to_i$ 2–6 |
2.
| # | Formula | Justification |
|---|---|---|
| 1 | $p \land q \to r$ | hypothesis |
| 2 | │ $p$ | assumed |
| 3 | │ │ $q$ | assumed |
| 4 | │ │ $p \land q$ | $\land_i$ 2, 3 |
| 5 | │ │ $r$ | $\to_e$ 1, 4 |
| 6 | │ $q \to r$ | $\to_i$ 3–5 |
| 7 | $p \to (q \to r)$ | $\to_i$ 2–6 |
A function that takes a pair $(a, b)$ is equivalent to a function that takes $a$ and returns a function waiting for $b$: this is currying, common in functional programming.
Solution
1.
| # | Formula | Justification |
|---|---|---|
| 1 | $p \to q$ | hypothesis |
| 2 | │ $\lnot q$ | assumed |
| 3 | │ │ $p$ | assumed |
| 4 | │ │ $q$ | $\to_e$ 1, 3 |
| 5 | │ │ $\bot$ | $\lnot_e$ 4, 2 |
| 6 | │ $\lnot p$ | $\lnot_i$ 3–5 |
| 7 | $\lnot q \to \lnot p$ | $\to_i$ 2–6 |
2.
| # | Formula | Justification |
|---|---|---|
| 1 | $p \lor q$ | hypothesis |
| 2 | │ $p$ | assumed (case 1) |
| 3 | │ $q \lor p$ | $\lor_{i2}$ 2 |
| 4 | │ $q$ | assumed (case 2) |
| 5 | │ $q \lor p$ | $\lor_{i1}$ 4 |
| 6 | $q \lor p$ | $\lor_e$ 1, 2–3, 4–5 |
3.
| # | Formula | Justification |
|---|---|---|
| 1 | $\lnot(p \lor q)$ | hypothesis |
| 2 | │ $p$ | assumed |
| 3 | │ $p \lor q$ | $\lor_{i1}$ 2 |
| 4 | │ $\bot$ | $\lnot_e$ 3, 1 |
| 5 | $\lnot p$ | $\lnot_i$ 2–4 |
| 6 | │ $q$ | assumed |
| 7 | │ $p \lor q$ | $\lor_{i2}$ 6 |
| 8 | │ $\bot$ | $\lnot_e$ 7, 1 |
| 9 | $\lnot q$ | $\lnot_i$ 6–8 |
| 10 | $\lnot p \land \lnot q$ | $\land_i$ 5, 9 |
Solution
1.
| # | Formula | Justification |
|---|---|---|
| 1 | $\lnot\lnot p$ | hypothesis |
| 2 | │ $\lnot p$ | assumed |
| 3 | │ $\bot$ | $\lnot_e$ 2, 1 |
| 4 | $p$ | RAA 2–3 |
2.
| # | Formula | Justification |
|---|---|---|
| 1 | │ $\lnot(p \lor \lnot p)$ | assumed |
| 2 | │ │ $p$ | assumed |
| 3 | │ │ $p \lor \lnot p$ | $\lor_{i1}$ 2 |
| 4 | │ │ $\bot$ | $\lnot_e$ 3, 1 |
| 5 | │ $\lnot p$ | $\lnot_i$ 2–4 |
| 6 | │ $p \lor \lnot p$ | $\lor_{i2}$ 5 |
| 7 | │ $\bot$ | $\lnot_e$ 6, 1 |
| 8 | $p \lor \lnot p$ | RAA 1–7 |
- For $p \vdash \lnot\lnot p$, the conclusion is a negation: we assume $\lnot p$, obtain $\bot$ with $p$, and $\lnot_i$ concludes. In the other two proofs, the conclusion is not a negation, and no hypothesis is contradictory: no other rule allows us to conclude. Logic without RAA is called intuitionistic logic. One shows there (a result we take for granted) that neither $\lnot\lnot p \to p$ nor $p \lor \lnot p$ is provable.
Solution
- Let $v$ make the hypotheses and $A \lor B$ true. Then $A$ or $B$ is true in $v$. If it is $A$, $v$ makes the hypotheses and $A$ true, hence $C$; otherwise $B$, likewise. In both cases $v \vDash C$.
- No. The interpretation $p = 0, q = 1$ makes $p \to q$ true and $q \to p$ false: $p \to q \not\vDash q \to p$. By soundness, $p \to q \not\vdash q \to p$.