I am still better trying to understand the first order Peano Axioms and their relation to the standard model. Just for reference, here are the axioms I work with:
$1.\space \forall x (\neg x+1=0)\hspace{2.14cm} 4.\space\forall x\forall y(x+1=y+1 \rightarrow x=y)\\ 2.\space\forall x(x+0=x) \hspace{2.41cm} 5.\space\forall x\forall y(x+(y+1)=(x+y)+1)\\ 3. \space \forall x(x\times0=0)\hspace{2.41cm} 6. \space \forall x\forall y (x\times(y+1) = (x\times y)+x)\\ $
As well as the axiom schema of infinite, but countable axioms for induction:
$$7. \space\forall x_1...\forall x_n(\varphi[0/y]\land \forall y( \varphi\rightarrow \varphi[y+1/y]))\rightarrow \forall y\varphi)$$
Now, for correctness to hold, whatever is deduced from these axioms, must hold in every interpretation. But, what I find weird is, it seems these axioms have already defined the function symbols and constants to be equivalent to the structure of $\mathfrak N$, ie. $\{+,\times,0,1\}$, instead of having undefined $f_1,f_2,c_1,c_2$, so as I understand it the mappings are already assigned. How is this allowed, since clearly that's just one interpretation of the functions/constants, while the deduction should apply to every interpretation?
Further if that's the case, do the different possible models of PA concern themselves only with the domain $A$ of the model? I read that there are non-standard models of PA for every cardinality, so what would a model with cardinality of one look like?
Any examples/sources for FO Peano deductions are of course also welcome.