Just trying to use some of these ideas in the writing of a proof just now and came across the weird notion that you might be able to use 0^0 in a proof even if it is "undefined!" You assume ^ is function on N -- you just don't know what value 0^0 has. So, you could prove 0^0 * 0 = 0 since x * 0 = 0 for ANY x in N. But you can't prove 0^0 = x for any x in N. This is getting really interesting!
As I said in my original posting, it can be shown (in 1038 lines in the DC Proof format) that there exists infinitely many binary functions ^ on N that have
(1) x^0 = 1 for x=/=0 (2) x^(y+1) = x^y * x
We can't determine the value of 0^0 from these equations alone, but it seems we can assume it is a natural number!