# Beth definability

> Mediated Wiki article. Canonical URL: https://mediated.wiki/source/Beth_definability
> Markdown URL: https://mediated.wiki/source/Beth_definability.md
> Source: https://en.wikipedia.org/wiki/Beth_definability
> Source revision: 1345422929
> License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/)

In [mathematical logic](/source/Mathematical_logic), **the Beth definability theorem** is a fundamental result in logic that states a property implicitly defined by a first-order theory has an explicit definition within that theory. This means that if a new symbol or property is uniquely determined across all models of a theory, there must be a formula using only the existing symbols of the theory that defines it. The theorem establishes an equivalence between implicit and explicit definability in classical first-order logic, linking its syntax (proofs) and semantics (models).[1]

## Statement

For first-order logic, the theorem states that, given a [theory](/source/Theory_(logic)) *T* in the [language](/source/Language_(logic)) *L'* ⊇ *L* and a [formula](/source/Formula) *φ* in *L'*, then the following are equivalent:

- for any two [models](/source/Model_(logic)) *A* and *B* of *T* such that *A*|*L* = *B*|*L* (where *A*|*L* is the [reduct](/source/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](/source/Logical_equivalence) modulo *T* to a formula *ψ* in *L*.

Less formally: a property is implicitly definable in a theory in language *L* (via a formula *φ* 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 explicitly definable with respect to a theory if and only if it is implicitly 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](/source/Evert_Willem_Beth) in a paper published in 1953.[2]

## References

1. [beth-theorem.pdf](https://www.princeton.edu/~hhalvors/teaching/phi520_f2012/beth-theorem.pdf) - Princeton University

1. Beth, E. W. (1953), "On Padoa's Method in the Theory of Definition", Elsevier BV, [doi:10.1016/s1385-7258(53)50042-3](https://doi.org/10.1016/s1385-7258(53)50042-3)

## Sources

- [Wilfrid Hodges](/source/Wilfrid_Hodges) *A Shorter Model Theory*. Cambridge University Press, 1997.

---
Adapted from the Wikipedia article [Beth definability](https://en.wikipedia.org/wiki/Beth_definability) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/Beth_definability?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.