It's legitimate but scrappy, if I understand correctly. You've made a proof by contradiction again.
The problem with contradiction is that it doesn't tell you anything other than "my assumption is false". If you prove that $\neg B \Rightarrow \neg A$ without assuming $A$, you know that any results you end up proving along the way (before you finally end up with $\neg A$) are implied by the single assumption $\neg B$.
If you prove that $\neg B \wedge A \Rightarrow \bot$, then you can't use anything you prove along the way: it only tells you that $A \Rightarrow B$, and nothing further.
Your result may be proved directly: if $x \leq y$ and $y \leq z$, then we have three possible cases of the relation between $x$ and $y$ (by trichotomy):
- $x = y$. Then $x = y \leq z$ immediately.
- $x < y$. Then:
- if $y = z$, we're done again: $x < y = z$ so $x \leq z$.
- if $y < z$, then $x < y$ and $y < z$; $<$ is known to be transitive so $x < z$, and in particular $x \leq z$.
- $x > y$ (which we already know is not the case, because $x \leq y$).
Did I translate this correctly?
No. The oddness needs to be quantified too.
You want $\forall n~\big(\exists k~(n=2k+1)~\to~\exists k~\exists l~(n=k^2-l^2)\big)$
It might be helpful to emphasise that the existance establishing oddness is distinct from the existances establishing sum-of-squares.
$$\forall n~\big(\exists k~(n=2k+1)~\to~\exists a~\exists b~(n=a^2-b^2)\big)$$
In my initial universal quantifier, I sometimes see people write $∀n∈S P(n)$. Is this just another way of specifying the domain so I don't have to say what the domain is after writing everything down in symbols? A kind of shorthand?
You may wish to explicitly indicate the domain of the discussion.
$$\forall n\in\Bbb Z~\big(\exists k\in\Bbb Z~(n=2k+1)~\to~\exists a\in\Bbb Z~\exists b\in\Bbb Z~(n=a^2-b^2)\big)$$
As you see, this can clutter the statement when every entity is drawn from the same domain. So if you have established in accompanying text that is the implicit domain is the Integers, there is no need to explicitly indicate it in the statement.
In the book I use they'll nest quantifiers explicitly like $∃k~∃l~Q(k,l)$. In my translation I did what I've seen elsewhere which is to do $∃~k,l~Q(k,l)$ is this okay?
It is a style choice. I prefer explictly quantifying each variable, but again, abbreviating things can reduce clutter
And if the answer to Question 2 above was that using the $∈$ shorthand is acceptable, then I'm guessing I could also write this as $∃~k,l~∈S~Q(k,l)$.
It ... is accepted, as long as you take care to avoid ambiguity.
I know to begin working on a universally quantified statement I can invoke universal instantiation. My book defines this as $∀x~P(x)~∴~P(c)$. It then goes on with an example of a formal proof using this on the form $∀x~(P(x)⟹Q(x))~∴~P(a)⟹Q(a)$. How are they applying Universal Instantiation across the $⟹$, when the definition only has a single predicate $P(x)$? Is it that they've set $P(x)$ to mean $P(x)⟹Q(x)$?
Yes, you substitute $c$ for $x$ everywhere in the scope of the quantification. Here that is $(P(x)\to Q(x))$. In Universal Elimination (or Instantiation) you are deducing that if something is true about the universal bound variable $x$, then it will be true for an unbound variable $c$. (Or $a$ or whatever.)
Finally, for direct proof we assume the antecedent is true and try to deduce the consequent. But, doesn't this create the same problem as above? Begging the question that is. Say I have $∀x(P(x)⟹Q(x))$. Then I use direct proof to assume $P(x)$ is true. Well wouldn't I use Universal instantiation here and have
$P(a)$, then using Universal Modus Ponens I could automatically infer
$Q(a)$ is true?
No. If $∀x~(P(x)\to Q(x))$ is what you are trying to prove, then you don't have it. You cannot assert that a conclusion is proven inside its own proof.
Your argument should go: Let $a$ be an arbitrary term. Assume $P(a)$ and derive $Q(a)$ by some valid logic. Thus deducing that $P(a)\to Q(a)$, and since $a$ is arbitrary therefore, by Universal Generalisation, $\forall x~(P(x)\to Q(x))$.
In this case:
Let $m$ be an arbitrary integer, and assume there exists some integer $c$ such that $m=2c+1$. Since for any $c$, $(c+1)^2=c^2+2c+1$ thus $m=(c+1)^2-c^2$.
Therefore: If an integer is odd, then it is the difference of the squares for two integers.
$$\def\fitch#1#2{\begin{array}{|l}#1 \\\hline #2\end{array}}
\fitch{}{\fitch{[m]}{\fitch{\exists k~(m=2k+1)}{\fitch{[b]~m=2b+1}{\fitch{[a]~ b+1}{a^2=b^2+2b+1\\a^2=b^2+m\\m=a^2-b^2\\\exists l~(m=a^2-l^2)\\\exists k~\exists l~(m=k^2-l^2)}\\\exists k~\exists l~(m=k^2-l^2)}\\\exists k~\exists l~(m=k^2-l^2)}\\\exists k~(m=2k+1)\to\exists k~\exists l~(m=k^2-l^2)}\\\forall n~(\exists k~(n=2k+1)\to\exists k~\exists l~(n=k^2-l^2))}$$
Time out ... that's enough for now ... maybe more to come later ...
Best Answer
Why doesn't it seem right?
Take, for example, the statement
In this statement, $A$ is "wall $x$ is red", and $B$ is "this room is red".
then $\neg B\implies\exists x: \neg A$ is equivalent to the statement
which is sounds right, doesn't it?
Or, in your assertion, you are trying to prove that if $x\cdot y=0$ for all $x\in\mathbb R^n$, then $y=0$. Well, in this case, $A$ is "$\forall x: x\cdot y=0$, and $B$ is $y=0$.
The statement $\neg B\implies \exists x:\neg A$ is then
This statement is indeed true, and easily shown by taking $x=y$.