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}
}
$
Best Answer
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)$.