其一般定义为：按照一定的规则，用具体谓词（即代入谓词变项）、专有名词（即代入个体变项）、具体命题（即代入命题变项）等对谓词逻辑公式进行相应的替代，进而从数理逻辑的公式得到自然语言的可判定真假的形式逻辑的命题。

其严格定义为：命题B是公式A相对于个体域D的解释，当且仅当，能按以下方式从A得到B：用相对于个体域D中的个体有意义的谓词和运算符号分别替代A中的谓词变项和运算符号，并且，用D中个体的专有名词替代A中的个体常项或自由个体变项。其中，解释域是被解释公式中个体变项的个体域。