Beth definability

In mathematical logic, Beth definability is a result that connects implicit definability of a property to its explicit definability, specifically the theorem states that the two senses of definability are equivalent.

Statement

The theorem states that, given a first-order theory T in the language L' ⊇ L and a formula φ in L', then the following are equivalent:

for any two models A and B of such that A|L = B|L (where A|L is the reduct of A to L), it is the case that A ⊨ φ[a] if and only if B ⊨ φ[a] (for all tuples a of A)
φ is equivalent modulo T to a formula ψ in L.

Less formally: a property is implicitly definable in a theory in language L (via introduction of a new symbol φ of an extended language L') only if that property is explicitly definable in that theory (by formula ψ in the original language L).

Clearly the converse holds as well, so that we have an equivalence between implicit and explicit definability. That is, a "property" is implicitly definable with respect to a theory if and only if it is explicitly definable.

The theorem does not hold if the condition is restricted to finite models. We may have A ⊨ φ[a] if and only if B ⊨ φ[a] for all pairs A,B of finite models without there being any L-formula ψ equivalent to φ modulo T.

The result was first proven by Evert Willem Beth.

Sources

Hodges W. A Shorter Model Theory. Cambridge University Press, 1997.

gollark: He seemed hostile to me *before* that, so who knows.

gollark: I visited jas777's house by flying a few thousand blocks there, and went inside (by breaking two cobblestone blocks, which I replaced), and then he started killing me.

gollark: I'm pretty sure I'm not.

gollark: 🇺 🇸 🇪 🇲 🇮 🇱 🇴

gollark: 🇲 🇮 🇱 🇴

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.