Finding the Perfect Substitution

While we were looking at the form structure when finding proof, I noticed that I had no recollection whatsoever on how to do it. I remember, while studying number theory, that there were some neat tricks on how to prove a certain expression for n and then n + 1, and finally for n + k. In essence, we are finding proof here of a single expression, but when we have to related expressions, the dynamics are a bit different, so here we will now focus on a postulate that involves two expressions and the way to tackle this problem, as well as finding the perfect substitution to get our desired result.

If we were to use the example:

∀ x ∈ Z, ∃ y ∈ Z, x = y + 1 ⇒ ∃ z ∈ Z, x^2 = z + 1

We would have the following steps for establishing the proof:

        Assume ∀ x ∈ Z # domain assumption

                Assume ∃ y ∈ Z, x = y + 1 # antecedent 

                        Let y' be a value that depends on x... # some value that depends on x 

                        Then, y' ∈ Z 

                        Let z' = y^2 + 2y
                        Then, z' ∈ Z
                        If x^2 = (y' + 1)^2 = y'^2 + 2y' + 1 and z' = y^2 + 2y
                        Then, x^2 = z' + 1

                Then ∃ z ∈ Z, x^2 = z + 1 # introducing ∃
        Then ∀ x ∈ Z, ∃ y ∈ Z, x = y + 1 ⇒ ∃ z ∈ Z, x^2 = z + 1

Let us focus now on the bold part. How did we find it? Easy: we knew where we wanted to go. If we are going from x to x^2, then we know that the expression on the left will be squared. Rearrange things a little bit, and voila!