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?

First attempt using Fitch

I have taken the hints in the comments. I think the proof is OK,

enter image description here

  • 1
    $\begingroup$ The lemma's are not very general ... strangely specific to the problem at hand ... were these given to you? Also, I know Fitch has a built-in Induction rule ... are you supposed to use that? If not, are you at least given the relevant instance of the Inductin scheme as a premise? $\endgroup$ – Bram28 Aug 25 '18 at 19:29
  • 1
    $\begingroup$ Yeah, upgrade Fitch if you can, but even if you cannot, try and express the base, hypothesis, and step ... and even more importantly, the theorem! Let me know if you need help. $\endgroup$ – Bram28 Aug 25 '18 at 21:07
  • 1
    $\begingroup$ @Bram28 Thanks for very detail help. It is much appreciated. I updated to Fitch 3.7 and uploaded another attempt. $\endgroup$ – Patrick Browne Aug 27 '18 at 13:57
  • 1
    $\begingroup$ OK, good! ... still not a fan of your premises. Premise 1 has no free variable $x$ so the quantifier is doing no work. Make it $\forall x \ x * 0 = 0$: standard Peano axiom! Instantiate it to get $0*0=0$. Also, the second one is a little more general as $\forall x \ x * x < s(x) * s(x)$. You can instantiate that to get 0 * 0 < s(0) * s(0), and since you have $0*0=0$ you can use $= \ Elim$ to get $0 < s(0) * s(0)$, which is what you really want. Your third premise is really weird ... use the last statement from my Post. And, you still need to add Trichotomy! $\endgroup$ – Bram28 Aug 27 '18 at 17:58
  • 1
    $\begingroup$ Also, your line 9 says 'Case 1', but your line 9 is the inductive hypothesis. The two cases come later on in the proof, when you are setting up the Proof by Cases using $\lor \ Elim$ $\endgroup$ – Bram28 Aug 27 '18 at 17:59

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:

enter image description here

And, to deal with that existential you have for the Inductive Hypothesis, use Existential Elimination:

enter image description here

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:

enter image description here

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!


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.