# Proving $\forall x(x \text{ is odd} \to x^2 \text{ is odd)}$ using First Order Logic.

Symbolization key: We define:

• $$O(x)$$: $$x$$ is odd.

Proof:

$$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\} \def\Ai#1{\qquad\mathbf{\forall I} \: #1 \\} \def\Ee#1{\qquad\mathbf{\exists E} \: #1 \\} \def\Ei#1{\qquad\mathbf{\exists I} \: #1 \\} \def\R#1{\qquad\mathbf{R} \: #1 \\} \def\ii#1{\qquad\mathbf{\to I} \: #1 \\} \def\ie#1{\qquad\mathbf{\to E} \: #1 \\} \def\be#1{\qquad\mathbf{\leftrightarrow E} \: #1 \\} \def\be#1{\qquad\mathbf{\leftrightarrow E} \: #1 \\} \def\qe#1{\qquad\mathbf{=E} \: #1 \\} \def\ne#1{\qquad\mathbf{\neg E} \: #1 \\} \def\IP#1{\qquad\mathbf{IP} \: #1 \\} \def\x#1{\qquad\mathbf{X} \: #1 \\}$$ $$\fitch{1.\, \forall x \exists y(O(x) \leftrightarrow (x = 2y+1)}{ \fitch{2.\, O(a)}{ 3.\, \exists y(O(a) \leftrightarrow a = 2y+1) \Ae{1} \fitch{4.\, O(a) \leftrightarrow a = 2k+1}{ 5.\, a = 2k+1 \be{4,2} 6.\, a^2 = (2k+1)^2 \quad Leibniz\, 5\\ 7.\, a^2 = 2(2k^2+2k)+1 \quad arithmetic\, 6\\ \fitch{8.\, c = 2k^2+2k}{ 9.\, a^2 = 2c+1 \qe{8,7} \ldots \\ }\\ \ldots }\\ m. O(a^2) }\\ m+1.\,O(a) \to O(a^2)\\ m+2.\, \forall x(O(x) \to O(x^2)) \Ai{m+1} }$$

I do not know how can I discharge the assumption made on line 8. Am I heading in the right direction ?

EDIT: based on @Magdiragdag suggestions, I modified the proof to arrive at this one.

$$\fitch{1.\, \forall x (O(x) \leftrightarrow \exists y(x = 2y+1))}{ \fitch{2.\, O(a)}{ 3.\, O(a) \leftrightarrow \exists y(a = 2y+1) \Ae{1} 4.\, \exists y(a = 2y+1) \be{3} \fitch{5.\, a = 2k+1}{ 6.\, a^2 = (2k+1)^2 \quad Leibniz\, 5\\ 7.\, a^2 = 2(2k^2+2k)+1 \quad arithmetic\, 6\\ 8.\, \exists y(a^2=2y+1) \Ei{8} 9.\, O(a^2) \leftrightarrow \exists y(a^2=2y+1) \Ae{1} 10.\, O(a^2) \be{10,9} }\\ 11. O(a^2) }\\ 12.\,O(a) \to O(a^2) \ii{2-12} 13.\, \forall x(O(x) \to O(x^2)) \Ai{13} }$$

Your interpretation of $$O(x)$$ at line 1 is wrong. It's not $$\forall x \exists y [ O(x) \leftrightarrow x = 2 y + 1]$$, but $$\forall x [ O(x) \leftrightarrow \exists y[x = 2y + 1]]$$.
Additionally, there is no need to assuming anything at line 8. You can directly use $$\exists I$$ after line 7 to conclude $$\exists y [ a^2 = 2 y + 1]$$. Then use the characterisation of $$O(x)$$ again to conclude $$O(a^2)$$.
• There is no need to assume anything there; you can just conclude $\exists y[a^2 + 2y+1]$ directly after line 7. (Also, what is happening at line 8 is that you're assuming that $c$ equals $2k^2 + 2k$, but there is no $c$ in your formula. What you want is define $c$ to be $2k^2 + 2k$.) Apr 10, 2020 at 5:57
• Given a formula $\phi(y)$ (i.e., a formula $\phi$ in which the variable $y$ appears freely) and a term (i.e., expression) $t$, you can conclude $\exists y [ \phi(y) ]$ from $\phi(t)$. This is $\exists I$ and there is no need for $t$ to be a variable. Apr 10, 2020 at 11:59