There are three sibling theorems of logic which guarantee that such characterizations are bound to happen.

• The Craig Interpolation Theorem
• The Robinson Joint Consistency Theorem
• The Beth Definability Theorem

[The wikipedia entries need some work. I suggest you look up these theorems in a good logic book, for example Hodges's Model Theory or his more accessible Shorter Model Theory.]

I will focus on the Beth Definability Theorem, though the other two siblings lead to similar conclusions in slightly different contexts.

Suppose you have a first-order language L₀ and a larger language L. Let T be a theory in L and let φ(x) be a formula of the larger language L with the following property. Whenever A₁ and A₂ are structures of the larger language L which have the same universe A and the same interpretation for all parts of the small language L₀, then A₁ ⊧ φ(a) iff A₂ ⊧ φ(a) for all a ∈ A. Beth's Definability Theorem says that there must be a formula φ₀(x) of the smaller language L₀ such that T ⊦ ∀x(φ(x) ↔ φ₀(x)).

The connection with your question is as follows. The base language L₀ is the 'internal' language of the structures you really care about, while the larger language L has some additional 'external' data. The theory T characterizes the structures with external data that you care about, and φ(x) is a property of such structures that you are interested in. If φ(x) is sufficiently independent of the external data, then φ(x) must be equivalent to an internal formula φ₀(x).

Not all of the examples you give are easily cast into this formalism, but the basic flavor is the same. Unfortunately, the Beth Definability Theorem (and its proof) does not say much on how to find the internal formula φ₀(x) but, at least, it says that the search will not be in vain.

There are three sibling theorems of logic which guarantee that such characterizations are bound to happen.

• The Craig Interpolation Theorem
• The Robinson Joint Consistency Theorem
• The Beth Definability Theorem

[The wikipedia entries need some work. I suggest you look up these theorems in a good logic book, for example Hodges's Model Theory or his more accessible Shorter Model Theory.]

I will focus on the Beth Definability Theorem, though the other two siblings lead to similar conclusions in slightly different contexts.

Suppose you have a first-order language L₀ and a larger language L. Let T be a theory in L and let φ(x) be a formula of the larger language L with the following property. Whenever A₁ and A₂ are two models of T which have the same universe A and the same interpretation for all parts of the small language L₀, then A₁ ⊧ φ(a) iff A₂ ⊧ φ(a) for all a ∈ A. Beth's Definability Theorem says that there must be a formula φ₀(x) of the smaller language L₀ such that T ⊦ ∀x(φ(x) ↔ φ₀(x)).

The connection with your question is as follows. The base language L₀ is the 'internal' language of the structures you really care about, while the larger language L has some additional 'external' data. The theory T characterizes the structures with external data that you care about, and φ(x) is a property of such structures that you are interested in. If φ(x) is sufficiently independent of the external data, then φ(x) must be equivalent to an internal formula φ₀(x).

Not all of the examples you give are easily cast into this formalism, but the basic flavor is the same. Unfortunately, the Beth Definability Theorem (and its proof) does not say much on how to find the internal formula φ₀(x) but, at least, it says that the search will not be in vain.