I also liked the one on lambda calculus. I hope one day we will be able to find interpretation of what it actually means for PLUS Times Plus. Maybe this is how we will explore nonstandard arithmetic.
Godel's incompleteness theorem lets you turn PLUS into a number, do some operations on it, and then turn it back into a symbol. So PLUS times PLUS already has a definite answer. Perhaps not a sensible one, but a definite one.
You're talking about Gödel encoding, not Godel's incompleteness theorem.
Yes it could just simply be a syntactic sugar for a complex operation taking in 4 numbers. But this reminds me of Mirror Symmetry between two theories in String Theory where complex calculations in one theory gets mapped to simple calculation in another theory. Similarly we might have translation dictionary between standard arithmetic and non-standard arithmetic where complex calculation in standard arithmetic becomes easy calculation in non-standard arithmetic.