Friday, October 7, 2011
Logical theorems and more proofs
1Logical theorems¶
A logical theorem (in $\Sigma$) is a $\Sigma$-formula $\Phi$ such that there can be a formal proof with last line $\vdash \Phi$.
Gödel's incompleteness threorem says that nothing can algorithmically decide whether or not $\Phi$ is a logical theorem. (Notably, there are algorithms for deciding if $\Phi$ is a tautology, or formula, etc.)
1.1Proof of a logical theorem¶
$$\forall x Px \iff \neg \exists x \neg Px$$
| Sequent | Justification/rule |
|---|---|
| (1) $Px ,\,\neg Px \vdash Py \land \neg Py$ | Tautology (due to material implication, $\bot \to$ anything) |
| (2) $\forall x Px \vdash Px$ | $\forall$-elimination |
| (3) $\forall x Px,\,Px,\,\neg Px \vdash Py \land \neg Py$ | Monotonicity from (1) |
| (4) $\forall x Px ,\,\neg Px \vdash Px$ | Monotonicity from (2) |
| (5) $\forall x Px ,\,\neg Px \vdash Py \land \neg Py$ | Transitivity using (3), (4) |
| (6) $\forall xPx,\,\exists x \neg Px \vdash Py \land \neg Py$ | $\exists$-elimination |
| (7) $\forall x Px \vdash \neg\exists x \neg Px$ | Contradiction from (6) |
| (8) $\vdash \forall x Px \to \neg \exists x \neg Px$ | Deduction from (7) |
| Now we need to get the other side: $\leftarrow$ basically | |
| (9) $\neg Px \vdash \neg Px$ | Tautology |
| (10) $\neg Px \vdash \exists x \neg Px$ | $\exists$-introduction from (9) |
| (11) $\vdash \neg Px \to \exists x \neg Px$ | Deduction from (10) |
| (12) $\neg Px \to \exists x \neg Px \vdash \neg \exists x \neg Px \to Px$ | Tautology, using contrapositives1 |
| (13) $\vdash \neg \exists x \neg Px \to Px$ | Transitivity using (11) and (12) |
| (14) $\neg \exists x \neg Px \vdash Px$ | Deduction from (13) |
| (15) $\neg \exists \neg P x \vdash \forall x Px$ | $\forall$-introduction from (14) |
| (16) $\vdash \neg \exists x \neg Px \to \forall x Px$ | Deduction from (15) |
| (17) $\forall x Px \to \exists x \neg Px,\, \neg \exists x \neg Px \to \forall x Px \vdash \forall x Px \iff \neg \exists x \neg Px$ | Tautology (connecting lines (1)-(8) and (9)-(16)) |
| (18) $\forall x Px \to \neg \exists x \neg Px \vdash \neg \exists x \neg Px \to \forall x Px$ | Monotonicity from (16) |
| (19) $\forall x Px \to \neg \exists x \neg Px \vdash \forall x Px \iff \neg \exists x \neg Px$ | Transitivity using (17) and (18) |
| (20) $\vdash \forall x Px \iff \neg \exists x \neg Px$ |
1.2Proof of another logical theorem¶
$$\forall x \forall y Pxy \iff \forall y \forall x Pxy$$
where $P$ is a binary predicate symbol. Again, we first prove the $\to$, then the $\leftarrow$.
| Sequent | Justification/rule |
|---|---|
| (1) $\forall x \forall y Pxy \vdash \forall y Pxy$ | $\forall$-elimination |
| (2) $\forall y Pxy \vdash Pxy$ | $\forall$-elimination |
| (3) $\forall x \forall y Pxy, \,\forall y Pxy \vdash Pxy$ | Monotonicity from (2) |
| (4) $\forall x \forall y Pxy \vdash Pxy$ | Transitivity using (1), (3) |
| (5) $\forall x \forall y Pxy \vdash \forall x Pxy$ | $\forall$-introduction from (4) |
| (6) $\forall x \forall y Pxy \vdash \forall y \forall x Pxy$ | $\forall$-introduction from (5) |
| (7) $\vdash \forall x \forall y Pxy \to \forall y \forall x Pxy$ | Deduction from (6) |
| ... | Same thing for (8)-(13), just switch the order on the left |
| (14) $\vdash \forall y \forall x Pxy \to \forall x \forall y Pxy$ | Deduction from (13) |
| (15) $\forall x \forall y Pxy \to \forall y \forall x Pxy,\, \forall y \forall x Pxy \to \forall x \forall y Pxy \vdash \forall x \forall y Pxy \iff \forall y \forall x Pxy$ | Tautology |
| (16) $\forall y \forall x Pxy \to \forall x \forall y Pxy \vdash \forall x \forall y Pxy \to \forall y \forall x Pxy$ | Monotonicity from (7) |
| (17) $\forall y \forall x Pxy \to \forall x \forall y Pxy \vdash \forall x \forall x Pxy \iff \forall y \forall x Pxy$ | Transitivity using (7), (16) |
| (18) $\vdash \forall x \forall y Pxy \iff \forall y \forall x Pxy$ | Transitivity using (14), (17)2 |
Note that $\exists x \forall y Pxy$ and $\forall y \exists x Pxy$ are not the same thing. However, $\exists x \exists y Pxy \iff \exists y \exists x Pxy$ is true.
1.3When something isn't a logical theorem¶
$$(\exists x Px \land \exists x Qx) \to \exists x (Px \land Qx)$$
This is not "sound" so we shouldn't be able to prove it. In fact, we should be able to come up with an empirical counterexample, and we can: if $Px$ means $x$ is a peach, and $Qx$ means $x$ is a quince, then if the theorem is sound there should be something that is both a quince and a peach. But there isn't.