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)$.