Theorem 2 prove that the natural number x is not equal to his successor, in this way all the elements of {1,2,3,...,n} are different one to each other, but I can't undestand how this implies that {1,2,3,...,n} is finite.

n is the cardinality of the set {1, 2, ..., n}.

A set is finite if its cardinality is finite.

This is my interpretation.

What is your definition of finite set?

My definition are:
1) a set X is a infinite iff there exists a bijective function f:X->Y where Y is a subset of X with Y not equal to X and Y not equal to empty set
2) a set X is finte iff it isn't infinite

Now I would like to prove that {x in N | 0<=x<=n} is a finite set, with "n" natural number, using the definition 1) and 2), or using Peano's axioms. But I think that use Peano's axiom with cardinality saying that "n" is the cardinality of set {x in N | 0<=x<=n} is tautological.

Let M be the subset of N = {1, 2, ...} that consists of n for which N_n is finite.

0 belongs to M because the empty set has no proper subsets at all. Assume m is in M and prove that so is m+1. (Or you can start with {1} which also has no proper subsets.)

Let there be a bijection f from N_m+1 onto a subset S. Order the elements of S and define a permutation g that yields this reordering. The composition of f and g, call it F, is an order preserving bijection from N_m+1 onto its proper subset S.

S may or may not contain m+1. If it does not, define a subset T of N_n that contains all the elements of the latter that are larger than all the elements of S. T has a smallest element t. But then t-1 is in S and is its largest element. For, if there was s in S with s > t-1 we would have, by the definition of t and from s being an element of S, t > s, implying the existence of an integer between t-1 and t, in contradiction to Peano's axioms.

So, S has a largest element u. Swap u and m+1 to obtain a proper subset S' of N_m+1 with a bijection F' that takes m+1 to m+1.

To sum up, either a bijection from N_m+1 onto a subset has the property of mapping m+1 onto itself, or it may be converted to one with this property.

By removing m+1 from both N_m+1 and its bijective image we get a bijection of N_m on its proper subset which contradicts the selection of m.

The induction is complete.

Forgive me but I stuck at this point. How can we prove that the existence of a natural number "s" such that "t-1<s<t" contradicts the Peano's Axioms?

P.S.
Forgive me for so long time that I used to answer.

All natural number are obtained from 1 through the successor operations. Furthermore, n' > n. Thus they are obtained in an increasing sequence. So, it must be true that there are no numbers between n and n', or so I would expect.

There is Skolem's theorem about non-standard models which claims existence of innumerable sets that satisfy Peano's axioms. It looks like the notion of finiteness differs from the intuitive (customary) one. So, perhaps, my reasoning is faulty, after all.