Beth definability
Encyclopedia
In mathematical logic
, Beth definability states that if for any two models A, B of a first-order theory T in the language L' ⊇ L with A|L = B|L (where A|L is the reduct of A to L) it is satisfied A ⊨ φ[a] if and only if B ⊨ φ[a] for φ a formula
in L' and for all tuples a of A, then φ is equivalent modulo T to a formula ψ in L.
Informally this states that implicit definability implies explicit definability. 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 existing any L-formula ψ equivalent to φ modulo T.
The result was first proven by Evert Willem Beth
.
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, Beth definability states that if for any two models A, B of a first-order theory T in the language L' ⊇ L with A|L = B|L (where A|L is the reduct of A to L) it is satisfied A ⊨ φ[a] if and only if B ⊨ φ[a] for φ a formula
Formula
In mathematics, a formula is an entity constructed using the symbols and formation rules of a given logical language....
in L' and for all tuples a of A, then φ is equivalent modulo T to a formula ψ in L.
Informally this states that implicit definability implies explicit definability. 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 existing any L-formula ψ equivalent to φ modulo T.
The result was first proven by Evert Willem Beth
Evert Willem Beth
Evert Willem Beth was a Dutch philosopher and logician, whose work principally concerned the foundations of mathematics.- Biography :...
.
Sources
- Hodges W. A Shorter Model Theory. Cambridge University Press, 1997.