Theories can be be represented recursion-theoretically by an encoding of the language as natural numbers (most simply, a bijective encoding, which I assume), and a Turing machine accepts all and only theorems. Theories defined in terms of a Hilbert system will then be either recursive or partial-recursive sets.

It's easy to formalise the idea of such a language having a provability predicate: it's a predicate with a free variable for which the instantiation of that formula with each natural number is accepted iff the formula corresponding to that number is accepted. Theories that have such a predicate are self-descriptive. If you can formalise a substitution operator, you can diagonalise on this predicate. You get four interesting classes (among others) of theory:

1. For inconsistent theories, any predicate will do as a self-description predicate (always accept), and any binary function will do as a substitution function;
2. Regular completeable theories are not self-descriptive;
3. Self-verifying theories have self-description operators, but not substitution operators, and accept the sentence asserting their own consistency;
4. Goedel-incomplete theories have both self-description operators and substitution operators, and do not accept the sentence asserting their inconsistency.

Observe that these definitions are generalisable in an important sense: you can extend to notions of hypercomputation, by using oracle Turing machines, allowing "theories" that are sets that are not recursive or partial recursive. The treatment can be generalised in other ways, such as to the second-order concept of mass problems, which is where I learned about this way of looking at incompleteness.

Note though, that the formalisation here of self-descriptive, susbtitution function, and consistency sentence are still dependent on the language of predicate logic. Loking at provability logic might offer a way to generalise this still further.

Theories can be be represented recursion-theoretically by an encoding of the language as natural numbers (most simply, a bijective encoding, which I assume), and a Turing machine that accepts all and only theorems. Theories defined in terms of a Hilbert system will then be either recursive or partial-recursive sets.

It's easy to formalise the idea of such a language having a provability predicate: it's a predicate with a free variable for which the instantiation of that formula with each natural number is accepted iff the formula corresponding to that number is accepted. Theories that have such a predicate are self-descriptive. If you can formalise a substitution operator, you can diagonalise on this predicate. You get four interesting classes (among others) of theory:

1. For inconsistent theories, any predicate will do as a self-description predicate (always accept), and any binary function will do as a substitution function;
2. Regular completeable theories are not self-descriptive;
3. Self-verifying theories have self-description operators, but not substitution operators, and accept the sentence asserting their own consistency;
4. Goedel-incomplete theories have both self-description operators and substitution operators, and do not accept the sentences asserting their consistency and inconsistency.

Observe that these definitions are generalisable in an important sense: you can extend to notions of hypercomputation, by using oracle Turing machines, allowing "theories" that are sets that are not recursive or partial recursive. The treatment can be generalised in other ways, such as to the second-order concept of mass problems, which is where I learned about this way of looking at incompleteness.

Note though, that the formalisation here of self-descriptive, susbtitution function, and consistency sentence are still dependent on the language of predicate logic. Loking at provability logic might offer a way to generalise this still further.