Prove $\langle \mathbb{N}, x \mapsto x +1, 1 \rangle$ is a Peano system without circular reasoning How can we show that the structure $\langle \mathbb{N}, x \mapsto x +1, 1 \rangle$ is a model of a Peano system?


*

*How can we show that it satisfies the axiom of induction? Don't we have to implicitly rely on this axiom, and thereby make our reasoning circular? And if we do, then what has the axiomatization achieved?

*For the other axioms, aren't we assuming that we've already proved some properties of the addition function? 
It would be nice if you could write a proof, since I would like to see in general how one goes about proving that a given construction is a model of some given set of axioms. I want to see the kind of language we use for such proofs.
Update: You can assume any definition of $\mathbb{N}$. I just want to see how one writes these kinds of proofs.
References:


*

*List of axioms: http://www.math.wustl.edu/~kumar/courses/310-2011/Peano.pdf
 A: Actually, you cannot give a truly non-circular 'proof' that anything is a model of PA (whether first-order or second-order Peano Arithmetic). This is because there is a fundamental circularity that we cannot avoid when building mathematics. Now the post I linked to focuses on the more specific question of whether ZFC set theory is circular, but in fact the same reasons apply to any formal system that we will ever be able to imagine or describe. The fundamental reason is simply that we can only ever handle finite sequences, and the only way we can precisely and objectively describe something to another person is by a finite sequence of symbols in a common language. Pictures do not work because they are subject to interpretation unless they are in an agreed fixed format, in which case they could easily be encoded by symbol strings anyway. The mere notion of mathematical proof involves finite sequences of symbols, hence by accepting any formal system as being meaningful, we already accept the basic properties of string manipulation, which amount to accepting the existence of a model of PA (more or less).
More specifically, you could define the successor of a string to be the result of appending a '1' to it. And then you could define the unary numbers to be all the strings that could be obtained by doing this some number of times to the empty string. Next define the sum of two unary numbers to be their concatenation, and observe that you believe commutativity of addition of unary numbers! Next define the product of two unary numbers to be the result of replacing each '1' in the first number by the whole second number. You now have two choices:


*

*Accept first-order logic plus the basic properties of unary numbers. This quite clearly gives you first-order PA. (This is not a mathematical claim per se, since the above paragraph is in natural language; how do we know it can be interpreted meaningfully? Witness Quine's and Berry's paradoxes and one possible resolution, which show that one has to be quite careful with natural language.)

*Reject first-order logic or some basic property of string manipulation. But then one has no way to describe any formal system, let alone a precise notion of mathematical proof. (If you have a way, please let the world know!)
For more on what you need as you climb further up the ladder of philosophical commitment, see this 'brief' post.
Given the above, it is necessary that any meta-system (which is the system we use to reason about formal systems) already has a notion of a collection of natural numbers that satisfy PA. Without it we cannot do much at all. We will almost certainly rely on induction in the meta-system to prove that some structure is a model of PA, just like we will have to rely on induction to prove almost every non-trivial property about formal systems. For example, if the meta-system is capable of reasoning about strings, one should be able to perform the reasoning in the second paragraph of this post in the meta-system, showing that the structure of unary numbers is a model of PA, and most likely you would also be able to prove that the unary numbers are isomorphic to the natural numbers. More precise statements can be made once you choose a meta-system, and if you learn more about various weak systems you will get a better idea of what philosophical commitments one makes in stronger systems.
A: 
How can we show that the structure $\langle \mathbb{N}, x \mapsto x +1, 1 \rangle$ is a model of a Peano system?

Not sure what you mean by a "model of a Peano system." I'm guessing you want to know how we might prove that Peano's Axioms hold on some set that we have constructed or assumed to exist. 
It can be shown that if we have an injective function $f: X \to X$ and $x_0\in X$ such for all $y\in X$, we have $f(y)\ne x_0$ then there exists a subset $N \subset X$ such that $(N,f,x_0)$ satisfies the Peano Axioms with $f$ being the successor function and $x_0$ being the "first element."  
In my formal proof (274 lines), we construct $N=\{ x_0, f(x_0), f(f(x_0)), \cdots \}$ and show that each of Peano's Axiom is indeed satsified.

  
*
  
*How can we show that it satisfies the axiom of induction? Don't we have to implicitly rely on this axiom, and thereby make our reasoning circular? And if we do, then what has the axiomatization achieved?
  

See lines 82 to 106 of my proof.  No "circular reasoning" is required.


  
*For the other axioms, aren't we assuming that we've already proved
  some properties of the addition function?
  

That is a problem. It is not obvious from your question what the author meant us to assume about the $+$ operator.
