In 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]
For first-order logic, the theorem states that, given a theory T in the language L' ⊇ L and a formula φ in L', then the following are equivalent:
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 in a paper published in 1953. [2]
| General | |||||||||
|---|---|---|---|---|---|---|---|---|---|
| Theorems (list) and paradoxes | |||||||||
| Logics |
| ||||||||
| Set theory |
| ||||||||
| Formal systems (list), language and syntax |
| ||||||||
| Proof theory | |||||||||
| Model theory | |||||||||
| Computability theory | |||||||||
| Related | |||||||||
 | This mathematical logic-related article is a stub. You can help Wikipedia by expanding it. |
