System S5 - Universal Closure


I'm not aware of this system being explicitly given a name in the literature, so I'm arbitrarily giving it the name S5-UC here. But, without giving it a name, there are a number of places that point out that it is not the same as S5 - JH

See, for example, Hughes and Creswell's "Modal Logic", the chapter on modality and existance, the comments in the Kripke semantics.) Specificly, see page 182, last paragraph.

Melvin Fitting's "First Order Modal Logic" [Fitting, 1998]covers the issue in better detail.

This system is weaker than S5, and any theorem of this system is a theorem of S5... But the converse is not true.


There is a tendency for people (particularly, for some reason, people dealing with computers people to want to assume that the axioms of S5 that are given by free variables such as:

   Lp > p

are the same as the universal closure of those same axioms:

   forall(p, Lp > p)

This is simply not the case.

The Barcan Formula:

   L (forall(x, F(x)) > forall(x, L F(x))

is a valid theorem in S5, but is *NOT* a valid theorem in the system you get when you universally quantify each axiom of S5.

The Barcan formula for quantified Modal Logic was first introduced by Ruth Barcan Marcus (publishing under her maiden name Ruth C. Barcan) in 1946 [Ruth Barcan, 1946, "A Functional Calculus of First Order Based on Strict Implication", Journal of Symbolic Logic, Vol. 11, No. 1, Mar., 1946), pp. 1-16] and later in her doctoral thesis. The validity of it in universally quantified vs free variable S5 is documented in the literature everywhere from Melvin Fitting's "First Order Modal Logic" to numerious papers, to standard textbooks like Hughes and Cresswell's "Introduction to Modal Logic".

This issue is a problem for a number of Modal Logics, but for some reason S5-UC standing in for S5 seems to be the one most common miss-labeling.


I'm unaware of any systematic analysis of which modal logic systems are, or are not, changed by universal closure. Papers in Modal Logic, and text books in the field, avoid the problem by always using the free variable forms consistantly. If anyone knows of a systematic study of which modal logics that universal closure change it would be nice if they could forward a reference to me (

Go to ...

© Copyright 2008, by John Halleck, All Rights Reserved.
This page is
This page was last modified on October 26th, 2008