The new symbols extend the language, while their definitions, obtained from agent and world programs respectively by standard methods of defining recursively enumerable functions, extend the theory.

I haven't yet read beyond this point, but this is a kind of confusing thing to write. Definitions can't extend a theory, because they don't give you new theorems. My assumption is that you will add axioms that incorporate the new symbols, and the axioms will extend the theory.