巴肯公式

在量化模态逻辑中，巴肯公式和相反的巴肯公式（更准确地说，是图式而不是公式）（i）在语法上陈述了量词和模态之间的互换原则；（ii）在语义上陈述了可能世界域之间的关系。

这些公式是由露丝·巴肯·马库斯 (RuthBarcanMarcus) 作为公理引入的，在模态命题逻辑的第 一个扩展中包括量化。相关的公式包括布里丹公式。

巴肯公式是。用英语来说，这个模式是这样的。如果每一个x都必然是F，那么每一个x都必须是F，这等同于◊∃xFx→∃x◊Fx{displaystyle钻石型存在xFxto钻石型存在xFx}。

巴尔坎公式产生了一些争议，因为就可能世界的语义而言，它意味着所有存在于任何可能世界（实际世界可访问的）的对象都存在于实际世界，也就是说，当人们转移到可访问的世界时，域不能增长。

这一论点有时被称为实际主义--即不存在仅仅可能的个体。

对于巴尔坎公式的非正式解释和它的反面，有一些争论。

一个反对巴尔坎公式合理性的非正式论点是将谓词Fx解释为x是一台机器，能够以实际有效的方式挖掘锁定在海浪中的所有能量。

在上面的等价形式中，前题是◊∃xFx{displaystyle`Diamond`existsxFx}，似乎是可信的，因为它是一个有价值的东西。似乎是合理的，因为至少在理论上有可能存在这样一台机器。然而，这并不明显，这意味着存在一台有可能挖掘大西洋能量的机器。

它等同于如果一个框架是基于对称的可及性关系，那么当且仅当反面的巴尔坎公式在框架中有效时，巴尔坎公式才会有效。

它指出，域不能随着人们向可及世界的移动而缩小，也就是说，个体不能停止存在。相反的巴尔坎公式被认为比巴尔坎公式更可信。