An Intuitive Walkthrough of PA as a formal system
*Peano Arithmetic are a set of axioms in first order logic that describe how arithmetic of the natural numbers works. A first order formal language is a collection of variables, constants, logical symbols (such as negation, conjunction, etc.), parentheses, function letters, and predicate letters. Function letters represent functions that take some amount of variables and or constants and map them to another variable or constant. Predicates are similar, however they map to truth values. An obvious example of the difference between functions and predicates from mathematics is the difference between "addition" which is a function and "less than" which is a predicate. Remember that when we are starting out with a formal language we are starting out with syntax, the symbols don't have interpretations yet, that's what the semantics of model theory is for. Functions in this form, without the semantics, are just things that take one symbol and map them to another. When we introduce interpretations, thats when we have actual numbers being mapped to other numbers.
In the Principia Mathematica Bertrand Russell found that it is perfectly fine to replace functions with predicates. This is referred to as "function elimination." As an example consider this pair:
F(x,y): z where x,y,z, are variables or constants in a formal language, and F is a 2-place function that maps x and y to z.
G(x,y,z,): True, False where x,y,z, are variables or constants in a formal language, and G is a 3-place predicate that maps x, y, and z to a truth value.
If we give an interpretation for F and G that describe the concept of addition, then we would say
F(1,1): 2
G(1,1,2): True
So, because it is logically equivalent, you can view functions as something that maps variables and or constants to variables and or constants or you can view them as predicates that map variables and or constants to truth values. The next thing to understand are interpretations and model theory. Remember that a model of a set of axioms is a pair of sets (D,I). D is the domain of the model and I is the function that maps members of the domain to the variables, functions, constants, and predicates of the formal language. This is the formal language interfacing of semantics and syntax.
In a minimal form of PA we have variables, one constant "a", one 1-place function "F(x)", and one 2-place predicate "P(x,y)". "a" is the constant which when we give it an interpretation will become the number 0. "F(x)" is a function that will take a variable, or the constant, and map it to another variable, which when we give it an interpretation will become the "successor" function, which maps a number to its immediate successor. "P(x,y)" is a predicate that takes two variables or the constant and maps them to a truth value. When we give P an interpretation it will become the identity function, or "=", and will map to a True truth value if and only if x and y are the same.
Peano Arithmetic is made up out of a bunch of variables, one constant, one function, and one predicate. When we give it an interpretation (the natural numbers and our understanding of zero, successor, and equality) we are then presented with a system that works the same way that arithmetic works. Note the idea of composition of functions as well. The successor of 0 is 1, the successor of 1 is 2 and so on. We can come up with a new function, "A(x,y)", which starts at x and applies the successor function to "x" "y" times. This, of course, is a recursive definition of addition. Recursive definitions can be created for multiplication and exponentiation in the same way. Note that you don't need to introduce addition, multiplication, or exponentiation to get arithmetic. Those functions can just be viewed as "short hand" for successive application of the successor function.
Finally, remember that I said before that Russell showed us we can eliminate n-place functions and reintroduce n+1-predicates in their place. To do this with the successor function we would create a new predicate, S(x,y) that maps to a True truth value if y is the successor of x. Consider these two examples:
F(0):1
S(0,1): True
So, functions are viewed as a mapping from symbols to symbols. Once they are given an interpretation they make meaningful statements about actual numbers. Russell showed us that it is logically equivalent to replace functions with predicates that map to a truth value instead of a variable. Both of these are logically equivalent ways of thinking about the formal language.
The successor function is what is referred to as a primitive recursive function. These are a set of functions that are crucially important in the foundations of mathematics and computer science. You might be interested in reading on their history and why they are considered to be "primitive" or "irreducible" functions that are used to compose more complex functions.
*As a reference I have been using Introduction to Mathematical Logic, Sixth Edition (Discrete Mathematics and Its Applications) by Elliott Mendelson.
Answers to the subquestions of the question
(1) What are functions in the Peano axioms?
(2) How do I know that functions in PA exist?
(3) Does the PA concept of a function also have the form of a bijection between sets?
The answer to (1) and additionally (3) is that they are mappings of symbols to symbols before semantics. It maps numbers to numbers after semantics are introduced via a model. Regrettably I think I could do a better job of showing this if I was able to use super scripts and subscripts however Phil.SE does not allow for mathjax. The only function in a minimalist program of PA is the successor function. The successor function takes a symbol and maps it to another symbol and with an interpretation it maps a number to another number. The domain of the successor function is every variable and constant in the language, which with an interpretation correspond to all of the natural numbers. Likewise, the range is the set of natural numbers, excluding zero because zero is defined as not being the successor of any natural number. So the range of the successor function is a subset of the domain, it is the domain without zero.
What does this mean if we eliminate the function and replace it with a predicate? The successor predicate maps in the exact same way except that its range is a set of truth values. S(0,x) will always map to false because zero is not the successor of any number. S(4,1) will also map to false, S(2,3) will map to true, and so on. The domain of the function is ever ordered pair (x,y) of natural numbers and the range is the set of truth values that correspond to whether or not y is the successor of x.
The answer to (2) is that PA is a formal system and formal systems have functions, or predicates or both. Remember, formal systems are just systems of logic. They are a formal syntax and semantics. We use interpretations to give them meaning outside of just a collection of symbols. Functions and predicates are an intrinsic part of logical systems so PA has them because it is a logical system.
