Beth definability

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).