2
$\begingroup$

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} } $

$\endgroup$

1 Answer 1

3
$\begingroup$

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

$\endgroup$
9
  • $\begingroup$ Thanks, @Magdiragdag. But how can I discharge the assumption on line 8? I get no benefit from applying →𝐈, for example. $\endgroup$
    – F. Zer
    Apr 9, 2020 at 23:38
  • 2
    $\begingroup$ 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$.) $\endgroup$ Apr 10, 2020 at 5:57
  • $\begingroup$ Thank you, @Magdiragdag. I edited the post. Do you think it is correct, now ? $\endgroup$
    – F. Zer
    Apr 10, 2020 at 10:49
  • $\begingroup$ Looks ok. I don't know how your system deals with introducing abbreviations like you do in line 8, but it seems reasonable. You can drop that line, though. $\endgroup$ Apr 10, 2020 at 11:24
  • 1
    $\begingroup$ 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. $\endgroup$ Apr 10, 2020 at 11:59

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .