A set $S$ is called finite if there exists a bijection from $S$ to $\{1,...,n\}$ for one $n \in \mathbf{N}$. It is then common to write its elements as $s_1,...,s_n$. I now wonder, why this is possible/rigorous or if this is informal and in the latter case, how to formalize this. I guess that $\{1,...,n\}$ is also informal and if one wants to write this set down more formally one could write it as $\{k \in \mathbf{N} : k \leq n\}$. I understand that the idea is to start by $1$ and then applying the successor until one reaches $n$, meaning for $n=1$ one has $s_1$, for $n=2$ one has $s_1,s_2$ and so on as its elements. This makes sense intuitively, but is just that for now, an intuition. Since $n$ is not an explicit number, I am not really sure why it is possible to write something like $s_1,...,s_n$. Is this formalized by something like $\{s_i : i \leq n\}$ where $s_i$ is defined to be the image of $i$ under this bijection? If this is one way to do it, I think this makes sense.
Furthermore I wondered about the following: Let $n \in \mathbf{N}$, then $n$ can be obtained by applying the successor $s$ to $0$ a finite amount of times. However, in order to do this, one would have to define what finite means beforehand, right? Since this result follows from the Peano-axioms, is the procedure to first state the axioms, then give an example construction of $\mathbf{N}$ by using the intersection of induction sets, then defining finite as above, where $\mathbf{N}$ is the constructed set and then prove the property about the successor afterwards? The question arises since this is not the way it is done in the document I read, which is: https://www.math.wustl.edu/~freiwald/310peanof.pdf
The result I mentioned can be found on page $4$, where finiteness has not been defined previously.
For your first question: Yes, this is one way to do it. It could also have been something such as an abbreviation for union of pairs. If you are working on ZF or some similar system, it is possible to do that, so we don’t bother writing its lengthy and pointless ‘original’ definition.
For your second question, I think what the author mean by ‘finite’ is finiteness in metalanguage. That is, in principle, a natural is obtained by apply $s$ to $0$ several times. If you would like to formalize this fact in a set-theoretic background, it is okay to argue that a finite set is something bijective to a set-theoretic natural number, and that theorem says a Peano number has a property related to that idea. But keep in mind that we are doing so in the metalanguage, so these facts are proved a priori: finiteness is defined before introducing and working on Peano axioms. This avoids the vicious circle of definitions.