Beth property

A logic is said to have the Beth property if whenever a predicateMathworldPlanetmathPlanetmath R is implicitly definable by ϕ (i.e. if all models have at most one unique extensionPlanetmathPlanetmath satisfying ϕ), then R is explicitly definable relative to ϕ (i.e. there is a ψ not containing R,such that ϕx1,..,xn(R(x1,,xn)ψ(x1,,xn))).

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