I apologize in advance if this seems like a silly question - I have absolutely no experience in this branch of math.
So, let's define a 'programming language' that starts out with an empty string $s$ and can do the following:
- Receive inputs $a$ and $b$
- Loop, either a set number of times, $a$ times or $b$ times
- Append any letter to that string
- Output the number of letters in s.
Now, it is obvious that you can add and multiply numbers in this language, but what if it wasn't? What if we had a more complex set of rules or more complex goal such that intuition couldn't tell us whether the goal was possible or not? How could we mathematically prove that something in that language was possible or not possible?
Simply speaking, how, mathematically, given a language with a set of rules and functions, can you see if something is possible or not?
To show that something is possible, we normally just describe a program in the appropriate system to do it.
There are at least two ways to show that something is not possible. The first is the method of diagonalization. This is used to show the uncomputability of the halting problem, the uncomputability of the Busy Beaver function, and similarly the uncomputability of many other functions.
The second method is by finding an external characterization of the functions in a particular system, and then showing that the function we have in mind does not meet that characterization. That shows the function we have in mind cannot be constructed in that system. This method is used, for example, to show that Goodstein's theorem is not provable in Peano Arithmetic, and therefore the associated function is not provably total in Peano Arithmetic, although it is a total computable function in the ordinary sense.
For an example of the second technique, consider the formal system in the question. We can prove that for each particular program $P$ in that system there is a polynomial $q_P(n,m)$ so that output number $P(a,b)$ is $q_P(|a|, |b|)$. Thus the function that takes $a$ and $b$ and returns the number ${|a|}^{|b|}$ is not computable using the system in the question, because the function $n^m$ is a polynomial of $n$ and $m$.
Proof of the characterization. The proof of the polynomial characterization is by induction on the structure of the program. It may seem surprising because the language is not much different from LOOP, and LOOP is able to compute all primitive recursive functions. But the system here is different enough.
The basic operation of the program is to append a single letter to the output string $s$, which is to say add 1 to the length of the output string. The strings $a$ and $b$ don't change, the output string never gets shorter, and loops run either a constant number of times, $|a|$ times, or $|b|$ times.
We need to check three programming constructs: concatenation, appending a single letter to $s$, and looping.
If we concatenate two programs $P_1$ and $P_2$ to make a program $P$, the work done by $P_1$ will not affect $P_2$. We can ignore the fact that $s$ will not start out empty when $P_2$ runs, which also will not affect $P_2$. Thus we will have $q_{P}(n.m) = q_{P_1}(n,m) + q_{P_2}(n,m)$.
The program that appends a single letter to $s$ has polynomial $q(n,m) = 1$.
Finally, suppose that we have a program $P$ which we wrap in a loop to make a larger program. We want to show there is a polynomial $q(n,m)$ for the new program. According to the rules for our system. each iteration of the loop will append the same number of letters to $s$; there is no way for the program to change how many letters are appended on each iteration. So we just need to multiply by the number of iterations. If the loop runs $|a|$ times, we can take $q(n,m) = n\cdot q_P(n,m)$. If the loop runs $|b|$ times, we can take $q(n,m) = m\cdot q_P(n,m)$. If the program runs a constant number of times, $c$, we can take $q(n,m) = c \cdot q_P(n,m)$.