The Beth Definability Theorem states that in first-order logic, if a theory implicitly defines a relation, meaning no two models of the theory that agree on every other symbol can disagree on that relation, then the theory in fact explicitly defines the relation by some formula built only from its other symbols. Named for Evert Willem Beth, it is a foundational model-theoretic result closely related to the Craig Interpolation Theorem, from which it can be derived.
Facts
StatementThe Beth definability theorem states that if a property is fixed uniquely by a first order theory across every model of that theory, then the theory already contains a formula in its own existing symbols that defines the property explicitly. 1 Sources
1. Beth Definability (Wikipedia)
Wikimedia Foundationlead paragraph, first sentence
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.
closing sentence of the lead, before See also
The result was first proven by Evert Willem Beth in a paper published in 1953.
View the Source Reader Challenges (0)
No disputes yet. Spotted an error or a better source? Open the first one.
Sign in to dispute this or suggest a correction.