Gödel Incompleteness Theorem - Primitive Recursive Functions

I'm currently studying Gödel's Incompleteness Theorem and I am in doubt about his use of primitive recursive functions.

To study it, i'm in the point of view of a system of predicate logic with the theory of Peano Arithmetic. That predicate logic has the extensions of equality (symbol $=$ defined) and function symbols.

1) In Gödel's proof he defines in some point the primitive recursive functions. Those definitions are necessary even if i'm using the function symbols extensions for predicate logic? The function symbols already offer an way of composing functions. An function $f \in F$ has the form of $f(t_1, t_2, \dotsc, t_n)$ where $t_n$ is any term of the logical system. But a function $f$ represents a term too. So we can compose functions like in $f(g(x))$ where $t_1=g(x)$. I don't see where the primitive recursion rule would give some benefit.

2) Another doubt is whether the primitive recursive functions is in the syntax domain or in the semantics domain. If in the semantic domain, how can I use expressions from inside the logical system? For example, in defining those functions i use the concepts $\forall$, $\exists$, $\land$ and the like.

3) At some point in the proof, he introduces the representability concept. It afirms that any definable relation can be expressed as a formula of the system. Why is this used for?

-
Representability shows that (among others) the primitive recursive functions have analogues within the system. This is part of what makes it possible for the system to "talk about itself" (via indexing). –  André Nicolas May 25 '12 at 14:46

(2) If you're reading Gödel's original paper, he's certainly defining the primitive recursive functions as semantic objects at first -- it's only much later in the paper that he shows they can be expressed in a particular formal system.

(1) The point of defining primitive recursive functions is not to give you a new way of making functions. It is to name a certain subset of all the functions you already have, namely the functions that happen to be definable using the rules for p.r. functions and nothing else. These particular functions are going to have some nice properties ...

(3) ... in particular they are all representable in the formal system we're reasoning about, in the sense that for each p.r. function there's a fixed logical formula that you can plug numerals into, and the result will be a provable or disprovable according to whether the numerals you plug in represent a correct set of inputs and corresponding output to your p.r. function.

You're right in observing that it is not very exciting that the representable functions are closed under function composition -- that is not particular to PA, and can be proved for about any reasonable first-order theory. But it is interesting and nontrivial that the primitive recursion rule does not take us outside the space of Peano-Arithmetic representible functions. You cannot prove that for first-order theories in general -- for example it is not true for Presburger Arithmetic (which has addition but not multiplication as a primitive notion).

What this is used for is to connect "correct proof" at the metalevel with a property in the formal system. Gödel proves that "$x$ is (the Gödel number of) a valid proof of formula $y$" is a primitive recursive property, and therefore there is a formula in the system itself that is provable exactly when you plug in numerals for Gödel numbers of valid proofs. This is the core of the construction of an undecidable sentence.

-
The representability concept affirms that we can represent relations of the semantic domain as functions within the formal system. Then, primitive recursive functions can be reduced to relations? And, in defining the p.r. functions he uses logical operators that i thought were available only inside the logical system. So, the domain of the formal system is arithmetic plus something else that enables the use of logical operators? –  felipegf May 25 '12 at 16:14
"Logical operators that [I] thought were available only inside the logical system"??? The operators of formal logic model intuitive mathematical concepts that exist outside of, and prior to, any formal systems. –  Henning Makholm May 29 '12 at 20:11