Barcan formula

From Wikipedia, the free encyclopedia

In quantified modal logic, the Barcan formula and the converse Barcan formula state possible relationships between quantifiers and modalities.

The Barcan formula states:

\forall x \Box A \rightarrow \Box \forall x A.

In English, the statement reads, "'For all x, it is necessary that A', implies, 'It is necessary that for all x, A'". The formula tells us that for all x in the actual world, if x is such that A in every possible world, then in every possible world, all x in those worlds are such that A. The Barcan formula has generated some controversy because it implies that all objects which exist in every possible world accessible to the actual world exist in the actual world. In other words, the domain of any accessible possible world is a subset of the domain of the actual world. This condition on domains is known as anti-monotonicity. (Anti-monotonicity and the Barcan formula are not equivalent in all modal systems.)

The Barcan formula is most often used when adding quantifiers to Clarence Irving Lewis's modal logic S5, and was first proposed by Ruth Barcan Marcus.

The converse Barcan formula states

\Box \forall x A \rightarrow \forall x \Box A.

It implies the converse condition of the Barcan formula regarding the existence of objects in the actual world and all accessible possible worlds--i.e. that nothing in this world can cease to exist. The corresponding condition on domains is called 'monotonicity' and it states that the domain of this world is a subset of the domain of any accessible possible world.

It has been proved that if a frame is based on a symmetric accessibility relation then adding either one of the Barcan or converse Barcan formulas implies the other. In this case the corresponding condition on domains is an equivalence relation.

Related formulas include the Buridian formula, and the converse Buridian formula.

[edit] External Links

Retrieved from "http://en.wikipedia.org../../../b/a/r/Barcan_formula.html"