I am trying to prove the integer square root theorem $\forall x: \mathbb{N}, \exists y : \mathbb{N}((y^2 \leq x) \land (x < (y+1)^2))$ for $\lfloor \sqrt{x} \rfloor$. In words: for any natural number $x$, there exists a natural number $y$ which is the integer part of the square root of $x$. I would like to use proof by induction in the Fitch system. The outline of proof is based on and Kreitz and goes as follows:
Show that the predicate holds for the base case $x=0$
Assume the predicate holds for some arbitrary $x=k$
Prove the predicate holds for $x=k+1$
- Case 1: If the new number $k+1$ is less than the $k^{th}$ root plus one squared then let the $k^{th}$ root be a witness. That is if $(k+1)<(\lfloor \sqrt{k}\rfloor+1)^2$ then $\lfloor\sqrt{k}\rfloor$
- Case 2: If the new number $k+1$ is is greater or equal to the $k^{th}$ root plus one squared then the witness is $(\lfloor\sqrt{x}\rfloor + 1)$. That is if $(k+1) \geq (\lfloor\sqrt{k}\rfloor+1)^2$ then $(\lfloor\sqrt{k}\rfloor + 1)$.
Below is my flawed attempt at the proof using the Fitch software. I am trying to follow the outline proof above. The lemmas are taken to be theorems from arithmetic. As can be seen the attempt ends universals only. I do not know how to prove the theorem with the existential quantifier. Assuming that my interpretation of the original outline is correct, what Fitch specific strategies do I need that will help me provide a correct proof?
I have taken the hints in the comments. I think the proof is OK,
The most important thing you need to do here is to state the theorem in logic ... you never did this!
I suggest:
$$\forall x \exists y ((y * y < x \lor y * y = x) \land x < s(y) * s(y))$$
In here, $s(y)$ is the successor function as applied to $y$, i.e. $s(y) = y + 1$
It is typical to use $s(x)$ instead of $x+1$ when formalizing the natural numbers. The Peano Axioms for Arithmetic, for example, are typically stated in terms of this successor function.
Now, it looks like you're using a fairly old version of Fitch. The newer version of Fitch has a built-in rule for doing inductive proofs, called 'Peano Induction'. So, with that, the basic set-up for your proof is:
And, to deal with that existential you have for the Inductive Hypothesis, use Existential Elimination:
OK, now you can nicely use Trichotomy (a very basic and general law) to separate between the two cases as indicated in the mathematical proof by Kreitz:
The rest is basic arithmetic ... though I would suggest the following Lemma's that are just a little less specific than the ones you were going to use:
$$\forall x \ x * 0 = 0 $$
This is one of the Peano axioms of arithmetic .. you'll need it to prove the base case
$$\forall x \forall y (x < s(y) \leftrightarrow (x < y \lor x = y))$$
This is a basic lemma. If you wanted to, you can derive it from the Peano Axioms together with a definition of $<$ such as:
$$\forall x \forall y (x < y \leftrightarrow \exists z \ y = x + s(z))$$
Finally, two basic Lemma's that are also fairly easily derived from the Peano Axioms:
$$\forall x \ x * x < s(x) * s(x)$$
$$\forall x \forall y ( x < y * y \rightarrow s(x) < s(y) * s(y))$$
OK, so add those to your proof as Lemma's, and you should be able to complete the proof. Good luck!