Beth property

A logic is said to have the Beth property if whenever a predicate $R$ is implicitly definable by $\varphi$ (i.e. if all models have at most one unique extension satisfying $\varphi$), then $R$ is explicitly definable relative to $\varphi$ (i.e. there is a $\psi$ not containing $R$,such that $\varphi \vDash \forall x_1,..,x_n(R(x_1,\mathrm{\dots },x_n)\leftrightarrow \psi (x_1,\mathrm{\dots },x_n))$).

Title	Beth property
Canonical name	BethProperty
Date of creation	2013-03-22 13:49:40
Last modified on	2013-03-22 13:49:40
Owner	Aatu (2569)
Last modified by	Aatu (2569)
Numerical id	7
Author	Aatu (2569)
Entry type	Definition
Classification	msc 03B99
Defines	Beth property
Defines	Beth definability property