Fórmula de Barcan
# Fórmula de Barcan

En la lógica modal cuantificada, la fórmula de Barcan y la fórmula de Barcan inversa (más exactamente, esquemas en lugar de fórmulas) (i) establecen sintácticamente principios de intercambio entre cuantificadores y modalidades; (ii) establecen semánticamente una relación entre dominios de mundos posibles. Las fórmulas fueron introducidas como axiomas por Ruth Barcan Marcus, en las primeras extensiones de la lógica modal proposicional para incluir la cuantificación.
Las fórmulas relacionadas incluyen la fórmula de Buridan.

# Fórmula de Barcan
## Fórmula de Barcan

La fórmula de Barcan es:
    $\forall x\Box Fx\rightarrow \Box \forall xFx$.
El esquema dice: Si todo x es necesariamente F, entonces es necesario que todo x sea F. Es equivalente a:
    $\Diamond \exists xFx\to \exists x\Diamond Fx$.
La fórmula de Barcan ha generado cierta controversia porque -en términos de semántica del mundo posible- implica que todos los objetos que existen en cualquier mundo posible (accesible al mundo real) existen en el mundo real, es decir, que los dominios no pueden crecer cuando uno se desplaza a mundos accesibles. Esta tesis se conoce a veces como actualismo, es decir, que no existen individuos meramente posibles. Existe cierto debate sobre la interpretación informal de la fórmula de Barcan y su inversa.
Un argumento informal contra la plausibilidad de la fórmula de Barcan sería la interpretación del predicado Fx como "x es una máquina que puede aprovechar toda la energía encerrada en las olas del Océano Atlántico de una manera práctica y eficiente". En su forma equivalente anterior, el antecedente $\Diamond \exists xFx$ parece plausible, ya que es al menos teóricamente posible que tal máquina pueda existir. Sin embargo, no es obvio que esto implique que existe una máquina que posiblemente podría aprovechar la energía del Atlántico.

# Fórmula de Barcan
## Fórmula inversa de Barcan

La fórmula inversa de Barcan es:
    $\Box \forall xFx\rightarrow \forall x\Box Fx$.
Ella es equivalente a:
    $\exists x\Diamond Fx\to \Diamond \exists xFx$.
Si un marco se basa en una relación de accesibilidad simétrica, entonces la fórmula de Barcan será válida en el marco si, y solo si, la fórmula inversa de Barcan es válida en el marco. En ella se afirma que los dominios no pueden reducirse cuando uno se desplaza a mundos accesibles, es decir, que los individuos no pueden dejar de existir. La fórmula inversa de Barcan se considera más plausible que la fórmula de Barcan.