贝思可定义性定理

关于形式语言表达能力的一个定理。设P是一阶语言L的一个n元谓词符号，∑是L中的一公式集，如果存在L的一个公式A(x，…，x)，P不在A中出现，使得

∑┝P(x，…，x)A(x，…，x)

就称∑明显地定义了P。设P′是L之外的一个n元谓词符号，对L的每一公式B，令B′是把P在B中每一出现换为P′而得的公式，对L的一公式集Φ，让Φ′=｛B′｜B∈Φ｝。如果

∑∪∑′┝P(x，…，x)P′(x，…，x)

就称∑隐含地定义了P。

从语义方面看，这意味着，如果和是∑的任何两个模型，和′的论域相同并且对除P以外的非逻辑符号的解释一致，则和对P的解释也一致。

E．W．贝思证明了下面的可定义性定理：

∑隐含地定义了P当且仅当它明显地定义了P。

上述定理首先由帕多瓦(Padoa，A．)在1900年提出，作为一个显然的结果而未加证明。根据贝思定理，要说明一公式∑不能明显地定义P，只需说明∑不能隐含地定义P就够了，也就是说，只需找到∑∪∑′的一个模型，在其中P和P′有不同的解释就够了。这一方法称为帕多瓦方法。