Consider a first-order language and a theory in that language (defining the way agent reasons, the kinds of concepts it can understand and the kinds of statements it can prove). This could be a set theory such as ZFC or a theory of arithmetic such as PA. The theory should provide sufficient tools to define recursive functions and/or other necessary concepts.

This is unclear to me, and I've read and understood Enderton. I would have thought that ZFC and PA were sets of axioms and would say nothing about how an agent reasons.

Also,

In first-order logic, all valid statements are also provable by a formal syntactic argument.

Do you mean in the context of some axioms? (of course, you can always talk about whether the statement "PA implies X" is valid, so it doesn't really matter).

I haven't read the rest yet. I'm confident that you have a very precise and formally defined idea in mind, but I'd appreciate it if you could spell out your definitions, or link to them (mathworld, wikipedia, or even some textbook).