can you guys help me check the fleshed out logic of 'my' proof of the cancellation law for the natural numbers? It's in Peano's system of the natural numbers with the recursive definitions of addition and multiplication. I was trying to prove it without trichotomy and stumbled across a proof given by Mauro Allegranza here. I'm basically unsure about whether I have articulated the logic in step 19 correctly. Also, I find it kinda iffy to use the same symbol $b$ in steps 8 and 9 when articulating what $P_1(c)$ and $P_1(S(c))$ state. This is cos' when we reason about both statements simultaneously, $b$ in one statement is not equal to $b$ in another statement, but I don't know if there's a way to notate the variables elegantly with this fact in mind.
Also, $A2$ states that $0$ succeeds no number and that every number has a predecessor, $A3$ states that $a=b$ iff $S(a)=S(b)$, and positivity theorem 2 states that if $a\times b=0$, then $a=0$ or $b=0$.
By the way, it'll be nice if I can do away with invoking the concept of positivity. I just think it's more natural to talk about addition, then multiplication, and then positivity and order. Invoking positivity just messes this natural sequence up (which is why I didn't want to use trichotomy).
You are doing a really good job in trying to convey the structure of the proof. However, there are a couple of times where you don't get the interplay between the universals and the conditionals that are involved here quite right.
OK, so as the inductive step part of the inductive proof, you are trying to prove that:
where $P_1(c)$ is:
Thus, you are trying to show :
Now, I think the source of your worry is that you didn't spell out in lines 8 and 9 that the universal quantifiers for $a$ and $b$ are part and parcel of the property $P_1$. And by not doing so, it now suddenly seems as if you are trying to prove:
And yes, if that is what you are trying to show, then we have a worry: the $b$ on line 8 would have to be the same $b$ as on line 9 .. but given that on line 19 we want to pick the $b$ to be $c$ to get out desired result, how come it can then also be $S(c)$?
Well, if you spell out lines 8 and 9 more carefully, that worry will disappear:
That is, your line 8 (which expresses the inductive assumption) should be:
And your line 9 should be:
In fact, your line 10 isn;t quite right either: $P_1(c)$ is not a conditional statement ... it is a (double) universal statement. So, before line 10 you should say:
9.5 Let's pick arbitrary $a \neq 0$ and $b$. We now need to show $a * b = a * S(c) \to b = S(c)$
and then on line 10 you simply say: OK, so let's assume $a * b = a * S(c)$
OK, so now everything proceeds just fine ... until we hit line 19. So here we of course want to use the inductive hypothesis, but you don't do this right. In fact, you make two mistakes when you say "$P_1(c)$ holds for any $c$ and $b$"
First, the inductive hypothesis was made after picking an arbitrary $c$. That is: first you pick an arbitrary $c$, and then you assume, for that $c$, the inductive hypothesis $P_1(c)$. So, the inductive hypothesis is simply $P_1(c)$, and not that $\forall \ P_1(c)$. by saying that "$P_1(c)$ holds for any $c$" you seem to be saying the latter, but that's not right.
Indeed, this distinction is exactly what some people don't understand when they charge that induction is a circular proof technique. They think that the inductive hypothesis is $\forall \ P(c)$, which is exactly what the inductive proof concludes as well. But the inductive hypothesis is merely $P(x)$ after having picked an arbitrary $c$.
You second mistake is related to the 'mistake' I described at the start of the post. Since the $b$ is a universally quantified variable as part of the inductive hypothesis $P_1(c)$, it is not a free variable of $P_1(c)$, and as such it makes no sense to say that "$P_1(c)$ holds for any $b$"
Instead, you should have said: $P_1(c)$ states that for any $a \neq 0$ and any $b$ we have $a*b = a*c \to b=c$. So, let's pick $b=z$. .... and now the rest follows
So yes, overall a good job already: certainly already far more careful than many of the inductive proofs I typically get from my students. But, you need to take some more care yet, especially with those universal proofs: be more explicit at what point you introduce certain variables to be used as arbitrary objects from the domain. Indeed, at times like these I recommend trying to use a 100% formal logic proof: before that will check out, you will need to have every line exactly spelled out right ... and also have everything in the right order.