Is there an error in this textbook about Peano Arithmetic?

Question

I encountered this doubt in an online intro-logic open course offered by Stanford Uni.

Under the section 9.4 of this textbook here: http://logic.stanford.edu/intrologic/secondary/notes/chapter_09.html

It says:

The axioms shown here define the same relation in terms of 0 and s.(where the functional constant letter s below represents the successor function, e.g. s(0)=1, s(1)=2, s(2)=3 )

∀x.same(x,x)

∀x.(¬same(0,s(x)) ∧ ¬same(s(x),0))

∀x.∀y.(¬same(x,y) ⇒ ¬same(s(x),s(y)))

As my understanding, :

The first sentence says two identical numbers are same. The second and third sentences are used to define what is not same.

The second says no successor of any number is same to 0.

The third says if two numbers are not the same, then their successors are not same. For example, if 1≠3, then 2≠4.

However, I think the third sentence should be bi-conditional because, if I'm not wrong, the definition didn't cover the instance where the number being testified are smaller than the given number,otherwise it is possible to say if 2≠4, then 1=3.

So I wondered is this an error in text book or there's something wrong of my reasoning.

Answer 1

There is no error here. The book is asserting that these axioms are enough to determine whether any two particular natural numbers (of the form $s(s(\dots (s(0))\dots))$) are the same, as it explains after stating the definition. It is not attempting to write down every single true statement about the "same" relation. It is indeed true that the reverse implication of the third axiom holds for natural numbers, but it is not necessary to include this in the axiomatization in order to be able to determine whether any two particular natural numbers are the same. Failing to include this reverse implication as an axiom doesn't mean they are claiming it isn't true; it just means that they don't need it as an assumption.

Answer 2

Edit: I actually read more of the source and see now that the author addressed this three paragraphs later

" Viewed the other way around, to see that two non-identical terms are not the same, we just strip away occurrences of s from each term till one of the two terms becomes 0 and the other one is not 0. By the second axiom, these are not the same, and so the original terms are not the same."

==== here's my much longer take===

The condition is intentionaly one directional for sufficiency.

You will never need to deduce $\lnot same (1,3) $ from $\lnot same (2,4) $ because the only way you will ever know that $\lnot same (2,4)$ in the first place is by deducing it from knowing $\lnot same (1,3) $ previously.

And the only way we'd know $\lnot same (1,3) $ previously is if we knew $\lnot same (0,2)$ even earlier.

Which we would have by Axiom 2: $\lnot same (0,s (s (0))=2) $.

We will simply never need the other direction because we can deduce everything from one direction only.

====

Or put another way. From these three axioms We can prove:

Theorem: if $s (y') =y$ and $s (x')=x $ then $same(x,y) \iff same (x',y') $

Proof: if $\lnot same(x',y') $ then $\lnot same (x,y) $ by axiom 3.

If $same (x',y') $:

If $x'$ or $y'$ is 0 then both are 0 because otherwise $same (x',y') $ would violate axiom 2. If both are 0 then x and y are both $s (0)$ are 1, and by axiom 1 $same (s (0),s (0)) $ and we'd be done.

If neither $x'$ or $y'$ are 0 there are $x''$ and $y''$ such that $s (x'') $ is $x'$ and $s (y'') $ is $y $. In which case we can repeat the argument until we determine that $x'$ and $y'$ are both $s (s(s (.....(0).....))) $ and so $x $ and $y $ are both the successor to that.

And so by axiom 1, $same (x,y) $ and we are done.

Moral: bidirectional should be a theorem. Not an axiom.