Mathematical logic and foundations First-order logic Theorem

Beth definability theorem

Builds on Theory Model Structure Well-formed formula Craig interpolation theorem

Statement

Let $L$ be a signature, let $P$ be an $n$ -ary relation symbol not in $L$ , and let $T$ be a theory in the signature $L \cup \set{P}$ . Suppose that $P$ is implicitly defined by $T$ . That is, any two models of $T$ with the same domain and the same interpretation of each symbol of $L$ interpret $P$ alike. Then $P$ is explicitly defined by $T$ . That is, there is an $L$ -formula $\varphi(x_1, \dots, x_n)$ with $T \models \forall x_1 \cdots \forall x_n \, \big(P(x_1, \dots, x_n) \leftrightarrow \varphi(x_1, \dots, x_n)\big).$

Remarks

The converse is immediate: an explicit definition fixes $P$ in each structure for $L$ . The standard proof uses the Craig interpolation theorem. Take a copy $P'$ of $P$ and the copy $T'$ of $T$ ; implicit definability says $T \cup T' \models P(\bar x) \to P'(\bar x)$ . By compactness, finitely many sentences suffice, and an interpolant between the $P$ -side and the $P'$ -side is the required formula $\varphi$ .

Example: let $L = \set{+, \cdot, 0, 1}$ and let $T$ be the theory of real closed ordered fields, with the order symbol $\le$ in the role of $P$ . In each model of $T$ , the nonnegative elements are exactly the squares, so $\le$ is implicitly defined. An explicit definition is $x \le y \leftrightarrow \exists z \, (y = x + z \cdot z)$ .

Going deeper

For a student

The theorem was proved by Evert Willem Beth in 1953. It follows from Craig interpolation, and both results fail for many logics beyond first-order logic. In abstract model theory, logics with the Beth property are studied as those in which implicit definitions can always be made explicit.

Reading path

To understand this page from the ground up, read these 9 pages in order. The foundations come first.

Show the path as a graph

Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.

no evidence level

Logical consequence concept
Model concept
Sentence concept
Signature concept
Structure concept
Theory concept
Well-formed formula concept
Craig interpolation theorem statement
Beth definability theorem statement

Tag	`RJBDSA2ETP`
URI	`m2://RJBDSA2ETP`
Kind	statement, theorem
Writing	W0 stub
MSC	03C40
Status	This copy of the site has no build data. Run `m2 status RJBDSA2ETP`.
About	Theory
Uses	Theory, Model, Structure, Well-formed formula, Craig interpolation theorem
Same as	Wikidata Q4897670 Wikipedia Beth definability theorem
Changed	2 November 2026

Markdown · JSON · Edit on GitHub

What this page needs for W1

an inventory row: the row of the inventory that the node accounts for (0 of 1)
a source with a locator (0 of 1)

The writing levels say how complete the text of a page is. They do not measure its truth.

What links here

No page links to this page yet.