# 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.

1. $\neg A \to B \vdash \neg B \to A$. It's legitimate.

2. Bet you never thought the proof could be so long