T S Bailey said:
Are there possibly larger logical systems than us for which we cannot derive Godels theorem?
Possibly. Godel's Theorem applies only to logical languages that are 'countable' and 'reasonable', where the latter has a specific technical meaning. So it is conceivable that there are uncountable languages (languages with an uncountable number of symbols) and if so it would not apply to them. Personally, I find it difficult to imagine an uncountable language, but that doesn't make them impossible.
If we restrict ourselves to countable, reasonable languages then the only languages for which we could not prove the theorem would be those that are in some loose sense too 'large' for any human or computer to deal with them. In practice we can prove it for any language we wish to use. If we want to then prove it for the language we used to prove that, we only need a slightly larger language. But if we iterate that a billion billion times, processing power for the formal theorem-proving might become an issue.
It's a while since I worked on Godel but my vague memory is that one of the issues preventing self-referentiality is that for the theorem - which on its own is just a bunch of symbols that obey certain rules - to
mean anything it must have a
semantic interpretation, which is a mapping from the symbols used in the theorem to the things they are talking about. In this case the things they are talking about are symbols in a logical language. If that's a logical language that is a proper subset of the language used to prove the theorem, there's no problem. Every symbol of the object language is the interpretation of a
constant symbol in the proof language that maps to it. Then there are additional symbols in the proof language (like ##\forall, \exists, \to, x, y##) that are used to prove things about those constants. That means that there will be two versions of some symbols. For instance, presuming the object language to contain the logical symbol ##\to##, the proof language must contain a constant symbol, say ##\to^\dagger## that refers to that symbol as an object in the object language, as well as a symbol ##\to## that has the usual meaning in the proof language.
It follows from this that the proof cannot refer to the language in which it is written, as its alphabet must be strictly larger than the alphabet of the language to which it refers.