What are the axioms required for a formal system to be able to state the Diagonal Lemma or Fixed Point Theorem? If possible, could you please also relate with the following systems, if it applies to them and/or if they are able to state it:
- ZF Set Theory
- Robinson Arithmetic
- First Order Logic
- Peano Arithmetic
- Primitive recursive arithmetic
The requirement is usually stated as: the theory is able to represent all the computable functions. In reality, the theory only needs to be able to represent the particular computable functions that are used in the proof. Usually, the easiest way to show that a particular theory is able to represent these particular functions is to show that it represents all computable functions, which is why there is no real loss in stating the requirement that way.
Of the theories listed in the question, all but "first order logic" meet this requirement. All of these include or interpret Robinson arithmetic, which was specifically designed to be able to represent all computable functions.
"First order logic" is not really a theory. In particular, it does not have a fixed signature, and if the signature is not right then there is no hope of even being able to state the diagonal lemma. Even if the signature is OK, there still need to be some axioms to ensure that every computable function is representable. But Robinson Arithmetic has very few axioms, and so it does not take much.