Modern statements of Gödel's incompleteness theorems are usually in terms of first-order predicate logic. However, I've often read the claim that they extend to arbitrary formal systems that can prove basic propositions about numbers. Indeed, according to Wikipedia, the original theorems referred to the type theory of Principia Mathematica, which is apparently not based on predicate logic.

My two questions are:

 1. What is the most general concept/definition of a formal system for which Gödel's theorems have been stated?
 2. How does their proof differ from the predicate logic variant?

Regarding 1., I could imagine several equally general definitions, for example based on either strings of symbols or abstract syntax trees. Being a little biased, I actually think of formal systems as data structures of more or less arbitrary computer programs, so maybe there is a definition based on Turing machines... In any case, it would need to specify what a "proof" of a "theorem" is, but I would like to do without the concept of "axioms." (See also https://mathoverflow.net/questions/29774/derivation-rules-and-godel-theorem/29989#29989.)

Regarding 2., I'm specifically thinking about the diagonal lemma (or arithmetic fixed-point theorem, or whatever it is really called). The version I know refers to a "formula with one free variable," but that presupposes such concepts as "formula" and "free variable" in the formal system, and I'm wondering how to generalize that to arbitrary formal systems. I know there are proofs of the first incompleteness theorem which take an entirely different route, but AFAIK they don't carry over to the second incompleteness theorem.

I would like to add that I don't doubt the generality of Gödel's incompleteness theorems in any way. I just feel there is a gap between their claimed general nature and the way they are usually presented. A year ago, I devised a nonstandard formal system for a proof assistant. Although it could easily formalize its own concepts and express its own consistency, a translation of Gödel's incompleteness theorems from predicate logic turned out to be surprisingly nontrivial.