巴坎公式

模态谓词逻辑研究中的一个重要公式。可表述为：（■ xi）□A→□（■xi）A，其中的■ 、→、□分别是“全称量词”、“实质蕴涵”和“必然”，xi是任意的个体变元，A是公式。由逻辑学家巴坎（R. C. Barcan）于1946年提出，故称，亦称“BF公式”。该公式也可表述为：（■ x i）□A■□（■xi）A或（ ■xi）◇A■◇（ ■xi）A，其中的■是“等值”。这意味着：全称量词（■ xi）和必然算子□可以交换位置，存在量词（■xi）和可能算子◇也可以交换位置。容纳巴坎公式的模态谓词逻辑系统（例如系统T+BF、S4+BF、LPC + B和LPC + S5 ），其可能世界模型中的各个世界有相同的个体域，不容纳巴坎公式的模态谓词逻辑系统（例如系统LPC + T和LPC+S4），其可能世界模型中的各个世界可以有不同的个体域。